-- 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)
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