-- Mathlib/Order/BooleanSubalgebra.lean
theorem mem_closure_iff_sup_sdiff {a : α} :
    a ∈ closure s ↔ ∃ t : Finset (s × s), a = t.sup fun x ↦ x.1.1 \ x.2.1

Proof state:
case h
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t✝¹ : Finset (↑s × ↑s)
x✝⁵ : ↑s × ↑s
t✝ : Finset (↑s × ↑s)
x✝⁴ : ∃ t, (t✝.sup fun x => ↑x.1 \ ↑x.2)ᶜ = t.sup fun x => ↑x.1 \ ↑x.2
x y : ↑s
x✝³ : (x, y) ∉ t✝
tc✝ : Finset (↑s × ↑s)
eq✝ : (t✝.sup fun x => ↑x.1 \ ↑x.2)ᶜ = tc✝.sup fun x => ↑x.1 \ ↑x.2
x✝² : ↑s × ↑s
tc : Finset (↑s × ↑s)
x✝¹ : ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x => ↑x.1 \ ↑x.2) = t.sup fun x => ↑x.1 \ ↑x.2
z w : ↑s
x✝ : (z, w) ∉ tc
t : Finset (↑s × ↑s)
eq : ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x => ↑x.1 \ ↑x.2) = t.sup fun x => ↑x.1 \ ↑x.2
⊢ ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x => ↑x.1 \ ↑x.2) =
    ({(z, ⟨↑x ⊔ ↑w, ⋯⟩), (⟨↑y ⊓ ↑z, ⋯⟩, w)} ∪ t).sup fun x => ↑x.1 \ ↑x.2

Tactic:
simp_rw [Finset.sup_union, Finset.sup_insert, Finset.sup_singleton, sdiff_eq,
  compl_sup, inf_left_comm z.1, compl_inf, compl_compl, inf_sup_right, inf_assoc]

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ (∃ t, a = t.sup fun x => ↑x.1 \ ↑x.2) → a ∈ closure s

Tactic:
rintro ⟨t, rfl⟩

Result:
case refine_1.intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
t : Finset (↑s × ↑s)
⊢ (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t₁ t₂ : Finset (↑s × ↑s)
⊢ ((t₁.sup fun x => ↑x.1 \ ↑x.2) ⊔ t₂.sup fun x => ↑x.1 \ ↑x.2) = (t₁ ∪ t₂).sup fun x => ↑x.1 \ ↑x.2

Tactic:
rw [Finset.sup_union]

Result:
no goals

Proof state:
case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s, (∃ t, x = t.sup fun x => ↑x.1 \ ↑x.2) → ∃ t, xᶜ = t.sup fun x => ↑x.1 \ ↑x.2

Tactic:
rintro x - ⟨t, rfl⟩

Result:
case refine_3.intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t : Finset (↑s × ↑s)
⊢ ∃ t_1, (t.sup fun x => ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x => ↑x.1 \ ↑x.2

Proof state:
case refine_2
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s,
    ∀ y ∈ closure s,
      (∃ t, x = t.sup fun x => ↑x.1 \ ↑x.2) →
        (∃ t, y = t.sup fun x => ↑x.1 \ ↑x.2) → ∃ t, x ⊔ y = t.sup fun x => ↑x.1 \ ↑x.2

Tactic:
rintro _ - _ - ⟨t₁, rfl⟩ ⟨t₂, rfl⟩

Result:
case refine_2.intro.intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t₁ t₂ : Finset (↑s × ↑s)
⊢ ∃ t, ((t₁.sup fun x => ↑x.1 \ ↑x.2) ⊔ t₂.sup fun x => ↑x.1 \ ↑x.2) = t.sup fun x => ↑x.1 \ ↑x.2

Proof state:
case refine_2.intro.intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t₁ t₂ : Finset (↑s × ↑s)
⊢ ∃ t, ((t₁.sup fun x => ↑x.1 \ ↑x.2) ⊔ t₂.sup fun x => ↑x.1 \ ↑x.2) = t.sup fun x => ↑x.1 \ ↑x.2

Tactic:
exact ⟨t₁ ∪ t₂, by rw [Finset.sup_union]⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ a ∈ closure s ↔ ∃ t, a = t.sup fun x => ↑x.1 \ ↑x.2

Tactic:
refine ⟨closure_bot_sup_induction
  (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩

Result:
case refine_1
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ (∃ t, a = t.sup fun x => ↑x.1 \ ↑x.2) → a ∈ closure s

case refine_2
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s,
    ∀ y ∈ closure s,
      (∃ t, x = t.sup fun x => ↑x.1 \ ↑x.2) →
        (∃ t, y = t.sup fun x => ↑x.1 \ ↑x.2) → ∃ t, x ⊔ y = t.sup fun x => ↑x.1 \ ↑x.2

case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s, (∃ t, x = t.sup fun x => ↑x.1 \ ↑x.2) → ∃ t, xᶜ = t.sup fun x => ↑x.1 \ ↑x.2