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
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
pos :
  ∀ (hr : 0 ≤ r),
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
      r •
        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) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have neg : ∀ (hr : r < 0),
  HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: by_cases! hr : 0 ≤ r
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
hr : 0 ≤ r
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have pos : ∀ (r : ℝ≥0),
  HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) ((↑r : ℝ) • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-((↑r : ℝ) • f)).toNNReal : A) =
    (↑r : ℝ) •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
hr : r < 0
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have hr₁ : 0 < -r
Tactic: rw [← neg_pos] at hr
Cleared hypotheses: hr
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
hr : 0 < -r
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have neg : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) (-r • f).toNNReal : A) =
  r •
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: rw [← neg_smul]
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
hr : 0 < -r
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-r • f).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have neg : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (- -r • f).toNNReal : A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) (-r • f).toNNReal : A) =
  r •
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: nth_rw 1 [← neg_neg r]
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
hr : 0 < -r
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (- -r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-r • f).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have neg : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (- -r • f).toNNReal : A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) (-r • f).toNNReal : A) =
  - -r •
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: nth_rw 3 [← neg_neg r]
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
hr : 0 < -r
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (- -r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-r • f).toNNReal : A) =
    - -r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have neg : ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)),
  HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (-(↑r : ℝ) • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) ((↑r : ℝ) • f).toNNReal : A) =
    -(↑r : ℝ) •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: lift -r to ℝ≥0 using hr.le with r
Cleared hypotheses: hr
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r_1 : ℝ
f : C(X, ℝ)₀
r : ℝ≥0
hr : 0 < (↑r : ℝ)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (-(↑r : ℝ) • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) ((↑r : ℝ) • f).toNNReal : A) =
    -(↑r : ℝ) •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have neg : HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A) -
    HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) =
  -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) +
    HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: simp only [neg_smul, ← smul_def, toNNReal_neg_smul, map_smul, toNNReal_smul, smul_sub,
        sub_neg_eq_add]
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r_1 : ℝ
f : C(X, ℝ)₀
r : ℝ≥0
hr : 0 < (↑r : ℝ)
⊢ HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A) -
      HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) =
    -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) +
      HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have neg : HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A) +
    -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) =
  -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) +
    HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: rw [sub_eq_add_neg, add_comm]
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r_1 : ℝ
f : C(X, ℝ)₀
r : ℝ≥0
hr : 0 < (↑r : ℝ)
neg :
  HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A) +
      -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) =
    -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) +
      HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
⊢ HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A) -
      HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) =
    -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) +
      HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have neg₁ : -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) +
    HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A) =
  -HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A) +
    HSMul.hSMul (β := A) r ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: rw [sub_eq_add_neg, add_comm]
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f g : C(X, ℝ)₀
⊢ 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 this : Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)₀) → A) ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) : A)
  ((φ : (a : C(X, ℝ≥0)₀) → A) ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) : A)
Tactic: have := congr(φ $(f.toNNReal_add_add_neg_add_neg_eq g))
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f g : C(X, ℝ)₀
this :
  Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)₀) → A) ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) : A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) ((-(f + g)).toNNReal + f.toNNReal + 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 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)
Tactic: simp only [map_add] at this ⊢
Cleared hypotheses: this
-- 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
φ : NonUnitalStarAlgHom.{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
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
φ : NonUnitalStarAlgHom.{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 rw : 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: rw [← this]
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f g : C(X, ℝ)₀
⊢ 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 this : Eq.{u_2 + 1} (α := A)
  ((φ : (a : C(X, ℝ≥0)₀) → A) ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) : A)
  ((φ : (a : C(X, ℝ≥0)₀) → A) ((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) : A)
Tactic: have := congr(φ $(f.toNNReal_mul_add_neg_mul_add_mul_neg_eq g))
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f g : C(X, ℝ)₀
this :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) : A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) ((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-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 simp : ∀
  (this :
    HAdd.hAdd (α := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (f * g).toNNReal : A)
          (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)₀) → A) g.toNNReal : A)) +
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)₀) → A) (-g).toNNReal : A) =
      HAdd.hAdd (α := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (-(f * g)).toNNReal : A)
          (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)₀) → A) g.toNNReal : A)) +
        HMul.hMul (α := A) (β := 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) =
    HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)₀) → A) g.toNNReal : A) -
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)₀) → A) g.toNNReal : A) -
      (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)₀) → A) (-g).toNNReal : A) -
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)₀) → A) (-g).toNNReal : A))
Tactic: simp only [map_add, map_mul, sub_mul, mul_sub] at this ⊢
Cleared hypotheses: this
-- 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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
hφ : Continuous[_, inst_5] (⇑φ : (a : C(X, ℝ≥0)₀) → A)
⊢ Continuous[_, inst_5] (⇑φ.realContinuousMapZeroOfNNReal : (a : C(X, ℝ)₀) → A)
have dsimp : Continuous[_, inst_5] 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 [realContinuousMapZeroOfNNReal]
-- 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)
    ((φ.realContinuousMapZeroOfNNReal : (a : C(X, ℝ)₀) → A)
        ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : 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, map_zero' := sorry : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      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) f
Tactic: simp only [realContinuousMapZeroOfNNReal_apply]
-- 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)
          ({ 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) f : A)
Tactic: convert_to φ f - φ 0 = φ f using 2