exact this
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
this✝ :
  ∀ (i j : ℕ) (hj : i + j = n) (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n (?m.30970 i j hj macc) macc i
this : foldlM.aux n f 0 init = foldl.loop n (?m.30970 0 n ⋯ (pure init)) (pure init) 0
⊢ foldlM.aux n f 0 init =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (pure init) 0
no goals