-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean
theorem cfc (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) (h0 : p 0)
    (h : ∀ a, p a ↔ q a ∧ QuasispectrumRestricts a f) :
    NonUnitalContinuousFunctionalCalculus R p where
  predicate_zero := h0
  compactSpace_quasispectrum 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✝¹⁹ : 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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
s : S
hs : s ∈ σₙ S ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) g)
⊢ (algebraMap R S) (f s) = s

Tactic:
rw [nonUnitalStarAlgHom_apply,
  cfcₙHom_map_quasispectrum] at hs

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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
s : S
hs :
  s ∈
    range
      ⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp
          (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
⊢ (algebraMap R S) (f s) = s

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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
⊢ q ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) g) ∧ QuasispectrumRestricts ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) g) ⇑f

Tactic:
refine ⟨cfcₙHom_predicate _ _, ?_⟩

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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(σₙ R a), R)₀
⊢ QuasispectrumRestricts ((nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯) g) ⇑f

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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
ha : p a
⊢ (nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯)
      { toContinuousMap := ContinuousMap.restrict (σₙ R a) (ContinuousMap.id R), map_zero' := ⋯ } =
    a

Tactic:
exact ((h a).mp ha).2.nonUnitalStarAlgHom_id <| cfcₙHom_id ((h a).mp ha).1

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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
⊢ CompactSpace ↑(σₙ R a)

Tactic:
have := NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum (R := S) a

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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f
a : A
this : CompactSpace ↑(σₙ S a)
⊢ CompactSpace ↑(σₙ R a)