-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
lemma cfcHom_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S))
    {a : A} (hpa : p a) (hqa : q a) (h : SpectrumRestricts a f) :
    cfcHom hpa = h.starAlgHom (cfcHom hqa)

Proof state:
case hφ₁
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
⊢ Continuous ⇑(starAlgHom (cfcHom hqa) h)

Tactic:
exact h.isClosedEmbedding_starAlgHom (cfcHom_isClosedEmbedding hqa) halg |>.continuous

Result:
no goals

Proof state:
case hφ₂
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
⊢ (starAlgHom (cfcHom hqa) h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a

Tactic:
exact h.starAlgHom_id (cfcHom_id hqa)

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✝¹⁷ : 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
⊢ cfcHom hpa = starAlgHom (cfcHom hqa) h

Tactic:
apply cfcHom_eq_of_continuous_of_map_id

Result:
case hφ₁
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
⊢ Continuous ⇑(starAlgHom (cfcHom hqa) h)

case hφ₂
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
⊢ (starAlgHom (cfcHom hqa) h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a