fixes

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

@@ -27,12 +27,12 @@ open Nat
   | succ n, [] => by simp [Nat.min_zero]
   | succ n, _ :: l => by simp [Nat.succ_min_succ, length_take]
 
-theorem length_take_le (n) (l : List α) : length (take n l) ≤ n := by simp [Nat.min_le_left]
+theorem length_take_le (i) (l : List α) : length (take i l) ≤ i := by simp [Nat.min_le_left]
 
-theorem length_take_le' (n) (l : List α) : length (take n l) ≤ l.length :=
+theorem length_take_le' (i) (l : List α) : length (take i l) ≤ l.length :=
   by simp [Nat.min_le_right]
 
-theorem length_take_of_le (h : n ≤ length l) : length (take n l) = n := by simp [Nat.min_eq_left h]
+theorem length_take_of_le (h : i ≤ length l) : length (take i l) = i := by simp [Nat.min_eq_left h]
 
 /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
 length `> i`. Version designed to rewrite from the big list to the small list. -/
@@ -47,30 +47,30 @@ length `> i`. Version designed to rewrite from the small list to the big list. -
     L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
   rw [length_take, Nat.lt_min] at h; rw [getElem_take' L _ h.1]
 
-theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
-    (l.take n)[m]? = none :=
+theorem getElem?_take_eq_none {l : List α} {i j : Nat} (h : i ≤ j) :
+    (l.take i)[j]? = none :=
   getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
 
-theorem getElem?_take {l : List α} {n m : Nat} :
-    (l.take n)[m]? = if m < n then l[m]? else none := by
+theorem getElem?_take {l : List α} {i j : Nat} :
+    (l.take i)[j]? = if j < i then l[j]? else none := by
   split
   · next h => exact getElem?_take_of_lt h
   · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h)
 
-theorem head?_take {l : List α} {n : Nat} :
-    (l.take n).head? = if n = 0 then none else l.head? := by
+theorem head?_take {l : List α} {i : Nat} :
+    (l.take i).head? = if i = 0 then none else l.head? := by
   simp [head?_eq_getElem?, getElem?_take]
   split
   · rw [if_neg (by omega)]
   · rw [if_pos (by omega)]
 
-theorem head_take {l : List α} {n : Nat} (h : l.take n ≠ []) :
-    (l.take n).head h = l.head (by simp_all) := by
+theorem head_take {l : List α} {i : Nat} (h : l.take i ≠ []) :
+    (l.take i).head h = l.head (by simp_all) := by
   apply Option.some_inj.1
   rw [← head?_eq_head, ← head?_eq_head, head?_take, if_neg]
   simp_all
 
-theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none else l[n - 1]?.or l.getLast? := by
+theorem getLast?_take {l : List α} : (l.take i).getLast? = if i = 0 then none else l[i - 1]?.or l.getLast? := by
   rw [getLast?_eq_getElem?, getElem?_take, length_take]
   split
   · rw [if_neg (by omega)]
@@ -83,8 +83,8 @@ theorem getLast?_take {l : List α} : (l.take n).getLast? = if n = 0 then none e
   · rw [if_pos]
     omega
 
-theorem getLast_take {l : List α} (h : l.take n ≠ []) :
-    (l.take n).getLast h = l[n - 1]?.getD (l.getLast (by simp_all)) := by
+theorem getLast_take {l : List α} (h : l.take i ≠ []) :
+    (l.take i).getLast h = l[i - 1]?.getD (l.getLast (by simp_all)) := by
   rw [getLast_eq_getElem, getElem_take]
   simp [length_take, Nat.min_def]
   simp at h
@@ -94,15 +94,15 @@ theorem getLast_take {l : List α} (h : l.take n ≠ []) :
   · rw [getElem?_eq_none (by omega), getLast_eq_getElem]
     simp
 
-theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m) l
+theorem take_take : ∀ (i j) (l : List α), take i (take j l) = take (min i j) l
   | n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
   | 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
   | succ n, succ m, nil => by simp only [take_nil]
   | succ n, succ m, a :: l => by
     simp only [take, succ_min_succ, take_take n m l]
 
