-- Module: Mathlib.Order.BooleanSubalgebra
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 : α)
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 : α)
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 : α)
refine_3₁ 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 : α)
refine_3₃ :
  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    ∃ (t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
      Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
        (t_1.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
refine_3₄ :
  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))) (x : (↑s : Type u_2) × (↑s : Type u_2))
    (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    (∃ (t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
        Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
          (t_1.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))) →
      ∀ (x y : (↑s : Type u_2)),
        (x, y) ∉ t →
          ∀ (tc : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
            (eq :
              Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
                (tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
            ∃ (t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
              Eq (α := α) ((insert (x, y) t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
                (t_1.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
refine_3₅ :
  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))) (x : (↑s : Type u_2) × (↑s : Type u_2))
    (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    (∃ (t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
        Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
          (t_1.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))) →
      ∀ (x y : (↑s : Type u_2)),
        (x, y) ∉ t →
          ∀ (tc : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
            (eq :
              Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
                (tc.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 : α))ᶜ ⊓ tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
refine_3₆ :
  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))) (x : (↑s : Type u_2) × (↑s : Type u_2))
    (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    (∃ (t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
        Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
          (t_1.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))) →
      ∀ (x y : (↑s : Type u_2)),
        (x, y) ∉ t →
          ∀ (tc : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
            (eq :
              Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
                (tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)))
            (x_2 : (↑s : Type u_2) × (↑s : Type u_2)) (tc : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
            (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
                (((↑x : α) \ (↑y : α))ᶜ ⊓
                    tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                  t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
              ∀ (z w : (↑s : Type u_2)),
                (z, w) ∉ tc →
                  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
                    (eq :
                      (((↑x : α) \ (↑y : α))ᶜ ⊓
                          tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                        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 : α))ᶜ ⊓
                          (insert (z, w) tc).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦
                            (↑x.1 : α) \ (↑x.2 : α)) =
                        t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
refine_3₇ :
  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))) (x : (↑s : Type u_2) × (↑s : Type u_2))
    (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    (∃ (t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
        Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
          (t_1.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))) →
      ∀ (x y : (↑s : Type u_2)),
        (x, y) ∉ t →
          ∀ (tc : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
            (eq :
              Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
                (tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)))
            (x_2 : (↑s : Type u_2) × (↑s : Type u_2)) (tc : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
            (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
                (((↑x : α) \ (↑y : α))ᶜ ⊓
                    tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                  t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
              ∀ (z w : (↑s : Type u_2)),
                (z, w) ∉ tc →
                  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
                    (eq :
                      (((↑x : α) \ (↑y : α))ᶜ ⊓
                          tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                        t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)),
                    ∃ (t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
                      (((↑x : α) \ (↑y : α))ᶜ ⊓ (↑z : α) \ (↑w : α) ⊔
                          t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                        t_1.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
h :
  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))) (x : (↑s : Type u_2) × (↑s : Type u_2))
    (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    (∃ (t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
        Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
          (t_1.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))) →
      ∀ (x y : (↑s : Type u_2)),
        (x, y) ∉ t →
          ∀ (tc : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
            (eq :
              Eq (α := α) (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
                (tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)))
            (x_2 : (↑s : Type u_2) × (↑s : Type u_2)) (tc : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
            (∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
                (((↑x : α) \ (↑y : α))ᶜ ⊓
                    tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                  t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) →
              ∀ (z w : (↑s : Type u_2)),
                (z, w) ∉ tc →
                  ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
                    (eq :
                      (((↑x : α) \ (↑y : α))ᶜ ⊓
                          tc.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                        t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)),
                    (((↑x : α) \ (↑y : α))ᶜ ⊓ (↑z : α) \ (↑w : α) ⊔
                        t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
                      ({(z, Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑x : α) ⊔ (↑w : α)) ⋯),
                              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑y : α) ⊓ (↑z : α)) ⋯, w)} ∪
                            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 : α)

Tactic:
classical
  refine ⟨closure_bot_sup_induction
    (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩
  · rintro ⟨t, rfl⟩
    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)
  · rintro _ - _ - ⟨t₁, rfl⟩ ⟨t₂, rfl⟩
    exact ⟨t₁ ∪ t₂, by rw [Finset.sup_union]⟩
  rintro x - ⟨t, rfl⟩
  refine t.induction ⟨{(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}, by simp⟩ fun ⟨x, y⟩ t _ ⟨tc, eq⟩ ↦ ?_
  simp_rw [Finset.sup_insert, compl_sup, eq]
  refine tc.induction ⟨∅, by simp⟩ fun ⟨z, w⟩ tc _ ⟨t, eq⟩ ↦ ?_
  simp_rw [Finset.sup_insert, inf_sup_left, eq]
  use {(z, ⟨_, isSublattice.supClosed x.2 w.2⟩), (⟨_, isSublattice.infClosed y.2 z.2⟩, w)} ∪ t
  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]

Premises used: compl_inf, Finset.sup_insert, compl_compl, Finset.sup_singleton, sdiff_eq, inf_sup_right, Finset.sup_union, inf_sup_left, compl_sup, inf_assoc, rfl