Theorem: Array.foldlM_push (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 : β
as : Array α
a : α
⊢ foldlM f init (push as a) 0 (size (push as a)) = do
    let b ← foldlM f init as 0 (size as)
    f b a
Tactic:
simp only [foldlM_eq_foldlM_data', as.push_data a]
State after:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type v
f : β → α → m β
init : β
as : Array α
a : α
⊢ List.foldlM f init (as.data ++ [a]) = do
    let b ← List.foldlM f init as.data
    f b a

State before:
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
β : Type v
f : β → α → m β
init : β
as : Array α
a : α
⊢ List.foldlM f init (as.data ++ [a]) = do
    let b ← List.foldlM f init as.data
    f b a
Tactic:
conv => lhs; rw [List.foldlM_append]; rhs; ext; simp only [List.foldlM, bind_pure]
State after:
no goals