-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
h0 : Fact (0 ∈ s)
φ ψ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst_5] (⇑φ : (a : C((↑s : Type), ℝ≥0)₀) → A)
hψ : Continuous[_, inst_5] (⇑ψ : (a : C((↑s : Type), ℝ≥0)₀) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this_1 : Fact (0 ∈ s')
e0 : Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0
e0' : Eq (α := (↑s : Type)) ((e.symm : (a : (↑s' : Type)) → (↑s : Type)) 0) 0
this_2 :
  ∀ (ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A) (hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)),
    let ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
      ξ.realContinuousMapZeroOfNNReal.comp
        (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 });
    Continuous[_, inst_5] (⇑ξ' : (a : C((↑s' : Type), ℝ)₀) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)₀) → A) (ContinuousMapZero.id s') : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hφ' :
  Continuous[_, inst_5]
    (⇑(φ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapZeroOfNNReal.comp
            (nonUnitalStarAlgHom_precomp ℝ
              { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
          (a : C((↑s' : Type), ℝ)₀) → A)
        (ContinuousMapZero.id s') :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hψ' :
  Continuous[_, inst_5]
    (⇑(ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
hψ_id :
  Eq (α := A)
    ((ψ.realContinuousMapZeroOfNNReal.comp
            (nonUnitalStarAlgHom_precomp ℝ
              { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
          (a : C((↑s' : Type), ℝ)₀) → A)
        (ContinuousMapZero.id s') :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hs' : CompactSpace (↑s' : Type)
this : ContinuousMapZero.UniqueHom ℝ A
h' :
  Eq (α := C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A)
    (φ.realContinuousMapZeroOfNNReal.comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }))
    (ψ.realContinuousMapZeroOfNNReal.comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }))
⊢ φ = ψ
have h'' : Eq (α := C((↑s : Type), ℝ)₀ →⋆ₙₐ[ℝ] A)
  (NonUnitalStarAlgHom.comp (B := C((↑s' : Type), ℝ)₀)
    (φ.realContinuousMapZeroOfNNReal.comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }))
    (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e.symm : C((↑s' : Type), (↑s : Type))), map_zero' := e0' }))
  (NonUnitalStarAlgHom.comp (B := C((↑s' : Type), ℝ)₀)
    (ψ.realContinuousMapZeroOfNNReal.comp
      (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }))
    (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e.symm : C((↑s' : Type), (↑s : Type))), map_zero' := e0' }))
Tactic: have h'' := congr($(h').comp <|
      ContinuousMapZero.nonUnitalStarAlgHom_precomp ℝ ⟨(e.symm : C(s', s)), e0'⟩)