-theorem take_set_of_le (a : α) {n m : Nat} (l : List α) (h : m ≤ n) :
-    (l.set n a).take m = l.take m :=
+theorem take_set_of_le (a : α) {i j : Nat} (l : List α) (h : j ≤ i) :
+    (l.set i a).take j = l.take j :=
   List.ext_getElem? fun i => by
     rw [getElem?_take, getElem?_take]
     split
@@ -112,31 +112,31 @@ theorem take_set_of_le (a : α) {n m : Nat} (l : List α) (h : m ≤ n) :
 @[deprecated take_set_of_le (since := "2025-02-04")]
 abbrev take_set_of_lt := @take_set_of_le
 
-@[simp] theorem take_replicate (a : α) : ∀ n m : Nat, take n (replicate m a) = replicate (min n m) a
+@[simp] theorem take_replicate (a : α) : ∀ i j : Nat, take i (replicate j a) = replicate (min i j) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
   | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]
 
-@[simp] theorem drop_replicate (a : α) : ∀ n m : Nat, drop n (replicate m a) = replicate (m - n) a
+@[simp] theorem drop_replicate (a : α) : ∀ i j : Nat, drop i (replicate j a) = replicate (j - i) a
   | n, 0 => by simp
   | 0, m => by simp
   | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]
 
-/-- Taking the first `n` elements in `l₁ ++ l₂` is the same as appending the first `n` elements
+/-- Taking the first `i` elements in `l₁ ++ l₂` is the same as appending the first `i` elements
 of `l₁` to the first `n - l₁.length` elements of `l₂`. -/
-theorem take_append_eq_append_take {l₁ l₂ : List α} {n : Nat} :
-    take n (l₁ ++ l₂) = take n l₁ ++ take (n - l₁.length) l₂ := by
-  induction l₁ generalizing n
+theorem take_append_eq_append_take {l₁ l₂ : List α} {i : Nat} :
+    take i (l₁ ++ l₂) = take i l₁ ++ take (i - l₁.length) l₂ := by
+  induction l₁ generalizing i
   · simp
-  · cases n
+  · cases i
     · simp [*]
     · simp only [cons_append, take_succ_cons, length_cons, succ_eq_add_one, cons.injEq,
         append_cancel_left_eq, true_and, *]
       congr 1
       omega
 
-theorem take_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
-    (l₁ ++ l₂).take n = l₁.take n := by
+theorem take_append_of_le_length {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) :
+    (l₁ ++ l₂).take i = l₁.take i := by
   simp [take_append_eq_append_take, Nat.sub_eq_zero_of_le h]
 
 /-- Taking the first `l₁.length + i` elements in `l₁ ++ l₂` is the same as appending the first
@@ -147,33 +147,33 @@ theorem take_append {l₁ l₂ : List α} (i : Nat) :
 
 @[simp]
 theorem take_eq_take :
-    ∀ {l : List α} {m n : Nat}, l.take m = l.take n ↔ min m l.length = min n l.length
-  | [], m, n => by simp [Nat.min_zero]
+    ∀ {l : List α} {i j : Nat}, l.take i = l.take j ↔ min i l.length = min j l.length
+  | [], i, j => by simp [Nat.min_zero]
   | _ :: xs, 0, 0 => by simp
-  | x :: xs, m + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
-  | x :: xs, 0, n + 1 => by simp [Nat.zero_min, succ_min_succ]
-  | x :: xs, m + 1, n + 1 => by simp [succ_min_succ, take_eq_take]
+  | x :: xs, i + 1, 0 => by simp [Nat.zero_min, succ_min_succ]
+  | x :: xs, 0, j + 1 => by simp [Nat.zero_min, succ_min_succ]
+  | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, take_eq_take]
 
-theorem take_add (l : List α) (m n : Nat) : l.take (m + n) = l.take m ++ (l.drop m).take n := by
-  suffices take (m + n) (take m l ++ drop m l) = take m l ++ take n (drop m l) by
+theorem take_add (l : List α) (i j : Nat) : l.take (i + j) = l.take i ++ (l.drop i).take j := by
+  suffices take (i + j) (take i l ++ drop i l) = take i l ++ take j (drop i l) by
     rw [take_append_drop] at this
     assumption
   rw [take_append_eq_append_take, take_of_length_le, append_right_inj]
   · simp only [take_eq_take, length_take, length_drop]
     omega
