-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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)
⊢ 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))
have 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
Tactic: rw [← sub_eq_zero] at this ⊢
Cleared hypotheses: this