-- Mathlib/Order/BooleanSubalgebra.lean
theorem closure_sdiff_sup_induction {p : ∀ g ∈ closure s, Prop}
    (sdiff : ∀ x hx y hy, p (x \ y) (sdiff_mem (subset_closure hx) (subset_closure hy)))
    (sup : ∀ x hx y hy, p x hx → p y hy → p (x ⊔ y) (sup_mem hx hy))
    (x) (hx : x ∈ closure s) : p x hx

Proof state:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s
⊢ p (t.sup fun x => ↑x.1 \ ↑x.2) hx

Tactic:
revert hx

Result:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x => ↑x.1 \ ↑x.2) hx

Proof state:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x => ↑x.1 \ ↑x.2) hx

Tactic:
refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_

Result:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t✝ : Finset (↑s × ↑s)
x : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝ : x ∉ t
ih : ∀ (hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x => ↑x.1 \ ↑x.2) hx
hxt : ((insert x t).sup fun x => ↑x.1 \ ↑x.2) ∈ closure s
⊢ p ((insert x t).sup fun x => ↑x.1 \ ↑x.2) hxt

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (∅.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s), p (∅.sup fun x => ↑x.1 \ ↑x.2) hx

Tactic:
simpa using sdiff _ bot_mem _ bot_mem

Result:
no goals

Proof state:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
⊢ ∀ (hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x => ↑x.1 \ ↑x.2) hx

Tactic:
classical
refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
simp only [Finset.sup_insert] at hxt ⊢
exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
  (sdiff _ x.1.2 _ x.2.2) (ih _)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
x : α
hx : x ∈ closure s
⊢ p x hx

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

Result:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset (↑s × ↑s)
hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s
⊢ p (t.sup fun x => ↑x.1 \ ↑x.2) hx

Proof state:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t✝ : Finset (↑s × ↑s)
x : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝ : x ∉ t
ih : ∀ (hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x => ↑x.1 \ ↑x.2) hx
hxt : ((insert x t).sup fun x => ↑x.1 \ ↑x.2) ∈ closure s
⊢ p ((insert x t).sup fun x => ↑x.1 \ ↑x.2) hxt

Tactic:
simp only [Finset.sup_insert] at hxt ⊢

Result:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t✝ : Finset (↑s × ↑s)
x : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝ : x ∉ t
ih : ∀ (hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x => ↑x.1 \ ↑x.2) hx
hxt✝ : ((insert x t).sup fun x => ↑x.1 \ ↑x.2) ∈ closure s
hxt : (↑x.1 \ ↑x.2 ⊔ t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s
⊢ p (↑x.1 \ ↑x.2 ⊔ t.sup fun x => ↑x.1 \ ↑x.2) ⋯

Proof state:
case intro
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → g ∈ closure s → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup : ∀ (x : α) (hx : x ∈ closure s) (y : α) (hy : y ∈ closure s), p x hx → p y hy → p (x ⊔ y) ⋯
t✝ : Finset (↑s × ↑s)
x : ↑s × ↑s
t : Finset (↑s × ↑s)
x✝ : x ∉ t
ih : ∀ (hx : (t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s), p (t.sup fun x => ↑x.1 \ ↑x.2) hx
hxt✝ : ((insert x t).sup fun x => ↑x.1 \ ↑x.2) ∈ closure s
hxt : (↑x.1 \ ↑x.2 ⊔ t.sup fun x => ↑x.1 \ ↑x.2) ∈ closure s
⊢ p (↑x.1 \ ↑x.2 ⊔ t.sup fun x => ↑x.1 \ ↑x.2) ⋯

Tactic:
exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
  (sdiff _ x.1.2 _ x.2.2) (ih _)

Result:
no goals