awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (star f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-star f).toNNReal : A) =
    star
      (HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A))

Tactic:
simp only [star_trivial, star_sub, ← map_star]

Premises used: StarHomClass.map_star, TrivialStar.star_trivial, star_sub
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
hφ : Continuous[_, inst_4] (⇑φ : (a : C(X, ℝ≥0)) → A)
dsimp :
  Continuous[_, inst_4] fun (f : C(X, ℝ)) ↦
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
⊢ Continuous[_, inst_4] (⇑φ.realContinuousMapOfNNReal : (a : C(X, ℝ)) → A)

Tactic:
dsimp [realContinuousMapOfNNReal]

Premises used: StarAlgHom.realContinuousMapOfNNReal
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
hφ : Continuous[_, inst_4] (⇑φ : (a : C(X, ℝ≥0)) → A)
⊢ Continuous[_, inst_4] fun (f : C(X, ℝ)) ↦
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)

Tactic:
fun_prop
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
simp :
  HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) ({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal :
        A)
      ((φ : (a : C(X, ℝ≥0)) → A)
          (-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal :
        A) =
    (φ : (a : C(X, ℝ≥0)) → A) f
⊢ Eq.{u_2 + 1} (α := A)
    ((φ.realContinuousMapOfNNReal : (a : C(X, ℝ)) → A)
        ({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f) :
      A)
    ((φ : (a : C(X, ℝ≥0)) → A) f : A)

Tactic:
simp only [realContinuousMapOfNNReal_apply]

Premises used: StarAlgHom.realContinuousMapOfNNReal_apply
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
h :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)) → A) ({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)) → A) f : A)
h₁ :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)) → A) (-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)) → A) 0 : A)
convert_to :
  HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f : A) ((φ : (a : C(X, ℝ≥0)) → A) 0 : A) =
    (φ : (a : C(X, ℝ≥0)) → A) f
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) ({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal :
        A)
      ((φ : (a : C(X, ℝ≥0)) → A)
          (-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal :
        A) =
    (φ : (a : C(X, ℝ≥0)) → A) f

Tactic:
convert_to φ f - φ 0 = φ f using 2

Premises used: OfNat.ofNat, DFunLike.coe
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
rw : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f : A) (0 : A) = (φ : (a : C(X, ℝ≥0)) → A) f
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)) → A) f : A) ((φ : (a : C(X, ℝ≥0)) → A) f : A)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f : A) ((φ : (a : C(X, ℝ≥0)) → A) 0 : A) =
    (φ : (a : C(X, ℝ≥0)) → A) f

Tactic:
rw [map_zero, sub_zero]

Premises used: sub_zero, map_zero
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f : A) ((φ : (a : C(X, ℝ≥0)) → A) 0 : A) =
    (φ : (a : C(X, ℝ≥0)) → A) f

Tactic:
on_goal -1 => rw [map_zero, sub_zero]

Premises used: sub_zero, map_zero
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
h : ({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal = f
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)) → A) ({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)) → A) f : A)

Tactic:
congr
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
h :
  ∀ (x : X),
    (↑((({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) =
      (↑((f : (a : X) → ℝ≥0) x) : ℝ)
⊢ ({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal = f

Tactic:
ext x
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
x : X
⊢ (↑((({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) =
    (↑((f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simp
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
h : (-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal = 0
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)) → A) (-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)) → A) 0 : A)

Tactic:
congr
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
h :
  ∀ (x : X),
    (↑(((-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal : (a : X) → ℝ≥0) x) :
        ℝ) =
      (↑(((0 : C(X, ℝ≥0)) : (a : X) → ℝ≥0) x) : ℝ)
⊢ (-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal = 0

Tactic:
ext x
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f : C(X, ℝ≥0)
x : X
⊢ (↑(((-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(((0 : C(X, ℝ≥0)) : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simp
-- 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
φ ψ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
h₁ : ∀ (f : C(X, ℝ≥0)), Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)) → A) f : A) ((ψ : (a : C(X, ℝ≥0)) → A) f : A)
⊢ φ = ψ

Tactic:
ext f
-- 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
φ ψ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
f : C(X, ℝ≥0)
⊢ Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)) → A) f : A) ((ψ : (a : C(X, ℝ≥0)) → A) f : A)

Tactic:
simpa using congr($(h) ((ContinuousMap.mk toReal continuous_coe).comp f))
-- 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
ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)
ξ' : 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)

Tactic:
⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
        ContinuousMap.continuous_precomp _, ?_⟩

Premises used: Continuous.comp, StarAlgHom.continuous_realContinuousMapOfNNReal, And.intro, ContinuousMap.continuous_precomp
-- 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
ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)
ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
  ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))
refine :
  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)
⊢ 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)

Tactic:
refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
        ContinuousMap.continuous_precomp _, ?_⟩
-- 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
ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)
ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
  ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))
⊢ 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)

Tactic:
ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0)

Premises used: Set.Mem, Equiv.setCongr, ContinuousMap.comp, Equiv.subtypeEquiv, StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, NNReal, ContinuousMap.id, Equiv.subtypeEquivProp, Set.image, Set.range, NNReal.toReal, ContinuousMap.restrict
-- 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
ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)
ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
  ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))
⊢ 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)

Tactic:
exact ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0)

Premises used: StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal, NNReal, ContinuousMap.id, ContinuousMap.restrict
-- 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
⊢ ∀ (ξ : 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)

Tactic:
have (ξ : C(s, ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous ξ) :
        (let ξ' := ξ.realContinuousMapOfNNReal.comp <| ContinuousMap.compStarAlgHom' ℝ ℝ e
        Continuous ξ' ∧ ξ' (.restrict s' <| .id ℝ) = ξ (.restrict s <| .id ℝ≥0)) := by
      intro ξ'
      refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
        ContinuousMap.continuous_precomp _, ?_⟩
      exact ξ.realContinuousMapOfNNReal_apply_comp_toReal (.restrict s <| .id ℝ≥0)
-- 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)
⊢ Continuous[_, inst_4]
    (⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (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
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)
⊢ 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)

Tactic:
obtain ⟨hφ', hφ_id⟩ := this φ hφ
-- 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)
⊢ Continuous[_, inst_4]
    (⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)

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