this is tedious

src/Init/Data/Array/Attach.lean

@@ -8,8 +8,9 @@ import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Count
 import Init.Data.List.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.
+
+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 Array
 

src/Init/Data/Array/Basic.lean

@@ -14,8 +14,8 @@ import Init.GetElem
 import Init.Data.List.ToArrayImpl
 import Init.Data.Array.Set
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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.
 
 universe u v w
 

src/Init/Data/Array/BasicAux.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.NotationExtra
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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.
 
 theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by
   simp only [push, mk.injEq] at h

src/Init/Data/Array/BinSearch.lean

@@ -9,7 +9,7 @@ import Init.Data.Int.DivMod.Lemmas
 import Init.Omega
 universe u v
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- We do not use `linter.indexVariables` here as it is helpful to name the index variables as `lo`, `mid`, and `hi`.
 
 namespace Array

src/Init/Data/Array/Bootstrap.lean

@@ -13,8 +13,8 @@ import Init.Data.List.TakeDrop
 This file contains some theorems about `Array` and `List` needed for `Init.Data.List.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.
+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 Array
 

src/Init/Data/Array/Count.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Nat.Count
 # Lemmas about `Array.countP` and `Array.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.
+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 Array
 

src/Init/Data/Array/DecidableEq.lean

@@ -9,8 +9,8 @@ import Init.Data.BEq
 import Init.Data.List.Nat.BEq
 import Init.ByCases
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 

src/Init/Data/Array/Erase.lean

@@ -12,8 +12,8 @@ import Init.Data.List.Nat.Basic
 # Lemmas about `Array.eraseP`, `Array.erase`, and `Array.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.
+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 Array
 

src/Init/Data/Array/Extract.lean

@@ -13,8 +13,8 @@ import Init.Data.List.Nat.TakeDrop
 This file follows the contents of `Init.Data.List.TakeDrop` and `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.
+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 Array

src/Init/Data/Array/FinRange.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.FinRange
 import Init.Data.Array.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.
+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 Array
 

src/Init/Data/Array/Find.lean

@@ -13,8 +13,8 @@ import Init.Data.Array.Range
 # Lemmas about `Array.findSome?`, `Array.find?, `Array.findIdx`, `Array.findIdx?`, `Array.idxOf`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 
 open Nat

src/Init/Data/Array/GetLit.lean

@@ -7,8 +7,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.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.
+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 Array
 

src/Init/Data/Array/InsertIdx.lean

@@ -13,8 +13,8 @@ import Init.Data.List.Nat.InsertIdx
 Proves various lemmas about `Array.insertIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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.
 
 open Function
 

src/Init/Data/Array/InsertionSort.lean

@@ -6,8 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.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.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 @[inline] def Array.insertionSort (xs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α :=
   traverse xs 0 xs.size

src/Init/Data/Array/Lemmas.lean

@@ -22,8 +22,8 @@ import Init.Data.List.ToArray
 ## Theorems about `Array`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 
@@ -833,9 +833,9 @@ theorem getElem?_set (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) (j : N
   cases xs
   simp
 
-@[simp] theorem set_eq_empty_iff {xs : Array α} (n : Nat) (a : α) (h) :
-     xs.set n a = #[] ↔ xs = #[] := by
-  cases xs <;> cases n <;> simp [set]
+@[simp] theorem set_eq_empty_iff {xs : Array α} (i : Nat) (a : α) (h) :
+     xs.set i a = #[] ↔ xs = #[] := by
+  cases xs <;> cases i <;> simp [set]
 
 theorem set_comm (a b : α)
     {i j : Nat} (xs : Array α) {hi : i < xs.size} {hj : j < (xs.set i a).size} (h : i ≠ j) :
@@ -2021,7 +2021,7 @@ theorem flatten_eq_flatMap {xss : Array (Array α)} : flatten xss = xss.flatMap
   rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
 theorem flatten_filter_not_isEmpty {xss : Array (Array α)} :
-    flatten (xss.filter fun l => !l.isEmpty) = xss.flatten := by
+    flatten (xss.filter fun xs => !xs.isEmpty) = xss.flatten := by
   induction xss using array₂_induction
   simp [List.filter_map, Function.comp_def, List.flatten_filter_not_isEmpty]
 

src/Init/Data/Array/Lex/Basic.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Range
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 

src/Init/Data/Array/Lex/Lemmas.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Lex
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 

src/Init/Data/Array/MapIdx.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.List.MapIdx
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 

src/Init/Data/Array/Mem.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.Data.List.BasicAux
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 

src/Init/Data/Array/Monadic.lean

@@ -12,8 +12,8 @@ import Init.Data.List.Monadic
 # Lemmas about `Array.forIn'` and `Array.forIn`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 

