-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
x : ExteriorAlgebra R M
rw :
  Eq.{u_3 + 1} (α := N)
    ((((((foldl 0
                        (LinearMap.mk₂ R
                          (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                            (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                          ⋯ ⋯ ⋯ ⋯)
                        ⋯ :
                      (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → CliffordAlgebra 0 →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    ((((LinearMap.mk₂ R
                                (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                                  (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                                ⋯ ⋯ ⋯ ⋯ :
                              (a : M) → ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                            m :
                          ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                        (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                      f) :
                  CliffordAlgebra.{u_1, u_2} (R := R) (M := M) 0 →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : CliffordAlgebra 0) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              x 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
    (((((foldl 0
                      (LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        ⋯ ⋯ ⋯ ⋯)
                      ⋯ :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  fun (i : ℕ) ↦ (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              x 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
⊢ Eq.{u_3 + 1} (α := N)
    ((((((foldl 0
                        (LinearMap.mk₂ R
                          (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                            (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                          ⋯ ⋯ ⋯ ⋯)
                        ⋯ :
                      (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                    f :
                  ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              (HMul.hMul (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) x)
              0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)
    (((((foldl 0
                      (LinearMap.mk₂ R
                        (fun (m : M) (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) (i : ℕ) ↦
                          (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m)
                        ⋯ ⋯ ⋯ ⋯)
                      ⋯ :
                    (a : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N) → ExteriorAlgebra R M →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
                  fun (i : ℕ) ↦ (AlternatingMap.curryLeft (f (i + 1)) : (a : M) → M [⋀^Fin i]→ₗ[R] N) m :
                (a : ExteriorAlgebra R M) → (i : ℕ) → M [⋀^Fin i]→ₗ[R] N)
              x 0 :
            M [⋀^Fin 0]→ₗ[R] N) :
          (a : Fin 0 → M) → N)
        0 :
      N)

Tactic:
rw [foldl_mul, foldl_ι]

Premises used: CliffordAlgebra.foldl_mul, CliffordAlgebra.foldl_ι