-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
inst_6 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
φ ψ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst_4] (⇑φ : (a : C((↑s : Type), ℝ≥0)) → A)
hψ : Continuous[_, inst_4] (⇑ψ : (a : C((↑s : Type), ℝ≥0)) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)),
    let ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
      ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))));
    Continuous[_, inst_4] (⇑ξ' : (a : C((↑s' : Type), ℝ)) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)) → A) (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hφ' :
  Continuous[_, inst_4]
    (⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hψ' :
  Continuous[_, inst_4]
    (⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hψ_id :
  Eq (α := A)
    ((ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hs' : CompactSpace (↑s' : Type)
h' :
  Eq (α := C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A)
    (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
    (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
h'' :
  Eq (α := C((↑s : Type), ℝ) →⋆ₐ[ℝ] A)
    (StarAlgHom.comp (B := C((↑s' : Type), ℝ))
      (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
      (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e.symm : C((↑s' : Type), (↑s : Type)))))
    (StarAlgHom.comp (B := C((↑s' : Type), ℝ))
      (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
      (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e.symm : C((↑s' : Type), (↑s : Type)))))
⊢ Eq (α := C((↑s : Type), ℝ) →⋆ₐ[ℝ] C((↑s : Type), ℝ))
    (StarAlgHom.comp (B := C((↑s' : Type), ℝ)) (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))
      (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e.symm : C((↑s' : Type), (↑s : Type)))))
    (StarAlgHom.id ℝ C((↑s : Type), ℝ))

Tactic:
have : (ContinuousMap.compStarAlgHom' ℝ ℝ (e : C(s, s'))).comp
        (ContinuousMap.compStarAlgHom' ℝ ℝ (e.symm : C(s', s))) = StarAlgHom.id _ _ := by
      ext1; simp