src/Init/Data/Array/OfFn.lean

@@ -11,8 +11,8 @@ import Init.Data.List.OfFn
 # Theorems about `Array.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.
+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 Array
 

src/Init/Data/Array/Perm.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.List.Nat.Perm
 import Init.Data.Array.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.
+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 Array
 

src/Init/Data/Array/QSort.lean

@@ -7,7 +7,7 @@ prelude
 import Init.Data.Vector.Basic
 import Init.Data.Ord
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
 
 namespace Array

src/Init/Data/Array/Range.lean

@@ -15,8 +15,8 @@ import Init.Data.List.Nat.Range
 
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 
@@ -149,9 +149,9 @@ theorem range_succ (n : Nat) : range (succ n) = range n ++ #[n] := by
       dite_eq_ite]
     split <;> omega
 
-theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
+theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by
   rw [← range'_eq_map_range]
-  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm
+  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm
 
 theorem reverse_range' (s n : Nat) : reverse (range' s n) = map (s + n - 1 - ·) (range n) := by
   simp [← toList_inj, List.reverse_range']
@@ -164,7 +164,7 @@ theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp
 
 theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp
 
-@[simp] theorem take_range (m n : Nat) : take (range n) m = range (min m n) := by
+@[simp] theorem take_range (i n : Nat) : take (range n) i = range (min i n) := by
   ext <;> simp
 
 @[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :

src/Init/Data/Array/Set.lean

@@ -6,8 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro
 prelude
 import Init.Tactics
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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.
 
 
 /--

src/Init/Data/Array/Subarray.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 universe u v w
 

src/Init/Data/Array/Subarray/Split.lean

@@ -15,8 +15,8 @@ automation. Placing them in another module breaks an import cycle, because `omeg
 array library.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Subarray
 /--

src/Init/Data/Array/TakeDrop.lean

@@ -12,8 +12,8 @@ These lemmas are used in the internals of HashMap.
 They should find a new home and/or be reformulated.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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
 

src/Init/Data/Array/Zip.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Zip
 # Lemmas about `Array.zip`, `Array.zipWith`, `Array.zipWithAll`, and `Array.unzip`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 
@@ -114,7 +114,7 @@ theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (cs : A
   cases ds
   simp [List.map_zipWith]
 
-theorem take_zipWith : (zipWith f as bs).take n = zipWith f (as.take n) (bs.take n) := by
+theorem take_zipWith : (zipWith f as bs).take i = zipWith f (as.take i) (bs.take i) := by
   cases as
   cases bs
   simp [List.take_zipWith]

src/Init/Data/List/Attach.lean

@@ -8,8 +8,8 @@ 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.
+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/Basic.lean

@@ -58,8 +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.
+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
 

src/Init/Data/List/BasicAux.lean

@@ -6,8 +6,8 @@ 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.
+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
 

src/Init/Data/List/Control.lean

@@ -9,8 +9,8 @@ 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.
+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,8 +10,8 @@ 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.
+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/Erase.lean

@@ -12,8 +12,8 @@ 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.
+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/FinRange.lean

@@ -6,8 +6,8 @@ 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.
+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/Find.lean

@@ -15,8 +15,8 @@ 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.
+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/Impl.lean

@@ -16,8 +16,8 @@ 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.
+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/Lemmas.lean

@@ -74,8 +74,8 @@ Also
 
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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
 

src/Init/Data/List/Lex.lean

@@ -7,8 +7,8 @@ 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.
+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/MapIdx.lean

@@ -11,8 +11,8 @@ 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.
+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/MinMax.lean

@@ -10,8 +10,8 @@ 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.
+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/Monadic.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Attach
 # 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.
+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/Nat/BEq.lean

@@ -7,8 +7,8 @@ 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.
+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/Nat/Basic.lean

@@ -15,8 +15,8 @@ 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.
+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
 

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

@@ -7,8 +7,8 @@ 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.
+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/Nat/Erase.lean

@@ -7,8 +7,8 @@ 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.
+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/Nat/Find.lean

@@ -7,8 +7,8 @@ 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.
+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/Nat/InsertIdx.lean

@@ -12,8 +12,8 @@ import Init.Data.List.Nat.Modify
 Proves various lemmas about `List.insertIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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.
 
 open Function Nat
 

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

@@ -8,8 +8,8 @@ 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.
+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/Nat/Pairwise.lean

@@ -12,8 +12,8 @@ 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.
+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/Nat/Perm.lean

@@ -7,8 +7,8 @@ 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.
+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/Nat/Range.lean

@@ -14,8 +14,8 @@ 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.
+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/Nat/Sublist.lean

@@ -16,8 +16,8 @@ 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.
+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/Nat/TakeDrop.lean

@@ -16,8 +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.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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
 
@@ -115,12 +115,12 @@ theorem take_set_of_le (a : α) {i j : Nat} (l : List α) (h : j ≤ i) :
 @[deprecated take_set_of_le (since := "2025-02-04")]
 abbrev take_set_of_lt := @take_set_of_le
 
-@[simp] theorem take_replicate (a : α) : ∀ i j : Nat, take i (replicate j a) = replicate (min i j) a
+@[simp] theorem take_replicate (a : α) : ∀ i n : Nat, take i (replicate n a) = replicate (min i n) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
   | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]
 
-@[simp] theorem drop_replicate (a : α) : ∀ i j : Nat, drop i (replicate j a) = replicate (j - i) a
+@[simp] theorem drop_replicate (a : α) : ∀ i n : Nat, drop i (replicate n a) = replicate (n - i) a
   | n, 0 => by simp
   | 0, m => by simp
   | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]

