awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : 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
ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)
ξ' : 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)

Tactic:
⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩

Premises used: Continuous.comp, And.intro, NonUnitalStarAlgHom.continuous_realContinuousMapZeroOfNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : 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
ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)
ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp
    (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })
refine_1 :
  Continuous (X := C((↑s' : Type), ℝ)₀) (Y := C((↑s : Type), ℝ)₀)
    (⇑(↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
              (nonUnitalStarAlgHom_precomp ℝ
                { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
          C((↑s' : Type), ℝ)₀ →ₙ* C((↑s : Type), ℝ)₀) :
      (a : C((↑s' : Type), ℝ)₀) → C((↑s : Type), ℝ)₀)
refine_2 :
  Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)₀) → A) (ContinuousMapZero.id s') : A)
    ((ξ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
⊢ 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)

Tactic:
refine ⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : 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
ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)
ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp
    (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })
refine_1 :
  Continuous (X := C((↑s' : Type), ℝ)₀) (Y := C((↑s : Type), ℝ))
    (Function.comp (β := C((↑s : Type), ℝ)₀) _root_.toContinuousMap
      (⇑(↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (nonUnitalStarAlgHom_precomp ℝ
                  { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
            C((↑s' : Type), ℝ)₀ →ₙ* C((↑s : Type), ℝ)₀) :
        (a : C((↑s' : Type), ℝ)₀) → C((↑s : Type), ℝ)₀))
⊢ Continuous (X := C((↑s' : Type), ℝ)₀) (Y := C((↑s : Type), ℝ)₀)
    (⇑(↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
              (nonUnitalStarAlgHom_precomp ℝ
                { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
          C((↑s' : Type), ℝ)₀ →ₙ* C((↑s : Type), ℝ)₀) :
      (a : C((↑s' : Type), ℝ)₀) → C((↑s : Type), ℝ)₀)

Tactic:
rw [continuous_induced_rng]

Premises used: continuous_induced_rng
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : 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
ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)
ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp
    (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })
⊢ Continuous (X := C((↑s' : Type), ℝ)₀) (Y := C((↑s : Type), ℝ))
    (Function.comp (β := C((↑s : Type), ℝ)₀) _root_.toContinuousMap
      (⇑(↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (nonUnitalStarAlgHom_precomp ℝ
                  { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
            C((↑s' : Type), ℝ)₀ →ₙ* C((↑s : Type), ℝ)₀) :
        (a : C((↑s' : Type), ℝ)₀) → C((↑s : Type), ℝ)₀))

Tactic:
ContinuousMap.continuous_precomp _ |>.comp continuous_induced_dom

Premises used: Continuous.comp, ContinuousMap.comp, toContinuousMap, continuous_induced_dom, ContinuousMap.continuous_precomp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : 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
ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)
ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp
    (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })
⊢ Continuous (X := C((↑s' : Type), ℝ)₀) (Y := C((↑s : Type), ℝ))
    (Function.comp (β := C((↑s : Type), ℝ)₀) _root_.toContinuousMap
      (⇑(↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (nonUnitalStarAlgHom_precomp ℝ
                  { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
            C((↑s' : Type), ℝ)₀ →ₙ* C((↑s : Type), ℝ)₀) :
        (a : C((↑s' : Type), ℝ)₀) → C((↑s : Type), ℝ)₀))

Tactic:
exact ContinuousMap.continuous_precomp _ |>.comp continuous_induced_dom

Premises used: Continuous.comp, continuous_induced_dom, ContinuousMap.continuous_precomp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : 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
ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)
ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp
    (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })
⊢ Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)₀) → A) (ContinuousMapZero.id s') : A)
    ((ξ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)

Tactic:
ξ.realContinuousMapZeroOfNNReal_apply_comp_toReal (.id _)

Premises used: NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, Set.Mem, setOf, Equiv.setCongr, ContinuousMap.comp, Equiv.subtypeEquiv, NNReal, toContinuousMap, ContinuousMapZero.id, ContinuousMap.id, Equiv.subtypeEquivProp, ContinuousMapZero.comp, Set.image, Set.range, NNReal.toReal, ContinuousMap.restrict
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : 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
ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)
ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
  ξ.realContinuousMapZeroOfNNReal.comp
    (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })
⊢ Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)₀) → A) (ContinuousMapZero.id s') : A)
    ((ξ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)

Tactic:
exact ξ.realContinuousMapZeroOfNNReal_apply_comp_toReal (.id _)

Premises used: NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal, ContinuousMapZero.id
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : 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
⊢ ∀ (ξ : 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)

Tactic:
have (ξ : C(s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A) (hξ : Continuous ξ) :
        (let ξ' := ξ.realContinuousMapZeroOfNNReal.comp <|
          ContinuousMapZero.nonUnitalStarAlgHom_precomp ℝ ⟨e, e0⟩;
          Continuous ξ' ∧ ξ' (.id s') = ξ (.id s)) := by
      intro ξ'
      refine ⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩
      · rw [continuous_induced_rng]
        exact ContinuousMap.continuous_precomp _ |>.comp continuous_induced_dom
      · exact ξ.realContinuousMapZeroOfNNReal_apply_comp_toReal (.id _)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 :
  ∀ (ξ : 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)
⊢ Continuous[_, inst_5]
    (⇑(φ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)

Tactic:
obtain ⟨hφ', hφ_id⟩ := this φ hφ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 :
  ∀ (ξ : 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)
⊢ 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)

Tactic:
obtain ⟨hφ', hφ_id⟩ := this φ hφ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 :
  ∀ (ξ : 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)
⊢ Continuous[_, inst_5]
    (⇑(ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)

Tactic:
obtain ⟨hψ', hψ_id⟩ := this ψ hψ