-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : TopologicalSpace A
inst_6 : Ring A
inst_7 : StarRing A
inst_8 : Algebra R A
instCFC : ContinuousFunctionalCalculus R A p
inst_9 : UniqueHom R A
g f : R → R
a : A
ha : p a
hg : ContinuousOn g (f '' spectrum R a)
hf : ContinuousOn f (spectrum R a)
this : ContinuousOn (g ∘ f) (spectrum R a)
sp_eq :
  spectrum.{u_1, u_2} R (A := A)
      ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1), R) } :
        A) =
    f '' spectrum R a
rw :
  Eq.{u_2 + 1} (α := A)
    ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) (g ∘ f), continuous_toFun := ⋯ :
          C((↑(spectrum R a) : Type u_1), R) } :
      A)
    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
        (comp
          {
            toFun :=
              (spectrum.{u_1, u_2} R (A := A)
                    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                          C((↑(spectrum R a) : Type u_1), R) } :
                      A)).restrict
                (π := fun (a : R) ↦ R) g,
            continuous_toFun := ⋯ }
          {
            toFun :=
              Set.codRestrict ((spectrum R a).restrict (π := fun (a : R) ↦ R) f)
                (spectrum.{u_1, u_2} R (A := A)
                  ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                      { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                        C((↑(spectrum R a) : Type u_1), R) } :
                    A))
                ⋯,
            continuous_toFun := ⋯ :
            C((↑(spectrum R a) : Type u_1),
              (↑(spectrum.{u_1, u_2} R (A := A)
                    ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                        { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                          C((↑(spectrum R a) : Type u_1), R) } :
                      A)) :
                Type u_1)) }) :
      A)
f' :
  C((↑(spectrum R a) : Type u_1),
    (↑(spectrum.{u_1, u_2} R (A := A)
          ((cfcHom (p := p) ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
              { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(spectrum R a) : Type u_1), R) } :
            A)) :
      Type u_1))
⊢ cfc (p := p) (g ∘ f) a = cfc (p := p) g (cfc (p := p) f a)
have hff' : ∀ (x : (↑(spectrum R a) : Type u_1)),
  Eq (α := R)
    (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
            C((↑(spectrum R a) : Type u_1), R) } :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        x :
      R)
    ((↑(({
                toFun :=
                  Set.codRestrict ((spectrum R a).restrict (π := fun (a : R) ↦ R) f)
                    (spectrum.{u_1, u_2} R (A := A)
                      ((cfcHom (p := p) sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                          { toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
                            C((↑(spectrum R a) : Type u_1), R) } :
                        A))
                    sorry,
                continuous_toFun := sorry } :
              (a_1 : (↑(spectrum R a) : Type u_1)) →
                (↑(spectrum R
                      ((cfcHom sorry : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                        { toFun := (spectrum R a).restrict f, continuous_toFun := sorry })) :
                  Type u_1))
            x) :
        R) :
      R)
Tactic: rw [cfc_apply .., cfc_apply f a,
    cfc_apply _ _ (cfcHom_predicate (show p a from ha) _) (by convert! hg), ← cfcHom_comp _ _]