awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : NonUnitalRing A
inst_4 : StarRing A
inst_5 : Module 𝕜 A
inst_6 : IsScalarTower 𝕜 A A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace.{u_1} (↑s : Type u_1)
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
f : ContinuousMapZero (↑s : Type u_1) 𝕜
hf :
  f ∈
    (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
      Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
⊢ ContinuousMapZero.id s ∈ (↑(NonUnitalStarAlgHom.equalizer φ ψ) : Set (ContinuousMapZero (↑s : Type u_1) 𝕜))

Tactic:
exact h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f : C(X, ℝ)₀
⊢ Eq (α := ℝ≥0) (((ContinuousMap.realToNNReal.comp (↑f : C(X, ℝ)) : C(X, ℝ≥0)) : (a : X) → ℝ≥0) 0 : ℝ≥0) (0 : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f : C(X, ℝ)₀
x : X
⊢ (f.toNNReal : (a : X) → ℝ≥0) x = Real.toNNReal ((f : (a : X) → ℝ) x)

Tactic:
rfl

Premises used: NNReal.mk, rfl, Real.toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
rw : Continuous (X := C(X, ℝ)₀) (Y := C(X, ℝ≥0)) (_root_.toContinuousMap ∘ toNNReal)
⊢ Continuous.{u_1, u_1} (X := C(X, ℝ)₀) toNNReal

Tactic:
rw [continuous_induced_rng]

Premises used: continuous_induced_rng
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
⊢ Continuous (X := C(X, ℝ)₀) (Y := C(X, ℝ≥0)) (ContinuousMap.toNNReal ∘ _root_.toContinuousMap)

Tactic:
ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom

Premises used: ContinuousMap.continuous_postcomp, Continuous.comp, continuous_induced_dom, ContinuousMap.toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
⊢ Continuous (X := C(X, ℝ)₀) (Y := C(X, ℝ≥0)) (ContinuousMap.toNNReal ∘ _root_.toContinuousMap)

Tactic:
exact ContinuousMap.continuous_postcomp _ |>.comp continuous_induced_dom

Premises used: ContinuousMap.continuous_postcomp, Continuous.comp, continuous_induced_dom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f : C(X, ℝ)₀
⊢ Eq.{u_1 + 1} (α := C(X, ℝ≥0)) (ContinuousMap.toNNReal ((toContinuousMapHom : (a : C(X, ℝ)₀) → C(X, ℝ)) f))
    ((toContinuousMapHom : (a : C(X, ℝ≥0)₀) → C(X, ℝ≥0)) f.toNNReal)

Tactic:
rfl

Premises used: ContinuousMap.comp, NNReal.mk, toContinuousMap, ContinuousMap.toNNReal, rfl, Real.toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
h : ∀ (x : X), (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
⊢ (r • f).toNNReal = r • f.toNNReal

Tactic:
ext x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
pos :
  ∀ (h : LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)),
    (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
neg :
  ∀ (h : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)),
    (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
⊢ (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
by_cases! h : 0 ≤ f x

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
h : LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simpa [max_eq_left h, NNReal.smul_def] using mul_nonneg r.coe_nonneg h

Premises used: mul_nonneg, max_eq_left, NNReal.smul_def, NNReal.coe_nonneg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
h : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)
⊢ (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simpa [max_eq_right h.le, NNReal.smul_def]
      using mul_nonpos_of_nonneg_of_nonpos r.coe_nonneg h.le

Premises used: LT.lt.le, max_eq_right, NNReal.smul_def, NNReal.coe_nonneg, mul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f g : C(X, ℝ)₀
a :
  Eq (α := C(X, ℝ≥0)) (↑((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) : C(X, ℝ≥0))
    (↑((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) : C(X, ℝ≥0))
⊢ (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
    (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal

Tactic:
apply toContinuousMap_injective

Premises used: ContinuousMapZero.toContinuousMap_injective
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f g : C(X, ℝ)₀
⊢ Eq (α := C(X, ℝ≥0)) (↑((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) : C(X, ℝ≥0))
    (↑((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) : C(X, ℝ≥0))

Tactic:
simpa only [← toContinuousMapHom_apply, map_add, map_mul, map_neg, toContinuousMapHom_toNNReal]
    using (f : C(X, ℝ)).toNNReal_mul_add_neg_mul_add_mul_neg_eq g

Premises used: map_add, map_neg, toContinuousMap, ContinuousMap.toNNReal_mul_add_neg_mul_add_mul_neg_eq, map_mul, ContinuousMapZero.toContinuousMapHom_toNNReal, ContinuousMapZero.toContinuousMapHom_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f g : C(X, ℝ)₀
a :
  Eq (α := C(X, ℝ≥0)) (↑((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) : C(X, ℝ≥0))
    (↑((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) : C(X, ℝ≥0))
⊢ (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal

Tactic:
apply toContinuousMap_injective

Premises used: ContinuousMapZero.toContinuousMap_injective
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f g : C(X, ℝ)₀
⊢ Eq (α := C(X, ℝ≥0)) (↑((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) : C(X, ℝ≥0))
    (↑((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) : C(X, ℝ≥0))

Tactic:
simpa only [← toContinuousMapHom_apply, map_add, map_mul, map_neg, toContinuousMapHom_toNNReal]
    using (f : C(X, ℝ)).toNNReal_add_add_neg_add_neg_eq g

Premises used: map_add, map_neg, toContinuousMap, map_mul, ContinuousMapZero.toContinuousMapHom_toNNReal, ContinuousMapZero.toContinuousMapHom_apply, ContinuousMap.toNNReal_add_add_neg_add_neg_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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, ℝ)₀
simp :
  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) =
    HSMul.hSMul (α := ℝ) ((MonoidHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
      (HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A))

Tactic:
simp only [MonoidHom.id_apply]

Premises used: MonoidHom.id_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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)
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)
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
⊢ 0 ≤ r

Tactic:
hr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
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)
⊢ 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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : C(X, ℝ)₀
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:
simp only [← smul_def, toNNReal_smul, map_smul, toNNReal_neg_smul, smul_sub]

Premises used: smul_sub, NNReal.smul_def, ContinuousMapZero.toNNReal_neg_smul, ContinuousMapZero.toNNReal_smul, map_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
⊢ 0 < -r

Tactic:
rw [← neg_pos] at hr

Premises used: neg_pos
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
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)
⊢ 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]

Premises used: neg_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
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)
⊢ 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]

Premises used: neg_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
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)
⊢ 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]

Premises used: neg_neg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
⊢ 0 ≤ -r

Tactic:
hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
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)
⊢ 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

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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)
⊢ 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:
simp only [neg_smul, ← smul_def, toNNReal_neg_smul, map_smul, toNNReal_smul, smul_sub,
        sub_neg_eq_add]

Premises used: neg_smul, smul_sub, NNReal.smul_def, ContinuousMapZero.toNNReal_neg_smul, ContinuousMapZero.toNNReal_smul, sub_neg_eq_add, map_smul
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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)
neg₁ 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)

Tactic:
rw [sub_eq_add_neg, add_comm]

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (toNNReal 0) : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (toNNReal (-0)) : A) =
    0

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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, ℝ)₀
⊢ 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
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)
⊢ 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
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)
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