-- 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 : SpectrumRestricts a f) (g : R → R) :
    cfc g a = cfc (fun x ↦ algebraMap R S (g (f x))) a

Proof state:
case pos
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✝¹⁷ : Semifield S
inst✝¹⁶ : StarRing S
inst✝¹⁵ : MetricSpace S
inst✝¹⁴ : IsTopologicalSemiring S
inst✝¹³ : ContinuousStar S
inst✝¹² : Ring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Algebra S A
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : ContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (spectrum R a)
⊢ cfc g a = cfc (fun x => (algebraMap R S) (g (f x))) a

Tactic:
rw [cfc_apply g a, cfcHom_eq_restrict f halg hpa hqa h, SpectrumRestricts.starAlgHom_apply,
  cfcHom_eq_cfc_extend 0]

Result:
case pos
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✝¹⁷ : Semifield S
inst✝¹⁶ : StarRing S
inst✝¹⁵ : MetricSpace S
inst✝¹⁴ : IsTopologicalSemiring S
inst✝¹³ : ContinuousStar S
inst✝¹² : Ring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Algebra S A
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : ContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (spectrum R a)
⊢ cfc
      (Function.extend Subtype.val
        (⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
            ({ toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }.comp
              { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ })))
        0)
      a =
    cfc (fun x => (algebraMap R S) (g (f x))) a

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✝¹⁷ : Semifield S
inst✝¹⁶ : StarRing S
inst✝¹⁵ : MetricSpace S
inst✝¹⁴ : IsTopologicalSemiring S
inst✝¹³ : ContinuousStar S
inst✝¹² : Ring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Algebra S A
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : ContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
⊢ cfc g a = cfc (fun x => (algebraMap R S) (g (f x))) a

Tactic:
by_cases hg : ContinuousOn g (spectrum R a)

Result:
case pos
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✝¹⁷ : Semifield S
inst✝¹⁶ : StarRing S
inst✝¹⁵ : MetricSpace S
inst✝¹⁴ : IsTopologicalSemiring S
inst✝¹³ : ContinuousStar S
inst✝¹² : Ring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Algebra S A
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : ContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ContinuousOn g (spectrum R a)
⊢ cfc g a = cfc (fun x => (algebraMap R S) (g (f x))) a

case neg
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✝¹⁷ : Semifield S
inst✝¹⁶ : StarRing S
inst✝¹⁵ : MetricSpace S
inst✝¹⁴ : IsTopologicalSemiring S
inst✝¹³ : ContinuousStar S
inst✝¹² : Ring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Algebra S A
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : ContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ¬ContinuousOn g (spectrum R a)
⊢ cfc g a = cfc (fun x => (algebraMap R S) (g (f x))) a

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✝¹⁷ : Semifield S
inst✝¹⁶ : StarRing S
inst✝¹⁵ : MetricSpace S
inst✝¹⁴ : IsTopologicalSemiring S
inst✝¹³ : ContinuousStar S
inst✝¹² : Ring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Algebra S A
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : ContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ¬ContinuousOn g (spectrum R a)
hg' : ContinuousOn (fun x => (algebraMap R S) (g (f x))) (spectrum S a)
⊢ ContinuousOn g (spectrum R a)

Tactic:
rw [halg.isEmbedding.continuousOn_iff]

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✝¹⁷ : Semifield S
inst✝¹⁶ : StarRing S
inst✝¹⁵ : MetricSpace S
inst✝¹⁴ : IsTopologicalSemiring S
inst✝¹³ : ContinuousStar S
inst✝¹² : Ring A
inst✝¹¹ : StarRing A
inst✝¹⁰ : Algebra S A
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : StarModule R S
inst✝⁵ : ContinuousSMul R S
inst✝⁴ : TopologicalSpace A
inst✝³ : ContinuousFunctionalCalculus S q
inst✝² : CompleteSpace R
inst✝¹ : ContinuousFunctionalCalculus R p
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
a : A
hpa : p a
hqa : q a
h : SpectrumRestricts a ⇑f
g : R → R
hg : ¬ContinuousOn g (spectrum R a)
hg' : ContinuousOn (fun x => (algebraMap R S) (g (f x))) (spectrum S a)
⊢ ContinuousOn (⇑(algebraMap R S) ∘ g) (spectrum R a)