-- Lean 4 proof step from Mathlib.LinearAlgebra.CliffordAlgebra.Contraction (goal)
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
r : R
b : CliffordAlgebra Q
rw :
  (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (r • b) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          b :
        CliffordAlgebra Q)
rw₁ :
  HSMul.hSMul (β := CliffordAlgebra Q) r
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          b :
        CliffordAlgebra Q) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          b :
        CliffordAlgebra Q)
⊢ (((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
          CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
        (a : CliffordAlgebra Q) → CliffordAlgebra Q)
      (HMul.hMul (α := CliffordAlgebra Q)
        ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q) b) =
    HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
      ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
      ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
              CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
            (a : CliffordAlgebra Q) → CliffordAlgebra Q)
          b :
        CliffordAlgebra Q)
have rw₂ : HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        b :
      CliffordAlgebra Q) =
  HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
    ((algebraMap R (CliffordAlgebra Q) : (a : R) → CliffordAlgebra Q) r : CliffordAlgebra Q)
    ((((contractLeft : (a : Module.Dual R M) → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) d :
            CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) :
          (a : CliffordAlgebra Q) → CliffordAlgebra Q)
        b :
      CliffordAlgebra Q)
Tactic: rw [← Algebra.smul_def, map_smul, Algebra.smul_def]