-- 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
a b : M
rw :
  HMul.hMul (β := CliffordAlgebra Q)
      ((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))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
rw₁ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) -
      HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q))
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
rw₂ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) :
          CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) a) : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
rw₄ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) a) : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
rw₅ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) -
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) a) : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
rw₆ :
  HSMul.hSMul (α := R) (β := CliffordAlgebra Q) (QuadraticMap.polar (⇑Q : (a : M) → R) a b)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) -
      HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((Q : (a : M) → R) a : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
rw₇ :
  HSub.hSub (α := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a) :
        CliffordAlgebra Q)
      (HSMul.hSMul (α := R) (β := CliffordAlgebra Q) ((Q : (a : M) → R) a : R)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q)) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
rw₈ :
  HSub.hSub (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a) :
        CliffordAlgebra Q)
      ((ι Q : (a : M) → CliffordAlgebra Q) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b) :
        CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
⊢ HMul.hMul (β := CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) b : CliffordAlgebra Q))
      ((ι Q : (a : M) → CliffordAlgebra Q) a : CliffordAlgebra Q) =
    (ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b)
have rw₉ : Eq (α := CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b) :
    CliffordAlgebra Q)
  ((ι Q : (a : M) → CliffordAlgebra Q)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (QuadraticMap.polar (⇑Q : (a : M) → R) a b) a -
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((Q : (a : M) → R) a : R) b) :
    CliffordAlgebra Q)
Tactic: rw [ι_mul_ι_comm, sub_mul, mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← Algebra.commutes, ←
    Algebra.smul_def, ← map_smul, ← map_smul, ← map_sub]