-- 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:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a x : α
h : x ∈ s
⊢ x = {(⟨x, h⟩, ⟨⊥, bot_mem⟩)}.sup fun x => ↑x.1 \ ↑x.2

Tactic:
simp

Result:
no goals

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

Tactic:
simp

Result:
no goals

Proof state:
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

Tactic:
refine t.induction ⟨{(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}, by simp⟩ fun ⟨x, y⟩ t _ ⟨tc, eq⟩ ↦ ?_

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)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x => ↑x.1 \ ↑x.2)ᶜ = t_1.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
⊢ ∃ t_1, ((insert (x, y) t).sup fun x => ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x => ↑x.1 \ ↑x.2

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
t : Finset (↑s × ↑s)
⊢ (∅.sup fun x => ↑x.1 \ ↑x.2)ᶜ = {(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}.sup fun x => ↑x.1 \ ↑x.2

Tactic:
simp

Result:
no goals

Proof state:
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)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x => ↑x.1 \ ↑x.2)ᶜ = t_1.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
⊢ ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x => ↑x.1 \ ↑x.2) = t.sup fun x => ↑x.1 \ ↑x.2

Tactic:
refine tc.induction ⟨∅, by simp⟩ fun ⟨z, w⟩ tc _ ⟨t, eq⟩ ↦ ?_

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)
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
⊢ ∃ t, ((↑x \ ↑y)ᶜ ⊓ (insert (z, w) tc).sup fun x => ↑x.1 \ ↑x.2) = t.sup fun x => ↑x.1 \ ↑x.2

Proof state:
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

Tactic:
exact t.sup_mem _ (subset_closure bot_mem) (fun _ h _ ↦ sup_mem h) _
  fun x hx ↦ sdiff_mem (subset_closure x.1.2) (subset_closure x.2.2)

Result:
no goals

Proof state:
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)
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
⊢ ∃ t_1, ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x => ↑x.1 \ ↑x.2) = t_1.sup fun x => ↑x.1 \ ↑x.2

Tactic:
use {(z, ⟨_, isSublattice.supClosed x.2 w.2⟩), (⟨_, isSublattice.infClosed y.2 z.2⟩, w)} ∪ t

Result:
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

Proof state:
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)
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
⊢ ∃ t, ((↑x \ ↑y)ᶜ ⊓ (insert (z, w) tc).sup fun x => ↑x.1 \ ↑x.2) = t.sup fun x => ↑x.1 \ ↑x.2

Tactic:
simp_rw [Finset.sup_insert, inf_sup_left, eq]

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)
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
⊢ ∃ t_1, ((↑x \ ↑y)ᶜ ⊓ ↑z \ ↑w ⊔ t.sup fun x => ↑x.1 \ ↑x.2) = t_1.sup fun x => ↑x.1 \ ↑x.2

Proof state:
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)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x => ↑x.1 \ ↑x.2)ᶜ = t_1.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
⊢ ∃ t_1, ((insert (x, y) t).sup fun x => ↑x.1 \ ↑x.2)ᶜ = t_1.sup fun x => ↑x.1 \ ↑x.2

Tactic:
simp_rw [Finset.sup_insert, compl_sup, eq]

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)
x✝² : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝¹ : ∃ t_1, (t.sup fun x => ↑x.1 \ ↑x.2)ᶜ = t_1.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
⊢ ∃ t, ((↑x \ ↑y)ᶜ ⊓ tc.sup fun x => ↑x.1 \ ↑x.2) = t.sup fun x => ↑x.1 \ ↑x.2

Proof state:
α : 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_1, (t.sup fun x => ↑x.1 \ ↑x.2)ᶜ = t_1.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 \ ↑y)ᶜ ⊓ ∅.sup fun x => ↑x.1 \ ↑x.2) = ∅.sup fun x => ↑x.1 \ ↑x.2

Tactic:
simp

Result:
no goals