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
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : (↑s : Set α) ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
refine : (↑t : Set α) ⊆ S
⊢ ∃ T ⊆ S, t.sup id = sSup T

Tactic:
refine ⟨t, ?_, Finset.sup_id_eq_sSup t⟩
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : (↑s : Set α) ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ (↑t : Set α) ⊆ S

Tactic:
Set.Subset.trans ?_ hs₁

Premises used: Set.Subset.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : (↑s : Set α) ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
refine : (↑t : Set α) ⊆ (↑s : Set α)
⊢ (↑t : Set α) ⊆ S

Tactic:
refine Set.Subset.trans ?_ hs₁

Premises used: Set.Subset.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
s : Finset α
hs₁ : (↑s : Set α) ⊆ S
t : Finset α
ht : t ⊆ s
hb : IsCompactElement (t.sup id)
hbS : t.sup id ≤ sSup S
hs₂ : t.sup id ≤ s.sup id
⊢ (↑t : Set α) ⊆ (↑s : Set α)

Tactic:
simpa only [Finset.coe_subset] using ht

Premises used: Finset.coe_subset
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
⊢ ∀ (b : α), IsCompactElement b → b ≤ sSup S → ∃ T ⊆ S, b = sSup T

Tactic:
have aux : ∀ b : α, IsCompactElement b → b ≤ sSup S → ∃ T ⊆ S, b = sSup T := by
    intro b hb hbS
    obtain ⟨s, hs₁, hs₂⟩ := (isCompactElement_iff_exists_le_sSup_of_le_sSup α b).1 hb S hbS
    obtain ⟨t, ht, rfl⟩ := hS.finitelyAtomistic s b hs₁ hb hs₂
    refine ⟨t, ?_, Finset.sup_id_eq_sSup t⟩
    refine Set.Subset.trans ?_ hs₁
    simpa only [Finset.coe_subset] using ht
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
aux : ∀ (b : α), IsCompactElement b → b ≤ sSup S → ∃ T ⊆ S, b = sSup T
choose :
  ∀ (T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α)
    (hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S)
    (hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)), ∃ T ⊆ S, sSup C = sSup T
⊢ ∃ T ⊆ S, sSup C = sSup T

Tactic:
choose T hT₁ hT₂ using aux
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
h :
  sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} ⊆ S ∧
    sSup C = sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
⊢ ∃ T ⊆ S, sSup C = sSup T

Tactic:
use sSup {T c h₁ h₂ | (c ∈ C) (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S)}

Premises used: setOf, Membership.mem, Exists, And, Eq, SupSet.sSup
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
h : sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} ⊆ S
h₁ : sSup C = sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
⊢ sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} ⊆ S ∧
    sSup C = sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

Tactic:
constructor
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
h :
  ∀ (b : Set α),
    Membership.mem (γ := Set (Set α))
        {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} b →
      b ≤ S
⊢ sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} ⊆ S

Tactic:
apply _root_.sSup_le

Premises used: sSup_le
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
c : α
h₁ : IsCompactElement c
h₂ : c ≤ sSup S
⊢ T c h₁ h₂ ≤ S

Tactic:
apply hT₁
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
h : sSup C ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
h₁ : sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}) ≤ sSup C
⊢ sSup C = sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

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
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
h : ∀ b ∈ C, b ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
⊢ sSup C ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

Tactic:
apply _root_.sSup_le

Premises used: sSup_le
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
c : α
hc : c ∈ C
h : sSup (T c ⋯ ⋯) ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
⊢ c ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

Tactic:
rw [hT₂ c (hC _ hc) ((le_sSup hc).trans ha)]

Premises used: le_sSup, LE.le.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
c : α
hc : c ∈ C
h : T c ⋯ ⋯ ⊆ sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
⊢ sSup (T c ⋯ ⋯) ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})

Tactic:
apply sSup_le_sSup

Premises used: sSup_le_sSup
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
c : α
hc : c ∈ C
h :
  Membership.mem (γ := Set (Set α)) {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
    (T c ⋯ ⋯)
⊢ T c ⋯ ⋯ ⊆ sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}

Tactic:
apply _root_.le_sSup

Premises used: le_sSup
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
c : α
hc : c ∈ C
w : α
left : c ∈ C
w₁ : IsCompactElement c
w₂ : c ≤ sSup S
h : T c ⋯ ⋯ = T c ⋯ ⋯
⊢ Membership.mem (γ := Set (Set α)) {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
    (T c ⋯ ⋯)

Tactic:
use c, hc, hC _ hc, (le_sSup hc).trans ha

Premises used: le_sSup, LE.le.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
h :
  ∀ (b : α) (x : Set α),
    ∀ x_1 ∈ C, ∀ (x_2 : IsCompactElement x_1) (x_3 : x_1 ≤ sSup S) (h : T x_1 x_2 x_3 = x), b ∈ x → b ≤ sSup C
⊢ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}) ≤ sSup C

