awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ≤ sSup T₁

Tactic:
exact (_root_.le_sSup hI).trans (hX'.ge.trans inf_le_left)

Premises used: Eq.ge, inf_le_left, le_sSup, LE.le.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
apply : IsAtom I
apply₁ : I ≤ sSup T₂
⊢ I ∈ T₂

Tactic:
apply (hS.mono hT₂).mem_of_isAtom_of_le_sSup_atoms _ _ _

Premises used: IsCompactlyGenerated.BooleanGenerators.mono, IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ≤ sSup T₂

Tactic:
(_root_.le_sSup hI).trans (hX'.ge.trans inf_le_right)

Premises used: Eq.ge, inf_le_right, le_sSup, LE.le.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
X : Set α
hX : X ⊆ S
hX' : sSup T₁ ⊓ sSup T₂ = sSup X
I : α
hI : I ∈ X
⊢ I ≤ sSup T₂

Tactic:
exact (_root_.le_sSup hI).trans (hX'.ge.trans inf_le_right)

Premises used: Eq.ge, inf_le_right, le_sSup, LE.le.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a b c : α
obtain : ∀ (Ta : Set α) (hTa : Ta ⊆ S), (sSup Ta ⊔ b) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ b ⊓ c
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c

Tactic:
obtain ⟨Ta, hTa, rfl⟩ := hS.atomistic a (h ▸ le_top)

Premises used: IsCompactlyGenerated.BooleanGenerators.atomistic, Eq.rec, le_top, Eq.symm, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
b c : α
Ta : Set α
hTa : Ta ⊆ S
obtain : ∀ (Tb : Set α) (hTb : Tb ⊆ S), (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ sSup Tb ⊓ c
⊢ (sSup Ta ⊔ b) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ b ⊓ c

Tactic:
obtain ⟨Tb, hTb, rfl⟩ := hS.atomistic b (h ▸ le_top)

Premises used: IsCompactlyGenerated.BooleanGenerators.atomistic, Eq.rec, le_top, Eq.symm, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
c : α
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
obtain : ∀ (Tc : Set α) (hTc : Tc ⊆ S), (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) ≤ sSup Ta ⊔ sSup Tb ⊓ sSup Tc
⊢ (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ c) ≤ sSup Ta ⊔ sSup Tb ⊓ c

Tactic:
obtain ⟨Tc, hTc, rfl⟩ := hS.atomistic c (h ▸ le_top)

Premises used: IsCompactlyGenerated.BooleanGenerators.atomistic, Eq.rec, le_top, Eq.symm, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) = sSup Ta ⊔ sSup Tb ⊓ sSup Tc
⊢ (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) ≤ sSup Ta ⊔ sSup Tb ⊓ sSup Tc

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)
hab₁ : Ta ∪ Tb ⊆ S
hab₂ : Ta ∪ Tc ⊆ S
⊢ (sSup Ta ⊔ sSup Tb) ⊓ (sSup Ta ⊔ sSup Tc) = sSup Ta ⊔ sSup Tb ⊓ sSup Tc

Tactic:
rw [← sSup_union, ← sSup_union, ← hS.sSup_inter hTb hTc, ← hS.sSup_inter, ← sSup_union]

Premises used: IsCompactlyGenerated.BooleanGenerators.sSup_inter, sSup_union
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : (Ta ∪ Tb) ∩ (Ta ∪ Tc) = Ta ∪ Tb ∩ Tc
⊢ sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)

Tactic:
congr 1
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : ∀ (x : α), x ∈ (Ta ∪ Tb) ∩ (Ta ∪ Tc) ↔ x ∈ Ta ∪ Tb ∩ Tc
⊢ (Ta ∪ Tb) ∩ (Ta ∪ Tc) = Ta ∪ Tb ∩ Tc

Tactic:
ext
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : ∀ (x : α), x ∈ (Ta ∪ Tb) ∩ (Ta ∪ Tc) ↔ x ∈ Ta ∪ Tb ∩ Tc
⊢ sSup ((Ta ∪ Tb) ∩ (Ta ∪ Tc)) = sSup (Ta ∪ Tb ∩ Tc)

Tactic:
on_goal 1 => congr 1; ext
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
x : α
hab : (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁ : x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₃ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₄ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₆ : x ∈ Ta → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₇ : x ∈ Ta → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₈ : x ∈ Tb → x ∈ Ta → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₉ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
hab₁₀ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₁ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₁₂ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tb
hab₁₃ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tc
hab₁₄ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₁₅ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₁₆ : x ∈ Tb → x ∈ Tc → x ∉ Ta → x ∈ Tb
hab₁₇ : x ∈ Tb → x ∈ Tc → x ∉ Ta → x ∈ Tc
hab₁₈ : x ∈ Ta → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₁₉ : x ∈ Tb → x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂₀ : x ∈ Ta → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂₁ : x ∈ Tb → x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
hab₂₂ : x ∈ Ta → x ∈ Ta ∨ x ∈ Tb
hab₂₃ : x ∈ Ta → x ∈ Ta ∨ x ∈ Tc
hab₂₄ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb
hab₂₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tc
hab₂₆ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₂₇ : x ∈ Ta → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₂₈ : x ∈ Ta → x ∈ Tc → x ∉ Ta → x ∈ Tb
hab₂₉ : x ∈ Tb → x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₃₀ hab₃₁ : x ∈ Ta → x ∈ Ta ∨ x ∈ Tb
hab₃₂ : x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₃₃ hab₃₄ : x ∈ Ta → x ∈ Ta ∨ x ∈ Tc
hab₃₅ : x ∈ Ta → x ∉ Ta → x ∈ Tc
hab₃₆ hab₃₇ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb
hab₃₈ : x ∈ Tb → x ∈ Tc → x ∉ Ta → x ∈ Tb
hab₃₉ hab₄₀ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tc
hab₄₁ : x ∈ Tb → x ∈ Tc → x ∉ Ta → x ∈ Tc
hab₄₂ : x ∈ Ta → x ∉ Ta → x ∈ Tb
hab₄₃ : x ∈ Ta → x ∉ Ta → x ∈ Tc
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc

Tactic:
tauto
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : Ta ⊆ S ∧ Tb ⊆ S
⊢ Ta ∪ Tb ⊆ S

Tactic:
simp only [Set.union_subset_iff, Set.mem_inter_iff, Set.mem_union]

Premises used: Set.mem_union, Set.union_subset_iff, Set.mem_inter_iff
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : Ta ⊆ S
hab₁ : Tb ⊆ S
⊢ Ta ⊆ S ∧ Tb ⊆ S

Tactic:
tauto
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : Ta ⊆ S ∧ Tc ⊆ S
⊢ Ta ∪ Tc ⊆ S

Tactic:
simp only [Set.union_subset_iff, Set.mem_inter_iff, Set.mem_union]

Premises used: Set.mem_union, Set.union_subset_iff, Set.mem_inter_iff
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
hab : Ta ⊆ S
hab₁ : Tc ⊆ S
⊢ Ta ⊆ S ∧ Tc ⊆ S

Tactic:
tauto
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
_i : DistribLattice α := hS.distribLattice_of_sSup_eq_top (S := S) h
⊢ IsAtomistic α

Tactic:
have _i₁ := isAtomistic_of_sSup_eq_top hS h
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
_i : DistribLattice α := hS.distribLattice_of_sSup_eq_top (S := S) h
_i₁ : IsAtomistic α
⊢ ComplementedLattice α

Tactic:
apply complementedLattice_of_isAtomistic

Premises used: complementedLattice_of_isAtomistic
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
⊢ sSup X ≤ sSup Y ↔ X ⊆ Y

Tactic:
⟨?_, sSup_le_sSup⟩

Premises used: Iff.intro, sSup_le_sSup
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
refine : sSup X ≤ sSup Y → X ⊆ Y
⊢ sSup X ≤ sSup Y ↔ X ⊆ Y

Tactic:
refine ⟨?_, sSup_le_sSup⟩
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
apply : IsAtom a
⊢ a ∈ Y

Tactic:
apply (hS.mono hY).mem_of_isAtom_of_le_sSup_atoms _ _ ((le_sSup ha).trans h)

Premises used: IsCompactlyGenerated.BooleanGenerators.mono, IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms, le_sSup, LE.le.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
⊢ IsAtom a

Tactic:
(hS.mono hX).isAtom a ha

Premises used: IsCompactlyGenerated.BooleanGenerators.mono, IsCompactlyGenerated.BooleanGenerators.isAtom
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
⊢ IsAtom a

Tactic:
exact (hS.mono hX).isAtom a ha

Premises used: IsCompactlyGenerated.BooleanGenerators.mono, IsCompactlyGenerated.BooleanGenerators.isAtom
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : S ≤ {a : α | IsAtom a}
a₁ : {a : α | IsAtom a} ≤ S
⊢ S = {a : α | IsAtom a}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ S ≤ {a : α | IsAtom a}

Tactic:
hS.isAtom

Premises used: IsCompactlyGenerated.BooleanGenerators.isAtom, Set.Mem, setOf, Set.Subset, IsAtom
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ S ≤ {a : α | IsAtom a}

Tactic:
exact hS.isAtom

Premises used: IsCompactlyGenerated.BooleanGenerators.isAtom
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
ha : Membership.mem (γ := Set α) {a : α | IsAtom a} a
a₁ : ∀ (T : Set α) (hT : T ⊆ S) (ha : Membership.mem (γ := Set α) {a : α | IsAtom a} (sSup T)), sSup T ∈ S
⊢ a ∈ S

Tactic:
obtain ⟨T, hT, rfl⟩ := hS.atomistic a (le_top.trans h.ge)

Premises used: Eq.ge, IsCompactlyGenerated.BooleanGenerators.atomistic, le_top, LE.le.trans, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
T : Set α
hT : T ⊆ S
ha : Membership.mem (γ := Set α) {a : α | IsAtom a} (sSup T)
⊢ sSup T ∈ S

Tactic:
hS.mem_of_isAtom_of_le_sSup_atoms _ ha (sSup_le_sSup hT)

Premises used: IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms, sSup_le_sSup
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
T : Set α
hT : T ⊆ S
ha : Membership.mem (γ := Set α) {a : α | IsAtom a} (sSup T)
⊢ sSup T ∈ S

Tactic:
exact hS.mem_of_isAtom_of_le_sSup_atoms _ ha (sSup_le_sSup hT)

Premises used: IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms, sSup_le_sSup
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M_1 : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L M : BooleanSubalgebra α
h :
  Eq.{u_2 + 1} (α := Set α) ((fun (L : BooleanSubalgebra α) ↦ L.carrier) L)
    ((fun (L : BooleanSubalgebra α) ↦ L.carrier) M)
obtain :
  ∀ (carrier : Set α) (supClosed' : SupClosed carrier) (infClosed' : InfClosed carrier)
    (compl_mem' :
      ∀ {a : α},
        a ∈ { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α }.carrier →
          aᶜ ∈ { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α }.carrier)
    (bot_mem' : ⊥ ∈ { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α }.carrier)
    (h :
      Eq.{u_2 + 1} (α := Set α)
        ((fun (L : BooleanSubalgebra α) ↦ L.carrier)
          { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed', compl_mem' := @compl_mem',
            bot_mem' := bot_mem' })
        ((fun (L : BooleanSubalgebra α) ↦ L.carrier) M)),
    { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed', compl_mem' := @compl_mem',
        bot_mem' := bot_mem' : BooleanSubalgebra α } =
      M
⊢ L = M

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := L
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L M_1 : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
M : BooleanSubalgebra α
carrier : Set α
supClosed' : SupClosed carrier
infClosed' : InfClosed carrier
compl_mem' :
  ∀ {a : α},
    a ∈ { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α }.carrier →
      aᶜ ∈ { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α }.carrier
bot_mem' : ⊥ ∈ { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed' : Sublattice α }.carrier
h :
  Eq.{u_2 + 1} (α := Set α)
    ((fun (L : BooleanSubalgebra α) ↦ L.carrier)
      { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed', compl_mem' := @compl_mem',
        bot_mem' := bot_mem' })
    ((fun (L : BooleanSubalgebra α) ↦ L.carrier) M)
⊢ { carrier := carrier, supClosed' := supClosed', infClosed' := infClosed', compl_mem' := @compl_mem',
      bot_mem' := bot_mem' : BooleanSubalgebra α } =
    M

Tactic:
congr
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : BooleanSubalgebra α
⊢ (↑L : Set α) = (↑M : Set α) ↔ L = M

Tactic:
SetLike.coe_set_eq

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ SupClosed (↑L : Set α)

Tactic:
L.supClosed'

Premises used: BooleanSubalgebra.toSublattice, Sublattice.supClosed'
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ InfClosed (↑L : Set α)

Tactic:
L.infClosed'

Premises used: Sublattice.infClosed', BooleanSubalgebra.toSublattice
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
ha : a ∈ L
⊢ aᶜ ∈ L

Tactic:
L.compl_mem' ha

Premises used: Set.Mem, BooleanSubalgebra.compl_mem'
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
ha : aᶜ ∈ L
⊢ a ∈ L

Tactic:
simpa using compl_mem ha

Premises used: BooleanSubalgebra.compl_mem
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ⊥ ∈ L

Tactic:
L.bot_mem'

Premises used: Set.Mem, BooleanSubalgebra.bot_mem'
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ ⊤ ∈ L

Tactic:
simpa using compl_mem L.bot_mem

Premises used: BooleanSubalgebra.bot_mem, BooleanSubalgebra.compl_mem
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⊔ b ∈ L

Tactic:
L.supClosed ha hb

Premises used: BooleanSubalgebra.supClosed
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⊓ b ∈ L

Tactic:
L.infClosed ha hb

Premises used: BooleanSubalgebra.infClosed
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a \ b ∈ L

Tactic:
simpa [sdiff_eq] using L.infClosed ha (compl_mem hb)

Premises used: sdiff_eq, BooleanSubalgebra.infClosed, BooleanSubalgebra.compl_mem
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a b : α
ha : a ∈ L
hb : b ∈ L
⊢ a ⇨ b ∈ L

Tactic:
simpa [himp_eq] using L.supClosed hb (compl_mem ha)

Premises used: himp_eq, BooleanSubalgebra.compl_mem, BooleanSubalgebra.supClosed
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
⊢ a ∈ L.carrier ↔ a ∈ L

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
a : α
⊢ a ∈ L.toSublattice ↔ a ∈ L

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
L : Sublattice α
h_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier
h_bot : ⊥ ∈ L.carrier
⊢ a ∈ { toSublattice := L, compl_mem' := @h_compl, bot_mem' := h_bot : BooleanSubalgebra α } ↔ a ∈ L

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : Sublattice α
h_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier
h_bot : ⊥ ∈ L.carrier
⊢ (↑{ toSublattice := L, compl_mem' := @h_compl, bot_mem' := h_bot : BooleanSubalgebra α } : Set α) = (↑L : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : Sublattice α
hL_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier
hL_bot : ⊥ ∈ L.carrier
hM_compl : ∀ {a : α}, a ∈ M.carrier → aᶜ ∈ M.carrier
hM_bot : ⊥ ∈ M.carrier
⊢ { toSublattice := L, compl_mem' := @hL_compl, bot_mem' := hL_bot : BooleanSubalgebra α } ≤
      { toSublattice := M, compl_mem' := @hM_compl, bot_mem' := hM_bot } ↔
    L ≤ M

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L M : Sublattice α
hL_compl : ∀ {a : α}, a ∈ L.carrier → aᶜ ∈ L.carrier
hL_bot : ⊥ ∈ L.carrier
hM_compl : ∀ {a : α}, a ∈ M.carrier → aᶜ ∈ M.carrier
hM_bot : ⊥ ∈ M.carrier
⊢ { toSublattice := L, compl_mem' := @hL_compl, bot_mem' := hL_bot : BooleanSubalgebra α } <
      { toSublattice := M, compl_mem' := @hM_compl, bot_mem' := hM_bot } ↔
    L < M

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s_1 t : Set α
a b : α
L : BooleanSubalgebra α
s : Set α
hs : s = (↑L : Set α)
subst : (↑L : Set α) = (↑L.toSublattice : Set α)
⊢ s = (↑L.toSublattice : Set α)

Tactic:
subst hs
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
⊢ (↑L : Set α) = (↑L.toSublattice : Set α)

Tactic:
rfl
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s_1 t : Set α
a b : α
L : BooleanSubalgebra α
s : Set α
hs : s = (↑L : Set α)
subst : ∀ {a : α}, a ∈ (L.copy (↑L : Set α) ⋯).carrier → aᶜ ∈ (L.copy (↑L : Set α) ⋯).carrier
⊢ ∀ {a : α}, a ∈ (L.copy s ⋯).carrier → aᶜ ∈ (L.copy s ⋯).carrier

Tactic:
subst hs
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice : Sublattice α := L.copy (↑L : Set α) ⋯
a_1 : α
⊢ a_1 ∈ (L.copy (↑L : Set α) ⋯).carrier → a_1ᶜ ∈ (L.copy (↑L : Set α) ⋯).carrier

Tactic:
L.compl_mem'

Premises used: Set.Mem, BooleanSubalgebra.compl_mem'
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice : Sublattice α := L.copy (↑L : Set α) ⋯
⊢ ∀ {a : α}, a ∈ (L.copy (↑L : Set α) ⋯).carrier → aᶜ ∈ (L.copy (↑L : Set α) ⋯).carrier

Tactic:
exact L.compl_mem'

Premises used: BooleanSubalgebra.compl_mem'
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s_1 t : Set α
a b : α
L : BooleanSubalgebra α
s : Set α
hs : s = (↑L : Set α)
subst : ⊥ ∈ (L.copy (↑L : Set α) ⋯).carrier
⊢ ⊥ ∈ (L.copy s ⋯).carrier

Tactic:
subst hs
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice : Sublattice α := L.copy (↑L : Set α) ⋯
⊢ ⊥ ∈ (L.copy (↑L : Set α) ⋯).carrier

Tactic:
L.bot_mem'

Premises used: Set.Mem, BooleanSubalgebra.bot_mem'
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
inst_2 : BooleanAlgebra γ
L_1 M : BooleanSubalgebra α
f : BoundedLatticeHom α β
s t : Set α
a b : α
L : BooleanSubalgebra α
__Sublattice : Sublattice α := L.copy (↑L : Set α) ⋯
⊢ ⊥ ∈ (L.copy (↑L : Set α) ⋯).carrier

Tactic:
exact L.bot_mem'

Premises used: BooleanSubalgebra.bot_mem'