awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : NonUnitalStarAlgHom.{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, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) f : A)
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)₀) → A)
          ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
        A)
      ((φ : (a : C(X, ℝ≥0)₀) → A)
          (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
        A) =
    (φ : (a : C(X, ℝ≥0)₀) → A) f
have h₁ : Eq.{u_2 + 1} (α := A)
  ((φ : (a : C(X, ℝ≥0)₀) → A)
      (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := sorry : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
    A)
  ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A)
Tactic: convert_to φ f - φ 0 = φ f using 2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : NonUnitalStarAlgHom.{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, map_zero' := ⋯ : 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, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A)
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)₀) → A)
          ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
        A)
      ((φ : (a : C(X, ℝ≥0)₀) → A)
          (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
        A) =
    (φ : (a : C(X, ℝ≥0)₀) → A) f
have 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
Tactic: convert_to φ f - φ 0 = φ f using 2
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : NonUnitalStarAlgHom.{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
have rw : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) (0 : A) = (φ : (a : C(X, ℝ≥0)₀) → A) f
Tactic: rw [map_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : NonUnitalStarAlgHom.{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
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A) =
    (φ : (a : C(X, ℝ≥0)₀) → A) f
have rw₁ : Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A)
Tactic: rw [map_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)₀) → A)
        ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) f : A)
have h : ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := sorry : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal = f
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
⊢ ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal = f
have h : ∀ (x : X),
  (↑((({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := sorry : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
            (a : X) → ℝ≥0)
          x) :
      ℝ) =
    (↑((f : (a : X) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)₀) → A)
        (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A)
have h : (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := sorry : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal = 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
⊢ (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal = 0
have h : ∀ (x : X),
  (↑(((-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := sorry : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
            (a : X) → ℝ≥0)
          x) :
      ℝ) =
    (↑(((0 : C(X, ℝ≥0)₀) : (a : X) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ ψ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
⊢ φ = ψ
have 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
-- 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
⊢ φ = ψ
have this : Fact (0 ∈ s')
Tactic: have : Fact (0 ∈ s') := ⟨0, Fact.out, coe_zero⟩
-- 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 : Fact (0 ∈ s')
⊢ φ = ψ
have e0 : Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0
Tactic: have e0 : e 0 = 0 := rfl
-- 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 : Fact (0 ∈ s')
e0 : Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0
⊢ φ = ψ
have e0' : Eq (α := (↑s : Type)) ((e.symm : (a : (↑s' : Type)) → (↑s : Type)) 0) 0
Tactic: have e0' : e.symm 0 = 0 := e.symm_apply_eq.mpr e0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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)
have 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), ℝ)₀)
Tactic: refine ⟨ξ.continuous_realContinuousMapZeroOfNNReal hξ |>.comp <| ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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), ℝ)₀)
⊢ 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)
have refine_2 : 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 <| ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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), ℝ)₀)
    (⇑(↑(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), ℝ)₀)
have 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), ℝ)₀))
Tactic: rw [continuous_induced_rng]
-- 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 : 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
⊢ φ = ψ
have 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)
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 _)
-- 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 :
  ∀ (ξ : 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)
⊢ φ = ψ
have hφ' : 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φ
-- 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 :
  ∀ (ξ : 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)
⊢ φ = ψ
have 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)
Tactic: obtain ⟨hφ', hφ_id⟩ := this φ hφ