-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
Goal:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : ContinuousStar A
inst_7 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst_8 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
hs0 : Fact (0 ∈ s)
f : C((↑s : Type u_2), 𝕜)₀
a : X → A
ha_cont : Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
zero :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) 0
id :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
      (ContinuousMapZero.id s)
star_id :
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
      (star (ContinuousMapZero.id s))
⊢ Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) ⋯ (s := s) ⋯ : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) f
have add : ∀ (f g : C((↑s : Type u_2), 𝕜)₀)
  (hf :
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A) f)
  (hg :
    Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      ((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
        g),
  Continuous[inst_8, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    ((cfcₙHomSuperset (p := p) sorry (s := s) sorry : C((↑s : Type u_2), 𝕜)₀ →⋆ₙₐ[𝕜] A) : (a : C((↑s : Type u_2), 𝕜)₀) → A)
      (f + g)
Tactic: induction f using ContinuousMapZero.induction_on_of_compact with
  | zero => simpa [map_zero] using continuous_const
  | id => simpa only [cfcₙHomSuperset_id]
  | star_id => simp only [map_star, cfcₙHomSuperset_id]; fun_prop
  | add f g hf hg => simpa only [map_add] using hf.add hg
  | mul f g hf hg => simpa only [map_mul] using hf.mul hg
  | smul r f hf => simpa only [map_smul] using hf.const_smul r
  | frequently f hf =>
    apply continuous_of_uniform_approx_of_continuous
    rw [Metric.uniformity_basis_dist_le.forall_iff (by aesop)]
    intro ε hε
    simp only [Set.mem_setOf_eq, dist_eq_norm]
    obtain ⟨g, hg, g_cont⟩ := frequently_iff.mp hf (Metric.closedBall_mem_nhds f hε)
    simp only [Metric.mem_closedBall, dist_comm g, dist_eq_norm] at hg
    refine ⟨_, g_cont, fun x ↦ ?_⟩
    rw [← map_sub, cfcₙHomSuperset_apply]
    rw [isometry_cfcₙHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcₙHom (ha' x)))]
    rw [ContinuousMapZero.norm_def, ContinuousMap.norm_le _ hε.le] at hg ⊢
    aesop
Cleared hypotheses: f