induction i generalizing j b with
| zero =>
  simp only [Nat.zero_eq, Nat.zero_add] at H; cases H
  unfold foldlM.loop
  rw [dif_neg (Nat.lt_irrefl _), List.drop_length]
  rfl
| succ i IH =>
  have IH := IH (j+1) $ H.trans $ Nat.succ_add i j
  have : j < arr.size :=
    ((Nat.add_comm ..).trans H.symm) ▸ Nat.lt_add_of_pos_right i.zero_lt_succ
  unfold foldlM.loop
  simp only [dif_pos this, bind_congr IH]
  conv => rhs; rw [← List.get_drop_eq_drop arr.data j this]
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr = i + j
b : β
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
no goals