cleanup

doc/declarations.md

@@ -764,12 +764,11 @@ Structures and Records
 The ``structure`` command in Lean is used to define an inductive data type with a single constructor and to define its projections at the same time. The syntax is as follows:
 
 ```
-structure Foo (a : α) : Sort u extends Bar, Baz :=
+structure Foo (a : α) extends Bar, Baz : Sort u :=
 constructor :: (field₁ : β₁) ... (fieldₙ : βₙ)
 ```
 
-Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``Foo``, and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible (unless all the fields are ``Prop``, in which case it infers ``Prop``).
-Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
+Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``Foo``, and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible. Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
 
 The declaration above is syntactic sugar for an inductive type declaration, and so results in the addition of the following constants to the environment:
 

src/CMakeLists.txt

@@ -144,12 +144,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   # do not import the world from windows.h using appropriately named flag
   string(APPEND LEAN_EXTRA_CXX_FLAGS " -D WIN32_LEAN_AND_MEAN")
   # DLLs must go next to executables on Windows
-  set(CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY "bin")
+  set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
 else()
-  set(CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY "lib/lean")
+  set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
 endif()
 
-set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}")
 set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
 
 # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.

src/Init/Control/Basic.lean

@@ -78,7 +78,7 @@ Error recovery and state can interact subtly. For example, the implementation of
 -/
 -- NB: List instance is in mathlib. Once upstreamed, add
 -- * `List`, where `failure` is the empty list and `<|>` concatenates.
-class Alternative (f : Type u → Type v) : Type (max (u+1) v) extends Applicative f where
+class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) where
   /--
   Produces an empty collection or recoverable failure.  The `<|>` operator collects values or recovers
   from failures. See `Alternative` for more details.

src/Init/Control/Lawful/Basic.lean

@@ -47,7 +47,7 @@ pure f <*> pure x = pure (f x)
 u <*> pure y = pure (· y) <*> u
 ```
 -/
-class LawfulApplicative (f : Type u → Type v) [Applicative f] : Prop extends LawfulFunctor f where
+class LawfulApplicative (f : Type u → Type v) [Applicative f] extends LawfulFunctor f : Prop where
   seqLeft_eq  (x : f α) (y : f β)     : x <* y = const β <$> x <*> y
   seqRight_eq (x : f α) (y : f β)     : x *> y = const α id <$> x <*> y
   pure_seq    (g : α → β) (x : f α)   : pure g <*> x = g <$> x
@@ -77,7 +77,7 @@ x >>= f >>= g = x >>= (fun x => f x >>= g)
 
 `LawfulMonad.mk'` is an alternative constructor containing useful defaults for many fields.
 -/
-class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplicative m where
+class LawfulMonad (m : Type u → Type v) [Monad m] extends LawfulApplicative m : Prop where
   bind_pure_comp (f : α → β) (x : m α) : x >>= (fun a => pure (f a)) = f <$> x
   bind_map       {α β : Type u} (f : m (α → β)) (x : m α) : f >>= (. <$> x) = f <*> x
   pure_bind      (x : α) (f : α → m β) : pure x >>= f = f x

src/Init/Core.lean