-  apply Nat.le_trans (m := m)
+  apply Nat.le_trans (m := i)
   · apply length_take_le
   · apply Nat.le_add_right
 
 theorem take_one {l : List α} : l.take 1 = l.head?.toList := by
   induction l <;> simp
 
-theorem take_eq_append_getElem_of_pos {n} {l : List α} (h₁ : 0 < n) (h₂ : n < l.length) : l.take n = l.take (n - 1) ++ [l[n - 1]] :=
-  match n, h₁ with
-  | n + 1, _ => take_succ_eq_append_getElem (n := n) (by omega)
+theorem take_eq_append_getElem_of_pos {i} {l : List α} (h₁ : 0 < i) (h₂ : i < l.length) : l.take i = l.take (i - 1) ++ [l[i - 1]] :=
+  match i, h₁ with
+  | i + 1, _ => take_succ_eq_append_getElem (n := i) (by omega)
 
-theorem dropLast_take {n : Nat} {l : List α} (h : n < l.length) :
-    (l.take n).dropLast = l.take (n - 1) := by
+theorem dropLast_take {i : Nat} {l : List α} (h : i < l.length) :
+    (l.take i).dropLast = l.take (i - 1) := by
   simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]
 
 @[deprecated map_eq_append_iff (since := "2024-09-05")] abbrev map_eq_append_split := @map_eq_append_iff
@@ -192,17 +192,17 @@ theorem take_eq_dropLast {l : List α} {i : Nat} (h : i + 1 = l.length) :
         rw [ih]
         simpa using h
 
-theorem take_prefix_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l <+: take n l := by
+theorem take_prefix_take_left (l : List α) {i j : Nat} (h : i ≤ j) : take i l <+: take j l := by
   rw [isPrefix_iff]
   intro i w
   rw [getElem?_take_of_lt, getElem_take, getElem?_eq_getElem]
   simp only [length_take] at w
   exact Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le w (Nat.min_le_left _ _)) h
 
-theorem take_sublist_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l <+ take n l :=
+theorem take_sublist_take_left (l : List α) {i j : Nat} (h : i ≤ j) : take i l <+ take j l :=
   (take_prefix_take_left l h).sublist
 
-theorem take_subset_take_left (l : List α) {m n : Nat} (h : m ≤ n) : take m l ⊆ take n l :=
+theorem take_subset_take_left (l : List α) {i j : Nat} (h : i ≤ j) : take i l ⊆ take j l :=
   (take_sublist_take_left l h).subset
 
 /-! ### drop -/
@@ -242,17 +242,17 @@ theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? :=
     apply Nat.lt_sub_of_add_lt h
 
 theorem mem_take_iff_getElem {l : List α} {a : α} :
-    a ∈ l.take n ↔ ∃ (i : Nat) (hm : i < min n l.length), l[i] = a := by
+    a ∈ l.take i ↔ ∃ (j : Nat) (hm : j < min i l.length), l[j] = a := by
   rw [mem_iff_getElem]
   constructor
-  · rintro ⟨i, hm, rfl⟩
+  · rintro ⟨j, hm, rfl⟩
     simp at hm
-    refine ⟨i, by omega, by rw [getElem_take]⟩
-  · rintro ⟨i, hm, rfl⟩
-    refine ⟨i, by simpa, by rw [getElem_take]⟩
+    refine ⟨j, by omega, by rw [getElem_take]⟩
+  · rintro ⟨j, hm, rfl⟩
+    refine ⟨j, by simpa, by rw [getElem_take]⟩
 
 theorem mem_drop_iff_getElem {l : List α} {a : α} :
-    a ∈ l.drop n ↔ ∃ (i : Nat) (hm : i + n < l.length), l[n + i] = a := by
+    a ∈ l.drop i ↔ ∃ (j : Nat) (hm : j + i < l.length), l[i + j] = a := by
   rw [mem_iff_getElem]
   constructor
   · rintro ⟨i, hm, rfl⟩
