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 _ _
case cons
α : Type u
β : Type v
γ : Type w
f : α → β → γ
a : α
x : Array α
IH : ∀ (y : Array β) (z : Array γ), (zipWithAux f x y 0 z).data = List.zipWithTR.go f x.data y.data z
y : Array β
z : Array γ
⊢ (zipWithAux f (cons a x) y 0 z).data = List.zipWithTR.go f (cons a x).data y.data z
no goals