-- 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 : α
t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
x_1 : (↑s : Type u_2) × (↑s : Type u_2)
t_2 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
h_1 :
  ∃ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    Eq (α := α) (t_2.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 : (↑s : Type u_2)
h_2 : (x, y) ∉ t_2
tc_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
eq_1 :
  Eq (α := α) (t_2.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
    (tc_1.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))
h_3 :
  ∃ (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)
h_4 : (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 : α)
h :
  (((↑x : α) \ (↑y : α))ᶜ ⊓ (↑z : α) \ (↑w : α) ⊔
      t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
    (Finset.sup
        {(z, Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑x : α) ⊔ (↑w : α)) ⋯),
          (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑y : α) ⊓ (↑z : α)) ⋯, w)}
        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 : α)
h₁ :
  (((↑x : α) \ (↑y : α))ᶜ ⊓ (↑z : α) \ (↑w : α) ⊔
      t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
    ((↑z : α) \ ((↑x : α) ⊔ (↑w : α)) ⊔
        Finset.sup {(Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑y : α) ⊓ (↑z : α)) ⋯, w)}
          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 : α)
h₂ :
  (((↑x : α) \ (↑y : α))ᶜ ⊓ (↑z : α) \ (↑w : α) ⊔
      t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
    (↑z : α) \ ((↑x : α) ⊔ (↑w : α)) ⊔ ((↑y : α) ⊓ (↑z : α)) \ (↑w : α) ⊔
      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 : α)
have h₃ : (((↑x : α) ⊓ (↑y : α)ᶜ)ᶜ ⊓ ((↑z : α) ⊓ (↑w : α)ᶜ) ⊔
    t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) ⊓ (↑x.2 : α)ᶜ) =
  (↑z : α) ⊓ ((↑x : α) ⊔ (↑w : α))ᶜ ⊔ (↑y : α) ⊓ (↑z : α) ⊓ (↑w : α)ᶜ ⊔
    t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑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]