-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
p q : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Field S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalRing S
inst_9 : ContinuousStar S
inst_10 : NonUnitalRing A
inst_11 : StarRing A
inst_12 : Module S A
inst_13 : IsScalarTower S A A
inst_14 : SMulCommClass S A A
inst_15 : Algebra R S
inst_16 : Module R A
inst_17 : IsScalarTower R S A
inst_18 : StarModule R S
inst_19 : ContinuousSMul R S
inst_20 : IsScalarTower R A A
inst_21 : SMulCommClass R A A
inst_22 : MetricSpace A
inst_23 : NonUnitalIsometricContinuousFunctionalCalculus S A q
inst_24 : CompleteSpace R
inst_25 : ContinuousMapZero.UniqueHom R A
f : C(S, R)
halg : Isometry.{u_1, u_2} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h0 : p 0
h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : QuasispectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : NonUnitalContinuousFunctionalCalculus R A p
g₁ g₂ : ContinuousMapZero (↑(σₙ R a) : Type u_1) R
x : (↑(σₙ R a) : Type u_1)
x' : (↑(σₙ S a) : Type u_2) :=
  Subtype.map (p := fun (x : R) ↦ x ∈ σₙ R a) (q := fun (x : S) ↦ x ∈ σₙ S a) (⇑(algebraMap R S) : (a : R) → S) ⋯ x
apply :
  dist (α := R) (((↑g₁ : C((↑(σₙ R a) : Type u_1), R)) : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      (((↑g₂ : C((↑(σₙ R a) : Type u_1), R)) : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) =
    dist (α := S)
      (((↑(ContinuousMapZero.comp
                  { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
                  (g₁.comp
                    {
                      toFun :=
                        Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R)
                          ⋯,
                      continuous_toFun := ⋯, map_zero' := ⋯ :
                      ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) :
              C((↑(σₙ S a) : Type u_2), S)) :
            (a : (↑(σₙ S a) : Type u_2)) → S)
          x' :
        S)
      (((↑(ContinuousMapZero.comp
                  { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
                  (g₂.comp
                    {
                      toFun :=
                        Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R)
                          ⋯,
                      continuous_toFun := ⋯, map_zero' := ⋯ :
                      ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) })) :
              C((↑(σₙ S a) : Type u_2), S)) :
            (a : (↑(σₙ S a) : Type u_2)) → S)
          x' :
        S)
⊢ dist (α := R) (((↑g₁ : C((↑(σₙ R a) : Type u_1), R)) : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
      (((↑g₂ : C((↑(σₙ R a) : Type u_1), R)) : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ≤
    dist (α := ContinuousMapZero (↑(σₙ S a) : Type u_2) S)
      (ContinuousMapZero.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
        (g₁.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }))
      (ContinuousMapZero.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯, map_zero' := ⋯ }
        (g₂.comp
          { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σₙ S a) (q := fun (x : R) ↦ x ∈ σₙ R a) (⇑f : (a : S) → R) ⋯,
            continuous_toFun := ⋯, map_zero' := ⋯ :
            ContinuousMapZero.{u_2, u_1} (↑(σₙ S a) : Type u_2) (↑(σₙ R a) : Type u_1) }))

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

Premises used: ContinuousMap.dist_apply_le_dist, le_of_eq_of_le