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

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

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

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)₀), (∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)₀
h : ∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f
f : C(↑s, 𝕜)₀
⊢ ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)₀), (∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)₀
h : ∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f
f : C(↑s, 𝕜)₀
this : f ∈ closure ↑(adjoin 𝕜 {ContinuousMapZero.id h0})
⊢ ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g

Tactic:
exact mem_closure_iff_frequently.mp this |>.mp <| .of_forall h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)₀), (∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)₀
h : ∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f
f : C(↑s, 𝕜)₀
⊢ ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g

Tactic:
have := (ContinuousMapZero.adjoin_id_dense h0).closure_eq ▸ Set.mem_univ (x := f)

Result:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
s : Set 𝕜
inst✝¹ : Zero ↑s
h0 : ↑0 = 0
inst✝ : CompactSpace ↑s
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)
frequently : ∀ (f : C(↑s, 𝕜)₀), (∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g) → p f
f✝ : C(↑s, 𝕜)₀
h : ∀ f ∈ adjoin 𝕜 {ContinuousMapZero.id h0}, p f
f : C(↑s, 𝕜)₀
this : f ∈ closure ↑(adjoin 𝕜 {ContinuousMapZero.id h0})
⊢ ∃ᶠ (g : C(↑s, 𝕜)₀) in 𝓝 f, p g