-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
v : M
x fx : CliffordAlgebra Q
rw :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₁ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) *
          fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₂ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HMul.hMul (α := CliffordAlgebra Q)
          ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) v) : CliffordAlgebra Q)
          fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₃ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) -
        HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₄ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
          (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x) +
      HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₅ :
  HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
        HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
          (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) +
      HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
rw₆ : 0 + HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx = HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
⊢ HSMul.hSMul (α := R) ((d : (a : M) → R) v : R)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) x) -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q)
        (HSMul.hSMul (α := R) ((d : (a : M) → R) v : R) x -
          HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) v : CliffordAlgebra Q) fx) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
have rw₇ : HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx = HSMul.hSMul (α := R) ((Q : (a : M) → R) v : R) fx
Tactic: rw [mul_sub, ← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← sub_add, mul_smul_comm, sub_self,
    zero_add]