. apply zipWithNSizeGo
  . apply Nat.succ_le_of_lt
    assumption
  . rw [Array.size_push]
    simp
    assumption
case inl
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : i < size as
⊢ size
      (let a := as[i];
      let b := bs[i];
      go as bs f p (push arr (f a b)) (i + 1)) =
    size as

case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as
case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as