-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_comp (g f : R → R) (a : A)
    (hg : ContinuousOn g (f '' σₙ R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
⊢ cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)

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 _ _]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
⊢ (cfcₙHom ha) { toFun := (σₙ R a).restrict (g ∘ f), continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ⋯)
      ({
            toFun :=
              (σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ })).restrict g,
            continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        ?f')

case f'
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
⊢ C(↑(σₙ R a), ↑(σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ })))₀

case hff'
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
⊢ ∀ (x : ↑(σₙ R a)), { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x = ↑(?f' x)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
this : ContinuousOn (g ∘ f) (σₙ R a)
⊢ cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)

Tactic:
have sp_eq :
    σₙ R (cfcₙHom (show p a from ha) ⟨ContinuousMap.mk _ hf.restrict, hf0⟩) = f '' (σₙ R a) := by
  rw [cfcₙHom_map_quasispectrum (by exact ha) _]
  ext
  simp

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
⊢ cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
g f : R → R
a : A
hg : autoParam (ContinuousOn g (f '' σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
this : ContinuousOn (g ∘ f) (σₙ R a)
sp_eq : σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a
⊢ (cfcₙHom ha) { toFun := (σₙ R a).restrict (g ∘ f), continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ⋯)
      ({
            toFun :=
              (σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ })).restrict g,
            continuous_toFun := ⋯, map_zero' := ⋯ }.comp
        {
          toFun :=
            Set.codRestrict ((σₙ R a).restrict f)
              (σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ })) ⋯,
          continuous_toFun := ⋯, map_zero' := ⋯ })

Tactic:
congr

Result:
no goals