-- 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 ∧ SpectrumRestricts a f) :
    ContinuousFunctionalCalculus R p where
  predicate_zero := h0
  spectrum_nonempty a ha := ((h a).mp ha).2.image ▸
    (ContinuousFunctionalCalculus.spectrum_nonempty a ((h a).mp ha).1 |>.image f)
  compactSpace_spectrum a

Proof state:
case h.mp.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✝¹⁵ : 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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
x : R
y : ↑(spectrum S a)
hy :
  ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      y =
    (algebraMap R S) x
⊢ x ∈ range ⇑g

Tactic:
have := congr_arg f hy

Result:
case h.mp.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✝¹⁵ : 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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
x : R
y : ↑(spectrum S a)
hy :
  ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      y =
    (algebraMap R S) x
this :
  f
      (({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
          (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
        y) =
    f ((algebraMap R S) x)
⊢ x ∈ range ⇑g

Proof state:
case h.mpr
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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
x : R
⊢ x ∈ range ⇑g →
    x ∈
      ⇑(algebraMap R S) ⁻¹'
        range
          ⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
              (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.mpr.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✝¹⁵ : 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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
y : ↑(spectrum R a)
⊢ g y ∈
    ⇑(algebraMap R S) ⁻¹'
      range
        ⇑({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
            (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))

Proof state:
case predicate_hom
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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
⊢ ∀ (f_1 : C(↑(spectrum R a), R)), p ((starAlgHom (cfcHom ⋯) ⋯) f_1)

Tactic:
case predicate_hom =>
  intro g
  rw [h]
  refine ⟨cfcHom_predicate _ _, ?_⟩
  refine .of_rightInvOn (((h a).mp ha).2.left_inv) fun s hs ↦ ?_
  rw [SpectrumRestricts.starAlgHom_apply, cfcHom_map_spectrum] at hs
  obtain ⟨r, rfl⟩ := hs
  simp [((h a).mp ha).2.left_inv _]

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

Tactic:
obtain ⟨r, rfl⟩ := hs

Result:
case 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✝¹⁵ : 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
f : C(S, R)
halg : IsUniformEmbedding ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
g : C(↑(spectrum R a), R)
r : ↑(spectrum S a)
⊢ (algebraMap R S)
      (f
        (({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
            (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
          r)) =
    ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      r