awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s₁' s₂' : Set α
x : α
h :
  (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t →
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₁ :
  (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t) →
    (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₂ : x ∈ t → x ∈ s₁ → x ∈ s₂ → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₃ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₄ : x ∈ t → x ∈ s₁ → x ∈ s₂ → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₅ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
h₆ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t
h₇ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t
h₈ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t
h₉ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t
h₁₀ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₁ : x ∈ s₁ → x ∈ t → x ∈ s₂' → ¬x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₂ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂ → x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₃ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₄ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₅ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t
h₁₆ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → x ∈ s₁'
h₁₇ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → x ∈ s₂'
h₁₈ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → ¬x ∈ t
h₁₉ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → x ∈ s₁'
h₂₀ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → x ∈ s₂'
h₂₁ : x ∈ s₁' → ¬x ∈ t → x ∈ s₂' → ¬x ∈ t → ¬((x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t) → ¬x ∈ t
h₂₂ h₂₃ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t
h₂₄ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬(x ∈ s₁ ∧ x ∈ t) → x ∈ s₁'
h₂₅ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬(x ∈ s₁ ∧ x ∈ t) → ¬x ∈ t
h₂₆ h₂₇ : x ∈ t → x ∈ s₁ → x ∈ s₂ → x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t
h₂₈ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬(x ∈ s₂ ∧ x ∈ t) → x ∈ s₂'
h₂₉ : x ∈ t → x ∈ s₁ → x ∈ s₂ → ¬(x ∈ s₂ ∧ x ∈ t) → ¬x ∈ t
h₃₀ h₃₁ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t
h₃₂ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → ¬(x ∈ s₁ ∧ x ∈ t) → x ∈ s₁'
h₃₃ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → ¬(x ∈ s₁ ∧ x ∈ t) → ¬x ∈ t
h₃₄ h₃₅ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t
h₃₆ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → ¬(x ∈ s₂ ∧ x ∈ t) → x ∈ s₂'
h₃₇ : ¬x ∈ t → x ∈ s₁' → x ∈ s₂' → ¬(x ∈ s₂ ∧ x ∈ t) → ¬x ∈ t
⊢ (x ∈ s₁ ∧ x ∈ s₂) ∧ x ∈ t ∨ (x ∈ s₁' ∧ x ∈ s₂') ∧ ¬x ∈ t ↔
    (x ∈ s₁ ∧ x ∈ t ∨ x ∈ s₁' ∧ ¬x ∈ t) ∧ (x ∈ s₂ ∧ x ∈ t ∨ x ∈ s₂' ∧ ¬x ∈ t)
have h₃₈ : x ∈ s₁ → x ∈ t → x ∈ s₂ → x ∈ t → ¬(x ∈ s₁ ∧ x ∈ s₂) → x ∈ s₁'
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s : Set α
⊢ t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s
have rw : t.ite s₁ s₂ ∩ t.ite s s = t.ite s₁ s₂ ∩ s
Tactic: rw [ite_inter_inter, ite_same]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s : Set α
rw : t.ite s₁ s₂ ∩ t.ite s s = t.ite s₁ s₂ ∩ s
⊢ t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s
have rw₁ : t.ite s₁ s₂ ∩ s = t.ite s₁ s₂ ∩ s
Tactic: rw [ite_inter_inter, ite_same]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
⊢ t.ite s₁ s₂ ∩ s = s₁ ∩ s
have rw : t.ite (s₁ ∩ s) (s₂ ∩ s) = s₁ ∩ s
Tactic: rw [← ite_inter, ← h, ite_same]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
rw : t.ite (s₁ ∩ s) (s₂ ∩ s) = s₁ ∩ s
⊢ t.ite s₁ s₂ ∩ s = s₁ ∩ s
have rw₁ : t.ite (s₁ ∩ s) (s₁ ∩ s) = s₁ ∩ s
Tactic: rw [← ite_inter, ← h, ite_same]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ s : Set α
h : s₁ ∩ s = s₂ ∩ s
rw : t.ite (s₁ ∩ s) (s₂ ∩ s) = s₁ ∩ s
rw₁ : t.ite (s₁ ∩ s) (s₁ ∩ s) = s₁ ∩ s
⊢ t.ite s₁ s₂ ∩ s = s₁ ∩ s
have rw₂ : s₁ ∩ s = s₁ ∩ s
Tactic: rw [← ite_inter, ← h, ite_same]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' u : Set α
⊢ u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'
have simp : (∀ (x : α), x ∈ u → x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
Tactic: simp only [subset_def, ← forall_and]
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' u : Set α
⊢ (∀ (x : α), x ∈ u → x ∈ t.ite s s') ↔ ∀ (x : α), (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
have refine : ∀ (x : α), x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
Tactic: refine forall_congr' fun x => ?_
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' u : Set α
x : α
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
have pos : ∀ (hx : x ∈ t), x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s s' u : Set α
x : α
pos : ∀ (hx : x ∈ t), x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
⊢ x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
have neg : ∀ (hx : ¬x ∈ t), x ∈ u → x ∈ t.ite s s' ↔ (x ∈ u ∩ t → x ∈ s) ∧ (x ∈ u \ t → x ∈ s')
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
⊢ t.ite s₁ s₂ = s₁ ∪ s₂ \ t
have h₁ : ∀ (x : α), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
have pos : ∀ (hx : x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₁ ⊆ s₂
x : α
pos : ∀ (hx : x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
have neg : ∀ (hx : ¬x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∪ s₂ \ t
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
⊢ t.ite s₁ s₂ = s₁ ∩ t ∪ s₂
have h₁ : ∀ (x : α), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
have pos : ∀ (hx : x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Order.BooleanAlgebra.Set (goal)
Goal:
α : Type u_1
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
pos : ∀ (hx : x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
have neg : ∀ (hx : ¬x ∈ t), x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
Tactic: by_cases hx : x ∈ t
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
a : α
ha : a ≤ sSup S
⊢ ∃ T ⊆ S, a = sSup T
have obtain : ∀ (C : Set α) (hC : ∀ x ∈ C, IsCompactElement x) (ha : sSup C ≤ sSup S), ∃ T ⊆ S, sSup C = sSup T
Tactic: obtain ⟨C, hC, rfl⟩ := IsCompactlyGenerated.exists_sSup_eq a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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 : α
hb : IsCompactElement b
hbS : b ≤ sSup S
⊢ ∃ T ⊆ S, b = sSup T
have obtain : ∀ (s : Finset α) (hs₁ : (↑s : Set α) ⊆ S) (hs₂ : b ≤ s.sup id), ∃ T ⊆ S, b = sSup T
Tactic: obtain ⟨s, hs₁, hs₂⟩ := (isCompactElement_iff_exists_le_sSup_of_le_sSup α b).1 hb S hbS
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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 : α
hb : IsCompactElement b
hbS : b ≤ sSup S
s : Finset α
hs₁ : (↑s : Set α) ⊆ S
hs₂ : b ≤ s.sup id
⊢ ∃ T ⊆ S, b = sSup T
have obtain : ∀ (t : Finset α) (ht : t ⊆ s) (hb : IsCompactElement (t.sup id)) (hbS : t.sup id ≤ sSup S) (hs₂ : t.sup id ≤ s.sup id),
  ∃ T ⊆ S, t.sup id = sSup T
Tactic: obtain ⟨t, ht, rfl⟩ := hS.finitelyAtomistic s b hs₁ hb hs₂
Cleared hypotheses: b, hb, hbS, hs₂
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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 ⊆ S, t.sup id = sSup T
have refine : (↑t : Set α) ⊆ S
Tactic: refine ⟨t, ?_, Finset.sup_id_eq_sSup t⟩
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
have refine : (↑t : Set α) ⊆ (↑s : Set α)
Tactic: refine Set.Subset.trans ?_ hs₁
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (hypothesis)
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 ⊆ S, sSup C = sSup T
have aux : ∀ (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
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ ∃ T ⊆ S, sSup C = sSup T
have 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
Tactic: choose T hT₁ hT₂ using aux
Cleared hypotheses: aux
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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)
⊢ ∃ T ⊆ S, sSup C = sSup T
have 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})
Tactic: use sSup {T c h₁ h₂ | (c ∈ C) (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S)}
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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)
⊢ 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})
have h : sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} ⊆ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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 {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})
have h₁ : sSup C = sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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)
⊢ sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x} ⊆ S
have 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
Tactic: apply _root_.sSup_le
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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)
⊢ sSup C = sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
have h : sSup C ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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})
⊢ sSup C = sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
have h₁ : sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}) ≤ sSup C
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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)
⊢ sSup C ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
have h : ∀ b ∈ C, b ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
Tactic: apply _root_.sSup_le
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ c ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
have h : sSup (T c sorry sorry) ≤ 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)]
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ sSup (T c ⋯ ⋯) ≤ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x})
have h : T c sorry sorry ⊆ sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
Tactic: apply sSup_le_sSup
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ T c ⋯ ⋯ ⊆ sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
have h : Membership.mem (γ := Set (Set α)) {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
  (T c sorry sorry)
Tactic: apply _root_.le_sSup
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ Membership.mem (γ := Set (Set α)) {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
    (T c ⋯ ⋯)
have w₁ : IsCompactElement c
Tactic: use c, hc, hC _ hc, (le_sSup hc).trans ha
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ Membership.mem (γ := Set (Set α)) {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
    (T c ⋯ ⋯)
have w₂ : c ≤ sSup S
Tactic: use c, hc, hC _ hc, (le_sSup hc).trans ha
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ Membership.mem (γ := Set (Set α)) {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}
    (T c ⋯ ⋯)
have h : T c sorry sorry = T c sorry sorry
Tactic: use c, hc, hC _ hc, (le_sSup hc).trans ha
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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)
⊢ sSup (sSup {x : Set α | ∃ c ∈ C, ∃ (h₁ : IsCompactElement c) (h₂ : c ≤ sSup S), T c h₁ h₂ = x}) ≤ sSup C
have 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
Tactic: simp only [Set.sSup_eq_sUnion, sSup_le_iff, Set.mem_sUnion, Set.mem_setOf_eq,
        forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ a ≤ sSup C
have h : sSup (T b hb hbS) ≤ sSup C
Tactic: apply (le_sSup haT).trans
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
⊢ sSup (T b hb hbS) ≤ sSup C
have h : b ≤ sSup C
Tactic: rw [← hT₂]
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ IsAtomistic α
have refine : ∀ (a : α), ∃ (s : Set α), a = sSup s ∧ ∀ a ∈ s, IsAtom a
Tactic: refine CompleteLattice.isAtomistic_iff.2 fun a ↦ ?_
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
⊢ ∃ (s : Set α), a = sSup s ∧ ∀ a ∈ s, IsAtom a
have obtain : ∀ (s : Set α) (hs : s ⊆ S) (hs' : a = sSup s), ∃ (s : Set α), a = sSup s ∧ ∀ a ∈ s, IsAtom a
Tactic: obtain ⟨s, hs, hs'⟩ := hS.atomistic a (h ▸ le_top)
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
S : Set α
inst_1 : IsCompactlyGenerated α
hS : BooleanGenerators S
a : α
ha : IsAtom a
haS : a ≤ sSup S
⊢ a ∈ S
have obtain : ∀ (T : Set α) (hT : T ⊆ S) (ha : IsAtom (sSup T)) (haS : sSup T ≤ sSup S), sSup T ∈ S
Tactic: obtain ⟨T, hT, rfl⟩ := hS.atomistic a haS
Cleared hypotheses: a, ha, haS