-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem ContinuousMap.induction_on_of_compact {𝕜 : Type*} [RCLike 𝕜] {s : Set 𝕜} [CompactSpace s]
    {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))
    (frequently : ∀ f, (∃ᶠ g in 𝓝 f, p g) → p f) (f : C(s, 𝕜)) :
    p f

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
this : f ∈ (polynomialFunctions s).starClosure.topologicalClosure
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g

Tactic:
rw [← SetLike.mem_coe, topologicalClosure_coe, mem_closure_iff_frequently] at this

Result:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
this : ∃ᶠ (x : C(↑s, 𝕜)) in 𝓝 f, x ∈ ↑(polynomialFunctions s).starClosure
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
this : ∃ᶠ (x : C(↑s, 𝕜)) in 𝓝 f, x ∈ ↑(polynomialFunctions s).starClosure
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g

Tactic:
exact this.mp <| .of_forall h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f : C(↑s, 𝕜)
⊢ p f

Tactic:
refine f.induction_on const id star_id add mul fun h f ↦ frequently f ?_

Result:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g

Proof state:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g

Tactic:
have := polynomialFunctions.starClosure_topologicalClosure s ▸ mem_top (x := f)

Result:
𝕜 : Type u_1
inst✝¹ : RCLike 𝕜
s : Set 𝕜
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)
h : ∀ f ∈ (polynomialFunctions s).starClosure, p f
f : C(↑s, 𝕜)
this : f ∈ (polynomialFunctions s).starClosure.topologicalClosure
⊢ ∃ᶠ (g : C(↑s, 𝕜)) in 𝓝 f, p g