@@ -261,16 +261,16 @@ theorem mem_drop_iff_getElem {l : List α} {a : α} :
   · rintro ⟨i, hm, rfl⟩
     refine ⟨i, by simp; omega, by rw [getElem_drop]⟩
 
-@[simp] theorem head?_drop (l : List α) (n : Nat) :
-    (l.drop n).head? = l[n]? := by
+@[simp] theorem head?_drop (l : List α) (i : Nat) :
+    (l.drop i).head? = l[i]? := by
   rw [head?_eq_getElem?, getElem?_drop, Nat.add_zero]
 
-@[simp] theorem head_drop {l : List α} {n : Nat} (h : l.drop n ≠ []) :
-    (l.drop n).head h = l[n]'(by simp_all) := by
-  have w : n < l.length := length_lt_of_drop_ne_nil h
+@[simp] theorem head_drop {l : List α} {i : Nat} (h : l.drop i ≠ []) :
+    (l.drop i).head h = l[i]'(by simp_all) := by
+  have w : i < l.length := length_lt_of_drop_ne_nil h
   simp [getElem?_eq_getElem, h, w, head_eq_iff_head?_eq_some]
 
-theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n then none else l.getLast? := by
+theorem getLast?_drop {l : List α} : (l.drop i).getLast? = if l.length ≤ i then none else l.getLast? := by
   rw [getLast?_eq_getElem?, getElem?_drop]
   rw [length_drop]
   split
@@ -279,8 +279,8 @@ theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n th
     congr
     omega
 
