-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic
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
h : QuadraticMap.IsOrtho Q a b
y : CliffordAlgebra Q
rw :
  (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) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y)
rw₁ :
  (algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) 0 * (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) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y)
rw₂ :
  0 * (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) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y)
rw₃ :
  0 -
      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) b : CliffordAlgebra Q) *
        HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) y)
rw₄ rw₅ :
  -(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) 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 =
    -(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_ι_mul_ι_mul_comm, h.polar_eq_zero, map_zero, zero_mul, zero_sub]

Premises used: MulZeroClass.zero_mul, map_zero, QuadraticMap.IsOrtho.polar_eq_zero, zero_sub, CliffordAlgebra.mul_ι_mul_ι_mul_comm