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