-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
/-- Star algebra homomorphisms commute with the continuous functional calculus. -/
lemma StarAlgHomClass.map_cfc (φ : F) (f : R → R) (a : A)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Ring A
inst✝¹⁸ : StarRing A
inst✝¹⁷ : TopologicalSpace A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R p
inst✝⁴ : ContinuousFunctionalCalculus R q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
⊢ φ (cfc f a) = cfc f (φ a)

Tactic:
have : Continuous ψ := hφ

Result:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Ring A
inst✝¹⁸ : StarRing A
inst✝¹⁷ : TopologicalSpace A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R p
inst✝⁴ : ContinuousFunctionalCalculus R q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this : Continuous ⇑ψ
⊢ φ (cfc f a) = cfc f (φ a)

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Ring A
inst✝¹⁸ : StarRing A
inst✝¹⁷ : TopologicalSpace A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R p
inst✝⁴ : ContinuousFunctionalCalculus R q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this : Continuous ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
⊢ φ (cfc f a) = cfc f (φ a)

Tactic:
suffices ψ.comp (cfcHom ha) = (cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι) by
  have hf' : ContinuousOn f (spectrum R (ψ a)) := hf.mono h_spec
  rw [cfc_apply .., cfc_apply ..]
  congrm($(this) ⟨_, hf.restrict⟩)

Result:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Ring A
inst✝¹⁸ : StarRing A
inst✝¹⁷ : TopologicalSpace A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R p
inst✝⁴ : ContinuousFunctionalCalculus R q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this : Continuous ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
⊢ ψ.comp (cfcHom ha) = (cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι)

Proof state:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst✝²⁴ : CommSemiring R
inst✝²³ : StarRing R
inst✝²² : MetricSpace R
inst✝²¹ : IsTopologicalSemiring R
inst✝²⁰ : ContinuousStar R
inst✝¹⁹ : Ring A
inst✝¹⁸ : StarRing A
inst✝¹⁷ : TopologicalSpace A
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Ring B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Algebra R B
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Algebra S A
inst✝⁸ : Algebra S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : ContinuousFunctionalCalculus R p
inst✝⁴ : ContinuousFunctionalCalculus R q
inst✝³ : ContinuousMap.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₐ[R] B := StarAlgHom.restrictScalars R ↑φ
this✝ : Continuous ⇑ψ
h_spec : spectrum R (ψ a) ⊆ spectrum R a
hψa : q (ψ a)
ι : C(↑(spectrum R (ψ a)), ↑(spectrum R a)) := { toFun := Set.inclusion h_spec, continuous_toFun := ⋯ }
this : ψ.comp (cfcHom ha) = (cfcHom hψa).comp (ContinuousMap.compStarAlgHom' R R ι)
hf' : ContinuousOn f (spectrum R (ψ a))
⊢ φ ((cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) =
    (cfcHom hψa) { toFun := (spectrum R (φ a)).restrict f, continuous_toFun := ⋯ }

Tactic:
congrm($(this) ⟨_, hf.restrict⟩)

Result:
no goals