@@ -2020,7 +2020,7 @@ free variables. The frontend automatically declares a fresh auxiliary constant `
 
 Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
 This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers that do not implement this feature.
+external type checkers (e.g., Trepplein) that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 
@@ -2055,7 +2055,7 @@ decidability instance can be evaluated to `true` using the lean compiler / inter
 
 Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
 This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers that do not implement this feature.
+external type checkers (e.g., Trepplein) that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
@@ -2066,7 +2066,7 @@ The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool
 
 Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
 This is extra 30k lines of code. More importantly, you will probably not be able to check your development using
-external type checkers that do not implement this feature.
+external type checkers (e.g., Trepplein) that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
@@ -2125,7 +2125,7 @@ class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 `LawfulLeftIdentify op o` indicates `o` is a verified left identity of
 `op`.
 -/
-class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extends LeftIdentity op o where
+class LawfulLeftIdentity (op : α → β → β) (o : outParam α) extends LeftIdentity op o : Prop where
   /-- Left identity `o` is an identity. -/
   left_id : ∀ a, op o a = a
 
@@ -2141,7 +2141,7 @@ class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 `LawfulRightIdentify op o` indicates `o` is a verified right identity of
 `op`.
 -/
-class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop extends RightIdentity op o where
+class LawfulRightIdentity (op : α → β → α) (o : outParam β) extends RightIdentity op o : Prop where
   /-- Right identity `o` is an identity. -/
   right_id : ∀ a, op a o = a
 
@@ -2151,13 +2151,13 @@ class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop exten
 This class does not require a proof that `o` is an identity, and is used
 primarily for inferring the identity using class resolution.
 -/
-class Identity (op : α → α → α) (o : outParam α) : Prop extends LeftIdentity op o, RightIdentity op o
+class Identity (op : α → α → α) (o : outParam α) extends LeftIdentity op o, RightIdentity op o : Prop
 
 /--
 `LawfulIdentity op o` indicates `o` is a verified left and right
 identity of `op`.
 -/
-class LawfulIdentity (op : α → α → α) (o : outParam α) : Prop extends Identity op o, LawfulLeftIdentity op o, LawfulRightIdentity op o
+class LawfulIdentity (op : α → α → α) (o : outParam α) extends Identity op o, LawfulLeftIdentity op o, LawfulRightIdentity op o : Prop
 
 /--
 `LawfulCommIdentity` can simplify defining instances of `LawfulIdentity`
@@ -2168,7 +2168,7 @@ This class is intended for simplifying defining instances of
 `LawfulIdentity` and functions needed commutative operations with
 identity should just add a `LawfulIdentity` constraint.
 -/
-class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commutative op] : Prop extends LawfulIdentity op o where
+class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commutative op] extends LawfulIdentity op o : Prop where
   left_id a := Eq.trans (hc.comm o a) (right_id a)
   right_id a := Eq.trans (hc.comm a o) (left_id a)
 

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

@@ -25,7 +25,7 @@ class ReflBEq (α) [BEq α] : Prop where
   refl : (a : α) == a
 
 /-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
-class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
+class EquivBEq (α) [BEq α] extends PartialEquivBEq α, ReflBEq α : Prop
 
 @[simp]
 theorem BEq.refl [BEq α] [ReflBEq α] {a : α} : a == a :=

src/Init/Data/BitVec/Bitblast.lean

@@ -907,7 +907,7 @@ The input to the shift subtractor is a legal input to `divrem`, and we also need
 input bit to perform shift subtraction on, and thus we need `0 < wn`.
 -/
 structure DivModState.Poised {w : Nat} (args : DivModArgs w) (qr : DivModState w)
-  extends DivModState.Lawful args qr where
+  extends DivModState.Lawful args qr : Type where
   /-- Only perform a round of shift-subtract if we have dividend bits. -/
   hwn_lt : 0 < qr.wn
 

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/DivMod/Basic.lean

@@ -112,10 +112,9 @@ instance : Mod Int where
 @[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
 theorem ofNat_ediv_ofNat {a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat) := rfl
-@[norm_cast]
 theorem negSucc_ediv_ofNat_succ {a b : Nat} : ((-[a+1]) / ↑(b+1) : Int) = -[a / succ b +1] := rfl
 theorem negSucc_ediv_negSucc {a b : Nat} : ((-[a+1]) / (-[b+1]) : Int) = ((a / (b + 1)) + 1 : Nat) := rfl
-theorem ofNat_ediv_negSucc {a b : Nat} : (ofNat a / (-[b+1])) = -(a / (b + 1) : Nat) := rfl
+
 theorem negSucc_emod_ofNat {a b : Nat} : -[a+1] % (b : Int) = subNatNat b (succ (a % b)) := rfl
 theorem negSucc_emod_negSucc {a b : Nat} : -[a+1] % -[b+1] = subNatNat (b + 1) (succ (a % (b + 1))) := rfl
 

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -300,12 +300,6 @@ protected theorem ediv_mul_cancel {a b : Int} (H : b ∣ a) : a / b * b = a :=
 protected theorem mul_ediv_cancel' {a b : Int} (H : a ∣ b) : a * (b / a) = b := by
   rw [Int.mul_comm, Int.ediv_mul_cancel H]
 
-theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a := by
-  rw [dvd_iff_emod_eq_zero] at h
-  by_cases w : a = 0
-  · simp_all
-  · exact Or.inr (Int.lt_iff_le_and_ne.mpr ⟨emod_nonneg b w, Ne.symm h⟩)
-
 /-! ### bmod -/
 
 @[simp] theorem bmod_emod : bmod x m % m = x % m := by

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -7,7 +7,6 @@ Authors: Jeremy Avigad, Mario Carneiro
 prelude
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Div.Lemmas
 import Init.Data.Int.Order
 import Init.Data.Int.Lemmas
 import Init.Data.Nat.Dvd
@@ -73,14 +72,6 @@ theorem dvd_natAbs_self {a : Int} : a ∣ (a.natAbs : Int) := by
 theorem ofNat_dvd_right {n : Nat} {z : Int} : z ∣ (↑n : Int) ↔ z.natAbs ∣ n := by
   rw [← natAbs_dvd_natAbs, natAbs_ofNat]
 
-@[simp] theorem negSucc_dvd {a : Nat} {b : Int} : -[a+1] ∣ b ↔ ((a + 1 : Nat) : Int) ∣ b := by
-  rw [← natAbs_dvd]
-  norm_cast
-
-@[simp] theorem dvd_negSucc {a : Int} {b : Nat} : a ∣ -[b+1] ↔ a ∣ ((b + 1 : Nat) : Int) := by
-  rw [← dvd_natAbs]
-  norm_cast
-
 theorem eq_one_of_dvd_one {a : Int} (H : 0 ≤ a) (H' : a ∣ 1) : a = 1 :=
   match a, eq_ofNat_of_zero_le H, H' with
   | _, ⟨_, rfl⟩, H' => congrArg ofNat <| Nat.eq_one_of_dvd_one <| ofNat_dvd.1 H'
@@ -91,9 +82,6 @@ theorem eq_one_of_mul_eq_one_right {a b : Int} (H : 0 ≤ a) (H' : a * b = 1) :
 theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b = 1 :=
   eq_one_of_mul_eq_one_right (b := a) H <| by rw [Int.mul_comm, H']
 
-instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun _ _ =>
-  decidable_of_decidable_of_iff (dvd_iff_emod_eq_zero ..).symm
-
 /-! ### *div zero  -/
 
 @[simp] protected theorem zero_tdiv : ∀ b : Int, tdiv 0 b = 0
@@ -113,126 +101,20 @@ unseal Nat.div in
   | succ _ => rfl
   | -[_+1] => rfl
 
-/-! ### preliminaries for div equivalences -/
-
-theorem negSucc_emod_ofNat_succ_eq_zero_iff {a b : Nat} :
-    -[a+1] % (b + 1 : Int) = 0 ↔ (a + 1) % (b + 1) = 0 := by
-  rw [← natCast_one, ← natCast_add]
-  change Int.emod _ _ = 0 ↔ _
-  rw [emod, natAbs_ofNat]
-  simp only [Nat.succ_eq_add_one, subNat_eq_zero_iff, Nat.add_right_cancel_iff]
-  rw [eq_comm]
-  apply Nat.succ_mod_succ_eq_zero_iff.symm
-
-theorem negSucc_emod_negSucc_eq_zero_iff {a b : Nat} :
-    -[a+1] % -[b+1] = 0 ↔ (a + 1) % (b + 1) = 0 := by
-  change Int.emod _ _ = 0 ↔ _
-  rw [emod, natAbs_negSucc]
-  simp only [Nat.succ_eq_add_one, subNat_eq_zero_iff, Nat.add_right_cancel_iff]
-  rw [eq_comm]
-  apply Nat.succ_mod_succ_eq_zero_iff.symm
-
 /-! ### div equivalences  -/
 
-theorem tdiv_eq_ediv_of_nonneg : ∀ {a b : Int}, 0 ≤ a → a.tdiv b = a / b
+theorem tdiv_eq_ediv : ∀ {a b : Int}, 0 ≤ a → a.tdiv b = a / b
   | 0, _, _
   | _, 0, _ => by simp
   | succ _, succ _, _ => rfl
   | succ _, -[_+1], _ => rfl
 
-theorem tdiv_eq_ediv {a b : Int} :
-    a.tdiv b = a / b + if 0 ≤ a ∨ b ∣ a then 0 else sign b := by
-  simp only [dvd_iff_emod_eq_zero]
-  match a, b with
-  | ofNat a, ofNat b => simp [tdiv_eq_ediv_of_nonneg]
-  | ofNat a, -[b+1] => simp [tdiv_eq_ediv_of_nonneg]
-  | -[a+1], 0 => simp
-  | -[a+1], ofNat (succ b) =>
-    simp only [tdiv, Nat.succ_eq_add_one, ofNat_eq_coe, natCast_add, Nat.cast_ofNat_Int,
-      negSucc_not_nonneg, sign_of_add_one]
-    simp only [negSucc_emod_ofNat_succ_eq_zero_iff]
-    norm_cast
-    simp only [subNat_eq_zero_iff, Nat.succ_eq_add_one, sign_negSucc, Int.sub_neg, false_or]
-    split <;> rename_i h
-    · rw [Int.add_zero, neg_ofNat_eq_negSucc_iff]
-      exact Nat.succ_div_of_mod_eq_zero h
-    · rw [neg_ofNat_eq_negSucc_add_one_iff]
-      exact Nat.succ_div_of_mod_ne_zero h
-  | -[a+1], -[b+1] =>
-    simp only [tdiv, ofNat_eq_coe, negSucc_not_nonneg, false_or, sign_negSucc]
-    norm_cast
-    simp only [negSucc_ediv_negSucc]
-    rw [natCast_add, natCast_one]
-    simp only [negSucc_emod_negSucc_eq_zero_iff]
-    split <;> rename_i h
-    · norm_cast
-      exact Nat.succ_div_of_mod_eq_zero h
-    · rw [← Int.sub_eq_add_neg, Int.add_sub_cancel]
-      norm_cast
-      exact Nat.succ_div_of_mod_ne_zero h
-
-theorem ediv_eq_tdiv {a b : Int} :
-    a / b = a.tdiv b - if 0 ≤ a ∨ b ∣ a then 0 else sign b := by
-  simp [tdiv_eq_ediv]
-
-theorem fdiv_eq_ediv_of_nonneg : ∀ (a : Int) {b : Int}, 0 ≤ b → fdiv a b = a / b
+theorem fdiv_eq_ediv : ∀ (a : Int) {b : Int}, 0 ≤ b → fdiv a b = a / b
   | 0, _, _ | -[_+1], 0, _ => by simp
   | succ _, ofNat _, _ | -[_+1], succ _, _ => rfl
 
-theorem fdiv_eq_ediv {a b : Int} :
-    a.fdiv b = a / b - if 0 ≤ b ∨ b ∣ a then 0 else 1 := by
-  match a, b with
-  | ofNat a, ofNat b => simp [fdiv_eq_ediv_of_nonneg]
-  | -[a+1], ofNat b => simp [fdiv_eq_ediv_of_nonneg]
-  | 0, -[b+1] => simp
-  | ofNat (a + 1), -[b+1] =>
-    simp only [fdiv, ofNat_ediv_negSucc, negSucc_not_nonneg, negSucc_dvd, false_or]
-    simp only [ofNat_eq_coe, ofNat_dvd]
-    norm_cast
-    rw [Nat.succ_div, negSucc_eq]
-    split <;> rename_i h
-    · simp
-    · simp [Int.neg_add]
-      norm_cast
-  | -[a+1], -[b+1] =>
-    simp only [fdiv, ofNat_eq_coe, negSucc_ediv_negSucc, negSucc_not_nonneg, dvd_negSucc, negSucc_dvd,
-      false_or]
-    norm_cast
-    rw [natCast_add, natCast_one, Nat.succ_div]
-    split <;> simp
-
-theorem ediv_eq_fdiv {a b : Int} :
-    a / b = a.fdiv b + if 0 ≤ b ∨ b ∣ a then 0 else 1 := by
-  simp [fdiv_eq_ediv]
-
-theorem fdiv_eq_tdiv_of_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = tdiv a b :=
-  tdiv_eq_ediv_of_nonneg Ha ▸ fdiv_eq_ediv_of_nonneg _ Hb
-
-theorem fdiv_eq_tdiv {a b : Int} :
-    a.fdiv b = a.tdiv b -
-      if b ∣ a then 0
-      else
-        if 0 ≤ a then
-          if 0 ≤ b then 0
-          else 1
-        else
-          if 0 ≤ b then b.sign
-          else 1 + b.sign := by
-  rw [fdiv_eq_ediv, tdiv_eq_ediv]
-  by_cases h : b ∣ a <;> simp [h] <;> omega
-
-theorem tdiv_eq_fdiv {a b : Int} :
-    a.tdiv b = a.fdiv b +
-      if b ∣ a then 0
-      else
-        if 0 ≤ a then
-          if 0 ≤ b then 0
-          else 1
-        else
-          if 0 ≤ b then b.sign
-          else 1 + b.sign := by
-  rw [fdiv_eq_tdiv]
-  omega
+theorem fdiv_eq_tdiv {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = tdiv a b :=
+  tdiv_eq_ediv Ha ▸ fdiv_eq_ediv _ Hb
 
 /-! ### mod zero -/
 
@@ -308,63 +190,14 @@ theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
 
 /-! ### mod equivalences  -/
 
-theorem fmod_eq_emod_of_nonneg (a : Int) {b : Int} (hb : 0 ≤ b) : fmod a b = a % b := by
-  simp [fmod_def, emod_def, fdiv_eq_ediv_of_nonneg _ hb]
+theorem fmod_eq_emod (a : Int) {b : Int} (hb : 0 ≤ b) : fmod a b = a % b := by
+  simp [fmod_def, emod_def, fdiv_eq_ediv _ hb]
 
-theorem fmod_eq_emod {a b : Int} :
-    fmod a b = a % b + if 0 ≤ b ∨ b ∣ a then 0 else b := by
-  simp [fmod_def, emod_def, fdiv_eq_ediv]
-  split <;> simp [Int.mul_sub]
-  omega
+theorem tmod_eq_emod {a b : Int} (ha : 0 ≤ a) : tmod a b = a % b := by
+  simp [emod_def, tmod_def, tdiv_eq_ediv ha]
 
-theorem emod_eq_fmod {a b : Int} :
-    a % b = fmod a b - if 0 ≤ b ∨ b ∣ a then 0 else b := by
-  simp [fmod_eq_emod]
-
-theorem tmod_eq_emod_of_nonneg {a b : Int} (ha : 0 ≤ a) : tmod a b = a % b := by
-  simp [emod_def, tmod_def, tdiv_eq_ediv_of_nonneg ha]
-
-theorem tmod_eq_emod {a b : Int} :
-    tmod a b = a % b - if 0 ≤ a ∨ b ∣ a then 0 else b.natAbs := by
-  rw [tmod_def, tdiv_eq_ediv]
-  simp only [dvd_iff_emod_eq_zero]
-  split
-  · simp [emod_def]
-  · rw [Int.mul_add, ← Int.sub_sub, emod_def]
-    simp
-
-theorem emod_eq_tmod {a b : Int} :
-    a % b = tmod a b + if 0 ≤ a ∨ b ∣ a then 0 else b.natAbs := by
-  simp [tmod_eq_emod]
-
-theorem fmod_eq_tmod_of_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : fmod a b = tmod a b :=
-  tmod_eq_emod_of_nonneg ha ▸ fmod_eq_emod_of_nonneg _ hb
-
-theorem fmod_eq_tmod {a b : Int} :
-    fmod a b = tmod a b +
-      if b ∣ a then 0
-      else
-        if 0 ≤ a then
-          if 0 ≤ b then 0
-          else b
-        else
-          if 0 ≤ b then b.natAbs
-          else 2 * b.toNat := by
-  simp [fmod_eq_emod, tmod_eq_emod]
-  by_cases h : b ∣ a <;> simp [h]
-  split <;> split <;> omega
-
-theorem tmod_eq_fmod {a b : Int} :
-    tmod a b = fmod a b -
-      if b ∣ a then 0
-      else
-        if 0 ≤ a then
-          if 0 ≤ b then 0
-          else b
-        else
-          if 0 ≤ b then b.natAbs
-          else 2 * b.toNat := by
-  simp [fmod_eq_tmod]
+theorem fmod_eq_tmod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = tmod a b :=
+  tmod_eq_emod Ha ▸ fmod_eq_emod _ Hb
 
 /-! ### `/` ediv -/
 
@@ -496,6 +329,23 @@ theorem emod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a :=
 @[simp] theorem emod_self_add_one {x : Int} (h : 0 ≤ x) : x % (x + 1) = x :=
   emod_eq_of_lt h (Int.lt_succ x)
 
+theorem negSucc_emod_ofNat_succ_eq_zero_iff {a b : Nat} :
+    -[a+1] % (b + 1 : Int) = 0 ↔ (a + 1) % (b + 1) = 0 := by
+  rw [← natCast_one, ← natCast_add]
+  change Int.emod _ _ = 0 ↔ _
+  rw [emod, natAbs_ofNat]
+  simp only [Nat.succ_eq_add_one, subNat_eq_zero_iff, Nat.add_right_cancel_iff]
+  rw [eq_comm]
+  apply Nat.succ_mod_succ_eq_zero_iff.symm
+
+theorem negSucc_emod_negSucc_eq_zero_iff {a b : Nat} :
+    -[a+1] % -[b+1] = 0 ↔ (a + 1) % (b + 1) = 0 := by
+  change Int.emod _ _ = 0 ↔ _
+  rw [emod, natAbs_negSucc]
+  simp only [Nat.succ_eq_add_one, subNat_eq_zero_iff, Nat.add_right_cancel_iff]
+  rw [eq_comm]
+  apply Nat.succ_mod_succ_eq_zero_iff.symm
+
 /-! ### properties of `/` and `%` -/
 
 theorem emod_two_eq (x : Int) : x % 2 = 0 ∨ x % 2 = 1 := by
@@ -563,6 +413,15 @@ theorem dvd_emod_sub_self {x : Int} {m : Nat} : (m : Int) ∣ x % m - x := by
   rw [← dvd_iff_emod_eq_zero, Int.dvd_neg]
   exact Int.dvd_mul_right a b
 
+instance decidableDvd : DecidableRel (α := Int) (· ∣ ·) := fun _ _ =>
+  decidable_of_decidable_of_iff (dvd_iff_emod_eq_zero ..).symm
+
+theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a := by
+  rw [dvd_iff_emod_eq_zero] at h
+  by_cases w : a = 0
+  · simp_all
+  · exact Or.inr (Int.lt_iff_le_and_ne.mpr ⟨emod_nonneg b w, Ne.symm h⟩)
+
 @[simp] theorem neg_mul_ediv_cancel (a b : Int) (h : b ≠ 0) : -(a * b) / b = -a := by
   rw [neg_ediv_of_dvd (Int.dvd_mul_left a b), mul_ediv_cancel _ h]
 
@@ -811,7 +670,7 @@ theorem ofNat_tmod (m n : Nat) : (↑(m % n) : Int) = tmod m n := rfl
   simp [tmod_def, Int.tdiv_one, Int.one_mul, Int.sub_self]
 
 theorem tmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : tmod a b = a := by
-  rw [tmod_eq_emod_of_nonneg H1, emod_eq_of_lt H1 H2]
+  rw [tmod_eq_emod H1, emod_eq_of_lt H1 H2]
 
 theorem tmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : tmod a b < b :=
   match a, b, eq_succ_of_zero_lt H with
@@ -920,7 +779,7 @@ theorem fdiv_neg' : ∀ {a b : Int}, a < 0 → 0 < b → a.fdiv b < 0
 
 @[simp] theorem mul_fdiv_cancel (a : Int) {b : Int} (H : b ≠ 0) : fdiv (a * b) b = a :=
   if b0 : 0 ≤ b then by
-    rw [fdiv_eq_ediv_of_nonneg _ b0, mul_ediv_cancel _ H]
+    rw [fdiv_eq_ediv _ b0, mul_ediv_cancel _ H]
   else
     match a, b, Int.not_le.1 b0 with
     | 0, _, _ => by simp [Int.zero_mul]
@@ -936,7 +795,7 @@ theorem fdiv_neg' : ∀ {a b : Int}, a < 0 → 0 < b → a.fdiv b < 0
   have := Int.mul_fdiv_cancel 1 H; rwa [Int.one_mul] at this
 
 theorem lt_fdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.fdiv b + 1) * b :=
-  Int.fdiv_eq_ediv_of_nonneg _ (Int.le_of_lt H) ▸ lt_ediv_add_one_mul_self a H
+  Int.fdiv_eq_ediv _ (Int.le_of_lt H) ▸ lt_ediv_add_one_mul_self a H
 
 /-! ### fmod -/
 
@@ -947,16 +806,16 @@ theorem ofNat_fmod (m n : Nat) : ↑(m % n) = fmod m n := by
   simp [fmod_def, Int.one_mul, Int.sub_self]
 
 theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a := by
-  rw [fmod_eq_emod_of_nonneg _ (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
+  rw [fmod_eq_emod _ (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
 
 theorem fmod_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a.fmod b :=
-  fmod_eq_tmod_of_nonneg ha hb ▸ tmod_nonneg _ ha
+  fmod_eq_tmod ha hb ▸ tmod_nonneg _ ha
 
 theorem fmod_nonneg' (a : Int) {b : Int} (hb : 0 < b) : 0 ≤ a.fmod b :=
-  fmod_eq_emod_of_nonneg _ (Int.le_of_lt hb) ▸ emod_nonneg _ (Int.ne_of_lt hb).symm
+  fmod_eq_emod _ (Int.le_of_lt hb) ▸ emod_nonneg _ (Int.ne_of_lt hb).symm
 
 theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
-  fmod_eq_emod_of_nonneg _ (Int.le_of_lt H) ▸ emod_lt_of_pos a H
+  fmod_eq_emod _ (Int.le_of_lt H) ▸ emod_lt_of_pos a H
 
 @[simp] theorem mul_fmod_left (a b : Int) : (a * b).fmod b = 0 :=
   if h : b = 0 then by simp [h, Int.mul_zero] else by

src/Init/Data/Int/Lemmas.lean

@@ -341,20 +341,6 @@ theorem toNat_of_nonpos : ∀ {z : Int}, z ≤ 0 → z.toNat = 0
   | 0, _ => rfl
   | -[_+1], _ => rfl
 
-@[simp] theorem neg_ofNat_eq_negSucc_iff {a b : Nat} : - (a : Int) = -[b+1] ↔ a = b + 1 := by
-  rw [Int.neg_eq_comm]
-  rw [Int.neg_negSucc]
-  norm_cast
-  simp [eq_comm]
-
-@[simp] theorem neg_ofNat_eq_negSucc_add_one_iff {a b : Nat} : - (a : Int) = -[b+1] + 1 ↔ a = b := by
-  cases b with
-  | zero => simp; norm_cast
-  | succ b =>
-    rw [Int.neg_eq_comm, ← Int.negSucc_sub_one, Int.sub_add_cancel, Int.neg_negSucc]
-    norm_cast
-    simp [eq_comm]
-
 /- ## add/sub injectivity -/
 
 protected theorem add_left_inj {i j : Int} (k : Int) : (i + k = j + k) ↔ i = j := by

src/Init/Data/Int/Linear.lean

@@ -147,9 +147,28 @@ where
     | .neg a    => go (-coeff) a
 
 /-- Converts the given expression into a polynomial, and then normalizes it. -/
-def Expr.norm (e : Expr) : Poly :=
+def Expr.toPoly (e : Expr) : Poly :=
   e.toPoly'.norm
 
+/-- Relational contraints: equality and inequality. -/
+inductive RelCnstr  where
+  | /-- `p = 0` constraint. -/
+    eq (p : Poly)
+  | /-- `p ≤ 0` contraint. -/
+    le (p : Poly)
+  deriving BEq
+
+def RelCnstr.denote (ctx : Context) : RelCnstr → Prop
+  | .eq p => p.denote ctx = 0
+  | .le p => p.denote ctx ≤ 0
+
+def RelCnstr.denote' (ctx : Context) : RelCnstr → Prop
+  | .eq p => p.denote' ctx = 0
+  | .le p => p.denote' ctx ≤ 0
+
+theorem RelCnstr.denote'_eq_denote (ctx : Context) (c : RelCnstr) : c.denote' ctx = c.denote ctx := by
+  cases c <;> simp [denote, denote', Poly.denote'_eq_denote]
+
 /--
 Returns the ceiling of the division `a / b`. That is, the result is equivalent to `⌈a / b⌉`.
 Examples:
@@ -259,6 +278,83 @@ def Poly.mul (p : Poly) (k : Int) : Poly :=
   induction p <;> simp [mul, denote, *]
   rw [Int.mul_assoc, Int.mul_add]
 
+/-- Normalizes the polynomial of the given relational constraint. -/
+def RelCnstr.norm : RelCnstr → RelCnstr
+  | .eq p => .eq p.norm
+  | .le p => .le p.norm
+
+/-- Returns `true` if `k` divides all coefficients and constant of the given relational constraint. -/
+def RelCnstr.divAll (k : Int) : RelCnstr → Bool
+  | .eq p | .le p => p.divAll k
+
+/-- Returns `true` if `k` divides all coefficients of the given relational constraint. -/
+def RelCnstr.divCoeffs (k : Int) : RelCnstr → Bool
+  | .eq p | .le p => p.divCoeffs k
+
+/-- Returns `true` if the given relational constraint is an inequality constraint of the form `p ≤ 0`. -/
+def RelCnstr.isLe : RelCnstr → Bool
+  | .eq _ => false
+  | .le _ => true
+
+/--
+Divides all coefficients and constants in the linear polynomial of the given constraint by `k`.
+We rounds up the constant using `cdiv`.
+-/
+def RelCnstr.div (k : Int) : RelCnstr → RelCnstr
+  | .eq p => .eq <| p.div k
+  | .le p => .le <| p.div k
+
+/--
+Multiplies all coefficients and constants in the linear polynomial of the given constraint by `k`.
+-/
+def RelCnstr.mul (k : Int) : RelCnstr → RelCnstr
+  | .eq p => .eq <| p.mul k
+  | .le p => .le <| p.mul k
+
+def RelCnstr.addConst (k : Int) : RelCnstr → RelCnstr
+  | .eq p => .eq <| p.addConst k
+  | .le p => .le <| p.addConst k
+
+@[simp] theorem RelCnstr.denote_mul (ctx : Context) (c : RelCnstr) (k : Int) (h : k > 0) : (c.mul k).denote ctx = c.denote ctx := by
+  cases c <;> simp [mul, denote]
+  next =>
+    constructor
+    · intro h₁; cases (Int.mul_eq_zero.mp h₁)
+      next hz => simp [hz] at h
+      next => assumption
+    · intro h'; simp [*]
+  next =>
+    constructor
+    · intro h₁
+      conv at h₁ => rhs; rw [← Int.mul_zero k]
+      exact Int.le_of_mul_le_mul_left h₁ h
+    · intro h₂
+      have := Int.mul_le_mul_of_nonneg_left h₂ (Int.le_of_lt h)
+      simp at this; assumption
+
+/-- Raw relational constraint. They are later converted into `RelCnstr`. -/
+inductive RawRelCnstr  where
+  | eq (p₁ p₂ : Expr)
+  | le (p₁ p₂ : Expr)
+  deriving Inhabited, BEq
+
+/-- Returns `true` if the given relational constraint is an inequality constraint of the form `e₁ ≤ e₂`. -/
+def RawRelCnstr.isLe : RawRelCnstr → Bool
+  | .eq .. => false
+  | .le .. => true
+
+def RawRelCnstr.denote (ctx : Context) : RawRelCnstr → Prop
+  | .eq e₁ e₂ => e₁.denote ctx = e₂.denote ctx
+  | .le e₁ e₂ => e₁.denote ctx ≤ e₂.denote ctx
+
+def RawRelCnstr.norm : RawRelCnstr → RelCnstr
+  | .eq e₁ e₂ => .eq (e₁.sub e₂).toPoly.norm
+  | .le e₁ e₂ => .le (e₁.sub e₂).toPoly.norm
+
+/-- A certificate for normalizing the coefficients of a raw relational constraint. -/
+def divBy (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : Bool :=
+  k > 0 && c.norm == c'.mul k
+
 attribute [local simp] Int.add_comm Int.add_assoc Int.add_left_comm Int.add_mul Int.mul_add
 attribute [local simp] Poly.insert Poly.denote Poly.norm Poly.addConst
 
@@ -293,14 +389,12 @@ theorem Poly.denote_combine' (ctx : Context) (fuel : Nat) (p₁ p₂ : Poly) : (
 theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
   simp [combine, denote_combine']
 
-attribute [local simp] Poly.denote_combine
-
 theorem sub_fold (a b : Int) : a.sub b = a - b := rfl
 theorem neg_fold (a : Int) : a.neg = -a := rfl
 
 attribute [local simp] sub_fold neg_fold
 
-attribute [local simp] Poly.div Poly.divAll
+attribute [local simp] Poly.div Poly.divAll RelCnstr.denote
 
 theorem Poly.denote_div_eq_of_divAll (ctx : Context) (p : Poly) (k : Int) : p.divAll k → (p.div k).denote ctx * k = p.denote ctx := by
   induction p with
@@ -324,7 +418,7 @@ theorem Poly.denote_div_eq_of_divCoeffs (ctx : Context) (p : Poly) (k : Int) : p
     rw [← ih h₂]
     rw [Int.mul_right_comm, h₁, Int.add_assoc]
 
-attribute [local simp] Expr.denote
+attribute [local simp] RawRelCnstr.denote RawRelCnstr.norm Expr.denote
 
 theorem Expr.denote_toPoly'_go (ctx : Context) (e : Expr) :
   (toPoly'.go k e p).denote ctx = k * e.denote ctx + p.denote ctx := by
@@ -354,10 +448,20 @@ theorem Expr.denote_toPoly'_go (ctx : Context) (e : Expr) :
     simpa [Int.mul_assoc] using ih
   | case10 k a ih => simp [toPoly'.go, ih]
 
-theorem Expr.denote_norm (ctx : Context) (e : Expr) : e.norm.denote ctx = e.denote ctx := by
-  simp [norm, toPoly', Expr.denote_toPoly'_go]
+theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.denote ctx := by
+  simp [toPoly, toPoly', Expr.denote_toPoly'_go]
 
-attribute [local simp] Expr.denote_norm
+attribute [local simp] Expr.denote_toPoly RelCnstr.denote
+
+theorem RelCnstr.denote_norm (ctx : Context) (c : RelCnstr) : c.norm.denote ctx = c.denote ctx := by
+  cases c <;> simp [RelCnstr.norm]
+
+theorem RawRelCnstr.denote_norm (ctx : Context) (c : RawRelCnstr) : c.norm.denote ctx = c.denote ctx := by
+  cases c <;> simp
+  · rw [Int.sub_eq_zero]
+  · constructor
+    · exact Int.le_of_sub_nonpos
+    · exact Int.sub_nonpos_of_le
 
 instance : LawfulBEq Poly where
   eq_of_beq {a} := by
@@ -370,83 +474,54 @@ instance : LawfulBEq Poly where
     induction a <;> simp! [BEq.beq]
     assumption
 
-attribute [local simp] Poly.denote'_eq_denote
+instance : LawfulBEq RelCnstr where
+  eq_of_beq {a b} := by
+    cases a <;> cases b <;> rename_i p₁ p₂ <;> simp_all! [BEq.beq]
+    · show (p₁ == p₂) = true → _
+      simp
+    · show (p₁ == p₂) = true → _
+      simp
+  rfl {a} := by
+    cases a <;> rename_i p <;> show (p == p) = true
+      <;> simp
 
-theorem Expr.eq_of_norm_eq (ctx : Context) (e : Expr) (p : Poly) (h : e.norm == p) : e.denote ctx = p.denote' ctx := by
+theorem Expr.eq_of_toPoly_eq (ctx : Context) (e e' : Expr) (h : e.toPoly == e'.toPoly) : e.denote ctx = e'.denote ctx := by
   have h := congrArg (Poly.denote ctx) (eq_of_beq h)
   simp [Poly.norm] at h
-  simp [*]
+  assumption
 
-def norm_eq_cert (lhs rhs : Expr) (p : Poly) : Bool :=
-  p == (lhs.sub rhs).norm
+theorem RawRelCnstr.eq_of_norm_eq (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (h : c.norm == c') : c.denote ctx = c'.denote' ctx := by
+  have h := congrArg (RelCnstr.denote ctx) (eq_of_beq h)
+  rw [denote_norm] at h
+  rw [RelCnstr.denote'_eq_denote, h]
 
-theorem norm_eq (ctx : Context) (lhs rhs : Expr) (p : Poly) (h : norm_eq_cert lhs rhs p) : (lhs.denote ctx = rhs.denote ctx) = (p.denote' ctx = 0) := by
-  simp [norm_eq_cert] at h; subst p
-  simp
-  rw [Int.sub_eq_zero]
+theorem RawRelCnstr.eq_of_norm_eq_var (ctx : Context) (x y : Var) (c : RawRelCnstr) (h : c.norm == .eq (.add 1 x (.add (-1) y (.num 0))))
+    : c.denote ctx = (x.denote ctx = y.denote ctx) := by
+  have h := congrArg (RelCnstr.denote ctx) (eq_of_beq h)
+  rw [denote_norm] at h
+  rw [h]; simp
+  rw [← Int.sub_eq_add_neg, Int.sub_eq_zero]
 
-theorem norm_le (ctx : Context) (lhs rhs : Expr) (p : Poly) (h : norm_eq_cert lhs rhs p) : (lhs.denote ctx ≤ rhs.denote ctx) = (p.denote' ctx ≤ 0) := by
-  simp [norm_eq_cert] at h; subst p
-  simp
-  constructor
-  · exact Int.sub_nonpos_of_le
-  · exact Int.le_of_sub_nonpos
+theorem RawRelCnstr.eq_of_norm_eq_const (ctx : Context) (x : Var) (k : Int) (c : RawRelCnstr) (h : c.norm == .eq (.add 1 x (.num (-k))))
+    : c.denote ctx = (x.denote ctx = k) := by
+  have h := congrArg (RelCnstr.denote ctx) (eq_of_beq h)
+  rw [denote_norm] at h
+  rw [h]; simp
+  rw [Int.add_comm, ← Int.sub_eq_add_neg, Int.sub_eq_zero]
 
-def norm_eq_var_cert (lhs rhs : Expr) (x y : Var) : Bool :=
-  (lhs.sub rhs).norm == .add 1 x (.add (-1) y (.num 0))
+attribute [local simp] RelCnstr.divAll
 
-theorem norm_eq_var (ctx : Context) (lhs rhs : Expr) (x y : Var) (h : norm_eq_var_cert lhs rhs x y)
-    : (lhs.denote ctx = rhs.denote ctx) = (x.denote ctx = y.denote ctx) := by
-  simp [norm_eq_var_cert] at h
-  replace h := congrArg (Poly.denote ctx) h
-  simp at h
-  rw [←Int.sub_eq_zero, h, ← @Int.sub_eq_zero (Var.denote ctx x), Int.sub_eq_add_neg]
+theorem RawRelCnstr.eq_of_norm_eq_mul (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) (hz : k > 0) (h : c.norm = c'.mul k) : c.denote ctx = c'.denote ctx := by
+  replace h := congrArg (RelCnstr.denote ctx) h
+  simp only [RawRelCnstr.denote_norm, RelCnstr.denote_mul, *] at h
+  assumption
 
-def norm_eq_var_const_cert (lhs rhs : Expr) (x : Var) (k : Int) : Bool :=
-  (lhs.sub rhs).norm == .add 1 x (.num (-k))
-
-theorem norm_eq_var_const (ctx : Context) (lhs rhs : Expr) (x : Var) (k : Int) (h : norm_eq_var_const_cert lhs rhs x k)
-    : (lhs.denote ctx = rhs.denote ctx) = (x.denote ctx = k) := by
-  simp [norm_eq_var_const_cert] at h
-  replace h := congrArg (Poly.denote ctx) h
-  simp at h
-  rw [←Int.sub_eq_zero, h, Int.add_comm, ← Int.sub_eq_add_neg, Int.sub_eq_zero]
-
-private theorem mul_eq_zero_iff (a k : Int) (h₁ : k > 0) : k * a = 0 ↔ a = 0 := by
-  conv => lhs; rw [← Int.mul_zero k]
-  apply Int.mul_eq_mul_left_iff
-  exact Int.ne_of_gt h₁
-
-theorem norm_eq_coeff' (ctx : Context) (p p' : Poly) (k : Int) : p = p'.mul k → k > 0 → (p.denote ctx = 0 ↔ p'.denote ctx = 0) := by
-  intro; subst p; intro h; simp [mul_eq_zero_iff, *]
-
-def norm_eq_coeff_cert (lhs rhs : Expr) (p : Poly) (k : Int) : Bool :=
-  (lhs.sub rhs).norm == p.mul k && k > 0
-
-theorem norm_eq_coeff (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int)
-    : norm_eq_coeff_cert lhs rhs p k → (lhs.denote ctx = rhs.denote ctx) = (p.denote' ctx = 0) := by
-  simp [norm_eq_coeff_cert]
-  rw [norm_eq ctx lhs rhs (lhs.sub rhs).norm BEq.refl, Poly.denote'_eq_denote]
-  apply norm_eq_coeff'
-
-private theorem mul_le_zero_iff (a k : Int) (h₁ : k > 0) : k * a ≤ 0 ↔ a ≤ 0 := by
-  constructor
-  · intro h
-    rw [← Int.mul_zero k] at h
-    exact Int.le_of_mul_le_mul_left h h₁
-  · intro h
-    replace h := Int.mul_le_mul_of_nonneg_left h (Int.le_of_lt h₁)
-    simp at h; assumption
-
-private theorem norm_le_coeff' (ctx : Context) (p p' : Poly) (k : Int) : p = p'.mul k → k > 0 → (p.denote ctx ≤ 0 ↔ p'.denote ctx ≤ 0) := by
-  simp [norm_eq_coeff_cert]
-  intro; subst p; intro h; simp [mul_le_zero_iff, *]
-
-theorem norm_le_coeff (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int)
-    : norm_eq_coeff_cert lhs rhs p k → (lhs.denote ctx ≤ rhs.denote ctx) = (p.denote' ctx ≤ 0) := by
-  simp [norm_eq_coeff_cert]
-  rw [norm_le ctx lhs rhs (lhs.sub rhs).norm BEq.refl, Poly.denote'_eq_denote]
-  apply norm_le_coeff'
+theorem RawRelCnstr.eq_of_divBy (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : divBy c c' k → c.denote ctx = c'.denote' ctx := by
+  intro h
+  simp only [RelCnstr.denote'_eq_denote]
+  simp only [divBy, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq, decide_eq_true_eq] at h
+  have ⟨h₁, h₂⟩ := h
+  exact eq_of_norm_eq_mul ctx c c' k h₁ h₂
 
 private theorem mul_add_cmod_le_iff {a k b : Int} (h : k > 0) : a*k + cmod b k ≤ 0 ↔ a ≤ 0 := by
   constructor
@@ -472,93 +547,62 @@ private theorem mul_add_cmod_le_iff {a k b : Int} (h : k > 0) : a*k + cmod b k
     simp at this
     assumption
 
-private theorem eq_of_norm_eq_of_divCoeffs {ctx : Context} {p₁ p₂ : Poly} {k : Int}
-    : k > 0 → p₁.divCoeffs k → p₂ = p₁.div k → (p₁.denote ctx ≤ 0 ↔ p₂.denote ctx ≤ 0) := by
-  intro h₀ h₁ h₂
+theorem RelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c₁ c₂ : RelCnstr) (k : Int)
+    : k > 0 → c₁.divCoeffs k → c₁.isLe → c₂ = c₁.div k → c₁.denote ctx = c₂.denote ctx := by
+  intro h₀ h₁ h₂ h₃
   have hz : k ≠ 0 := Int.ne_of_gt h₀
-  replace h₁ := Poly.denote_div_eq_of_divCoeffs ctx p₁ k h₁
-  replace h₂ := congrArg (Poly.denote ctx) h₂
-  simp at h₂
-  rw [h₂, ← h₁]; clear h₁ h₂
-  apply mul_add_cmod_le_iff
+  cases c₁ <;> simp [RelCnstr.isLe] at h₂
+  clear h₂
+  next p =>
+    simp [RelCnstr.divCoeffs] at h₁
+    replace h₁ := Poly.denote_div_eq_of_divCoeffs ctx p k h₁
+    replace h₃ := congrArg (RelCnstr.denote ctx) h₃
+    simp only [RelCnstr.div, RelCnstr.denote.eq_2] at h₃
+    rw [h₃, denote, ← h₁]; clear h₁ h₃
+    apply propext
+    apply mul_add_cmod_le_iff
+    assumption
+
+theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c₁ : RawRelCnstr) (c₂ : RelCnstr) (c₃ : RelCnstr) (k : Int)
+    : k > 0 → c₂.divCoeffs k → c₂.isLe → c₁.norm = c₂ → c₃ = c₂.div k → c₁.denote ctx = c₃.denote ctx := by
+  intro h₀ h₁ h₂ h₃ h₄
+  replace h₃ := congrArg (RelCnstr.denote ctx) h₃
+  rw [denote_norm] at h₃
+  rw [h₃]
+  apply RelCnstr.eq_of_norm_eq_of_divCoeffs _ _ _ _ h₀ h₁ h₂ h₄
+
+/-- Certificate for normalizing the coefficients of inequality constraint with bound tightening. -/
+def divByLe (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : Bool :=
+  k > 0 && c.isLe && c.norm.divCoeffs k && c' == c.norm.div k
+
+theorem RawRelCnstr.eq_of_divByLe (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : divByLe c c' k → c.denote ctx = c'.denote' ctx := by
+  intro h
+  simp only [RelCnstr.denote'_eq_denote]
+  simp only [divByLe, Bool.and_eq_true, bne_iff_ne, ne_eq, beq_iff_eq, decide_eq_true_eq] at h
+  have ⟨⟨⟨h₀, h₁⟩, h₂⟩, h₃⟩ := h
+  have hle : c.norm.isLe := by
+    cases c <;> simp [RawRelCnstr.isLe] at h₁
+    simp [RelCnstr.isLe]
+  apply eq_of_norm_eq_of_divCoeffs ctx c c.norm c' k h₀ h₂ hle rfl h₃
+
+def RelCnstr.isUnsat : RelCnstr → Bool
+  | .eq (.num k) => k != 0
+  | .eq _ => false
+  | .le (.num k) => k > 0
+  | .le _ => false
+
+theorem RelCnstr.eq_false_of_isUnsat (ctx : Context) (c : RelCnstr) : c.isUnsat → c.denote ctx = False := by
+  unfold isUnsat <;> split <;> simp <;> try contradiction
+  apply Int.not_le_of_gt
+
+theorem RawRelCnstr.eq_false_of_isUnsat (ctx : Context) (c : RawRelCnstr) (h : c.norm.isUnsat) : c.denote ctx = False := by
+  have := RelCnstr.eq_false_of_isUnsat ctx c.norm h
+  rw [RawRelCnstr.denote_norm] at this
   assumption
 
-def norm_le_coeff_tight_cert (lhs rhs : Expr) (p : Poly) (k : Int) : Bool :=
-  let p' := lhs.sub rhs |>.norm
-  k > 0 && (p'.divCoeffs k && p == p'.div k)
-
-theorem norm_le_coeff_tight (ctx : Context) (lhs rhs : Expr) (p : Poly) (k : Int)
-    : norm_le_coeff_tight_cert lhs rhs p k → (lhs.denote ctx ≤ rhs.denote ctx) = (p.denote' ctx ≤ 0) := by
-  simp [norm_le_coeff_tight_cert]
-  rw [norm_le ctx lhs rhs (lhs.sub rhs).norm BEq.refl, Poly.denote'_eq_denote]
-  apply eq_of_norm_eq_of_divCoeffs
-
-def Poly.isUnsatEq (p : Poly) : Bool :=
-  match p with
-  | .num k => k != 0
-  | _ => false
-
-def Poly.isValidEq (p : Poly) : Bool :=
-  match p with
-  | .num k => k == 0
-  | _ => false
-
-theorem eq_eq_false (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isUnsatEq → (lhs.denote ctx = rhs.denote ctx) = False := by
-  simp [Poly.isUnsatEq] <;> split <;> simp
-  next p k h =>
-    intro h'
-    replace h := congrArg (Poly.denote ctx) h
-    simp at h
-    rw [← Int.sub_eq_zero, h]
-    assumption
-
-theorem eq_eq_true (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isValidEq → (lhs.denote ctx = rhs.denote ctx) = True := by
-  simp [Poly.isValidEq] <;> split <;> simp
-  next p k h =>
-    intro h'
-    replace h := congrArg (Poly.denote ctx) h
-    simp at h
-    rw [← Int.sub_eq_zero, h]
-    assumption
-
-def Poly.isUnsatLe (p : Poly) : Bool :=
-  match p with
-  | .num k => k > 0
-  | _ => false
-
-def Poly.isValidLe (p : Poly) : Bool :=
-  match p with
-  | .num k => k ≤ 0
-  | _ => false
-
-theorem le_eq_false (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isUnsatLe → (lhs.denote ctx ≤ rhs.denote ctx) = False := by
-  simp [Poly.isUnsatLe] <;> split <;> simp
-  next p k h =>
-    intro h'
-    replace h := congrArg (Poly.denote ctx) h
-    simp at h
-    replace h := congrArg (Expr.denote ctx rhs + ·) h
-    simp at h
-    rw [Int.add_comm, Int.sub_add_cancel] at h
-    rw [h]; clear h
-    intro h
-    conv at h => rhs; rw [← Int.zero_add (Expr.denote ctx rhs)]
-    rw [Int.add_le_add_iff_right] at h
-    replace h := Int.lt_of_lt_of_le h' h
-    contradiction
-
-theorem le_eq_true (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isValidLe → (lhs.denote ctx ≤ rhs.denote ctx) = True := by
-  simp [Poly.isValidLe] <;> split <;> simp
-  next p k h =>
-    intro h'
-    replace h := congrArg (Poly.denote ctx) h
-    simp at h
-    replace h := congrArg (Expr.denote ctx rhs + ·) h
-    simp at h
-    rw [Int.add_comm, Int.sub_add_cancel] at h
-    rw [h]; clear h; simp
-    conv => rhs; rw [← Int.zero_add (Expr.denote ctx rhs)]
-    rw [Int.add_le_add_iff_right]; assumption
+def RelCnstr.isUnsatCoeff (k : Int) : RelCnstr → Bool
+  | .eq p => p.divCoeffs k && k > 0 && cmod p.getConst k < 0
+  | .le _ => false
 
 private theorem contra {a b k : Int} (h₀ : 0 < k) (h₁ : -k < b) (h₂ : b < 0) (h₃ : a*k + b = 0) : False := by
   have : b = -a*k := by
@@ -575,7 +619,7 @@ private theorem contra {a b k : Int} (h₀ : 0 < k) (h₁ : -k < b) (h₂ : b <
   have : (1 : Int) < 1 := Int.lt_of_le_of_lt h₂ h₁
   contradiction
 
-private theorem poly_eq_zero_eq_false (ctx : Context) {p : Poly} {k : Int} : p.divCoeffs k → k > 0 → cmod p.getConst k < 0 → (p.denote ctx = 0) = False := by
+private theorem RelCnstr.eq_false (ctx : Context) (p : Poly) (k : Int) : p.divCoeffs k → k > 0 → cmod p.getConst k < 0 → (RelCnstr.eq p).denote ctx = False := by
   simp
   intro h₁ h₂ h₃ h
   have hnz : k ≠ 0 := by intro h; rw [h] at h₂; contradiction
@@ -585,17 +629,30 @@ private theorem poly_eq_zero_eq_false (ctx : Context) {p : Poly} {k : Int} : p.d
   have high := h₃
   exact contra h₂ low high this
 
-def unsatEqDivCoeffCert (lhs rhs : Expr) (k : Int) : Bool :=
-  let p := (lhs.sub rhs).norm
-  p.divCoeffs k && k > 0 && cmod p.getConst k < 0
+theorem RawRelCnstr.eq_false_of_isUnsat_coeff (ctx : Context) (c : RawRelCnstr) (k : Int) : c.norm.isUnsatCoeff k → c.denote ctx = False := by
+  intro h
+  cases c <;> simp [norm, RelCnstr.isUnsatCoeff] at h
+  next e₁ e₂ =>
+    have ⟨⟨h₁, h₂⟩, h₃⟩ := h
+    have := RelCnstr.eq_false ctx _ _ h₁ h₂ h₃
+    simp at this
+    simp
+    intro he
+    simp [he] at this
 
-theorem eq_eq_false_of_divCoeff (ctx : Context) (lhs rhs : Expr) (k : Int) : unsatEqDivCoeffCert lhs rhs k → (lhs.denote ctx = rhs.denote ctx) = False := by
-  simp [unsatEqDivCoeffCert]
-  intro h₁ h₂ h₃
-  have h := poly_eq_zero_eq_false ctx h₁ h₂ h₃; clear h₁ h₂ h₃
-  simp at h
-  intro h'
-  simp [h'] at h
+def RelCnstr.isValid : RelCnstr → Bool
+  | .eq (.num k) => k == 0
+  | .eq _ => false
+  | .le (.num k) => k ≤ 0
+  | .le _ => false
+
+theorem RelCnstr.eq_true_of_isValid (ctx : Context) (c : RelCnstr) : c.isValid → c.denote ctx = True := by
+  unfold isValid <;> split <;> simp
+
+theorem RawRelCnstr.eq_true_of_isValid (ctx : Context) (c : RawRelCnstr) (h : c.norm.isValid) : c.denote ctx = True := by
+  have := RelCnstr.eq_true_of_isValid ctx c.norm h
+  rw [RawRelCnstr.denote_norm] at this
+  assumption
 
 private def gcd (a b : Int) : Int :=
   Int.ofNat <| Int.gcd a b
@@ -621,23 +678,43 @@ theorem Poly.gcd_dvd_const {ctx : Context} {p : Poly} {k : Int} (h : k ∣ p.den
     rw [Int.add_comm] at h
     exact ih (gcd_dvd_step h)
 
-def Poly.isUnsatDvd (k : Int) (p : Poly) : Bool :=
-  p.getConst % p.gcdCoeffs k != 0
+/-- Divibility constraint of the form `k ∣ p`. -/
+structure DvdCnstr where
+  k : Int
+  p : Poly
+
+def DvdCnstr.denote (ctx : Context) (c : DvdCnstr) : Prop :=
+  c.k ∣ c.p.denote ctx
+
+def DvdCnstr.denote' (ctx : Context) (c : DvdCnstr) : Prop :=
+  c.k ∣ c.p.denote' ctx
+
+theorem DvdCnstr.denote'_eq_denote (ctx : Context) (c : DvdCnstr) : c.denote' ctx = c.denote ctx := by
+  simp [denote', denote, Poly.denote'_eq_denote]
+
+def DvdCnstr.isUnsat (c : DvdCnstr) : Bool :=
+  c.p.getConst % c.p.gcdCoeffs c.k != 0
+
+def DvdCnstr.isEqv (c₁ c₂ : DvdCnstr) (k : Int) : Bool :=
+  k != 0 && c₁.k == k*c₂.k && c₁.p == c₂.p.mul k
+
+def DvdCnstr.div (k' : Int) : DvdCnstr → DvdCnstr
+  | { k, p } => { k := k / k', p := p.div k' }
 
 private theorem not_dvd_of_not_mod_zero {a b : Int} (h : ¬ b % a = 0) : ¬ a ∣ b := by
   intro h; have := Int.emod_eq_zero_of_dvd h; contradiction
 
-private theorem dvd_eq_false' (ctx : Context) (k : Int) (p : Poly) : p.isUnsatDvd k → (k ∣ p.denote' ctx) = False := by
-  simp [Poly.isUnsatDvd]
+theorem DvdCnstr.eq_false_of_isUnsat (ctx : Context) (c : DvdCnstr) : c.isUnsat → c.denote ctx = False := by
+  rcases c with ⟨a, p⟩
+  simp [isUnsat, denote]
   intro h₁ h₂
   have := Poly.gcd_dvd_const h₂
   have := not_dvd_of_not_mod_zero h₁
   contradiction
 
-theorem dvd_unsat (ctx : Context) (k : Int) (p : Poly) : p.isUnsatDvd k → k ∣ p.denote' ctx → False := by
-  intro h₁
-  rw [dvd_eq_false' ctx _ _ h₁]
-  intro; contradiction
+theorem DvdCnstr.false_of_isUnsat_of_denote (ctx : Context) (c : DvdCnstr) : c.isUnsat → c.denote ctx → False := by
+  intro h₁ h₂
+  simp [eq_false_of_isUnsat, h₁] at h₂
 
 @[local simp] private theorem mul_dvd_mul_eq {a b c : Int} (hnz : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c := by
   constructor
@@ -651,36 +728,16 @@ theorem dvd_unsat (ctx : Context) (k : Int) (p : Poly) : p.isUnsatDvd k → k
     exists k
     rw [h, Int.mul_assoc]
 
-theorem norm_dvd (ctx : Context) (k : Int) (e : Expr) (p : Poly) : e.norm == p → (k ∣ e.denote ctx) = (k ∣ p.denote' ctx) := by
-  simp; intro h; simp [← h]
-
-theorem dvd_eq_false (ctx : Context) (k : Int) (e : Expr) (h : e.norm.isUnsatDvd k) : (k ∣ e.denote ctx) = False := by
-  rw [norm_dvd ctx k e e.norm BEq.refl]
-  apply dvd_eq_false' ctx k e.norm h
-
-def dvd_coeff_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) (k : Int) : Bool :=
-  k != 0 && (k₁ == k*k₂ && p₁ == p₂.mul k)
-
-def norm_dvd_gcd_cert (k₁ : Int) (e₁ : Expr) (k₂ : Int) (p₂ : Poly) (k : Int) : Bool :=
-  dvd_coeff_cert k₁ e₁.norm k₂ p₂ k
-
-theorem norm_dvd_gcd (ctx : Context) (k₁ : Int) (e₁ : Expr) (k₂ : Int) (p₂ : Poly) (g : Int)
-    : norm_dvd_gcd_cert k₁ e₁ k₂ p₂ g → (k₁ ∣ e₁.denote ctx) = (k₂ ∣ p₂.denote' ctx) := by
-  simp [norm_dvd_gcd_cert, dvd_coeff_cert]
-  intro h₁ h₂ h₃
+@[local simp] theorem DvdCnstr.eq_of_isEqv (ctx : Context) (c₁ c₂ : DvdCnstr) (k : Int) (h : isEqv c₁ c₂ k) : c₁.denote ctx = c₂.denote ctx := by
+  rcases c₁ with ⟨a₁, e₁⟩
+  rcases c₂ with ⟨a₂, e₂⟩
+  simp [isEqv] at h
+  rcases h with ⟨⟨h₁, h₂⟩, h₃⟩
   replace h₃ := congrArg (Poly.denote ctx) h₃
   simp at h₃
-  simp [*]
+  simp [denote, *]
 
-theorem dvd_coeff (ctx : Context) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) (g : Int)
-    : dvd_coeff_cert k₁ p₁ k₂ p₂ g → k₁ ∣ p₁.denote' ctx → k₂ ∣ p₂.denote' ctx := by
-  simp [dvd_coeff_cert]
-  intro h₁ h₂ h₃
-  replace h₃ := congrArg (Poly.denote ctx) h₃
-  simp at h₃
-  simp [*]
-
-private theorem dvd_gcd_of_dvd (d a x p : Int) (h : d ∣ a * x + p) : gcd d a ∣ p := by
+theorem dvd_gcd_of_dvd (d a x p : Int) (h : d ∣ a * x + p) : gcd d a ∣ p := by
   rcases h with ⟨k, h⟩
   simp [Int.Linear.gcd]
   replace h := congrArg (· - a*x) h
@@ -692,20 +749,49 @@ private theorem dvd_gcd_of_dvd (d a x p : Int) (h : d ∣ a * x + p) : gcd d a
   rw [Int.mul_assoc, Int.mul_assoc, ← Int.mul_sub] at h
   exists k₁ * k - k₂ * x
 
-def dvd_elim_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly) : Bool :=
-  match p₁ with
-  | .add a _ p => k₂ == gcd k₁ a && p₂ == p
+def DvdCnstr.isElim (c₁ c₂ : DvdCnstr) : Bool :=
+  match c₁.p with
+  | .add a _ p => c₂.k == gcd c₁.k a && c₂.p == p
   | _ => false
 
-theorem dvd_elim (ctx : Context) (k₁ : Int) (p₁ : Poly) (k₂ : Int) (p₂ : Poly)
-    : dvd_elim_cert k₁ p₁ k₂ p₂ → k₁ ∣ p₁.denote' ctx → k₂ ∣ p₂.denote' ctx := by
-  rcases p₁ <;> simp [dvd_elim_cert]
+theorem DvdCnstr.elim (ctx : Context) (c₁ c₂ : DvdCnstr) : isElim c₁ c₂ → c₁.denote' ctx → c₂.denote' ctx := by
+  rcases c₁ with ⟨k₁, p₁⟩
+  rcases c₂ with ⟨k₂, p₂⟩
+  rcases p₁ <;> simp [DvdCnstr.isElim]
   next a _ p =>
   intro _ _; subst k₂ p₂
+  simp [DvdCnstr.denote'_eq_denote, denote]
   rw [Int.add_comm]
   apply dvd_gcd_of_dvd
 
-private theorem dvd_solve_combine' {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p₂ : Int} {α β d : Int}
+/-- Raw divisibility constraint of the form `k ∣ e`. -/
+structure RawDvdCnstr where
+  k : Int
+  e : Expr
+  deriving BEq
+
+def RawDvdCnstr.denote (ctx : Context) (c : RawDvdCnstr) : Prop :=
+  c.k ∣ c.e.denote ctx
+
+def RawDvdCnstr.norm (c : RawDvdCnstr) : DvdCnstr :=
+  { k := c.k, p := c.e.toPoly }
+
+@[simp] theorem RawDvdCnstr.denote_norm_eq (ctx : Context) (c : RawDvdCnstr) : c.denote ctx = c.norm.denote ctx := by
+  simp [norm, denote, DvdCnstr.denote]
+
+def RawDvdCnstr.isEqv (c : RawDvdCnstr) (c' : DvdCnstr) (k : Int) : Bool :=
+  c.norm.isEqv c' k
+
+def RawDvdCnstr.isUnsat (c : RawDvdCnstr) : Bool :=
+  c.norm.isUnsat
+
+theorem RawDvdCnstr.eq_of_isEqv (ctx : Context) (c : RawDvdCnstr) (c' : DvdCnstr) (k : Int) (h : isEqv c c' k) : c.denote ctx = c'.denote' ctx := by
+  simp [DvdCnstr.eq_of_isEqv ctx c.norm c' k h, DvdCnstr.denote'_eq_denote]
+
+theorem RawDvdCnstr.eq_false_of_isUnsat (ctx : Context) (c : RawDvdCnstr) (h : c.isUnsat) : c.denote ctx = False := by
+  simp [DvdCnstr.eq_false_of_isUnsat ctx c.norm h]
+
+theorem solveCombine {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p₂ : Int} {α β d : Int}
    (h : α*a₁*d₂ + β*a₂*d₁ = d)
    (h₁ : d₁ ∣ a₁*x + p₁)
    (h₂ : d₂ ∣ a₂*x + p₂)
@@ -732,7 +818,7 @@ private theorem dvd_solve_combine' {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p
  rw [h, ←ac]
  assumption
 
-private theorem dvd_solve_elim' {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p₂ : Int} {d : Int}
+theorem solveElim {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p₂ : Int} {d : Int}
    (h : d = Int.gcd (a₁*d₂) (a₂*d₁))
    (h₁ : d₁ ∣ a₁*x + p₁)
    (h₂ : d₂ ∣ a₂*x + p₂)
@@ -754,257 +840,96 @@ private theorem dvd_solve_elim' {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p₂
  rw [h₃, h₄, Int.mul_assoc, Int.mul_assoc, ←Int.mul_sub] at this
  exact ⟨k₄ * k₁ - k₃ * k₂, this⟩
 
-def dvd_solve_combine_cert (d₁ : Int) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d : Int) (p : Poly) (g α β : Int) : Bool :=
-  match p₁, p₂ with
-  | .add a₁ x₁ p₁, .add a₂ x₂ p₂ =>
+def isSolveCombine (c₁ c₂ c : DvdCnstr) (d α β : Int) : Bool :=
+  match c₁, c₂ with
+  | { k := d₁, p := .add a₁ x₁ p₁ }, { k := d₂, p := .add a₂ x₂ p₂ } =>
     x₁ == x₂ &&
-    (g == α*a₁*d₂ + β*a₂*d₁ &&
-    (d == d₁*d₂ &&
-     p == .add g x₁ (p₁.mul (α*d₂) |>.combine (p₂.mul (β*d₁)))))
+    (d == α*a₁*d₂ + β*a₂*d₁ &&
+    (c.k == d₁*d₂ &&
+     c.p == .add d x₁ (p₁.mul (α*d₂) |>.combine (p₂.mul (β*d₁)))))
   | _, _ => false
 
-theorem dvd_solve_combine (ctx : Context) (d₁ : Int) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d : Int) (p : Poly) (g α β : Int)
-    : dvd_solve_combine_cert d₁ p₁ d₂ p₂ d p g α β → d₁ ∣ p₁.denote' ctx → d₂ ∣ p₂.denote' ctx → d ∣ p.denote' ctx := by
-  simp [dvd_solve_combine_cert]
-  split <;> simp
-  next a₁ x₁ p₁ a₂ x₂ p₂ =>
-  intro _ hg hd hp; subst x₁ p
-  simp [Poly.denote'_add]
+theorem DvdCnstr.solve_combine (ctx : Context) (c₁ c₂ c : DvdCnstr) (d α β : Int)
+    : isSolveCombine c₁ c₂ c d α β → c₁.denote' ctx → c₂.denote' ctx → c.denote' ctx := by
+  simp [isSolveCombine]
+  split <;> simp <;> cases c <;> simp [denote', Poly.denote_combine, Poly.denote'_add]
+  next d₁ a₁ x₁ p₁ d₂ a₂ x₂ p₂ k p =>
+  intro _ hd _ hp; subst x₁ k p
+  simp [Poly.denote'_add, Poly.denote, Poly.denote_combine]
   intro h₁ h₂
   rw [Int.add_comm] at h₁ h₂
-  rw [Int.add_comm _ (g * x₂.denote ctx), Int.add_left_comm, ← Int.add_assoc, hd]
-  exact dvd_solve_combine' hg.symm h₁ h₂
+  rw [Int.add_comm _ (d * x₂.denote ctx), Int.add_left_comm, ← Int.add_assoc]
+  exact solveCombine hd.symm h₁ h₂
 
-def dvd_solve_elim_cert (d₁ : Int) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d : Int) (p : Poly) : Bool :=
-  match p₁, p₂ with
-  | .add a₁ x₁ p₁, .add a₂ x₂ p₂ =>
+def isSolveElim (c₁ c₂ c : DvdCnstr) (d : Int) : Bool :=
+  match c₁, c₂ with
+  | { k := d₁, p := .add a₁ x₁ p₁ }, { k := d₂, p := .add a₂ x₂ p₂ } =>
     x₁ == x₂ &&
     (d == Int.gcd (a₁*d₂) (a₂*d₁) &&
-     p == (p₁.mul a₂ |>.combine (p₂.mul (- a₁))))
+    (c.k == d &&
+     c.p == (p₁.mul a₂ |>.combine (p₂.mul (- a₁)))))
   | _, _ => false
 
-theorem dvd_solve_elim (ctx : Context) (d₁ : Int) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d : Int) (p : Poly)
-    : dvd_solve_elim_cert d₁ p₁ d₂ p₂ d p → d₁ ∣ p₁.denote' ctx → d₂ ∣ p₂.denote' ctx → d ∣ p.denote' ctx := by
-  simp [dvd_solve_elim_cert]
-  split <;> simp
-  next a₁ x₁ p₁ a₂ x₂ p₂ =>
-  intro _ hd _; subst x₁ p; simp
+theorem DvdCnstr.solve_elim (ctx : Context) (c₁ c₂ c : DvdCnstr) (d : Int)
+    : isSolveElim c₁ c₂ c d → c₁.denote' ctx → c₂.denote' ctx → c.denote' ctx := by
+  simp [isSolveElim]
+  split <;> simp <;> cases c <;> simp [denote', Poly.denote_combine, Poly.denote'_add]
+  next d₁ a₁ x₁ p₁ d₂ a₂ x₂ p₂ k p =>
+  intro _ hd _ hp; subst x₁ k p
+  simp [Poly.denote'_eq_denote, Poly.denote_combine]
   intro h₁ h₂
   rw [Int.add_comm] at h₁ h₂
   rw [← Int.sub_eq_add_neg]
-  exact dvd_solve_elim' hd h₁ h₂
+  exact solveElim hd h₁ h₂
 
-theorem dvd_norm (ctx : Context) (d : Int) (p₁ p₂ : Poly) : p₁.norm == p₂ → d ∣ p₁.denote' ctx → d ∣ p₂.denote' ctx := by
+def DvdCnstr.isNorm (c₁ c₂ : DvdCnstr) : Bool :=
+  c₁.k == c₂.k && c₁.p.norm == c₂.p
+
+theorem DvdCnstr.of_isNorm (ctx : Context) (c₁ c₂ : DvdCnstr)
+    : isNorm c₁ c₂ → c₁.denote' ctx → c₂.denote' ctx := by
+  cases c₁ <;> cases c₂ <;> simp [isNorm, denote', Poly.denote'_eq_denote]
+  next k₁ p₁ k₂ p₂ =>
+    intro; subst k₁; intro; subst p₂
+    intro h₁
+    simp [Poly.denote_norm ctx p₁, h₁]
+
+theorem DvdCnstr.of_isEqv (ctx : Context) (c₁ c₂ : DvdCnstr) (k : Int) (h : isEqv c₁ c₂ k) : c₁.denote' ctx → c₂.denote' ctx := by
+  simp [DvdCnstr.denote'_eq_denote, DvdCnstr.eq_of_isEqv ctx c₁ c₂ k h]
+
+theorem RelCnstr.of_norm_eq (ctx : Context) (c₁ c₂ : RelCnstr) (h : c₁.norm == c₂) : c₁.denote' ctx → c₂.denote' ctx := by
+  simp at h
+  replace h := congrArg (RelCnstr.denote ctx) h
+  simp only [RelCnstr.denote_norm] at h
+  simp only [RelCnstr.denote'_eq_denote, h]
+  intro; assumption
+
+def RelCnstr.divByLe (c₁ c₂ : RelCnstr) (k : Int) : Bool :=
+  k > 0 && (c₁.isLe && (c₁.divCoeffs k && c₂ == c₁.div k))
+
+theorem RelCnstr.of_divByLe (ctx : Context) (c₁ c₂ : RelCnstr) (k : Int) (h : divByLe c₁ c₂ k) : c₁.denote' ctx → c₂.denote' ctx := by
+  simp [divByLe] at h
+  rcases h with ⟨h₁, h₂, h₃, h₄⟩
+  simp only [RelCnstr.denote'_eq_denote]
+  exact RelCnstr.eq_of_norm_eq_of_divCoeffs ctx c₁ c₂ k h₁ h₃ h₂ h₄ |>.mp
+
+def RelCnstr.negLe (c₁ c₂ : RelCnstr) : Bool :=
+  c₁.isLe && c₂ == (c₁.mul (-1) |>.addConst 1)
+
+theorem RelCnstr.of_negLe (ctx : Context) (c₁ c₂ : RelCnstr) (h : negLe c₁ c₂) : ¬ c₁.denote' ctx → c₂.denote' ctx := by
+  simp [negLe] at h
+  rcases h with ⟨h₁, h₂⟩
+  cases c₁ <;> simp [isLe] at h₁; clear h₁
+  replace h₂ := congrArg (RelCnstr.denote ctx) h₂
+  simp only [RelCnstr.denote'_eq_denote, h₂, RelCnstr.mul, RelCnstr.addConst]
   simp
-  intro; subst p₂
-  intro h₁
-  simp [Poly.denote_norm ctx p₁, h₁]
-
-theorem le_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 le_coeff_cert (p₁ p₂ : Poly) (k : Int) : Bool :=
-  k > 0 && (p₁.divCoeffs k && p₂ == p₁.div k)
-
-theorem le_coeff (ctx : Context) (p₁ p₂ : Poly) (k : Int) : le_coeff_cert p₁ p₂ k → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
-  simp [le_coeff_cert]
-  intro h₁ h₂ h₃
-  exact eq_of_norm_eq_of_divCoeffs h₁ h₂ h₃ |>.mp
-
-def le_neg_cert (p₁ p₂ : Poly) : Bool :=
-  p₂ == (p₁.mul (-1) |>.addConst 1)
-
-theorem le_neg (ctx : Context) (p₁ p₂ : Poly) : le_neg_cert p₁ p₂ → ¬ p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
-  simp [le_neg_cert]
-  intro; subst p₂; simp; intro h
+  intro h
   replace h : _ + 1 ≤ -0 := Int.neg_lt_neg <| Int.lt_of_not_ge h
   simp at h
   exact h
 
-def Poly.leadCoeff (p : Poly) : Int :=
-  match p with
-  | .add a _ _ => a
-  | _ => 1
-
-def le_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
-  let a₁ := p₁.leadCoeff.natAbs
-  let a₂ := p₂.leadCoeff.natAbs
-  p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
-
-theorem le_combine (ctx : Context) (p₁ p₂ p₃ : Poly)
-    : le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
-  simp [le_combine_cert]
-  intro; subst p₃
-  intro h₁ h₂; simp
-  rw [← Int.add_zero 0]
-  apply Int.add_le_add
-  · rw [← Int.zero_mul (Poly.denote ctx p₂)]; apply Int.mul_le_mul_of_nonpos_right <;> simp [*]
-  · rw [← Int.zero_mul (Poly.denote ctx p₁)]; apply Int.mul_le_mul_of_nonpos_right <;> simp [*]
-
-theorem le_unsat (ctx : Context) (p : Poly) : p.isUnsatLe → p.denote' ctx ≤ 0 → False := by
-  simp [Poly.isUnsatLe]; split <;> simp
+theorem RelCnstr.false_of_isUnsat_of_denote (ctx : Context) (c : RelCnstr) : c.isUnsat → c.denote ctx → False := by
   intro h₁ h₂
-  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
-  | .num _ => 0
-
-private theorem eq_add_coeff_insert (ctx : Context) (p : Poly) (x : Var) : p.denote ctx = (p.coeff x) * (x.denote ctx) + (p.insert (-p.coeff x) x).denote ctx := by
-  simp; rw [← Int.add_assoc, Int.add_neg_cancel_right]
-
-private theorem dvd_of_eq' {a x p : Int} : a*x + p = 0 → a ∣ p := by
-  intro h
-  replace h := Int.neg_eq_of_add_eq_zero h
-  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
-
-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₃
-
-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
-  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]
-    rw [Int.mul_add, ←Int.add_assoc, Int.mul_left_comm a b x]
-    rw [Int.add_comm (b*(a*x)), Int.add_neg_cancel_right, Int.sub_eq_add_neg]
-  rw [h₁, h₂] at h
-  simp at h
-  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 :=
-  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₂) &&
-  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]
-  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 d₃
-  intro; subst p₃
-  intro h₁ h₂
-  rw [Int.add_comm] at h₁ h₂
-  have := eq_dvd_subst' 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 :=
-  let a := p₁.coeff x
-  let b := p₂.coeff x
-  p₃ == (p₁.mul b |>.combine (p₂.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]
-  intro; subst p₃
-  intro h₁ h₂
-  simp [*]
-
-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₂
-  replace h₂ := Int.mul_le_mul_of_nonneg_left h₂ 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]
-  assumption
-
-def eq_of_core_cert (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
-  p₃ == p₁.combine (p₂.mul (-1))
-
-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]
+  simp [eq_false_of_isUnsat, h₁, -RelCnstr.denote] at h₂
 
 end Int.Linear
 

src/Init/Data/Int/Order.lean

@@ -1011,16 +1011,11 @@ theorem sign_eq_neg_one_iff_neg {a : Int} : sign a = -1 ↔ a < 0 :=
     exact Int.le_add_one (ofNat_nonneg _)
   | .negSucc _ => simp +decide [sign]
 
-@[simp] theorem mul_sign_self : ∀ i : Int, i * sign i = natAbs i
+theorem mul_sign : ∀ i : Int, i * sign i = natAbs i
   | succ _ => Int.mul_one _
   | 0 => Int.mul_zero _
   | -[_+1] => Int.mul_neg_one _
 
-@[deprecated mul_sign_self (since := "2025-02-24")] abbrev mul_sign := @mul_sign_self
-
-@[simp] theorem sign_mul_self : sign i * i = natAbs i := by
-  rw [Int.mul_comm, mul_sign_self]
-
 /- ## natAbs -/
 
 theorem natAbs_ne_zero {a : Int} : a.natAbs ≠ 0 ↔ a ≠ 0 := not_congr Int.natAbs_eq_zero

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/Nat/Div/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 prelude
 import Init.Omega
 import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Simproc
 
 /-!
 # Further lemmas about `Nat.div` and `Nat.mod`, with the convenience of having `omega` available.
@@ -63,53 +62,4 @@ theorem div_add_le_right {z : Nat} (h : 0 < z) (x y : Nat) :
     x / (y + z) ≤ x / z :=
   div_le_div_left (Nat.le_add_left z y) h
 
-theorem succ_div_of_dvd {a b : Nat} (h : b ∣ a + 1) :
-    (a + 1) / b = a / b + 1 := by
-  replace h := mod_eq_zero_of_dvd h
-  cases b with
-  | zero => simp at h
-  | succ b =>
-    by_cases h' : b ≤ a
-    · rw [Nat.div_eq]
-      simp only [zero_lt_succ, Nat.add_le_add_iff_right, h', and_self, ↓reduceIte,
-        Nat.reduceSubDiff, Nat.add_right_cancel_iff]
-      obtain ⟨_|k, h⟩ := Nat.dvd_of_mod_eq_zero h
-      · simp at h
-      · simp only [Nat.mul_add, Nat.add_mul, Nat.one_mul, Nat.mul_one, ← Nat.add_assoc,
-          Nat.add_right_cancel_iff] at h
-        subst h
-        rw [Nat.add_sub_cancel, ← Nat.add_one_mul, mul_div_right _ (zero_lt_succ _), Nat.add_comm,
-          Nat.add_mul_div_left _ _ (zero_lt_succ _), Nat.self_eq_add_left, div_eq_of_lt le.refl]
-    · simp only [Nat.not_le] at h'
-      replace h' : a + 1 < b + 1 := Nat.add_lt_add_right h' 1
-      rw [Nat.mod_eq_of_lt h'] at h
-      simp at h
-
-theorem succ_div_of_mod_eq_zero {a b : Nat} (h : (a + 1) % b = 0) :
-    (a + 1) / b = a / b + 1 := by
-  rw [succ_div_of_dvd (by rwa [dvd_iff_mod_eq_zero])]
-
-theorem succ_div_of_not_dvd {a b : Nat} (h : ¬ b ∣ a + 1) :
-    (a + 1) / b = a / b := by
-  replace h := mt dvd_of_mod_eq_zero h
-  cases b with
-  | zero => simp
-  | succ b =>
-    rw [eq_comm, Nat.div_eq_iff (by simp)]
-    constructor
-    · rw [Nat.div_mul_self_eq_mod_sub_self]
-      have : (a + 1) % (b + 1) < b + 1 := Nat.mod_lt _ (by simp)
-      omega
-    · rw [Nat.div_mul_self_eq_mod_sub_self]
-      omega
-
-theorem succ_div_of_mod_ne_zero {a b : Nat} (h : (a + 1) % b ≠ 0) :
-    (a + 1) / b = a / b := by
-  rw [succ_div_of_not_dvd (by rwa [dvd_iff_mod_eq_zero])]
-
-theorem succ_div {a b : Nat} : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0 := by
-  split <;> rename_i h
-  · simp [succ_div_of_dvd h]
-  · simp [succ_div_of_not_dvd h]
-
 end Nat

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