-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
lemma cfcₙ_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A}
    (hpa : p a) (hqa : q a) (h : QuasispectrumRestricts a f) (g : R → R) :
    cfcₙ g a = cfcₙ (fun x ↦ algebraMap R S (g (f x))) a

Proof state:
case pos.intro
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁶ : Semifield R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Field S
inst✝²⁰ : StarRing S
inst✝¹⁹ : MetricSpace S
inst✝¹⁸ : IsTopologicalRing S
inst✝¹⁷ : ContinuousStar S
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module S A
inst✝¹³ : IsScalarTower S A A
inst✝¹² : SMulCommClass S A A
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module R A
inst✝⁹ : IsScalarTower R S A
inst✝⁸ : StarModule R S
inst✝⁷ : ContinuousSMul R S
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus S q
inst✝⁴ : CompleteSpace R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
⊢ cfcₙ
      (Function.extend Subtype.val
        (⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
            ({ toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }.comp
              { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })))
        0)
      a =
    cfcₙ (fun x => (algebraMap R S) (g (f x))) a

Tactic:
apply cfcₙ_congr fun x hx ↦ ?_

Result:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁶ : Semifield R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Field S
inst✝²⁰ : StarRing S
inst✝¹⁹ : MetricSpace S
inst✝¹⁸ : IsTopologicalRing S
inst✝¹⁷ : ContinuousStar S
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module S A
inst✝¹³ : IsScalarTower S A A
inst✝¹² : SMulCommClass S A A
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module R A
inst✝⁹ : IsScalarTower R S A
inst✝⁸ : StarModule R S
inst✝⁷ : ContinuousSMul R S
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus S q
inst✝⁴ : CompleteSpace R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
x : S
hx : x ∈ σₙ S a
⊢ Function.extend Subtype.val
      (⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
          ({ toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }.comp
            { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ })))
      0 x =
    (algebraMap R S) (g (f x))

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁶ : Semifield R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Field S
inst✝²⁰ : StarRing S
inst✝¹⁹ : MetricSpace S
inst✝¹⁸ : IsTopologicalRing S
inst✝¹⁷ : ContinuousStar S
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module S A
inst✝¹³ : IsScalarTower S A A
inst✝¹² : SMulCommClass S A A
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module R A
inst✝⁹ : IsScalarTower R S A
inst✝⁸ : StarModule R S
inst✝⁷ : ContinuousSMul R S
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus S q
inst✝⁴ : CompleteSpace R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ¬ContinuousOn g (σₙ R a)
⊢ ¬ContinuousOn (fun x => (algebraMap R S) (g (f x))) (σₙ S a)

Tactic:
refine fun hg' ↦ hg ?_

Result:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁶ : Semifield R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Field S
inst✝²⁰ : StarRing S
inst✝¹⁹ : MetricSpace S
inst✝¹⁸ : IsTopologicalRing S
inst✝¹⁷ : ContinuousStar S
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module S A
inst✝¹³ : IsScalarTower S A A
inst✝¹² : SMulCommClass S A A
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module R A
inst✝⁹ : IsScalarTower R S A
inst✝⁸ : StarModule R S
inst✝⁷ : ContinuousSMul R S
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus S q
inst✝⁴ : CompleteSpace R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ¬ContinuousOn g (σₙ R a)
hg' : ContinuousOn (fun x => (algebraMap R S) (g (f x))) (σₙ S a)
⊢ ContinuousOn g (σₙ R a)

Proof state:
case neg.inr
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁶ : Semifield R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Field S
inst✝²⁰ : StarRing S
inst✝¹⁹ : MetricSpace S
inst✝¹⁸ : IsTopologicalRing S
inst✝¹⁷ : ContinuousStar S
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module S A
inst✝¹³ : IsScalarTower S A A
inst✝¹² : SMulCommClass S A A
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module R A
inst✝⁹ : IsScalarTower R S A
inst✝⁸ : StarModule R S
inst✝⁷ : ContinuousSMul R S
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus S q
inst✝⁴ : CompleteSpace R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ¬g 0 = 0
⊢ cfcₙ g a = cfcₙ (fun x => (algebraMap R S) (g (f x))) a

Tactic:
rw [cfcₙ_apply_of_not_map_zero a hg, cfcₙ_apply_of_not_map_zero a (by simpa [h.map_zero])]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst✝²⁶ : Semifield R
inst✝²⁵ : StarRing R
inst✝²⁴ : MetricSpace R
inst✝²³ : IsTopologicalSemiring R
inst✝²² : ContinuousStar R
inst✝²¹ : Field S
inst✝²⁰ : StarRing S
inst✝¹⁹ : MetricSpace S
inst✝¹⁸ : IsTopologicalRing S
inst✝¹⁷ : ContinuousStar S
inst✝¹⁶ : NonUnitalRing A
inst✝¹⁵ : StarRing A
inst✝¹⁴ : Module S A
inst✝¹³ : IsScalarTower S A A
inst✝¹² : SMulCommClass S A A
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module R A
inst✝⁹ : IsScalarTower R S A
inst✝⁸ : StarModule R S
inst✝⁷ : ContinuousSMul R S
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus S q
inst✝⁴ : CompleteSpace R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : QuasispectrumRestricts a ⇑f
g : R → R
hg : ¬ContinuousOn g (σₙ R a)
hg' : ContinuousOn (fun x => (algebraMap R S) (g (f x))) (σₙ S a)
⊢ ContinuousOn (⇑(algebraMap R S) ∘ g) (σₙ R a)

Tactic:
simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
  hg'.comp halg.isEmbedding.continuous.continuousOn
  (fun _ : R ↦ quasispectrum.algebraMap_mem S)

Result:
no goals