-- Module: Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
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
a : CliffordAlgebra Q
r : R
rw :
  (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (α := CliffordAlgebra Q)
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) a) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
rw₁ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
rw₂ rw₃ :
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
⊢ (((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q)
            (HMul.hMul (β := CliffordAlgebra Q) a
              ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)) :
          Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
        (a : Module.Dual R M) → CliffordAlgebra Q)
      d =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((((contractRight : (a : CliffordAlgebra Q) → Module.Dual R M →ₗ[R] CliffordAlgebra Q) a :
              Module.Dual R M →ₗ[R] CliffordAlgebra Q) :
            (a : Module.Dual R M) → CliffordAlgebra Q)
          d :
        CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)

Tactic:
rw [← Algebra.commutes, contractRight_algebraMap_mul, Algebra.commutes]

Premises used: CliffordAlgebra.contractRight_algebraMap_mul, Algebra.commutes