have hi : i < n := by calc
  _ ≤ Nat.succ i + j' := Nat.le_add_right _ _
  _ = n := hj
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    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
i : ℕ
hj : i.succ + 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
case succ
m : Type u → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
n : ℕ
β : Type u
init : β
f : Fin n → β → m β
j' : ℕ
ih :
  ∀ (i : ℕ),
    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
i : ℕ
hj : i.succ + j' = n
macc : m β
hi : i < n
⊢ (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