no goals
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁ : List α
l₂ : List β
⊢ length (zipWith f l₁ l₂) = min (length l₁) (length l₂)
induction l₁ generalizing l₂ <;> cases l₂ <;>
  simp_all [add_one, min_succ_succ, Nat.zero_min, Nat.min_zero]