-- 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 : α)
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 : α)
⊢ 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₆ : ∀ (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 : α)
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]