rw [Array.foldlM_eq_foldlM_data']
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ Array.foldlM f init x.val 0 (Array.size x.val) = foldlMIdx (fun x => f) init x
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x