-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric (goal)
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 : Semifield S
inst_6 : StarRing S
inst_7 : MetricSpace S
inst_8 : IsTopologicalSemiring S
inst_9 : ContinuousStar S
inst_10 : Ring A
inst_11 : StarRing A
inst_12 : Algebra S A
inst_13 : Algebra R S
inst_14 : Algebra R A
inst_15 : IsScalarTower R S A
inst_16 : StarModule R S
inst_17 : ContinuousSMul R S
inst_18 : MetricSpace A
inst_19 : IsometricContinuousFunctionalCalculus S A q
inst_20 : CompleteSpace R
inst_21 : ContinuousMap.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 ∧ SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
a : A
ha : p a
ha' : q a
haf : SpectrumRestricts.{u_1, u_2, u_3} (R := R) (S := S) a (⇑f : (a : S) → R)
this : ContinuousFunctionalCalculus R A p
g₁ g₂ : C((↑(σ R a) : Type u_1), R)
refine_1 :
  dist.{u_2} (α := C((↑(σ S a) : Type u_2), S))
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(R, S) }
        (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 := ⋯ : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) }))
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(R, S) }
        (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 := ⋯ : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) })) ≤
    dist g₁ g₂
⊢ dist.{u_2} (α := C((↑(σ S a) : Type u_2), S))
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(R, S) }
        (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 := ⋯ : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) }))
      (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := ⋯ : C(R, S) }
        (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 := ⋯ : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) })) =
    dist g₁ g₂
have refine_2 : dist g₁ g₂ ≤
  dist.{u_2} (α := C((↑(σ S a) : Type u_2), S))
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry }
      (g₁.comp
        { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σ S a) (q := fun (x : R) ↦ x ∈ σ R a) (⇑f : (a : S) → R) sorry,
          continuous_toFun := sorry : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) }))
    (ContinuousMap.comp { toFun := (⇑(StarAlgHom.ofId R S) : (a : R) → S), continuous_toFun := sorry }
      (g₂.comp
        { toFun := Subtype.map (p := fun (x : S) ↦ x ∈ σ S a) (q := fun (x : R) ↦ x ∈ σ R a) (⇑f : (a : S) → R) sorry,
          continuous_toFun := sorry : ContinuousMap.{u_2, u_1} (↑(σ S a) : Type u_2) (↑(σ R a) : Type u_1) }))
Tactic: refine le_antisymm ?_ ?_