-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem ContinuousMap.induction_on {𝕜 : Type*} [RCLike 𝕜] {s : Set 𝕜}
    {p : C(s, 𝕜) → Prop} (const : ∀ r, p (.const s r)) (id : p (.restrict s <| .id 𝕜))
    (star_id : p (star (.restrict s <| .id 𝕜)))
    (add : ∀ f g, p f → p g → p (f + g)) (mul : ∀ f g, p f → p g → p (f * g))
    (closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ f, p f) (f : C(s, 𝕜)) :
    p f

Proof state:
case add
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f x✝ y✝ : C(↑s, 𝕜)
hx✝ : x✝ ∈ Algebra.adjoin 𝕜 ({(toContinuousMapOnAlgHom s) X} ∪ star {(toContinuousMapOnAlgHom s) X})
hy✝ : y✝ ∈ Algebra.adjoin 𝕜 ({(toContinuousMapOnAlgHom s) X} ∪ star {(toContinuousMapOnAlgHom s) X})
hf : p x✝
hg : p y✝
⊢ p (x✝ + y✝)

Tactic:
exact add _ _ hf hg

Result:
no goals

Proof state:
case algebraMap
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f : C(↑s, 𝕜)
r : 𝕜
⊢ p ((algebraMap 𝕜 C(↑s, 𝕜)) r)

Tactic:
exact const r

Result:
no goals

Proof state:
case mem
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝¹ f✝ f : C(↑s, 𝕜)
hf : f ∈ {(toContinuousMapOnAlgHom s) X} ∪ star {(toContinuousMapOnAlgHom s) X}
⊢ 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 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝¹ f✝ f : C(↑s, 𝕜)
hf : f = (toContinuousMapOnAlgHom s) X ∨ star f = (toContinuousMapOnAlgHom s) X
⊢ p f

Proof state:
case mem.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
s : Set 𝕜
p : C(↑s, 𝕜) → Prop
const : ∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)
id : p (restrict s (ContinuousMap.id 𝕜))
star_id : p (star (restrict s (ContinuousMap.id 𝕜)))
add : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)
mul : ∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)
closure : (∀ f ∈ (polynomialFunctions s).starClosure, p f) → ∀ (f : C(↑s, 𝕜)), p f
f✝ f : C(↑s, 𝕜)
⊢ p (star ((toContinuousMapOnAlgHom s) X))

Tactic:
simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]

Result:
no goals