-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
/-- An induction principle for `C(s, 𝕜)₀`. -/
@[elab_as_elim]
lemma ContinuousMapZero.induction_on {s : Set 𝕜} [Zero s] (h0 : ((0 : s) : 𝕜) = 0)
    {p : C(s, 𝕜)₀ → Prop} (zero : p 0) (id : p (.id h0)) (star_id : p (star (.id h0)))
    (add : ∀ f g, p f → p g → p (f + g)) (mul : ∀ f g, p f → p g → p (f * g))
    (smul : ∀ (r : 𝕜) f, p f → p (r • f))
    (closure : (∀ f ∈ adjoin 𝕜 {(.id h0 : C(s, 𝕜)₀)}, p f) → ∀ f, p f) (f : C(s, 𝕜)₀) :
    p f

Proof state:
case mem
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝¹ f✝ f : C(↑s, 𝕜)₀
hf : f ∈ {ContinuousMapZero.id h0} ∪ star {ContinuousMapZero.id h0}
⊢ p f

Tactic:
simp only [Set.mem_union, Set.mem_singleton_iff, Set.mem_star] at hf

Result:
case mem
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝¹ f✝ f : C(↑s, 𝕜)₀
hf : f = ContinuousMapZero.id h0 ∨ star f = ContinuousMapZero.id h0
⊢ p f

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f : C(↑s, 𝕜)₀
⊢ p f

Tactic:
refine closure (fun f hf => ?_) f

Result:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f : C(↑s, 𝕜)₀
hf : f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}
⊢ p f

Proof state:
case mul
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : Zero ↑s
h0 : ↑0 = 0
p : C(↑s, 𝕜)₀ → Prop
zero : p 0
id : p (ContinuousMapZero.id h0)
star_id : p (star (ContinuousMapZero.id h0))
add : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)₀), p f → p g → p (f * g)
smul : ∀ (r : 𝕜) (f : C(↑s, 𝕜)₀), p f → p (r • f)
closure : (∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f) → ∀ (f : C(↑s, 𝕜)₀), p f
f✝ f x✝ y✝ : C(↑s, 𝕜)₀
hx✝ : x✝ ∈ NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id h0} ∪ star {ContinuousMapZero.id h0})
hy✝ : y✝ ∈ NonUnitalAlgebra.adjoin 𝕜 ({ContinuousMapZero.id h0} ∪ star {ContinuousMapZero.id h0})
hf : p x✝
hg : p y✝
⊢ p (x✝ * y✝)

Tactic:
exact mul _ _ hf hg

Result:
no goals