-- 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:
𝕜 : 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, 𝕜)
hf : f ∈ StarAlgebra.adjoin 𝕜 {(toContinuousMapOnAlgHom s) X}
⊢ p f

Tactic:
induction hf using Algebra.adjoin_induction with
| mem f hf =>
  simp only [Set.mem_union, Set.mem_singleton_iff, Set.mem_star] at hf
  rw [star_eq_iff_star_eq, eq_comm (b := f)] at hf
  obtain (rfl | rfl) := hf
  all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]
| algebraMap r => exact const r
| add _ _ _ _ hf hg => exact add _ _ hf hg
| mul _ _ _ _ hf hg => exact mul _ _ hf hg

Result:
no goals

Proof state:
case mul
𝕜 : 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 mul _ _ hf hg

Result:
no goals

Proof state:
𝕜 : 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, 𝕜)
hf : f ∈ (polynomialFunctions s).starClosure
⊢ p f

Tactic:
rw [polynomialFunctions.starClosure_eq_adjoin_X] at hf

Result:
𝕜 : 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, 𝕜)
hf : f ∈ StarAlgebra.adjoin 𝕜 {(toContinuousMapOnAlgHom s) X}
⊢ p f

Proof state:
𝕜 : 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 : C(↑s, 𝕜)
⊢ p f

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

Result:
𝕜 : 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, 𝕜)
hf : f ∈ (polynomialFunctions s).starClosure
⊢ p f

Proof state:
case mem.inl
𝕜 : 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 ((toContinuousMapOnAlgHom s) X)

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:
all_goals simpa only [toContinuousMapOnAlgHom_apply, toContinuousMapOn_X_eq_restrict_id]

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 f = (toContinuousMapOnAlgHom s) X
⊢ p f

Tactic:
rw [star_eq_iff_star_eq, eq_comm (b := f)] 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 ∨ f = star ((toContinuousMapOnAlgHom s) X)
⊢ p f

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 ∨ f = star ((toContinuousMapOnAlgHom s) X)
⊢ p f

Tactic:
obtain (rfl | rfl) := hf

Result:
case mem.inl
𝕜 : 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 ((toContinuousMapOnAlgHom s) X)

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