awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L M : BooleanSubalgebra β
f : BoundedLatticeHom α β
⊢ comap f L ⊔ comap f M ≤ comap f (L ⊔ M)

Tactic:
comap_mono.le_map_sup _ _

Premises used: Monotone.le_map_sup, BooleanSubalgebra.comap_mono
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
L : ι → BooleanSubalgebra β
⊢ ⨆ (i : ι), comap f (L i) ≤ comap f (⨆ (i : ι), L i)

Tactic:
comap_mono.le_map_iSup

Premises used: Set.Mem, Monotone.le_map_iSup, BooleanSubalgebra.comap_mono
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
rw : (↑(map f (L ⊓ M)) : Set β) = (↑(map f L ⊓ map f M) : Set β)
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
rw [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ (↑(map f (L ⊓ M)) : Set β) = (↑(map f L ⊓ map f M) : Set β)

Tactic:
simp [Set.image_inter hf]

Premises used: Set.image_inter
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
β : Type u_3
inst : BooleanAlgebra α
inst_1 : BooleanAlgebra β
f : BoundedLatticeHom α β
h : Surjective.{u_2 + 1, u_3 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ (↑(map f ⊤) : Set β) = (↑⊤ : Set β)

Tactic:
simp [h.range_eq]

Premises used: Function.Surjective.range_eq
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
x : α
⊢ Membership.mem (γ := BooleanSubalgebra α) (closure s) x ↔ ∀ ⦃L : BooleanSubalgebra α⦄, s ⊆ (↑L : Set α) → x ∈ L

Tactic:
mem_sInf

Premises used: Set.Mem, setOf, BooleanSubalgebra.mem_sInf
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
⊢ s ⊆ (↑(closure s) : Set α)

Tactic:
fun _ hx ↦ mem_closure.2 fun _ hK ↦ hK hx

Premises used: Iff.mpr, Set.Subset, BooleanSubalgebra.mem_closure
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
x : α
hx : x ∈ s
⊢ Membership.mem (γ := BooleanSubalgebra α) (closure s) x

Tactic:
subset_closure hx

Premises used: BooleanSubalgebra.subset_closure
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
L : BooleanSubalgebra α
s : Set α
⊢ closure s ≤ L ↔ s ⊆ (↑L : Set α)

Tactic:
⟨subset_closure.trans, fun h ↦ sInf_le h⟩

Premises used: HasSubset.Subset.trans, BooleanSubalgebra.subset_closure, sInf_le, Iff.intro
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
t s : Set α
hst : s ⊆ t
⊢ LE.le (α := BooleanSubalgebra α) (closure s) (closure t)

Tactic:
sInf_le_sInf fun _L ↦ hst.trans

Premises used: Set.Mem, sInf_le_sInf, HasSubset.Subset.trans
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
⊢ (latticeClosure : (a : Set α) → Set α) s ⊆ (↑(closure s) : Set α)

Tactic:
latticeClosure_min subset_closure (closure s).isSublattice

Premises used: BooleanSubalgebra.closure, Sublattice.isSublattice, BooleanSubalgebra.toSublattice, BooleanSubalgebra.subset_closure, latticeClosure_min
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
⊢ Eq (α := BooleanSubalgebra α) (closure ((latticeClosure : (a : Set α) → Set α) s)) (closure s)

Tactic:
le_antisymm (closure_le.2 latticeClosure_subset_closure) (closure_mono subset_latticeClosure)

Premises used: Iff.mpr, BooleanSubalgebra.closure_mono, BooleanSubalgebra.closure_le, subset_latticeClosure, BooleanSubalgebra.latticeClosure_subset_closure, le_antisymm
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
mem : ∀ (x : α) (hx : x ∈ s), p x ⋯
bot : p ⊥ ⋯
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) ⋯
compl : ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x), p x hx → p xᶜ ⋯
x_1 : α
hx_1 : Membership.mem (γ := BooleanSubalgebra α) (closure s) x_1
x : α
hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x
y : α
hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y
hx' : p x hx
hy' : p y hy
⊢ p (x ⊓ y) ⋯

