simp [foldl, foldlM]
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ foldlM n init f =
    foldl n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init)
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0