-- 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 : NormedRing A
inst_2 : StarRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p
inst_5 : ContinuousStar A
inst_6 : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : C((↑s : Type u_2), 𝕜)
a : X → A
ha_cont : Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s
ha' : ∀ (x : X), p (a x)
this : CompactSpace.{u_2} (↑s : Type u_2)
const :
  ∀ (r : 𝕜),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) (ContinuousMap.const (↑s : Type u_2) r)
id :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A)
      (ContinuousMap.restrict s (ContinuousMap.id 𝕜))
star_id :
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A)
      (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜)))
add :
  ∀ (f g : C((↑s : Type u_2), 𝕜))
    (hf :
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
        (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f)
    (hg :
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
        (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) (f + g)
mul :
  ∀ (f g : C((↑s : Type u_2), 𝕜))
    (hf :
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
        (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f)
    (hg :
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
        (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) g),
    Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
      (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) (f * g)
⊢ Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) ⋯ (s := s) ⋯ : (a : C((↑s : Type u_2), 𝕜)) → A) f
have frequently : ∀ (f : C((↑s : Type u_2), 𝕜))
  (hf :
    ∃ᶠ (g : C((↑s : Type u_2), 𝕜)) in 𝓝 f,
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
        (cfcHomSuperset (p := p) sorry (s := s) sorry : (a : C((↑s : Type u_2), 𝕜)) → A) g),
  Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    (cfcHomSuperset (p := p) sorry (s := s) sorry : (a : C((↑s : Type u_2), 𝕜)) → A) f
Tactic: induction f using ContinuousMap.induction_on_of_compact with
  | const r =>
    have : ContinuousMap.const s r = algebraMap 𝕜 C(s, 𝕜) r := rfl
    simpa only [this, AlgHomClass.commutes] using continuous_const
  | id =>
    simp only [cfcHomSuperset_id]
    fun_prop
  | star_id =>
    simp only [map_star, cfcHomSuperset_id]
    fun_prop
  | add f g hf hg => simpa using hf.add hg
  | mul f g hf hg => simpa using hf.mul hg
  | 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, cfcHomSuperset_apply]
    rw [isometry_cfcHom (R := 𝕜) _ (ha' x) |>.norm_map_of_map_zero (map_zero (cfcHom (ha' x)))]
    rw [ContinuousMap.norm_le _ hε.le] at hg ⊢
    aesop
Cleared hypotheses: f