-- 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) ((φ : (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)
rw :
  ∀
    (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))) =
      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))

Tactic:
rw [← sub_eq_zero] at this ⊢

Premises used: sub_eq_zero