-- 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_1 d' : Module.Dual R M
c : R
d : Module.Dual R M
x : CliffordAlgebra Q
m : M
hx :
  (foldr' Q (contractLeftAux Q (c • d)) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x =
    HSMul.hSMul (β := CliffordAlgebra Q) c
      ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
ι_mul :
  HSMul.hSMul (β := R) c ((d : (a : M) → R) m : R) • x -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        (HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    c •
      (HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
ι_mul₁ :
  c • HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        (HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    c •
      (HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
ι_mul₂ :
  c • HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
      c •
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
    c •
      (HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
⊢ HSMul.hSMul (α := R) ((c • d : (a : M) → R) m : R) x -
      HMul.hMul (α := CliffordAlgebra Q) ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        (HSMul.hSMul (β := CliffordAlgebra Q) c
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)) =
    c •
      (HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
        HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
          ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
          ((foldr' Q (contractLeftAux Q d) ⋯ 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q))
have ι_mul₃ : c • HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
    c •
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q) =
  c • HSMul.hSMul (α := R) ((d : (a : M) → R) m : R) x -
    c •
      HMul.hMul (α := CliffordAlgebra Q) (β := CliffordAlgebra Q)
        ((ι Q : (a : M) → CliffordAlgebra Q) m : CliffordAlgebra Q)
        ((foldr' Q (contractLeftAux Q d) sorry 0 : (a : CliffordAlgebra Q) → CliffordAlgebra Q) x : CliffordAlgebra Q)
Tactic: rw [LinearMap.smul_apply, smul_assoc, mul_smul_comm, smul_sub]