no goals
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM f init arr 0 (size arr) = List.foldlM f init arr.data
simp [foldlM, foldlM_eq_foldlM_data.aux]