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 g : C(X, ℝ)
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)) =
    0
⊢ 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)) =
    0

Tactic:
this
-- 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 g : C(X, ℝ)
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)) =
    0
h :
  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))) =
    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))) =
    0

Tactic:
convert! this using 1
-- 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 g : C(X, ℝ)
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)) =
    0
⊢ 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))) =
    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))

Tactic:
abel
-- 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
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal 0) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-0)) : A) =
    0

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
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f g : C(X, ℝ)
⊢ 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))
-- 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 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)
⊢ 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 ⊢

Premises used: map_add
-- 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 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)
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
⊢ 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)

Tactic:
rw [← sub_eq_zero] at this ⊢

Premises used: sub_eq_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
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
⊢ 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

Tactic:
this
-- 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 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
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)
⊢ 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:
convert! this using 1
-- 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 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)) =
    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:
abel
-- 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
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
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
⊢ 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

Premises used: le_total, OfNat.ofNat
-- 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
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r

Tactic:
hr
-- 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
r : ℝ
hr : 0 ≤ r
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 : ℝ)
⊢ 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
-- 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
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:
simpa only [ContinuousMap.toNNReal_algebraMap, ContinuousMap.toNNReal_neg_algebraMap,
        map_zero, sub_zero] using AlgHomClass.commutes φ r

Premises used: ContinuousMap.toNNReal_neg_algebraMap, sub_zero, ContinuousMap.toNNReal_algebraMap, map_zero, AlgHomClass.commutes
-- 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
r : ℝ
hr : r ≤ 0
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)
⊢ 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)]

Premises used: neg_neg, map_neg, Neg.neg
-- 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
r : ℝ
hr : r ≤ 0
⊢ 0 ≤ -r

Tactic:
rw [← neg_nonneg] at hr

Premises used: neg_nonneg
-- 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
r : ℝ
hr : 0 ≤ -r
⊢ 0 ≤ -r

Tactic:
hr
-- 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
r : ℝ
hr : 0 ≤ -r
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 : ℝ))
⊢ 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
-- 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
r_1 : ℝ
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:
simpa only [map_neg, ContinuousMap.toNNReal_neg_algebraMap, map_zero,
        ContinuousMap.toNNReal_algebraMap, zero_sub, neg_inj] using AlgHomClass.commutes φ r

Premises used: ContinuousMap.toNNReal_neg_algebraMap, ContinuousMap.toNNReal_algebraMap, map_zero, map_neg, AlgHomClass.commutes, neg_inj, zero_sub