rw [Array.foldlM.loop]
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - start) start b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if hlt : start < stop then
      match stop - start with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[start]
        foldlM.loop f as stop ⋯ i' (start + 1) __do_lift
    else pure b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b