-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
/-- Non-unital star algebra homomorphisms commute with the non-unital continuous functional
calculus. -/
lemma NonUnitalStarAlgHomClass.map_cfcₙ (φ : F) (f : R → R) (a : A)
    (hf : ContinuousOn f (quasispectrum 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✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this✝ : Continuous ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
this : ψ.comp (cfcₙHom ha) = (cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι)
hf' : ContinuousOn f (quasispectrum R (ψ a))
⊢ φ ((cfcₙHom ha) { toFun := (quasispectrum R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ }) =
    (cfcₙHom hψa) { toFun := (quasispectrum R (φ a)).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
exact DFunLike.congr_fun this _

Result:
no goals

Proof state:
case refine_2
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✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this : Continuous ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Continuous (⇑(cfcₙHom hψa) ∘ fun g => g.comp ι)

Tactic:
fun_prop

Result:
no goals

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✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this : Continuous ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ φ (cfcₙ f a) = cfcₙ f (φ a)

Tactic:
suffices ψ.comp (cfcₙHom ha) =
    (cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι) by
  have hf' : ContinuousOn f (quasispectrum R (ψ a)) := hf.mono h_spec
  rw [cfcₙ_apply .., cfcₙ_apply ..]
  exact DFunLike.congr_fun this _

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✝²⁸ : Nontrivial R
inst✝²⁷ : StarRing R
inst✝²⁶ : MetricSpace R
inst✝²⁵ : IsTopologicalSemiring R
inst✝²⁴ : ContinuousStar R
inst✝²³ : CommRing S
inst✝²² : Algebra R S
inst✝²¹ : NonUnitalRing A
inst✝²⁰ : StarRing A
inst✝¹⁹ : TopologicalSpace A
inst✝¹⁸ : Module R A
inst✝¹⁷ : IsScalarTower R A A
inst✝¹⁶ : SMulCommClass R A A
inst✝¹⁵ : NonUnitalRing B
inst✝¹⁴ : StarRing B
inst✝¹³ : TopologicalSpace B
inst✝¹² : Module R B
inst✝¹¹ : IsScalarTower R B B
inst✝¹⁰ : SMulCommClass R B B
inst✝⁹ : Module S A
inst✝⁸ : Module S B
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : IsScalarTower R S B
inst✝⁵ : NonUnitalContinuousFunctionalCalculus R p
inst✝⁴ : NonUnitalContinuousFunctionalCalculus R q
inst✝³ : ContinuousMapZero.UniqueHom R B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F S A B
inst✝ : StarHomClass F A B
φ : F
f : R → R
a : A
hf : autoParam (ContinuousOn f (quasispectrum R a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
hφ : autoParam (Continuous ⇑φ) _auto✝
ha : autoParam (p a) _auto✝
hφa : autoParam (q (φ a)) _auto✝
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R ↑φ
this : Continuous ⇑ψ
h_spec : quasispectrum R (φ a) ⊆ quasispectrum R a
hψa : q (ψ a)
ι : C(↑(quasispectrum R (ψ a)), ↑(quasispectrum R a))₀ :=
  { toFun := Set.inclusion h_spec, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ ψ.comp (cfcₙHom ha) = (cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι)