Theorem: Array.foldl_cons (LeanSAT/Upstream/ToStd.lean)

State before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
a : α
as : List α
⊢ foldl f init { data := a :: as } 0 = foldl f (f init a) { data := as } 0
Tactic:
simp only [foldl_eq_foldl_data]
State after:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
a : α
as : List α
⊢ List.foldl f init (a :: as) = List.foldl f (f init a) as

State before:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
a : α
as : List α
⊢ List.foldl f init (a :: as) = List.foldl f (f init a) as
Tactic:
rfl
State after:
no goals