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
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 g : C(X, ℝ)
this :
  HAdd.hAdd (β := A)
      (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A))
      ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) =
    HAdd.hAdd (β := A)
      (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A))
      ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A) =
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A) +
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)
have rw : ∀
  (this :
    HAdd.hAdd (β := A)
          (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A))
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) -
        HAdd.hAdd (β := A)
          (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A))
          ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A) =
      0),
  HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A) -
      (HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A) +
        HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)) =
    0
Tactic: rw [← sub_eq_zero] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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 g : C(X, ℝ)
this :
  HAdd.hAdd (β := A)
        (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A))
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) -
      HAdd.hAdd (β := A)
        (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A))
        ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A) =
    0
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A) -
      (HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A) +
        HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)) =
    0
have h : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A) -
    (HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A) +
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)) =
  HAdd.hAdd (β := A)
      (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A))
      ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) -
    HAdd.hAdd (β := A)
      (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A))
      ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
r : ℝ
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) r
have inl : ∀ (hr : 0 ≤ r),
  HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) r
Tactic: obtain (hr | hr) := le_total 0 r
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
r : ℝ
inl :
  ∀ (hr : 0 ≤ r),
    HSub.hSub (α := A) (β := A)
        ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A) =
      (algebraMap ℝ A : (a : ℝ) → A) r
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) r
have inr : ∀ (hr : r ≤ 0),
  HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) r
Tactic: obtain (hr | hr) := le_total 0 r
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
r : ℝ
hr : 0 ≤ r
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) r
have inl : ∀ (r : ℝ≥0),
  HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (↑r : ℝ))) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (↑r : ℝ))) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) (↑r : ℝ)
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
r : ℝ
hr : r ≤ 0
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) r)) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) r
have inr : HSub.hSub (α := A) (β := A)
    ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (- -r))) : A)
    ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (-r))) : A) =
  (algebraMap ℝ A : (a : ℝ) → A) (- -r)
Tactic: rw [← neg_neg r, ← map_neg, neg_neg (-r)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
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
r : ℝ
hr : r ≤ 0
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (- -r))) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (-r))) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) (- -r)
have hr₁ : 0 ≤ -r
Tactic: rw [← neg_nonneg] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
r : ℝ
hr : 0 ≤ -r
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (- -r))) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (-r))) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) (- -r)
have inr : ∀ (r : ℝ≥0),
  HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (-(↑r : ℝ)))) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (↑r : ℝ))) : A) =
    (algebraMap ℝ A : (a : ℝ) → A) (-(↑r : ℝ))
Tactic: lift -r to ℝ≥0 using hr with r
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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] (⇑φ.realContinuousMapOfNNReal : (a : C(X, ℝ)) → A)
have 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)
Tactic: dsimp [realContinuousMapOfNNReal]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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)
⊢ 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)
have 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
Tactic: simp only [realContinuousMapOfNNReal_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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) ({ 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
have 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)
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
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)
⊢ 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
have 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)
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
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)
⊢ 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
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
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
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
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
⊢ 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
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)
⊢ 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)
have h : ({ toFun := toReal, continuous_toFun := continuous_coe : 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
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)
⊢ ({ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal = f
have h : ∀ (x : X),
  (↑((({ toFun := toReal, continuous_toFun := continuous_coe : 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
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)
⊢ 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)
have h : (-{ toFun := toReal, continuous_toFun := continuous_coe : 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
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)
⊢ (-{ toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) }.comp f).toNNReal = 0
have 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) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
⊢ φ = ψ
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 (goal)
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)
have 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)
Tactic: refine ⟨ξ.continuous_realContinuousMapOfNNReal hξ |>.comp <|
        ContinuousMap.continuous_precomp _, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
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
⊢ φ = ψ
have 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)
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)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
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)
⊢ φ = ψ
have hφ' : 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φ