Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique

Goal state before:
pp: X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this✝¹ : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
this✝ :
  ∀ (ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A),
    Continuous[_, inst✝⁴] ⇑ξ →
      let ξ' :=
        ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 });
      Continuous[_, inst✝⁴] ⇑ξ' ∧ ξ' (ContinuousMapZero.id s') = ξ (ContinuousMapZero.id s)
hφ' :
  Continuous[_, inst✝⁴]
    ⇑(φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hφ_id :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    φ (ContinuousMapZero.id s)
hψ' :
  Continuous[_, inst✝⁴]
    ⇑(ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hψ_id :
  (ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    ψ (ContinuousMapZero.id s)
hs' : CompactSpace ↑s'
this : ContinuousMapZero.UniqueHom ℝ A
h' :
  φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }) =
    ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })
h'' :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' }) =
    (ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' })
⊢ φ = ψ

Tactic:
have : (ContinuousMapZero.nonUnitalStarAlgHom_precomp ℝ ⟨(e : C(s, s')), e0⟩).comp
        (ContinuousMapZero.nonUnitalStarAlgHom_precomp ℝ ⟨(e.symm : C(s', s)), e0'⟩) =
        NonUnitalStarAlgHom.id _ _ := by
      ext; simp

Goal state after:
X : Type u_1
inst✝⁹ : TopologicalSpace X
inst✝⁸ : Zero X
A : Type u_2
inst✝⁷ : NonUnitalRing A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsSemitopologicalRing A
inst✝² : IsScalarTower ℝ A A
inst✝¹ : SMulCommClass ℝ A A
inst✝ : T2Space A
s : Set ℝ≥0
hs : CompactSpace ↑s
h0 : Fact (0 ∈ s)
φ ψ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst✝⁴] ⇑φ
hψ : Continuous[_, inst✝⁴] ⇑ψ
h : φ (ContinuousMapZero.id s) = ψ (ContinuousMapZero.id s)
s' : Set ℝ := toReal '' s
e : ↑s ≃ₜ ↑s' := isEmbedding_coe.homeomorphImage s
this✝² : Fact (0 ∈ s')
e0 : e 0 = 0
e0' : e.symm 0 = 0
this✝¹ :
  ∀ (ξ : C(↑s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A),
    Continuous[_, inst✝⁴] ⇑ξ →
      let ξ' :=
        ξ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 });
      Continuous[_, inst✝⁴] ⇑ξ' ∧ ξ' (ContinuousMapZero.id s') = ξ (ContinuousMapZero.id s)
hφ' :
  Continuous[_, inst✝⁴]
    ⇑(φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hφ_id :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    φ (ContinuousMapZero.id s)
hψ' :
  Continuous[_, inst✝⁴]
    ⇑(ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
hψ_id :
  (ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }))
      (ContinuousMapZero.id s') =
    ψ (ContinuousMapZero.id s)
hs' : CompactSpace ↑s'
this✝ : ContinuousMapZero.UniqueHom ℝ A
h' :
  φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }) =
    ψ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })
h'' :
  (φ.realContinuousMapZeroOfNNReal.comp (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' }) =
    (ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 })).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' })
this :
  (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e, map_zero' := e0 }).comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := ↑e.symm, map_zero' := e0' }) =
    NonUnitalStarAlgHom.id ℝ C(↑s, ℝ)₀
⊢ φ = ψ