Tactic:
simpa using compl _ _ <| sup _ _ _ _ (compl _ _ hx') (compl _ _ hy')
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a x : α
h : x ∈ s
⊢ x =
    Finset.sup {(Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h, Subtype.mk (p := fun (x : α) ↦ x ∈ s) ⊥ bot_mem)}
      fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ Eq.{u_2 + 1} (α := α) ⊥ (Finset.sup ∅ fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))

Tactic:
simp
-- 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 : α)
⊢ 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:
refine ⟨closure_bot_sup_induction
    (fun x h ↦ ⟨{(⟨x, h⟩, ⟨⊥, bot_mem⟩)}, by simp⟩) ⟨∅, by simp⟩ ?_ ?_, ?_⟩
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
⊢ Membership.mem (γ := BooleanSubalgebra α) (closure s)
    (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))

Tactic:
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)

Premises used: BooleanSubalgebra.sup_mem, BooleanSubalgebra.sdiff_mem, Prod.fst, BooleanSubalgebra.subset_closure, Finset.sup_mem, Prod.snd, Subtype.property
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
⊢ Membership.mem (γ := BooleanSubalgebra α) (closure s)
    (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))

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)

Premises used: BooleanSubalgebra.sup_mem, BooleanSubalgebra.sdiff_mem, Prod.fst, BooleanSubalgebra.subset_closure, Finset.sup_mem, Prod.snd, Subtype.property
-- Module: Mathlib.Order.BooleanSubalgebra
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))
rw 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 : α))
⊢ 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 : α))

Tactic:
rw [Finset.sup_union]

Premises used: Finset.sup_union
-- Module: Mathlib.Order.BooleanSubalgebra
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))
⊢ ∃ (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.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))

Tactic:
exact ⟨t₁ ∪ t₂, by rw [Finset.sup_union]⟩
-- Module: Mathlib.Order.BooleanSubalgebra
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))
⊢ Eq (α := α) (Finset.sup ∅ fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))ᶜ
    (Finset.sup {(Subtype.mk (p := fun (x : α) ↦ x ∈ s) ⊤ top_mem, Subtype.mk (p := fun (x : α) ↦ x ∈ s) ⊥ bot_mem)}
      fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
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))
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 : α))
⊢ ∃ (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 : α))

Tactic:
refine t.induction ⟨{(⟨⊤, top_mem⟩, ⟨⊥, bot_mem⟩)}, by simp⟩ fun ⟨x, y⟩ t _ ⟨tc, eq⟩ ↦ ?_
-- Module: Mathlib.Order.BooleanSubalgebra
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 : α))
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 : α)
⊢ ∃ (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 : α))

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

Premises used: Finset.sup_insert, compl_sup
-- Module: Mathlib.Order.BooleanSubalgebra
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 : α))
⊢ (((↑x : α) \ (↑y : α))ᶜ ⊓ Finset.sup ∅ fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) =
    Finset.sup ∅ fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)

Tactic:
simp
-- Module: Mathlib.Order.BooleanSubalgebra
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 : α))
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 : α)
⊢ ∃ (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:
refine tc.induction ⟨∅, by simp⟩ fun ⟨z, w⟩ tc _ ⟨t, eq⟩ ↦ ?_
-- Module: Mathlib.Order.BooleanSubalgebra
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 : α)
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 : α)
⊢ ∃ (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:
simp_rw [Finset.sup_insert, inf_sup_left, eq]

Premises used: Finset.sup_insert, inf_sup_left
-- Module: Mathlib.Order.BooleanSubalgebra
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 : α)) =
    ({(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 : α)
⊢ ∃ (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:
use {(z, ⟨_, isSublattice.supClosed x.2 w.2⟩), (⟨_, isSublattice.infClosed y.2 z.2⟩, w)} ∪ t

Premises used: Prod.mk
-- Module: Mathlib.Order.BooleanSubalgebra
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
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
⊢ p x hx

Tactic:
obtain ⟨t, rfl⟩ := (mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mp hx

Premises used: BooleanSubalgebra.mem_closure_iff_sup_sdiff, Iff.mp, rfl
-- Module: Mathlib.Order.BooleanSubalgebra
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 : α))
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
⊢ p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx

Tactic:
revert hx
-- Module: Mathlib.Order.BooleanSubalgebra
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)
        (Finset.sup ∅ fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (Finset.sup ∅ fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx

Tactic:
simpa using sdiff _ bot_mem _ bot_mem