stacks 005H

leanprover-community · Dec 26, 2024 · 2a50c59 · 2a50c59
1 parent cccb6fe
commit 2a50c59
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/Mathlib/Order/BooleanSubalgebra.lean b/Mathlib/Order/BooleanSubalgebra.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Order.Sublattice
+import Mathlib.Tactic.StacksAttribute
 
 /-!
 # Boolean subalgebras
@@ -366,7 +367,7 @@ section sdiff_sup
 variable (sup : SupClosed s) (inf : InfClosed s) (bot_mem : ⊥ ∈ s) (top_mem : ⊤ ∈ s)
 include sup inf bot_mem top_mem
 
-theorem mem_closure_iff_sup_sdiff {a : α} :
+@[stacks 005H] theorem mem_closure_iff_sup_sdiff {a : α} :
     a ∈ closure s ↔ ∃ t : Finset (s × s), a = t.sup fun x ↦ x.1.1 \ x.2.1 := by
   classical
   refine ⟨closure_bot_sup_induction