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

Proof state:
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 =
      ↑({
            toFun :=
              Set.codRestrict ((σₙ R a).restrict f)
                (σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ })) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ }
          x)

Tactic:
exact fun _ ↦ rfl

Result:
no goals

Proof state:
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' := ⋯ })))₀

Tactic:
exact ⟨.mk _ <| hf.restrict.codRestrict fun x ↦ by rw [sp_eq]; use x.1; simp, Subtype.ext hf0⟩

Result:
no goals

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)
⊢ Set.range ⇑{ toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 } = f '' σₙ R a

Tactic:
ext

Result:
case h
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)
x✝ : R
⊢ x✝ ∈ Set.range ⇑{ toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 } ↔ x✝ ∈ 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✝
⊢ cfcₙ (g ∘ f) a = cfcₙ g (cfcₙ f a)

Tactic:
have := hg.comp hf <| (σₙ R a).mapsTo_image f

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)
⊢ 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)
⊢ σₙ R ((cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 }) = f '' σₙ R a

Tactic:
rw [cfcₙHom_map_quasispectrum (by exact ha) _]

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)
⊢ Set.range ⇑{ toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := hf0 } = f '' σₙ R a