-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
inst_12 : UniqueHom R A
g f : R → R
a : A
hg : ContinuousOn g (f '' σₙ R a)
hg0 : g 0 = 0
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
ha : p a
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq :
  quasispectrum.{u_1, u_2} R (A := A)
      ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := hf0 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A) =
    f '' σₙ R a
rw :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) (g ∘ f), continuous_toFun := ⋯, map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (comp
          {
            toFun :=
              (quasispectrum.{u_1, u_2} R (A := A)
                    ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
                        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
                          C((↑(σₙ R a) : Type u_1), R)₀ } :
                      A)).restrict
                (π := fun (a : R) ↦ R) g,
            continuous_toFun := ⋯, map_zero' := ⋯ }
          {
            toFun :=
              Set.codRestrict ((σₙ R a).restrict (π := fun (a : R) ↦ R) f)
                (quasispectrum.{u_1, u_2} R (A := A)
                  ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
                      { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
                    A))
                ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ }) :
      A)
f' :
  C((↑(σₙ R a) : Type u_1),
    (↑(quasispectrum.{u_1, u_2} R (A := A)
          ((cfcₙHom (p := p) ⋯ : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
              { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
                C((↑(σₙ 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 : (↑(σₙ R a) : Type u_1)),
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        x :
      R)
    ((↑(({
                toFun :=
                  Set.codRestrict ((σₙ R a).restrict (π := fun (a : R) ↦ R) f)
                    (quasispectrum.{u_1, u_2} R (A := A)
                      ((cfcₙHom (p := p) sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
                          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry,
                            map_zero' := sorry } :
                        A))
                    sorry,
                continuous_toFun := sorry, map_zero' := sorry } :
              (a_1 : (↑(σₙ R a) : Type u_1)) →
                (↑(σₙ R
                      ((cfcₙHom sorry : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
                        { toFun := (σₙ R a).restrict f, continuous_toFun := sorry, map_zero' := sorry })) :
                  Type u_1))
            x) :
        R) :
      R)
Tactic: rw [cfcₙ_apply .., cfcₙ_apply f a,
    cfcₙ_apply _ _ (by convert! hg) (ha := cfcₙHom_predicate (show p a from ha) _),
    ← cfcₙHom_comp _ _]