-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
theorem cfcHom_comp [UniqueHom R A] (f : C(spectrum R a, R))
    (f' : C(spectrum R a, spectrum R (cfcHom ha f)))
    (hff' : ∀ x, f x = f' x) (g : C(spectrum R (cfcHom ha f), R)) :
    cfcHom ha (g.comp f') = cfcHom (cfcHom_predicate ha f) g

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
⊢ (cfcHom ha) (g.comp f') = (cfcHom ⋯) g

Tactic:
let φ : C(spectrum R (cfcHom ha f), R) →⋆ₐ[R] A :=
  (cfcHom ha).comp <| ContinuousMap.compStarAlgHom' R R f'

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ (cfcHom ha) (g.comp f') = (cfcHom ⋯) g

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ cfcHom ⋯ = φ

Tactic:
refine cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha f) φ ?_ ?_

Result:
case refine_1
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ Continuous ⇑φ

case refine_2
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
ha : p a
inst✝ : UniqueHom R A
f : C(↑(spectrum R a), R)
f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))
hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)
g : C(↑(spectrum R ((cfcHom ha) f)), R)
φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (compStarAlgHom' R R f')
⊢ φ (restrict (spectrum R ((cfcHom ha) f)) (ContinuousMap.id R)) = (cfcHom ha) f