induction j generalizing i with
| zero =>
  intro macc
  simp at hj; cases hj
  unfold foldl.loop; unfold foldlM.aux
  simp
| succ j' ih =>
  intro macc
  rw [Nat.add_succ, ← Nat.succ_add] at hj
  have hi : i < n := by calc
    _ ≤ Nat.succ i + j' := Nat.le_add_right _ _
    _ = n := hj
  have := ih (i+1) hj (macc >>= fun acc => f ⟨i,hi⟩ acc)
  clear ih
  unfold foldl.loop; unfold foldlM.aux
  simp_all
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
i j : ℕ
hj : i + j = n
⊢ ∀ (macc : m β),
    (do
        let acc ← macc
        foldlM.aux n f i acc) =
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        macc i
no goals