feat(data/list/zip): nth_zip_with univ polymorphic, `zip_with_eq_ni…

…l_iff` (#6974)

Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>

src/data/list/zip.lean

@@ -26,6 +26,10 @@ namespace list
 @[simp] theorem zip_with_nil_right (f : α → β → γ) (l)  : zip_with f l [] = [] :=
 by cases l; refl
 
+@[simp] lemma zip_with_eq_nil_iff {f : α → β → γ} {l l'} :
+  zip_with f l l' = [] ↔ l = [] ∨ l' = [] :=
+by { cases l; cases l'; simp }
+
 @[simp] theorem zip_nil_left (l : list α) : zip ([] : list β) l = [] := rfl
 
 @[simp] theorem zip_nil_right (l : list α) : zip l ([] : list β) = [] :=
@@ -199,15 +203,14 @@ by rw [← zip_unzip.{u u} (revzip l).reverse, unzip_eq_map]; simp; simp [revzip
 theorem revzip_swap (l : list α) : (revzip l).map prod.swap = revzip l.reverse :=
 by simp [revzip]
 
-lemma nth_zip_with {α β γ} (f : α → β → γ) (l₁ : list α) (l₂ : list β) (i : ℕ) :
-  (zip_with f l₁ l₂).nth i = f <$> l₁.nth i <*> l₂.nth i :=
+lemma nth_zip_with (f : α → β → γ) (l₁ : list α) (l₂ : list β) (i : ℕ) :
+  (zip_with f l₁ l₂).nth i = ((l₁.nth i).map f).bind (λ g, (l₂.nth i).map g) :=
 begin
   induction l₁ generalizing l₂ i,
   { simp [zip_with, (<*>)] },
   { cases l₂; simp only [zip_with, has_seq.seq, functor.map, nth, option.map_none'],
     { cases ((l₁_hd :: l₁_tl).nth i); refl },
-    { cases i; simp only [option.map_some', nth, option.some_bind', *],
-      refl } },
+    { cases i; simp only [option.map_some', nth, option.some_bind', *] } }
 end
 
 lemma nth_zip_with_eq_some {α β γ} (f : α → β → γ) (l₁ : list α) (l₂ : list β) (z : γ) (i : ℕ) :