-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
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))
hff' :
  ∀ (x : (↑(spectrum R a) : Type u_1)),
    Eq (α := R)
      (({ toFun := (spectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
              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) ⋯ : (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 := ⋯ } :
                (a_1 : (↑(spectrum R a) : Type u_1)) →
                  (↑(spectrum R
                        ((cfcHom ⋯ : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
                          { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })) :
                    Type u_1))
              x) :
          R) :
        R)
⊢ cfc (p := p) (g ∘ f) a = cfc (p := p) g (cfc (p := p) f a)

Tactic:
rw [cfc_apply .., cfc_apply f a,
    cfc_apply _ _ (cfcHom_predicate (show p a from ha) _) (by convert! hg), ← cfcHom_comp _ _]

Premises used: cfcHom_comp, cfc_apply, cfcHom_predicate