unfold foldlM.aux
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      foldlM.aux n f i acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
this :
  (do
      let acc ←
        do
          let acc ← macc
          f ⟨i, hi⟩ acc
      foldlM.aux n f (i + 1) acc) =
    foldl.loop n
      (fun macc i => do
        let acc ← macc
        f i acc)
      (do
        let acc ← macc
        f ⟨i, hi⟩ acc)
      (i + 1)
⊢ (do
      let acc ← macc
      if h' : i < n then do
          let acc ← f ⟨i, h'⟩ acc
          foldlM.aux n f (i + 1) acc
        else pure acc) =
    if h : i < n then
      foldl.loop n
        (fun macc i => do
          let acc ← macc
          f i acc)
        (do
          let acc ← macc
          f ⟨i, h⟩ acc)
        (i + 1)
    else macc