awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = ⊤
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
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₈ : x ∈ Ta → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
Tactic: tauto
-- 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 = ⊤
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)
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₁₉ : x ∈ Tb → x ∈ Tc → (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc)
Tactic: tauto
-- 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 = ⊤
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)
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₂₂ : x ∈ Ta → x ∈ Ta ∨ x ∈ Tb
Tactic: tauto
-- 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 = ⊤
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
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₂₃ : x ∈ Ta → x ∈ Ta ∨ x ∈ Tc
Tactic: tauto
-- 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 = ⊤
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
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₂₄ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tb
Tactic: tauto
-- 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 = ⊤
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
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₂₅ : x ∈ Tb → x ∈ Tc → x ∈ Ta ∨ x ∈ Tc
Tactic: tauto
-- 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 = ⊤
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
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₃₂ : x ∈ Ta → x ∉ Ta → x ∈ Tb
Tactic: tauto
-- 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 = ⊤
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
⊢ (x ∈ Ta ∨ x ∈ Tb) ∧ (x ∈ Ta ∨ x ∈ Tc) ↔ x ∈ Ta ∨ x ∈ Tb ∧ x ∈ Tc
have hab₃₅ : x ∈ Ta → x ∉ Ta → x ∈ Tc
Tactic: tauto
-- 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 = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ Ta ∪ Tb ⊆ S
have hab : Ta ⊆ S ∧ Tb ⊆ S
Tactic: simp only [Set.union_subset_iff, Set.mem_inter_iff, Set.mem_union]
-- 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 = ⊤
Ta : Set α
hTa : Ta ⊆ S
Tb : Set α
hTb : Tb ⊆ S
Tc : Set α
hTc : Tc ⊆ S
⊢ Ta ∪ Tc ⊆ S
have hab : Ta ⊆ S ∧ Tc ⊆ S
Tactic: simp only [Set.union_subset_iff, Set.mem_inter_iff, Set.mem_union]
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (hypothesis)
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
⊢ ComplementedLattice α
have _i₁ : IsAtomistic α
Tactic: have _i₁ := isAtomistic_of_sSup_eq_top hS h
-- Lean 4 proof step from Mathlib.Order.BooleanGenerators (goal)
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
have refine : sSup X ≤ sSup Y → X ⊆ Y
Tactic: refine ⟨?_, 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
X Y : Set α
hX : X ⊆ S
hY : Y ⊆ S
h : sSup X ≤ sSup Y
a : α
ha : a ∈ X
⊢ a ∈ Y
have apply : IsAtom a
Tactic: apply (hS.mono hY).mem_of_isAtom_of_le_sSup_atoms _ _ ((le_sSup ha).trans h)
-- 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 = ⊤
⊢ S = {a : α | IsAtom a}
have a : S ≤ {a : α | IsAtom a}
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
h : sSup S = ⊤
a : S ≤ {a : α | IsAtom a}
⊢ S = {a : α | IsAtom a}
have a₁ : {a : α | IsAtom a} ≤ S
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
h : sSup S = ⊤
a : α
ha : Membership.mem (γ := Set α) {a : α | IsAtom a} a
⊢ a ∈ S
have a₁ : ∀ (T : Set α) (hT : T ⊆ S) (ha : Membership.mem (γ := Set α) {a : α | IsAtom a} (sSup T)), sSup T ∈ S
Tactic: obtain ⟨T, hT, rfl⟩ := hS.atomistic a (le_top.trans h.ge)
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
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)
⊢ L = M
have 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
Tactic: obtain ⟨⟨_, _⟩, _⟩ := L
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
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 α)
⊢ s = (↑L.toSublattice : Set α)
have subst : (↑L : Set α) = (↑L.toSublattice : Set α)
Tactic: subst hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
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 α)
⊢ ∀ {a : α}, a ∈ (L.copy s ⋯).carrier → aᶜ ∈ (L.copy s ⋯).carrier
have subst : ∀ {a : α}, a ∈ (L.copy (↑L : Set α) sorry).carrier → aᶜ ∈ (L.copy (↑L : Set α) sorry).carrier
Tactic: subst hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
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 α)
⊢ ⊥ ∈ (L.copy s ⋯).carrier
have subst : ⊥ ∈ (L.copy (↑L : Set α) sorry).carrier
Tactic: subst hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
⊢ (↑L : Set α) = univ ↔ L = ⊤
have rw : (↑L : Set α) = (↑⊤ : Set α) ↔ L = ⊤
Tactic: rw [← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
rw : (↑L : Set α) = (↑⊤ : Set α) ↔ L = ⊤
⊢ (↑L : Set α) = univ ↔ L = ⊤
have rw₁ : L = ⊤ ↔ L = ⊤
Tactic: rw [← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L : BooleanSubalgebra α
M : BooleanSubalgebra β
e : β ≃o α
⊢ map
        (let __src : LatticeHom α β := { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e.symm : (a : α) → β), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        L =
      M ↔
    L =
      map
        (let __src : LatticeHom β α := { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := (⇑e : (a : β) → α), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        M
have simp_rw : (↑(map
          { toFun := (⇑e.symm : (a : α) → β), map_sup' := sorry, map_inf' := sorry, map_top' := sorry, map_bot' := sorry :
            BoundedLatticeHom α β }
          L) :
      Set β) =
    (↑M : Set β) ↔
  (↑L : Set α) =
    (↑(map { toFun := (⇑e : (a : β) → α), map_sup' := sorry, map_inf' := sorry, map_top' := sorry, map_bot' := sorry } M) : Set α)
Tactic: simp_rw [← coe_inj]
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ map f (L ⊓ M) = map f L ⊓ map f M
have rw : (↑(map f (L ⊓ M)) : Set β) = (↑(map f L ⊓ map f M) : Set β)
Tactic: rw [← SetLike.coe_set_eq]
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ Membership.mem (γ := BooleanSubalgebra α) (closure s) a ↔
    ∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      a = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
have refine_1 : (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    a = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
  Membership.mem (γ := BooleanSubalgebra α) (closure s) a
Tactic: refine ⟨closure_bot_sup_induction
    (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
refine_1 :
  (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      a = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
    Membership.mem (γ := BooleanSubalgebra α) (closure s) a
⊢ Membership.mem (γ := BooleanSubalgebra α) (closure s) a ↔
    ∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      a = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
have refine_2 : ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
  (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y),
  (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      x = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
    (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
        y = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
      ∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
        x ⊔ y = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
Tactic: refine ⟨closure_bot_sup_induction
    (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
refine_1 :
  (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      a = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
    Membership.mem (γ := BooleanSubalgebra α) (closure s) a
refine_2 :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y),
    (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
        x = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
      (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
          y = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
        ∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
          x ⊔ y = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
⊢ Membership.mem (γ := BooleanSubalgebra α) (closure s) a ↔
    ∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      a = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
have refine_3 : ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x),
  (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      x = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
    ∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      xᶜ = t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
Tactic: refine ⟨closure_bot_sup_induction
    (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