complete fmod/tmod/emod comparisons

src/Init/Data/Array/Attach.lean

@@ -8,9 +8,8 @@ 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
 
@@ -1090,11 +1090,6 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
-def replace [BEq α] (xs : Array α) (a b : α) : Array α :=
-  match xs.finIdxOf? a with
-  | none => xs
-  | some i => xs.set i b
-
 /-! ### Lexicographic ordering -/
 
 instance instLT [LT α] : LT (Array α) := ⟨fun as bs => as.toList < bs.toList⟩
@@ -1107,20 +1102,6 @@ instance instLE [LT α] : LE (Array α) := ⟨fun as bs => as.toList ≤ bs.toLi
 We do not currently intend to provide verification theorems for these functions.
 -/
 
-/-! ### leftpad and rightpad -/
-
-/--
-Pads `l : Array α` on the left with repeated occurrences of `a : α` until it is of size `n`.
-If `l` is initially larger than `n`, just return `l`.
--/
-def leftpad (n : Nat) (a : α) (xs : Array α) : Array α := mkArray (n - xs.size) a ++ xs
-
-/--
-Pads `l : Array α` on the right with repeated occurrences of `a : α` until it is of size `n`.
-If `l` is initially larger than `n`, just return `l`.
--/
-def rightpad (n : Nat) (a : α) (xs : Array α) : Array α := xs ++ mkArray (n - xs.size) a
-
 /- ### reduceOption -/
 
 /-- Drop `none`s from a Array, and replace each remaining `some a` with `a`. -/

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
@@ -99,6 +99,11 @@ theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
   simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
+theorem back?_flatten {xss : Array (Array α)} :
+    (flatten xss).back? = (xss.findSomeRev? fun xs => xs.back?) := by
+  cases xss using array₂_induction
+  simp [List.getLast?_flatten, ← List.map_reverse, List.findSome?_map, Function.comp_def]
+
 theorem findSome?_mkArray : findSome? f (mkArray n a) = if n = 0 then none else f a := by
   simp [← List.toArray_replicate, List.findSome?_replicate]
 
@@ -299,6 +304,24 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
   rcases xs with ⟨xs⟩
   simp [List.find?_eq_some_iff_getElem]
 
