feat: review of List.erase / List.find lemmas

src/Init/Data/List/Erase.lean

@@ -109,6 +109,10 @@ protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP
 theorem length_eraseP_le (l : List α) : (l.eraseP p).length ≤ l.length :=
   l.eraseP_sublist.length_le
 
+theorem le_length_eraseP (l : List α) : l.length - 1 ≤ (l.eraseP p).length := by
+  rw [length_eraseP]
+  split <;> simp
+
 theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (eraseP_subset _ ·)
 
 @[simp] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by
@@ -332,6 +336,10 @@ theorem IsPrefix.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁
 theorem length_erase_le (a : α) (l : List α) : (l.erase a).length ≤ l.length :=
   (erase_sublist a l).length_le
 
+theorem le_length_erase [LawfulBEq α] (a : α) (l : List α) : l.length - 1 ≤ (l.erase a).length := by
+  rw [length_erase]
+  split <;> simp
+
 theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset _ _ h
 
 @[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
@@ -452,13 +460,22 @@ end erase
 
 /-! ### eraseIdx -/
 
-theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i) = length l - 1
-  | [], _, _ => rfl
-  | _::_, 0, _ => by simp [eraseIdx]
-  | x::xs, i+1, h => by
-    have : i < length xs := Nat.lt_of_succ_lt_succ h
-    simp [eraseIdx, ← Nat.add_one]
-    rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)]
+theorem length_eraseIdx (l : List α) (i : Nat) :
+    (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length := by
+  induction l generalizing i with
+  | nil => simp
+  | cons x l ih =>
+    cases i with
+    | zero => simp
+    | succ i =>
+      simp only [eraseIdx, length_cons, ih, add_one_lt_add_one_iff, Nat.add_one_sub_one]
+      split
+      · cases l <;> simp_all
+      · rfl
+
+theorem length_eraseIdx_of_lt {l : List α} {i} (h : i < length l) :
+    (l.eraseIdx i).length = length l - 1 := by
+  simp [length_eraseIdx, h]
 
 @[simp] theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l := by cases l <;> rfl
 
@@ -468,6 +485,8 @@ theorem eraseIdx_eq_take_drop_succ :
   | a::l, 0 => by simp
   | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]
 
+-- See `Init.Data.List.Nat.Erase` for `getElem?_eraseIdx` and `getElem_eraseIdx`.
+
 @[simp] theorem eraseIdx_eq_nil {l : List α} {i : Nat} : eraseIdx l i = [] ↔ l = [] ∨ (length l = 1 ∧ i = 0) := by
   match l, i with
   | [], _
@@ -499,6 +518,13 @@ theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ len
 theorem eraseIdx_of_length_le {l : List α} {k : Nat} (h : length l ≤ k) : eraseIdx l k = l := by
   rw [eraseIdx_eq_self.2 h]
 
+theorem length_eraseIdx_le (l : List α) (i : Nat) : length (l.eraseIdx i) ≤ length l :=
+  (eraseIdx_sublist l i).length_le
+
+theorem le_length_eraseIdx (l : List α) (i : Nat) : length l - 1 ≤ length (l.eraseIdx i) := by
+  rw [length_eraseIdx]
+  split <;> simp
+
 theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
     eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by
   induction l generalizing k with
@@ -520,7 +546,7 @@ theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤
 theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
     (replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a := by
   split <;> rename_i h
-  · rw [eq_replicate_iff, length_eraseIdx (by simpa using h)]
+  · rw [eq_replicate_iff, length_eraseIdx_of_lt (by simpa using h)]
     simp only [length_replicate, true_and]
     intro b m
     replace m := mem_of_mem_eraseIdx m

src/Init/Data/List/Find.lean

@@ -620,6 +620,18 @@ theorem IsPrefix.findIdx_eq_of_findIdx_lt_length {l₁ l₂ : List α} {p : α
   · rfl
   · simp_all
 
+theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p x → q x) : l.findIdx q ≤ l.findIdx p := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx_cons, cond_eq_if]
+    split
+    · simp
+    · split
+      · simp_all
+      · simp only [Nat.add_le_add_iff_right]
+        exact ih fun _ m w => h _ (mem_cons_of_mem x m) w
+
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl
@@ -803,7 +815,7 @@ theorem findIdx?_join {l : List (List α)} {p : α → Bool} :
     simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, zero_lt_succ, true_and]
     split <;> simp_all
 
-theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
+theorem findIdx?_eq_findSome?_enum {xs : List α} {p : α → Bool} :
     xs.findIdx? p = xs.enum.findSome? fun ⟨i, a⟩ => if p a then some i else none := by
   induction xs with
   | nil => simp
@@ -814,6 +826,30 @@ theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
     · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
       simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map]
 
+theorem findIdx?_eq_fst_find?_enum {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.enum.find? fun ⟨_, x⟩ => p x).map (·.1) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, enum_cons]
+    split
+    · simp_all
+    · simp only [Option.map_map, enumFrom_eq_map_enum, Bool.false_eq_true, not_false_eq_true,
+        find?_cons_of_neg, find?_map, *]
+      congr
+
+-- See also `findIdx_le_findIdx`.
+theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) :
+    xs.findIdx? q = none → xs.findIdx? p = none := by
+  simp only [findIdx?_eq_none_iff]
+  intro h x m
+  cases z : p x
+  · rfl
+  · exfalso
+    specialize w x m z
+    specialize h x m
+    simp_all
+
 theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     (l₁.findIdx? p).isSome → (l₂.findIdx? p).isSome := by
   simp only [List.findIdx?_isSome, any_eq_true]

src/Init/Data/List/Lemmas.lean

@@ -266,9 +266,15 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l
 theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
   simp only [← get?_eq_getElem?, get?_eq_some, get_eq_getElem]
 
+theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.length, l[n] = a := by
+  rw [eq_comm, getElem?_eq_some_iff]
+
 @[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
   simp only [← get?_eq_getElem?, get?_eq_none]
 
+@[simp] theorem none_eq_getElem?_iff {l : List α} {n : Nat} : none = l[n]? ↔ length l ≤ n := by
+  simp [eq_comm (a := none)]
+
 theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
 theorem getElem?_eq (l : List α) (i : Nat) :

src/Init/Data/List/Nat.lean

@@ -10,3 +10,5 @@ import Init.Data.List.Nat.Range
 import Init.Data.List.Nat.Sublist
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Count
+import Init.Data.List.Nat.Erase
+import Init.Data.List.Nat.Find

src/Init/Data/List/Nat/Basic.lean

@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Count
+import Init.Data.List.Find
 import Init.Data.List.MinMax
 import Init.Data.Nat.Lemmas
 

src/Init/Data/List/Nat/Erase.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2024 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Erase
+
+namespace List
+
+theorem getElem?_eraseIdx (l : List α) (i : Nat) (j : Nat) :
+    (l.eraseIdx i)[j]? = if h : j < i then l[j]? else l[j + 1]? := by
+  rw [eraseIdx_eq_take_drop_succ, getElem?_append]
+  split <;> rename_i h
+  · rw [getElem?_take]
+    split
+    · rfl
+    · simp_all
+      omega
+  · rw [getElem?_drop]
+    split <;> rename_i h'
+    · simp only [length_take, Nat.min_def, Nat.not_lt] at h
+      split at h
+      · omega
+      · simp_all [getElem?_eq_none]
+        omega
+    · simp only [length_take]
+      simp only [length_take, Nat.min_def, Nat.not_lt] at h
+      split at h
+      · congr 1
+        omega
+      · rw [getElem?_eq_none, getElem?_eq_none] <;> omega
+
+theorem getElem?_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < i) :
+    (l.eraseIdx i)[j]? = l[j]? := by
+  rw [getElem?_eraseIdx]
+  simp [h]
+
+theorem getElem?_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : i ≤ j) :
+    (l.eraseIdx i)[j]? = l[j + 1]? := by
+  rw [getElem?_eraseIdx]
+  simp only [dite_eq_ite, ite_eq_right_iff]
+  intro h'
+  omega
+
+theorem getElem_eraseIdx (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) :
+    (l.eraseIdx i)[j] = if h' : j < i then
+        l[j]'(by have := length_eraseIdx_le l i; omega)
+      else
+        l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem, getElem?_eraseIdx]
+  split <;> simp
+
+theorem getElem_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : j < i) :
+    (l.eraseIdx i)[j] = l[j]'(by have := length_eraseIdx_le l i; omega) := by
+  rw [getElem_eraseIdx]
+  simp only [dite_eq_left_iff, Nat.not_lt]
+  intro h'
+  omega
+
+theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : i ≤ j) :
+    (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
+  rw [getElem_eraseIdx, dif_neg]
+  omega

src/Init/Data/List/Nat/Find.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Nat.Range
+import Init.Data.List.Find
+
+namespace List
+
+theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
+    (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j := by
+  simp only [findIdx?_eq_findSome?_enum] at h
+  rw [findSome?_eq_some_iff] at h
+  simp only [Option.ite_none_right_eq_some, Option.some.injEq, ite_eq_right_iff, reduceCtorEq,
+    imp_false, Bool.not_eq_true, Prod.forall, exists_and_right, Prod.exists] at h
+  obtain ⟨h, h₁, b, ⟨es, h₂⟩, ⟨hb, rfl⟩, h₃⟩ := h
+  rw [enum_eq_enumFrom, enumFrom_eq_append_iff] at h₂
+  obtain ⟨l₁', l₂', rfl, rfl, h₂⟩ := h₂
+  rw [eq_comm, enumFrom_eq_cons_iff] at h₂
+  obtain ⟨a, as, rfl, h₂, rfl⟩ := h₂
+  simp only [Nat.zero_add, Prod.mk.injEq] at h₂
+  obtain ⟨rfl, rfl⟩ := h₂
+  simp only [findIdx?_append]
+  match h : findIdx? q l₁' with
+  | some j =>
+    refine ⟨j, ?_, by simp⟩
+    rw [findIdx?_eq_some_iff_findIdx_eq] at h
+    omega
+  | none =>
+    refine ⟨l₁'.length, by simp, by simp_all⟩

src/Init/Data/List/Nat/Range.lean

@@ -358,17 +358,6 @@ theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
     map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by
   induction l generalizing n <;> simp_all
 
-@[simp]
-theorem enumFrom_map_fst (n) :
-    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
-  | [] => rfl
-  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
-
-@[simp]
-theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
-  | _, [] => rfl
-  | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
-
 theorem snd_mem_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.2 ∈ l :=
   enumFrom_map_snd n l ▸ mem_map_of_mem _ h
 
@@ -391,10 +380,6 @@ theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enum
       x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) :=
   ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_eq_of_mem_enumFrom h⟩
 
-theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
-    enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
-  rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]
-
 theorem enumFrom_map (n : Nat) (l : List α) (f : α → β) :
     enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f) := by
   induction l with
@@ -411,22 +396,39 @@ theorem enumFrom_append (xs ys : List α) (n : Nat) :
     rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, Nat.add_right_comm,
       Nat.add_assoc]
 
-theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
-  zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
+theorem enumFrom_eq_cons_iff {l : List α} {n : Nat} :
+    l.enumFrom n = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (n, a) ∧ l' = enumFrom (n + 1) as := by
+  rw [enumFrom_eq_zip_range', zip_eq_cons_iff]
+  constructor
+  · rintro ⟨l₁, l₂, h, rfl, rfl⟩
+    rw [range'_eq_cons_iff] at h
+    obtain ⟨rfl, -, rfl⟩ := h
+    exact ⟨x.2, l₂, by simp [enumFrom_eq_zip_range']⟩
+  · rintro ⟨a, as, rfl, rfl, rfl⟩
+    refine ⟨range' (n+1) as.length, as, ?_⟩
+    simp [enumFrom_eq_zip_range', range'_succ]
 
-@[simp]
-theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
-    (l.enumFrom n).unzip = (range' n l.length, l) := by
-  simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
+theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
+    l.enumFrom n = l₁ ++ l₂ ↔
+      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enumFrom n ∧ l₂ = l₂'.enumFrom (n + l₁'.length) := by
+  rw [enumFrom_eq_zip_range', zip_eq_append_iff]
+  constructor
+  · rintro ⟨w, x, y, z, h, h', rfl, rfl, rfl⟩
+    rw [range'_eq_append_iff] at h'
+    obtain ⟨k, -, rfl, rfl⟩ := h'
+    simp only [length_range'] at h
+    obtain rfl := h
+    refine ⟨y, z, rfl, ?_⟩
+    simp only [enumFrom_eq_zip_range', length_append, true_and]
+    congr
+    omega
+  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
+    simp only [enumFrom_eq_zip_range']
+    refine ⟨range' n l₁'.length, range' (n + l₁'.length) l₂'.length, l₁', l₂', ?_⟩
+    simp [Nat.add_comm]
 
 /-! ### enum -/
 
-theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
-
-theorem enum_cons' (x : α) (xs : List α) :
-    enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
-  enumFrom_cons' _ _ _
-
 @[simp]
 theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
 

src/Init/Data/List/Range.lean

@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Pairwise
+import Init.Data.List.Zip
 
 /-!
 # Lemmas about `List.range` and `List.enum`
@@ -241,4 +242,47 @@ theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) :
     map (Prod.map (· + n) id) (enum l) = enumFrom n l :=
   map_fst_add_enumFrom_eq_enumFrom l _ _
 
+theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
+    enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
+  rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]
+
+@[simp]
+theorem enumFrom_map_fst (n) :
+    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
+  | [] => rfl
+  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
+
+@[simp]
+theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
+  | _, [] => rfl
+  | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
+
+theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
+  zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
+
+@[simp]
+theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
+    (l.enumFrom n).unzip = (range' n l.length, l) := by
+  simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
+
+/-! ### enum -/
+
+theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
+
+theorem enum_cons' (x : α) (xs : List α) :
+    enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
+  enumFrom_cons' _ _ _
+
+theorem enum_eq_enumFrom {l : List α} : l.enum = l.enumFrom 0 := rfl
+
+theorem enumFrom_eq_map_enum (l : List α) (n : Nat) :
+    enumFrom n l = (enum l).map (Prod.map (· + n) id) := by
+  induction l generalizing n with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [enumFrom_cons, ih, enum_cons, map_cons, Prod.map_apply, Nat.zero_add, id_eq, map_map,
+      cons.injEq, map_inj_left, Function.comp_apply, Prod.forall, Prod.mk.injEq, and_true, true_and]
+    intro a b _
+    exact (succ_add a n).symm
+
 end List

src/Init/Data/List/Zip.lean

@@ -16,87 +16,6 @@ open Nat
 
 /-! ## Zippers -/
 
-/-! ### zip -/
-
-theorem zip_map (f : α → γ) (g : β → δ) :
-    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
-  | [], l₂ => rfl
-  | l₁, [] => by simp only [map, zip_nil_right]
-  | a :: l₁, b :: l₂ => by
-    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
-
-theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
-    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
-
-theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
-    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
-
-@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
-    (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
-  cases l₁ <;> cases l₂ <;> simp
-
-theorem zip_append :
-    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
-      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
-  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
-  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
-  | a :: l₁, r₁, b :: l₂, r₂, h => by
-    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
-
-theorem zip_map' (f : α → β) (g : α → γ) :
-    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
-  | [] => rfl
-  | a :: l => by simp only [map, zip_cons_cons, zip_map']
-
-theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
-  | _ :: l₁, _ :: l₂, h => by
-    cases h
-    case head => simp
-    case tail h =>
-    · have := of_mem_zip h
-      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
-
-@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
-
-theorem map_fst_zip :
-    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
-  | [], bs, _ => rfl
-  | _ :: as, _ :: bs, h => by
-    simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.fst (zip as bs) = _ :: as
-    rw [map_fst_zip as bs h]
-  | a :: as, [], h => by simp at h
-
-theorem map_snd_zip :
-    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
-  | _, [], _ => by
-    rw [zip_nil_right]
-    rfl
-  | [], b :: bs, h => by simp at h
-  | a :: as, b :: bs, h => by
-    simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.snd (zip as bs) = _ :: bs
-    rw [map_snd_zip as bs h]
-
-theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
-    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
-  rw [← zip_map']
-  congr
-  simp
-
-theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
-    (l.map fun x => (f x, x)) = (l.map f).zip l := by
-  rw [← zip_map']
-  congr
-  simp
-
-/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
-@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
-    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
-  induction n with
-  | zero => rfl
-  | succ n ih => simp [replicate_succ, ih]
-
 /-! ### zipWith -/
 
 theorem zipWith_comm (f : α → β → γ) :
@@ -253,6 +172,65 @@ theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
       simp only [length_cons, Nat.succ.injEq] at h
       simp [ih _ h]
 
+theorem zipWith_eq_cons_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
+    zipWith f l₁ l₂ = g :: l ↔
+      ∃ a l₁' b l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂' := by
+  match l₁, l₂ with
+  | [], [] => simp
+  | [], b :: l₂ => simp
+  | a :: l₁, [] => simp
+  | a' :: l₁, b' :: l₂ =>
+    simp only [zip_cons_cons, cons.injEq, Prod.mk.injEq]
+    constructor
+    · rintro ⟨⟨rfl, rfl⟩, rfl⟩
+      refine ⟨a', l₁, b', l₂, by simp⟩
+    · rintro ⟨a, l₁, b, l₂, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl, rfl⟩
+      simp
+
+theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
+    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
+      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z := by
+  induction l₁ generalizing l₂ l₁' with
+  | nil =>
+    simp
+    constructor
+    · rintro ⟨rfl, rfl⟩
+      exact ⟨[], [], [], by simp⟩
+    · rintro ⟨_, _, _, -, ⟨rfl, rfl⟩, _, rfl, rfl, rfl⟩
+      simp
+  | cons x₁ l₁ ih₁ =>
+    cases l₂ with
+    | nil =>
+      constructor
+      · simp only [zipWith_nil_right, nil_eq, append_eq_nil, exists_and_left, and_imp]
+        rintro rfl  rfl
+        exact ⟨[], x₁ :: l₁, [], by simp⟩
+      · rintro ⟨w, x, y, z, h₁, _, h₃, rfl, rfl⟩
+        simp only [nil_eq, append_eq_nil] at h₃
+        obtain ⟨rfl, rfl⟩ := h₃
+        simp
+    | cons x₂ l₂ =>
+      simp only [zipWith_cons_cons]
+      rw [cons_eq_append_iff]
+      constructor
+      · rintro (⟨rfl, rfl⟩ | ⟨l₁'', rfl, h⟩)
+        · exact ⟨[], x₁ :: l₁, [], x₂ :: l₂, by simp⟩
+        · rw [ih₁] at h
+          obtain ⟨w, x, y, z, h, rfl, rfl, h', rfl⟩ := h
+          refine ⟨x₁ :: w, x, x₂ :: y, z, by simp [h, h']⟩
+      · rintro ⟨w, x, y, z, h₁, h₂, h₃, rfl, rfl⟩
+        rw [cons_eq_append_iff] at h₂
+        rw [cons_eq_append_iff] at h₃
+        obtain (⟨rfl, rfl⟩ | ⟨w', rfl, rfl⟩) := h₂
+        · simp only [zipWith_nil_left, true_and, nil_eq, reduceCtorEq, false_and, exists_const,
+          or_false]
+          obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃
+          · simp
+          · simp_all
+        · obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃
+          · simp_all
+          · simp_all [zipWith_append, Nat.succ_inj']
+
 /-- See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
 @[simp] theorem zipWith_replicate' {a : α} {b : β} {n : Nat} :
     zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
@@ -260,6 +238,113 @@ theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
   | zero => rfl
   | succ n ih => simp [replicate_succ, ih]
 
+/-! ### zip -/
+
+theorem zip_eq_zipWith : ∀ (l₁ : List α) (l₂ : List β), zip l₁ l₂ = zipWith Prod.mk l₁ l₂
+  | [], _ => rfl
+  | _, [] => rfl
+  | a :: l₁, b :: l₂ => by simp [zip_cons_cons, zip_eq_zipWith l₁ l₂]
+
+theorem zip_map (f : α → γ) (g : β → δ) :
+    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
+  | [], l₂ => rfl
+  | l₁, [] => by simp only [map, zip_nil_right]
+  | a :: l₁, b :: l₂ => by
+    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
+
+theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
+    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
+
+theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
+    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
+
+@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
+    (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
+  cases l₁ <;> cases l₂ <;> simp
+
+theorem zip_append :
+    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
+      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
+  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
+  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
+  | a :: l₁, r₁, b :: l₂, r₂, h => by
+    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
+
+theorem zip_map' (f : α → β) (g : α → γ) :
+    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
+  | [] => rfl
+  | a :: l => by simp only [map, zip_cons_cons, zip_map']
+
+theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
+  | _ :: l₁, _ :: l₂, h => by
+    cases h
+    case head => simp
+    case tail h =>
+    · have := of_mem_zip h
+      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
+
+@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
+
+theorem map_fst_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
+  | [], bs, _ => rfl
+  | _ :: as, _ :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.fst (zip as bs) = _ :: as
+    rw [map_fst_zip as bs h]
+  | a :: as, [], h => by simp at h
+
+theorem map_snd_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
+  | _, [], _ => by
+    rw [zip_nil_right]
+    rfl
+  | [], b :: bs, h => by simp at h
+  | a :: as, b :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.snd (zip as bs) = _ :: bs
+    rw [map_snd_zip as bs h]
+
+theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
+    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
+  rw [← zip_map']
+  congr
+  simp
+
+theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
+    (l.map fun x => (f x, x)) = (l.map f).zip l := by
+  rw [← zip_map']
+  congr
+  simp
+
+@[simp] theorem zip_eq_nil_iff {l₁ : List α} {l₂ : List β} :
+    zip l₁ l₂ = [] ↔ l₁ = [] ∨ l₂ = [] := by
+  simp [zip_eq_zipWith]
+
+theorem zip_eq_cons_iff {l₁ : List α} {l₂ : List β} :
+    zip l₁ l₂ = (a, b) :: l ↔
+      ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zip l₁' l₂' := by
+  simp only [zip_eq_zipWith, zipWith_eq_cons_iff]
+  constructor
+  · rintro ⟨a, l₁, b, l₂, rfl, rfl, h, rfl, rfl⟩
+    simp only [Prod.mk.injEq] at h
+    obtain ⟨rfl, rfl⟩ := h
+    simp
+  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
+    refine ⟨a, l₁', b, l₂', by simp⟩
+
+theorem zip_eq_append_iff {l₁ : List α} {l₂ : List β} :
+    zip l₁ l₂ = l₁' ++ l₂' ↔
+      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z := by
+  simp [zip_eq_zipWith, zipWith_eq_append_iff]
+
+/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
+@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
+    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [replicate_succ, ih]
+
 /-! ### zipWithAll -/
 
 theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :

src/Init/Data/Nat/Lemmas.lean

@@ -230,6 +230,17 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 @[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
   rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]
 
+@[simp] theorem min_add_left {a b : Nat} : min a (b + a) = a := by
+  rw [Nat.min_def]
+  simp
+@[simp] theorem min_add_right {a b : Nat} : min a (a + b) = a := by
+  rw [Nat.min_def]
+  simp
+@[simp] theorem add_left_min {a b : Nat} : min (b + a) a = a := by
+  rw [Nat.min_comm, min_add_left]
+@[simp] theorem add_right_min {a b : Nat} : min (a + b) a = a := by
+  rw [Nat.min_comm, min_add_right]
+
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
   | _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]
@@ -284,6 +295,17 @@ protected theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b
   | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
 instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
+@[simp] theorem max_add_left {a b : Nat} : max a (b + a) = b + a := by
+  rw [Nat.max_def]
+  simp
+@[simp] theorem max_add_right {a b : Nat} : max a (a + b) = a + b := by
+  rw [Nat.max_def]
+  simp
+@[simp] theorem add_left_max {a b : Nat} : max (b + a) a = b + a := by
+  rw [Nat.max_comm, max_add_left]
+@[simp] theorem add_right_max {a b : Nat} : max (a + b) a = a + b := by
+  rw [Nat.max_comm, max_add_right]
+
 protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
   match Nat.le_total a b with
   | .inl hl => rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]