-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
y : CliffordAlgebra Q
rw :
  x *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) y) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
rw₁ :
  x *
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        y) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
rw₂ :
  x *
      (((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) -
          HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
            ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)) *
        y) =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
⊢ HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) y =
    (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
        (x * y) -
      HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
have rw₃ : x *
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) * y -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) *
        y) =
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) *
      (x * y) -
    HMul.hMul (β := CliffordAlgebra Q) x ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) *
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y
Tactic: rw [mul_assoc, ← mul_assoc _ _ y, ι_mul_ι_comm, sub_mul, mul_sub, Algebra.left_comm, mul_assoc,
    mul_assoc]