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

State before:
α : Type u
β : Type v
f : β → α → β
init : β
a : α
as : Array α
⊢ foldl f init (cons a as) 0 (size (cons a as)) = foldl f (f init a) as 0 (size as)
Tactic:
exact foldlM_cons (m:=Id) (λ b a => pure (f b a)) init a as
State after:
no goals