no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
⊢ foldrM f init arr (size arr) = List.foldrM f init arr.data
rw [foldrM_eq_reverse_foldlM_data, List.foldlM_reverse]