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

State before:
α : Type u
β : Type v
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
a : α
as : Array α
l : List α
⊢ foldlM f init (cons a { data := l }) 0 (size (cons a { data := l })) = do
    let b ← f init a
    foldlM f b { data := l } 0 (size { data := l })
Tactic:
simp only [foldlM_eq_foldlM_data', cons]
State after:
α : Type u
β : Type v
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
a : α
as : Array α
l : List α
⊢ List.foldlM f init (a :: l) = do
    let b ← f init a
    List.foldlM f b l

State before:
α : Type u
β : Type v
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
a : α
as : Array α
l : List α
⊢ List.foldlM f init (a :: l) = do
    let b ← f init a
    List.foldlM f b l
Tactic:
rfl
State after:
no goals