-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
theorem isometric_cfc (f : C(S, R)) (halg : Isometry (algebraMap R S)) (h0 : p 0)
    (h : ∀ a, p a ↔ q a ∧ SpectrumRestricts a f) :
    IsometricContinuousFunctionalCalculus R A p where
  toContinuousFunctionalCalculus := SpectrumRestricts.cfc f halg.isUniformEmbedding h0 h
  isometric a ha

Proof state:
case intro.refine_2
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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
_inst : ∀ (a : A), CompactSpace ↑(σ R a)
this : ContinuousFunctionalCalculus R p
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ R a)
x' : ↑(σ S a) := Subtype.map ⇑(algebraMap R S) ⋯ x
⊢ dist (g₁ x) (g₂ x) ≤
    dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))

Tactic:
apply le_of_eq_of_le ?_ <| ContinuousMap.dist_apply_le_dist x'

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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
_inst : ∀ (a : A), CompactSpace ↑(σ R a)
this : ContinuousFunctionalCalculus R p
g₁ g₂ : C(↑(σ R a), R)
x : ↑(σ R a)
x' : ↑(σ S a) := Subtype.map ⇑(algebraMap R S) ⋯ x
⊢ dist (g₁ x) (g₂ x) =
    dist
      (({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
          (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
        x')
      (({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
          (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
        x')

Proof state:
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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
_inst : ∀ (a : A), CompactSpace ↑(σ R a)
this : ContinuousFunctionalCalculus R p
g₁ g₂ : C(↑(σ R a), R)
⊢ dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ })) =
    dist g₁ g₂

Tactic:
refine le_antisymm ?_ ?_

Result:
case intro.refine_1
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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
_inst : ∀ (a : A), CompactSpace ↑(σ R a)
this : ContinuousFunctionalCalculus R p
g₁ g₂ : C(↑(σ R a), R)
⊢ dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ })) ≤
    dist g₁ g₂

case intro.refine_2
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✝³ : MetricSpace A
inst✝² : IsometricContinuousFunctionalCalculus S A q
inst✝¹ : CompleteSpace R
inst✝ : ContinuousMap.UniqueHom R A
f : C(S, R)
halg : Isometry ⇑(algebraMap R S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts a ⇑f
_inst : ∀ (a : A), CompactSpace ↑(σ R a)
this : ContinuousFunctionalCalculus R p
g₁ g₂ : C(↑(σ R a), R)
⊢ dist g₁ g₂ ≤
    dist
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₁.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (g₂.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))