Theorem: Array.foldlM_eq_foldl (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type v
f : β → α → m β
init : β
x✝ a : Array α
x : α
IH :
  foldlM f init a 0 (size a) =
    foldl
      (fun z a => do
        let b ← z
        f b a)
      (pure init) a 0 (size a)
⊢ foldlM f init (push a x) 0 (size (push a x)) =
    foldl
      (fun z a => do
        let b ← z
        f b a)
      (pure init) (push a x) 0 (size (push a x))
Tactic:
rw [foldlM_push, foldl_push, IH]
State after:
no goals