Tactic:
simp only [Set.sSup_eq_sUnion, sSup_le_iff, Set.mem_sUnion, Set.mem_setOf_eq,
        forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, Set.mem_setOf_eq, Set.sSup_eq_sUnion, sSup_le_iff, Set.mem_sUnion
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
a b : α
hbC : b ∈ C
hb : IsCompactElement b
hbS : b ≤ sSup S
haT : a ∈ T b hb hbS
h : sSup (T b hb hbS) ≤ sSup C
⊢ a ≤ sSup C

Tactic:
apply (le_sSup haT).trans

Premises used: le_sSup, LE.le.trans
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
a b : α
hbC : b ∈ C
hb : IsCompactElement b
hbS : b ≤ sSup S
haT : a ∈ T b hb hbS
h : b ≤ sSup C
⊢ sSup (T b hb hbS) ≤ sSup C

Tactic:
rw [← hT₂]
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
a b : α
hbC : b ∈ C
hb : IsCompactElement b
hbS : b ≤ sSup S
haT : a ∈ T b hb hbS
⊢ b ≤ sSup C

Tactic:
le_sSup hbC

Premises used: le_sSup
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
C : Set α
hC : ∀ x ∈ C, IsCompactElement x
ha : sSup C ≤ sSup S
T : (b : α) → IsCompactElement b → b ≤ sSup S → Set α
hT₁ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), T b a a_1 ⊆ S
hT₂ : ∀ (b : α) (a : IsCompactElement b) (a_1 : b ≤ sSup S), b = sSup (T b a a_1)
a b : α
hbC : b ∈ C
hb : IsCompactElement b
hbS : b ≤ sSup S
haT : a ∈ T b hb hbS
⊢ b ≤ sSup C

Tactic:
exact le_sSup hbC

Premises used: le_sSup
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ IsAtomistic α

Tactic:
CompleteLattice.isAtomistic_iff.2 fun a ↦ ?_

Premises used: Iff.mpr, CompleteLattice.isAtomistic_iff
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
refine : ∀ (a : α), ∃ (s : Set α), a = sSup s ∧ ∀ a ∈ s, IsAtom a
⊢ IsAtomistic α

Tactic:
refine CompleteLattice.isAtomistic_iff.2 fun a ↦ ?_

