Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A),
    Continuous[_, inst✝²] ⇑ξ →
      let ξ' := ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e);
      Continuous[_, inst✝²] ⇑ξ' ∧
        ξ' (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) = ξ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hφ' : Continuous[_, inst✝²] ⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hφ_id :
  (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hψ' : Continuous[_, inst✝²] ⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hψ_id :
  (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hs' : CompactSpace ↑s'
h' :
  φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e) =
    ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)
⊢ φ = ψ

Tactic:
have h'' := congr($(h').comp <| ContinuousMap.compStarAlgHom' ℝ ℝ (e.symm : C(s', s)))

Goal state after:
X : Type u_1
inst✝⁶ : TopologicalSpace X
A : Type u_2
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra ℝ A
inst✝² : TopologicalSpace A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
φ ψ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst✝²] ⇑φ
hψ : Continuous[_, inst✝²] ⇑ψ
h : φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) = ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C(↑s, ℝ≥0) →⋆ₐ[ℝ≥0] A),
    Continuous[_, inst✝²] ⇑ξ →
      let ξ' := ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e);
      Continuous[_, inst✝²] ⇑ξ' ∧
        ξ' (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) = ξ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hφ' : Continuous[_, inst✝²] ⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hφ_id :
  (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    φ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hψ' : Continuous[_, inst✝²] ⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
hψ_id :
  (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e))
      (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) =
    ψ (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0))
hs' : CompactSpace ↑s'
h' :
  φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e) =
    ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)
h'' :
  (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)).comp
      (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e.symm) =
    (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e)).comp
      (ContinuousMap.compStarAlgHom' ℝ ℝ ↑e.symm)
⊢ φ = ψ