α : Type u_1
arr arr' : Array α
⊢ (Array.append arr arr').data = arr.data ++ arr'.data
α : Type u_1
arr arr' : Array α
⊢ (arr ++ arr').data = arr.data ++ arr'.data
rw [← append_eq_append]
α : Type u_1
arr arr' : Array α
⊢ (foldl (fun r v => push r v) arr arr' 0 (size arr')).data = arr.data ++ arr'.data
α : Type u_1
arr arr' : Array α
⊢ (Array.append arr arr').data = arr.data ++ arr'.data
unfold Array.append
α : Type u_1
arr arr' : Array α
⊢ (List.foldl (fun r v => push r v) arr arr'.data).data = arr.data ++ arr'.data
α : Type u_1
arr arr' : Array α
⊢ (foldl (fun r v => push r v) arr arr' 0 (size arr')).data = arr.data ++ arr'.data
rw [foldl_eq_foldl_data]
no goals
α : Type u_1
arr arr' : Array α
⊢ (List.foldl (fun r v => push r v) arr arr'.data).data = arr.data ++ arr'.data
induction arr'.data generalizing arr <;> simp [*]