α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (List.foldl (fun bs a => push bs (f a)) #[] arr.data).data = List.map f arr.data
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (map f arr).data = List.map f arr.data
apply congrArg data (foldl_eq_foldl_data (fun bs a => push bs (f a)) #[] arr) |>.trans
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
H : ∀ (l : List α) (arr : Array β), List.foldl (fun bs a => push bs (f a)) arr l = { data := arr.data ++ List.map f l }
⊢ (List.foldl (fun bs a => push bs (f a)) #[] arr.data).data = List.map f arr.data
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
⊢ (List.foldl (fun bs a => push bs (f a)) #[] arr.data).data = List.map f arr.data
have H (l arr) : List.foldl (fun bs a => push bs (f a)) arr l = ⟨arr.data ++ l.map f⟩ := by
  induction l generalizing arr <;> simp [*]
no goals
α : Type u_1
β : Type u_2
f : α → β
arr : Array α
H : ∀ (l : List α) (arr : Array β), List.foldl (fun bs a => push bs (f a)) arr l = { data := arr.data ++ List.map f l }
⊢ (List.foldl (fun bs a => push bs (f a)) #[] arr.data).data = List.map f arr.data
simp [H]
no goals
α : Type u_1
β : Type u_2
f : α → β
arr✝ : Array α
l : List α
arr : Array β
⊢ List.foldl (fun bs a => push bs (f a)) arr l = { data := arr.data ++ List.map f l }
induction l generalizing arr <;> simp [*]