awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ t₂ : 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₂.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
    ((t₁ ∪ t₂).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
have rw : Eq (α := α)
  ((t₁.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₁.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: rw [Finset.sup_union]
-- 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 : 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 : α))
have refine_3 : ∀ (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 : α))
Tactic: refine t.induction ⟨{(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}, by simp⟩ fun ⟨x, y⟩ t _ ⟨tc, eq⟩ ↦ ?_
-- 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 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
h :
  ∃ (t_2 : 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_2.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
x y : (↑s : Type u_2)
h_1 : (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_2 : 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_2.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 : α) \ (↑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 : α)
Tactic: simp_rw [Finset.sup_insert, compl_sup, eq]
-- 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 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
h :
  ∃ (t_2 : 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_2.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
x y : (↑s : Type u_2)
h_1 : (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 : α)
have refine_3 : ∀ (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: refine tc.induction ⟨∅, by simp⟩ fun ⟨z, w⟩ tc _ ⟨t, eq⟩ ↦ ?_
-- 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 :
  ∃ (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_1 : (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_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)
h_3 : (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 : α)
have refine_3 : ∃ (t_3 : 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_3.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
Tactic: simp_rw [Finset.sup_insert, inf_sup_left, eq]
-- 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 :
  ∃ (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_1 : (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_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)
h_3 : (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_3 : 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_3.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, Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑x : α) ⊔ (↑w : α)) sorry),
          (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑y : α) ⊓ (↑z : α)) sorry, w)} ∪
        t).sup
    fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)
Tactic: use {(z, ⟨_, isSublattice.supClosed x.2 w.2⟩), (⟨_, isSublattice.infClosed y.2 z.2⟩, w)} ∪ t
-- 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 :
  ∃ (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_1 : (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_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)
h_3 : (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 : α)
have 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 : α)) sorry),
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑y : α) ⊓ (↑z : α)) sorry, 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 : α)
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]
-- 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 : α)
⊢ (((↑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 : α)) ⊔
      Finset.sup {(Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑y : α) ⊓ (↑z : α)) sorry, 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 : α)
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]
-- 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 : α
⊢ 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_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
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]
-- 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
⊢ 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_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 : α)
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]
-- 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 : α)
⊢ 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 : ∀ (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 : α)
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]
-- 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
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
x : α
hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x
⊢ p x hx
have obtain : ∀ (t : Finset ((↑s : Type u_2) × (↑s : Type u_2)))
  (hx :
    Membership.mem (γ := BooleanSubalgebra α) (closure s)
      (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
  p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
Tactic: obtain ⟨t, rfl⟩ := (mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mp hx
Cleared hypotheses: x, hx
-- 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
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
hx :
  Membership.mem (γ := BooleanSubalgebra α) (closure s)
    (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
⊢ p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
have revert : ∀
  (hx :
    Membership.mem (γ := BooleanSubalgebra α) (closure s)
      (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
  p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
Tactic: revert hx
Cleared hypotheses: hx