-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating (goal)
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
⊢ 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)
have 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)
                        sorry sorry sorry sorry)
                      sorry :
                    (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)
                              sorry sorry sorry sorry :
                            (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)
                      sorry sorry sorry sorry)
                    sorry :
                  (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_ι]