-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Even (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
A : Type u_3
B : Type u_4
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
m₁ m₂ m₃ : M
rw :
  HMul.hMul (α := CliffordAlgebra Q) ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      (HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q))
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q)) =
    HMul.hMul (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m₂) : CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q))
rw₁ :
  HMul.hMul (α := CliffordAlgebra Q) ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m₂) : CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q)) =
    HMul.hMul (α := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m₂) : CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q))
⊢ HMul.hMul (α := CliffordAlgebra Q) ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      (HMul.hMul (β := CliffordAlgebra Q)
        (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q)
          ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₂ : CliffordAlgebra Q))
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) m₂ : R)
      (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
        ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q))
have rw₂ : HMul.hMul (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m₂) : CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q)) =
  HMul.hMul (α := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) ((Q : (a : M) → R) m₂) : CliffordAlgebra Q)
    (HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₁ : CliffordAlgebra Q)
      ((CliffordAlgebra.ι Q : (a : M) → CliffordAlgebra Q) m₃ : CliffordAlgebra Q))
Tactic: rw [Algebra.smul_def, ι_sq_scalar, Algebra.left_comm]