induction x, y using cons_induction_on₂ generalizing i with
| empty => cases h
| cons a x b y IH =>
  simp only [zipWith_cons]
  cases i with
  | zero => simp only [get_cons_zero]
  | succ i =>
    simp only [Nat.succ_eq_add_one, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
    exact IH
α : Type u
β : Type v
γ : Type w
δ : Type uu
n : Nat
x : SizedArray α n
y : SizedArray β n
f : α → β → γ
i : Nat
h : i < n
⊢ (zipWith x y f)[i] = f x[i] y[i]
no goals