+/-! ### findFinIdx? -/
+
+@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := rfl
+
+-- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
+theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
+    findFinIdx? p xs = (findFinIdx? p ys).map (fun i => i.cast (by simp [w])) := by
+  subst w
+  simp
+
+@[simp] theorem findFinIdx?_subtype {p : α → Prop} {xs : Array { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    xs.findFinIdx? f = (xs.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
+  cases xs
+  simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
+  rw [findFinIdx?_congr List.unattach_toArray]
+  simp [Function.comp_def]
+
 /-! ### findIdx -/
 
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
@@ -524,47 +547,6 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
   cases xs
   simp
 
-/-! ### findFinIdx? -/
-
-@[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := rfl
-
--- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
-theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
-    findFinIdx? p xs = (findFinIdx? p ys).map (fun i => i.cast (by simp [w])) := by
-  subst w
-  simp
-
-theorem findFinIdx?_eq_pmap_findIdx? {xs : Array α} {p : α → Bool} :
-    xs.findFinIdx? p =
-      (xs.findIdx? p).pmap
-        (fun i m => by simp [findIdx?_eq_some_iff_getElem] at m; exact ⟨i, m.choose⟩)
-        (fun i h => h) := by
-  simp [findIdx?_eq_map_findFinIdx?_val, Option.pmap_map]
-
-@[simp] theorem findFinIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
-    xs.findFinIdx? p = none ↔ ∀ x, x ∈ xs → ¬ p x := by
-  simp [findFinIdx?_eq_pmap_findIdx?]
-
-@[simp]
-theorem findFinIdx?_eq_some_iff {xs : Array α} {p : α → Bool} {i : Fin xs.size} :
-    xs.findFinIdx? p = some i ↔
-      p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji i.2)) := by
-  simp only [findFinIdx?_eq_pmap_findIdx?, Option.pmap_eq_some_iff, findIdx?_eq_some_iff_getElem,
-    Bool.not_eq_true, Option.mem_def, exists_and_left, and_exists_self, Fin.getElem_fin]
-  constructor
-  · rintro ⟨a, ⟨h, w₁, w₂⟩, rfl⟩
-    exact ⟨w₁, fun j hji => by simpa using w₂ j hji⟩
-  · rintro ⟨h, w⟩
-    exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
-
-@[simp] theorem findFinIdx?_subtype {p : α → Prop} {xs : Array { x // p x }}
-    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
-    xs.findFinIdx? f = (xs.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
-  cases xs
-  simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
-  rw [findFinIdx?_congr List.unattach_toArray]
-  simp [Function.comp_def]
-
 /-! ### idxOf
 
 The verification API for `idxOf` is still incomplete.
@@ -602,26 +584,10 @@ The lemmas below should be made consistent with those for `findIdx?` (and proved
   rcases xs with ⟨xs⟩
   simp [List.idxOf?_eq_none_iff]
 
-/-! ### finIdxOf?
-
-The verification API for `finIdxOf?` is still incomplete.
-The lemmas below should be made consistent with those for `findFinIdx?` (and proved using them).
--/
+/-! ### finIdxOf? -/
 
 theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
 
-@[simp] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := rfl
-
-@[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
-    xs.finIdxOf? a = none ↔ a ∉ xs := by
-  rcases xs with ⟨xs⟩
-  simp [List.finIdxOf?_eq_none_iff]
-
-@[simp] theorem finIdxOf?_eq_some_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} {i : Fin xs.size} :
-    xs.finIdxOf? a = some i ↔ xs[i] = a ∧ ∀ j (_ : j < i), ¬xs[j] = a := by
-  rcases xs with ⟨xs⟩
-  simp [List.finIdxOf?_eq_some_iff]
-
 end Array

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

@@ -8,7 +8,6 @@ import Init.Data.Nat.Lemmas
 import Init.Data.List.Range
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
-import Init.Data.List.Nat.Basic
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
@@ -22,8 +21,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
 
@@ -61,27 +60,21 @@ theorem size_empty : (#[] : Array α).size = 0 := rfl
 
 /-! ### size -/
 
-theorem eq_empty_of_size_eq_zero (h : xs.size = 0) : xs = #[] := by
-  cases xs
+theorem eq_empty_of_size_eq_zero (h : l.size = 0) : l = #[] := by
+  cases l
   simp_all
 
-theorem ne_empty_of_size_eq_add_one (h : xs.size = n + 1) : xs ≠ #[] := by
-  cases xs
+theorem ne_empty_of_size_eq_add_one (h : l.size = n + 1) : l ≠ #[] := by
+  cases l
   simpa using List.ne_nil_of_length_eq_add_one h
 
-theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
-  cases xs
+theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[] := by
+  cases l
   simpa using List.ne_nil_of_length_pos h
 
-theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
+theorem size_eq_zero : l.size = 0 ↔ l = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
-@[deprecated size_eq_zero_iff (since := "2025-02-24")]
-abbrev size_eq_zero := @size_eq_zero_iff
-
-theorem eq_empty_iff_size_eq_zero : xs = #[] ↔ xs.size = 0 :=
-  size_eq_zero_iff.symm
-
 theorem size_pos_of_mem {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size := by
   cases xs
   simp only [mem_toArray] at h
@@ -98,18 +91,12 @@ theorem exists_mem_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
   cases xs
   simpa using List.exists_mem_of_length_eq_add_one h
 
-theorem size_pos_iff {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
-  Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero_iff)
+theorem size_pos {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
+  Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero)
 
-@[deprecated size_pos_iff (since := "2025-02-24")]
-abbrev size_pos := @size_pos_iff
-
-theorem size_eq_one_iff {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
+theorem size_eq_one {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
   cases xs
-  simpa using List.length_eq_one_iff
-
-@[deprecated size_eq_one_iff (since := "2025-02-24")]
-abbrev size_eq_one := @size_eq_one_iff
+  simpa using List.length_eq_one
 
 /-! ### push -/
 
@@ -166,7 +153,7 @@ theorem ne_empty_iff_exists_push {xs : Array α} :
 
 theorem exists_push_of_size_pos {xs : Array α} (h : 0 < xs.size) :
     ∃ (ys : Array α) (a : α), xs = ys.push a := by
-  replace h : xs ≠ #[] := size_pos_iff.mp h
+  replace h : xs ≠ #[] := size_pos.mp h
   exact exists_push_of_ne_empty h
 
 theorem size_pos_iff_exists_push {xs : Array α} :
@@ -453,7 +440,7 @@ abbrev isEmpty_eq_true := @isEmpty_iff
 abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
 
 theorem isEmpty_iff_size_eq_zero {xs : Array α} : xs.isEmpty ↔ xs.size = 0 := by
-  rw [isEmpty_iff, size_eq_zero_iff]
+  rw [isEmpty_iff, size_eq_zero]
 
 /-! ### Decidability of bounded quantifiers -/
 
@@ -833,9 +820,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 α} (i : Nat) (a : α) (h) :
-     xs.set i a = #[] ↔ xs = #[] := by
-  cases xs <;> cases i <;> simp [set]
+@[simp] theorem set_eq_empty_iff {xs : Array α} (n : Nat) (a : α) (h) :
+     xs.set n a = #[] ↔ xs = #[] := by
+  cases xs <;> cases n <;> 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) :
@@ -1036,20 +1023,6 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a ==
   cases ys
   simp
 
-/-! ### back -/
-
-theorem back_eq_getElem (xs : Array α) (h : 0 < xs.size) : xs.back = xs[xs.size - 1] := by
-  cases xs
-  simp [List.getLast_eq_getElem]
-
-theorem back?_eq_getElem? (xs : Array α) : xs.back? = xs[xs.size - 1]? := by
-  cases xs
-  simp [List.getLast?_eq_getElem?]
-
-@[simp] theorem back_mem {xs : Array α} (h : 0 < xs.size) : xs.back h ∈ xs := by
-  cases xs
-  simp
-
 /-! ### map -/
 
 theorem mapM_eq_foldlM [Monad m] [LawfulMonad m] (f : α → m β) (xs : Array α) :
@@ -1424,18 +1397,6 @@ theorem filter_eq_push_iff {p : α → Bool} {xs ys : Array α} {a : α} :
 theorem mem_of_mem_filter {a : α} {xs : Array α} (h : a ∈ filter p xs) : a ∈ xs :=
   (mem_filter.mp h).1
 
-@[simp]
-theorem size_filter_pos_iff {xs : Array α} {p : α → Bool} :
-    0 < (filter p xs).size ↔ ∃ x ∈ xs, p x := by
-  rcases xs with ⟨xs⟩
-  simp
-
-@[simp]
-theorem size_filter_lt_size_iff_exists {xs : Array α} {p : α → Bool} :
-    (filter p xs).size < xs.size ↔ ∃ x ∈ xs, ¬p x := by
-  rcases xs with ⟨xs⟩
-  simp
-
 /-! ### filterMap -/
 
 @[congr]
@@ -1602,18 +1563,6 @@ theorem filterMap_eq_push_iff {f : α → Option β} {xs : Array α} {ys : Array
   · rintro ⟨⟨l₁⟩, a, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
     refine ⟨l₂.reverse, a, l₁.reverse, by simp_all⟩
 
-@[simp]
-theorem size_filterMap_pos_iff {xs : Array α} {f : α → Option β} :
-    0 < (filterMap f xs).size ↔ ∃ (x : α) (_ : x ∈ xs) (b : β), f x = some b := by
-  rcases xs with ⟨xs⟩
-  simp
-
-@[simp]
-theorem size_filterMap_lt_size_iff_exists {xs : Array α} {f : α → Option β} :
-    (filterMap f xs).size < xs.size ↔ ∃ (x : α) (_ : x ∈ xs), f x = none := by
-  rcases xs with ⟨xs⟩
-  simp
-
 /-! ### singleton -/
 
 @[simp] theorem singleton_def (v : α) : Array.singleton v = #[v] := rfl
@@ -2021,7 +1970,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 xs => !xs.isEmpty) = xss.flatten := by
+    flatten (xss.filter fun l => !l.isEmpty) = xss.flatten := by
   induction xss using array₂_induction
   simp [List.filter_map, Function.comp_def, List.flatten_filter_not_isEmpty]
 
@@ -3236,266 +3185,6 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} (r : β
   rcases xs with ⟨xs⟩
   simp
 
-/-! #### Further results about `back` and `back?` -/
-
-@[simp] theorem back?_eq_none_iff {xs : Array α} : xs.back? = none ↔ xs = #[] := by
-  simp only [back?_eq_getElem?, ← size_eq_zero_iff]
-  simp only [_root_.getElem?_eq_none_iff]
-  omega
-
-theorem back?_eq_some_iff {xs : Array α} {a : α} :
-    xs.back? = some a ↔ ∃ ys : Array α, xs = ys.push a := by
-  rcases xs with ⟨xs⟩
-  simp only [List.back?_toArray, List.getLast?_eq_some_iff, toArray_eq, push_toList]
-  constructor
-  · rintro ⟨ys, rfl⟩
-    exact ⟨ys.toArray, by simp⟩
-  · rintro ⟨ys, rfl⟩
-    exact ⟨ys.toList, by simp⟩
-
-@[simp] theorem back?_isSome : xs.back?.isSome ↔ xs ≠ #[] := by
-  cases xs
-  simp
-
-theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
-  obtain ⟨ys, rfl⟩ := back?_eq_some_iff.1 h
-  simp
-
-@[simp] theorem back_append_of_size_pos {xs ys : Array α} {h₁} (h₂ : 0 < ys.size) :
-    (xs ++ ys).back h₁ = ys.back h₂ := by
-  rcases xs with ⟨l⟩
-  rcases ys with ⟨l'⟩
-  simp only [List.append_toArray, List.back_toArray]
-  rw [List.getLast_append_of_ne_nil]
-
-theorem back_append {xs : Array α} (h : 0 < (xs ++ ys).size) :
-    (xs ++ ys).back h =
-      if h' : ys.isEmpty then
-        xs.back (by simp_all)
-      else
-        ys.back (by simp only [isEmpty_iff, eq_empty_iff_size_eq_zero] at h'; omega) := by
-  rcases xs with ⟨xs⟩
-  rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.back_toArray, List.getLast_append, List.isEmpty_iff,
-    List.isEmpty_toArray]
-  split
-  · rw [dif_pos]
-    simpa only [List.isEmpty_toArray]
-  · rw [dif_neg]
-    simpa only [List.isEmpty_toArray]
-
-theorem back_append_right {xs ys : Array α} (h : 0 < ys.size) :
-    (xs ++ ys).back (by simp; omega) = ys.back h := by
-  rcases xs with ⟨xs⟩
-  rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.back_toArray]
-  rw [List.getLast_append_right]
-
-theorem back_append_left {xs ys : Array α} (w : 0 < (xs ++ ys).size) (h : ys.size = 0) :
-    (xs ++ ys).back w = xs.back (by simp_all) := by
-  rcases xs with ⟨xs⟩
-  rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.back_toArray]
-  rw [List.getLast_append_left]
-  simpa using h
-
-@[simp] theorem back?_append {xs ys : Array α} : (xs ++ ys).back? = ys.back?.or xs.back? := by
-  rcases xs with ⟨xs⟩
-  rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.back?_toArray]
-  rw [List.getLast?_append]
-
-theorem back_filter_of_pos {p : α → Bool} {xs : Array α} (w : 0 < xs.size) (h : p (back xs w) = true) :
-    (filter p xs).back (by simpa using ⟨_, by simp, h⟩) = xs.back w := by
-  rcases xs with ⟨xs⟩
-  simp only [List.back_toArray] at h
-  simp only [List.size_toArray, List.filter_toArray', List.back_toArray]
-  rw [List.getLast_filter_of_pos _ h]
-
-theorem back_filterMap_of_eq_some {f : α → Option β} {xs : Array α} {w : 0 < xs.size} {b : β} (h : f (xs.back w) = some b) :
-    (filterMap f xs).back (by simpa using ⟨_, by simp, b, h⟩) = some b := by
-  rcases xs with ⟨xs⟩
-  simp only [List.back_toArray] at h
-  simp only [List.size_toArray, List.filterMap_toArray', List.back_toArray]
-  rw [List.getLast_filterMap_of_eq_some h]
-
-theorem back?_flatMap {xs : Array α} {f : α → Array β} :
-    (xs.flatMap f).back? = xs.reverse.findSome? fun a => (f a).back? := by
-  rcases xs with ⟨xs⟩
-  simp [List.getLast?_flatMap]
-
-theorem back?_flatten {xss : Array (Array α)} :
-    (flatten xss).back? = xss.reverse.findSome? fun xs => xs.back? := by
-  simp [← flatMap_id, back?_flatMap]
-
-theorem back?_mkArray (a : α) (n : Nat) :
-    (mkArray n a).back? = if n = 0 then none else some a := by
-  rw [mkArray_eq_toArray_replicate]
-  simp only [List.back?_toArray, List.getLast?_replicate]
-
-@[simp] theorem back_mkArray (w : 0 < n) : (mkArray n a).back (by simpa using w) = a := by
-  simp [back_eq_getElem]
-
-/-! ## Additional operations -/
-
-/-! ### leftpad -/
-
--- We unfold `leftpad` and `rightpad` for verification purposes.
-attribute [simp] leftpad rightpad
-
-theorem size_leftpad (n : Nat) (a : α) (xs : Array α) :
-    (leftpad n a xs).size = max n xs.size := by simp; omega
-
-theorem size_rightpad (n : Nat) (a : α) (xs : Array α) :
-    (rightpad n a xs).size = max n xs.size := by simp; omega
-
-/-! ### contains -/
-
-theorem elem_cons_self [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.push a).elem a = true := by simp
-
-theorem contains_eq_any_beq [BEq α] (xs : Array α) (a : α) : xs.contains a = xs.any (a == ·) := by
-  rcases xs with ⟨xs⟩
-  simp [List.contains_eq_any_beq]
-
-theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
-    xs.contains a ↔ ∃ a' ∈ xs, a == a' := by
-  rcases xs with ⟨xs⟩
-  simp [List.contains_iff_exists_mem_beq]
-
-theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
-    xs.contains a ↔ a ∈ xs := by
-  simp
-
-/-! ### more lemmas about `pop` -/
-
-@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
-
-@[simp] theorem pop_push (xs : Array α) : (xs.push x).pop = xs := by simp [pop]
-
-@[simp] theorem getElem_pop {xs : Array α} {i : Nat} (h : i < xs.pop.size) :
-    xs.pop[i] = xs[i]'(by simp at h; omega) := by
-  rcases xs with ⟨xs⟩
-  simp [List.getElem_dropLast]
-
-theorem getElem?_pop (xs : Array α) (i : Nat) :
-    xs.pop[i]? = if i < xs.size - 1 then xs[i]? else none := by
-  rcases xs with ⟨xs⟩
-  simp [List.getElem?_dropLast]
-
-theorem back_pop {xs : Array α} (h) :
-   xs.pop.back h =
-     xs[xs.size - 2]'(by simp at h; omega) := by
-  rcases xs with ⟨xs⟩
-  simp [List.getLast_dropLast]
-
-theorem back?_pop {xs : Array α} :
-    xs.pop.back? = if xs.size ≤ 1 then none else xs[xs.size - 2]? := by
-  rcases xs with ⟨xs⟩
-  simp [List.getLast?_dropLast]
-
-@[simp] theorem pop_append_of_ne_empty {xs : Array α} {ys : Array α} (h : ys ≠ #[]) :
-    (xs ++ ys).pop = xs ++ ys.pop := by
-  rcases xs with ⟨xs⟩
-  rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.pop_toArray, mk.injEq]
-  rw [List.dropLast_append_of_ne_nil _ (by simpa using h)]
-
-theorem pop_append {xs ys : Array α} :
-    (xs ++ ys).pop = if ys.isEmpty then xs.pop else xs ++ ys.pop := by
-  split <;> simp_all
-
-@[simp] theorem pop_mkArray (n) (a : α) : (mkArray n a).pop = mkArray (n - 1) a := by
-  ext <;> simp
-
-theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {xs : Array α} (h : xs.size ≠ 0) :
-    xs = xs.pop.push xs.back! := by
-  apply ext
-  · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
-  · intros i h h'
-    if hlt : i < xs.pop.size then
-      rw [getElem_push_lt (h:=hlt), getElem_pop]
-    else
-      have heq : i = xs.pop.size :=
-        Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq
-      rw [getElem_push_eq, back!]
-      simp [← getElem!_pos]
-
-/-! ### replace -/
-
-section replace
-variable [BEq α]
-
-@[simp] theorem size_replace {xs : Array α} : (xs.replace a b).size = xs.size := by
-  simp only [replace]
-  split <;> simp
-
--- This hypothesis could probably be dropped from some of the lemmas below,
--- by proving them direct from the definition rather than going via `List`.
-variable [LawfulBEq α]
-
-@[simp] theorem replace_of_not_mem {xs : Array α} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
-  cases xs
-  simp_all
-
-theorem getElem?_replace {xs : Array α} {i : Nat} :
-    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
-  rcases xs with ⟨xs⟩
-  simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, beq_iff_eq,
-    take_eq_extract, List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero,
-    mem_toArray]
-  split <;> rename_i h
-  · rw (occs := [2]) [if_pos]
-    simpa using h
-  · rw [if_neg]
-    simpa using h
-
-theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
-    (xs.replace a b)[i]? = xs[i]? := by
-  simp_all [getElem?_replace]
-
-theorem getElem_replace {xs : Array α} {i : Nat} (h : i < xs.size) :
-    (xs.replace a b)[i]'(by simpa) = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
-  apply Option.some.inj
-  rw [← getElem?_eq_getElem, getElem?_replace]
-  split <;> split <;> simp_all
-
-theorem getElem_replace_of_ne {xs : Array α} {i : Nat} {h : i < xs.size} (h' : xs[i] ≠ a) :
-    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
-  rw [getElem_replace h]
-  simp [h']
-
-theorem replace_append {xs ys : Array α} :
-    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
-  rcases xs with ⟨xs⟩
-  rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.replace_toArray, List.replace_append, mem_toArray]
-  split <;> simp
-
-theorem replace_append_left {xs ys : Array α} (h : a ∈ xs) :
-    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
-  simp [replace_append, h]
-
-theorem replace_append_right {xs ys : Array α} (h : ¬ a ∈ xs) :
-    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
-  simp [replace_append, h]
-
-theorem replace_extract {xs : Array α} {i : Nat} :
-    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
-  rcases xs with ⟨xs⟩
-  simp [List.replace_take]
-
-@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
-    (mkArray n a).replace a b = #[b] ++ mkArray (n - 1) a := by
-  cases n <;> simp_all [mkArray_succ', replace_append]
-
-@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
-    (mkArray n a).replace b c = mkArray n a := by
-  rw [replace_of_not_mem]
-  simp_all
-
-end replace
-
 /-! Content below this point has not yet been aligned with `List`. -/
 
 /-! ### sum -/
@@ -3674,6 +3363,10 @@ theorem back!_eq_back? [Inhabited α] (xs : Array α) : xs.back! = xs.back?.getD
 @[simp] theorem back!_push [Inhabited α] (xs : Array α) : (xs.push x).back! = x := by
   simp [back!_eq_back?]
 
+theorem mem_of_back? {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs := by
+  cases xs
+  simpa using List.mem_of_getLast? (by simpa using h)
+
 @[deprecated mem_of_back? (since := "2024-10-21")] abbrev mem_of_back?_eq_some := @mem_of_back?
 
 theorem getElem?_push_lt (xs : Array α) (x : α) (i : Nat) (h : i < xs.size) :
@@ -3735,6 +3428,28 @@ theorem swapAt!_def (xs : Array α) (i : Nat) (v : α) (h : i < xs.size) :
   · simp
   · rfl
 
+@[simp] theorem pop_empty : (#[] : Array α).pop = #[] := rfl
+
+@[simp] theorem pop_push (xs : Array α) : (xs.push x).pop = xs := by simp [pop]
+
+@[simp] theorem getElem_pop (xs : Array α) (i : Nat) (hi : i < xs.pop.size) :
+    xs.pop[i] = xs[i]'(Nat.lt_of_lt_of_le (xs.size_pop ▸ hi) (Nat.sub_le _ _)) :=
+  List.getElem_dropLast ..
+
+theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {xs : Array α} (h : xs.size ≠ 0) :
+    xs = xs.pop.push xs.back! := by
+  apply ext
+  · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
+  · intros i h h'
+    if hlt : i < xs.pop.size then
+      rw [getElem_push_lt (h:=hlt), getElem_pop]
+    else
+      have heq : i = xs.pop.size :=
+        Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
+      cases heq
+      rw [getElem_push_eq, back!]
+      simp [← getElem!_pos]
+
 theorem eq_push_of_size_ne_zero {xs : Array α} (h : xs.size ≠ 0) :
     ∃ (bs : Array α) (c : α), xs = bs.push c :=
   let _ : Inhabited α := ⟨xs[0]⟩

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
 
@@ -31,7 +31,7 @@ theorem range'_succ (s n step) : range' s (n + 1) step = #[s] ++ range' (s + ste
   simp [List.range'_succ]
 
 @[simp] theorem range'_eq_empty_iff : range' s n step = #[] ↔ n = 0 := by
-  rw [← size_eq_zero_iff, size_range']
+  rw [← size_eq_zero, size_range']
 
 theorem range'_ne_empty_iff (s : Nat) {n step : Nat} : range' s n step ≠ #[] ↔ n ≠ 0 := by
   cases n <;> simp
@@ -136,7 +136,7 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) :=
   rw [range_eq_range', map_add_range']; rfl
 
 @[simp] theorem range_eq_empty_iff {n : Nat} : range n = #[] ↔ n = 0 := by
-  rw [← size_eq_zero_iff, size_range]
+  rw [← size_eq_zero, size_range]
 
 theorem range_ne_empty_iff {n : Nat} : range n ≠ #[] ↔ n ≠ 0 := by
   cases n <;> simp
@@ -149,9 +149,9 @@ theorem range_succ (n : Nat) : range (succ n) = range n ++ #[n] := by
       dite_eq_ite]
     split <;> omega
 
-theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by
+theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
   rw [← range'_eq_map_range]
-  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm
+  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).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 (i n : Nat) : take (range n) i = range (min i n) := by
+@[simp] theorem take_range (m n : Nat) : take (range n) m = range (min m 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 i = zipWith f (as.take i) (bs.take i) := by
+theorem take_zipWith : (zipWith f as bs).take n = zipWith f (as.take n) (bs.take n) := by
   cases as
   cases bs
   simp [List.take_zipWith]

src/Init/Data/BitVec/Lemmas.lean

@@ -1517,8 +1517,8 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
   all_goals { simp_all <;> omega }
 
 @[simp] theorem getElem_shiftLeft {x : BitVec m} {n : Nat} (h : i < m) :
-    (x <<< n)[i] = (!decide (i < n) && x[i - n]) := by
-  rw [getElem_eq_testBit_toNat, getElem_eq_testBit_toNat]
+    (x <<< n)[i] = (!decide (i < n) && getLsbD x (i - n)) := by
+  rw [← testBit_toNat, getElem_eq_testBit_toNat]
   simp only [toNat_shiftLeft, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft, ge_iff_le]
   -- This step could be a case bashing tactic.
   cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
@@ -1568,8 +1568,8 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
   · omega
 
 @[simp] theorem getElem_shiftLeftZeroExtend {x : BitVec m} {n : Nat} (h : i < m + n) :
-    (shiftLeftZeroExtend x n)[i] = if h' : i < n then false else x[i - n] := by
-  rw [shiftLeftZeroExtend_eq]
+    (shiftLeftZeroExtend x n)[i] = ((! decide (i < n)) && getLsbD x (i - n)) := by
+  rw [shiftLeftZeroExtend_eq, getLsbD]
   simp only [getElem_eq_testBit_toNat, getLsbD_shiftLeft, getLsbD_setWidth]
   cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n)
     <;> simp_all [h]
@@ -1598,8 +1598,8 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
 theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
     x <<< (n + m) = (x <<< n) <<< m := by
   ext i
-  simp only [getElem_shiftLeft]
-  rw [show x[i - (n + m)] = x[i - m - n] by congr 1; omega]
+  simp only [getElem_shiftLeft, Fin.is_lt, decide_true, Bool.true_and]
+  rw [show i - (n + m) = (i - m - n) by omega]
   cases h₂ : decide (i < m) <;>
   cases h₃ : decide (i - m < w) <;>
   cases h₄ : decide (i - m < n) <;>
@@ -1632,7 +1632,7 @@ theorem getLsbD_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} :
   simp [shiftLeft_eq', getLsbD_shiftLeft]
 
 theorem getElem_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) :
-    (x <<< y)[i] = (!decide (i < y.toNat) && x[i - y.toNat]) := by
+    (x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat)) := by
   simp
 
 @[simp] theorem shiftLeft_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) : x <<< n = 0#w := by
@@ -1844,10 +1844,13 @@ theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
       omega
 
 theorem getElem_sshiftRight {x : BitVec w} {s i : Nat} (h : i < w) :
-    (x.sshiftRight s)[i] = (if h : s + i < w then x[s + i] else x.msb) := by
-  rw [← getLsbD_eq_getElem, getLsbD_sshiftRight]
-  simp only [show ¬(w ≤ i) by omega, decide_false, Bool.not_false, Bool.true_and]
-  by_cases h' : s + i < w <;> simp [h']
+    (x.sshiftRight s)[i] = (if s + i < w then x.getLsbD (s + i) else x.msb) := by
+  rcases hmsb : x.msb with rfl | rfl
+  · simp only [sshiftRight_eq_of_msb_false hmsb, getElem_ushiftRight, Bool.if_false_right,
+    Bool.iff_and_self, decide_eq_true_eq]
+    intros hlsb
+    apply BitVec.lt_of_getLsbD hlsb
+  · simp [sshiftRight_eq_of_msb_true hmsb]
 
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
@@ -1954,8 +1957,9 @@ theorem getLsbD_sshiftRight' {x y : BitVec w} {i : Nat} :
 
 -- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form.
 theorem getElem_sshiftRight' {x y : BitVec w} {i : Nat} (h : i < w) :
-    (x.sshiftRight' y)[i] = (if h : y.toNat + i < w then x[y.toNat + i] else x.msb) := by
-  simp [show ¬ w ≤ i by omega, getElem_sshiftRight]
+    (x.sshiftRight' y)[i] =
+      (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
+  simp only [← getLsbD_eq_getElem, BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
 
 theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
     (x.sshiftRight y.toNat).getMsbD i =
@@ -2026,8 +2030,9 @@ theorem getMsbD_signExtend {x : BitVec w} {v i : Nat} :
     by_cases h : i < v <;> by_cases h' : v - w ≤ i <;> simp [h, h'] <;> omega
 
 theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
-    (x.signExtend v)[i] = if h : i < w then x[i] else x.msb := by
-  simp [←getLsbD_eq_getElem, getLsbD_signExtend, h]
+    (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by
+  rw [←getLsbD_eq_getElem, getLsbD_signExtend]
+  simp [h]
 
 theorem msb_signExtend {x : BitVec w} :
     (x.signExtend v).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb) := by
@@ -2039,7 +2044,9 @@ theorem msb_signExtend {x : BitVec w} :
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
   ext i h
-  simp [getElem_signExtend, show i < w by omega]
+  simp only [getElem_signExtend, h, decide_true, Bool.true_and, getElem_setWidth,
+    ite_eq_left_iff, Nat.not_lt]
+  omega
 
 /-- Sign extending to the same bitwidth is a no op. -/
 theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
@@ -2094,7 +2101,6 @@ theorem toInt_signExtend_of_lt {x : BitVec w} (hv : w < v):
   have : (x.signExtend v).msb = x.msb := by
     rw [msb_eq_getLsbD_last, getLsbD_eq_getElem (Nat.sub_one_lt_of_lt hv)]
     simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]
-    omega
   have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega)
   simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]
   by_cases h : x.msb
@@ -2276,11 +2282,11 @@ theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
 theorem shiftLeft_eq_concat_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
     x <<< n = (x.extractLsb' 0 (w - n) ++ 0#n).cast (by omega) := by
   ext i hi
-  simp only [getElem_shiftLeft, getElem_cast, getElem_append, getElem_zero, getElem_extractLsb',
+  simp only [getElem_shiftLeft, getElem_cast, getElem_append, getLsbD_zero, getLsbD_extractLsb',
     Nat.zero_add, Bool.if_false_left]
   by_cases hi' : i < n
   · simp [hi']
-  · simp [hi', show i - n < w by omega]
+  · simp [hi']
 
 /-! ### rev -/
 
@@ -2330,7 +2336,7 @@ theorem getLsbD_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
     simp [p1, p2, Nat.testBit_bool_to_nat]
 
 theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
-    (cons b x)[i] = if h : i = n then b else x[i] := by
+    (cons b x)[i] = if i = n then b else getLsbD x i := by
   simp only [getElem_eq_testBit_toNat, toNat_cons, Nat.testBit_or, getLsbD]
   rw [Nat.testBit_shiftLeft]
   rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
@@ -2438,7 +2444,7 @@ theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
   · simp [Nat.div_eq_of_lt b.toNat_lt, Nat.testBit_add_one]
 
 theorem getElem_concat (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
-    (concat x b)[i] = if h : i = 0 then b else x[i - 1] := by
+    (concat x b)[i] = if i = 0 then b else x.getLsbD (i - 1) := by
   simp only [concat, getElem_eq_testBit_toNat, getLsbD, toNat_append,
     toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
   cases i
@@ -2478,7 +2484,10 @@ theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
   simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_true, Nat.add_one_sub_one,
     Nat.sub_zero, Bool.true_and]
   by_cases h₀ : 0 < w
-  · simp [getElem_concat, h₀, show ¬ w = 0 by omega, show w - 1 < w by omega]
+  · simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_true,
+      Bool.true_and, ite_eq_right_iff]
+    intro
+    omega
   · simp [h₀, show w = 0 by omega]
 
 @[simp] theorem toInt_concat (x : BitVec w) (b : Bool) :
@@ -4208,10 +4217,6 @@ theorem toInt_abs_eq_natAbs_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) :
     x.abs.toInt = x.toInt.natAbs := by
   simp [toInt_abs_eq_natAbs, hx]
 
-theorem toFin_abs {x : BitVec w} :
-    x.abs.toFin = if x.msb then Fin.ofNat' (2 ^ w) (2 ^ w - x.toNat) else x.toFin := by
-  by_cases h : x.msb <;> simp [BitVec.abs, h]
-
 /-! ### Reverse -/
 
 theorem getLsbD_reverse {i : Nat} {x : BitVec w} :

src/Init/Data/Int/Linear.lean

@@ -850,31 +850,6 @@ theorem le_unsat (ctx : Context) (p : Poly) : p.isUnsatLe → p.denote' ctx ≤
   have := Int.lt_of_le_of_lt h₂ h₁
   simp at this
 
-theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm == p₂) : p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
-  simp at h
-  replace h := congrArg (Poly.denote ctx) h
-  simp at h
-  simp [*]
-
-def eq_coeff_cert (p p' : Poly) (k : Int) : Bool :=
-  p == p'.mul k && k > 0
-
-theorem eq_coeff (ctx : Context) (p p' : Poly) (k : Int) : eq_coeff_cert p p' k → p.denote' ctx = 0 → p'.denote' ctx = 0 := by
-  simp [eq_coeff_cert]
-  intro _ _; simp [mul_eq_zero_iff, *]
-
-theorem eq_unsat (ctx : Context) (p : Poly) : p.isUnsatEq → p.denote' ctx = 0 → False := by
-  simp [Poly.isUnsatEq] <;> split <;> simp
-
-def eq_unsat_coeff_cert (p : Poly) (k : Int) : Bool :=
-  p.divCoeffs k && k > 0 && cmod p.getConst k < 0
-
-theorem eq_unsat_coeff (ctx : Context) (p : Poly) (k : Int) : eq_unsat_coeff_cert p k → p.denote' ctx = 0 → False := by
-  simp [eq_unsat_coeff_cert]
-  intro h₁ h₂ h₃
-  have h := poly_eq_zero_eq_false ctx h₁ h₂ h₃; clear h₁ h₂ h₃
-  simp [h]
-
 def Poly.coeff (p : Poly) (x : Var) : Int :=
   match p with
   | .add a y p => bif x == y then a else coeff p x
@@ -889,30 +864,19 @@ private theorem dvd_of_eq' {a x p : Int} : a*x + p = 0 → a ∣ p := by
   rw [Int.mul_comm, ← Int.neg_mul, Eq.comm, Int.mul_comm] at h
   exact ⟨-x, h⟩
 
-private def abs (x : Int) : Int :=
-  Int.ofNat x.natAbs
-
-private theorem abs_dvd {a p : Int} (h : a ∣ p) : abs a ∣ p := by
-  cases a <;> simp [abs]
-  · simp at h; assumption
-  · simp [Int.negSucc_eq] at h; assumption
-
 def dvd_of_eq_cert (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) : Bool :=
-  let a := p₁.coeff x
-  d₂ == abs a && p₂ == p₁.insert (-a) x
+  d₂ == p₁.coeff x && p₂ == p₁.insert (-d₂) x
 
 theorem dvd_of_eq (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly)
     : dvd_of_eq_cert x p₁ d₂ p₂ → p₁.denote' ctx = 0 → d₂ ∣ p₂.denote' ctx := by
   simp [dvd_of_eq_cert]
   intro h₁ h₂
   have h := eq_add_coeff_insert ctx p₁ x
-  rw [← h₂] at h
-  rw [h, h₁]
-  intro h₃
-  apply abs_dvd
-  apply dvd_of_eq' h₃
+  rw [← h₁, ← h₂] at h
+  rw [h]
+  apply dvd_of_eq'
 
-private theorem eq_dvd_subst' {a x p d b q : Int} : a*x + p = 0 → d ∣ b*x + q → a*d ∣ a*q - b*p := by
+private theorem eq_dvd_elim' {a x p d b q : Int} : a*x + p = 0 → d ∣ b*x + q → a*d ∣ a*q - b*p := by
   intro h₁ ⟨z, h₂⟩
   have h : a*q - b*p = a*(b*x + q) - b*(a*x+p) := by
     conv => rhs; rw [Int.sub_eq_add_neg]; rhs; rw [Int.mul_add, Int.neg_add]
@@ -923,17 +887,17 @@ private theorem eq_dvd_subst' {a x p d b q : Int} : a*x + p = 0 → d ∣ b*x +
   rw [← Int.mul_assoc] at h
   exact ⟨z, h⟩
 
-def eq_dvd_subst_cert (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d₃ : Int) (p₃ : Poly) : Bool :=
+def eq_dvd_elim_cert (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d₃ : Int) (p₃ : Poly) : Bool :=
   let a := p₁.coeff x
   let b := p₂.coeff x
   let p := p₁.insert (-a) x
   let q := p₂.insert (-b) x
-  d₃ == abs (a * d₂) &&
+  d₃ == a * d₂ &&
   p₃ == (q.mul a |>.combine (p.mul (-b)))
 
-theorem eq_dvd_subst (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d₃ : Int) (p₃ : Poly)
-    : eq_dvd_subst_cert x p₁ d₂ p₂ d₃ p₃ → p₁.denote' ctx = 0 → d₂ ∣ p₂.denote' ctx → d₃ ∣ p₃.denote' ctx := by
-  simp [eq_dvd_subst_cert]
+theorem eq_dvd_elim (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d₃ : Int) (p₃ : Poly)
+    : eq_dvd_elim_cert x p₁ d₂ p₂ d₃ p₃ → p₁.denote' ctx = 0 → d₂ ∣ p₂.denote' ctx → d₃ ∣ p₃.denote' ctx := by
+  simp [eq_dvd_elim_cert]
   have eq₁ := eq_add_coeff_insert ctx p₁ x
   have eq₂ := eq_add_coeff_insert ctx p₂ x
   revert eq₁ eq₂
@@ -947,64 +911,126 @@ theorem eq_dvd_subst (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂
   intro; subst p₃
   intro h₁ h₂
   rw [Int.add_comm] at h₁ h₂
-  have := eq_dvd_subst' h₁ h₂
+  have := eq_dvd_elim' h₁ h₂
   rw [Int.sub_eq_add_neg, Int.add_comm] at this
-  apply abs_dvd
   simp [this]
 
-def eq_eq_subst_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
+private theorem eq_eq_elim' {a x p b q : Int} : a*x + p = 0 → b*x + q = 0 → b*p - a*q = 0 := by
+  intro h₁ h₂
+  replace h₁ := congrArg (b*·) h₁; simp at h₁
+  replace h₂ := congrArg ((-a)*.) h₂; simp at h₂
+  rw [Int.add_comm] at h₁
+  replace h₁ := Int.neg_eq_of_add_eq_zero h₁
+  rw [← h₁]; clear h₁
+  replace h₂ := Int.neg_eq_of_add_eq_zero h₂; simp at h₂
+  rw [h₂]; clear h₂
+  rw [Int.mul_left_comm]
+  simp
+
+def eq_eq_elim_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
   let a := p₁.coeff x
   let b := p₂.coeff x
-  p₃ == (p₁.mul b |>.combine (p₂.mul (-a)))
+  let p := p₁.insert (-a) x
+  let q := p₂.insert (-b) x
+  p₃ == (p.mul b |>.combine (q.mul (-a)))
 
-theorem eq_eq_subst (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
-    : eq_eq_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 → p₃.denote' ctx = 0 := by
-  simp [eq_eq_subst_cert]
+theorem eq_eq_elim (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
+    : eq_eq_elim_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 → p₃.denote' ctx = 0 := by
+  simp [eq_eq_elim_cert]
+  have eq₁ := eq_add_coeff_insert ctx p₁ x
+  have eq₂ := eq_add_coeff_insert ctx p₂ x
+  revert eq₁ eq₂
+  generalize p₁.coeff x = a
+  generalize p₂.coeff x = b
+  generalize p₁.insert (-a) x = p
+  generalize p₂.insert (-b) x = q
+  intro eq₁; simp [eq₁]; clear eq₁
+  intro eq₂; simp [eq₂]; clear eq₂
   intro; subst p₃
   intro h₁ h₂
-  simp [*]
+  rw [Int.add_comm] at h₁ h₂
+  have := eq_eq_elim' h₁ h₂
+  rw [Int.sub_eq_add_neg] at this
+  simp [this]
 
-def eq_le_subst_nonneg_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
-  let a := p₁.coeff x
-  let b := p₂.coeff x
-  a ≥ 0 && p₃ == (p₂.mul a |>.combine (p₁.mul (-b)))
-
-theorem eq_le_subst_nonneg (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
-    : eq_le_subst_nonneg_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
-  simp [eq_le_subst_nonneg_cert]
-  intro h
-  intro; subst p₃
-  intro h₁ h₂
+private theorem eq_le_elim_nonneg' {a x p b q : Int} : a ≥ 0 → a*x + p = 0 → b*x + q ≤ 0 → a*q - b*p ≤ 0 := by
+  intro h h₁ h₂
+  replace h₁ := congrArg ((-b)*·) h₁; simp at h₁
+  rw [Int.add_comm, Int.mul_left_comm] at h₁
+  replace h₁ := Int.neg_eq_of_add_eq_zero h₁; simp at h₁
   replace h₂ := Int.mul_le_mul_of_nonneg_left h₂ h
+  rw [Int.mul_add, h₁] at h₂; clear h₁
   simp at h₂
-  simp [*]
-
-def eq_le_subst_nonpos_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
-  let a := p₁.coeff x
-  let b := p₂.coeff x
-  a ≤ 0 && p₃ == (p₁.mul b |>.combine (p₂.mul (-a)))
-
-theorem eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
-    : eq_le_subst_nonpos_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
-  simp [eq_le_subst_nonpos_cert]
-  intro h
-  intro; subst p₃
-  intro h₁ h₂
-  simp [*]
-  replace h₂ := Int.mul_le_mul_of_nonpos_left h₂ h; simp at h₂; clear h
-  rw [← Int.neg_zero]
-  apply Int.neg_le_neg
-  rw [Int.mul_comm]
+  rw [Int.sub_eq_add_neg]
   assumption
 
-def eq_of_core_cert (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
-  p₃ == p₁.combine (p₂.mul (-1))
+def eq_le_elim_nonneg_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
+  let a := p₁.coeff x
+  let b := p₂.coeff x
+  let p := p₁.insert (-a) x
+  let q := p₂.insert (-b) x
+  a ≥ 0 && p₃ == (q.mul a |>.combine (p.mul (-b)))
 
-theorem eq_of_core (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
-    : eq_of_core_cert p₁ p₂ p₃ → p₁.denote' ctx = p₂.denote' ctx → p₃.denote' ctx = 0 := by
-  simp [eq_of_core_cert]
-  intro; subst p₃; simp
-  intro h; rw [h, ←Int.sub_eq_add_neg, Int.sub_self]
+theorem eq_le_elim_nonneg (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
+    : eq_le_elim_nonneg_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
+  simp [eq_le_elim_nonneg_cert]
+  have eq₁ := eq_add_coeff_insert ctx p₁ x
+  have eq₂ := eq_add_coeff_insert ctx p₂ x
+  revert eq₁ eq₂
+  generalize p₁.coeff x = a
+  generalize p₂.coeff x = b
+  generalize p₁.insert (-a) x = p
+  generalize p₂.insert (-b) x = q
+  intro eq₁; simp [eq₁]; clear eq₁
+  intro eq₂; simp [eq₂]; clear eq₂
+  intro h
+  intro; subst p₃
+  intro h₁ h₂
+  rw [Int.add_comm] at h₁ h₂
+  have := eq_le_elim_nonneg' h h₁ h₂
+  rw [Int.sub_eq_add_neg, Int.add_comm] at this
+  simp [this]
+
+private theorem eq_le_elim_nonpos' {a x p b q : Int} : a ≤ 0 → a*x + p = 0 → b*x + q ≤ 0 → b*p - a*q ≤ 0 := by
+  intro h h₁ h₂
+  replace h₁ := congrArg (b*·) h₁; simp at h₁
+  rw [Int.add_comm, Int.mul_left_comm] at h₁
+  replace h₁ := Int.neg_eq_of_add_eq_zero h₁; simp at h₁
+  replace h : (-a) ≥ 0 := by
+    have := Int.neg_le_neg h
+    simp at this
+    exact this
+  replace h₂ := Int.mul_le_mul_of_nonneg_left h₂ h; simp at h₂; clear h
+  rw [h₁] at h₂
+  rw [Int.add_comm, ←Int.sub_eq_add_neg] at h₂
+  assumption
+
+def eq_le_elim_nonpos_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
+  let a := p₁.coeff x
+  let b := p₂.coeff x
+  let p := p₁.insert (-a) x
+  let q := p₂.insert (-b) x
+  a ≤ 0 && p₃ == (p.mul b |>.combine (q.mul (-a)))
+
+theorem eq_le_elim_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
+    : eq_le_elim_nonpos_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
+  simp [eq_le_elim_nonpos_cert]
+  have eq₁ := eq_add_coeff_insert ctx p₁ x
+  have eq₂ := eq_add_coeff_insert ctx p₂ x
+  revert eq₁ eq₂
+  generalize p₁.coeff x = a
+  generalize p₂.coeff x = b
+  generalize p₁.insert (-a) x = p
+  generalize p₂.insert (-b) x = q
+  intro eq₁; simp [eq₁]; clear eq₁
+  intro eq₂; simp [eq₂]; clear eq₂
+  intro h
+  intro; subst p₃
+  intro h₁ h₂
+  rw [Int.add_comm] at h₁ h₂
+  have := eq_le_elim_nonpos' h h₁ h₂
+  rw [Int.sub_eq_add_neg] at this
+  simp [this]
 
 end Int.Linear
 

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
 
@@ -190,7 +190,7 @@ theorem length_attachWith {p : α → Prop} {l H} : length (l.attachWith p H) =
 
 @[simp]
 theorem pmap_eq_nil_iff {p : α → Prop} {f : ∀ a, p a → β} {l H} : pmap f l H = [] ↔ l = [] := by
-  rw [← length_eq_zero_iff, length_pmap, length_eq_zero_iff]
+  rw [← length_eq_zero, length_pmap, length_eq_zero]
 
 theorem pmap_ne_nil_iff {P : α → Prop} (f : (a : α) → P a → β) {xs : List α}
     (H : ∀ (a : α), a ∈ xs → P a) : xs.pmap f H ≠ [] ↔ xs ≠ [] := by

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
 
@@ -87,7 +87,7 @@ theorem countP_le_length : countP p l ≤ l.length := by
   countP_pos_iff
 
 @[simp] theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
-  simp only [countP_eq_length_filter, length_eq_zero_iff, filter_eq_nil_iff]
+  simp only [countP_eq_length_filter, length_eq_zero, filter_eq_nil_iff]
 
 @[simp] theorem countP_eq_length {p} : countP p l = l.length ↔ ∀ a ∈ l, p a := by
   rw [countP_eq_length_filter, filter_length_eq_length]

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
 
@@ -137,7 +137,7 @@ theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (erase
 @[simp] theorem eraseP_eq_self_iff {p} {l : List α} : l.eraseP p = l ↔ ∀ a ∈ l, ¬ p a := by
   rw [← Sublist.length_eq (eraseP_sublist l), length_eraseP]
   split <;> rename_i h
-  · simp only [any_eq_true, length_eq_zero_iff] at h
+  · simp only [any_eq_true, length_eq_zero] at h
     constructor
     · intro; simp_all [Nat.sub_one_eq_self]
     · intro; obtain ⟨x, m, h⟩ := h; simp_all

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
@@ -514,6 +514,47 @@ private theorem findIdx?_go_eq {p : α → Bool} {xs : List α} {i : Nat} :
     (x :: xs).findIdx? p = if p x then some 0 else (xs.findIdx? p).map fun i => i + 1 := by
   simp [findIdx?, findIdx?_go_eq]
 
+/-! ### findFinIdx? -/
+
+@[simp] theorem findFinIdx?_nil {p : α → Bool} : findFinIdx? p [] = none := rfl
+
+theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
+    List.findIdx?.go p xs i =
+      (List.findFinIdx?.go p l xs i h).map (·.val) := by
+  unfold findIdx?.go
+  unfold findFinIdx?.go
+  split
+  · simp_all
+  · simp only
+    split
+    · simp
+    · rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+
+theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
+  simp [findIdx?, findFinIdx?]
+  rw [findIdx?_go_eq_map_findFinIdx?_go_val]
+
+@[simp] theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
+    findFinIdx? p (x :: xs) = if p x then some 0 else (findFinIdx? p xs).map Fin.succ := by
+  rw [← Option.map_inj_right (f := Fin.val) (fun a b => Fin.eq_of_val_eq)]
+  rw [← findIdx?_eq_map_findFinIdx?_val]
+  rw [findIdx?_cons]
+  split
+  · simp
+  · rw [findIdx?_eq_map_findFinIdx?_val]
+    simp [Function.comp_def]
+
+@[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
+  unfold unattach
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp [hf, findFinIdx?_cons]
+    split <;> simp [ih, Function.comp_def]
+
 /-! ### findIdx -/
 
 theorem findIdx_cons (p : α → Bool) (b : α) (l : List α) :
@@ -935,71 +976,6 @@ theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} :
     simp [hf, findIdx?_cons]
     split <;> simp [ih, Function.comp_def]
 
-/-! ### findFinIdx? -/
-
-@[simp] theorem findFinIdx?_nil {p : α → Bool} : findFinIdx? p [] = none := rfl
-
-theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
-    List.findIdx?.go p xs i =
-      (List.findFinIdx?.go p l xs i h).map (·.val) := by
-  unfold findIdx?.go
-  unfold findFinIdx?.go
-  split
-  · simp_all
-  · simp only
-    split
-    · simp
-    · rw [findIdx?_go_eq_map_findFinIdx?_go_val]
-
-theorem findIdx?_eq_map_findFinIdx?_val {xs : List α} {p : α → Bool} :
-    xs.findIdx? p = (xs.findFinIdx? p).map (·.val) := by
-  simp [findIdx?, findFinIdx?]
-  rw [findIdx?_go_eq_map_findFinIdx?_go_val]
-
-theorem findFinIdx?_eq_pmap_findIdx? {xs : List α} {p : α → Bool} :
-    xs.findFinIdx? p =
-      (xs.findIdx? p).pmap
-        (fun i m => by simp [findIdx?_eq_some_iff_getElem] at m; exact ⟨i, m.choose⟩)
-        (fun i h => h) := by
-  simp [findIdx?_eq_map_findFinIdx?_val, Option.pmap_map]
-
-@[simp] theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
-    findFinIdx? p (x :: xs) = if p x then some 0 else (findFinIdx? p xs).map Fin.succ := by
-  rw [← Option.map_inj_right (f := Fin.val) (fun a b => Fin.eq_of_val_eq)]
-  rw [← findIdx?_eq_map_findFinIdx?_val]
-  rw [findIdx?_cons]
-  split
-  · simp
-  · rw [findIdx?_eq_map_findFinIdx?_val]
-    simp [Function.comp_def]
-
-@[simp] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
-    l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by
-  simp [findFinIdx?_eq_pmap_findIdx?]
-
-@[simp]
-theorem findFinIdx?_eq_some_iff {xs : List α} {p : α → Bool} {i : Fin xs.length} :
-    xs.findFinIdx? p = some i ↔
-      p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji i.2)) := by
-  simp only [findFinIdx?_eq_pmap_findIdx?, Option.pmap_eq_some_iff, findIdx?_eq_some_iff_getElem,
-    Bool.not_eq_true, Option.mem_def, exists_and_left, and_exists_self, Fin.getElem_fin]
-  constructor
-  · rintro ⟨a, ⟨h, w₁, w₂⟩, rfl⟩
-    exact ⟨w₁, fun j hji => by simpa using w₂ j hji⟩
-  · rintro ⟨h, w⟩
-    exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
-
-@[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
-    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
-    l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
-  unfold unattach
-  induction l with
-  | nil => simp
-  | cons a l ih =>
-    simp [hf, findFinIdx?_cons]
-    split <;> simp [ih, Function.comp_def]
-
-
 /-! ### idxOf
 
 The verification API for `idxOf` is still incomplete.
@@ -1059,36 +1035,6 @@ theorem idxOf_lt_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∈ l) : l.
 @[deprecated idxOf_lt_length (since := "2025-01-29")]
 abbrev indexOf_lt_length := @idxOf_lt_length
 
-/-! ### finIdxOf?
-
-The verification API for `finIdxOf?` is still incomplete.
-The lemmas below should be made consistent with those for `findFinIdx?` (and proved using them).
--/
-
-theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
-    xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
-  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
-
-@[simp] theorem finIdxOf?_nil [BEq α] : ([] : List α).finIdxOf? a = none := rfl
-
-@[simp] theorem finIdxOf?_cons [BEq α] (a : α) (xs : List α) :
-    (a :: xs).finIdxOf? b =
-      if a == b then some ⟨0, by simp⟩ else (xs.finIdxOf? b).map (·.succ) := by
-  simp [finIdxOf?]
-
-@[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
-    l.finIdxOf? a = none ↔ a ∉ l := by
-  simp only [finIdxOf?, findFinIdx?_eq_none_iff, beq_iff_eq]
-  constructor
-  · intro w m
-    exact w a m rfl
-  · rintro h a m rfl
-    exact h m
-
-@[simp] theorem finIdxOf?_eq_some_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Fin l.length} :
-    l.finIdxOf? a = some i ↔ l[i] = a ∧ ∀ j (_ : j < i), ¬l[j] = a := by
-  simp only [finIdxOf?, findFinIdx?_eq_some_iff, beq_iff_eq]
-
 /-! ### idxOf?
 
 The verification API for `idxOf?` is still incomplete.
@@ -1114,6 +1060,12 @@ theorem idxOf?_cons [BEq α] (a : α) (xs : List α) (b : α) :
 @[deprecated idxOf?_eq_none_iff (since := "2025-01-29")]
 abbrev indexOf?_eq_none_iff := @idxOf?_eq_none_iff
 
+/-! ### finIdxOf? -/
+
+theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
+    xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
+  simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
+
 /-! ### lookup -/
 
 section lookup

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
 
@@ -96,15 +96,9 @@ theorem ne_nil_of_length_eq_add_one (_ : length l = n + 1) : l ≠ [] := fun _ =
 
 theorem ne_nil_of_length_pos (_ : 0 < length l) : l ≠ [] := fun _ => nomatch l
 
-@[simp] theorem length_eq_zero_iff : length l = 0 ↔ l = [] :=
+@[simp] theorem length_eq_zero : length l = 0 ↔ l = [] :=
   ⟨eq_nil_of_length_eq_zero, fun h => h ▸ rfl⟩
 
-@[deprecated length_eq_zero_iff (since := "2025-02-24")]
-abbrev length_eq_zero := @length_eq_zero_iff
-
-theorem eq_nil_iff_length_eq_zero : l = [] ↔ length l = 0 :=
-  length_eq_zero_iff.symm
-
 theorem length_pos_of_mem {a : α} : ∀ {l : List α}, a ∈ l → 0 < length l
   | _::_, _ => Nat.zero_lt_succ _
 
@@ -129,21 +123,12 @@ theorem exists_cons_of_length_eq_add_one :
     ∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
   | _::_, _ => ⟨_, _, rfl⟩
 
-theorem length_pos_iff {l : List α} : 0 < length l ↔ l ≠ [] :=
-  Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero_iff)
+theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
+  Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)
 
-@[deprecated length_pos_iff (since := "2025-02-24")]
-abbrev length_pos := @length_pos_iff
-
-theorem ne_nil_iff_length_pos {l : List α} : l ≠ [] ↔ 0 < length l :=
-  length_pos_iff.symm
-
-theorem length_eq_one_iff {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
+theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
-@[deprecated length_eq_one_iff (since := "2025-02-24")]
-abbrev length_eq_one := @length_eq_one_iff
-
 /-! ### cons -/
 
 theorem cons_ne_nil (a : α) (l : List α) : a :: l ≠ [] := nofun
@@ -299,7 +284,7 @@ such a rewrite, with `rw [getElem_of_eq h]`.
 theorem getElem_of_eq {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length) :
     l[i] = l'[i]'(h ▸ w) := by cases h; rfl
 
-theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos_iff.mp h) :=
+theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos.mp h) :=
   match l, h with
   | _ :: _, _ => rfl
 
@@ -390,7 +375,7 @@ theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
 theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
 
 theorem exists_mem_of_ne_nil (l : List α) (h : l ≠ []) : ∃ x, x ∈ l :=
-  exists_mem_of_length_pos (length_pos_iff.2 h)
+  exists_mem_of_length_pos (length_pos.2 h)
 
 theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := by
   cases l <;> simp [-not_or]
@@ -548,7 +533,7 @@ theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
   cases xs <;> simp
 
 theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
-  rw [isEmpty_iff, length_eq_zero_iff]
+  rw [isEmpty_iff, length_eq_zero]
 
 /-! ### any / all -/
 
@@ -925,13 +910,13 @@ theorem head?_eq_getElem? : ∀ l : List α, head? l = l[0]?
   | [] => rfl
   | a :: l => by simp
 
-theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos_iff.mpr h) := by
+theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos.mpr h) := by
   cases l with
   | nil => simp at h
   | cons _ _ => simp
 
 theorem getElem_zero_eq_head (l : List α) (h : 0 < l.length) :
-    l[0] = head l (by simpa [length_pos_iff] using h) := by
+    l[0] = head l (by simpa [length_pos] using h) := by
   cases l with
   | nil => simp at h
   | cons _ _ => simp
@@ -1018,7 +1003,7 @@ theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail ≠ []) : 1 < l.l
   | nil => simp at h
   | cons _ l =>
     simp only [tail_cons, ne_eq] at h
-    exact Nat.lt_add_of_pos_left (length_pos_iff.mpr h)
+    exact Nat.lt_add_of_pos_left (length_pos.mpr h)
 
 @[simp] theorem head_tail (l : List α) (h : l.tail ≠ []) :
     (tail l).head h = l[1]'(one_lt_length_of_tail_ne_nil h) := by
@@ -2898,7 +2883,7 @@ theorem getLast?_replicate (a : α) (n : Nat) : (replicate n a).getLast? = if n
 -- We unfold `leftpad` and `rightpad` for verification purposes.
 attribute [simp] leftpad rightpad
 
--- `length_leftpad` and `length_rightpad` are in `Init.Data.List.Nat.Basic`.
+-- `length_leftpad` is in `Init.Data.List.Nat.Basic`.
 
 theorem leftpad_prefix (n : Nat) (a : α) (l : List α) :
     replicate (n - length l) a <+: leftpad n a l := by
@@ -3086,12 +3071,8 @@ variable [BEq α]
 @[simp] theorem replace_cons_self [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
   simp [replace_cons]
 
-@[simp] theorem replace_of_not_mem [LawfulBEq α] {l : List α} (h : a ∉ l) : l.replace a b = l := by
-  induction l with
-  | nil => rfl
-  | cons x xs ih =>
-    simp only [replace_cons]
-    split <;> simp_all
+@[simp] theorem replace_of_not_mem {l : List α} (h : !l.elem a) : l.replace a b = l := by
+  induction l <;> simp_all [replace_cons]
 
 @[simp] theorem length_replace {l : List α} : (l.replace a b).length = l.length := by
   induction l with
@@ -3174,7 +3155,7 @@ theorem replace_take {l : List α} {i : Nat} :
     (replicate n a).replace a b = b :: replicate (n - 1) a := by
   cases n <;> simp_all [replicate_succ, replace_cons]
 
-@[simp] theorem replace_replicate_ne [LawfulBEq α] {a b c : α} (h : !b == a) :
+@[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
     (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all
@@ -3436,7 +3417,7 @@ theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} :
 theorem get_cons_succ' {as : List α} {i : Fin as.length} :
   (a :: as).get i.succ = as.get i := rfl
 
-theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos_iff.mp h)
+theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h)
   | _::_, _ => rfl
 
 set_option linter.deprecated false in

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
 
@@ -44,42 +44,10 @@ theorem tail_dropLast (l : List α) : tail (dropLast l) = dropLast (tail l) := b
 
 /-! ### filter -/
 
-@[simp]
-theorem length_filter_pos_iff {l : List α} {p : α → Bool} :
-    0 < (filter p l).length ↔ ∃ x ∈ l, p x := by
-  simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using
-    countP_pos_iff (p := p)
-
-@[simp]
 theorem length_filter_lt_length_iff_exists {l} :
-    (filter p l).length < l.length ↔ ∃ x ∈ l, ¬p x := by
-  simp [length_eq_countP_add_countP p l, countP_eq_length_filter]
-
-/-! ### filterMap -/
-
-@[simp]
-theorem length_filterMap_pos_iff {xs : List α} {f : α → Option β} :
-    0 < (filterMap f xs).length ↔ ∃ (x : α) (_ : x ∈ xs) (b : β), f x = some b := by
-  induction xs with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [filterMap, mem_cons, exists_prop, exists_eq_or_imp]
-    split
-    · simp_all [ih]
-    · simp_all
-
-@[simp]
-theorem length_filterMap_lt_length_iff_exists {xs : List α} {f : α → Option β} :
-    (filterMap f xs).length < xs.length ↔ ∃ (x : α) (_ : x ∈ xs), f x = none := by
-  induction xs with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [filterMap, mem_cons, exists_prop, exists_eq_or_imp]
-    split
-    · simp_all only [exists_prop, length_cons, true_or, iff_true]
-      have := length_filterMap_le f xs
-      omega
-    · simp_all
+    length (filter p l) < length l ↔ ∃ x ∈ l, ¬p x := by
+  simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using
+    countP_pos_iff (p := fun x => ¬p x)
 
 /-! ### reverse -/
 
@@ -95,18 +63,10 @@ theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) :
   to the larger of `n` and `l.length` -/
 -- We don't mark this as a `@[simp]` lemma since we allow `simp` to unfold `leftpad`,
 -- so the left hand side simplifies directly to `n - l.length + l.length`.
-theorem length_leftpad (n : Nat) (a : α) (l : List α) :
+theorem leftpad_length (n : Nat) (a : α) (l : List α) :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
 
-@[deprecated length_leftpad (since := "2025-02-24")]
-abbrev leftpad_length := @length_leftpad
-
-theorem length_rightpad (n : Nat) (a : α) (l : List α) :
-    (rightpad n a l).length = max n l.length := by
-  simp [rightpad]
-  omega
-
 /-! ### eraseIdx -/
 
 theorem mem_eraseIdx_iff_getElem {x : α} :

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
 
@@ -156,7 +156,7 @@ theorem append_sublist_of_sublist_left {xs ys zs : List α} (h : zs <+ xs) :
     have hl' := h'.length_le
     simp only [length_append] at hl'
     have : ys.length = 0 := by omega
-    simp_all only [Nat.add_zero, length_eq_zero_iff, true_and, append_nil]
+    simp_all only [Nat.add_zero, length_eq_zero, true_and, append_nil]
     exact Sublist.eq_of_length_le h' hl
   · rintro ⟨rfl, rfl⟩
     simp
@@ -169,7 +169,7 @@ theorem append_sublist_of_sublist_right {xs ys zs : List α} (h : zs <+ ys) :
     have hl' := h'.length_le
     simp only [length_append] at hl'
     have : xs.length = 0 := by omega
-    simp_all only [Nat.zero_add, length_eq_zero_iff, true_and, append_nil]
+    simp_all only [Nat.zero_add, length_eq_zero, true_and, append_nil]
     exact Sublist.eq_of_length_le h' hl
   · rintro ⟨rfl, rfl⟩
     simp

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 n : Nat, take i (replicate n a) = replicate (min i n) a
+@[simp] theorem take_replicate (a : α) : ∀ i j : Nat, take i (replicate j a) = replicate (min i j) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
   | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]
 
-@[simp] theorem drop_replicate (a : α) : ∀ i n : Nat, drop i (replicate n a) = replicate (n - i) a
+@[simp] theorem drop_replicate (a : α) : ∀ i j : Nat, drop i (replicate j a) = replicate (j - i) a
   | n, 0 => by simp
   | 0, m => by simp
   | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]

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
 
@@ -33,7 +33,7 @@ theorem range'_succ (s n step) : range' s (n + 1) step = s :: range' (s + step)
   | _ + 1 => congrArg succ (length_range' _ _ _)
 
 @[simp] theorem range'_eq_nil_iff : range' s n step = [] ↔ n = 0 := by
-  rw [← length_eq_zero_iff, length_range']
+  rw [← length_eq_zero, length_range']
 
 @[deprecated range'_eq_nil_iff (since := "2025-01-29")] abbrev range'_eq_nil := @range'_eq_nil_iff
 
@@ -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 n : Nat}, i < n → (range' s n step)[i]? = some (s + step * i)
+    ∀ {i j : Nat}, i < j → (range' s j 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 n : Nat} (h : i < n) : (range n)[i]? = some i := by
+theorem getElem?_range {i j : Nat} (h : i < j) : (range j)[i]? = some i := by
   simp [range_eq_range', getElem?_range' _ _ h]
 
-@[simp] theorem getElem_range {n : Nat} (j) (h : j < (range n).length) : (range n)[j] = j := by
+@[simp] theorem getElem_range {i : Nat} (j) (h : j < (range i).length) : (range i)[j] = j := by
   simp [range_eq_range']
 
 theorem range_succ_eq_map (n : Nat) : range (n + 1) = 0 :: map succ (range n) := by
@@ -164,7 +164,7 @@ theorem range'_eq_map_range (s n : Nat) : range' s n = map (s + ·) (range n) :=
   simp only [range_eq_range', length_range']
 
 @[simp] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by
-  rw [← length_eq_zero_iff, length_range]
+  rw [← length_eq_zero, length_range]
 
 theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
@@ -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 (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by
+theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
   rw [← range'_eq_map_range]
-  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm
+  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).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
 
@@ -45,7 +45,7 @@ theorem drop_one : ∀ l : List α, drop 1 l = tail l
     _ = succ (length l) - succ i := (Nat.succ_sub_succ_eq_sub (length l) i).symm
 
 theorem drop_of_length_le {l : List α} (h : l.length ≤ i) : drop i l = [] :=
-  length_eq_zero_iff.1 (length_drop .. ▸ Nat.sub_eq_zero_of_le h)
+  length_eq_zero.1 (length_drop .. ▸ Nat.sub_eq_zero_of_le h)
 
 theorem length_lt_of_drop_ne_nil {l : List α} {i} (h : drop i l ≠ []) : i < l.length :=
   gt_of_not_le (mt drop_of_length_le h)

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
 
@@ -44,16 +44,6 @@ theorem toArray_inj {as bs : List α} (h : as.toArray = bs.toArray) : as = bs :=
     | nil => simp at h
     | cons b bs => simpa using h
 
-theorem toArray_eq_iff {as : List α} {bs : Array α} : as.toArray = bs ↔ as = bs.toList := by
-  cases bs
-  simp
-
--- We can't make this a `@[simp]` lemma because `#[] = [].toArray` at reducible transparency,
--- so this would loop with `toList_eq_nil_iff`
-theorem eq_toArray_iff {as : Array α} {bs : List α} : as = bs.toArray ↔ as.toList = bs := by
-  cases as
-  simp
-
 @[simp] theorem size_toArrayAux {as : List α} {xs : Array α} :
     (as.toArrayAux xs).size = xs.size + as.length := by
   simp [size]
@@ -87,21 +77,6 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
     l.toArray.back = l.getLast (by simp at h; exact ne_nil_of_length_pos h) := by
   simp [back, List.getLast_eq_getElem]
 
-@[simp] theorem _root_.Array.getLast!_toList [Inhabited α] (xs : Array α) :
-    xs.toList.getLast! = xs.back! := by
-  rcases xs with ⟨xs⟩
-  simp
-
-@[simp] theorem _root_.Array.getLast?_toList (xs : Array α) :
-    xs.toList.getLast? = xs.back? := by
-  rcases xs with ⟨xs⟩
-  simp
-
-@[simp] theorem _root_.Array.getLast_toList (xs : Array α) (h) :
-    xs.toList.getLast h = xs.back (by simpa [ne_nil_iff_length_pos] using h) := by
-  rcases xs with ⟨xs⟩
-  simp
-
 @[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) :
     (l.toArray.set i a) = (l.set i a).toArray := rfl
 
@@ -539,8 +514,8 @@ private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) :
 
 @[simp] theorem toArray_replicate (n : Nat) (v : α) : (List.replicate n v).toArray = mkArray n v := rfl
 
-theorem _root_.Array.mkArray_eq_toArray_replicate : mkArray n v = (List.replicate n v).toArray := by
-  simp
+@[deprecated toArray_replicate (since := "2024-12-13")]
+abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
 
 @[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
 
@@ -658,46 +633,4 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
   · simp only [size_toArray, Nat.not_le] at h'
     rw [List.insertIdx_of_length_lt (h := h')]
 
-@[simp]
-theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) :
-    l.toArray.replace a b = (l.replace a b).toArray := by
-  rw [Array.replace]
-  split <;> rename_i i h
-  · simp only [finIdxOf?_toArray, finIdxOf?_eq_none_iff] at h
-    rw [replace_of_not_mem]
-    simpa
-  · simp_all only [finIdxOf?_toArray, finIdxOf?_eq_some_iff, Fin.getElem_fin, set_toArray,
-      mk.injEq]
-    apply List.ext_getElem
-    · simp
-    · intro j h₁ h₂
-      rw [List.getElem_replace, List.getElem_set]
-      by_cases h₃ : j < i
-      · rw [if_neg (by omega), if_neg]
-        simp only [length_set] at h₁ h₃
-        simpa using h.2 ⟨j, by omega⟩ h₃
-      · by_cases h₃ : j = i
-        · rw [if_pos (by omega), if_pos, if_neg]
-          · simp only [mem_take_iff_getElem, not_exists]
-            intro k hk
-            simpa using h.2 ⟨k, by omega⟩ (by show k < i.1; omega)
-          · subst h₃
-            simpa using h.1
-        · rw [if_neg (by omega)]
-          split
-          · rw [if_pos]
-            · simp_all
-            · simp only [mem_take_iff_getElem]
-              simp only [length_set] at h₁
-              exact ⟨i, by omega, h.1⟩
-          · rfl
-
-@[simp] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) :
-    Array.leftpad n a l.toArray = (leftpad n a l).toArray := by
-  simp [leftpad, Array.leftpad, ← toArray_replicate]
-
-@[simp] theorem rightpad_toArray (n : Nat) (a : α) (l : List α) :
-    Array.rightpad n a l.toArray = (rightpad n a l).toArray := by
-  simp [rightpad, Array.rightpad, ← toArray_replicate]
-
 end List

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/NeZero.lean

@@ -40,20 +40,3 @@ theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
 instance {p : Prop} [Decidable p] {n m : Nat} [NeZero n] [NeZero m] :
     NeZero (if p then n else m) := by
   split <;> infer_instance
-
-instance {n m : Nat} [h : NeZero n] : NeZero (n + m) where
-  out :=
-    match n, h, m with
-    | _ + 1, _, 0
-    | _ + 1, _, _ + 1 => fun h => nomatch h
-
-instance {n m : Nat} [h : NeZero m] : NeZero (n + m) where
-  out :=
-    match m, h, n with
-    | _ + 1, _, 0 => fun h => nomatch h
-    | _ + 1, _, _ + 1 => fun h => nomatch h
-
-instance {n m : Nat} [hn : NeZero n] [hm : NeZero m] : NeZero (n * m) where
-  out :=
-    match n, hn, m, hm with
-    | _ + 1, _, _ + 1, _ => fun h => nomatch h

src/Init/Data/Option/Lemmas.lean

@@ -654,11 +654,6 @@ theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H)
     Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H := by
   cases o <;> simp
 
-theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p b → γ) (H) :
-    pmap g (o.map f) H =
-      pmap (fun a h => g (f a) h) o (fun a m => H (f a) (mem_map_of_mem f m)) := by
-  cases o <;> simp
-
 /-! ### pelim -/
 
 @[simp] theorem pelim_none : pelim none b f = b := rfl

src/Init/Data/SInt.lean

@@ -7,7 +7,6 @@ prelude
 import Init.Data.SInt.Basic
 import Init.Data.SInt.Float
 import Init.Data.SInt.Float32
-import Init.Data.SInt.Lemmas
 
 /-!
 This module contains the definitions and basic theory about signed fixed width integer types.

src/Init/Data/SInt/Lemmas.lean

@@ -1,13 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-prelude
-import Init.Data.SInt.Basic
-
-@[simp] theorem UInt8.toBitVec_toInt8 (x : UInt8) : x.toInt8.toBitVec = x.toBitVec := rfl
-@[simp] theorem UInt16.toBitVec_toInt16 (x : UInt16) : x.toInt16.toBitVec = x.toBitVec := rfl
-@[simp] theorem UInt32.toBitVec_toInt32 (x : UInt32) : x.toInt32.toBitVec = x.toBitVec := rfl
-@[simp] theorem UInt64.toBitVec_toInt64 (x : UInt64) : x.toInt64.toBitVec = x.toBitVec := rfl
-@[simp] theorem USize.toBitVec_toISize (x : USize) : x.toISize.toBitVec = x.toBitVec := rfl

src/Init/Data/UInt/Basic.lean

@@ -295,16 +295,11 @@ def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
 def USize.ofNatCore (n : Nat) (h : n < USize.size) : USize :=
   USize.ofNatLT n h
 
-@[simp] theorem USize.le_size : 2 ^ 32 ≤ USize.size := by cases USize.size_eq <;> simp_all
-@[simp] theorem USize.size_le : USize.size ≤ 2 ^ 64 := by cases USize.size_eq <;> simp_all
+theorem usize_size_le : USize.size ≤ 18446744073709551616 := by
+  cases usize_size_eq <;> next h => rw [h]; decide
 
-@[deprecated USize.size_le (since := "2025-02-24")]
-theorem usize_size_le : USize.size ≤ 18446744073709551616 :=
-  USize.size_le
-
-@[deprecated USize.le_size (since := "2025-02-24")]
-theorem le_usize_size : 4294967296 ≤ USize.size :=
-  USize.le_size
+theorem le_usize_size : 4294967296 ≤ USize.size := by
+  cases usize_size_eq <;> next h => rw [h]; decide
 
 @[extern "lean_usize_mul"]
 def USize.mul (a b : USize) : USize := ⟨a.toBitVec * b.toBitVec⟩
@@ -331,7 +326,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_of_nat"]
 def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize :=
-  USize.ofNatLT n (Nat.lt_of_lt_of_le h USize.le_size)
+  USize.ofNatLT n (Nat.lt_of_lt_of_le h le_usize_size)
 @[extern "lean_uint8_to_usize"]
 def UInt8.toUSize (a : UInt8) : USize :=
   USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide))
@@ -356,7 +351,7 @@ This function is overridden with a native implementation.
 -/
 @[extern "lean_usize_to_uint64"]
 def USize.toUInt64 (a : USize) : UInt64 :=
-  UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt USize.size_le)
+  UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt usize_size_le)
 
 instance : Mul USize       := ⟨USize.mul⟩
 instance : Mod USize       := ⟨USize.mod⟩

src/Init/Data/UInt/BasicAux.lean

@@ -138,16 +138,8 @@ def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBit
 
 instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 
-@[deprecated USize.size_eq (since := "2025-02-24")]
-theorem usize_size_eq : USize.size = 4294967296 ∨ USize.size = 18446744073709551616 :=
-  USize.size_eq
-
-@[deprecated USize.size_pos (since := "2025-02-24")]
-theorem usize_size_pos : 0 < USize.size :=
-  USize.size_pos
-
-@[deprecated USize.size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
-  USize.size_pos
+@[deprecated usize_size_pos (since := "2024-11-24")] theorem usize_size_gt_zero : USize.size > 0 :=
+  usize_size_pos
 
 /-- Converts a `USize` into the corresponding `Fin USize.size`. -/
 def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin
@@ -163,7 +155,7 @@ def USize.ofNatTruncate (n : Nat) : USize :=
   if h : n < USize.size then
     USize.ofNatLT n h
   else
-    USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt USize.size_pos))
+    USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt usize_size_pos))
 abbrev Nat.toUSize := USize.ofNat
 @[extern "lean_usize_to_nat"]
 def USize.toNat (n : USize) : Nat := n.toBitVec.toNat

src/Init/Data/UInt/Bitwise.lean

@@ -25,11 +25,11 @@ namespace $typeName
 @[simp, int_toBitVec] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
 @[simp, int_toBitVec] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
 
-@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat, -toNat_toBitVec]
-@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat, -toNat_toBitVec]
-@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by simp [toNat, -toNat_toBitVec]
-@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := by simp [toNat, -toNat_toBitVec]
-@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := by simp [toNat, -toNat_toBitVec]
+@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat]
+@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat]
+@[simp] protected theorem toNat_xor (a b : $typeName) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := by simp [toNat]
+@[simp] protected theorem toNat_shiftLeft (a b : $typeName) : (a <<< b).toNat = a.toNat <<< (b.toNat % $bits) % 2 ^ $bits := by simp [toNat]
+@[simp] protected theorem toNat_shiftRight (a b : $typeName) : (a >>> b).toNat = a.toNat >>> (b.toNat % $bits) := by simp [toNat]
 
 open $typeName (toNat_and) in
 @[deprecated toNat_and (since := "2024-11-28")]
@@ -37,6 +37,7 @@ protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.
 
 end $typeName
 )
+
 declare_bitwise_uint_theorems UInt8 8
 declare_bitwise_uint_theorems UInt16 16
 declare_bitwise_uint_theorems UInt32 32

src/Init/Data/UInt/Lemmas.lean

@@ -34,23 +34,15 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   @[deprecated toNat_ofNatLT (since := "2025-02-13")]
   theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT ..
 
-  @[simp] theorem toFin_val (x : $typeName) : x.toFin.val = x.toNat := rfl
-  @[deprecated toFin_val (since := "2025-02-12")]
+  @[simp] theorem toFin_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl
+  @[deprecated toFin_val_eq_toNat (since := "2025-02-12")]
   theorem val_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl
 
-  @[simp] theorem toNat_toBitVec (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
-  @[simp] theorem toFin_toBitVec (x : $typeName) : x.toBitVec.toFin = x.toFin := rfl
-
-  @[deprecated toNat_toBitVec (since := "2025-02-21")]
   theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := rfl
 
-  @[simp] theorem ofBitVec_toBitVec : ∀ (a : $typeName), ofBitVec a.toBitVec = a
+  @[simp] theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
     | ⟨_, _⟩ => rfl
 
-  @[deprecated ofBitVec_toBitVec (since := "2025-02-21")]
-  theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a :=
-    ofBitVec_toBitVec
-
   @[deprecated ofBitVec_toBitVec_eq (since := "2025-02-12")]
   theorem mk_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
     | ⟨_, _⟩ => rfl
@@ -249,174 +241,21 @@ declare_uint_theorems USize System.Platform.numBits
 
 @[simp] theorem USize.toNat_ofNat32 {n : Nat} {h : n < 4294967296} : (ofNat32 n h).toNat = n := rfl
 
-@[simp] theorem USize.toNat_toUInt8 (x : USize) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
-@[simp] theorem USize.toNat_toUInt16 (x : USize) : x.toUInt16.toNat = x.toNat % 2 ^ 16 := rfl
-@[simp] theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl
+@[simp] theorem USize.toNat_toUInt32 (x : USize) : x.toUInt32.toNat = x.toNat % 2 ^ 32  := rfl
+
 @[simp] theorem USize.toNat_toUInt64 (x : USize) : x.toUInt64.toNat = x.toNat := rfl
 
 theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : toNat (ofNat n) = n :=
-  toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h USize.le_size)
+  toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h le_usize_size)
 
 theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
-  simp [-toNat_toBitVec, lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
 
 theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by
-  simp [-toNat_toBitVec, lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  simp [lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
 
 theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by
-  simp [-toNat_toBitVec, le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
 
 theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
-  simp [-toNat_toBitVec, le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
-
-@[simp] theorem UInt8.toNat_lt (n : UInt8) : n.toNat < 2 ^ 8 := n.toFin.isLt
-@[simp] theorem UInt16.toNat_lt (n : UInt16) : n.toNat < 2 ^ 16 := n.toFin.isLt
-@[simp] theorem UInt32.toNat_lt (n : UInt32) : n.toNat < 2 ^ 32 := n.toFin.isLt
-@[simp] theorem UInt64.toNat_lt (n : UInt64) : n.toNat < 2 ^ 64 := n.toFin.isLt
-
-theorem UInt8.size_lt_usizeSize : UInt8.size < USize.size := by
-  cases USize.size_eq <;> simp_all +decide
-theorem UInt8.size_le_usizeSize : UInt8.size ≤ USize.size :=
-  Nat.le_of_lt UInt8.size_lt_usizeSize
-theorem UInt16.size_lt_usizeSize : UInt16.size < USize.size := by
-  cases USize.size_eq <;> simp_all +decide
-theorem UInt16.size_le_usizeSize : UInt16.size ≤ USize.size :=
-  Nat.le_of_lt UInt16.size_lt_usizeSize
-theorem UInt32.size_le_usizeSize : UInt32.size ≤ USize.size := by
-  cases USize.size_eq <;> simp_all +decide
-theorem USize.size_eq_two_pow : USize.size = 2 ^ System.Platform.numBits := rfl
-theorem USize.toNat_lt_two_pow_numBits (n : USize) : n.toNat < 2 ^ System.Platform.numBits := n.toFin.isLt
-@[simp] theorem USize.toNat_lt (n : USize) : n.toNat < 2 ^ 64 := Nat.lt_of_lt_of_le n.toFin.isLt size_le
-
-theorem UInt8.toNat_lt_usizeSize (n : UInt8) : n.toNat < USize.size :=
-  Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
-theorem UInt16.toNat_lt_usizeSize (n : UInt16) : n.toNat < USize.size :=
-  Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
-theorem UInt32.toNat_lt_usizeSize (n : UInt32) : n.toNat < USize.size :=
-  Nat.lt_of_lt_of_le n.toNat_lt (by cases USize.size_eq <;> simp_all)
-
-@[simp] theorem Fin.mk_uInt8ToNat (n : UInt8) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-@[simp] theorem Fin.mk_uInt16ToNat (n : UInt16) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-@[simp] theorem Fin.mk_uInt32ToNat (n : UInt32) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-@[simp] theorem Fin.mk_uInt64ToNat (n : UInt64) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-@[simp] theorem Fin.mk_uSizeToNat (n : USize) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-
-@[simp] theorem BitVec.ofNatLT_uInt8ToNat (n : UInt8) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-@[simp] theorem BitVec.ofNatLT_uInt16ToNat (n : UInt16) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-@[simp] theorem BitVec.ofNatLT_uInt32ToNat (n : UInt32) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-@[simp] theorem BitVec.ofNatLT_uInt64ToNat (n : UInt64) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-@[simp] theorem BitVec.ofNatLT_uSizeToNat (n : USize) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-
-@[simp] theorem BitVec.ofFin_uInt8ToFin (n : UInt8) : BitVec.ofFin n.toFin = n.toBitVec := rfl
-@[simp] theorem BitVec.ofFin_uInt16ToFin (n : UInt16) : BitVec.ofFin n.toFin = n.toBitVec := rfl
-@[simp] theorem BitVec.ofFin_uInt32ToFin (n : UInt32) : BitVec.ofFin n.toFin = n.toBitVec := rfl
-@[simp] theorem BitVec.ofFin_uInt64ToFin (n : UInt64) : BitVec.ofFin n.toFin = n.toBitVec := rfl
-@[simp] theorem BitVec.ofFin_uSizeToFin (n : USize) : BitVec.ofFin n.toFin = n.toBitVec := rfl
-
-@[simp] theorem UInt8.toFin_toUInt16 (n : UInt8) : n.toUInt16.toFin = n.toFin.castLE (by decide) := rfl
-@[simp] theorem UInt8.toFin_toUInt32 (n : UInt8) : n.toUInt32.toFin = n.toFin.castLE (by decide) := rfl
-@[simp] theorem UInt8.toFin_toUInt64 (n : UInt8) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
-@[simp] theorem UInt8.toFin_toUSize (n : UInt8) :
-  n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
-
-@[simp] theorem UInt16.toFin_toUInt32 (n : UInt16) : n.toUInt32.toFin = n.toFin.castLE (by decide) := rfl
-@[simp] theorem UInt16.toFin_toUInt64 (n : UInt16) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
-@[simp] theorem UInt16.toFin_toUSize (n : UInt16) :
-  n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
-
-@[simp] theorem UInt32.toFin_toUInt64 (n : UInt32) : n.toUInt64.toFin = n.toFin.castLE (by decide) := rfl
-@[simp] theorem UInt32.toFin_toUSize (n : UInt32) :
-  n.toUSize.toFin = n.toFin.castLE size_le_usizeSize := rfl
-
-@[simp] theorem USize.toFin_toUInt64 (n : USize) : n.toUInt64.toFin = n.toFin.castLE size_le_usizeSize := rfl
-
-@[simp] theorem UInt16.toBitVec_toUInt8 (n : UInt16) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
-@[simp] theorem UInt32.toBitVec_toUInt8 (n : UInt32) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
-@[simp] theorem UInt64.toBitVec_toUInt8 (n : UInt64) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := rfl
-@[simp] theorem USize.toBitVec_toUInt8 (n : USize) : n.toUInt8.toBitVec = n.toBitVec.setWidth 8 := BitVec.eq_of_toNat_eq (by simp)
-
-@[simp] theorem UInt8.toBitVec_toUInt16 (n : UInt8) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
-@[simp] theorem UInt32.toBitVec_toUInt16 (n : UInt32) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
-@[simp] theorem UInt64.toBitVec_toUInt16 (n : UInt64) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := rfl
-@[simp] theorem USize.toBitVec_toUInt16 (n : USize) : n.toUInt16.toBitVec = n.toBitVec.setWidth 16 := BitVec.eq_of_toNat_eq (by simp)
-
-@[simp] theorem UInt8.toBitVec_toUInt32 (n : UInt8) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
-@[simp] theorem UInt16.toBitVec_toUInt32 (n : UInt16) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
-@[simp] theorem UInt64.toBitVec_toUInt32 (n : UInt64) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := rfl
-@[simp] theorem USize.toBitVec_toUInt32 (n : USize) : n.toUInt32.toBitVec = n.toBitVec.setWidth 32 := BitVec.eq_of_toNat_eq (by simp)
-
-@[simp] theorem UInt8.toBitVec_toUInt64 (n : UInt8) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
-@[simp] theorem UInt16.toBitVec_toUInt64 (n : UInt16) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
-@[simp] theorem UInt32.toBitVec_toUInt64 (n : UInt32) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 := rfl
-@[simp] theorem USize.toBitVec_toUInt64 (n : USize) : n.toUInt64.toBitVec = n.toBitVec.setWidth 64 :=
-  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt (USize.toNat_lt _)])
-
-@[simp] theorem UInt8.toBitVec_toUSize (n : UInt8) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
-  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
-@[simp] theorem UInt16.toBitVec_toUSize (n : UInt16) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
-  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
-@[simp] theorem UInt32.toBitVec_toUSize (n : UInt32) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
-  BitVec.eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt n.toNat_lt_usizeSize])
-@[simp] theorem UInt64.toBitVec_toUSize (n : UInt64) : n.toUSize.toBitVec = n.toBitVec.setWidth System.Platform.numBits :=
-  BitVec.eq_of_toNat_eq (by simp)
-
-@[simp] theorem UInt8.ofNatLT_toNat (n : UInt8) : UInt8.ofNatLT n.toNat n.toNat_lt = n := rfl
-@[simp] theorem UInt16.ofNatLT_uInt8ToNat (n : UInt8) : UInt16.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt16 := rfl
-@[simp] theorem UInt32.ofNatLT_uInt8ToNat (n : UInt8) : UInt32.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt32 := rfl
-@[simp] theorem UInt64.ofNatLT_uInt8ToNat (n : UInt8) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
-@[simp] theorem USize.ofNatLT_uInt8ToNat (n : UInt8) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
-
-@[simp] theorem UInt16.ofNatLT_toNat (n : UInt16) : UInt16.ofNatLT n.toNat n.toNat_lt = n := rfl
-@[simp] theorem UInt32.ofNatLT_uInt16ToNat (n : UInt16) : UInt32.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt32 := rfl
-@[simp] theorem UInt64.ofNatLT_uInt16ToNat (n : UInt16) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
-@[simp] theorem USize.ofNatLT_uInt16ToNat (n : UInt16) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
-
-@[simp] theorem UInt32.ofNatLT_toNat (n : UInt32) : UInt32.ofNatLT n.toNat n.toNat_lt = n := rfl
-@[simp] theorem UInt64.ofNatLT_uInt32ToNat (n : UInt32) : UInt64.ofNatLT n.toNat (Nat.lt_trans n.toNat_lt (by decide)) = n.toUInt64 := rfl
-@[simp] theorem USize.ofNatLT_uInt32ToNat (n : UInt32) : USize.ofNatLT n.toNat n.toNat_lt_usizeSize = n.toUSize := rfl
-
-@[simp] theorem UInt64.ofNatLT_toNat (n : UInt64) : UInt64.ofNatLT n.toNat n.toNat_lt = n := rfl
-
-@[simp] theorem USize.ofNatLT_toNat (n : USize) : USize.ofNatLT n.toNat n.toNat_lt_size = n := rfl
-@[simp] theorem UInt64.ofNatLT_uSizeToNat (n : USize) : UInt64.ofNatLT n.toNat n.toNat_lt = n.toUInt64 := rfl
-
--- We are not making these into `simp` lemmas because they lose the information stored in `h`. ·
-theorem UInt8.ofNatLT_uInt16ToNat (n : UInt16) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
-  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt8.ofNatLT_uInt32ToNat (n : UInt32) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
-  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt8.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
-  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt8.ofNatLT_uSizeToNat (n : USize) (h) : UInt8.ofNatLT n.toNat h = n.toUInt8 :=
-  UInt8.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt16.ofNatLT_uInt32ToNat (n : UInt32) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
-  UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt16.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
-  UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt16.ofNatLT_uSizeToNat (n : USize) (h) : UInt16.ofNatLT n.toNat h = n.toUInt16 :=
-  UInt16.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt32.ofNatLT_uInt64ToNat (n : UInt64) (h) : UInt32.ofNatLT n.toNat h = n.toUInt32 :=
-  UInt32.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem UInt32.ofNatLT_uSizeToNat (n : USize) (h) : UInt32.ofNatLT n.toNat h = n.toUInt32 :=
-  UInt32.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-theorem USize.ofNatLT_uInt64ToNat (n : UInt64) (h) : USize.ofNatLT n.toNat h = n.toUSize :=
-  USize.toNat.inj (by simp [Nat.mod_eq_of_lt h])
-
-@[simp] theorem UInt8.ofFin_toFin (n : UInt8) : UInt8.ofFin n.toFin = n := rfl
-@[simp] theorem UInt16.ofFin_toFin (n : UInt16) : UInt16.ofFin n.toFin = n := rfl
-@[simp] theorem UInt32.ofFin_toFin (n : UInt32) : UInt32.ofFin n.toFin = n := rfl
-@[simp] theorem UInt64.ofFin_toFin (n : UInt64) : UInt64.ofFin n.toFin = n := rfl
-@[simp] theorem USize.ofFin_toFin (n : USize) : USize.ofFin n.toFin = n := rfl
-
-@[simp] theorem UInt16.ofFin_uint8ToFin (n : UInt8) : UInt16.ofFin (n.toFin.castLE (by decide)) = n.toUInt16 := rfl
-
-@[simp] theorem UInt32.ofFin_uint8ToFin (n : UInt8) : UInt32.ofFin (n.toFin.castLE (by decide)) = n.toUInt32 := rfl
-@[simp] theorem UInt32.ofFin_uint16ToFin (n : UInt16) : UInt32.ofFin (n.toFin.castLE (by decide)) = n.toUInt32 := rfl
-
-@[simp] theorem UInt64.ofFin_uint8ToFin (n : UInt8) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
-@[simp] theorem UInt64.ofFin_uint16ToFin (n : UInt16) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
-@[simp] theorem UInt64.ofFin_uint32ToFin (n : UInt32) : UInt64.ofFin (n.toFin.castLE (by decide)) = n.toUInt64 := rfl
-
-@[simp] theorem USize.ofFin_uint8ToFin (n : UInt8) : USize.ofFin (n.toFin.castLE UInt8.size_le_usizeSize) = n.toUSize := rfl
-@[simp] theorem USize.ofFin_uint16ToFin (n : UInt16) : USize.ofFin (n.toFin.castLE UInt16.size_le_usizeSize) = n.toUSize := rfl
-@[simp] theorem USize.ofFin_uint32ToFin (n : UInt32) : USize.ofFin (n.toFin.castLE UInt32.size_le_usizeSize) = n.toUSize := rfl
+  simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]

src/Init/Data/Vector/Basic.lean

@@ -455,27 +455,6 @@ to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
 @[inline] def count [BEq α] (a : α) (xs : Vector α n) : Nat :=
   xs.toArray.count a
 
-@[inline] def replace [BEq α] (xs : Vector α n) (a b : α) : Vector α n :=
-  ⟨xs.toArray.replace a b, by simp⟩
-
-/--
-Pad a vector on the left with a given element.
-
-Note that we immediately simplify this to an `++` operation,
-and do not provide separate verification theorems.
--/
-@[inline, simp] def leftpad (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m) :=
-  (mkVector (n - m) a ++ xs).cast (by omega)
-
-/--
-Pad a vector on the right with a given element.
-
-Note that we immediately simplify this to an `++` operation,
-and do not provide separate verification theorems.
--/
-@[inline, simp] def rightpad (n : Nat) (a : α) (xs : Vector α m) : Vector α (max n m) :=
-  (xs ++ mkVector (n - m) a).cast (by omega)
-
 /-! ### ForIn instance -/
 
 @[simp] theorem mem_toArray_iff (a : α) (xs : Vector α n) : a ∈ xs.toArray ↔ a ∈ xs :=

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,7 +101,6 @@ 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⟩
@@ -160,7 +159,6 @@ 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

@@ -6,13 +6,11 @@ Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison
 prelude
 import Init.Data.Vector.Basic
 import Init.Data.Array.Attach
-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.
 
@@ -246,9 +244,6 @@ abbrev zipWithIndex_mk := @zipIdx_mk
 @[simp] theorem count_mk [BEq α] (xs : Array α) (h : xs.size = n) (a : α) :
     (Vector.mk xs h).count a = xs.count a := rfl
 
-@[simp] theorem replace_mk [BEq α] (xs : Array α) (h : xs.size = n) (a b) :
-    (Vector.mk xs h).replace a b = Vector.mk (xs.replace a b) (by simp [h]) := rfl
-
 @[simp] theorem eq_mk : xs = Vector.mk as h ↔ xs.toArray = as := by
   cases xs
   simp
@@ -409,9 +404,6 @@ theorem toArray_mapM_go [Monad m] [LawfulMonad m] (f : α → m β) (xs : Vector
   cases xs
   simp
 
-@[simp] theorem replace_toArray [BEq α] (xs : Vector α n) (a b) :
-    xs.toArray.replace a b = (xs.replace a b).toArray := rfl
-
 @[simp] theorem find?_toArray (p : α → Bool) (xs : Vector α n) :
     xs.toArray.find? p = xs.find? p := by
   cases xs
@@ -670,12 +662,12 @@ protected theorem eq_empty (xs : Vector α 0) : xs = #v[] := by
 theorem eq_empty_of_size_eq_zero (xs : Vector α n) (h : n = 0) : xs = #v[].cast h.symm := by
   rcases xs with ⟨xs, rfl⟩
   apply toArray_inj.1
-  simp only [List.length_eq_zero_iff, Array.toList_eq_nil_iff] at h
+  simp only [List.length_eq_zero, Array.toList_eq_nil_iff] at h
   simp [h]
 
 theorem size_eq_one {xs : Vector α 1} : ∃ a, xs = #v[a] := by
   rcases xs with ⟨xs, h⟩
-  simpa using Array.size_eq_one_iff.mp h
+  simpa using Array.size_eq_one.mp h
 
 /-! ### push -/
 
@@ -1345,20 +1337,6 @@ theorem mem_setIfInBounds (xs : Vector α n) (i : Nat) (hi : i < n) (a : α) :
   cases ys
   simp
 
-/-! ### back -/
-
-theorem back_eq_getElem [NeZero n] (xs : Vector α n) : xs.back = xs[n - 1]'(by have := NeZero.ne n; omega) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.back_eq_getElem]
-
-theorem back?_eq_getElem? (xs : Vector α n) : xs.back? = xs[n - 1]? := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.back?_eq_getElem?]
-
-@[simp] theorem back_mem [NeZero n] {xs : Vector α n} : xs.back ∈ xs := by
-  cases xs
-  simp
-
 /-! ### map -/
 
 @[simp] theorem getElem_map (f : α → β) (xs : Vector α n) (i : Nat) (hi : i < n) :
@@ -2353,237 +2331,6 @@ theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} (r : β
   rcases xs with ⟨xs⟩
   simp
 
-/-! #### Further results about `back` and `back?` -/
-
-@[simp] theorem back?_eq_none_iff {xs : Vector α n} : xs.back? = none ↔ n = 0 := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-theorem back?_eq_some_iff {xs : Vector α n} {a : α} :
-    xs.back? = some a ↔ ∃ (w : 0 < n)(ys : Vector α (n - 1)), xs = (ys.push a).cast (by omega) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp only [back?_mk, Array.back?_eq_some_iff, mk_eq, toArray_cast, toArray_push]
-  constructor
-  · rintro ⟨ys, rfl⟩
-    simp
-    exact ⟨⟨ys, by simp⟩, by simp⟩
-  · rintro ⟨w, ⟨ys, h₁⟩, h₂⟩
-    exact ⟨ys, by simpa using h₂⟩
-
-@[simp] theorem back?_isSome {xs : Vector α n} : xs.back?.isSome ↔ n ≠ 0 := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem back_append_of_neZero {xs : Vector α n} {ys : Vector α m} [NeZero m] :
-    (xs ++ ys).back = ys.back := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp only [mk_append_mk, back_mk]
-  rw [Array.back_append_of_size_pos]
-
-theorem back_append {xs : Vector α n} {ys : Vector α m} [NeZero (n + m)] :
-    (xs ++ ys).back =
-      if h' : m = 0 then
-        have : NeZero n := by subst h'; simp_all
-        xs.back
-      else
-        have : NeZero m := ⟨h'⟩
-        ys.back := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp [Array.back_append]
-  split <;> rename_i h
-  · rw [dif_pos]
-    simp_all
-  · rw [dif_neg]
-    rwa [Array.isEmpty_iff_size_eq_zero] at h
-
-theorem back_append_right {xs : Vector α n} {ys : Vector α m} [NeZero m] :
-    (xs ++ ys).back = ys.back := by
-  rcases xs with ⟨xs⟩
-  rcases ys with ⟨ys⟩
-  simp only [mk_append_mk, back_mk]
-  rw [Array.back_append_right]
-
-theorem back_append_left {xs : Vector α n} {ys : Vector α 0} [NeZero n] :
-    (xs ++ ys).back = xs.back := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, h⟩
-  simp only [mk_append_mk, back_mk]
-  rw [Array.back_append_left _ h]
-
-@[simp] theorem back?_append {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).back? = ys.back?.or xs.back? := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp
-
-theorem back?_flatMap {xs : Vector α n} {f : α → Vector β m} :
-    (xs.flatMap f).back? = xs.reverse.findSome? fun a => (f a).back? := by
-  rcases xs with ⟨xs, rfl⟩
-  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⟩
-  simp [Array.back?_flatten, ← Array.map_reverse, Array.findSome?_map, Function.comp_def]
-  rfl
-
-theorem back?_mkVector (a : α) (n : Nat) :
-    (mkVector n a).back? = if n = 0 then none else some a := by
-  rw [mkVector_eq_mk_mkArray]
-  simp only [back?_mk, Array.back?_mkArray]
-
-@[simp] theorem back_mkArray [NeZero n] : (mkVector n a).back = a := by
-  simp [back_eq_getElem]
-
-/-! ### leftpad and rightpad -/
-
-@[simp] theorem leftpad_mk (n : Nat) (a : α) (xs : Array α) (h : xs.size = m) :
-    (Vector.mk xs h).leftpad n a = Vector.mk (Array.leftpad n a xs) (by simp [h]; omega) := by
-  simp [h]
-
-@[simp] theorem rightpad_mk (n : Nat) (a : α) (xs : Array α) (h : xs.size = m) :
-    (Vector.mk xs h).rightpad n a = Vector.mk (Array.rightpad n a xs) (by simp [h]; omega) := by
-  simp [h]
-
-/-! ### contains -/
-
-theorem contains_eq_any_beq [BEq α] (xs : Vector α n) (a : α) : xs.contains a = xs.any (a == ·) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.contains_eq_any_beq]
-
-theorem contains_iff_exists_mem_beq [BEq α] {xs : Vector α n} {a : α} :
-    xs.contains a ↔ ∃ a' ∈ xs, a == a' := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.contains_iff_exists_mem_beq]
-
-theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
-    xs.contains a ↔ a ∈ xs := by
-  simp
-
-/-! ### more lemmas about `pop` -/
-
-@[simp] theorem pop_empty : (#v[] : Vector α 0).pop = #v[] := rfl
-
-@[simp] theorem pop_push (xs : Vector α n) : (xs.push x).pop = xs := by simp [pop]
-
-@[simp] theorem getElem_pop {xs : Vector α n} {i : Nat} (h : i < n - 1) :
-    xs.pop[i] = xs[i] := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-theorem getElem?_pop (xs : Vector α n) (i : Nat) :
-    xs.pop[i]? = if i < n - 1 then xs[i]? else none := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.getElem?_pop]
-
-theorem back_pop {xs : Vector α n} [h : NeZero (n - 1)] :
-   xs.pop.back =
-     xs[n - 2]'(by have := h.out; omega) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.back_pop]
-
-theorem back?_pop {xs : Vector α n} :
-    xs.pop.back? = if n ≤ 1 then none else xs[n - 2]? := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.back?_pop]
-
-@[simp] theorem pop_append_of_size_ne_zero {xs : Vector α n} {ys : Vector α m} (h : m ≠ 0) :
-    (xs ++ ys).pop = (xs ++ ys.pop).cast (by omega) := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp only [mk_append_mk, pop_mk, cast_mk, eq_mk]
-  rw [Array.pop_append_of_ne_empty]
-  apply Array.ne_empty_of_size_pos
-  omega
-
-theorem pop_append {xs : Vector α n} {ys : Vector α m} :
-    (xs ++ ys).pop = if h : m = 0 then xs.pop.cast (by omega) else (xs ++ ys.pop).cast (by omega) := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp only [mk_append_mk, pop_mk, List.length_eq_zero_iff, Array.toList_eq_nil_iff, cast_mk, mk_eq]
-  rw [Array.pop_append]
-  split <;> simp_all
-
-@[simp] theorem pop_mkVector (n) (a : α) : (mkVector n a).pop = mkVector (n - 1) a := by
-  ext <;> simp
-
-/-! ### replace -/
-
-section replace
-variable [BEq α]
-
-@[simp] theorem replace_cast {xs : Vector α n} {a b : α} :
-    (xs.cast h).replace a b = (xs.replace a b).cast (by simp [h]) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
--- This hypothesis could probably be dropped from some of the lemmas below,
--- by proving them direct from the definition rather than going via `List`.
-variable [LawfulBEq α]
-
-@[simp] theorem replace_of_not_mem {xs : Vector α n} (h : ¬ a ∈ xs) : xs.replace a b = xs := by
-  rcases xs with ⟨xs, rfl⟩
-  simp_all
-
-theorem getElem?_replace {xs : Vector α n} {i : Nat} :
-    (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.getElem?_replace]
-  split <;> rename_i h
-  · rw (occs := [2]) [if_pos]
-    simpa using h
-  · rw [if_neg]
-    simpa using h
-
-theorem getElem?_replace_of_ne {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some a) :
-    (xs.replace a b)[i]? = xs[i]? := by
-  simp_all [getElem?_replace]
-
-theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
-    (xs.replace a b)[i] = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
-  apply Option.some.inj
-  rw [← getElem?_eq_getElem, getElem?_replace]
-  split <;> split <;> simp_all
-
-theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[i] ≠ a) :
-    (xs.replace a b)[i]'(by simpa) = xs[i]'(h) := by
-  rw [getElem_replace h]
-  simp [h']
-
-theorem replace_append {xs : Vector α n} {ys : Vector α m} :
-    (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp only [mk_append_mk, replace_mk, eq_mk, Array.replace_append]
-  split <;> simp_all
-
-theorem replace_append_left {xs : Vector α n} {ys : Vector α m} (h : a ∈ xs) :
-    (xs ++ ys).replace a b = xs.replace a b ++ ys := by
-  simp [replace_append, h]
-
-theorem replace_append_right {xs : Vector α n} {ys : Vector α m} (h : ¬ a ∈ xs) :
-    (xs ++ ys).replace a b = xs ++ ys.replace a b := by
-  simp [replace_append, h]
-
-theorem replace_extract {xs : Vector α n} {i : Nat} :
-    (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.replace_extract]
-
-@[simp] theorem replace_mkArray_self {a : α} (h : 0 < n) :
-    (mkVector n a).replace a b = (#v[b] ++ mkVector (n - 1) a).cast (by omega) := by
-  match n, h with
-  | n + 1, _ => simp_all [mkVector_succ', replace_append]
-
-@[simp] theorem replace_mkArray_ne {a b c : α} (h : !b == a) :
-    (mkVector n a).replace b c = mkVector n a := by
-  rw [replace_of_not_mem]
-  simp_all
-
-end replace
 
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
@@ -2592,6 +2339,10 @@ set_option linter.indexVariables false in
   rcases xs with ⟨xs, rfl⟩
   simp
 
+@[simp] theorem getElem_pop {xs : Vector α n} {i : Nat} (h : i < n - 1) : (xs.pop)[i] = xs[i] := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
 /--
 Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
 defeq issues in the implicit size argument.

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/Init/Prelude.lean

@@ -2150,14 +2150,14 @@ instance : Inhabited UInt64 where
 /-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/
 abbrev USize.size : Nat := (hPow 2 System.Platform.numBits)
 
-theorem USize.size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
+theorem usize_size_eq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) :=
   show Or (Eq (hPow 2 System.Platform.numBits) 4294967296) (Eq (hPow 2 System.Platform.numBits) 18446744073709551616) from
   match System.Platform.numBits, System.Platform.numBits_eq with
   | _, Or.inl rfl => Or.inl (of_decide_eq_true rfl)
   | _, Or.inr rfl => Or.inr (of_decide_eq_true rfl)
 
-theorem USize.size_pos : LT.lt 0 USize.size :=
-  match USize.size, USize.size_eq with
+theorem usize_size_pos : LT.lt 0 USize.size :=
+  match USize.size, usize_size_eq with
   | _, Or.inl rfl => of_decide_eq_true rfl
   | _, Or.inr rfl => of_decide_eq_true rfl
 
@@ -2207,7 +2207,7 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) :=
 instance : DecidableEq USize := USize.decEq
 
 instance : Inhabited USize where
-  default := USize.ofNatLT 0 USize.size_pos
+  default := USize.ofNatLT 0 usize_size_pos
 
 /--
 A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and

src/Lean/CoreM.lean

@@ -46,15 +46,14 @@ register_builtin_option Elab.async : Bool := {
 
 /--
 If the `diagnostics` option is not already set, gives a message explaining this option.
-Begins with a `\n\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
-The double newline gives better visual separation from the main error message
+Begins with a `\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
 -/
 def useDiagnosticMsg : MessageData :=
   MessageData.lazy fun ctx =>
     if diagnostics.get ctx.opts then
       pure ""
     else
-      pure s!"\n\nAdditional diagnostic information may be available using the `set_option {diagnostics.name} true` command."
+      pure s!"\nAdditional diagnostic information may be available using the `set_option {diagnostics.name} true` command."
 
 namespace Core
 

src/Lean/Data/PersistentHashSet.lean

@@ -53,11 +53,4 @@ variable {_ : BEq α} {_ : Hashable α}
 def toList (s : PersistentHashSet α) : List α :=
   s.set.toList.map (·.1)
 
-protected def forIn {_ : BEq α} {_ : Hashable α} [Monad m]
-    (s : PersistentHashSet α) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ := do
-  PersistentHashMap.forIn s.set init fun p s => f p.1 s
-
-instance {_ : BEq α} {_ : Hashable α} : ForIn m (PersistentHashSet α) α where
-  forIn := PersistentHashSet.forIn
-
 end PersistentHashSet

src/Lean/Elab/Quotation.lean

@@ -190,7 +190,7 @@ private partial def quoteSyntax : Syntax → TermElabM Term
                 | $[some $ids:ident],* => $(quote inner)
                 | $[_%$ids],*          => Array.empty)
             | _ =>
-              let arr ← ids[:ids.size - 1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
+              let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back!
               `(Array.map (fun $(← mkTuple ids) => $(inner[0]!)) $arr)
           let arr ← if k == `sepBy then
             `(mkSepArray $arr $(getSepStxFromSplice arg))

src/Lean/Elab/Tactic/Basic.lean

@@ -177,7 +177,7 @@ where
     throwExs (failures : Array EvalTacticFailure) : TacticM Unit := do
      if h : 0 < failures.size  then
        -- For macros we want to report the error from the first registered / last tried rule (#3770)
-       let fail := failures[failures.size - 1]
+       let fail := failures[failures.size-1]
        fail.state.restore (restoreInfo := true)
        throw fail.exception -- (*)
      else

src/Lean/Linter/List.lean

@@ -237,23 +237,20 @@ def listVariablesLinter : Linter
           if let .str _ n := n then
           let n := stripBinderName n
           if !allowedListNames.contains n then
-            -- 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
+            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, 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
-            -- Allow `xss` for `Array (Array α)` or `Array (Vector α)`
-            unless ((ty.getArg! 0).isAppOf `Array || (ty.getArg! 0).isAppOf `Vector) && n == "xss" do
+            unless (ty.getArg! 0).isAppOf `Array && 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}"

src/Lean/Message.lean

@@ -490,17 +490,6 @@ def indentD (msg : MessageData) : MessageData :=
 def indentExpr (e : Expr) : MessageData :=
   indentD e
 
-/-- Atom quotes -/
-def aquote (msg : MessageData) : MessageData :=
-  "「" ++ msg ++ "」"
-
-/-- Quote `e` using `「` and `」` if `e` is not a free variable, constant, or literal. -/
-def quoteIfNotAtom (e : Expr) : MessageData :=
-  if e.isFVar || e.isConst || e.isLit then
-    e
-  else
-    aquote e
-
 class AddMessageContext (m : Type → Type) where
   /--
   Without context, a `MessageData` object may be missing information

src/Lean/Meta/ArgsPacker.lean

@@ -560,7 +560,7 @@ where
   go : List Expr → Array Expr → MetaM α
   | [], acc => k acc
   | t::ts, acc => do
-    let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size + 1}"
+    let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size+1}"
     withLocalDeclD name t fun x => do
       go ts (acc.push x)