-@[simp] theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
-    (l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
+@[simp] theorem getLast_drop {l : List α} (h : l.drop i ≠ []) :
+    (l.drop i).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
   simp only [ne_eq, drop_eq_nil_iff] at h
   apply Option.some_inj.1
   simp only [← getLast?_eq_getLast, getLast?_drop, ite_eq_right_iff]
@@ -298,20 +298,20 @@ theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
     rw [getLast_cons h₁]
     exact ih h₁ y
 
-/-- Dropping the elements up to `n` in `l₁ ++ l₂` is the same as dropping the elements up to `n`
-in `l₁`, dropping the elements up to `n - l₁.length` in `l₂`, and appending them. -/
-theorem drop_append_eq_append_drop {l₁ l₂ : List α} {n : Nat} :
-    drop n (l₁ ++ l₂) = drop n l₁ ++ drop (n - l₁.length) l₂ := by
-  induction l₁ generalizing n
+/-- Dropping the elements up to `i` in `l₁ ++ l₂` is the same as dropping the elements up to `i`
+in `l₁`, dropping the elements up to `i - l₁.length` in `l₂`, and appending them. -/
+theorem drop_append_eq_append_drop {l₁ l₂ : List α} {i : Nat} :
+    drop i (l₁ ++ l₂) = drop i l₁ ++ drop (i - l₁.length) l₂ := by
+  induction l₁ generalizing i
   · simp
-  · cases n
+  · cases i
     · simp [*]
     · simp only [cons_append, drop_succ_cons, length_cons, succ_eq_add_one, append_cancel_left_eq, *]
       congr 1
       omega
 
-theorem drop_append_of_le_length {l₁ l₂ : List α} {n : Nat} (h : n ≤ l₁.length) :
-    (l₁ ++ l₂).drop n = l₁.drop n ++ l₂ := by
+theorem drop_append_of_le_length {l₁ l₂ : List α} {i : Nat} (h : i ≤ l₁.length) :
+    (l₁ ++ l₂).drop i = l₁.drop i ++ l₂ := by
   simp [drop_append_eq_append_drop, Nat.sub_eq_zero_of_le h]
 
 /-- Dropping the elements up to `l₁.length + i` in `l₁ + l₂` is the same as dropping the elements
@@ -321,24 +321,24 @@ theorem drop_append {l₁ l₂ : List α} (i : Nat) : drop (l₁.length + i) (l
   rw [drop_append_eq_append_drop, drop_eq_nil_of_le] <;>
     simp [Nat.add_sub_cancel_left, Nat.le_add_right]
 
-theorem set_eq_take_append_cons_drop (l : List α) (n : Nat) (a : α) :
-    l.set n a = if n < l.length then l.take n ++ a :: l.drop (n + 1) else l := by
+theorem set_eq_take_append_cons_drop (l : List α) (i : Nat) (a : α) :
+    l.set i a = if i < l.length then l.take i ++ a :: l.drop (i + 1) else l := by
   split <;> rename_i h
-  · ext1 m
-    by_cases h' : m < n
+  · ext1 j
+    by_cases h' : j < i
     · rw [getElem?_append_left (by simp [length_take]; omega), getElem?_set_ne (by omega),
         getElem?_take_of_lt h']
-    · by_cases h'' : m = n
+    · by_cases h'' : j = i
       · subst h''
         rw [getElem?_set_self ‹_›, getElem?_append_right, length_take,
           Nat.min_eq_left (by omega), Nat.sub_self, getElem?_cons_zero]
         rw [length_take]
-        exact Nat.min_le_left m l.length
-      · have h''' : n < m := by omega
+        exact Nat.min_le_left j l.length
+      · have h''' : i < j := by omega
         rw [getElem?_set_ne (by omega), getElem?_append_right, length_take,
           Nat.min_eq_left (by omega)]
         · obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt h'''
-          have p : n + k + 1 - n = k + 1 := by omega
+          have p : i + k + 1 - i = k + 1 := by omega
           rw [p]
           rw [getElem?_cons_succ, getElem?_drop]
           congr 1
@@ -348,39 +348,39 @@ theorem set_eq_take_append_cons_drop (l : List α) (n : Nat) (a : α) :
   · rw [set_eq_of_length_le]
     omega
 
-theorem exists_of_set {n : Nat} {a' : α} {l : List α} (h : n < l.length) :
-    ∃ l₁ l₂, l = l₁ ++ l[n] :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := by
-  refine ⟨l.take n, l.drop (n + 1), ⟨by simp, ⟨length_take_of_le (Nat.le_of_lt h), ?_⟩⟩⟩
+theorem exists_of_set {i : Nat} {a' : α} {l : List α} (h : i < l.length) :
+    ∃ l₁ l₂, l = l₁ ++ l[i] :: l₂ ∧ l₁.length = i ∧ l.set i a' = l₁ ++ a' :: l₂ := by
+  refine ⟨l.take i, l.drop (i + 1), ⟨by simp, ⟨length_take_of_le (Nat.le_of_lt h), ?_⟩⟩⟩
   simp [set_eq_take_append_cons_drop, h]
 
-theorem drop_set_of_lt (a : α) {n m : Nat} (l : List α)
-    (hnm : n < m) : drop m (l.set n a) = l.drop m :=
+theorem drop_set_of_lt (a : α) {i j : Nat} (l : List α)
+    (hnm : i < j) : drop j (l.set i a) = l.drop j :=
   ext_getElem? fun k => by simpa only [getElem?_drop] using getElem?_set_ne (by omega)
 
-theorem drop_take : ∀ (m n : Nat) (l : List α), drop n (take m l) = take (m - n) (drop n l)
+theorem drop_take : ∀ (i j : Nat) (l : List α), drop i (take j l) = take (j - i) (drop i l)
   | 0, _, _ => by simp
   | _, 0, _ => by simp
   | _, _, [] => by simp
-  | m+1, n+1, h :: t => by
-    simp [take_succ_cons, drop_succ_cons, drop_take m n t]
+  | i+1, j+1, h :: t => by
+    simp [take_succ_cons, drop_succ_cons, drop_take i j t]
     congr 1
     omega
 
-@[simp] theorem drop_take_self : drop n (take n l) = [] := by
+@[simp] theorem drop_take_self : drop i (take i l) = [] := by
   rw [drop_take]
   simp
 
-theorem take_reverse {α} {xs : List α} {n : Nat} :
-    xs.reverse.take n = (xs.drop (xs.length - n)).reverse := by
-  by_cases h : n ≤ xs.length
-  · induction xs generalizing n <;>
+theorem take_reverse {α} {xs : List α} {i : Nat} :
+    xs.reverse.take i = (xs.drop (xs.length - i)).reverse := by
+  by_cases h : i ≤ xs.length
+  · induction xs generalizing i <;>
       simp only [reverse_cons, drop, reverse_nil, Nat.zero_sub, length, take_nil]
     next xs_hd xs_tl xs_ih =>
     cases Nat.lt_or_eq_of_le h with
     | inl h' =>
       have h' := Nat.le_of_succ_le_succ h'
       rw [take_append_of_le_length, xs_ih h']
-      rw [show xs_tl.length + 1 - n = succ (xs_tl.length - n) from _, drop]
+      rw [show xs_tl.length + 1 - i = succ (xs_tl.length - i) from _, drop]
       · rwa [succ_eq_add_one, Nat.sub_add_comm]
       · rwa [length_reverse]
     | inr h' =>
@@ -390,14 +390,14 @@ theorem take_reverse {α} {xs : List α} {n : Nat} :
         rw [this, take_length, reverse_cons]
       rw [length_append, length_reverse]
       rfl
-  · have w : xs.length - n = 0 := by omega
+  · have w : xs.length - i = 0 := by omega
     rw [take_of_length_le, w, drop_zero]
     simp
     omega
 
-theorem drop_reverse {α} {xs : List α} {n : Nat} :
-    xs.reverse.drop n = (xs.take (xs.length - n)).reverse := by
-  by_cases h : n ≤ xs.length
+theorem drop_reverse {α} {xs : List α} {i : Nat} :
+    xs.reverse.drop i = (xs.take (xs.length - i)).reverse := by
+  by_cases h : i ≤ xs.length
   · conv =>
       rhs
       rw [← reverse_reverse xs]
@@ -407,47 +407,47 @@ theorem drop_reverse {α} {xs : List α} {n : Nat} :
     · simp only [length_reverse, reverse_reverse] at *
       congr
       omega
-  · have w : xs.length - n = 0 := by omega
+  · have w : xs.length - i = 0 := by omega
     rw [drop_of_length_le, w, take_zero, reverse_nil]
     simp
     omega
 
-theorem reverse_take {l : List α} {n : Nat} :
-    (l.take n).reverse = l.reverse.drop (l.length - n) := by
-  by_cases h : n ≤ l.length
+theorem reverse_take {l : List α} {i : Nat} :
+    (l.take i).reverse = l.reverse.drop (l.length - i) := by
+  by_cases h : i ≤ l.length
   · rw [drop_reverse]
     congr
     omega
-  · have w : l.length - n = 0 := by omega
+  · have w : l.length - i = 0 := by omega
     rw [w, drop_zero, take_of_length_le]
     omega
 
-theorem reverse_drop {l : List α} {n : Nat} :
-    (l.drop n).reverse = l.reverse.take (l.length - n) := by
-  by_cases h : n ≤ l.length
+theorem reverse_drop {l : List α} {i : Nat} :
+    (l.drop i).reverse = l.reverse.take (l.length - i) := by
+  by_cases h : i ≤ l.length
   · rw [take_reverse]
     congr
     omega
-  · have w : l.length - n = 0 := by omega
+  · have w : l.length - i = 0 := by omega
     rw [w, take_zero, drop_of_length_le, reverse_nil]
     omega
 
-theorem take_add_one {l : List α} {n : Nat} :
-    l.take (n + 1) = l.take n ++ l[n]?.toList := by
+theorem take_add_one {l : List α} {i : Nat} :
+    l.take (i + 1) = l.take i ++ l[i]?.toList := by
   simp [take_add, take_one]
 
-theorem drop_eq_getElem?_toList_append {l : List α} {n : Nat} :
-    l.drop n = l[n]?.toList ++ l.drop (n + 1) := by
-  induction l generalizing n with
+theorem drop_eq_getElem?_toList_append {l : List α} {i : Nat} :
+    l.drop i = l[i]?.toList ++ l.drop (i + 1) := by
+  induction l generalizing i with
   | nil => simp
   | cons hd tl ih =>
-    cases n
+    cases i
     · simp
     · simp only [drop_succ_cons, getElem?_cons_succ]
       rw [ih]
 
-theorem drop_sub_one {l : List α} {n : Nat} (h : 0 < n) :
-    l.drop (n - 1) = l[n - 1]?.toList ++ l.drop n := by
+theorem drop_sub_one {l : List α} {i : Nat} (h : 0 < i) :
+    l.drop (i - 1) = l[i - 1]?.toList ++ l.drop i := by
   rw [drop_eq_getElem?_toList_append]
   congr
   omega
@@ -460,24 +460,24 @@ theorem false_of_mem_take_findIdx {xs : List α} {p : α → Bool} (h : x ∈ xs
   obtain ⟨i, h, rfl⟩ := h
   exact not_of_lt_findIdx (by omega)
 
-@[simp] theorem findIdx_take {xs : List α} {n : Nat} {p : α → Bool} :
-    (xs.take n).findIdx p = min n (xs.findIdx p) := by
-  induction xs generalizing n with
+@[simp] theorem findIdx_take {xs : List α} {i : Nat} {p : α → Bool} :
+    (xs.take i).findIdx p = min i (xs.findIdx p) := by
+  induction xs generalizing i with
   | nil => simp
   | cons x xs ih =>
-    cases n
+    cases i
     · simp
     · simp only [take_succ_cons, findIdx_cons, ih, cond_eq_if]
       split
       · simp
       · rw [Nat.add_min_add_right]
 
-@[simp] theorem findIdx?_take {xs : List α} {n : Nat} {p : α → Bool} :
-    (xs.take n).findIdx? p = (xs.findIdx? p).bind (Option.guard (fun i => i < n)) := by
-  induction xs generalizing n with
+@[simp] theorem findIdx?_take {xs : List α} {i : Nat} {p : α → Bool} :
+    (xs.take i).findIdx? p = (xs.findIdx? p).bind (Option.guard (fun j => j < i)) := by
+  induction xs generalizing i with
   | nil => simp
   | cons x xs ih =>
-    cases n
+    cases i
     · simp
     · simp only [take_succ_cons, findIdx?_cons]
       split

src/Init/Data/List/ToArray.lean

@@ -573,9 +573,9 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
     rw [List.drop_set_of_lt _ _ (by omega)]
     rw [List.getElem_set_ne (by omega)]
     rw [List.getElem_set_self]
-    rw [List.take_set_of_le (m := j - 1) _ _ (by omega)]
-    rw [List.take_set_of_le (m := j - 1) _ _ (by omega)]
-    rw [List.take_eq_append_getElem_of_pos (n := j) (l := l) (by omega) hj]
+    rw [List.take_set_of_le (j := j - 1) _ _ (by omega)]
+    rw [List.take_set_of_le (j := j - 1) _ _ (by omega)]
+    rw [List.take_eq_append_getElem_of_pos (i := j) (l := l) (by omega) hj]
     rw [List.drop_append_of_le_length (by simp; omega)]
     simp only [append_assoc, cons_append, nil_append, append_cancel_right_eq]
     cases i with

src/Lean/Linter.lean

@@ -11,3 +11,4 @@ import Lean.Linter.Deprecated
 import Lean.Linter.UnusedVariables
 import Lean.Linter.MissingDocs
 import Lean.Linter.Omit
+import Lean.Linter.List

src/Lean/Linter/List.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Lean.Elab.Command
+import Lean.Server.InfoUtils
+set_option linter.missingDocs true -- keep it documented
+
+/-!
+This file defines style linters for the `List`/`Array`/`Vector` modules.
+
+Currently, we do not anticipate that they will be useful elsewhere.
+-/
+
+namespace Lean.Linter.List
+
+/--
+`set_option linter.indexVariables true` enables a strict linter that
+validates that the only variables appearing as an index (e.g. in `xs[i]` or `xs.take i`)
+are `i`, `j`, or `k`.
+-/
+register_builtin_option linter.indexVariables : Bool := {
+  defValue := false
+  descr := "Validate that variables appearing as an index (e.g. in `xs[i]` or `xs.take i`) are only `i`, `j`, or `k`."
+}
+
+open Lean Elab Command
+
+/--
+Return the syntax for all expressions in which an `fvarId` appears as a "numerical index", along with the user name of that `fvarId`.
+-/
+partial def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
+  t.deepestNodes fun _ info _ => do
+    let stx := info.stx
+    if let .ofTermInfo info := info then
+      let idx? := match_expr info.expr with
+      | GetElem.getElem _ _ _ _ _ _ i _ => some i
+      | GetElem?.getElem? _ _ _ _ _ _ i => some i
+      | List.take _ i _ => some i
+      | List.drop _ i _ => some i
+      | List.set _ _ i _ => some i
+      | List.insertIdx _ i _ _ => some i
+      | List.eraseIdx _ _ i _ => some i
+      | _ => none
+      match idx? with
+      | some (.fvar i) =>
+        match info.lctx.find? i with
+        | some ldecl => some (stx, ldecl.userName)
+        | none => none
+      | _ => none
+    else
+      none
+
+/--
+A linter which validates that the only variables used as "indices" (e.g. in `xs[i]` or `xs.take i`)
+are `i`, `j`, or `k`.
+-/
+def indexLinter : Linter
+  where run := withSetOptionIn fun stx => do
+    unless Linter.getLinterValue linter.indexVariables (← getOptions) do return
+    if (← get).messages.hasErrors then return
+    if ! (← getInfoState).enabled then return
+    for t in ← getInfoTrees do
+      if let .context _ _ := t then -- Only consider info trees with top-level context
+      for (idxStx, n) in numericalIndices t do
+        if n != `i && n != `j && n != `k then
+          Linter.logLint linter.indexVariables idxStx
+            m!"Forbidden variable appearing as an index: use `i`, `j`, or `k`: {n}"
+
+builtin_initialize addLinter indexLinter
+
+end Lean.Linter.List

src/Std/Time/Zoned/ZonedDateTime.lean

@@ -10,7 +10,8 @@ import Std.Time.Zoned.ZoneRules
 namespace Std
 namespace Time
 
-set_option linter.all true
+-- TODO (@kim-em): re-enable this once there is a mechanism to exclude `linter.indexVariables`.
+-- set_option linter.all true
 
 /--
 Represents a date and time with timezone information.

tests/lean/run/index_variables_linter.lean

@@ -0,0 +1,46 @@
+set_option linter.indexVariables true
+
+#guard_msgs in
+example (xs : List Nat) (i : Nat) (h) : xs[i] = xs[i] := rfl
+
+/--
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+note: this linter can be disabled with `set_option linter.indexVariables false`
+---
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+note: this linter can be disabled with `set_option linter.indexVariables false`
+-/
+#guard_msgs in
+example (xs : List Nat) (m : Nat) (h) : xs[m] = xs[m] := rfl
+
+#guard_msgs in
+example (xs : List Nat) (i j : Nat) (h) : xs[i + j] = xs[i + j] := rfl
+
+#guard_msgs in
+example (xs : List Nat) (m n : Nat) (h) : xs[m + n] = xs[m + n] := rfl
+
+#guard_msgs in
+example (xs : List Nat) (i : Nat) : xs[i]? = xs[i]? := rfl
+
+/--
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+note: this linter can be disabled with `set_option linter.indexVariables false`
+---
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+note: this linter can be disabled with `set_option linter.indexVariables false`
+-/
+#guard_msgs in
+example (xs : List Nat) (m : Nat) : xs[m]? = xs[m]? := rfl
+
+#guard_msgs in
+example (xs : List Nat) (i : Nat) : xs.take i = xs.take i := rfl
+
+/--
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+note: this linter can be disabled with `set_option linter.indexVariables false`
+---
+warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
+note: this linter can be disabled with `set_option linter.indexVariables false`
+-/
+#guard_msgs in
+example (xs : List Nat) (m : Nat) : xs.drop m = xs.drop m := rfl