mem_zipIdx'

src/Init/Data/Array/Basic.lean

@@ -605,8 +605,10 @@ def mapIdx {α : Type u} {β : Type v} (f : Nat → α → β) (as : Array α) :
   Id.run <| as.mapIdxM f
 
 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
-def zipWithIndex (arr : Array α) : Array (α × Nat) :=
-  arr.mapIdx fun i a => (a, i)
+def zipIdx (arr : Array α) (start := 0) : Array (α × Nat) :=
+  arr.mapIdx fun i a => (a, i + start)
+
+@[deprecated zipIdx (since := "2025-01-21")] abbrev zipWithIndex := @zipIdx
 
 @[inline]
 def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α :=

src/Init/Data/Array/MapIdx.lean

@@ -48,9 +48,11 @@ theorem mapFinIdx_spec (as : Array α) (f : (i : Nat) → α → (h : i < as.siz
     (a.mapFinIdx f).size = a.size :=
   (mapFinIdx_spec (p := fun _ _ _ => True) (hs := fun _ _ => trivial)).1
 
-@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+@[simp] theorem size_zipIdx (as : Array α) (k : Nat) : (as.zipIdx k).size = as.size :=
   Array.size_mapFinIdx _ _
 
+@[deprecated size_zipIdx (since := "2025-01-21")] abbrev size_zipWithIndex := @size_zipIdx
+
 @[simp] theorem getElem_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat)
     (h : i < (mapFinIdx a f).size) :
     (a.mapFinIdx f)[i] = f i (a[i]'(by simp_all))  (by simp_all) :=
@@ -115,34 +117,58 @@ end List
 
 namespace Array
 
-/-! ### zipWithIndex -/
+/-! ### zipIdx -/
 
-@[simp] theorem getElem_zipWithIndex (a : Array α) (i : Nat) (h : i < a.zipWithIndex.size) :
-    (a.zipWithIndex)[i] = (a[i]'(by simp_all), i) := by
-  simp [zipWithIndex]
+@[simp] theorem getElem_zipIdx (a : Array α) (k : Nat) (i : Nat) (h : i < (a.zipIdx k).size) :
+    (a.zipIdx k)[i] = (a[i]'(by simp_all), i + k) := by
+  simp [zipIdx]
 
-@[simp] theorem zipWithIndex_toArray {l : List α} :
-    l.toArray.zipWithIndex = (l.enum.map fun (i, x) => (x, i)).toArray := by
-  ext i hi₁ hi₂ <;> simp
+@[deprecated getElem_zipIdx (since := "2025-01-21")]
+abbrev getElem_zipWithIndex := @getElem_zipIdx
 
-@[simp] theorem toList_zipWithIndex (a : Array α) :
-    a.zipWithIndex.toList = a.toList.enum.map (fun (i, a) => (a, i)) := by
+@[simp] theorem zipIdx_toArray {l : List α} {k : Nat} :
+    l.toArray.zipIdx k = (l.zipIdx k).toArray := by
+  ext i hi₁ hi₂ <;> simp [Nat.add_comm]
+
+@[deprecated zipIdx_toArray (since := "2025-01-21")]
+abbrev zipWithIndex_toArray := @zipIdx_toArray
+
+@[simp] theorem toList_zipIdx (a : Array α) (k : Nat) :
+    (a.zipIdx k).toList = a.toList.zipIdx k := by
   rcases a with ⟨a⟩
   simp
 
-theorem mk_mem_zipWithIndex_iff_getElem? {x : α} {i : Nat} {l : Array α} :
-    (x, i) ∈ l.zipWithIndex ↔ l[i]? = x := by
-  rcases l with ⟨l⟩
-  simp only [zipWithIndex_toArray, mem_toArray, List.mem_map, Prod.mk.injEq, Prod.exists,
-    List.mk_mem_enum_iff_getElem?, List.getElem?_toArray]
-  constructor
-  · rintro ⟨a, b, h, rfl, rfl⟩
-    exact h
-  · intro h
-    exact ⟨i, x, by simp [h]⟩
+@[deprecated toList_zipIdx (since := "2025-01-21")]
+abbrev toList_zipWithIndex := @toList_zipIdx
 
-theorem mem_enum_iff_getElem? {x : α × Nat} {l : Array α} : x ∈ l.zipWithIndex ↔ l[x.2]? = some x.1 :=
-  mk_mem_zipWithIndex_iff_getElem?
+theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {l : Array α} :
+    (x, i) ∈ zipIdx l k ↔ k ≤ i ∧ l[i - k]? = some x := by
+  rcases l with ⟨l⟩
+  simp [List.mk_mem_zipIdx_iff_le_and_getElem?_sub]
+
+/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
+to avoid the inequality and the subtraction. -/
+theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {l : Array α} :
+    (x, i) ∈ l.zipIdx ↔ l[i]? = x := by
+  rw [mk_mem_zipIdx_iff_le_and_getElem?_sub]
+  simp
+
+theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : Array α} {k : Nat} :
+    x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1 := by
+  cases x
+  simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]
+
+/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
+to avoid the inequality and the subtraction. -/
+theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : Array α} :
+    x ∈ l.zipIdx ↔ l[x.2]? = some x.1 := by
+  rw [mk_mem_zipIdx_iff_getElem?]
+
+@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
+abbrev mk_mem_zipWithIndex_iff_getElem? := @mk_mem_zipIdx_iff_getElem?
+
+@[deprecated mem_zipIdx_iff_getElem? (since := "2025-01-21")]
+abbrev mem_zipWithIndex_iff_getElem? := @mem_zipIdx_iff_getElem?
 
 /-! ### mapFinIdx -/
 
@@ -179,12 +205,15 @@ theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) →
     #[a].mapFinIdx f = #[f 0 a (by simp)] := by
   simp
 
-theorem mapFinIdx_eq_zipWithIndex_map {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
-    l.mapFinIdx f = l.zipWithIndex.attach.map
+theorem mapFinIdx_eq_zipIdx_map {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
+    l.mapFinIdx f = l.zipIdx.attach.map
       fun ⟨⟨x, i⟩, m⟩ =>
-        f i x (by simp [mk_mem_zipWithIndex_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
+        f i x (by simp [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
   ext <;> simp
 
+@[deprecated mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]
+abbrev mapFinIdx_eq_zipWithIndex_map := @mapFinIdx_eq_zipIdx_map
+
 @[simp]
 theorem mapFinIdx_eq_empty_iff {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
     l.mapFinIdx f = #[] ↔ l = #[] := by
@@ -285,10 +314,13 @@ theorem mapIdx_eq_mapFinIdx {l : Array α} {f : Nat → α → β} :
     l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
   simp [mapFinIdx_eq_mapIdx]
 
-theorem mapIdx_eq_zipWithIndex_map {l : Array α} {f : Nat → α → β} :
-    l.mapIdx f = l.zipWithIndex.map fun ⟨a, i⟩ => f i a := by
+theorem mapIdx_eq_zipIdx_map {l : Array α} {f : Nat → α → β} :
+    l.mapIdx f = l.zipIdx.map fun ⟨a, i⟩ => f i a := by
   ext <;> simp
 
+@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-21")]
+abbrev mapIdx_eq_zipWithIndex_map := @mapIdx_eq_zipIdx_map
+
 theorem mapIdx_append {K L : Array α} :
     (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.size) := by
   rcases K with ⟨K⟩

src/Init/Data/List/Basic.lean

@@ -43,7 +43,7 @@ The operations are organized as follow:
  `countP`, `count`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
 * Zippers: `zipWith`, `zip`, `zipWithAll`, and `unzip`.
-* Ranges and enumeration: `range`, `iota`, `enumFrom`, and `enum`.
+* Ranges and enumeration: `range`, `zipIdx`.
 * Minima and maxima: `min?` and `max?`.
 * Other functions: `intersperse`, `intercalate`, `eraseDups`, `eraseReps`, `span`, `splitBy`,
   `removeAll`
@@ -1530,28 +1530,51 @@ set_option linter.deprecated false in
 set_option linter.deprecated false in
 @[simp] theorem iota_succ : iota (i+1) = (i+1) :: iota i := rfl
 
+/-! ### zipIdx -/
+
+/--
+`O(|l|)`. `zipIdx l` zips a list with its indices, optionally starting from a given index.
+* `zipIdx [a, b, c] = [(a, 0), (b, 1), (c, 2)]`
+* `zipIdx [a, b, c] 5 = [(a, 5), (b, 6), (c, 7)]`
+-/
+def zipIdx : List α → (n : Nat := 0) → List (α × Nat)
+  | [], _ => nil
+  | x :: xs, n => (x, n) :: zipIdx xs (n + 1)
+
+@[simp] theorem zipIdx_nil : ([] : List α).zipIdx i = [] := rfl
+@[simp] theorem zipIdx_cons : (a::as).zipIdx i = (a, i) :: as.zipIdx (i+1) := rfl
+
 /-! ### enumFrom -/
 
 /--
 `O(|l|)`. `enumFrom n l` is like `enum` but it allows you to specify the initial index.
 * `enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]`
 -/
+@[deprecated "Use `zipIdx` instead; note the signature change." (since := "2025-01-21")]
 def enumFrom : Nat → List α → List (Nat × α)
   | _, [] => nil
   | n, x :: xs   => (n, x) :: enumFrom (n + 1) xs
 
-@[simp] theorem enumFrom_nil : ([] : List α).enumFrom i = [] := rfl
-@[simp] theorem enumFrom_cons : (a::as).enumFrom i = (i, a) :: as.enumFrom (i+1) := rfl
+set_option linter.deprecated false in
+@[deprecated zipIdx_nil (since := "2025-01-21"), simp]
+theorem enumFrom_nil : ([] : List α).enumFrom i = [] := rfl
+set_option linter.deprecated false in
+@[deprecated zipIdx_cons (since := "2025-01-21"), simp]
+theorem enumFrom_cons : (a::as).enumFrom i = (i, a) :: as.enumFrom (i+1) := rfl
 
 /-! ### enum -/
 
+set_option linter.deprecated false in
 /--
 `O(|l|)`. `enum l` pairs up each element with its index in the list.
 * `enum [a, b, c] = [(0, a), (1, b), (2, c)]`
 -/
+@[deprecated "Use `zipIdx` instead; note the signature change." (since := "2025-01-21")]
 def enum : List α → List (Nat × α) := enumFrom 0
 
-@[simp] theorem enum_nil : ([] : List α).enum = [] := rfl
+set_option linter.deprecated false in
+@[deprecated zipIdx_nil (since := "2025-01-21"), simp]
+theorem enum_nil : ([] : List α).enum = [] := rfl
 
 /-! ## Minima and maxima -/
 

src/Init/Data/List/Find.lean

@@ -822,28 +822,28 @@ theorem findIdx?_flatten {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_findSome?_enum {xs : List α} {p : α → Bool} :
-    xs.findIdx? p = xs.enum.findSome? fun ⟨i, a⟩ => if p a then some i else none := by
+theorem findIdx?_eq_findSome?_zipIdx {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, enum]
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_succ, zipIdx]
     split
     · simp_all
-    · 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]
+    · simp_all only [zipIdx_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
+      rw [← map_snd_add_zipIdx_eq_zipIdx (n := 1) (k := 0)]
+      simp [Function.comp_def, 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
+theorem findIdx?_eq_fst_find?_zipIdx {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.zipIdx.find? fun ⟨x, _⟩ => p x).map (·.2) := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
-    simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, enum_cons]
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, zipIdx_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
+    · rw [ih, ← map_snd_add_zipIdx_eq_zipIdx (n := 1) (k := 0)]
+      simp [Function.comp_def, *]
 
 -- 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) :

src/Init/Data/List/Impl.lean

@@ -316,14 +316,35 @@ theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ in
 
 /-! ## Ranges and enumeration -/
 
+/-! ### zipIdx -/
+
+/-- Tail recursive version of `List.zipIdx`. -/
+def zipIdxTR (l : List α) (n : Nat := 0) : List (α × Nat) :=
+  let arr := l.toArray
+  (arr.foldr (fun a (n, acc) => (n-1, (a, n-1) :: acc)) (n + arr.size, [])).2
+
+@[csimp] theorem zipIdx_eq_zipIdxTR : @zipIdx = @zipIdxTR := by
+  funext α l n; simp [zipIdxTR, -Array.size_toArray]
+  let f := fun (a : α) (n, acc) => (n-1, (a, n-1) :: acc)
+  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, zipIdx l n)
+    | [], n => rfl
+    | a::as, n => by
+      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
+      simp [zipIdx, f]
+  rw [← Array.foldr_toList]
+  simp +zetaDelta [go]
+
 /-! ### enumFrom -/
 
 /-- Tail recursive version of `List.enumFrom`. -/
+@[deprecated zipIdxTR (since := "2025-01-21")]
 def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
   let arr := l.toArray
   (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2
 
-@[csimp] theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
+set_option linter.deprecated false in
+@[deprecated zipIdx_eq_zipIdxTR (since := "2025-01-21"), csimp]
+theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
   funext α n l; simp [enumFromTR, -Array.size_toArray]
   let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
   let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)

src/Init/Data/List/MapIdx.lean

@@ -132,16 +132,19 @@ theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) →
     [a].mapFinIdx f = [f 0 a (by simp)] := by
   simp
 
-theorem mapFinIdx_eq_enum_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
-    l.mapFinIdx f = l.enum.attach.map
-      fun ⟨⟨i, x⟩, m⟩ =>
-        f i x (by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
+theorem mapFinIdx_eq_zipIdx_map {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+    l.mapFinIdx f = l.zipIdx.attach.map
+      fun ⟨⟨x, i⟩, m⟩ =>
+        f i x (by rw [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
   apply ext_getElem <;> simp
 
+@[deprecated mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]
+abbrev mapFinIdx_eq_zipWithIndex_map := @mapFinIdx_eq_zipIdx_map
+
 @[simp]
 theorem mapFinIdx_eq_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f = [] ↔ l = [] := by
-  rw [mapFinIdx_eq_enum_map, map_eq_nil_iff, attach_eq_nil_iff, enum_eq_nil_iff]
+  rw [mapFinIdx_eq_zipIdx_map, map_eq_nil_iff, attach_eq_nil_iff, zipIdx_eq_nil_iff]
 
 theorem mapFinIdx_ne_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.mapFinIdx f ≠ [] ↔ l ≠ [] := by
@@ -149,10 +152,10 @@ theorem mapFinIdx_ne_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.
 
 theorem exists_of_mem_mapFinIdx {b : β} {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β}
     (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.length), f i l[i] h = b := by
-  rw [mapFinIdx_eq_enum_map] at h
+  rw [mapFinIdx_eq_zipIdx_map] at h
   replace h := exists_of_mem_map h
-  simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_enum_iff_getElem?] at h
-  obtain ⟨i, b, h, rfl⟩ := h
+  simp only [mem_attach, true_and, Subtype.exists, Prod.exists, mk_mem_zipIdx_iff_getElem?] at h
+  obtain ⟨b, i, h, rfl⟩ := h
   rw [getElem?_eq_some_iff] at h
   obtain ⟨h', rfl⟩ := h
   exact ⟨i, h', rfl⟩
@@ -331,17 +334,19 @@ theorem mapIdx_eq_mapFinIdx {l : List α} {f : Nat → α → β} :
     l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
   simp [mapFinIdx_eq_mapIdx]
 
-theorem mapIdx_eq_enum_map {l : List α} :
-    l.mapIdx f = l.enum.map (Function.uncurry f) := by
+theorem mapIdx_eq_zipIdx_map {l : List α} {f : Nat → α → β} :
+    l.mapIdx f = l.zipIdx.map (fun ⟨a, i⟩ => f i a) := by
   ext1 i
-  simp only [getElem?_mapIdx, Option.map, getElem?_map, getElem?_enum]
+  simp only [getElem?_mapIdx, Option.map, getElem?_map, getElem?_zipIdx]
   split <;> simp
 
+@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-21")]
+abbrev mapIdx_eq_enum_map := @mapIdx_eq_zipIdx_map
+
 @[simp]
 theorem mapIdx_cons {l : List α} {a : α} :
     mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l := by
-  simp [mapIdx_eq_enum_map, enum_eq_zip_range, map_uncurry_zip_eq_zipWith,
-    range_succ_eq_map, zipWith_map_left]
+  simp [mapIdx_eq_zipIdx_map, List.zipIdx_succ]
 
 theorem mapIdx_append {K L : List α} :
     (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.length) := by
@@ -358,7 +363,7 @@ theorem mapIdx_singleton {a : α} : mapIdx f [a] = [f 0 a] := by
 
 @[simp]
 theorem mapIdx_eq_nil_iff {l : List α} : List.mapIdx f l = [] ↔ l = [] := by
-  rw [List.mapIdx_eq_enum_map, List.map_eq_nil_iff, List.enum_eq_nil_iff]
+  rw [List.mapIdx_eq_zipIdx_map, List.map_eq_nil_iff, List.zipIdx_eq_nil_iff]
 
 theorem mapIdx_ne_nil_iff {l : List α} :
     List.mapIdx f l ≠ [] ↔ l ≠ [] := by

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

@@ -37,14 +37,14 @@ theorem find?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {b : α} :
 
 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
+  simp only [findIdx?_eq_findSome?_zipIdx] 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₂
+  rw [zipIdx_eq_append_iff] at h₂
   obtain ⟨l₁', l₂', rfl, rfl, h₂⟩ := h₂
-  rw [eq_comm, enumFrom_eq_cons_iff] at h₂
+  rw [eq_comm, zipIdx_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₂

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

@@ -339,25 +339,166 @@ theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
 
 end
 
-/-! ### enumFrom -/
+/-! ### zipIdx -/
 
 @[simp]
+theorem zipIdx_singleton (x : α) (k : Nat) : zipIdx [x] k = [(x, k)] :=
+  rfl
+
+@[simp] theorem head?_zipIdx (l : List α) (k : Nat) :
+    (zipIdx l k).head? = l.head?.map fun a => (a, k) := by
+  simp [head?_eq_getElem?]
+
+@[simp] theorem getLast?_zipIdx (l : List α) (k : Nat) :
+    (zipIdx l k).getLast? = l.getLast?.map fun a => (a, k + l.length - 1) := by
+  simp [getLast?_eq_getElem?]
+  cases l <;> simp; omega
+
+theorem mk_add_mem_zipIdx_iff_getElem? {k i : Nat} {x : α} {l : List α} :
+    (x, k + i) ∈ zipIdx l k ↔ l[i]? = some x := by
+  simp [mem_iff_getElem?, and_left_comm]
+
+theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {l : List α} :
+    (x, i) ∈ zipIdx l k ↔ k ≤ i ∧ l[i - k]? = some x := by
+  if h : k ≤ i then
+    rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩
+    simp [mk_add_mem_zipIdx_iff_getElem?, Nat.add_sub_cancel_left]
+  else
+    have : ∀ m, k + m ≠ i := by rintro _ rfl; simp at h
+    simp [h, mem_iff_get?, this]
+
+/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
+to avoid the inequality and the subtraction. -/
+theorem mk_mem_zipIdx_iff_getElem? {i : Nat} {x : α} {l : List α} : (x, i) ∈ zipIdx l ↔ l[i]? = x := by
+  simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]
+
+theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : List α} {k : Nat} :
+    x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1 := by
+  cases x
+  simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]
+
+/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
+to avoid the inequality and the subtraction. -/
+theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : List α} : x ∈ zipIdx l ↔ l[x.2]? = some x.1 := by
+  cases x
+  simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]
+
+theorem le_snd_of_mem_zipIdx {x : α × Nat} {k : Nat} {l : List α} (h : x ∈ zipIdx l k) :
+    k ≤ x.2 :=
+  (mk_mem_zipIdx_iff_le_and_getElem?_sub.1 h).1
+
+theorem snd_lt_add_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) :
+    x.2 < k + length l := by
+  rcases mem_iff_get.1 h with ⟨i, rfl⟩
+  simpa using i.isLt
+
+theorem snd_lt_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ l.zipIdx k) : x.2 < l.length + k := by
+  simpa [Nat.add_comm] using snd_lt_add_of_mem_zipIdx h
+
+theorem map_zipIdx (f : α → β) (l : List α) (k : Nat) :
+    map (Prod.map f id) (zipIdx l k) = zipIdx (l.map f) k := by
+  induction l generalizing k <;> simp_all
+
+theorem fst_mem_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) : x.1 ∈ l :=
+  zipIdx_map_fst k l ▸ mem_map_of_mem _ h
+
+theorem fst_eq_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈ zipIdx l k) :
+    x.1 = l[x.2 - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) := by
+  induction l generalizing k with
+  | nil => cases h
+  | cons hd tl ih =>
+    cases h with
+    | head h => simp
+    | tail h m =>
+      specialize ih m
+      have : x.2 - k = x.2 - (k + 1) + 1 := by
+        have := le_snd_of_mem_zipIdx m
+        omega
+      simp [this, ih]
+
+theorem mem_zipIdx {x : α} {i : Nat} {xs : List α} {k : Nat} (h : (x, i) ∈ xs.zipIdx k) :
+    k ≤ i ∧ i < k + xs.length ∧
+      x = xs[i - k]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
+  ⟨le_snd_of_mem_zipIdx h, snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩
+
+/-- Variant of `mem_zipIdx` specialized at `k = 0`. -/
+theorem mem_zipIdx' {x : α} {i : Nat} {xs : List α} (h : (x, i) ∈ xs.zipIdx) :
+    i < xs.length ∧ x = xs[i]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
+  ⟨by simpa using snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩
+
+theorem zipIdx_map (l : List α) (k : Nat) (f : α → β) :
+    zipIdx (l.map f) k = (zipIdx l k).map (Prod.map f id) := by
+  induction l with
+  | nil => rfl
+  | cons hd tl IH =>
+    rw [map_cons, zipIdx_cons', zipIdx_cons', map_cons, map_map, IH, map_map]
+    rfl
+
+theorem zipIdx_append (xs ys : List α) (k : Nat) :
+    zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + xs.length) := by
+  induction xs generalizing ys k with
+  | nil => simp
+  | cons x xs IH =>
+    rw [cons_append, zipIdx_cons, IH, ← cons_append, ← zipIdx_cons, length, Nat.add_right_comm,
+      Nat.add_assoc]
+
+theorem zipIdx_eq_cons_iff {l : List α} {k : Nat} :
+    zipIdx l k = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (a, k) ∧ l' = zipIdx as (k + 1) := by
+  rw [zipIdx_eq_zip_range', zip_eq_cons_iff]
+  constructor
+  · rintro ⟨l₁, l₂, rfl, h, rfl⟩
+    rw [range'_eq_cons_iff] at h
+    obtain ⟨rfl, -, rfl⟩ := h
+    exact ⟨x.1, l₁, by simp [zipIdx_eq_zip_range']⟩
+  · rintro ⟨a, as, rfl, rfl, rfl⟩
+    refine ⟨as, range' (k+1) as.length, ?_⟩
+    simp [zipIdx_eq_zip_range', range'_succ]
+
+theorem zipIdx_eq_append_iff {l : List α} {k : Nat} :
+    zipIdx l k = l₁ ++ l₂ ↔
+      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = zipIdx l₁' k ∧ l₂ = zipIdx l₂' (k + l₁'.length) := by
+  rw [zipIdx_eq_zip_range', zip_eq_append_iff]
+  constructor
+  · rintro ⟨w, x, y, z, h, rfl, h', rfl, rfl⟩
+    rw [range'_eq_append_iff] at h'
+    obtain ⟨k, -, rfl, rfl⟩ := h'
+    simp only [length_range'] at h
+    obtain rfl := h
+    refine ⟨w, x, rfl, ?_⟩
+    simp only [zipIdx_eq_zip_range', length_append, true_and]
+    congr
+    omega
+  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
+    simp only [zipIdx_eq_zip_range']
+    refine ⟨l₁', l₂', range' k l₁'.length, range' (k + l₁'.length) l₂'.length, ?_⟩
+    simp [Nat.add_comm]
+
+/-! ### enumFrom -/
+
+section
+set_option linter.deprecated false
+
+@[deprecated zipIdx_singleton (since := "2025-01-21"), simp]
 theorem enumFrom_singleton (x : α) (n : Nat) : enumFrom n [x] = [(n, x)] :=
   rfl
 
-@[simp] theorem head?_enumFrom (n : Nat) (l : List α) :
+@[deprecated head?_zipIdx (since := "2025-01-21"), simp]
+theorem head?_enumFrom (n : Nat) (l : List α) :
     (enumFrom n l).head? = l.head?.map fun a => (n, a) := by
   simp [head?_eq_getElem?]
 
-@[simp] theorem getLast?_enumFrom (n : Nat) (l : List α) :
+@[deprecated getLast?_zipIdx (since := "2025-01-21"), simp]
+theorem getLast?_enumFrom (n : Nat) (l : List α) :
     (enumFrom n l).getLast? = l.getLast?.map fun a => (n + l.length - 1, a) := by
   simp [getLast?_eq_getElem?]
   cases l <;> simp; omega
 
+@[deprecated mk_add_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
 theorem mk_add_mem_enumFrom_iff_getElem? {n i : Nat} {x : α} {l : List α} :
     (n + i, x) ∈ enumFrom n l ↔ l[i]? = some x := by
   simp [mem_iff_get?]
 
+@[deprecated mk_mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-21")]
 theorem mk_mem_enumFrom_iff_le_and_getElem?_sub {n i : Nat} {x : α} {l : List α} :
     (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = x := by
   if h : n ≤ i then
@@ -367,22 +508,27 @@ theorem mk_mem_enumFrom_iff_le_and_getElem?_sub {n i : Nat} {x : α} {l : List
     have : ∀ k, n + k ≠ i := by rintro k rfl; simp at h
     simp [h, mem_iff_get?, this]
 
+@[deprecated le_snd_of_mem_zipIdx (since := "2025-01-21")]
 theorem le_fst_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
     n ≤ x.1 :=
   (mk_mem_enumFrom_iff_le_and_getElem?_sub.1 h).1
 
+@[deprecated snd_lt_add_of_mem_zipIdx (since := "2025-01-21")]
 theorem fst_lt_add_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
     x.1 < n + length l := by
   rcases mem_iff_get.1 h with ⟨i, rfl⟩
   simpa using i.isLt
 
+@[deprecated map_zipIdx (since := "2025-01-21")]
 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
 
+@[deprecated fst_mem_of_mem_zipIdx (since := "2025-01-21")]
 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
 
+@[deprecated fst_eq_of_mem_zipIdx (since := "2025-01-21")]
 theorem snd_eq_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
     x.2 = l[x.1 - n]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) := by
   induction l generalizing n with
@@ -397,11 +543,13 @@ theorem snd_eq_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x
         omega
       simp [this, ih]
 
+@[deprecated mem_zipIdx (since := "2025-01-21")]
 theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enumFrom j) :
     j ≤ i ∧ i < j + xs.length ∧
       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⟩
 
+@[deprecated zipIdx_map (since := "2025-01-21")]
 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
@@ -410,6 +558,7 @@ theorem enumFrom_map (n : Nat) (l : List α) (f : α → β) :
     rw [map_cons, enumFrom_cons', enumFrom_cons', map_cons, map_map, IH, map_map]
     rfl
 
+@[deprecated zipIdx_append (since := "2025-01-21")]
 theorem enumFrom_append (xs ys : List α) (n : Nat) :
     enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys := by
   induction xs generalizing ys n with
@@ -418,6 +567,7 @@ 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]
 
+@[deprecated zipIdx_eq_cons_iff (since := "2025-01-21")]
 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]
@@ -430,6 +580,7 @@ theorem enumFrom_eq_cons_iff {l : List α} {n : Nat} :
     refine ⟨range' (n+1) as.length, as, ?_⟩
     simp [enumFrom_eq_zip_range', range'_succ]
 
+@[deprecated zipIdx_eq_append_iff (since := "2025-01-21")]
 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
@@ -449,89 +600,113 @@ theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
     refine ⟨range' n l₁'.length, range' (n + l₁'.length) l₂'.length, l₁', l₂', ?_⟩
     simp [Nat.add_comm]
 
+end
+
 /-! ### enum -/
 
-@[simp]
+section
+set_option linter.deprecated false
+
+@[deprecated zipIdx_eq_nil_iff (since := "2025-01-21"), simp]
 theorem enum_eq_nil_iff {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
 
-@[deprecated enum_eq_nil_iff (since := "2024-11-04")]
+@[deprecated zipIdx_eq_nil_iff (since := "2024-11-04")]
 theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enum_eq_nil_iff
 
-@[simp] theorem enum_singleton (x : α) : enum [x] = [(0, x)] := rfl
+@[deprecated zipIdx_singleton (since := "2025-01-21"), simp]
+theorem enum_singleton (x : α) : enum [x] = [(0, x)] := rfl
 
-@[simp] theorem enum_length : (enum l).length = l.length :=
+@[deprecated length_zipIdx (since := "2025-01-21"), simp]
+theorem enum_length : (enum l).length = l.length :=
   enumFrom_length
 
-@[simp]
+@[deprecated getElem?_zipIdx (since := "2025-01-21"), simp]
 theorem getElem?_enum (l : List α) (n : Nat) : (enum l)[n]? = l[n]?.map fun a => (n, a) := by
   rw [enum, getElem?_enumFrom, Nat.zero_add]
 
-@[simp]
+@[deprecated getElem_zipIdx (since := "2025-01-21"), simp]
 theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) :
     l.enum[i] = (i, l[i]'(by simpa [enum_length] using h)) := by
   simp [enum]
 
-@[simp] theorem head?_enum (l : List α) :
+@[deprecated head?_zipIdx (since := "2025-01-21"), simp] theorem head?_enum (l : List α) :
     l.enum.head? = l.head?.map fun a => (0, a) := by
   simp [head?_eq_getElem?]
 
-@[simp] theorem getLast?_enum (l : List α) :
+@[deprecated getLast?_zipIdx (since := "2025-01-21"), simp]
+theorem getLast?_enum (l : List α) :
     l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a) := by
   simp [getLast?_eq_getElem?]
 
-@[simp] theorem tail_enum (l : List α) : (enum l).tail = enumFrom 1 l.tail := by
+@[deprecated tail_zipIdx (since := "2025-01-21"), simp]
+theorem tail_enum (l : List α) : (enum l).tail = enumFrom 1 l.tail := by
   simp [enum]
 
+@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
 theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l[i]? = x := by
   simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]
 
+@[deprecated mem_zipIdx_iff_getElem? (since := "2025-01-21")]
 theorem mem_enum_iff_getElem? {x : Nat × α} {l : List α} : x ∈ enum l ↔ l[x.1]? = some x.2 :=
   mk_mem_enum_iff_getElem?
 
+@[deprecated snd_lt_of_mem_zipIdx (since := "2025-01-21")]
 theorem fst_lt_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.1 < length l := by
   simpa using fst_lt_add_of_mem_enumFrom h
 
+@[deprecated fst_mem_of_mem_zipIdx (since := "2025-01-21")]
 theorem snd_mem_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.2 ∈ l :=
   snd_mem_of_mem_enumFrom h
 
+@[deprecated fst_eq_of_mem_zipIdx (since := "2025-01-21")]
 theorem snd_eq_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) :
     x.2 = l[x.1]'(fst_lt_of_mem_enum h) :=
   snd_eq_of_mem_enumFrom h
 
+@[deprecated mem_zipIdx (since := "2025-01-21")]
 theorem mem_enum {x : α} {i : Nat} {xs : List α} (h : (i, x) ∈ xs.enum) :
     i < xs.length ∧ x = xs[i]'(fst_lt_of_mem_enum h) :=
   by simpa using mem_enumFrom h
 
+@[deprecated map_zipIdx (since := "2025-01-21")]
 theorem map_enum (f : α → β) (l : List α) : map (Prod.map id f) (enum l) = enum (map f l) :=
   map_enumFrom f 0 l
 
-@[simp] theorem enum_map_fst (l : List α) : map Prod.fst (enum l) = range l.length := by
+@[deprecated zipIdx_map_snd (since := "2025-01-21"), simp]
+theorem enum_map_fst (l : List α) : map Prod.fst (enum l) = range l.length := by
   simp only [enum, enumFrom_map_fst, range_eq_range']
 
-@[simp]
+@[deprecated zipIdx_map_fst (since := "2025-01-21"), simp]
 theorem enum_map_snd (l : List α) : map Prod.snd (enum l) = l :=
   enumFrom_map_snd _ _
 
+@[deprecated zipIdx_map (since := "2025-01-21")]
 theorem enum_map (l : List α) (f : α → β) : (l.map f).enum = l.enum.map (Prod.map id f) :=
   enumFrom_map _ _ _
 
+@[deprecated zipIdx_append (since := "2025-01-21")]
 theorem enum_append (xs ys : List α) : enum (xs ++ ys) = enum xs ++ enumFrom xs.length ys := by
   simp [enum, enumFrom_append]
 
+@[deprecated zipIdx_eq_zip_range' (since := "2025-01-21")]
 theorem enum_eq_zip_range (l : List α) : l.enum = (range l.length).zip l :=
   zip_of_prod (enum_map_fst _) (enum_map_snd _)
 
-@[simp]
+@[deprecated unzip_zipIdx_eq_prod (since := "2025-01-21"), simp]
 theorem unzip_enum_eq_prod (l : List α) : l.enum.unzip = (range l.length, l) := by
   simp only [enum_eq_zip_range, unzip_zip, length_range]
 
+@[deprecated zipIdx_eq_cons_iff (since := "2025-01-21")]
 theorem enum_eq_cons_iff {l : List α} :
     l.enum = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (0, a) ∧ l' = enumFrom 1 as := by
   rw [enum, enumFrom_eq_cons_iff]
 
+@[deprecated zipIdx_eq_append_iff (since := "2025-01-21")]
 theorem enum_eq_append_iff {l : List α} :
     l.enum = l₁ ++ l₂ ↔
       ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enum ∧ l₂ = l₂'.enumFrom l₁'.length := by
   simp [enum, enumFrom_eq_append_iff]
 
+end
+
 end List

src/Init/Data/List/Range.lean

@@ -204,17 +204,97 @@ theorem getLast?_range (n : Nat) : (range n).getLast? = if n = 0 then none else
   | zero => simp at h
   | succ n => simp [getLast?_range, getLast_eq_iff_getLast_eq_some]
 
-/-! ### enumFrom -/
+/-! ### zipIdx -/
 
 @[simp]
+theorem zipIdx_eq_nil_iff {l : List α} {n : Nat} : List.zipIdx l n = [] ↔ l = [] := by
+  cases l <;> simp
+
+@[simp] theorem length_zipIdx : ∀ {l : List α} {n}, (zipIdx l n).length = l.length
+  | [], _ => rfl
+  | _ :: _, _ => congrArg Nat.succ length_zipIdx
+
+@[simp]
+theorem getElem?_zipIdx :
+    ∀ (l : List α) n m, (zipIdx l n)[m]? = l[m]?.map fun a => (a, n + m)
+  | [], _, _ => rfl
+  | _ :: _, _, 0 => by simp
+  | _ :: l, n, m + 1 => by
+    simp only [zipIdx_cons, getElem?_cons_succ]
+    exact (getElem?_zipIdx l (n + 1) m).trans <| by rw [Nat.add_right_comm]; rfl
+
+@[simp]
+theorem getElem_zipIdx (l : List α) (n) (i : Nat) (h : i < (l.zipIdx n).length) :
+    (l.zipIdx n)[i] = (l[i]'(by simpa [length_zipIdx] using h), n + i) := by
+  simp only [length_zipIdx] at h
+  rw [getElem_eq_getElem?_get]
+  simp only [getElem?_zipIdx, getElem?_eq_getElem h]
+  simp
+
+@[simp]
+theorem tail_zipIdx (l : List α) (n : Nat) : (zipIdx l n).tail = zipIdx l.tail (n + 1) := by
+  induction l generalizing n with
+  | nil => simp
+  | cons _ l ih => simp [ih, zipIdx_cons]
+
+theorem map_snd_add_zipIdx_eq_zipIdx (l : List α) (n k : Nat) :
+    map (Prod.map id (· + n)) (zipIdx l k) = zipIdx l (n + k) :=
+  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl
+
+theorem zipIdx_cons' (n : Nat) (x : α) (xs : List α) :
+    zipIdx (x :: xs) n = (x, n) :: (zipIdx xs n).map (Prod.map id (· + 1)) := by
+  rw [zipIdx_cons, Nat.add_comm, ← map_snd_add_zipIdx_eq_zipIdx]
+
+@[simp]
+theorem zipIdx_map_snd (n) :
+    ∀ (l : List α), map Prod.snd (zipIdx l n) = range' n l.length
+  | [] => rfl
+  | _ :: _ => congrArg (cons _) (zipIdx_map_snd _ _)
+
+@[simp]
+theorem zipIdx_map_fst : ∀ (n) (l : List α), map Prod.fst (zipIdx l n) = l
+  | _, [] => rfl
+  | _, _ :: _ => congrArg (cons _) (zipIdx_map_fst _ _)
+
+theorem zipIdx_eq_zip_range' (l : List α) {n : Nat} : l.zipIdx n = l.zip (range' n l.length) :=
+  zip_of_prod (zipIdx_map_fst _ _) (zipIdx_map_snd _ _)
+
+@[simp]
+theorem unzip_zipIdx_eq_prod (l : List α) {n : Nat} :
+    (l.zipIdx n).unzip = (l, range' n l.length) := by
+  simp only [zipIdx_eq_zip_range', unzip_zip, length_range']
+
+/-- Replace `zipIdx` with a starting index `n+1` with `zipIdx` starting from `n`,
+followed by a `map` increasing the indices by one. -/
+theorem zipIdx_succ (l : List α) (n : Nat) :
+    l.zipIdx (n + 1) = (l.zipIdx n).map (fun ⟨a, i⟩ => (a, i + 1)) := by
+  induction l generalizing n with
+  | nil => rfl
+  | cons _ _ ih => simp only [zipIdx_cons, ih (n + 1), map_cons]
+
+/-- Replace `zipIdx` with a starting index with `zipIdx` starting from 0,
+followed by a `map` increasing the indices. -/
+theorem zipIdx_eq_map_add (l : List α) (n : Nat) :
+    l.zipIdx n = l.zipIdx.map (fun ⟨a, i⟩ => (a, n + i)) := by
+  induction l generalizing n with
+  | nil => rfl
+  | cons _ _ ih => simp [ih (n+1), zipIdx_succ, Nat.add_assoc, Nat.add_comm 1]
+
+/-! ### enumFrom -/
+
+section
+set_option linter.deprecated false
+
+@[deprecated zipIdx_eq_nil_iff (since := "2025-01-21"), simp]
 theorem enumFrom_eq_nil {n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l = [] := by
   cases l <;> simp
 
-@[simp] theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length
+@[deprecated length_zipIdx (since := "2025-01-21"), simp]
+theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length
   | _, [] => rfl
   | _, _ :: _ => congrArg Nat.succ enumFrom_length
 
-@[simp]
+@[deprecated getElem?_zipIdx (since := "2025-01-21"), simp]
 theorem getElem?_enumFrom :
     ∀ n (l : List α) m, (enumFrom n l)[m]? = l[m]?.map fun a => (n + m, a)
   | _, [], _ => rfl
@@ -223,7 +303,7 @@ theorem getElem?_enumFrom :
     simp only [enumFrom_cons, getElem?_cons_succ]
     exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl
 
-@[simp]
+@[deprecated getElem_zipIdx (since := "2025-01-21"), simp]
 theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).length) :
     (l.enumFrom n)[i] = (n + i, l[i]'(by simpa [enumFrom_length] using h)) := by
   simp only [enumFrom_length] at h
@@ -231,53 +311,66 @@ theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).len
   simp only [getElem?_enumFrom, getElem?_eq_getElem h]
   simp
 
-@[simp]
+@[deprecated tail_zipIdx (since := "2025-01-21"), simp]
 theorem tail_enumFrom (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail := by
   induction l generalizing n with
   | nil => simp
   | cons _ l ih => simp [ih, enumFrom_cons]
 
+@[deprecated map_snd_add_zipIdx_eq_zipIdx (since := "2025-01-21"), simp]
 theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
     map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
   ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl
 
+@[deprecated map_snd_add_zipIdx_eq_zipIdx (since := "2025-01-21"), simp]
 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 _ _
 
+@[deprecated zipIdx_cons' (since := "2025-01-21"), simp]
 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]
+@[deprecated zipIdx_map_snd (since := "2025-01-21"), 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]
+@[deprecated zipIdx_map_fst (since := "2025-01-21"), simp]
 theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
   | _, [] => rfl
   | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
 
+@[deprecated zipIdx_eq_zip_range' (since := "2025-01-21")]
 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]
+@[deprecated unzip_zipIdx_eq_prod (since := "2025-01-21"), 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']
 
+end
+
 /-! ### enum -/
 
+section
+set_option linter.deprecated false
+
+@[deprecated zipIdx_cons (since := "2025-01-21")]
 theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
 
+@[deprecated zipIdx_cons (since := "2025-01-21")]
 theorem enum_cons' (x : α) (xs : List α) :
     enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
   enumFrom_cons' _ _ _
 
+@[deprecated "These are now both `l.zipIdx 0`" (since := "2025-01-21")]
 theorem enum_eq_enumFrom {l : List α} : l.enum = l.enumFrom 0 := rfl
 
+@[deprecated "Use the reverse direction of `map_snd_add_zipIdx_eq_zipIdx` instead" (since := "2025-01-21")]
 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
@@ -288,4 +381,6 @@ theorem enumFrom_eq_map_enum (l : List α) (n : Nat) :
     intro a b _
     exact (succ_add a n).symm
 
+end
+
 end List

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

@@ -73,14 +73,14 @@ termination_by xs => xs.length
 
 /--
 Given an ordering relation `le : α → α → Bool`,
-construct the reverse lexicographic ordering on `Nat × α`.
-which first compares the second components using `le`,
+construct the lexicographic ordering on `α × Nat`.
+which first compares the first components using `le`,
 but if these are equivalent (in the sense `le a.2 b.2 && le b.2 a.2`)
-then compares the first components using `≤`.
+then compares the second components using `≤`.
 
 This function is only used in stating the stability properties of `mergeSort`.
 -/
-def enumLE (le : α → α → Bool) (a b : Nat × α) : Bool :=
-  if le a.2 b.2 then if le b.2 a.2 then a.1 ≤ b.1 else true else false
+def zipIdxLE (le : α → α → Bool) (a b : α × Nat) : Bool :=
+  if le a.1 b.1 then if le b.1 a.1 then a.2 ≤ b.2 else true else false
 
 end List

src/Init/Data/List/Sort/Lemmas.lean

@@ -38,35 +38,35 @@ namespace MergeSort.Internal
 theorem splitInTwo_fst_append_splitInTwo_snd (l : { l : List α // l.length = n }) : (splitInTwo l).1.1 ++ (splitInTwo l).2.1 = l.1 := by
   simp
 
-theorem splitInTwo_cons_cons_enumFrom_fst (i : Nat) (l : List α) :
-    (splitInTwo ⟨(i, a) :: (i+1, b) :: l.enumFrom (i+2), rfl⟩).1.1 =
-      (splitInTwo ⟨a :: b :: l, rfl⟩).1.1.enumFrom i := by
-  simp only [length_cons, splitInTwo_fst, enumFrom_length]
+theorem splitInTwo_cons_cons_zipIdx_fst (i : Nat) (l : List α) :
+    (splitInTwo ⟨(a, i) :: (b, i+1) :: l.zipIdx (i+2), rfl⟩).1.1 =
+      (splitInTwo ⟨a :: b :: l, rfl⟩).1.1.zipIdx i := by
+  simp only [length_cons, splitInTwo_fst, length_zipIdx]
   ext1 j
-  rw [getElem?_take, getElem?_enumFrom, getElem?_take]
+  rw [getElem?_take, getElem?_zipIdx, getElem?_take]
   split
   · rw [getElem?_cons, getElem?_cons, getElem?_cons, getElem?_cons]
     split
     · simp; omega
     · split
       · simp; omega
-      · simp only [getElem?_enumFrom]
+      · simp only [getElem?_zipIdx]
         congr
         ext <;> simp; omega
   · simp
 
-theorem splitInTwo_cons_cons_enumFrom_snd (i : Nat) (l : List α) :
-    (splitInTwo ⟨(i, a) :: (i+1, b) :: l.enumFrom (i+2), rfl⟩).2.1 =
-      (splitInTwo ⟨a :: b :: l, rfl⟩).2.1.enumFrom (i+(l.length+3)/2) := by
-  simp only [length_cons, splitInTwo_snd, enumFrom_length]
+theorem splitInTwo_cons_cons_zipIdx_snd (i : Nat) (l : List α) :
+    (splitInTwo ⟨(a, i) :: (b, i+1) :: l.zipIdx (i+2), rfl⟩).2.1 =
+      (splitInTwo ⟨a :: b :: l, rfl⟩).2.1.zipIdx (i+(l.length+3)/2) := by
+  simp only [length_cons, splitInTwo_snd, length_zipIdx]
   ext1 j
-  rw [getElem?_drop, getElem?_enumFrom, getElem?_drop]
+  rw [getElem?_drop, getElem?_zipIdx, getElem?_drop]
   rw [getElem?_cons, getElem?_cons, getElem?_cons, getElem?_cons]
   split
   · simp; omega
   · split
     · simp; omega
-    · simp only [getElem?_enumFrom]
+    · simp only [getElem?_zipIdx]
       congr
       ext <;> simp; omega
 
@@ -88,13 +88,13 @@ end MergeSort.Internal
 
 open MergeSort.Internal
 
-/-! ### enumLE -/
+/-! ### zipIdxLE -/
 
 variable {le : α → α → Bool}
 
-theorem enumLE_trans (trans : ∀ a b c, le a b → le b c → le a c)
-    (a b c : Nat × α) : enumLE le a b → enumLE le b c → enumLE le a c := by
-  simp only [enumLE]
+theorem zipIdxLE_trans (trans : ∀ a b c, le a b → le b c → le a c)
+    (a b c : α × Nat) : zipIdxLE le a b → zipIdxLE le b c → zipIdxLE le a c := by
+  simp only [zipIdxLE]
   split <;> split <;> split <;> rename_i ab₂ ba₂ bc₂
   · simp_all
     intro ab₁
@@ -120,14 +120,14 @@ theorem enumLE_trans (trans : ∀ a b c, le a b → le b c → le a c)
   · simp_all
   · simp_all
 
-theorem enumLE_total (total : ∀ a b, le a b || le b a)
-    (a b : Nat × α) : enumLE le a b || enumLE le b a := by
-  simp only [enumLE]
+theorem zipIdxLE_total (total : ∀ a b, le a b || le b a)
+    (a b : α × Nat) : zipIdxLE le a b || zipIdxLE le b a := by
+  simp only [zipIdxLE]
   split <;> split
-  · simpa using Nat.le_total a.fst b.fst
+  · simpa using Nat.le_total a.2 b.2
   · simp
   · simp
-  · have := total a.2 b.2
+  · have := total a.1 b.1
     simp_all
 
 /-! ### merge -/
@@ -179,12 +179,12 @@ theorem mem_merge_left (s : α → α → Bool) (h : x ∈ l) : x ∈ merge l r
 theorem mem_merge_right (s : α → α → Bool) (h : x ∈ r) : x ∈ merge l r s :=
   mem_merge.2 <| .inr h
 
-theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.1 ≤ y.1),
-    (merge xs ys (enumLE le)).map (·.2) = merge (xs.map (·.2)) (ys.map (·.2)) le
+theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.2 ≤ y.2),
+    (merge xs ys (zipIdxLE le)).map (·.1) = merge (xs.map (·.1)) (ys.map (·.1)) le
   | [], ys, _ => by simp [merge]
   | xs, [], _ => by simp [merge]
   | (i, x) :: xs, (j, y) :: ys, h => by
-    simp only [merge, enumLE, map_cons]
+    simp only [merge, zipIdxLE, map_cons]
     split <;> rename_i w
     · rw [if_pos (by simp [h _ _ (mem_cons_self ..) (mem_cons_self ..)])]
       simp only [map_cons, cons.injEq, true_and]
@@ -331,57 +331,59 @@ See also:
 * `sublist_mergeSort`: if `c <+ l` and `c.Pairwise le`, then `c <+ mergeSort le l`.
 * `pair_sublist_mergeSort`: if `[a, b] <+ l` and `le a b`, then `[a, b] <+ mergeSort le l`)
 -/
-theorem mergeSort_enum {l : List α} :
-    (mergeSort (l.enum) (enumLE le)).map (·.2) = mergeSort l le :=
+theorem mergeSort_zipIdx {l : List α} :
+    (mergeSort (l.zipIdx) (zipIdxLE le)).map (·.1) = mergeSort l le :=
   go 0 l
 where go : ∀ (i : Nat) (l : List α),
-    (mergeSort (l.enumFrom i) (enumLE le)).map (·.2) = mergeSort l le
+    (mergeSort (l.zipIdx i) (zipIdxLE le)).map (·.1) = mergeSort l le
   | _, []
   | _, [a] => by simp [mergeSort]
   | _, a :: b :: xs => by
     have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega
     have : (splitInTwo ⟨a :: b :: xs, rfl⟩).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega
-    simp only [mergeSort, enumFrom]
-    rw [splitInTwo_cons_cons_enumFrom_fst]
-    rw [splitInTwo_cons_cons_enumFrom_snd]
+    simp only [mergeSort, zipIdx]
+    rw [splitInTwo_cons_cons_zipIdx_fst]
+    rw [splitInTwo_cons_cons_zipIdx_snd]
     rw [merge_stable]
     · rw [go, go]
     · simp only [mem_mergeSort, Prod.forall]
       intros j x k y mx my
-      have := mem_enumFrom mx
-      have := mem_enumFrom my
+      have := mem_zipIdx mx
+      have := mem_zipIdx my
       simp_all
       omega
 termination_by _ l => l.length
 
+@[deprecated mergeSort_zipIdx (since := "2025-01-21")] abbrev mergeSort_enum := @mergeSort_zipIdx
+
 theorem mergeSort_cons {le : α → α → Bool}
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
     (total : ∀ (a b : α), le a b || le b a)
     (a : α) (l : List α) :
     ∃ l₁ l₂, mergeSort (a :: l) le = l₁ ++ a :: l₂ ∧ mergeSort l le = l₁ ++ l₂ ∧
       ∀ b, b ∈ l₁ → !le a b := by
-  rw [← mergeSort_enum]
-  rw [enum_cons]
-  have nd : Nodup ((a :: l).enum.map (·.1)) := by rw [enum_map_fst]; exact nodup_range _
-  have m₁ : (0, a) ∈ mergeSort ((a :: l).enum) (enumLE le) :=
+  rw [← mergeSort_zipIdx]
+  rw [zipIdx_cons]
+  have nd : Nodup ((a :: l).zipIdx.map (·.2)) := by rw [zipIdx_map_snd]; exact nodup_range' _ _
+  have m₁ : (a, 0) ∈ mergeSort ((a :: l).zipIdx) (zipIdxLE le) :=
     mem_mergeSort.mpr (mem_cons_self _ _)
   obtain ⟨l₁, l₂, h⟩ := append_of_mem m₁
-  have s := sorted_mergeSort (enumLE_trans trans) (enumLE_total total) ((a :: l).enum)
+  have s := sorted_mergeSort (zipIdxLE_trans trans) (zipIdxLE_total total) ((a :: l).zipIdx)
   rw [h] at s
-  have p := mergeSort_perm ((a :: l).enum) (enumLE le)
+  have p := mergeSort_perm ((a :: l).zipIdx) (zipIdxLE le)
   rw [h] at p
-  refine ⟨l₁.map (·.2), l₂.map (·.2), ?_, ?_, ?_⟩
-  · simpa using congrArg (·.map (·.2)) h
-  · rw [← mergeSort_enum.go 1, ← map_append]
+  refine ⟨l₁.map (·.1), l₂.map (·.1), ?_, ?_, ?_⟩
+  · simpa using congrArg (·.map (·.1)) h
+  · rw [← mergeSort_zipIdx.go 1, ← map_append]
     congr 1
-    have q : mergeSort (enumFrom 1 l) (enumLE le) ~ l₁ ++ l₂ :=
-      (mergeSort_perm (enumFrom 1 l) (enumLE le)).trans
+    have q : mergeSort (l.zipIdx 1) (zipIdxLE le) ~ l₁ ++ l₂ :=
+      (mergeSort_perm (l.zipIdx 1) (zipIdxLE le)).trans
         (p.symm.trans perm_middle).cons_inv
-    apply Perm.eq_of_sorted (le := enumLE le)
-    · rintro ⟨i, a⟩ ⟨j, b⟩  ha hb
+    apply Perm.eq_of_sorted (le := zipIdxLE le)
+    · rintro ⟨a, i⟩ ⟨b, j⟩  ha hb
       simp only [mem_mergeSort] at ha
       simp only [← q.mem_iff, mem_mergeSort] at hb
-      simp only [enumLE]
+      simp only [zipIdxLE]
       simp only [Bool.if_false_right, Bool.and_eq_true, Prod.mk.injEq, and_imp]
       intro ab h ba h'
       simp only [Bool.decide_eq_true] at ba
@@ -389,24 +391,24 @@ theorem mergeSort_cons {le : α → α → Bool}
       replace h' : j ≤ i := by simpa [ab, ba] using h'
       cases Nat.le_antisymm h h'
       constructor
-      · rfl
-      · have := mem_enumFrom ha
-        have := mem_enumFrom hb
+      · have := mem_zipIdx ha
+        have := mem_zipIdx hb
         simp_all
-    · exact sorted_mergeSort (enumLE_trans trans) (enumLE_total total) ..
-    · exact s.sublist ((sublist_cons_self (0, a) l₂).append_left l₁)
+      · rfl
+    · exact sorted_mergeSort (zipIdxLE_trans trans) (zipIdxLE_total total) ..
+    · exact s.sublist ((sublist_cons_self (a, 0) l₂).append_left l₁)
     · exact q
   · intro b m
-    simp only [mem_map, Prod.exists, exists_eq_right] at m
-    obtain ⟨j, m⟩ := m
-    replace p := p.map (·.1)
+    simp only [mem_map, Prod.exists] at m
+    obtain ⟨j, _, m, rfl⟩ := m
+    replace p := p.map (·.2)
     have nd' := nd.perm p.symm
     rw [map_append] at nd'
     have j0 := nd'.rel_of_mem_append
-      (mem_map_of_mem (·.1) m) (mem_map_of_mem _ (mem_cons_self _ _))
+      (mem_map_of_mem (·.2) m) (mem_map_of_mem _ (mem_cons_self _ _))
     simp only [ne_eq] at j0
     have r := s.rel_of_mem_append m (mem_cons_self _ _)
-    simp_all [enumLE]
+    simp_all [zipIdxLE]
 
 /--
 Another statement of stability of merge sort.

src/Init/Data/List/Zip.lean

@@ -238,6 +238,14 @@ theorem map_uncurry_zip_eq_zipWith (f : α → β → γ) (l : List α) (l' : Li
   | cons hl tl ih =>
     cases l' <;> simp [ih]
 
+theorem map_zip_eq_zipWith (f : α × β → γ) (l : List α) (l' : List β) :
+    map f (l.zip l') = zipWith (Function.curry f) l l' := by
+  rw [zip]
+  induction l generalizing l' with
+  | nil => simp
+  | cons hl tl ih =>
+    cases l' <;> simp [ih]
+
 /-! ### zip -/
 
 theorem zip_eq_zipWith : ∀ (l₁ : List α) (l₂ : List β), zip l₁ l₂ = zipWith Prod.mk l₁ l₂

src/Init/Data/Vector/Basic.lean

@@ -185,8 +185,11 @@ which also receives the index of the element, and the fact that the index is les
 @[inline] def flatMap (v : Vector α n) (f : α → Vector β m) : Vector β (n * m) :=
   ⟨v.toArray.flatMap fun a => (f a).toArray, by simp [Array.map_const']⟩
 
-@[inline] def zipWithIndex (v : Vector α n) : Vector (α × Nat) n :=
-  ⟨v.toArray.zipWithIndex, by simp⟩
+@[inline] def zipIdx (v : Vector α n) (k : Nat := 0) : Vector (α × Nat) n :=
+  ⟨v.toArray.zipIdx k, by simp⟩
+
+@[deprecated zipIdx (since := "2025-01-21")]
+abbrev zipWithIndex := @zipIdx
 
 /-- Maps corresponding elements of two vectors of equal size using the function `f`. -/
 @[inline] def zipWith (a : Vector α n) (b : Vector β n) (f : α → β → φ) : Vector φ n :=

src/Init/Data/Vector/Lemmas.lean

@@ -151,8 +151,11 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 @[simp] theorem take_mk (a : Array α) (h : a.size = n) (m) :
     (Vector.mk a h).take m = Vector.mk (a.take m) (by simp [h]) := rfl
 
-@[simp] theorem zipWithIndex_mk (a : Array α) (h : a.size = n) :
-    (Vector.mk a h).zipWithIndex = Vector.mk (a.zipWithIndex) (by simp [h]) := rfl
+@[simp] theorem zipIdx_mk (a : Array α) (h : a.size = n) (k : Nat := 0) :
+    (Vector.mk a h).zipIdx k = Vector.mk (a.zipIdx k) (by simp [h]) := rfl
+
+@[deprecated zipIdx_mk (since := "2025-01-21")]
+abbrev zipWithIndex_mk := @zipIdx_mk
 
 @[simp] theorem mk_zipWith_mk (f : α → β → γ) (a : Array α) (b : Array β)
       (ha : a.size = n) (hb : b.size = n) : zipWith (Vector.mk a ha) (Vector.mk b hb) f =
@@ -273,8 +276,8 @@ theorem toArray_mk (a : Array α) (h : a.size = n) : (Vector.mk a h).toArray = a
 
 @[simp] theorem toArray_take (a : Vector α n) (m) : (a.take m).toArray = a.toArray.take m := rfl
 
-@[simp] theorem toArray_zipWithIndex (a : Vector α n) :
-    (a.zipWithIndex).toArray = a.toArray.zipWithIndex := rfl
+@[simp] theorem toArray_zipIdx (a : Vector α n) (k : Nat := 0) :
+    (a.zipIdx k).toArray = a.toArray.zipIdx k := rfl
 
 @[simp] theorem toArray_zipWith (f : α → β → γ) (a : Vector α n) (b : Vector β n) :
     (Vector.zipWith a b f).toArray = Array.zipWith a.toArray b.toArray f := rfl

src/Init/Data/Vector/MapIdx.lean

@@ -51,30 +51,60 @@ end Array
 
 namespace Vector
 
-/-! ### zipWithIndex -/
+/-! ### zipIdx -/
 
-@[simp] theorem toList_zipWithIndex (a : Vector α n) :
-    a.zipWithIndex.toList = a.toList.enum.map (fun (i, a) => (a, i)) := by
+@[simp] theorem toList_zipIdx (a : Vector α n) (k : Nat := 0) :
+    (a.zipIdx k).toList = a.toList.zipIdx k := by
   rcases a with ⟨a, rfl⟩
   simp
 
-@[simp] theorem getElem_zipWithIndex (a : Vector α n) (i : Nat) (h : i < n) :
-    (a.zipWithIndex)[i] = (a[i]'(by simp_all), i) := by
+@[simp] theorem getElem_zipIdx (a : Vector α n) (i : Nat) (h : i < n) :
+    (a.zipIdx k)[i] = (a[i]'(by simp_all), i + k) := by
   rcases a with ⟨a, rfl⟩
   simp
 
-@[simp] theorem zipWithIndex_toVector {l : Array α} :
-    l.toVector.zipWithIndex = l.zipWithIndex.toVector.cast (by simp) := by
+@[simp] theorem zipIdx_toVector {l : Array α} {k : Nat} :
+    l.toVector.zipIdx k = (l.zipIdx k).toVector.cast (by simp) := by
   ext <;> simp
 
-theorem mk_mem_zipWithIndex_iff_getElem? {x : α} {i : Nat} {l : Vector α n} :
-    (x, i) ∈ l.zipWithIndex ↔ l[i]? = x := by
+theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {x : α} {i : Nat} {l : Vector α n} {k : Nat} :
+    (x, i) ∈ l.zipIdx k ↔ k ≤ i ∧ l[i - k]? = x := by
   rcases l with ⟨l, rfl⟩
-  simp [Array.mk_mem_zipWithIndex_iff_getElem?]
+  simp [Array.mk_mem_zipIdx_iff_le_and_getElem?_sub]
 
-theorem mem_enum_iff_getElem? {x : α × Nat} {l : Vector α n} :
-    x ∈ l.zipWithIndex ↔ l[x.2]? = some x.1 :=
-  mk_mem_zipWithIndex_iff_getElem?
+/-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
+to avoid the inequality and the subtraction. -/
+theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {l : Vector α n} :
+    (x, i) ∈ l.zipIdx ↔ l[i]? = x := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.mk_mem_zipIdx_iff_le_and_getElem?_sub]
+
+theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : Vector α n} {k : Nat} :
+    x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1 := by
+  cases x
+  simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]
+
+/-- Variant of `mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
+to avoid the inequality and the subtraction. -/
+theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : Vector α n} :
+    x ∈ l.zipIdx ↔ l[x.2]? = some x.1 := by
+  rcases l with ⟨l, rfl⟩
+  simp [Array.mem_zipIdx_iff_getElem?]
+
+@[deprecated toList_zipIdx (since := "2025-01-27")]
+abbrev toList_zipWithIndex := @toList_zipIdx
+@[deprecated getElem_zipIdx (since := "2025-01-27")]
+abbrev getElem_zipWithIndex := @getElem_zipIdx
+@[deprecated zipIdx_toVector (since := "2025-01-27")]
+abbrev zipWithIndex_toVector := @zipIdx_toVector
+@[deprecated mk_mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-27")]
+abbrev mk_mem_zipWithIndex_iff_le_and_getElem?_sub := @mk_mem_zipIdx_iff_le_and_getElem?_sub
+@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-27")]
+abbrev mk_mem_zipWithIndex_iff_getElem? := @mk_mem_zipIdx_iff_getElem?
+@[deprecated mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-27")]
+abbrev mem_zipWithIndex_iff_le_and_getElem?_sub := @mem_zipIdx_iff_le_and_getElem?_sub
+@[deprecated mem_zipIdx_iff_getElem? (since := "2025-01-27")]
+abbrev mem_zipWithIndex_iff_getElem? := @mem_zipIdx_iff_getElem?
 
 /-! ### mapFinIdx -/
 
@@ -215,10 +245,13 @@ theorem mapIdx_eq_mapFinIdx {l : Vector α n} {f : Nat → α → β} :
     l.mapIdx f = l.mapFinIdx (fun i a _ => f i a) := by
   simp [mapFinIdx_eq_mapIdx]
 
-theorem mapIdx_eq_zipWithIndex_map {l : Vector α n} {f : Nat → α → β} :
-    l.mapIdx f = l.zipWithIndex.map fun ⟨a, i⟩ => f i a := by
+theorem mapIdx_eq_zipIdx_map {l : Vector α n} {f : Nat → α → β} :
+    l.mapIdx f = l.zipIdx.map fun ⟨a, i⟩ => f i a := by
   ext <;> simp
 
+@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-27")]
+abbrev mapIdx_eq_zipWithIndex_map := @mapIdx_eq_zipIdx_map
+
 theorem mapIdx_append {K : Vector α n} {L : Vector α m} :
     (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.size) := by
   rcases K with ⟨K, rfl⟩

src/Init/Omega/Coeffs.lean

@@ -67,9 +67,7 @@ abbrev leading (xs : Coeffs) : Int := IntList.leading xs
 abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs
 /-- Shim for `.enum.find?`. -/
 abbrev findIdx? (f : Int → Bool) (xs : Coeffs) : Option Nat :=
-  -- List.findIdx? f xs
-  -- We could avoid `Batteries.Data.List.Basic` by using the less efficient:
-  xs.enum.find? (f ·.2) |>.map (·.1)
+  List.findIdx? f xs
 /-- Shim for `IntList.bmod`. -/
 abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m
 /-- Shim for `IntList.bmod_dot_sub_dot_bmod`. -/

src/Init/Omega/LinearCombo.lean

@@ -28,7 +28,7 @@ namespace LinearCombo
 
 instance : ToString LinearCombo where
   toString lc :=
-    s!"{lc.const}{String.join <| lc.coeffs.toList.enum.map fun ⟨i, c⟩ => s!" + {c} * x{i+1}"}"
+    s!"{lc.const}{String.join <| lc.coeffs.toList.zipIdx.map fun ⟨c, i⟩ => s!" + {c} * x{i+1}"}"
 
 instance : Inhabited LinearCombo := ⟨{const := 1}⟩
 

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -585,10 +585,9 @@ where
       s!"{x} ≤ {e} ≤ {y}"
 
   prettyCoeffs (names : Array String) (coeffs : Coeffs) : String :=
-    coeffs.toList.enum
-      |>.filter (fun (_,c) => c ≠ 0)
-      |>.enum
-      |>.map (fun (j, (i,c)) =>
+    coeffs.toList.zipIdx
+      |>.filter (fun (c,_) => c ≠ 0)
+      |>.mapIdx (fun j (c,i) =>
         (if j > 0 then if c > 0 then " + " else " - " else if c > 0 then "" else "- ") ++
         (if Int.natAbs c = 1 then names[i]! else s!"{c.natAbs}*{names[i]!}"))
       |> String.join
@@ -596,13 +595,13 @@ where
   mentioned (atoms : Array Expr) (constraints : Std.HashMap Coeffs Fact) : MetaM (Array Bool) := do
     let initMask := Array.mkArray atoms.size false
     return constraints.fold (init := initMask) fun mask coeffs _ =>
-      coeffs.enum.foldl (init := mask) fun mask (i, c) =>
+      coeffs.zipIdx.foldl (init := mask) fun mask (c, i) =>
         if c = 0 then mask else mask.set! i true
 
   prettyAtoms (names : Array String) (atoms : Array Expr) (mask : Array Bool) : MessageData :=
-    (Array.zip names atoms).toList.enum
-      |>.filter (fun (i, _) => mask.getD i false)
-      |>.map (fun (_, (n, a)) => m!" {n} := {a}")
+    (Array.zip names atoms).toList.zipIdx
+      |>.filter (fun (_, i) => mask.getD i false)
+      |>.map (fun ((n, a),_) => m!" {n} := {a}")
       |> m!"\n".joinSep
 
 mutual

src/Lean/ParserCompiler.lean

@@ -46,7 +46,7 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
   else forallTelescope (← inferType e.getAppFn) fun params _ => do
     let lctx ← getLCtx
     -- if there is exactly one parameter of type `Parser`, search there
-    if let [(i, _)] := params.toList.enum.filter (lctx.getFVar! ·.2 |>.type.isConstOf ``Parser) then
+    if let #[(_, i)] := params.zipIdx.filter (lctx.getFVar! ·.1 |>.type.isConstOf ``Parser) then
       parserNodeKind? (e.getArg! i)
     else
       return none

src/Lean/Server/Completion/CompletionInfoSelection.lean

@@ -125,7 +125,7 @@ def findPrioritizedCompletionPartitionsAt
     (infoTree : InfoTree)
     : Array (Array (ContextualizedCompletionInfo × Nat)) :=
   findCompletionInfosAt fileMap hoverPos cmdStx infoTree
-    |>.zipWithIndex
+    |>.zipIdx
     |> computePrioritizedCompletionPartitions
 
 end Lean.Server.Completion

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -311,7 +311,7 @@ private def isSyntheticStructFieldCompletion
     if isCompletionInEmptyBlock then
       return true
 
-    let isCompletionAfterSep := fieldsAndSeps.zipWithIndex.any fun (fieldOrSep, i) => Id.run do
+    let isCompletionAfterSep := fieldsAndSeps.zipIdx.any fun (fieldOrSep, i) => Id.run do
       if i % 2 == 0 || !fieldOrSep.isAtom then
         return false
       let sep := fieldOrSep