chore: linting variable names for List (#7107)

src/Init/Data/List/Attach.lean

@@ -8,6 +8,9 @@ import Init.Data.List.Count
 import Init.Data.Subtype
 import Init.BinderNameHint
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
@@ -40,12 +43,12 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     List β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
 
 @[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
-  funext α β p f L h'
-  let rec go : ∀ L' (hL' : ∀ ⦃x⦄, x ∈ L' → p x),
-      pmap f L' hL' = map (fun ⟨x, hx⟩ => f x hx) (pmap Subtype.mk L' hL')
+  funext α β p f l h'
+  let rec go : ∀ l' (hL' : ∀ ⦃x⦄, x ∈ l' → p x),
+      pmap f l' hL' = map (fun ⟨x, hx⟩ => f x hx) (pmap Subtype.mk l' hL')
   | nil, hL' => rfl
-  | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
-  exact go L h'
+  | cons _ l', hL' => congrArg _ <| go l' fun _ hx => hL' (.tail _ hx)
+  exact go l h'
 
 @[simp] theorem pmap_nil {P : α → Prop} (f : ∀ a, P a → β) : pmap f [] (by simp) = [] := rfl
 
@@ -179,7 +182,7 @@ theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l
   · simp only [*, pmap, length]
 
 @[simp]
-theorem length_attach {L : List α} : L.attach.length = L.length :=
+theorem length_attach {l : List α} : l.attach.length = l.length :=
   length_pmap
 
 @[simp]
@@ -223,12 +226,12 @@ theorem attachWith_ne_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l,
 @[deprecated attach_ne_nil_iff (since := "2024-09-06")] abbrev attach_ne_nil := @attach_ne_nil_iff
 
 @[simp]
-theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
-  induction l generalizing n with
+theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (i : Nat) :
+    (pmap f l h)[i]? = Option.pmap f l[i]? fun x H => h x (mem_of_getElem? H) := by
+  induction l generalizing i with
   | nil => simp
   | cons hd tl hl =>
-    rcases n with ⟨n⟩
+    rcases i with ⟨i⟩
     · simp only [Option.pmap]
       split <;> simp_all
     · simp only [hl, pmap, Option.pmap, getElem?_cons_succ]
@@ -247,17 +250,17 @@ theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h :
   simp [getElem?_pmap, h]
 
 @[simp]
-theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
-    (hn : n < (pmap f l h).length) :
-    (pmap f l h)[n] =
-      f (l[n]'(@length_pmap _ _ p f l h ▸ hn))
+theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {i : Nat}
+    (hn : i < (pmap f l h).length) :
+    (pmap f l h)[i] =
+      f (l[i]'(@length_pmap _ _ p f l h ▸ hn))
         (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn))) := by
-  induction l generalizing n with
+  induction l generalizing i with
   | nil =>
     simp only [length, pmap] at hn
-    exact absurd hn (Nat.not_lt_of_le n.zero_le)
+    exact absurd hn (Nat.not_lt_of_le i.zero_le)
   | cons hd tl hl =>
-    cases n
+    cases i
     · simp
     · simp [hl]
 

src/Init/Data/List/Basic.lean

@@ -58,6 +58,8 @@ Further operations are defined in `Init.Data.List.BasicAux`
 -/
 
 set_option linter.missingDocs true -- keep it documented
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Decidable List
 
@@ -204,7 +206,7 @@ instance decidableLT [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List
 abbrev hasDecidableLt := @decidableLT
 
 /-- The lexicographic order on lists. -/
-@[reducible] protected def le [LT α] (a b : List α) : Prop := ¬ b < a
+@[reducible] protected def le [LT α] (as bs : List α) : Prop := ¬ bs < as
 
 instance instLE [LT α] : LE (List α) := ⟨List.le⟩
 
@@ -355,14 +357,15 @@ def tail? : List α → Option (List α)
 
 /-! ### tailD -/
 
+set_option linter.listVariables false in
 /--
 Drops the first element of the list.
 
 If the list is empty, this function returns `fallback`.
 Also see `head?` and `head!`.
 -/
-def tailD (list fallback : List α) : List α :=
-  match list with
+def tailD (l fallback : List α) : List α :=
+  match l with
   | [] => fallback
   | _ :: tl => tl
 
@@ -554,10 +557,10 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
 -/
 def flatten : List (List α) → List α
   | []      => []
-  | a :: as => a ++ flatten as
+  | l :: L => l ++ flatten L
 
 @[simp] theorem flatten_nil : List.flatten ([] : List (List α)) = [] := rfl
-@[simp] theorem flatten_cons : (l :: ls).flatten = l ++ ls.flatten := rfl
+@[simp] theorem flatten_cons : (l :: L).flatten = l ++ L.flatten := rfl
 
 @[deprecated flatten (since := "2024-10-14"), inherit_doc flatten] abbrev join := @flatten
 
@@ -576,7 +579,7 @@ set_option linter.missingDocs false in
 to get a list of lists, and then concatenates them all together.
 * `[2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]`
 -/
-@[inline] def flatMap {α : Type u} {β : Type v} (b : α → List β) (a : List α) : List β := flatten (map b a)
+@[inline] def flatMap {α : Type u} {β : Type v} (b : α → List β) (as : List α) : List β := flatten (map b as)
 
 @[simp] theorem flatMap_nil (f : α → List β) : List.flatMap f [] = [] := by simp [flatten, List.flatMap]
 @[simp] theorem flatMap_cons x xs (f : α → List β) :
@@ -781,14 +784,14 @@ def take : Nat → List α → List α
 * `drop 6 [a, b, c, d, e] = []`
 -/
 def drop : Nat → List α → List α
-  | 0,   a     => a
+  | 0,   as     => as
   | _+1, []    => []
   | n+1, _::as => drop n as
 
 @[simp] theorem drop_nil : ([] : List α).drop i = [] := by
   cases i <;> rfl
 @[simp] theorem drop_zero (l : List α) : l.drop 0 = l := rfl
-@[simp] theorem drop_succ_cons : (a :: l).drop (n + 1) = l.drop n := rfl
+@[simp] theorem drop_succ_cons : (a :: l).drop (i + 1) = l.drop i := rfl
 
 theorem drop_eq_nil_of_le {as : List α} {i : Nat} (h : as.length ≤ i) : as.drop i = [] := by
   match as, i with
@@ -1022,15 +1025,15 @@ def splitAt (n : Nat) (l : List α) : List α × List α := go l n [] where
 * `rotateLeft [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
 * `rotateLeft [1, 2, 3, 4, 5] = [2, 3, 4, 5, 1]`
 -/
-def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
+def rotateLeft (xs : List α) (i : Nat := 1) : List α :=
   let len := xs.length
   if len ≤ 1 then
     xs
   else
-    let n := n % len
-    let b := xs.take n
-    let e := xs.drop n
-    e ++ b
+    let i := i % len
+    let ys := xs.take i
+    let zs := xs.drop i
+    zs ++ ys
 
 @[simp] theorem rotateLeft_nil : ([] : List α).rotateLeft n = [] := rfl
 
@@ -1043,15 +1046,15 @@ def rotateLeft (xs : List α) (n : Nat := 1) : List α :=
 * `rotateRight [1, 2, 3, 4, 5] 5 = [1, 2, 3, 4, 5]`
 * `rotateRight [1, 2, 3, 4, 5] = [5, 1, 2, 3, 4]`
 -/
-def rotateRight (xs : List α) (n : Nat := 1) : List α :=
+def rotateRight (xs : List α) (i : Nat := 1) : List α :=
   let len := xs.length
   if len ≤ 1 then
     xs
   else
-    let n := len - n % len
-    let b := xs.take n
-    let e := xs.drop n
-    e ++ b
+    let i := len - i % len
+    let ys := xs.take i
+    let zs := xs.drop i
+    zs ++ ys
 
 @[simp] theorem rotateRight_nil : ([] : List α).rotateRight n = [] := rfl
 
@@ -1166,8 +1169,8 @@ def modify (f : α → α) : Nat → List α → List α :=
 insertIdx 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]
 ```
 -/
-def insertIdx (n : Nat) (a : α) : List α → List α :=
-  modifyTailIdx (cons a) n
+def insertIdx (i : Nat) (a : α) : List α → List α :=
+  modifyTailIdx (cons a) i
 
 /-! ### erase -/
 
@@ -1340,13 +1343,13 @@ and returns the first `β` value corresponding to an `α` value in the list equa
 -/
 def lookup [BEq α] : α → List (α × β) → Option β
   | _, []        => none
-  | a, (k,b)::es => match a == k with
+  | a, (k,b)::as => match a == k with
     | true  => some b
-    | false => lookup a es
+    | false => lookup a as
 
 @[simp] theorem lookup_nil [BEq α] : ([] : List (α × β)).lookup a = none := rfl
 theorem lookup_cons [BEq α] {k : α} :
-    ((k,b)::es).lookup a = match a == k with | true => some b | false => es.lookup a :=
+    ((k,b)::as).lookup a = match a == k with | true => some b | false => as.lookup a :=
   rfl
 
 /-! ## Permutations -/
@@ -1492,11 +1495,11 @@ def zipWithAll (f : Option α → Option β → γ) : List α → List β → Li
 -/
 def unzip : List (α × β) → List α × List β
   | []          => ([], [])
-  | (a, b) :: t => match unzip t with | (al, bl) => (a::al, b::bl)
+  | (a, b) :: t => match unzip t with | (as, bs) => (a::as, b::bs)
 
 @[simp] theorem unzip_nil : ([] : List (α × β)).unzip = ([], []) := rfl
 @[simp] theorem unzip_cons {h : α × β} :
-    (h :: t).unzip = match unzip t with | (al, bl) => (h.1::al, h.2::bl) := rfl
+    (h :: t).unzip = match unzip t with | (as, bs) => (h.1::as, h.2::bs) := rfl
 
 /-! ## Ranges and enumeration -/
 
@@ -1531,8 +1534,8 @@ def range (n : Nat) : List Nat :=
   loop n []
 where
   loop : Nat → List Nat → List Nat
-  | 0,   ns => ns
-  | n+1, ns => loop n (n::ns)
+  | 0,   acc => acc
+  | n+1, acc => loop n (n::acc)
 
 @[simp] theorem range_zero : range 0 = [] := rfl
 
@@ -1663,6 +1666,7 @@ def intersperse (sep : α) : List α → List α
 
 /-! ### intercalate -/
 
+set_option linter.listVariables false in
 /--
 `O(|xs|)`. `intercalate sep xs` alternates `sep` and the elements of `xs`:
 * `intercalate sep [] = []`
@@ -1699,10 +1703,10 @@ def eraseReps {α} [BEq α] : List α → List α
   | a::as => loop a as []
 where
   loop {α} [BEq α] : α → List α → List α → List α
-  | a, [], rs => (a::rs).reverse
-  | a, a'::as, rs => match a == a' with
-    | true  => loop a as rs
-    | false => loop a' as (a::rs)
+  | a, [], acc => (a::acc).reverse
+  | a, a'::as, acc => match a == a' with
+    | true  => loop a as acc
+    | false => loop a' as (a::acc)
 
 /-! ### span -/
 
@@ -1718,10 +1722,10 @@ and the second part is everything else.
   loop as []
 where
   @[specialize] loop : List α → List α → List α × List α
-  | [],    rs => (rs.reverse, [])
-  | a::as, rs => match p a with
-    | true  => loop as (a::rs)
-    | false => (rs.reverse, a::as)
+  | [],    acc => (acc.reverse, [])
+  | a::as, acc => match p a with
+    | true  => loop as (a::acc)
+    | false => (acc.reverse, a::as)
 
 /-! ### splitBy -/
 
@@ -1737,18 +1741,18 @@ such that adjacent elements are related by `R`.
   | a::as => loop as a [] []
 where
   /--
-  The arguments of `splitBy.loop l ag g gs` represent the following:
+  The arguments of `splitBy.loop l b g gs` represent the following:
 
   - `l : List α` are the elements which we still need to split.
-  - `ag : α` is the previous element for which a comparison was performed.
-  - `g : List α` is the group currently being assembled, in **reverse order**.
-  - `gs : List (List α)` is all of the groups that have been completed, in **reverse order**.
+  - `b : α` is the previous element for which a comparison was performed.
+  - `r : List α` is the group currently being assembled, in **reverse order**.
+  - `acc : List (List α)` is all of the groups that have been completed, in **reverse order**.
   -/
   @[specialize] loop : List α → α → List α → List (List α) → List (List α)
-  | a::as, ag, g, gs => match R ag a with
-    | true  => loop as a (ag::g) gs
-    | false => loop as a [] ((ag::g).reverse::gs)
-  | [], ag, g, gs => ((ag::g).reverse::gs).reverse
+  | a::as, b, r, acc => match R b a with
+    | true  => loop as a (b::r) acc
+    | false => loop as a [] ((b::r).reverse::acc)
+  | [], ag, r, acc => ((ag::r).reverse::acc).reverse
 
 @[deprecated splitBy (since := "2024-10-30"), inherit_doc splitBy] abbrev groupBy := @splitBy
 
@@ -1814,10 +1818,10 @@ theorem mapTR_loop_eq (f : α → β) (as : List α) (bs : List β) :
   loop as []
 where
   @[specialize] loop : List α → List α → List α
-  | [],    rs => rs.reverse
-  | a::as, rs => match p a with
-     | true  => loop as (a::rs)
-     | false => loop as rs
+  | [],    acc => acc.reverse
+  | a::as, acc => match p a with
+     | true  => loop as (a::acc)
+     | false => loop as acc
 
 theorem filterTR_loop_eq (p : α → Bool) (as bs : List α) :
     filterTR.loop p as bs = bs.reverse ++ filter p as := by
@@ -1873,7 +1877,7 @@ theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++
 
 /-- Tail recursive version of `List.unzip`. -/
 def unzipTR (l : List (α × β)) : List α × List β :=
-  l.foldr (fun (a, b) (al, bl) => (a::al, b::bl)) ([], [])
+  l.foldr (fun (a, b) (as, bs) => (a::as, b::bs)) ([], [])
 
 @[csimp] theorem unzip_eq_unzipTR : @unzip = @unzipTR := by
   apply funext; intro α; apply funext; intro β; apply funext; intro l

src/Init/Data/List/BasicAux.lean

@@ -6,6 +6,9 @@ Author: Leonardo de Moura
 prelude
 import Init.Data.Nat.Linear
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 universe u
 
 namespace List

src/Init/Data/List/Control.lean

@@ -9,6 +9,9 @@ import Init.Control.Id
 import Init.Control.Lawful
 import Init.Data.List.Basic
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 universe u v w u₁ u₂
 

src/Init/Data/List/Count.lean

@@ -10,6 +10,9 @@ import Init.Data.List.Sublist
 # Lemmas about `List.countP` and `List.count`.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -24,10 +27,10 @@ variable (p q : α → Bool)
 protected theorem countP_go_eq_add (l) : countP.go p l n = n + countP.go p l 0 := by
   induction l generalizing n with
   | nil => rfl
-  | cons head tail ih =>
+  | cons hd _ ih =>
     unfold countP.go
     rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
-    if h : p head then simp [h, Nat.add_assoc] else simp [h]
+    if h : p hd then simp [h, Nat.add_assoc] else simp [h]
 
 @[simp] theorem countP_cons_of_pos (l) (pa : p a) : countP p (a :: l) = countP p l + 1 := by
   have : countP.go p (a :: l) 0 = countP.go p l 1 := show cond .. = _ by rw [pa]; rfl
@@ -46,8 +49,8 @@ theorem countP_cons (a : α) (l) : countP p (a :: l) = countP p l + if p a then
 theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a => ¬p a) l := by
   induction l with
   | nil => rfl
-  | cons x h ih =>
-    if h : p x then
+  | cons hd _ ih =>
+    if h : p hd then
       rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]
       · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
       · simp [h]
@@ -210,7 +213,7 @@ theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
 
 theorem count_tail : ∀ (l : List α) (a : α) (h : l ≠ []),
       l.tail.count a = l.count a - if l.head h == a then 1 else 0
-  | head :: tail, a, _ => by simp [count_cons]
+  | _ :: _, a, _ => by simp [count_cons]
 
 theorem count_le_length (a : α) (l : List α) : count a l ≤ l.length := countP_le_length _
 

src/Init/Data/List/Erase.lean

@@ -12,6 +12,9 @@ import Init.Data.List.Find
 # Lemmas about `List.eraseP`, `List.erase`, and `List.eraseIdx`.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -437,10 +440,10 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {l : List α} :
   rw [erase_eq_eraseP', eraseP_eq_iff]
   simp only [beq_iff_eq, forall_mem_ne', exists_and_left]
   constructor
-  · rintro (⟨h, rfl⟩ | ⟨a', l', h, rfl, x, rfl, rfl⟩)
+  · rintro (⟨h, rfl⟩ | ⟨a', l', h, rfl, xs, rfl, rfl⟩)
     · left; simp_all
-    · right; refine ⟨l', h, x, by simp⟩
-  · rintro (⟨h, rfl⟩ | ⟨l₁, h, x, rfl, rfl⟩)
+    · right; refine ⟨l', h, xs, by simp⟩
+  · rintro (⟨h, rfl⟩ | ⟨l₁, h, xs, rfl, rfl⟩)
     · left; simp_all
     · right; refine ⟨a, l₁, h, by simp⟩
 

src/Init/Data/List/FinRange.lean

@@ -6,6 +6,9 @@ Authors: François G. Dorais
 prelude
 import Init.Data.List.OfFn
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-- `finRange n` lists all elements of `Fin n` in order -/

src/Init/Data/List/Find.lean

@@ -15,6 +15,10 @@ Lemmas about `List.findSome?`, `List.find?`, `List.findIdx`, `List.findIdx?`, `L
 and `List.lookup`.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+
 namespace List
 
 open Nat
@@ -335,11 +339,11 @@ theorem get_find?_mem (xs : List α) (p : α → Bool) (h) : (xs.find? p).get h
     simp only [cons_append, find?]
     by_cases h : p x <;> simp [h, ih]
 
-@[simp] theorem find?_flatten (xs : List (List α)) (p : α → Bool) :
-    xs.flatten.find? p = xs.findSome? (·.find? p) := by
-  induction xs with
+@[simp] theorem find?_flatten (xss : List (List α)) (p : α → Bool) :
+    xss.flatten.find? p = xss.findSome? (·.find? p) := by
+  induction xss with
   | nil => simp
-  | cons x xs ih =>
+  | cons _ _ ih =>
     simp only [flatten_cons, find?_append, findSome?_cons, ih]
     split <;> simp [*]
 
@@ -358,7 +362,7 @@ Moreover, no earlier list in `xs` has an element satisfying `p`.
 theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a : α} :
     xs.flatten.find? p = some a ↔
       p a ∧ ∃ as ys zs bs, xs = as ++ (ys ++ a :: zs) :: bs ∧
-        (∀ a ∈ as, ∀ x ∈ a, !p x) ∧ (∀ x ∈ ys, !p x) := by
+        (∀ l ∈ as, ∀ x ∈ l, !p x) ∧ (∀ x ∈ ys, !p x) := by
   rw [find?_eq_some_iff_append]
   constructor
   · rintro ⟨h, ⟨ys, zs, h₁, h₂⟩⟩
@@ -370,8 +374,8 @@ theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a :
       obtain ⟨bs, cs, ds, rfl, h₁, rfl⟩ := h₁
       refine ⟨as ++ bs, [], cs, ds, by simp, ?_⟩
       simp
-      rintro a (ma | mb) x m
-      · simpa using h₂ x (by simpa using ⟨a, ma, m⟩)
+      rintro l (ma | mb) x m
+      · simpa using h₂ x (by simpa using ⟨l, ma, m⟩)
       · specialize h₁ _ mb
         simp_all
     · simp [h₁]
@@ -519,7 +523,7 @@ theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {
       (List.findFinIdx?.go p l xs i h).map (·.val) := by
   unfold findIdx?.go
   unfold findFinIdx?.go
-  split <;> rename_i a xs
+  split
   · simp_all
   · simp only
     split
@@ -563,10 +567,10 @@ where
       List.findIdx.go p l (n + 1) = (findIdx.go p l n) + 1 := by
     cases l with
     | nil => unfold findIdx.go; exact Nat.succ_eq_add_one n
-    | cons head tail =>
+    | cons hd tl =>
       unfold findIdx.go
-      cases p head <;> simp only [cond_false, cond_true]
-      exact findIdx_go_succ p tail (n + 1)
+      cases p hd <;> simp only [cond_false, cond_true]
+      exact findIdx_go_succ p tl (n + 1)
 
 theorem findIdx_of_getElem?_eq_some {xs : List α} (w : xs[xs.findIdx p]? = some y) : p y := by
   induction xs with

src/Init/Data/List/Impl.lean

@@ -16,6 +16,9 @@ If you import `Init.Data.List.Basic` but do not import this file,
 then at runtime you will get non-tail recursive versions of the following definitions.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-! ## Basic `List` operations.
@@ -57,8 +60,8 @@ The following operations are given `@[csimp]` replacements below:
 
 @[csimp] theorem set_eq_setTR : @set = @setTR := by
   funext α l n a; simp [setTR]
-  let rec go (acc) : ∀ xs n, l = acc.toList ++ xs →
-    setTR.go l a xs n acc = acc.toList ++ xs.set n a
+  let rec go (acc) : ∀ xs i, l = acc.toList ++ xs →
+    setTR.go l a xs i acc = acc.toList ++ xs.set i a
   | [], _ => fun h => by simp [setTR.go, set, h]
   | x::xs, 0 => by simp [setTR.go, set]
   | x::xs, n+1 => fun h => by simp only [setTR.go, set]; rw [go _ xs] <;> simp [h]
@@ -131,13 +134,13 @@ The following operations are given `@[csimp]` replacements below:
   | a::as, n+1, acc => go as n (acc.push a)
 
 @[csimp] theorem take_eq_takeTR : @take = @takeTR := by
-  funext α n l; simp [takeTR]
-  suffices ∀ xs acc, l = acc.toList ++ xs → takeTR.go l xs n acc = acc.toList ++ xs.take n from
+  funext α i l; simp [takeTR]
+  suffices ∀ xs acc, l = acc.toList ++ xs → takeTR.go l xs i acc = acc.toList ++ xs.take i from
     (this l #[] (by simp)).symm
-  intro xs; induction xs generalizing n with intro acc
-  | nil => cases n <;> simp [take, takeTR.go]
+  intro xs; induction xs generalizing i with intro acc
+  | nil => cases i <;> simp [take, takeTR.go]
   | cons x xs IH =>
-    cases n with simp only [take, takeTR.go]
+    cases i with simp only [take, takeTR.go]
     | zero => simp
     | succ n => intro h; rw [IH] <;> simp_all
 
@@ -225,7 +228,7 @@ theorem modifyTR_go_eq : ∀ l n, modifyTR.go f l n acc = acc.toList ++ modify f
   | _, [], acc => acc.toList
   | n+1, a :: l, acc => go n l (acc.push a)
 
-theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l
+theorem insertIdxTR_go_eq : ∀ i l, insertIdxTR.go a i l acc = acc.toList ++ insertIdx i a l
   | 0, l | _+1, [] => by simp [insertIdxTR.go, insertIdx]
   | n+1, a :: l => by simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l]
 
@@ -284,15 +287,15 @@ theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ in
   | a::as, n+1, acc => go as n (acc.push a)
 
 @[csimp] theorem eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR := by
-  funext α l n; simp [eraseIdxTR]
-  suffices ∀ xs acc, l = acc.toList ++ xs → eraseIdxTR.go l xs n acc = acc.toList ++ xs.eraseIdx n from
+  funext α l i; simp [eraseIdxTR]
+  suffices ∀ xs acc, l = acc.toList ++ xs → eraseIdxTR.go l xs i acc = acc.toList ++ xs.eraseIdx i from
     (this l #[] (by simp)).symm
-  intro xs; induction xs generalizing n with intro acc h
+  intro xs; induction xs generalizing i with intro acc h
   | nil => simp [eraseIdx, eraseIdxTR.go, h]
   | cons x xs IH =>
-    match n with
+    match i with
     | 0 => simp [eraseIdx, eraseIdxTR.go]
-    | n+1 =>
+    | i+1 =>
       simp only [eraseIdxTR.go, eraseIdx]
       rw [IH]; simp; simp; exact h
 
@@ -320,13 +323,13 @@ theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ in
 
 /-- 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
+  let as := l.toArray
+  (as.foldr (fun a (n, acc) => (n-1, (a, n-1) :: acc)) (n + as.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)
+  let rec go : ∀ l i, l.foldr f (i + l.length, []) = (i, zipIdx l i)
     | [], n => rfl
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
@@ -339,8 +342,8 @@ def zipIdxTR (l : List α) (n : Nat := 0) : List (α × Nat) :=
 /-- 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
+  let as := l.toArray
+  (as.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + as.size, [])).2
 
 set_option linter.deprecated false in
 @[deprecated zipIdx_eq_zipIdxTR (since := "2025-01-21"), csimp]
@@ -359,6 +362,7 @@ theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
 
 /-! ### intercalate -/
 
+set_option linter.listVariables false in
 /-- Tail recursive version of `List.intercalate`. -/
 def intercalateTR (sep : List α) : List (List α) → List α
   | [] => []
@@ -371,6 +375,7 @@ where
   | x, [], acc => acc.toListAppend x
   | x, y::xs, acc => go sep y xs (acc ++ x ++ sep)
 
+set_option linter.listVariables false in
 @[csimp] theorem intercalate_eq_intercalateTR : @intercalate = @intercalateTR := by
   funext α sep l; simp [intercalate, intercalateTR]
   match l with

src/Init/Data/List/Lemmas.lean

@@ -73,6 +73,10 @@ Also
 * `Init.Data.List.Monadic` for addiation lemmas about `List.mapM` and `List.forM`.
 
 -/
+
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -146,10 +150,10 @@ theorem cons_inj_right (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :
 theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' :=
   List.cons.injEq .. ▸ .rfl
 
-theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L
+theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b l', l = b :: l'
   | c :: l', _ => ⟨c, l', rfl⟩
 
-theorem ne_nil_iff_exists_cons {l : List α} : l ≠ [] ↔ ∃ b L, l = b :: L :=
+theorem ne_nil_iff_exists_cons {l : List α} : l ≠ [] ↔ ∃ b l', l = b :: l' :=
   ⟨exists_cons_of_ne_nil, fun ⟨_, _, eq⟩ => eq.symm ▸ cons_ne_nil _ _⟩
 
 theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by
@@ -588,11 +592,11 @@ theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
 /-! ### set -/
 
 -- As `List.set` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
-@[simp] theorem set_nil (n : Nat) (a : α) : [].set n a = [] := rfl
+@[simp] theorem set_nil (i : Nat) (a : α) : [].set i a = [] := rfl
 @[simp] theorem set_cons_zero (x : α) (xs : List α) (a : α) :
   (x :: xs).set 0 a = a :: xs := rfl
-@[simp] theorem set_cons_succ (x : α) (xs : List α) (n : Nat) (a : α) :
-  (x :: xs).set (n + 1) a = x :: xs.set n a := rfl
+@[simp] theorem set_cons_succ (x : α) (xs : List α) (i : Nat) (a : α) :
+  (x :: xs).set (i + 1) a = x :: xs.set i a := rfl
 
 @[simp] theorem getElem_set_self {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
     (l.set i a)[i] = a :=
@@ -668,22 +672,22 @@ theorem getElem?_set' {l : List α} {i j : Nat} {a : α} :
     rw [getElem_set]
     split <;> simp_all
 
-theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α} :
-    l.set n a = l := by
-  induction l generalizing n with
+theorem set_eq_of_length_le {l : List α} {i : Nat} (h : l.length ≤ i) {a : α} :
+    l.set i a = l := by
+  induction l generalizing i with
   | nil => simp_all
   | cons a l ih =>
-    induction n
+    induction i
     · simp_all
     · simp only [set_cons_succ, cons.injEq, true_and]
       rw [ih]
       exact Nat.succ_le_succ_iff.mp h
 
-@[simp] theorem set_eq_nil_iff {l : List α} (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by
-  cases l <;> cases n <;> simp [set]
+@[simp] theorem set_eq_nil_iff {l : List α} (i : Nat) (a : α) : l.set i a = [] ↔ l = [] := by
+  cases l <;> cases i <;> simp [set]
 
-theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
-    (l.set n a).set m b = (l.set m b).set n a
+theorem set_comm (a b : α) : ∀ {i j : Nat} (l : List α), i ≠ j →
+    (l.set i a).set j b = (l.set j b).set i a
   | _, _, [], _ => by simp
   | _+1, 0, _ :: _, _ => by simp [set]
   | 0, _+1, _ :: _, _ => by simp [set]
@@ -691,17 +695,17 @@ theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m →
     congrArg _ <| set_comm a b t fun h' => h <| Nat.succ_inj'.mpr h'
 
 @[simp]
-theorem set_set (a b : α) : ∀ (l : List α) (n : Nat), (l.set n a).set n b = l.set n b
+theorem set_set (a b : α) : ∀ (l : List α) (i : Nat), (l.set i a).set i b = l.set i b
   | [], _ => by simp
   | _ :: _, 0 => by simp [set]
   | _ :: _, _+1 => by simp [set, set_set]
 
-theorem mem_set (l : List α) (n : Nat) (h : n < l.length) (a : α) :
-    a ∈ l.set n a := by
+theorem mem_set (l : List α) (i : Nat) (h : i < l.length) (a : α) :
+    a ∈ l.set i a := by
   simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
+  exact ⟨i, (by simpa using h), by simp⟩
 
-theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.set n b → a ∈ l ∨ a = b
+theorem mem_or_eq_of_mem_set : ∀ {l : List α} {i : Nat} {a b : α}, a ∈ l.set i b → a ∈ l ∨ a = b
   | _ :: _, 0, _, _, h => ((mem_cons ..).1 h).symm.imp_left (.tail _)
   | _ :: _, _+1, _, _, .head .. => .inl (.head ..)
   | _ :: _, _+1, _, _, .tail _ h => (mem_or_eq_of_mem_set h).imp_left (.tail _)
@@ -756,10 +760,10 @@ theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l
     simp
   · intro h
     constructor
-    intro a
-    induction a with
+    intro l
+    induction l with
     | nil => simp only [List.instBEq, List.beq]
-    | cons a as ih =>
+    | cons _ _ ih =>
       simp [List.instBEq, List.beq]
       exact ih
 
@@ -778,9 +782,9 @@ theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l
       simp
   · intro h
     constructor
-    · intro a b h
+    · intro _ _ h
       simpa using h
-    · intro a
+    · intro _
       simp
 
 /-! ### isEqv -/
@@ -1171,8 +1175,8 @@ theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs =
   | cons b l ih => cases i <;> simp_all
 
 @[deprecated "Use the reverse direction of `map_set`." (since := "2024-09-20")]
-theorem set_map {f : α → β} {l : List α} {n : Nat} {a : α} :
-    (map f l).set n (f a) = map f (l.set n a) := by
+theorem set_map {f : α → β} {l : List α} {i : Nat} {a : α} :
+    (map f l).set i (f a) = map f (l.set i a) := by
   simp
 
 @[simp] theorem head_map (f : α → β) (l : List α) (w) :
@@ -1627,16 +1631,16 @@ theorem append_right_inj {t₁ t₂ : List α} (s) : s ++ t₁ = s ++ t₂ ↔ t
 theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s₁ = s₂ :=
   ⟨fun h => append_inj_left' h rfl, congrArg (· ++ _)⟩
 
-@[simp] theorem append_left_eq_self {x y : List α} : x ++ y = y ↔ x = [] := by
-  rw [← append_left_inj (s₁ := x), nil_append]
+@[simp] theorem append_left_eq_self {xs ys : List α} : xs ++ ys = ys ↔ xs = [] := by
+  rw [← append_left_inj (s₁ := xs), nil_append]
 
-@[simp] theorem self_eq_append_left {x y : List α} : y = x ++ y ↔ x = [] := by
+@[simp] theorem self_eq_append_left {xs ys : List α} : ys = xs ++ ys ↔ xs = [] := by
   rw [eq_comm, append_left_eq_self]
 
-@[simp] theorem append_right_eq_self {x y : List α} : x ++ y = x ↔ y = [] := by
-  rw [← append_right_inj (t₁ := y), append_nil]
+@[simp] theorem append_right_eq_self {xs ys : List α} : xs ++ ys = xs ↔ ys = [] := by
+  rw [← append_right_inj (t₁ := ys), append_nil]
 
-@[simp] theorem self_eq_append_right {x y : List α} : x = x ++ y ↔ y = [] := by
+@[simp] theorem self_eq_append_right {xs ys : List α} : xs = xs ++ ys ↔ ys = [] := by
   rw [eq_comm, append_right_eq_self]
 
 theorem getLast_concat {a : α} : ∀ (l : List α), getLast (l ++ [a]) (by simp) = a
@@ -1663,14 +1667,14 @@ theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α)
 theorem append_ne_nil_of_ne_nil_right (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
 
 theorem append_eq_cons_iff :
-    a ++ b = x :: c ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
-  cases a with simp | cons a as => ?_
-  exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨a', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩
+    as ++ bs = x :: c ↔ (as = [] ∧ bs = x :: c) ∨ (∃ as', as = x :: as' ∧ c = as' ++ bs) := by
+  cases as with simp | cons a as => ?_
+  exact ⟨fun h => ⟨as, by simp [h]⟩, fun ⟨as', ⟨aeq, aseq⟩, h⟩ => ⟨aeq, by rw [aseq, h]⟩⟩
 
 @[deprecated append_eq_cons_iff (since := "2024-07-24")] abbrev append_eq_cons := @append_eq_cons_iff
 
 theorem cons_eq_append_iff :
-    x :: c = a ++ b ↔ (a = [] ∧ b = x :: c) ∨ (∃ a', a = x :: a' ∧ c = a' ++ b) := by
+    x :: cs = as ++ bs ↔ (as = [] ∧ bs = x :: cs) ∨ (∃ as', as = x :: as' ∧ cs = as' ++ bs) := by
   rw [eq_comm, append_eq_cons_iff]
 
 @[deprecated cons_eq_append_iff (since := "2024-07-24")] abbrev cons_eq_append := @cons_eq_append_iff
@@ -1683,11 +1687,11 @@ theorem singleton_eq_append_iff :
     [x] = a ++ b ↔ (a = [] ∧ b = [x]) ∨ (a = [x] ∧ b = []) := by
   cases a <;> cases b <;> simp [eq_comm]
 
-theorem append_eq_append_iff {a b c d : List α} :
-    a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b := by
-  induction a generalizing c with
+theorem append_eq_append_iff {ws xs ys zs : List α} :
+    ws ++ xs = ys ++ zs ↔ (∃ as, ys = ws ++ as ∧ xs = as ++ zs) ∨ ∃ bs, ws = ys ++ bs ∧ zs = bs ++ xs := by
+  induction ws generalizing ys with
   | nil => simp_all
-  | cons a as ih => cases c <;> simp [eq_comm, and_assoc, ih, and_or_left]
+  | cons a as ih => cases ys <;> simp [eq_comm, and_assoc, ih, and_or_left]
 
 @[deprecated append_inj (since := "2024-07-24")] abbrev append_inj_of_length_left := @append_inj
 @[deprecated append_inj' (since := "2024-07-24")] abbrev append_inj_of_length_right := @append_inj'
@@ -1778,7 +1782,7 @@ theorem filterMap_eq_append_iff {f : α → Option β} :
         simp_all
       · rename_i b w
         intro h
-        rcases cons_eq_append_iff.mp h with (⟨rfl, rfl⟩ | ⟨L₁, ⟨rfl, h⟩⟩)
+        rcases cons_eq_append_iff.mp h with (⟨rfl, rfl⟩ | ⟨_, ⟨rfl, h⟩⟩)
         · refine ⟨[], x :: l, ?_⟩
           simp [filterMap_cons, w]
         · obtain ⟨l₁, l₂, rfl, rfl, rfl⟩ := ih ‹_›
@@ -1861,11 +1865,11 @@ theorem map_concat (f : α → β) (a : α) (l : List α) : map f (concat l a) =
   | nil => rfl
   | cons x xs ih => simp [ih]
 
-theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = concat L b
+theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ l' b, l = concat l' b
   | [] => .inl rfl
   | a::l => match l, eq_nil_or_concat l with
     | _, .inl rfl => .inr ⟨[], a, rfl⟩
-    | _, .inr ⟨L, b, rfl⟩ => .inr ⟨a::L, b, rfl⟩
+    | _, .inr ⟨l', b, rfl⟩ => .inr ⟨a::l', b, rfl⟩
 
 /-! ### flatten -/
 
@@ -1879,7 +1883,7 @@ theorem flatten_singleton (l : List α) : [l].flatten = l := by simp
 
 @[simp] theorem mem_flatten : ∀ {L : List (List α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l
   | [] => by simp
-  | b :: l => by simp [mem_flatten, or_and_right, exists_or]
+  | _ :: _ => by simp [mem_flatten, or_and_right, exists_or]
 
 @[simp] theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] ↔ ∀ l ∈ L, l = [] := by
   induction L <;> simp_all
@@ -1887,7 +1891,7 @@ theorem flatten_singleton (l : List α) : [l].flatten = l := by simp
 @[simp] theorem nil_eq_flatten_iff {L : List (List α)} : [] = L.flatten ↔ ∀ l ∈ L, l = [] := by
   rw [eq_comm, flatten_eq_nil_iff]
 
-theorem flatten_ne_nil_iff {xs : List (List α)} : xs.flatten ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ [] := by
+theorem flatten_ne_nil_iff {xss : List (List α)} : xss.flatten ≠ [] ↔ ∃ xs, xs ∈ xss ∧ xs ≠ [] := by
   simp
 
 theorem exists_of_mem_flatten : a ∈ flatten L → ∃ l, l ∈ L ∧ a ∈ l := mem_flatten.1
@@ -1945,13 +1949,13 @@ theorem flatten_concat (L : List (List α)) (l : List α) : flatten (L ++ [l]) =
 theorem flatten_flatten {L : List (List (List α))} : flatten (flatten L) = flatten (map flatten L) := by
   induction L <;> simp_all
 
-theorem flatten_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
-    xs.flatten = y :: ys ↔
-      ∃ as bs cs, xs = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.flatten := by
+theorem flatten_eq_cons_iff {xss : List (List α)} {y : α} {ys : List α} :
+    xss.flatten = y :: ys ↔
+      ∃ as bs cs, xss = as ++ (y :: bs) :: cs ∧ (∀ l, l ∈ as → l = []) ∧ ys = bs ++ cs.flatten := by
   constructor
-  · induction xs with
+  · induction xss with
     | nil => simp
-    | cons x xs ih =>
+    | cons xs xss ih =>
       intro h
       simp only [flatten_cons] at h
       replace h := h.symm
@@ -1960,8 +1964,8 @@ theorem flatten_eq_cons_iff {xs : List (List α)} {y : α} {ys : List α} :
       · obtain ⟨as, bs, cs, rfl, _, rfl⟩ := ih h
         refine ⟨[] :: as, bs, cs, ?_⟩
         simpa
-      · obtain ⟨a', rfl, rfl⟩ := z
-        refine ⟨[], a', xs, ?_⟩
+      · obtain ⟨as', rfl, rfl⟩ := z
+        refine ⟨[], as', xss, ?_⟩
         simp
   · rintro ⟨as, bs, cs, rfl, h₁, rfl⟩
     simp [flatten_eq_nil_iff.mpr h₁]
@@ -1986,30 +1990,30 @@ theorem singleton_eq_flatten_iff {xs : List (List α)} {y : α} :
     [y] = xs.flatten ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l, l ∈ as → l = []) ∧ (∀ l, l ∈ bs → l = []) := by
   rw [eq_comm, flatten_eq_singleton_iff]
 
-theorem flatten_eq_append_iff {xs : List (List α)} {ys zs : List α} :
-    xs.flatten = ys ++ zs ↔
-      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
-        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧
+theorem flatten_eq_append_iff {xss : List (List α)} {ys zs : List α} :
+    xss.flatten = ys ++ zs ↔
+      (∃ as bs, xss = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
+        ∃ as bs c cs ds, xss = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧
           zs = c :: cs ++ ds.flatten := by
   constructor
-  · induction xs generalizing ys with
+  · induction xss generalizing ys with
     | nil =>
       simp only [flatten_nil, nil_eq, append_eq_nil_iff, and_false, cons_append, false_and,
         exists_const, exists_false, or_false, and_imp, List.cons_ne_nil]
       rintro rfl rfl
       exact ⟨[], [], by simp⟩
-    | cons x xs ih =>
+    | cons xs xss ih =>
       intro h
       simp only [flatten_cons] at h
       rw [append_eq_append_iff] at h
-      obtain (⟨ys, rfl, h⟩ | ⟨c', rfl, h⟩) := h
+      obtain (⟨ys, rfl, h⟩ | ⟨bs, rfl, h⟩) := h
       · obtain (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩) := ih h
-        · exact .inl ⟨x :: as, bs, by simp⟩
-        · exact .inr ⟨x :: as, bs, c, cs, ds, by simp⟩
+        · exact .inl ⟨xs :: as, bs, by simp⟩
+        · exact .inr ⟨xs :: as, bs, c, cs, ds, by simp⟩
       · simp only [h]
-        cases c' with
-        | nil => exact .inl ⟨[ys], xs, by simp⟩
-        | cons x c' => exact .inr ⟨[], ys, x, c', xs, by simp⟩
+        cases bs with
+        | nil => exact .inl ⟨[ys], xss, by simp⟩
+        | cons b bs => exact .inr ⟨[], ys, b, bs, xss, by simp⟩
   · rintro (⟨as, bs, rfl, rfl, rfl⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, rfl⟩)
     · simp
     · simp
@@ -2026,8 +2030,8 @@ sublists. -/
 theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
     L = L' ↔ L.flatten = L'.flatten ∧ map length L = map length L'
   | _, [] => by simp_all
-  | [], x' :: L' => by simp_all
-  | x :: L, x' :: L' => by
+  | [], _ :: _ => by simp_all
+  | _ :: _, _ :: _ => by
     simp
     rw [eq_iff_flatten_eq]
     constructor
@@ -2041,9 +2045,9 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
 
 theorem flatMap_def (l : List α) (f : α → List β) : l.flatMap f = flatten (map f l) := by rfl
 
-@[simp] theorem flatMap_id (l : List (List α)) : l.flatMap id = l.flatten := by simp [flatMap_def]
+@[simp] theorem flatMap_id (L : List (List α)) : L.flatMap id = L.flatten := by simp [flatMap_def]
 
-@[simp] theorem flatMap_id' (l : List (List α)) : l.flatMap (fun a => a) = l.flatten := by simp [flatMap_def]
+@[simp] theorem flatMap_id' (L : List (List α)) : L.flatMap (fun as => as) = L.flatten := by simp [flatMap_def]
 
 @[simp]
 theorem length_flatMap (l : List α) (f : α → List β) :
@@ -2166,16 +2170,16 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 
 @[deprecated replicate_eq_nil_iff (since := "2024-09-05")] abbrev replicate_eq_nil := @replicate_eq_nil_iff
 
-@[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) :
-    (replicate n a)[m] = a :=
+@[simp] theorem getElem_replicate (a : α) {n : Nat} {i} (h : i < (replicate n a).length) :
+    (replicate n a)[i] = a :=
   eq_of_mem_replicate (getElem_mem _)
 
-theorem getElem?_replicate : (replicate n a)[m]? = if m < n then some a else none := by
-  by_cases h : m < n
+theorem getElem?_replicate : (replicate n a)[i]? = if i < n then some a else none := by
+  by_cases h : i < n
   · rw [getElem?_eq_getElem (by simpa), getElem_replicate, if_pos h]
   · rw [getElem?_eq_none (by simpa using h), if_neg h]
 
-@[simp] theorem getElem?_replicate_of_lt {n : Nat} {m : Nat} (h : m < n) : (replicate n a)[m]? = some a := by
+@[simp] theorem getElem?_replicate_of_lt {n : Nat} {i : Nat} (h : i < n) : (replicate n a)[i]? = some a := by
   simp [getElem?_replicate, h]
 
 theorem head?_replicate (a : α) (n : Nat) : (replicate n a).head? = if n = 0 then none else some a := by
@@ -2357,18 +2361,18 @@ theorem eq_replicate_or_eq_replicate_append_cons {α : Type _} (l : List α) :
 
 /-- An induction principle for lists based on contiguous runs of identical elements. -/
 -- A `Sort _` valued version would require a different design. (And associated `@[simp]` lemmas.)
-theorem replicateRecOn {α : Type _} {p : List α → Prop} (m : List α)
+theorem replicateRecOn {α : Type _} {p : List α → Prop} (l : List α)
     (h0 : p []) (hr : ∀ a n, 0 < n → p (replicate n a))
-    (hi : ∀ a b n l, a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)) : p m := by
-  rcases eq_replicate_or_eq_replicate_append_cons m with
+    (hi : ∀ a b n l, a ≠ b → 0 < n → p (b :: l) → p (replicate n a ++ b :: l)) : p l := by
+  rcases eq_replicate_or_eq_replicate_append_cons l with
     rfl | ⟨n, a, rfl, hn⟩ | ⟨n, a, b, l', w, hn, h⟩
   · exact h0
   · exact hr _ _ hn
-  · have : (b :: l').length < m.length := by
+  · have : (b :: l').length < l.length := by
       simpa [w] using Nat.lt_add_of_pos_left hn
     subst w
     exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi)
-termination_by m.length
+termination_by l.length
 
 @[simp] theorem sum_replicate_nat (n : Nat) (a : Nat) : (replicate n a).sum = n * a := by
   induction n <;> simp_all [replicate_succ, Nat.add_mul, Nat.add_comm]
@@ -2552,7 +2556,7 @@ theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
 /-! ### foldl and foldr -/
 
 @[simp] theorem foldr_cons_eq_append (l : List α) (f : α → β) (l' : List β) :
-    l.foldr (fun x y => f x :: y) l' = l.map f ++ l' := by
+    l.foldr (fun x ys => f x :: ys) l' = l.map f ++ l' := by
   induction l <;> simp [*]
 
 /-- Variant of `foldr_cons_eq_append` specalized to `f = id`. -/
@@ -2563,7 +2567,7 @@ theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
 @[deprecated foldr_cons_eq_append (since := "2024-08-22")] abbrev foldr_self_append := @foldr_cons_eq_append
 
 @[simp] theorem foldl_flip_cons_eq_append (l : List α) (f : α → β) (l' : List β) :
-    l.foldl (fun x y => f y :: x) l' = (l.map f).reverse ++ l' := by
+    l.foldl (fun xs y => f y :: xs) l' = (l.map f).reverse ++ l' := by
   induction l generalizing l' <;> simp [*]
 
 @[simp] theorem foldr_append_eq_append (l : List α) (f : α → List β) (l' : List β) :
@@ -2575,11 +2579,11 @@ theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
   induction l generalizing l'<;> simp [*]
 
 @[simp] theorem foldr_flip_append_eq_append (l : List α) (f : α → List β) (l' : List β) :
-    l.foldr (fun x y => y ++ f x) l' = l' ++ (l.map f).reverse.flatten := by
+    l.foldr (fun x ys => ys ++ f x) l' = l' ++ (l.map f).reverse.flatten := by
   induction l generalizing l' <;> simp [*]
 
 @[simp] theorem foldl_flip_append_eq_append (l : List α) (f : α → List β) (l' : List β) :
-    l.foldl (fun x y => f y ++ x) l' = (l.map f).reverse.flatten ++ l' := by
+    l.foldl (fun xs y => f y ++ xs) l' = (l.map f).reverse.flatten ++ l' := by
   induction l generalizing l' <;> simp [*]
 
 theorem foldr_cons_nil (l : List α) : l.foldr cons [] = l := by simp
@@ -2869,8 +2873,8 @@ theorem getLast_filterMap_of_eq_some {f : α → Option β} {l : List α} {w : l
   rw [head_filterMap_of_eq_some (by simp_all)]
   simp_all
 
-theorem getLast?_flatMap {L : List α} {f : α → List β} :
-    (L.flatMap f).getLast? = L.reverse.findSome? fun a => (f a).getLast? := by
+theorem getLast?_flatMap {l : List α} {f : α → List β} :
+    (l.flatMap f).getLast? = l.reverse.findSome? fun a => (f a).getLast? := by
   simp only [← head?_reverse, reverse_flatMap]
   rw [head?_flatMap]
   rfl
@@ -3058,16 +3062,16 @@ We don't provide any API for `splitAt`, beyond the `@[simp]` lemma
 which is proved in `Init.Data.List.TakeDrop`.
 -/
 
-theorem splitAt_go (n : Nat) (l acc : List α) :
-    splitAt.go l xs n acc =
-      if n < xs.length then (acc.reverse ++ xs.take n, xs.drop n) else (l, []) := by
-  induction xs generalizing n acc with
+theorem splitAt_go (i : Nat) (l acc : List α) :
+    splitAt.go l xs i acc =
+      if i < xs.length then (acc.reverse ++ xs.take i, xs.drop i) else (l, []) := by
+  induction xs generalizing i acc with
   | nil => simp [splitAt.go]
   | cons x xs ih =>
-    cases n with
+    cases i with
     | zero => simp [splitAt.go]
-    | succ n =>
-      rw [splitAt.go, take_succ_cons, drop_succ_cons, ih n (x :: acc),
+    | succ i =>
+      rw [splitAt.go, take_succ_cons, drop_succ_cons, ih i (x :: acc),
         reverse_cons, append_assoc, singleton_append, length_cons]
       simp only [Nat.succ_lt_succ_iff]
 
@@ -3149,14 +3153,14 @@ theorem replace_append_right [LawfulBEq α] {l₁ l₂ : List α} (h : ¬ a ∈
     (l₁ ++ l₂).replace a b = l₁ ++ l₂.replace a b := by
   simp [replace_append, h]
 
-theorem replace_take {l : List α} {n : Nat} :
-    (l.take n).replace a b = (l.replace a b).take n := by
-  induction l generalizing n with
+theorem replace_take {l : List α} {i : Nat} :
+    (l.take i).replace a b = (l.replace a b).take i := by
+  induction l generalizing i with
   | nil => simp
   | cons x xs ih =>
-    cases n with
+    cases i with
     | zero => simp [ih]
-    | succ n =>
+    | succ i =>
       simp only [replace_cons, take_succ_cons]
       split <;> simp_all
 
@@ -3360,13 +3364,13 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!
     simp only [filterMap_cons]
     split <;> simp_all
 
-@[simp] theorem any_append {x y : List α} : (x ++ y).any f = (x.any f || y.any f) := by
-  induction x with
+@[simp] theorem any_append {xs ys : List α} : (xs ++ ys).any f = (xs.any f || ys.any f) := by
+  induction xs with
   | nil => rfl
   | cons h t ih => simp_all [Bool.or_assoc]
 
-@[simp] theorem all_append {x y : List α} : (x ++ y).all f = (x.all f && y.all f) := by
-  induction x with
+@[simp] theorem all_append {xs ys : List α} : (xs ++ ys).all f = (xs.all f && ys.all f) := by
+  induction xs with
   | nil => rfl
   | cons h t ih => simp_all [Bool.and_assoc]
 
@@ -3591,7 +3595,7 @@ theorem getElem?_eq (l : List α) (i : Nat) :
 @[deprecated getElem?_eq_none (since := "2024-11-29")] abbrev getElem?_len_le := @getElem?_eq_none
 
 @[deprecated _root_.isSome_getElem? (since := "2024-12-09")]
-theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
+theorem isSome_getElem? {l : List α} {i : Nat} : l[i]?.isSome ↔ i < l.length := by
   simp
 
 @[deprecated _root_.isNone_getElem? (since := "2024-12-09")]

src/Init/Data/List/Lex.lean

@@ -7,6 +7,9 @@ prelude
 import Init.Data.List.Lemmas
 import Init.Data.List.Nat.TakeDrop
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-! ### Lexicographic ordering -/
@@ -167,7 +170,7 @@ protected theorem lt_of_le_of_lt [DecidableEq α] [LT α] [DecidableLT α]
   induction h₂ generalizing l₁ with
   | nil => simp_all
   | rel hab =>
-    rename_i a b
+    rename_i a xs
     cases l₁ with
     | nil => simp_all
     | cons c l₁ =>

src/Init/Data/List/MapIdx.lean

@@ -11,6 +11,9 @@ import Init.Data.List.OfFn
 import Init.Data.Fin.Lemmas
 import Init.Data.Option.Attach
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-! ## Operations using indexes -/
@@ -131,10 +134,10 @@ theorem mapFinIdx_cons {l : List α} {a : α} {f : (i : Nat) → α → (h : i <
   · simp
   · rintro (_|i) h₁ h₂ <;> simp
 
-theorem mapFinIdx_append {K L : List α} {f : (i : Nat) → α → (h : i < (K ++ L).length) → β} :
-    (K ++ L).mapFinIdx f =
-      K.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
-        L.mapFinIdx (fun i a h => f (i + K.length) a (by simp; omega)) := by
+theorem mapFinIdx_append {xs ys : List α} {f : (i : Nat) → α → (h : i < (xs ++ ys).length) → β} :
+    (xs ++ ys).mapFinIdx f =
+      xs.mapFinIdx (fun i a h => f i a (by simp; omega)) ++
+        ys.mapFinIdx (fun i a h => f (i + xs.length) a (by simp; omega)) := by
   apply ext_getElem
   · simp
   · intro i h₁ h₂
@@ -299,15 +302,15 @@ theorem mapFinIdx_eq_replicate_iff {l : List α} {f : (i : Nat) → α → (h :
 theorem mapIdx_nil {f : Nat → α → β} : mapIdx f [] = [] :=
   rfl
 
-theorem mapIdx_go_length {arr : Array β} :
-    length (mapIdx.go f l arr) = length l + arr.size := by
-  induction l generalizing arr with
+theorem mapIdx_go_length {acc : Array β} :
+    length (mapIdx.go f l acc) = length l + acc.size := by
+  induction l generalizing acc with
   | nil => simp only [mapIdx.go, length_nil, Nat.zero_add]
   | cons _ _ ih =>
     simp only [mapIdx.go, ih, Array.size_push, Nat.add_succ, length_cons, Nat.add_comm]
 
-theorem length_mapIdx_go : ∀ {l : List α} {arr : Array β},
-    (mapIdx.go f l arr).length = l.length + arr.size
+theorem length_mapIdx_go : ∀ {l : List α} {acc : Array β},
+    (mapIdx.go f l acc).length = l.length + acc.size
   | [], _ => by simp [mapIdx.go]
   | a :: l, _ => by
     simp only [mapIdx.go, length_cons]
@@ -318,13 +321,13 @@ theorem length_mapIdx_go : ∀ {l : List α} {arr : Array β},
 @[simp] theorem length_mapIdx {l : List α} : (l.mapIdx f).length = l.length := by
   simp [mapIdx, length_mapIdx_go]
 
-theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
-    (mapIdx.go f l arr)[i]? =
-      if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.size]?
-  | [], arr, i => by
+theorem getElem?_mapIdx_go : ∀ {l : List α} {acc : Array β} {i : Nat},
+    (mapIdx.go f l acc)[i]? =
+      if h : i < acc.size then some acc[i] else Option.map (f i) l[i - acc.size]?
+  | [], acc, i => by
     simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList,
       ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']
-  | a :: l, arr, i => by
+  | a :: l, acc, i => by
     rw [mapIdx.go, getElem?_mapIdx_go]
     simp only [Array.size_push]
     split <;> split
@@ -332,10 +335,10 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
       rw [← Array.getElem_toList]
       simp only [Array.push_toList]
       rw [getElem_append_left, ← Array.getElem_toList]
-    · have : i = arr.size := by omega
+    · have : i = acc.size := by omega
       simp_all
     · omega
-    · have : i - arr.size = i - (arr.size + 1) + 1 := by omega
+    · have : i - acc.size = i - (acc.size + 1) + 1 := by omega
       simp_all
 
 @[simp] theorem getElem?_mapIdx {l : List α} {i : Nat} :
@@ -371,9 +374,9 @@ theorem mapIdx_cons {l : List α} {a : α} :
     mapIdx f (a :: l) = f 0 a :: mapIdx (fun i => f (i + 1)) l := by
   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
-  induction K generalizing f with
+theorem mapIdx_append {xs ys : List α} :
+    (xs ++ ys).mapIdx f = xs.mapIdx f ++ ys.mapIdx fun i => f (i + xs.length) := by
+  induction xs generalizing f with
   | nil => rfl
   | cons _ _ ih => simp [ih (f := fun i => f (i + 1)), Nat.add_assoc]
 

src/Init/Data/List/MinMax.lean

@@ -10,6 +10,9 @@ import Init.Data.List.Lemmas
 # Lemmas about `List.min?` and `List.max?.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat

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

@@ -7,18 +7,21 @@ prelude
 import Init.Data.Nat.Lemmas
 import Init.Data.List.Basic
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-! ### isEqv -/
 
-theorem isEqv_eq_decide (a b : List α) (r) :
-    isEqv a b r = if h : a.length = b.length then
-      decide (∀ (i : Nat) (h' : i < a.length), r (a[i]'(h ▸ h')) (b[i]'(h ▸ h'))) else false := by
-  induction a generalizing b with
+theorem isEqv_eq_decide (as bs : List α) (r) :
+    isEqv as bs r = if h : as.length = bs.length then
+      decide (∀ (i : Nat) (h' : i < as.length), r (as[i]'(h ▸ h')) (bs[i]'(h ▸ h'))) else false := by
+  induction as generalizing bs with
   | nil =>
-    cases b <;> simp
+    cases bs <;> simp
   | cons a as ih =>
-    cases b with
+    cases bs with
     | nil => simp
     | cons b bs =>
       simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]
@@ -26,12 +29,12 @@ theorem isEqv_eq_decide (a b : List α) (r) :
 
 /-! ### beq -/
 
-theorem beq_eq_isEqv [BEq α] (a b : List α) : a.beq b = isEqv a b (· == ·) := by
-  induction a generalizing b with
+theorem beq_eq_isEqv [BEq α] (as bs : List α) : as.beq bs = isEqv as bs (· == ·) := by
+  induction as generalizing bs with
   | nil =>
-    cases b <;> simp
+    cases bs <;> simp
   | cons a as ih =>
-    cases b with
+    cases bs with
     | nil => simp
     | cons b bs =>
       simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
@@ -39,9 +42,9 @@ theorem beq_eq_isEqv [BEq α] (a b : List α) : a.beq b = isEqv a b (· == ·) :
         Bool.decide_eq_true]
       split <;> simp
 
-theorem beq_eq_decide [BEq α] (a b : List α) :
-    (a == b) = if h : a.length = b.length then
-      decide (∀ (i : Nat) (h' : i < a.length), a[i] == b[i]'(h ▸ h')) else false := by
+theorem beq_eq_decide [BEq α] (as bs : List α) :
+    (as == bs) = if h : as.length = bs.length then
+      decide (∀ (i : Nat) (h' : i < as.length), as[i] == bs[i]'(h ▸ h')) else false := by
   simp [BEq.beq, beq_eq_isEqv, isEqv_eq_decide]
 
 end List

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

@@ -15,6 +15,9 @@ import Init.Data.Nat.Lemmas
 In particular, `omega` is available here.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 open Nat
 
 namespace List

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

@@ -7,6 +7,9 @@ prelude
 import Init.Data.List.Count
 import Init.Data.Nat.Lemmas
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat

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

@@ -7,6 +7,9 @@ prelude
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Erase
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 theorem getElem?_eraseIdx (l : List α) (i : Nat) (j : Nat) :

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

@@ -7,6 +7,9 @@ prelude
 import Init.Data.List.Nat.Range
 import Init.Data.List.Find
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -41,7 +44,7 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Boo
   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
+  obtain ⟨xs, h₁, b, ⟨ys, h₂⟩, ⟨hb, rfl⟩, h₃⟩ := h
   rw [zipIdx_eq_append_iff] at h₂
   obtain ⟨l₁', l₂', rfl, rfl, h₂⟩ := h₂
   rw [eq_comm, zipIdx_eq_cons_iff] at h₂

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

@@ -12,9 +12,10 @@ import Init.Data.List.Nat.Modify
 Proves various lemmas about `List.insertIdx`.
 -/
 
-open Function
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
-open Nat
+open Function Nat
 
 namespace List
 
@@ -35,31 +36,31 @@ theorem insertIdx_succ_nil (n : Nat) (a : α) : insertIdx (n + 1) a [] = [] :=
   rfl
 
 @[simp]
-theorem insertIdx_succ_cons (s : List α) (hd x : α) (n : Nat) :
-    insertIdx (n + 1) x (hd :: s) = hd :: insertIdx n x s :=
+theorem insertIdx_succ_cons (s : List α) (hd x : α) (i : Nat) :
+    insertIdx (i + 1) x (hd :: s) = hd :: insertIdx i x s :=
   rfl
 
-theorem length_insertIdx : ∀ n as, (insertIdx n a as).length = if n ≤ as.length then as.length + 1 else as.length
+theorem length_insertIdx : ∀ i as, (insertIdx i a as).length = if i ≤ as.length then as.length + 1 else as.length
   | 0, _ => by simp
   | n + 1, [] => by simp
   | n + 1, a :: as => by
     simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_le_add_iff_right]
     split <;> rfl
 
-theorem length_insertIdx_of_le_length (h : n ≤ length as) : length (insertIdx n a as) = length as + 1 := by
+theorem length_insertIdx_of_le_length (h : i ≤ length as) : length (insertIdx i a as) = length as + 1 := by
   simp [length_insertIdx, h]
 
-theorem length_insertIdx_of_length_lt (h : length as < n) : length (insertIdx n a as) = length as := by
+theorem length_insertIdx_of_length_lt (h : length as < i) : length (insertIdx i a as) = length as := by
   simp [length_insertIdx, h]
 
 @[simp]
-theorem eraseIdx_insertIdx (n : Nat) (l : List α) : (l.insertIdx n a).eraseIdx n = l := by
+theorem eraseIdx_insertIdx (i : Nat) (l : List α) : (l.insertIdx i a).eraseIdx i = l := by
   rw [eraseIdx_eq_modifyTailIdx, insertIdx, modifyTailIdx_modifyTailIdx_self]
   exact modifyTailIdx_id _ _
 
 theorem insertIdx_eraseIdx_of_ge :
-    ∀ n m as,
-      n < length as → n ≤ m → insertIdx m a (as.eraseIdx n) = (as.insertIdx (m + 1) a).eraseIdx n
+    ∀ i m as,
+      i < length as → i ≤ m → insertIdx m a (as.eraseIdx i) = (as.insertIdx (m + 1) a).eraseIdx i
   | 0, 0, [], has, _ => (Nat.lt_irrefl _ has).elim
   | 0, 0, _ :: as, _, _ => by simp [eraseIdx, insertIdx]
   | 0, _ + 1, _ :: _, _, _ => rfl
@@ -68,8 +69,8 @@ theorem insertIdx_eraseIdx_of_ge :
       insertIdx_eraseIdx_of_ge n m as (Nat.lt_of_succ_lt_succ has) (Nat.le_of_succ_le_succ hmn)
 
 theorem insertIdx_eraseIdx_of_le :
-    ∀ n m as,
-      n < length as → m ≤ n → insertIdx m a (as.eraseIdx n) = (as.insertIdx m a).eraseIdx (n + 1)
+    ∀ i j as,
+      i < length as → j ≤ i → insertIdx j a (as.eraseIdx i) = (as.insertIdx j a).eraseIdx (i + 1)
   | _, 0, _ :: _, _, _ => rfl
   | n + 1, m + 1, a :: as, has, hmn =>
     congrArg (cons a) <|
@@ -86,22 +87,22 @@ theorem insertIdx_comm (a b : α) :
     exact insertIdx_comm a b i j l (Nat.le_of_succ_le_succ h₀) (Nat.le_of_succ_le_succ h₁)
 
 theorem mem_insertIdx {a b : α} :
-    ∀ {n : Nat} {l : List α} (_ : n ≤ l.length), a ∈ l.insertIdx n b ↔ a = b ∨ a ∈ l
+    ∀ {i : Nat} {l : List α} (_ : i ≤ l.length), a ∈ l.insertIdx i b ↔ a = b ∨ a ∈ l
   | 0, as, _ => by simp
   | _ + 1, [], h => (Nat.not_succ_le_zero _ h).elim
   | n + 1, a' :: as, h => by
     rw [List.insertIdx_succ_cons, mem_cons, mem_insertIdx (Nat.le_of_succ_le_succ h),
       ← or_assoc, @or_comm (a = a'), or_assoc, mem_cons]
 
-theorem insertIdx_of_length_lt (l : List α) (x : α) (n : Nat) (h : l.length < n) :
-    insertIdx n x l = l := by
-  induction l generalizing n with
+theorem insertIdx_of_length_lt (l : List α) (x : α) (i : Nat) (h : l.length < i) :
+    insertIdx i x l = l := by
+  induction l generalizing i with
   | nil =>
-    cases n
+    cases i
     · simp at h
     · simp
   | cons x l ih =>
-    cases n
+    cases i
     · simp at h
     · simp only [Nat.succ_lt_succ_iff, length] at h
       simpa using ih _ h
@@ -112,84 +113,84 @@ theorem insertIdx_length_self (l : List α) (x : α) : insertIdx l.length x l =
   | nil => simp
   | cons x l ih => simpa using ih
 
-theorem length_le_length_insertIdx (l : List α) (x : α) (n : Nat) :
-    l.length ≤ (insertIdx n x l).length := by
+theorem length_le_length_insertIdx (l : List α) (x : α) (i : Nat) :
+    l.length ≤ (insertIdx i x l).length := by
   simp only [length_insertIdx]
   split <;> simp
 
-theorem length_insertIdx_le_succ (l : List α) (x : α) (n : Nat) :
-    (insertIdx n x l).length ≤ l.length + 1 := by
+theorem length_insertIdx_le_succ (l : List α) (x : α) (i : Nat) :
+    (insertIdx i x l).length ≤ l.length + 1 := by
   simp only [length_insertIdx]
   split <;> simp
 
-theorem getElem_insertIdx_of_lt {l : List α} {x : α} {n k : Nat} (hn : k < n)
-    (hk : k < (insertIdx n x l).length) :
-    (insertIdx n x l)[k] = l[k]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
-  induction n generalizing k l with
+theorem getElem_insertIdx_of_lt {l : List α} {x : α} {i j : Nat} (hn : j < i)
+    (hk : j < (insertIdx i x l).length) :
+    (insertIdx i x l)[j] = l[j]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
+  induction i generalizing j l with
   | zero => simp at hn
   | succ n ih =>
     cases l with
     | nil => simp
     | cons _ _=>
-      cases k
+      cases j
       · simp
       · rw [Nat.succ_lt_succ_iff] at hn
         simpa using ih hn _
 
 @[simp]
-theorem getElem_insertIdx_self {l : List α} {x : α} {n : Nat} (hn : n < (insertIdx n x l).length) :
-    (insertIdx n x l)[n] = x := by
-  induction l generalizing n with
+theorem getElem_insertIdx_self {l : List α} {x : α} {i : Nat} (hi : i < (insertIdx i x l).length) :
+    (insertIdx i x l)[i] = x := by
+  induction l generalizing i with
   | nil =>
-    simp [length_insertIdx] at hn
-    split at hn
+    simp [length_insertIdx] at hi
+    split at hi
     · simp_all
     · omega
   | cons _ _ ih =>
-    cases n
+    cases i
     · simp
-    · simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_lt_add_iff_right] at hn ih
-      simpa using ih hn
+    · simp only [insertIdx_succ_cons, length_cons, length_insertIdx, Nat.add_lt_add_iff_right] at hi ih
+      simpa using ih hi
 
-theorem getElem_insertIdx_of_gt {l : List α} {x : α} {n k : Nat} (hn : n < k)
-    (hk : k < (insertIdx n x l).length) :
-    (insertIdx n x l)[k] = l[k - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
-  induction l generalizing n k with
+theorem getElem_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (hn : i < j)
+    (hk : j < (insertIdx i x l).length) :
+    (insertIdx i x l)[j] = l[j - 1]'(by simp [length_insertIdx] at hk; split at hk <;> omega) := by
+  induction l generalizing i j with
   | nil =>
-    cases n with
+    cases i with
     | zero =>
       simp only [insertIdx_zero, length_singleton, lt_one_iff] at hk
       omega
     | succ n => simp at hk
   | cons _ _ ih =>
-    cases n with
+    cases i with
     | zero =>
       simp only [insertIdx_zero] at hk
-      cases k with
+      cases j with
       | zero => omega
-      | succ k => simp
+      | succ j => simp
     | succ n =>
-      cases k with
+      cases j with
       | zero => simp
-      | succ k =>
+      | succ j =>
         simp only [insertIdx_succ_cons, getElem_cons_succ]
         rw [ih (by omega)]
-        cases k with
+        cases j with
         | zero => omega
-        | succ k => simp
+        | succ j => simp
 
 @[deprecated getElem_insertIdx_of_gt (since := "2025-02-04")]
 abbrev getElem_insertIdx_of_ge := @getElem_insertIdx_of_gt
 
-theorem getElem_insertIdx {l : List α} {x : α} {n k : Nat} (h : k < (insertIdx n x l).length) :
-    (insertIdx n x l)[k] =
-      if h₁ : k < n then
-        l[k]'(by simp [length_insertIdx] at h; split at h <;> omega)
+theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (insertIdx i x l).length) :
+    (insertIdx i x l)[j] =
+      if h₁ : j < i then
+        l[j]'(by simp [length_insertIdx] at h; split at h <;> omega)
       else
-        if h₂ : k = n then
+        if h₂ : j = i then
           x
         else
-          l[k-1]'(by simp [length_insertIdx] at h; split at h <;> omega) := by
+          l[j-1]'(by simp [length_insertIdx] at h; split at h <;> omega) := by
   split <;> rename_i h₁
   · rw [getElem_insertIdx_of_lt h₁]
   · split <;> rename_i h₂
@@ -197,15 +198,15 @@ theorem getElem_insertIdx {l : List α} {x : α} {n k : Nat} (h : k < (insertIdx
       rw [getElem_insertIdx_self h]
     · rw [getElem_insertIdx_of_gt (by omega)]
 
-theorem getElem?_insertIdx {l : List α} {x : α} {n k : Nat} :
-    (insertIdx n x l)[k]? =
-      if k < n then
-        l[k]?
+theorem getElem?_insertIdx {l : List α} {x : α} {i j : Nat} :
+    (insertIdx i x l)[j]? =
+      if j < i then
+        l[j]?
       else
-        if k = n then
-          if k ≤ l.length then some x else none
+        if j = i then
+          if j ≤ l.length then some x else none
         else
-          l[k-1]? := by
+          l[j-1]? := by
   rw [getElem?_def]
   split <;> rename_i h
   · rw [getElem_insertIdx h]
@@ -228,17 +229,17 @@ theorem getElem?_insertIdx {l : List α} {x : α} {n k : Nat} :
       · rw [getElem?_eq_none]
         split at h <;> omega
 
-theorem getElem?_insertIdx_of_lt {l : List α} {x : α} {n k : Nat} (h : k < n) :
-    (insertIdx n x l)[k]? = l[k]? := by
+theorem getElem?_insertIdx_of_lt {l : List α} {x : α} {i j : Nat} (h : j < i) :
+    (insertIdx i x l)[j]? = l[j]? := by
   rw [getElem?_insertIdx, if_pos h]
 
-theorem getElem?_insertIdx_self {l : List α} {x : α} {n : Nat} :
-    (insertIdx n x l)[n]? = if n ≤ l.length then some x else none := by
+theorem getElem?_insertIdx_self {l : List α} {x : α} {i : Nat} :
+    (insertIdx i x l)[i]? = if i ≤ l.length then some x else none := by
   rw [getElem?_insertIdx, if_neg (by omega)]
   simp
 
-theorem getElem?_insertIdx_of_gt {l : List α} {x : α} {n k : Nat} (h : n < k) :
-    (insertIdx n x l)[k]? = l[k - 1]? := by
+theorem getElem?_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (h : i < j) :
+    (insertIdx i x l)[j]? = l[j - 1]? := by
   rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
 
 @[deprecated getElem?_insertIdx_of_gt (since := "2025-02-04")]

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

@@ -8,6 +8,9 @@ prelude
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Erase
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-! ### modifyHead -/
@@ -24,11 +27,11 @@ theorem modifyHead_eq_set [Inhabited α] (f : α → α) (l : List α) :
 @[simp] theorem modifyHead_modifyHead {l : List α} {f g : α → α} :
     (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
 
-theorem getElem_modifyHead {l : List α} {f : α → α} {n} (h : n < (l.modifyHead f).length) :
-    (l.modifyHead f)[n] = if h' : n = 0 then f (l[0]'(by simp at h; omega)) else l[n]'(by simpa using h) := by
+theorem getElem_modifyHead {l : List α} {f : α → α} {i} (h : i < (l.modifyHead f).length) :
+    (l.modifyHead f)[i] = if h' : i = 0 then f (l[0]'(by simp at h; omega)) else l[i]'(by simpa using h) := by
   cases l with
   | nil => simp at h
-  | cons hd tl => cases n <;> simp
+  | cons hd tl => cases i <;> simp
 
 @[simp] theorem getElem_modifyHead_zero {l : List α} {f : α → α} {h} :
     (l.modifyHead f)[0] = f (l[0]'(by simpa using h)) := by simp [getElem_modifyHead]
@@ -36,11 +39,11 @@ theorem getElem_modifyHead {l : List α} {f : α → α} {n} (h : n < (l.modifyH
 @[simp] theorem getElem_modifyHead_succ {l : List α} {f : α → α} {n} (h : n + 1 < (l.modifyHead f).length) :
     (l.modifyHead f)[n + 1] = l[n + 1]'(by simpa using h) := by simp [getElem_modifyHead]
 
-theorem getElem?_modifyHead {l : List α} {f : α → α} {n} :
-    (l.modifyHead f)[n]? = if n = 0 then l[n]?.map f else l[n]? := by
+theorem getElem?_modifyHead {l : List α} {f : α → α} {i} :
+    (l.modifyHead f)[i]? = if i = 0 then l[i]?.map f else l[i]? := by
   cases l with
   | nil => simp
-  | cons hd tl => cases n <;> simp
+  | cons hd tl => cases i <;> simp
 
 @[simp] theorem getElem?_modifyHead_zero {l : List α} {f : α → α} :
     (l.modifyHead f)[0]? = l[0]?.map f := by simp [getElem?_modifyHead]
@@ -60,19 +63,19 @@ theorem getElem?_modifyHead {l : List α} {f : α → α} {n} :
 @[simp] theorem tail_modifyHead {f : α → α} {l : List α} :
     (l.modifyHead f).tail = l.tail := by cases l <;> simp
 
-@[simp] theorem take_modifyHead {f : α → α} {l : List α} {n} :
-    (l.modifyHead f).take n = (l.take n).modifyHead f := by
-  cases l <;> cases n <;> simp
+@[simp] theorem take_modifyHead {f : α → α} {l : List α} {i} :
+    (l.modifyHead f).take i = (l.take i).modifyHead f := by
+  cases l <;> cases i <;> simp
 
-@[simp] theorem drop_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
-    (l.modifyHead f).drop n = l.drop n := by
-  cases l <;> cases n <;> simp_all
+@[simp] theorem drop_modifyHead_of_pos {f : α → α} {l : List α} {i} (h : 0 < i) :
+    (l.modifyHead f).drop i = l.drop i := by
+  cases l <;> cases i <;> simp_all
 
 theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
     (l.modifyHead f).eraseIdx 0 = l.eraseIdx 0 := by simp
 
-@[simp] theorem eraseIdx_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
-    (l.modifyHead f).eraseIdx n = (l.eraseIdx n).modifyHead f := by cases l <;> cases n <;> simp_all
+@[simp] theorem eraseIdx_modifyHead_of_pos {f : α → α} {l : List α} {i} (h : 0 < i) :
+    (l.modifyHead f).eraseIdx i = (l.eraseIdx i).modifyHead f := by cases l <;> cases i <;> simp_all
 
 @[simp] theorem modifyHead_id : modifyHead (id : α → α) = id := by funext l; cases l <;> simp
 
@@ -89,7 +92,7 @@ theorem eraseIdx_modifyHead_zero {f : α → α} {l : List α} :
   | _+1, [] => rfl
   | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
 
-theorem eraseIdx_eq_modifyTailIdx : ∀ n (l : List α), eraseIdx l n = modifyTailIdx tail n l
+theorem eraseIdx_eq_modifyTailIdx : ∀ i (l : List α), eraseIdx l i = modifyTailIdx tail i l
   | 0, l => by cases l <;> rfl
   | _+1, [] => rfl
   | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
@@ -105,7 +108,7 @@ theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
   induction l₁ <;> simp [*, Nat.succ_add]
 
 theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
-    ∀ n l, modifyTailIdx f n l = take n l ++ f (drop n l)
+    ∀ i l, modifyTailIdx f i l = take i l ++ f (drop i l)
   | 0, _ => rfl
   | _ + 1, [] => H.symm
   | n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
@@ -152,39 +155,39 @@ theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
     l.modify f n = [] ↔ l = [] := by cases l <;> cases n <;> simp
 
 theorem getElem?_modify (f : α → α) :
-    ∀ n (l : List α) m, (modify f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
+    ∀ i (l : List α) j, (modify f i l)[j]? = (fun a => if i = j then f a else a) <$> l[j]?
   | n, l, 0 => by cases l <;> cases n <;> simp
   | n, [], _+1 => by cases n <;> rfl
-  | 0, _ :: l, m+1 => by cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]
-  | n+1, a :: l, m+1 => by
+  | 0, _ :: l, j+1 => by cases h : l[j]? <;> simp [h, modify, j.succ_ne_zero.symm]
+  | i+1, a :: l, j+1 => by
     simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
-    refine (getElem?_modify f n l m).trans ?_
-    cases h' : l[m]? <;> by_cases h : n = m <;>
+    refine (getElem?_modify f i l j).trans ?_
+    cases h' : l[j]? <;> by_cases h : i = j <;>
       simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
 
-@[simp] theorem length_modify (f : α → α) : ∀ n l, length (modify f n l) = length l :=
+@[simp] theorem length_modify (f : α → α) : ∀ i l, length (modify f i l) = length l :=
   length_modifyTailIdx _ fun l => by cases l <;> rfl
 
-@[simp] theorem getElem?_modify_eq (f : α → α) (n) (l : List α) :
-    (modify f n l)[n]? = f <$> l[n]? := by
+@[simp] theorem getElem?_modify_eq (f : α → α) (i) (l : List α) :
+    (modify f i l)[i]? = f <$> l[i]? := by
   simp only [getElem?_modify, if_pos]
 
-@[simp] theorem getElem?_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
-    (modify f m l)[n]? = l[n]? := by
+@[simp] theorem getElem?_modify_ne (f : α → α) {i j} (l : List α) (h : i ≠ j) :
+    (modify f i l)[j]? = l[j]? := by
   simp only [getElem?_modify, if_neg h, id_map']
 
-theorem getElem_modify (f : α → α) (n) (l : List α) (m) (h : m < (modify f n l).length) :
-    (modify f n l)[m] =
-      if n = m then f (l[m]'(by simp at h; omega)) else l[m]'(by simp at h; omega) := by
+theorem getElem_modify (f : α → α) (i) (l : List α) (j) (h : j < (modify f i l).length) :
+    (modify f i l)[j] =
+      if i = j then f (l[j]'(by simp at h; omega)) else l[j]'(by simp at h; omega) := by
   rw [getElem_eq_iff, getElem?_modify]
   simp at h
   simp [h]
 
-@[simp] theorem getElem_modify_eq (f : α → α) (n) (l : List α) (h) :
-    (modify f n l)[n] = f (l[n]'(by simpa using h)) := by simp [getElem_modify]
+@[simp] theorem getElem_modify_eq (f : α → α) (i) (l : List α) (h) :
+    (modify f i l)[i] = f (l[i]'(by simpa using h)) := by simp [getElem_modify]
 
-@[simp] theorem getElem_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) (h') :
-    (modify f m l)[n] = l[n]'(by simpa using h') := by simp [getElem_modify, h]
+@[simp] theorem getElem_modify_ne (f : α → α) {i j} (l : List α) (h : i ≠ j) (h') :
+    (modify f i l)[j] = l[j]'(by simpa using h') := by simp [getElem_modify, h]
 
 theorem modify_eq_self {f : α → α} {n} {l : List α} (h : l.length ≤ n) :
     l.modify f n = l := by
@@ -211,8 +214,8 @@ theorem modify_modify_ne (f g : α → α) {m n} (l : List α) (h : m ≠ n) :
     simp only [getElem_modify, getElem_modify_ne, h₂]
     split <;> split <;> first | rfl | omega
 
-theorem modify_eq_set [Inhabited α] (f : α → α) (n) (l : List α) :
-    modify f n l = l.set n (f (l[n]?.getD default)) := by
+theorem modify_eq_set [Inhabited α] (f : α → α) (i) (l : List α) :
+    modify f i l = l.set i (f (l[i]?.getD default)) := by
   apply ext_getElem
   · simp
   · intro m h₁ h₂
@@ -224,11 +227,11 @@ theorem modify_eq_set [Inhabited α] (f : α → α) (n) (l : List α) :
     · rfl
 
 theorem modify_eq_take_drop (f : α → α) :
-    ∀ n l, modify f n l = take n l ++ modifyHead f (drop n l) :=
+    ∀ i l, modify f i l = take i l ++ modifyHead f (drop i l) :=
   modifyTailIdx_eq_take_drop _ rfl
 
-theorem modify_eq_take_cons_drop {f : α → α} {n} {l : List α} (h : n < l.length) :
-    modify f n l = take n l ++ f l[n] :: drop (n + 1) l := by
+theorem modify_eq_take_cons_drop {f : α → α} {i} {l : List α} (h : i < l.length) :
+    modify f i l = take i l ++ f l[i] :: drop (i + 1) l := by
   rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl
 
 theorem exists_of_modify (f : α → α) {n} {l : List α} (h : n < l.length) :
@@ -240,20 +243,20 @@ theorem exists_of_modify (f : α → α) {n} {l : List α} (h : n < l.length) :
 @[simp] theorem modify_id (n) (l : List α) : l.modify id n = l := by
   simp [modify]
 
-theorem take_modify (f : α → α) (n m) (l : List α) :
-    (modify f m l).take n = (take n l).modify f m := by
-  induction n generalizing l m with
+theorem take_modify (f : α → α) (i j) (l : List α) :
+    (modify f i l).take j = (take j l).modify f i := by
+  induction j generalizing l i with
   | zero => simp
   | succ n ih =>
     cases l with
     | nil => simp
     | cons hd tl =>
-      cases m with
+      cases i with
       | zero => simp
-      | succ m => simp [ih]
+      | succ i => simp [ih]
 
-theorem drop_modify_of_lt (f : α → α) (n m) (l : List α) (h : n < m) :
-    (modify f n l).drop m = l.drop m := by
+theorem drop_modify_of_lt (f : α → α) (i j) (l : List α) (h : i < j) :
+    (modify f i l).drop j = l.drop j := by
   apply ext_getElem
   · simp
   · intro m' h₁ h₂
@@ -261,16 +264,16 @@ theorem drop_modify_of_lt (f : α → α) (n m) (l : List α) (h : n < m) :
     intro h'
     omega
 
-theorem drop_modify_of_ge (f : α → α) (n m) (l : List α) (h : n ≥ m) :
-    (modify f n l).drop m = modify f (n - m) (drop m l) := by
+theorem drop_modify_of_ge (f : α → α) (i j) (l : List α) (h : i ≥ j) :
+    (modify f i l).drop j = modify f (i - j) (drop j l) := by
   apply ext_getElem
   · simp
   · intro m' h₁ h₂
     simp [getElem_drop, getElem_modify, ite_eq_right_iff]
     split <;> split <;> first | rfl | omega
 
-theorem eraseIdx_modify_of_eq (f : α → α) (n) (l : List α) :
-    (modify f n l).eraseIdx n = l.eraseIdx n := by
+theorem eraseIdx_modify_of_eq (f : α → α) (i) (l : List α) :
+    (modify f i l).eraseIdx i = l.eraseIdx i := by
   apply ext_getElem
   · simp [length_eraseIdx]
   · intro m h₁ h₂

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

@@ -12,31 +12,37 @@ import Init.Data.List.Pairwise
 # Lemmas about `List.Pairwise`
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
+set_option linter.listVariables false in
 /-- Given a list `is` of monotonically increasing indices into `l`, getting each index
   produces a sublist of `l`.  -/
 theorem map_getElem_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (· < ·)) :
     is.map (l[·]) <+ l := by
-  suffices ∀ n l', l' = l.drop n → (∀ i ∈ is, n ≤ i) → map (l[·]) is <+ l'
+  suffices ∀ j l', l' = l.drop j → (∀ i ∈ is, j ≤ i) → map (l[·]) is <+ l'
     from this 0 l (by simp) (by simp)
-  rintro n l' rfl his
-  induction is generalizing n with
+  rintro j l' rfl his
+  induction is generalizing j with
   | nil => simp
   | cons hd tl IH =>
     simp only [Fin.getElem_fin, map_cons]
     have := IH h.of_cons (hd+1) (pairwise_cons.mp h).1
     specialize his hd (.head _)
     have := (drop_eq_getElem_cons ..).symm ▸ this.cons₂ (get l hd)
-    have := Sublist.append (nil_sublist (take hd l |>.drop n)) this
+    have := Sublist.append (nil_sublist (take hd l |>.drop j)) this
     rwa [nil_append, ← (drop_append_of_le_length ?_), take_append_drop] at this
     simp [Nat.min_eq_left (Nat.le_of_lt hd.isLt), his]
 
+set_option linter.listVariables false in
 @[deprecated map_getElem_sublist (since := "2024-07-30")]
 theorem map_get_sublist {l : List α} {is : List (Fin l.length)} (h : is.Pairwise (·.val < ·.val)) :
     is.map (get l) <+ l := by
   simpa using map_getElem_sublist h
 
+set_option linter.listVariables false in
 /-- Given a sublist `l' <+ l`, there exists an increasing list of indices `is` such that
   `l' = is.map fun i => l[i]`. -/
 theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (Fin l.length),
@@ -52,11 +58,13 @@ theorem sublist_eq_map_getElem {l l' : List α} (h : l' <+ l) : ∃ is : List (F
     refine ⟨⟨0, by simp [Nat.zero_lt_succ]⟩ :: is.map (·.succ), ?_⟩
     simp [Function.comp_def, pairwise_map, IH, ← get_eq_getElem, get_cons_zero, get_cons_succ']
 
+set_option linter.listVariables false in
 @[deprecated sublist_eq_map_getElem (since := "2024-07-30")]
 theorem sublist_eq_map_get (h : l' <+ l) : ∃ is : List (Fin l.length),
     l' = map (get l) is ∧ is.Pairwise (· < ·) := by
   simpa using sublist_eq_map_getElem h
 
+set_option linter.listVariables false in
 theorem pairwise_iff_getElem : Pairwise R l ↔
     ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
   rw [pairwise_iff_forall_sublist]

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

@@ -7,6 +7,9 @@ prelude
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Perm
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-- Helper lemma for `set_set_perm`-/

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

@@ -14,6 +14,9 @@ import Init.Data.List.Erase
 # Lemmas about `List.range` and `List.enum`
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 open Nat
@@ -93,7 +96,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
     simp only [range'_succ]
     rw [cons_eq_append_iff]
     constructor
-    · rintro (⟨rfl, rfl⟩ | ⟨a, rfl, h⟩)
+    · rintro (⟨rfl, rfl⟩ | ⟨_, rfl, h⟩)
       · exact ⟨0, by simp [range'_succ]⟩
       · simp only [ih] at h
         obtain ⟨k, h, rfl, rfl⟩ := h
@@ -117,7 +120,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
   simp only [range'_eq_append_iff, eq_comm (a := i :: _), range'_eq_cons_iff]
   intro h
   constructor
-  · rintro ⟨as, ⟨x, k, h₁, rfl, rfl, h₂, rfl⟩, h₃⟩
+  · rintro ⟨as, ⟨_, k, h₁, rfl, rfl, h₂, rfl⟩, h₃⟩
     constructor
     · omega
     · simpa using h₃
@@ -177,7 +180,7 @@ theorem pairwise_lt_range (n : Nat) : Pairwise (· < ·) (range n) := by
 theorem pairwise_le_range (n : Nat) : Pairwise (· ≤ ·) (range n) :=
   Pairwise.imp Nat.le_of_lt (pairwise_lt_range _)
 
-@[simp] theorem take_range (m n : Nat) : take m (range n) = range (min m n) := by
+@[simp] theorem take_range (i n : Nat) : take i (range n) = range (min i n) := by
   apply List.ext_getElem
   · simp
   · simp +contextual [getElem_take, Nat.lt_min]
@@ -411,7 +414,7 @@ theorem fst_eq_of_mem_zipIdx {x : α × Nat} {l : List α} {k : Nat} (h : x ∈
   | nil => cases h
   | cons hd tl ih =>
     cases h with
-    | head h => simp
+    | head _ => simp
     | tail h m =>
       specialize ih m
       have : x.2 - k = x.2 - (k + 1) + 1 := by
@@ -462,12 +465,12 @@ theorem zipIdx_eq_append_iff {l : List α} {k : Nat} :
       ∃ 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⟩
+  · rintro ⟨ws, xs, ys, zs, 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, ?_⟩
+    refine ⟨ws, xs, rfl, ?_⟩
     simp only [zipIdx_eq_zip_range', length_append, true_and]
     congr
     omega
@@ -538,7 +541,7 @@ theorem snd_eq_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x
   | nil => cases h
   | cons hd tl ih =>
     cases h with
-    | head h => simp
+    | head _ => simp
     | tail h m =>
       specialize ih m
       have : x.1 - n = x.1 - (n + 1) + 1 := by
@@ -589,12 +592,12 @@ theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
       ∃ 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⟩
+  · rintro ⟨ws, xs, ys, zs, 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, ?_⟩
+    refine ⟨ys, zs, rfl, ?_⟩
     simp only [enumFrom_eq_zip_range', length_append, true_and]
     congr
     omega
@@ -624,7 +627,7 @@ theorem enum_length : (enum l).length = l.length :=
   enumFrom_length
 
 @[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
+theorem getElem?_enum (l : List α) (i : Nat) : (enum l)[i]? = l[i]?.map fun a => (i, a) := by
   rw [enum, getElem?_enumFrom, Nat.zero_add]
 
 @[deprecated getElem_zipIdx (since := "2025-01-21"), simp]

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

@@ -16,10 +16,13 @@ These are in a separate file from most of the lemmas about `List.IsSuffix`
 as they required importing more lemmas about natural numbers, and use `omega`.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
-theorem IsSuffix.getElem {x y : List α} (h : x <:+ y) {n} (hn : n < x.length) :
-    x[n] = y[y.length - x.length + n]'(by have := h.length_le; omega) := by
+theorem IsSuffix.getElem {xs ys : List α} (h : xs <:+ ys) {i} (hn : i < xs.length) :
+    xs[i] = ys[ys.length - xs.length + i]'(by have := h.length_le; omega) := by
   rw [getElem_eq_getElem_reverse, h.reverse.getElem, getElem_reverse]
   congr
   have := h.length_le
@@ -92,11 +95,11 @@ theorem suffix_iff_eq_append : l₁ <:+ l₂ ↔ take (length l₂ - length l₁
   ⟨by rintro ⟨r, rfl⟩; simp only [length_append, Nat.add_sub_cancel_right, take_left], fun e =>
     ⟨_, e⟩⟩
 
-theorem prefix_take_iff {x y : List α} {n : Nat} : x <+: y.take n ↔ x <+: y ∧ x.length ≤ n := by
+theorem prefix_take_iff {xs ys : List α} {i : Nat} : xs <+: ys.take i ↔ xs <+: ys ∧ xs.length ≤ i := by
   constructor
   · intro h
     constructor
-    · exact List.IsPrefix.trans h <| List.take_prefix n y
+    · exact List.IsPrefix.trans h <| List.take_prefix i ys
     · replace h := h.length_le
       rw [length_take, Nat.le_min] at h
       exact h.left
@@ -110,21 +113,21 @@ theorem suffix_iff_eq_drop : l₁ <:+ l₂ ↔ l₁ = drop (length l₂ - length
   ⟨fun h => append_cancel_left <| (suffix_iff_eq_append.1 h).trans (take_append_drop _ _).symm,
     fun e => e.symm ▸ drop_suffix _ _⟩
 
-theorem prefix_take_le_iff {L : List α} (hm : m < L.length) :
-    L.take m <+: L.take n ↔ m ≤ n := by
+theorem prefix_take_le_iff {xs : List α} (hm : i < xs.length) :
+    xs.take i <+: xs.take j ↔ i ≤ j := by
   simp only [prefix_iff_eq_take, length_take]
-  induction m generalizing L n with
+  induction i generalizing xs j with
   | zero => simp [Nat.min_eq_left, eq_self_iff_true, Nat.zero_le, take]
-  | succ m IH =>
-    cases L with
+  | succ i IH =>
+    cases xs with
     | nil => simp_all
-    | cons l ls =>
-      cases n with
+    | cons x xs =>
+      cases j with
       | zero =>
         simp
-      | succ n =>
+      | succ j =>
         simp only [length_cons, Nat.succ_eq_add_one, Nat.add_lt_add_iff_right] at hm
-        simp [← @IH n ls hm, Nat.min_eq_left, Nat.le_of_lt hm]
+        simp [← @IH j xs hm, Nat.min_eq_left, Nat.le_of_lt hm]
 
 @[simp] theorem append_left_sublist_self {xs : List α} (ys : List α) : xs ++ ys <+ ys ↔ xs = [] := by
   constructor

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

@@ -16,7 +16,8 @@ These are in a separate file from most of the list lemmas
 as they required importing more lemmas about natural numbers, and use `omega`.
 -/
 
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 
@@ -38,16 +39,16 @@ theorem length_take_of_le (h : i ≤ length l) : length (take i l) = i := by sim
 
 /-- 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. -/
-theorem getElem_take' (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
-    L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) :=
-  getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append_left ..
+theorem getElem_take' (xs : List α) {i j : Nat} (hi : i < xs.length) (hj : i < j) :
+    xs[i] = (xs.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) :=
+  getElem_of_eq (take_append_drop j xs).symm _ ▸ getElem_append_left ..
 
 /-- 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 small list to the big list. -/
-@[simp] theorem getElem_take (L : List α) {j i : Nat} {h : i < (L.take j).length} :
-    (L.take j)[i] =
-    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]
+@[simp] theorem getElem_take (xs : List α) {j i : Nat} {h : i < (xs.take j).length} :
+    (xs.take j)[i] =
+    xs[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
+  rw [length_take, Nat.lt_min] at h; rw [getElem_take' xs _ h.1]
 
 theorem getElem?_take_eq_none {l : List α} {i j : Nat} (h : i ≤ j) :
     (l.take i)[j]? = none :=
@@ -212,31 +213,31 @@ theorem take_subset_take_left (l : List α) {i j : Nat} (h : i ≤ j) : take i l
 
 /-! ### drop -/
 
-theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length := by
-  have A : i < L.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h
-  rw [(take_append_drop i L).symm] at h
+theorem lt_length_drop (xs : List α) {i j : Nat} (h : i + j < xs.length) : j < (xs.drop i).length := by
+  have A : i < xs.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h
+  rw [(take_append_drop i xs).symm] at h
   simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
     length_append] using h
 
 /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
 dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
-theorem getElem_drop' (L : List α) {i j : Nat} (h : i + j < L.length) :
-    L[i + j] = (L.drop i)[j]'(lt_length_drop L h) := by
-  have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
-  rw [getElem_of_eq (take_append_drop i L).symm h, getElem_append_right]
+theorem getElem_drop' (xs : List α) {i j : Nat} (h : i + j < xs.length) :
+    xs[i + j] = (xs.drop i)[j]'(lt_length_drop xs h) := by
+  have : i ≤ xs.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h)
+  rw [getElem_of_eq (take_append_drop i xs).symm h, getElem_append_right]
   · simp [Nat.min_eq_left this, Nat.add_sub_cancel_left]
   · simp [Nat.min_eq_left this, Nat.le_add_right]
 
 /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
 dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
-@[simp] theorem getElem_drop (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).length} :
-    (L.drop i)[j] = L[i + j]'(by
+@[simp] theorem getElem_drop (xs : List α) {i : Nat} {j : Nat} {h : j < (xs.drop i).length} :
+    (xs.drop i)[j] = xs[i + j]'(by
       rw [Nat.add_comm]
-      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h)) := by
+      exact Nat.add_lt_of_lt_sub (length_drop i xs ▸ h)) := by
   rw [getElem_drop']
 
 @[simp]
-theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := by
+theorem getElem?_drop (xs : List α) (i j : Nat) : (xs.drop i)[j]? = xs[i + j]? := by
   ext
   simp only [getElem?_eq_some_iff, getElem_drop, Option.mem_def]
   constructor <;> intro ⟨h, ha⟩
@@ -375,18 +376,18 @@ theorem take_reverse {α} {xs : List α} {i : Nat} :
   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 =>
+    next hd 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 - i = succ (xs_tl.length - i) from _, drop]
+      rw [show tl.length + 1 - i = succ (tl.length - i) from _, drop]
       · rwa [succ_eq_add_one, Nat.sub_add_comm]
       · rwa [length_reverse]
     | inr h' =>
       subst h'
       rw [length, Nat.sub_self, drop]
-      suffices xs_tl.length + 1 = (xs_tl.reverse ++ [xs_hd]).length by
+      suffices tl.length + 1 = (tl.reverse ++ [hd]).length by
         rw [this, take_length, reverse_cons]
       rw [length_append, length_reverse]
       rfl

src/Init/Data/List/Range.lean

@@ -214,10 +214,10 @@ theorem getLast?_range (n : Nat) : (range n).getLast? = if n = 0 then none else
 /-! ### zipIdx -/
 
 @[simp]
-theorem zipIdx_eq_nil_iff {l : List α} {n : Nat} : List.zipIdx l n = [] ↔ l = [] := by
+theorem zipIdx_eq_nil_iff {l : List α} {i : Nat} : List.zipIdx l i = [] ↔ l = [] := by
   cases l <;> simp
 
-@[simp] theorem length_zipIdx : ∀ {l : List α} {n}, (zipIdx l n).length = l.length
+@[simp] theorem length_zipIdx : ∀ {l : List α} {i}, (zipIdx l i).length = l.length
   | [], _ => rfl
   | _ :: _, _ => congrArg Nat.succ length_zipIdx
 
@@ -231,16 +231,16 @@ theorem getElem?_zipIdx :
     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
+theorem getElem_zipIdx (l : List α) (j) (i : Nat) (h : i < (l.zipIdx j).length) :
+    (l.zipIdx j)[i] = (l[i]'(by simpa [length_zipIdx] using h), j + 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
+theorem tail_zipIdx (l : List α) (i : Nat) : (zipIdx l i).tail = zipIdx l.tail (i + 1) := by
+  induction l generalizing i with
   | nil => simp
   | cons _ l ih => simp [ih, zipIdx_cons]
 
@@ -248,44 +248,44 @@ 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
+theorem zipIdx_cons' (i : Nat) (x : α) (xs : List α) :
+    zipIdx (x :: xs) i = (x, i) :: (zipIdx xs i).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
+theorem zipIdx_map_snd (i) :
+    ∀ (l : List α), map Prod.snd (zipIdx l i) = range' i l.length
   | [] => rfl
   | _ :: _ => congrArg (cons _) (zipIdx_map_snd _ _)
 
 @[simp]
-theorem zipIdx_map_fst : ∀ (n) (l : List α), map Prod.fst (zipIdx l n) = l
+theorem zipIdx_map_fst : ∀ (i) (l : List α), map Prod.fst (zipIdx l i) = 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) :=
+theorem zipIdx_eq_zip_range' (l : List α) {i : Nat} : l.zipIdx i = l.zip (range' i 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
+theorem unzip_zipIdx_eq_prod (l : List α) {i : Nat} :
+    (l.zipIdx i).unzip = (l, range' i 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
+theorem zipIdx_succ (l : List α) (i : Nat) :
+    l.zipIdx (i + 1) = (l.zipIdx i).map (fun ⟨a, i⟩ => (a, i + 1)) := by
+  induction l generalizing i with
   | nil => rfl
-  | cons _ _ ih => simp only [zipIdx_cons, ih (n + 1), map_cons]
+  | cons _ _ ih => simp only [zipIdx_cons, ih (i + 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
+theorem zipIdx_eq_map_add (l : List α) (i : Nat) :
+    l.zipIdx i = l.zipIdx.map (fun ⟨a, j⟩ => (a, i + j)) := by
+  induction l generalizing i with
   | nil => rfl
-  | cons _ _ ih => simp [ih (n+1), zipIdx_succ, Nat.add_assoc, Nat.add_comm 1]
+  | cons _ _ ih => simp [ih (i+1), zipIdx_succ, Nat.add_assoc, Nat.add_comm 1]
 
 /-! ### enumFrom -/
 

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

@@ -14,6 +14,9 @@ These definitions are intended for verification purposes,
 and are replaced at runtime by efficient versions in `Init.Data.List.Sort.Impl`.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /--

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

@@ -31,6 +31,9 @@ as long as such improvements are carefully validated by benchmarking,
 they can be done without changing the theory, as long as a `@[csimp]` lemma is provided.
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 open List
 
 namespace List.MergeSort.Internal
@@ -76,18 +79,18 @@ def splitRevAt (n : Nat) (l : List α) : List α × List α := go l n [] where
   | x :: xs, n+1, acc => go xs n (x :: acc)
   | xs, _, acc => (acc, xs)
 
-theorem splitRevAt_go (xs : List α) (n : Nat) (acc : List α) :
-    splitRevAt.go xs n acc = ((take n xs).reverse ++ acc, drop n xs) := by
-  induction xs generalizing n acc with
+theorem splitRevAt_go (xs : List α) (i : Nat) (acc : List α) :
+    splitRevAt.go xs i acc = ((take i xs).reverse ++ acc, drop i xs) := by
+  induction xs generalizing i acc with
   | nil => simp [splitRevAt.go]
   | cons x xs ih =>
-    cases n with
+    cases i with
     | zero => simp [splitRevAt.go]
-    | succ n =>
-      rw [splitRevAt.go, ih n (x :: acc), take_succ_cons, reverse_cons, drop_succ_cons,
+    | succ i =>
+      rw [splitRevAt.go, ih i (x :: acc), take_succ_cons, reverse_cons, drop_succ_cons,
         append_assoc, singleton_append]
 
-theorem splitRevAt_eq (n : Nat) (l : List α) : splitRevAt n l = ((l.take n).reverse, l.drop n) := by
+theorem splitRevAt_eq (i : Nat) (l : List α) : splitRevAt i l = ((l.take i).reverse, l.drop i) := by
   rw [splitRevAt, splitRevAt_go, append_nil]
 
 /--

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

@@ -21,6 +21,9 @@ import Init.Data.Bool
 
 -/
 
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
 namespace List
 
 /-! ### splitInTwo -/
@@ -418,10 +421,10 @@ then `c` is still a sublist of `mergeSort le l`.
 theorem sublist_mergeSort
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
     (total : ∀ (a b : α), le a b || le b a) :
-    ∀ {c : List α} (_ : c.Pairwise le) (_ : c <+ l),
-    c <+ mergeSort l le
+    ∀ {ys : List α} (_ : ys.Pairwise le) (_ : ys <+ xs),
+    ys <+ mergeSort xs le
   | _, _, .slnil => nil_sublist _
-  | c, hc, @Sublist.cons _ _ l a h => by
+  | ys, hc, @Sublist.cons _ _ l a h => by
     obtain ⟨l₁, l₂, h₁, h₂, -⟩ := mergeSort_cons trans total a l
     rw [h₁]
     have h' := sublist_mergeSort trans total hc h
@@ -460,9 +463,9 @@ theorem map_merge {f : α → β} {r : α → α → Bool} {s : β → β → Bo
     (hl : ∀ a ∈ l, ∀ b ∈ l', r a b = s (f a) (f b)) :
     (l.merge l' r).map f = (l.map f).merge (l'.map f) s := by
   match l, l' with
-  | [], x' => simp
-  | x, [] => simp
-  | x :: xs, x' :: xs' =>
+  | [], _ => simp
+  | _, [] => simp
+  | _ :: _, _ :: _ =>
     simp only [List.forall_mem_cons] at hl
     simp only [forall_and] at hl
     simp only [List.map, List.cons_merge_cons]

src/Init/Data/List/ToArray.lean

@@ -182,7 +182,7 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
 @[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
   induction l generalizing as <;> simp [*]
 
-@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
+@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
   rw [foldr_eq_foldl_reverse, foldl_push]
 
 @[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :

src/Lean/Linter/List.lean

@@ -19,7 +19,9 @@ 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`.
+are `i`, `j`, or `k`,
+and similarly that the only variables appearing as a width (e.g. in `List.replicate n a` or `Vector α n`)
+are `n` or `m`.
 -/
 register_builtin_option linter.indexVariables : Bool := {
   defValue := false
@@ -51,8 +53,24 @@ def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
       | List.drop _ i _ => [i]
       | List.set _ _ i _ => [i]
       | List.insertIdx _ i _ _ => [i]
-      | List.eraseIdx _ _ i _ => [i]
+      | List.eraseIdx _ _ i => [i]
+      | List.modify _ _ i _ => [i]
       | List.zipIdx _ _ i => [i]
+      | Array.extract _ _ i j => [i, j]
+      | Array.set _ _ i _ => [i]
+      | Array.setIfInBounds _ _ i _ => [i]
+      | Array.insertIdx _ _ i _ _ => [i]
+      | Array.insertIdxIfInBounds _ _ i _ => [i]
+      | Array.eraseIdx _ _ i _ => [i]
+      | Array.eraseIdxIfInBounds _ _ i _ => [i]
+      | Array.modify _ i _ _ => [i]
+      | Array.zipIdx _ _ i => [i]
+      | Vector.extract _ _ _ i j => [i, j]
+      | Vector.set _ _ _ i _ => [i]
+      | Vector.setIfInBounds _ _ _ i _ => [i]
+      | Vector.insertIdx _ _ _ i _ _ => [i]
+      | Vector.eraseIdx _ _ _ i _ => [i]
+      | Vector.zipIdx _ _ _ i => [i]
       | _ => []
       match idxs with
       | [] => none
@@ -66,6 +84,111 @@ def numericalIndices (t : InfoTree) : List (Syntax × Name) :=
     else
       none).flatten
 
+/--
+Return the syntax for all expressions in which an `fvarId` appears as a "numerical width", along with the user name of that `fvarId`.
+-/
+def numericalWidths (t : InfoTree) : List (Syntax × Name) :=
+  (t.deepestNodes fun _ info _ => do
+    let stx := info.stx
+    if let .ofTermInfo info := info then
+      let idxs := match_expr info.expr with
+      | List.replicate _ n _ => [n]
+      | Array.mkArray _ n _ => [n]
+      | Vector.mkVector _ n _ => [n]
+      | List.range n => [n]
+      | List.range' _ n _ => [n]
+      | Array.range n => [n]
+      | Array.range' _ n _ => [n]
+      | Vector.range n => [n]
+      | Vector.range' _ n _ => [n]
+      | Vector _ n => [n]
+      | _ => []
+      match idxs with
+      | [] => none
+      | _ => idxs.filterMap fun i =>
+        match i with
+        | .fvar i =>
+          match info.lctx.find? i with
+          | some ldecl => some (stx, ldecl.userName)
+          | none => none
+        | _ => none
+    else
+      none).flatten
+
+/--
+Return the syntax for all expressions in which an `fvarId` appears as a "BitVec width", along with the user name of that `fvarId`.
+-/
+def bitVecWidths (t : InfoTree) : List (Syntax × Name) :=
+  (t.deepestNodes fun _ info _ => do
+    let stx := info.stx
+    if let .ofTermInfo info := info then
+      let idxs := match_expr info.expr with
+      | BitVec w => [w]
+      | _ => []
+      match idxs with
+      | [] => none
+      | _ => idxs.filterMap fun i =>
+        match i with
+        | .fvar i =>
+          match info.lctx.find? i with
+          | some ldecl => some (stx, ldecl.userName)
+          | none => none
+        | _ => none
+    else
+      none).flatten
+
+/-- Strip optional suffixes from a binder name. -/
+def stripBinderName (s : String) : String :=
+  s.stripSuffix "'" |>.stripSuffix "₁" |>.stripSuffix "₂" |>.stripSuffix "₃" |>.stripSuffix "₄"
+
+/-- Allowed names for index variables. -/
+def allowedIndices : List String := ["i", "j", "k", "start", "stop"]
+
+/-- Allowed names for width variables. -/
+def allowedWidths : List String := ["n", "m"]
+
+/-- Allowed names for BitVec width variables. -/
+def allowedBitVecWidths : List String := ["w"]
+
+/--
+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
+    -- We intentionally do not use `getLinterValue` here, as we do *not* want to opt in to `linter.all`.
+    unless (← getOptions).get linter.indexVariables.name false 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 let .str _ n := n then
+          if !allowedIndices.contains (stripBinderName n) then
+            Linter.logLint linter.indexVariables idxStx
+              m!"Forbidden variable appearing as an index: use `i`, `j`, or `k`: {n}"
+      -- for (idxStx, n) in numericalWidths t do
+      --   if let .str _ n := n then
+      --     if !allowedWidths.contains (stripBinderName n) then
+      --       Linter.logLint linter.indexVariables idxStx
+      --         m!"Forbidden variable appearing as a width: use `n` or `m`: {n}"
+      -- for (idxStx, n) in bitVecWidths t do
+      --   if let .str _ n := n then
+      --     if !allowedBitVecWidths.contains (stripBinderName n) then
+      --       Linter.logLint linter.indexVariables idxStx
+      --         m!"Forbidden variable appearing as a BitVec width: use `w`: {n}"
+
+builtin_initialize addLinter indexLinter
+
+/-- Allowed names for `List` variables. -/
+def allowedListNames : List String := ["l", "r", "s", "t", "tl", "ws", "xs", "ys", "zs", "as", "bs", "cs", "ds", "acc"]
+
+/-- Allowed names for `Array` variables. -/
+def allowedArrayNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs", "acc"]
+
+/-- Allowed names for `Vector` variables. -/
+def allowedVectorNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs"]
+
 /-- Find all binders appearing in the given info tree. -/
 def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) : IO (List (Syntax × Name × Expr)) :=
   t.collectTermInfoM fun ctx ti => do
@@ -86,42 +209,6 @@ def binders (t : InfoTree) (p : Expr → Bool := fun _ => true) : IO (List (Synt
     else
       return none
 
-/-- Allowed names for index variables. -/
-def allowedIndices : List String := ["i", "j", "k"]
-
-/--
-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
-    -- We intentionally do not use `getLinterValue` here, as we do *not* want to opt in to `linter.all`.
-    unless (← getOptions).get linter.indexVariables.name false 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 let .str _ n := n then
-          if !allowedIndices.contains n then
-            Linter.logLint linter.indexVariables idxStx
-              m!"Forbidden variable appearing as an index: use `i`, `j`, or `k`: {n}"
-
-builtin_initialize addLinter indexLinter
-
-/-- Strip optional suffixes from a binder name. -/
-def stripBinderName (s : String) : String :=
-  s.stripSuffix "'" |>.stripSuffix "₁" |>.stripSuffix "₂" |>.stripSuffix "₃"
-
-/-- Allowed names for `List` variables. -/
-def allowedListNames : List String := ["l", "r", "s", "t", "tl", "ws", "xs", "ys", "zs", "as", "bs", "cs", "acc"]
-
-/-- Allowed names for `Array` variables. -/
-def allowedArrayNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs"]
-
-/-- Allowed names for `Vector` variables. -/
-def allowedVectorNames : List String := ["ws", "xs", "ys", "zs", "as", "bs", "cs"]
-
 /--
 A linter which validates that all `List`/`Array`/`Vector` variables use allowed names.
 -/
@@ -137,7 +224,7 @@ def listVariablesLinter : Linter
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedListNames.contains n then
-            unless (ty.getArg! 0).isAppOf `List && n == "L" do
+            unless (ty.getArg! 0).isAppOf `List && (n == "L" || n == "xss") do
               Linter.logLint linter.listVariables stx
                 m!"Forbidden variable appearing as a `List` name: {n}"
         for (stx, n, _) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do

tests/lean/run/list_name_linter.lean

@@ -13,14 +13,14 @@ example (l₁ : List Nat) : l₁ = l₁ := rfl
 example (l₂ : List Nat) : l₂ = l₂ := rfl
 
 /--
-warning: Forbidden variable appearing as a `List` name: l₄
+warning: Forbidden variable appearing as a `List` name: l₅
 note: this linter can be disabled with `set_option linter.listVariables false`
 ---
-warning: Forbidden variable appearing as a `List` name: l₄
+warning: Forbidden variable appearing as a `List` name: l₅
 note: this linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
-example (l₄ : List Nat) : l₄ = l₄ := rfl
+example (l₅ : List Nat) : l₅ = l₅ := rfl
 
 #guard_msgs in
 example (xs : List Nat) : xs = xs := rfl