Theorem: Array.foldlM_eq_foldlM_data' (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM f init arr 0 (size arr) = List.foldlM f init arr.data
Tactic:
simp only [foldlM, Nat.le_refl, dif_pos, Nat.sub_zero]
State after:
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (size arr) 0 init = List.foldlM f init arr.data

State before:
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (size arr) 0 init = List.foldlM f init arr.data
Tactic:
exact foldlM_eq_foldlM_data'.aux f arr arr.size 0 rfl init
State after:
no goals