induction x using cons_induction generalizing y z with
| empty =>
  rw [zipWithAux_nil_first]; exact z.toList_eq.symm
| cons a x IH =>
  cases y using cons_cases_on with
  | empty =>
    rw [zipWithAux_nil_second]; exact z.toList_eq.symm
  | cons b y =>
    rw [zipWithAux_cons_cons_zero]; exact IH _ _
α : Type u
β : Type v
γ : Type w
f : α → β → γ
x : Array α
y : Array β
z : Array γ
⊢ (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
no goals