src/Init/Data/List/Notation.lean

@@ -11,8 +11,8 @@ import Init.Data.Nat.Div.Basic
 -/
 
 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.
+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
 

src/Init/Data/List/OfFn.lean

@@ -11,8 +11,8 @@ import Init.Data.Fin.Fold
 # Theorems about `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.
+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/Pairwise.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Attach
 # Lemmas about `List.Pairwise` and `List.Nodup`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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
 

src/Init/Data/List/Perm.lean

@@ -18,8 +18,8 @@ another.
 The notation `~` is used for permutation equivalence.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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.
 
 open Nat
 

src/Init/Data/List/Range.lean

@@ -14,8 +14,8 @@ Most of the results are deferred to `Data.Init.List.Nat.Range`, where more resul
 natural arithmetic are available.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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
 
@@ -74,7 +74,7 @@ theorem mem_range' : ∀{n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step *
     rw [exists_comm]; simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
 
 theorem getElem?_range' (s step) :
-    ∀ {i j : Nat}, i < j → (range' s j step)[i]? = some (s + step * i)
+    ∀ {i n : Nat}, i < n → (range' s n step)[i]? = some (s + step * i)
   | 0, n + 1, _ => by simp [range'_succ]
   | m + 1, n + 1, h => by
     simp only [range'_succ, getElem?_cons_succ]
@@ -147,10 +147,10 @@ theorem range_loop_range' : ∀ s n : Nat, range.loop s (range' s n) = range' 0
 theorem range_eq_range' (n : Nat) : range n = range' 0 n :=
   (range_loop_range' n 0).trans <| by rw [Nat.zero_add]
 
-theorem getElem?_range {i j : Nat} (h : i < j) : (range j)[i]? = some i := by
+theorem getElem?_range {i n : Nat} (h : i < n) : (range n)[i]? = some i := by
   simp [range_eq_range', getElem?_range' _ _ h]
 
-@[simp] theorem getElem_range {i : Nat} (j) (h : j < (range i).length) : (range i)[j] = j := by
+@[simp] theorem getElem_range {n : Nat} (j) (h : j < (range n).length) : (range n)[j] = j := by
   simp [range_eq_range']
 
 theorem range_succ_eq_map (n : Nat) : range (n + 1) = 0 :: map succ (range n) := by
@@ -183,9 +183,9 @@ theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by
 theorem range_succ (n : Nat) : range (succ n) = range n ++ [n] := by
   simp only [range_eq_range', range'_1_concat, Nat.zero_add]
 
-theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
+theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by
   rw [← range'_eq_map_range]
-  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm
+  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm
 
 theorem head?_range (n : Nat) : (range n).head? = if n = 0 then none else some 0 := by
   induction n with

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

@@ -14,8 +14,8 @@ 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.
+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,8 +31,8 @@ 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.
+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
 

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

@@ -21,8 +21,8 @@ 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.
+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/Sublist.lean

@@ -11,8 +11,8 @@ import Init.Data.List.TakeDrop
 # Lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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
 

src/Init/Data/List/TakeDrop.lean

@@ -10,8 +10,8 @@ import Init.Data.List.Lemmas
 # Lemmas about `List.take` and `List.drop`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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
 

src/Init/Data/List/ToArray.lean

@@ -15,8 +15,8 @@ import Init.Data.Array.Lex.Basic
 We prefer to pull `List.toArray` outwards past `Array` operations.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Array
 

src/Init/Data/List/ToArrayImpl.lean

@@ -6,8 +6,8 @@ Authors: Henrik Böving
 prelude
 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.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 /--
 Auxiliary definition for `List.toArray`.

src/Init/Data/List/Zip.lean

@@ -11,8 +11,8 @@ import Init.Data.Function
 # Lemmas about `List.zip`, `List.zipWith`, `List.zipWithAll`, and `List.unzip`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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
 

src/Init/Data/Vector/Count.lean

@@ -11,8 +11,8 @@ import Init.Data.Vector.Lemmas
 # Lemmas about `Vector.countP` and `Vector.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.
+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 Vector
 
@@ -101,6 +101,7 @@ theorem countP_set (p : α → Bool) (xs : Vector α n) (i : Nat) (a : α) (h :
   rcases xs with ⟨xs, rfl⟩
   simp
 
+set_option linter.listVariables false in -- This can probably be removed later.
 @[simp] theorem countP_flatten (xss : Vector (Vector α m) n) :
     countP p xss.flatten = (xss.map (countP p)).sum := by
   rcases xss with ⟨xss, rfl⟩
@@ -159,6 +160,7 @@ theorem count_le_count_push (a b : α) (xs : Vector α n) : count a xs ≤ count
     count a (xs ++ ys) = count a xs + count a ys :=
   countP_append ..
 
+set_option linter.listVariables false in -- This can probably be removed later.
 @[simp] theorem count_flatten (a : α) (xss : Vector (Vector α m) n) :
     count a xss.flatten = (xss.map (count a)).sum := by
   rcases xss with ⟨xss, rfl⟩

src/Init/Data/Vector/DecidableEq.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.Array.DecidableEq
 import Init.Data.Vector.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.
+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 Vector
 

src/Init/Data/Vector/Erase.lean

@@ -11,8 +11,8 @@ import Init.Data.Array.Erase
 # Lemmas about `Vector.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.
+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 Vector
 

src/Init/Data/Vector/Extract.lean

@@ -11,8 +11,8 @@ import Init.Data.Array.Extract
 # Lemmas about `Vector.extract`
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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.
 
 open Nat
 

src/Init/Data/Vector/FinRange.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.Array.FinRange
 import Init.Data.Vector.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.
+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 Vector
 

src/Init/Data/Vector/InsertIdx.lean

@@ -13,8 +13,8 @@ import Init.Data.Array.InsertIdx
 Proves various lemmas about `Vector.insertIdx`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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.
 
 open Function Nat
 

src/Init/Data/Vector/Lemmas.lean

@@ -12,6 +12,7 @@ import Init.Data.Array.Find
 ## Vectors
 Lemmas about `Vector α n`
 -/
+
 -- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 -- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
@@ -2369,8 +2370,8 @@ theorem back?_eq_some_iff {xs : Vector α n} {a : α} :
 
 @[simp] theorem back_append_of_neZero {xs : Vector α n} {ys : Vector α m} [NeZero m] :
     (xs ++ ys).back = ys.back := by
-  rcases xs with ⟨l⟩
-  rcases ys with ⟨l'⟩
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
   simp only [mk_append_mk, back_mk]
   rw [Array.back_append_of_size_pos]
 
@@ -2416,6 +2417,7 @@ theorem back?_flatMap {xs : Vector α n} {f : α → Vector β m} :
   simp [Array.back?_flatMap]
   rfl
 
+set_option linter.listVariables false in -- This can probably be removed later.
 theorem back?_flatten {xss : Vector (Vector α m) n} :
     (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
   rcases xss with ⟨xss, rfl⟩

src/Init/Data/Vector/Lex.lean

@@ -8,8 +8,8 @@ import Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 import Init.Data.Array.Lex.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.
+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 Vector
 

src/Init/Data/Vector/MapIdx.lean

@@ -8,8 +8,8 @@ import Init.Data.Array.MapIdx
 import Init.Data.Vector.Attach
 import Init.Data.Vector.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.
+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 Vector
 

src/Init/Data/Vector/Monadic.lean

@@ -13,8 +13,8 @@ import Init.Control.Lawful.Lemmas
 # Lemmas about `Vector.forIn'` and `Vector.forIn`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Vector
 

src/Init/Data/Vector/OfFn.lean

@@ -11,8 +11,8 @@ import Init.Data.Array.OfFn
 # Theorems about `Vector.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.
+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 Vector
 

src/Init/Data/Vector/Range.lean

@@ -14,8 +14,8 @@ import Init.Data.Array.Range
 
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Vector
 

src/Init/Data/Vector/Zip.lean

@@ -11,8 +11,8 @@ import Init.Data.Vector.Lemmas
 # Lemmas about `Vector.zip`, `Vector.zipWith`, `Vector.zipWithAll`, and `Vector.unzip`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- 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 Vector
 

src/Lean/Linter/List.lean

@@ -237,20 +237,23 @@ 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" || n == "xss") do
+            -- Allow `L` or `xss` for `List (List α)` or `List (Array α)`
+            unless ((ty.getArg! 0).isAppOf `List || (ty.getArg! 0).isAppOf `Array) && (n == "L" || n == "xss") do
               Linter.logLint linter.listVariables stx
                 m!"Forbidden variable appearing as a `List` name: {n}"
         for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Array do
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedArrayNames.contains n then
-            unless (ty.getArg! 0).isAppOf `Array && n == "xss" do
+            -- Allow `xss` for `Array (Array α)` or `Array (Vector α)`
+            unless ((ty.getArg! 0).isAppOf `Array || (ty.getArg! 0).isAppOf `Vector) && n == "xss" do
               Linter.logLint linter.listVariables stx
                 m!"Forbidden variable appearing as a `Array` name: {n}"
         for (stx, n, ty) in binders.filter fun (_, _, ty) => ty.isAppOf `Vector do
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedVectorNames.contains n then
+            -- Allow `xss` for `Vector (Vector α)`
             unless (ty.getArg! 0).isAppOf `Vector && n == "xss" do
               Linter.logLint linter.listVariables stx
                 m!"Forbidden variable appearing as a `Vector` name: {n}"