Premises used: Iff.mpr, CompleteLattice.isAtomistic_iff
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
obtain : ∀ (s : Set α) (hs : s ⊆ S) (hs' : a = sSup s), ∃ (s : Set α), a = sSup s ∧ ∀ a ∈ s, IsAtom a
⊢ ∃ (s : Set α), a = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
obtain ⟨s, hs, hs'⟩ := hS.atomistic a (h ▸ le_top)

Premises used: IsCompactlyGenerated.BooleanGenerators.atomistic, Eq.rec, le_top, Eq.symm
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
s : Set α
hs : s ⊆ S
hs' : a = sSup s
⊢ ∃ (s : Set α), a = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
⟨s, hs', fun I hI ↦ hS.isAtom I (hs hI)⟩

Premises used: IsCompactlyGenerated.BooleanGenerators.isAtom, And.intro, Exists.intro
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
s : Set α
hs : s ⊆ S
hs' : a = sSup s
⊢ ∃ (s : Set α), a = sSup s ∧ ∀ a ∈ s, IsAtom a

Tactic:
exact ⟨s, hs', fun I hI ↦ hS.isAtom I (hs hI)⟩
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
a : α
ha : IsAtom a
haS : a ≤ sSup S
obtain : ∀ (T : Set α) (hT : T ⊆ S) (ha : IsAtom (sSup T)) (haS : sSup T ≤ sSup S), sSup T ∈ S
⊢ a ∈ S

Tactic:
obtain ⟨T, hT, rfl⟩ := hS.atomistic a haS

Premises used: IsCompactlyGenerated.BooleanGenerators.atomistic, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
inl : ∀ (hT : ∅ ⊆ S) (ha : IsAtom.{u_1} (α := α) (sSup ∅)) (haS : sSup ∅ ≤ sSup S), sSup ∅ ∈ S
inr : ∀ (a : α) (haT : a ∈ T), sSup T ∈ S
⊢ sSup T ∈ S

Tactic:
obtain rfl | ⟨a, haT⟩ := T.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
hT : ∅ ⊆ S
ha : IsAtom.{u_1} (α := α) (sSup ∅)
haS : sSup ∅ ≤ sSup S
⊢ IsAtom.{u_1} (α := α) ⊥

Tactic:
simp only [sSup_empty] at ha

Premises used: sSup_empty
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
hT : ∅ ⊆ S
haS : sSup ∅ ≤ sSup S
ha : IsAtom.{u_1} (α := α) ⊥
⊢ sSup ∅ ∈ S

Tactic:
(ha.1 rfl).elim

Premises used: False.elim, And.left, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
hT : ∅ ⊆ S
haS : sSup ∅ ≤ sSup S
ha : IsAtom.{u_1} (α := α) ⊥
⊢ sSup ∅ ∈ S

Tactic:
exact (ha.1 rfl).elim

Premises used: False.elim, And.left, rfl
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
inr : sSup T = a
⊢ sSup T ∈ S

Tactic:
suffices sSup T = a from this ▸ hT haT
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
⊢ a ≤ sSup T

Tactic:
have : a ≤ sSup T := le_sSup haT
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
this : a ≤ sSup T
inr : a ≠ ⊥
⊢ sSup T = a

Tactic:
rwa [ha.le_iff_eq, eq_comm] at this

Premises used: eq_comm, IsAtom.le_iff_eq
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
this : a ≤ sSup T
⊢ a ≠ ⊥

Tactic:
(hS.isAtom a (hT haT)).1

Premises used: IsCompactlyGenerated.BooleanGenerators.isAtom, And.left
-- Module: Mathlib.Order.BooleanGenerators
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
T : Set α
hT : T ⊆ S
ha : IsAtom (sSup T)
haS : sSup T ≤ sSup S
a : α
haT : a ∈ T
this : a ≤ sSup T
⊢ a ≠ ⊥

Tactic:
exact (hS.isAtom a (hT haT)).1

Premises used: IsCompactlyGenerated.BooleanGenerators.isAtom, And.left
-- 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
a : sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂
a₁ : sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
⊢ sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂

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
T₁ T₂ : Set α
hT₁ : T₁ ⊆ S
hT₂ : T₂ ⊆ S
a : sSup (T₁ ∩ T₂) ≤ sSup T₁
a₁ : sSup (T₁ ∩ T₂) ≤ sSup T₂
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₁ ⊓ sSup T₂

Tactic:
apply le_inf

Premises used: le_inf
-- 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
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₁

Tactic:
apply sSup_le_sSup Set.inter_subset_left

Premises used: Set.inter_subset_left, sSup_le_sSup
-- 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
⊢ sSup (T₁ ∩ T₂) ≤ sSup T₂

Tactic:
apply sSup_le_sSup Set.inter_subset_right

Premises used: sSup_le_sSup, Set.inter_subset_right
-- 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
a : ∀ (X : Set α) (hX : X ⊆ S) (hX' : sSup T₁ ⊓ sSup T₂ = sSup X), sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)
⊢ sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)

Tactic:
obtain ⟨X, hX, hX'⟩ := hS.atomistic (sSup T₁ ⊓ sSup T₂) (inf_le_left.trans (sSup_le_sSup hT₁))

Premises used: IsCompactlyGenerated.BooleanGenerators.atomistic, inf_le_left, LE.le.trans, sSup_le_sSup, Min.min, SupSet.sSup
-- 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
a : sSup X ≤ sSup (T₁ ∩ T₂)
⊢ sSup T₁ ⊓ sSup T₂ ≤ sSup (T₁ ∩ T₂)

Tactic:
rw [hX']
-- 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
a : ∀ b ∈ X, b ≤ sSup (T₁ ∩ T₂)
⊢ sSup X ≤ sSup (T₁ ∩ T₂)

Tactic:
apply _root_.sSup_le

Premises used: sSup_le
-- 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
a : I ∈ T₁ ∩ T₂
⊢ I ≤ sSup (T₁ ∩ T₂)

Tactic:
apply _root_.le_sSup

Premises used: le_sSup
-- 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
a : I ∈ T₁
a₁ : I ∈ T₂
⊢ I ∈ T₁ ∩ T₂

Tactic:
constructor
-- 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
⊢ IsAtom I

Tactic:
(hS.mono hX).isAtom I hI

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
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
⊢ IsAtom I

Tactic:
exact (hS.mono hX).isAtom I hI

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
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_left)

Premises used: Eq.ge, inf_le_left, le_sSup, LE.le.trans