perf: bad filter

`has_fvar(e)` is a bad filter. For example, the free variable may be a
let-variable. The kernel was timining out when checking some proof
terms produced by cutsat. Many thanks to @nomeata for finding the
issue.

.github/workflows/pr-release.yml

@@ -34,7 +34,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v8 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v9 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -155,6 +155,20 @@ jobs:
           fi
 
           if [[ -n "$MESSAGE" ]]; then
+            # Check if force-mathlib-ci label is present
+            LABELS="$(curl --retry 3 --location --silent \
+                          -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                          -H "Accept: application/vnd.github.v3+json" \
+                          "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
+                          | jq -r '.[].name')"
+            
+            if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
+              echo "force-mathlib-ci label detected, forcing CI despite issues"
+              MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
+              FORCE_CI=true
+            else
+              MESSAGE="$MESSAGE You can force Mathlib CI using the \`force-mathlib-ci\` label."
+            fi
 
             echo "Checking existing messages"
 
@@ -201,7 +215,12 @@ jobs:
             else
               echo "The message already exists in the comment body."
             fi
-            echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
+
+            if [[ "$FORCE_CI" == "true" ]]; then
+              echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
+            else
+              echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
+            fi
           else
             echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
           fi
@@ -252,7 +271,7 @@ jobs:
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
+            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
@@ -316,7 +335,7 @@ jobs:
           if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
             BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
           else
-            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
+            echo "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 

CMakeLists.txt

@@ -47,10 +47,11 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
       string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
     endif()
+    string(APPEND CADICAL_CXXFLAGS " -DNCLOSEFROM")
     ExternalProject_add(cadical
       PREFIX cadical
       GIT_REPOSITORY https://github.com/arminbiere/cadical
-      GIT_TAG rel-1.9.5
+      GIT_TAG rel-2.1.2
       CONFIGURE_COMMAND ""
       # https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
       BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}

doc/declarations.md

@@ -764,11 +764,12 @@ 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 : α) extends Bar, Baz : Sort u :=
+structure Foo (a : α) : Sort u extends Bar, Baz :=
 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. 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 (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``.
 
 The declaration above is syntactic sugar for an inductive type declaration, and so results in the addition of the following constants to the environment:
 

flake.lock

@@ -36,17 +36,17 @@
     },
     "nixpkgs-cadical": {
       "locked": {
-        "lastModified": 1722221733,
-        "narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
+        "lastModified": 1740791350,
+        "narHash": "sha256-igS2Z4tVw5W/x3lCZeeadt0vcU9fxtetZ/RyrqsCRQ0=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
+        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
+        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
         "type": "github"
       }
     },

flake.nix

@@ -8,8 +8,8 @@
   # old nixpkgs used for portable release with older glibc (2.26)
   inputs.nixpkgs-older.url = "github:NixOS/nixpkgs/0b307aa73804bbd7a7172899e59ae0b8c347a62d";
   inputs.nixpkgs-older.flake = false;
-  # for cadical 1.9.5; sync with CMakeLists.txt
-  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/12bf09802d77264e441f48e25459c10c93eada2e";
+  # for cadical 2.1.2; sync with CMakeLists.txt by taking commit from https://www.nixhub.io/packages/cadical
+  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/199169a2135e6b864a888e89a2ace345703c025d";
   inputs.flake-utils.url = "github:numtide/flake-utils";
 
   outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system:

script/prepare-llvm-mingw.sh

@@ -25,7 +25,10 @@ cp llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
 echo '
 // https://docs.microsoft.com/en-us/windows/win32/api/errhandlingapi/nf-errhandlingapi-seterrormode
 #define SEM_FAILCRITICALERRORS 0x0001
-__declspec(dllimport) __stdcall unsigned int SetErrorMode(unsigned int uMode);' > stage1/include/clang/windows.h
+__declspec(dllimport) __stdcall unsigned int SetErrorMode(unsigned int uMode);
+// https://docs.microsoft.com/en-us/windows/console/setconsoleoutputcp
+#define CP_UTF8 65001
+__declspec(dllimport) __stdcall int SetConsoleOutputCP(unsigned int wCodePageID);' > stage1/include/clang/windows.h
 # COFF dependencies
 cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # runtime

script/release_notes.py

@@ -65,20 +65,21 @@ def format_markdown_description(pr_number, description):
     link = f"[#{pr_number}](https://github.com/leanprover/lean4/pull/{pr_number})"
     return f"{link} {description}"
 
+def commit_types():
+    # see doc/dev/commit_convention.md
+    return ['feat', 'fix', 'doc', 'style', 'refactor', 'test', 'chore', 'perf']
+
 def count_commit_types(commits):
     counts = {
         'total': len(commits),
-        'feat': 0,
-        'fix': 0,
-        'refactor': 0,
-        'doc': 0,
-        'chore': 0
     }
+    for commit_type in commit_types():
+        counts[commit_type] = 0
     
     for _, first_line, _ in commits:
-        for commit_type in ['feat:', 'fix:', 'refactor:', 'doc:', 'chore:']:
-            if first_line.startswith(commit_type):
-                counts[commit_type.rstrip(':')] += 1
+        for commit_type in commit_types():
+            if first_line.startswith(f'{commit_type}:'):
+                counts[commit_type] += 1
                 break
     
     return counts
@@ -158,8 +159,9 @@ def main():
     counts = count_commit_types(commits)
     print(f"For this release, {counts['total']} changes landed. "
           f"In addition to the {counts['feat']} feature additions and {counts['fix']} fixes listed below "
-          f"there were {counts['refactor']} refactoring changes, {counts['doc']} documentation improvements "
-          f"and {counts['chore']} chores.\n")
+          f"there were {counts['refactor']} refactoring changes, {counts['doc']} documentation improvements, "
+          f"{counts['perf']} performance improvements, {counts['test']} improvements to the test suite "
+          f"and {counts['style'] + counts['chore']} other changes.\n")
 
     section_order = sort_sections_order()
     sorted_changelog = sorted(changelog.items(), key=lambda item: section_order.index(format_section_title(item[0])) if format_section_title(item[0]) in section_order else len(section_order))

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 18)
+set(LEAN_VERSION_MINOR 19)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -144,11 +144,12 @@ 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_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
+  set(CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY "bin")
 else()
-  set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
+  set(CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY "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) extends Applicative f : Type (max (u+1) v) where
+class Alternative (f : Type u → Type v) : Type (max (u+1) v) extends Applicative f 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] extends LawfulFunctor f : Prop where
+class LawfulApplicative (f : Type u → Type v) [Applicative f] : Prop extends LawfulFunctor f 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] extends LawfulApplicative m : Prop where
+class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplicative m 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 (e.g., Trepplein) that do not implement this feature.
+external type checkers 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 (e.g., Trepplein) that do not implement this feature.
+external type checkers 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 (e.g., Trepplein) that do not implement this feature.
+external type checkers 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 α) extends LeftIdentity op o : Prop where
+class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extends LeftIdentity op o 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 β) extends RightIdentity op o : Prop where
+class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop extends RightIdentity op o where
   /-- Right identity `o` is an identity. -/
   right_id : ∀ a, op a o = a
 
@@ -2151,13 +2151,13 @@ class LawfulRightIdentity (op : α → β → α) (o : outParam β) extends Righ
 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 α) extends LeftIdentity op o, RightIdentity op o : Prop
+class Identity (op : α → α → α) (o : outParam α) : Prop extends LeftIdentity op o, RightIdentity op o
 
 /--
 `LawfulIdentity op o` indicates `o` is a verified left and right
 identity of `op`.
 -/
-class LawfulIdentity (op : α → α → α) (o : outParam α) extends Identity op o, LawfulLeftIdentity op o, LawfulRightIdentity op o : Prop
+class LawfulIdentity (op : α → α → α) (o : outParam α) : Prop extends Identity op o, LawfulLeftIdentity op o, LawfulRightIdentity op o
 
 /--
 `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] extends LawfulIdentity op o : Prop where
+class LawfulCommIdentity (op : α → α → α) (o : outParam α) [hc : Commutative op] : Prop extends LawfulIdentity op o 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,8 +8,9 @@ import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Count
 import Init.Data.List.Attach
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Array
 
@@ -554,6 +555,10 @@ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array
     (xs.push a).unattach = xs.unattach.push a.1 := by
   simp only [unattach, Array.map_push]
 
+@[simp] theorem mem_unattach {p : α → Prop} {xs : Array { x // p x }} {a} :
+    a ∈ xs.unattach ↔ ∃ h : p a, ⟨a, h⟩ ∈ xs := by
+  simp only [unattach, mem_map, Subtype.exists, exists_and_right, exists_eq_right]
+
 @[simp] theorem size_unattach {p : α → Prop} {xs : Array { x // p x }} :
     xs.unattach.size = xs.size := by
   unfold unattach
@@ -675,6 +680,20 @@ and simplifies these to the function directly taking the value.
   simp
   rw [List.find?_subtype hf]
 
+@[simp] theorem all_subtype {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) (w : stop = xs.size) :
+    xs.all f 0 stop = xs.unattach.all g := by
+  subst w
+  rcases xs with ⟨xs⟩
+  simp [hf]
+
+@[simp] theorem any_subtype {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) (w : stop = xs.size) :
+    xs.any f 0 stop = xs.unattach.any g := by
+  subst w
+  rcases xs with ⟨xs⟩
+  simp [hf]
+
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
 @[simp] theorem unattach_filter {p : α → Prop} {xs : Array { x // p x }}

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
 
@@ -144,6 +144,8 @@ end List
 
 namespace Array
 
+theorem size_eq_length_toList (xs : Array α) : xs.size = xs.toList.length := rfl
+
 @[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @List.toList_toArray
 
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@@ -1090,6 +1092,11 @@ 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⟩
@@ -1102,6 +1109,20 @@ 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
 
@@ -23,6 +23,18 @@ section countP
 
 variable (p q : α → Bool)
 
+@[simp] theorem _root_.List.countP_toArray (l : List α) : countP p l.toArray = l.countP p := by
+  simp [countP]
+  induction l with
+  | nil => rfl
+  | cons hd tl ih =>
+    simp only [List.foldr_cons, ih, List.countP_cons]
+    split <;> simp_all
+
+@[simp] theorem countP_toList (xs : Array α) : xs.toList.countP p = countP p xs := by
+  cases xs
+  simp
+
 @[simp] theorem countP_empty : countP p #[] = 0 := rfl
 
 @[simp] theorem countP_push_of_pos (xs) (pa : p a) : countP p (xs.push a) = countP p xs + 1 := by
@@ -150,6 +162,13 @@ section count
 
 variable [BEq α]
 
+@[simp] theorem _root_.List.count_toArray (l : List α) (a : α) : count a l.toArray = l.count a := by
+  simp [count, List.count_eq_countP]
+
+@[simp] theorem count_toList (xs : Array α) (a : α) : xs.toList.count a = xs.count a := by
+  cases xs
+  simp
+
 @[simp] theorem count_empty (a : α) : count a #[] = 0 := rfl
 
 theorem count_push (a b : α) (xs : 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
 
@@ -282,6 +282,10 @@ end erase
 
 /-! ### eraseIdx -/
 
+theorem eraseIdx_eq_eraseIdxIfInBounds {xs : Array α} {i : Nat} (h : i < xs.size) :
+    xs.eraseIdx i h = xs.eraseIdxIfInBounds i := by
+  simp [eraseIdxIfInBounds, h]
+
 theorem eraseIdx_eq_take_drop_succ (xs : Array α) (i : Nat) (h) : xs.eraseIdx i = xs.take i ++ xs.drop (i + 1) := by
   rcases xs with ⟨xs⟩
   simp only [List.size_toArray] at h

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,11 +99,6 @@ 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]
 
@@ -304,24 +299,6 @@ 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
@@ -547,6 +524,47 @@ 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.
@@ -584,10 +602,26 @@ The lemmas below should be made consistent with those for `findIdx?` (and proved
   rcases xs with ⟨xs⟩
   simp [List.idxOf?_eq_none_iff]
 
-/-! ### finIdxOf? -/
+/-! ### 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 : 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/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

@@ -6,10 +6,11 @@ Authors: Mario Carneiro, Kim Morrison
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
+import Init.Data.Array.OfFn
 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
 
@@ -23,6 +23,9 @@ open Nat
 
 /-! ### mapM -/
 
+@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f := by
+  induction xs; simp_all
+
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {xs ys : Array α} :
     (xs ++ ys).mapM f = (return (← xs.mapM f) ++ (← ys.mapM f)) := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/OfFn.lean

@@ -11,11 +11,30 @@ 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
 
+@[simp] theorem ofFn_zero (f : Fin 0 → α) : ofFn f = #[] := rfl
+
+theorem ofFn_succ (f : Fin (n+1) → α) :
+    ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩) := by
+  ext i h₁ h₂
+  · simp
+  · simp [getElem_push]
+    split <;> rename_i h₃
+    · rfl
+    · congr
+      simp at h₁ h₂
+      omega
+
+@[simp] theorem _rooy_.List.toArray_ofFn (f : Fin n → α) : (List.ofFn f).toArray = Array.ofFn f := by
+  ext <;> simp
+
+@[simp] theorem toList_ofFn (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f := by
+  apply List.ext_getElem <;> simp
+
 @[simp]
 theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by
   rw [← Array.toList_inj]

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, size_range']
+  rw [← size_eq_zero_iff, 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, size_range]
+  rw [← size_eq_zero_iff, 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 (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·) := by
+theorem range_add (n m : Nat) : range (n + m) = range n ++ (range m).map (n + ·) := by
   rw [← range'_eq_map_range]
-  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm
+  simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 n m).symm
 
 theorem reverse_range' (s n : Nat) : reverse (range' s n) = map (s + n - 1 - ·) (range n) := by
   simp [← toList_inj, List.reverse_range']
@@ -164,7 +164,7 @@ theorem not_mem_range_self {n : Nat} : n ∉ range n := by simp
 
 theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1) := by simp
 
-@[simp] theorem take_range (m n : Nat) : take (range n) m = range (min m n) := by
+@[simp] theorem take_range (i n : Nat) : take (range n) i = range (min i n) := by
   ext <;> simp
 
 @[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :

src/Init/Data/Array/Set.lean

@@ -6,8 +6,8 @@ Authors: Leonardo de Moura, Mario Carneiro
 prelude
 import Init.Tactics
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 
 /--

src/Init/Data/Array/Subarray.lean

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

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

@@ -15,8 +15,8 @@ automation. Placing them in another module breaks an import cycle, because `omeg
 array library.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Subarray
 /--

src/Init/Data/Array/TakeDrop.lean

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

src/Init/Data/Array/Zip.lean

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

src/Init/Data/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 α] extends PartialEquivBEq α, ReflBEq α : Prop
+class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 
 @[simp]
 theorem BEq.refl [BEq α] [ReflBEq α] {a : α} : a == a :=
@@ -49,6 +49,14 @@ theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = fal
 theorem BEq.trans [BEq α] [PartialEquivBEq α] {a b c : α} : a == b → b == c → a == c :=
   PartialEquivBEq.trans
 
+theorem BEq.congr_left [BEq α] [PartialEquivBEq α] {a b c : α} (h : a == b) :
+    (a == c) = (b == c) :=
+  Bool.eq_iff_iff.mpr ⟨BEq.trans (BEq.symm h), BEq.trans h⟩
+
+theorem BEq.congr_right [BEq α] [PartialEquivBEq α] {a b c : α} (h : b == c) :
+    (a == b) = (a == c) :=
+  Bool.eq_iff_iff.mpr ⟨fun h' => BEq.trans h' h, fun h' => BEq.trans h' (BEq.symm h)⟩
+
 theorem BEq.neq_of_neq_of_beq [BEq α] [PartialEquivBEq α] {a b c : α} :
     (a == b) = false → b == c → (a == c) = false :=
   fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₁ (BEq.trans h₃ (BEq.symm h₂))

src/Init/Data/BitVec/Bitblast.lean

@@ -544,6 +544,15 @@ theorem slt_eq_not_carry (x y : BitVec w) :
 theorem sle_eq_not_slt (x y : BitVec w) : x.sle y = !y.slt x := by
   simp only [BitVec.sle, BitVec.slt, ← decide_not, decide_eq_decide]; omega
 
+theorem zero_sle_eq_not_msb {w : Nat} {x : BitVec w} : BitVec.sle 0#w x = !x.msb := by
+  rw [sle_eq_not_slt, BitVec.slt_zero_eq_msb]
+
+theorem zero_sle_iff_msb_eq_false {w : Nat} {x : BitVec w} : BitVec.sle 0#w x ↔ x.msb = false := by
+  simp [zero_sle_eq_not_msb]
+
+theorem toNat_toInt_of_sle {w : Nat} (b : BitVec w) (hb : BitVec.sle 0#w b) : b.toInt.toNat = b.toNat :=
+  toNat_toInt_of_msb b (zero_sle_iff_msb_eq_false.1 hb)
+
 theorem sle_eq_carry (x y : BitVec w) :
     x.sle y = !((x.msb == y.msb).xor (carry w y (~~~x) true)) := by
   rw [sle_eq_not_slt, slt_eq_not_carry, beq_comm]
@@ -907,7 +916,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 : Type where
+  extends DivModState.Lawful args qr where
   /-- Only perform a round of shift-subtract if we have dividend bits. -/
   hwn_lt : 0 < qr.wn
 

src/Init/Data/BitVec/Lemmas.lean

@@ -13,6 +13,7 @@ import Init.Data.Nat.Div.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Nat.Div.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
+import Init.Data.Int.LemmasAux
 import Init.Data.Int.Pow
 
 set_option linter.missingDocs true
@@ -323,6 +324,9 @@ theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
 @[simp, bitvec_to_nat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
   simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
 
+theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n :=
+  eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn])
+
 @[simp] theorem toFin_ofNat (x : Nat) : toFin (BitVec.ofNat w x) = Fin.ofNat' (2^w) x := rfl
 
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
@@ -528,6 +532,9 @@ theorem toInt_eq_toNat_of_msb {x : BitVec w} (h : x.msb = false) :
     x.toInt = x.toNat := by
   simp [toInt_eq_msb_cond, h]
 
+theorem toNat_toInt_of_msb {w : Nat} (b : BitVec w) (hb : b.msb = false) : b.toInt.toNat = b.toNat := by
+  simp [b.toInt_eq_toNat_of_msb hb]
+
 theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) := by
   simp only [toInt_eq_toNat_cond]
   split
@@ -569,6 +576,11 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
   have p : 0 ≤ i % (2^n : Nat) := by omega
   simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
 
+theorem toInt_ofInt_eq_self {w : Nat} (hw : 0 < w) {n : Int}
+    (h : -2 ^ (w - 1) ≤ n) (h' : n < 2 ^ (w - 1)) : (BitVec.ofInt w n).toInt = n := by
+  have hw : w = (w - 1) + 1 := by omega
+  rw [toInt_ofInt, Int.bmod_eq_self_of_le] <;> (rw [hw]; simp [Int.natCast_pow]; omega)
+
 @[simp] theorem ofInt_natCast (w n : Nat) :
   BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl
 
@@ -645,6 +657,12 @@ theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
     simp [BitVec.slt, this]
     omega
 
+theorem slt_zero_eq_msb {w : Nat} {x : BitVec  w} : x.slt 0#w = x.msb := by
+  rw [Bool.eq_iff_iff, BitVec.slt_zero_iff_msb_cond]
+
+theorem sle_iff_toInt_le {w : Nat} {b b' : BitVec w} : b.sle b' ↔ b.toInt ≤ b'.toInt :=
+  decide_eq_true_iff
+
 /-! ### setWidth, zeroExtend and truncate -/
 
 @[simp]
@@ -1467,6 +1485,16 @@ theorem extractLsb_not_of_lt {x : BitVec w} {hi lo : Nat} (hlo : lo ≤ hi) (hhi
   simp [hk, show k ≤ hi - lo by omega]
   omega
 
+@[simp]
+theorem ne_not_self {a : BitVec w} (h : 0 < w) : a ≠ ~~~a := by
+  have : ∃ x, x < w := ⟨w - 1, by omega⟩
+  simp [BitVec.eq_of_getElem_eq_iff, this]
+
+@[simp]
+theorem not_self_ne {a : BitVec w} (h : 0 < w) : ~~~a ≠ a := by
+  rw [ne_comm]
+  simp [h]
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(x.cast h) = (~~~x).cast h := by
@@ -1517,8 +1545,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) && getLsbD x (i - n)) := by
-  rw [← testBit_toNat, getElem_eq_testBit_toNat]
+    (x <<< n)[i] = (!decide (i < n) && x[i - n]) := by
+  rw [getElem_eq_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 +1596,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] = ((! decide (i < n)) && getLsbD x (i - n)) := by
-  rw [shiftLeftZeroExtend_eq, getLsbD]
+    (shiftLeftZeroExtend x n)[i] = if h' : i < n then false else x[i - n] := by
+  rw [shiftLeftZeroExtend_eq]
   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 +1626,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, Fin.is_lt, decide_true, Bool.true_and]
-  rw [show i - (n + m) = (i - m - n) by omega]
+  simp only [getElem_shiftLeft]
+  rw [show x[i - (n + m)] = x[i - m - n] by congr 1; omega]
   cases h₂ : decide (i < m) <;>
   cases h₃ : decide (i - m < w) <;>
   cases h₄ : decide (i - m < n) <;>
@@ -1632,7 +1660,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.getLsbD (i - y.toNat)) := by
+    (x <<< y)[i] = (!decide (i < y.toNat) && x[i - y.toNat]) := by
   simp
 
 @[simp] theorem shiftLeft_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) : x <<< n = 0#w := by
@@ -1844,13 +1872,10 @@ 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 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]
+    (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']
 
 theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
@@ -1957,9 +1982,8 @@ 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] =
-      (!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]
+    (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]
 
 theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
     (x.sshiftRight y.toNat).getMsbD i =
@@ -2030,9 +2054,8 @@ 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 i < w then x.getLsbD i else x.msb := by
-  rw [←getLsbD_eq_getElem, getLsbD_signExtend]
-  simp [h]
+    (x.signExtend v)[i] = if h : i < w then x[i] else x.msb := by
+  simp [←getLsbD_eq_getElem, getLsbD_signExtend, 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
@@ -2044,12 +2067,10 @@ 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 only [getElem_signExtend, h, decide_true, Bool.true_and, getElem_setWidth,
-    ite_eq_left_iff, Nat.not_lt]
-  omega
+  simp [getElem_signExtend, show i < w by omega]
 
 /-- Sign extending to the same bitwidth is a no op. -/
-theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
+@[simp] theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
   rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]
 
 /-- Sign extending to a larger bitwidth depends on the msb.
@@ -2091,42 +2112,63 @@ theorem toNat_signExtend (x : BitVec w) {v : Nat} :
   · have : 2^w ≤ 2^v := Nat.pow_le_pow_right Nat.two_pos (by omega)
     rw [toNat_signExtend_of_le x (by omega), toNat_setWidth, Nat.mod_eq_of_lt (by omega)]
 
-/-
+/--
 If the current width `w` is smaller than the extended width `v`,
 then the value when interpreted as an integer does not change.
 -/
-theorem toInt_signExtend_of_lt {x : BitVec w} (hv : w < v):
+theorem toInt_signExtend_of_le {x : BitVec w} (h : w ≤ v) :
     (x.signExtend v).toInt = x.toInt := by
-  simp only [toInt_eq_msb_cond, toNat_signExtend]
-  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]
-  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
-  <;> norm_cast
-  <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
-  omega
+  by_cases hlt : w < v
+  · rw [toInt_signExtend_of_lt hlt]
+  · obtain rfl : w = v := by omega
+    simp
+where
+  toInt_signExtend_of_lt {x : BitVec w} (hv : w < v):
+      (x.signExtend v).toInt = x.toInt := by
+    simp only [toInt_eq_msb_cond, toNat_signExtend]
+    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
+    <;> norm_cast
+    <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
+    omega
 
-/-
+/--
 If the current width `w` is larger than the extended width `v`,
 then the value when interpreted as an integer is truncated,
 and we compute a modulo by `2^v`.
 -/
-theorem toInt_signExtend_of_le {x : BitVec w} (hv : v ≤ w) :
+theorem toInt_signExtend_eq_toNat_bmod_of_le {x : BitVec w} (hv : v ≤ w) :
     (x.signExtend v).toInt = Int.bmod x.toNat (2^v) := by
   simp [signExtend_eq_setWidth_of_lt _ hv]
 
-/-
+/--
 Interpreting the sign extension of `(x : BitVec w)` to width `v`
-computes `x % 2^v` (where `%` is the balanced mod).
+computes `x % 2^v` (where `%` is the balanced mod). See `toInt_signExtend` for a version stated
+in terms of `toInt` instead of `toNat`.
 -/
-theorem toInt_signExtend (x : BitVec w) :
-    (x.signExtend v).toInt = Int.bmod x.toNat (2^(min v w)) := by
+theorem toInt_signExtend_eq_toNat_bmod (x : BitVec w) :
+    (x.signExtend v).toInt = Int.bmod x.toNat (2 ^ min v w) := by
   by_cases hv : v ≤ w
-  · simp [toInt_signExtend_of_le hv, Nat.min_eq_left hv]
+  · simp [toInt_signExtend_eq_toNat_bmod_of_le hv, Nat.min_eq_left hv]
   · simp only [Nat.not_le] at hv
-    rw [toInt_signExtend_of_lt hv, Nat.min_eq_right (by omega), toInt_eq_toNat_bmod]
+    rw [toInt_signExtend_of_le (Nat.le_of_lt hv),
+      Nat.min_eq_right (by omega), toInt_eq_toNat_bmod]
+
+theorem toInt_signExtend (x : BitVec w) :
+    (x.signExtend v).toInt = x.toInt.bmod (2 ^ min v w) := by
+  rw [toInt_signExtend_eq_toNat_bmod, BitVec.toInt_eq_toNat_bmod, Int.bmod_bmod_of_dvd]
+  exact Nat.pow_dvd_pow _ (Nat.min_le_right v w)
+
+theorem toInt_signExtend_eq_toInt_bmod_of_le (x : BitVec w) (h : v ≤ w) :
+    (x.signExtend v).toInt = x.toInt.bmod (2 ^ v) := by
+  rw [BitVec.toInt_signExtend, Nat.min_eq_left h]
+
+attribute [simp] BitVec.signExtend_eq
 
 /-! ### append -/
 
@@ -2282,11 +2324,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, getLsbD_zero, getLsbD_extractLsb',
+  simp only [getElem_shiftLeft, getElem_cast, getElem_append, getElem_zero, getElem_extractLsb',
     Nat.zero_add, Bool.if_false_left]
   by_cases hi' : i < n
   · simp [hi']
-  · simp [hi']
+  · simp [hi', show i - n < w by omega]
 
 /-! ### rev -/
 
@@ -2336,7 +2378,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 i = n then b else getLsbD x i := by
+    (cons b x)[i] = if h : i = n then b else 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
@@ -2444,7 +2486,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 i = 0 then b else x.getLsbD (i - 1) := by
+    (concat x b)[i] = if h : i = 0 then b else x[i - 1] := by
   simp only [concat, getElem_eq_testBit_toNat, getLsbD, toNat_append,
     toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
   cases i
@@ -2484,10 +2526,7 @@ 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 only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_true,
-      Bool.true_and, ite_eq_right_iff]
-    intro
-    omega
+  · simp [getElem_concat, h₀, show ¬ w = 0 by omega, show w - 1 < w by omega]
   · simp [h₀, show w = 0 by omega]
 
 @[simp] theorem toInt_concat (x : BitVec w) (b : Bool) :
@@ -2702,6 +2741,9 @@ theorem toInt_neg {x : BitVec w} :
   rw [← BitVec.zero_sub, toInt_sub]
   simp [BitVec.toInt_ofNat]
 
+theorem ofInt_neg {w : Nat} {n : Int} : BitVec.ofInt w (-n) = -BitVec.ofInt w n :=
+  eq_of_toInt_eq (by simp [toInt_neg])
+
 @[simp] theorem toFin_neg (x : BitVec n) :
     (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=
   rfl
@@ -4118,9 +4160,7 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
 
 theorem msb_eq_toInt {x : BitVec w}:
     x.msb = decide (x.toInt < 0) := by
-  by_cases h : x.msb <;>
-  · simp [h, toInt_eq_msb_cond]
-    omega
+  by_cases h : x.msb <;> simp [h, toInt_eq_msb_cond] <;> omega
 
 theorem msb_eq_toNat {x : BitVec w}:
     x.msb = decide (x.toNat ≥ 2 ^ (w - 1)) := by
@@ -4217,6 +4257,10 @@ 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/Bool.lean

@@ -539,8 +539,8 @@ theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) :
 @[simp] theorem cond_eq_false_distrib : ∀(c t f : Bool),
     (cond c t f = false) = ite (c = true) (t = false) (f = false) := by decide
 
-protected theorem cond_true  {α : Type u} {a b : α} : cond true  a b = a := cond_true  a b
-protected theorem cond_false {α : Type u} {a b : α} : cond false a b = b := cond_false a b
+protected theorem cond_true  {α : Sort u} {a b : α} : cond true  a b = a := cond_true  a b
+protected theorem cond_false {α : Sort u} {a b : α} : cond false a b = b := cond_false a b
 
 @[simp] theorem cond_true_left   : ∀(c f : Bool), cond c true f  = ( c || f) := by decide
 @[simp] theorem cond_false_left  : ∀(c f : Bool), cond c false f = (!c && f) := by decide

src/Init/Data/Fin/Lemmas.lean

@@ -45,6 +45,7 @@ theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
 theorem forall_iff {p : Fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩ :=
   ⟨fun h i hi => h ⟨i, hi⟩, fun h ⟨i, hi⟩ => h i hi⟩
 
+/-- Restatement of `Fin.mk.injEq` as an `iff`. -/
 protected theorem mk.inj_iff {n a b : Nat} {ha : a < n} {hb : b < n} :
     (⟨a, ha⟩ : Fin n) = ⟨b, hb⟩ ↔ a = b := Fin.ext_iff
 
@@ -55,6 +56,14 @@ theorem eq_mk_iff_val_eq {a : Fin n} {k : Nat} {hk : k < n} :
 
 theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 
+@[simp] theorem mk_eq_zero {n a : Nat} {ha : a < n} [NeZero n] :
+    (⟨a, ha⟩ : Fin n) = 0 ↔ a = 0 :=
+  mk.inj_iff
+
+@[simp] theorem zero_eq_mk {n a : Nat} {ha : a < n} [NeZero n] :
+    0 = (⟨a, ha⟩ : Fin n) ↔ a = 0 := by
+  simp [eq_comm]
+
 @[simp] theorem val_ofNat' (n : Nat) [NeZero n] (a : Nat) :
   (Fin.ofNat' n a).val = a % n := rfl
 

src/Init/Data/Int/Basic.lean

@@ -17,10 +17,12 @@ open Nat
 This file defines the `Int` type as well as
 
 * coercions, conversions, and compatibility with numeric literals,
-* basic arithmetic operations add/sub/mul/div/mod/pow,
+* basic arithmetic operations add/sub/mul/pow,
 * a few `Nat`-related operations such as `negOfNat` and `subNatNat`,
 * relations `<`/`≤`/`≥`/`>`, the `NonNeg` property and `min`/`max`,
 * decidability of equality, relations and `NonNeg`.
+
+Division and modulus operations are defined in `Init.Data.Int.DivMod.Basic`.
 -/
 
 /--

src/Init/Data/Int/Cooper.lean

@@ -227,33 +227,4 @@ theorem cooper_resolution_dvd_right
     · exact Int.mul_neg _ _ ▸ Int.neg_le_of_neg_le lower
     · exact Int.mul_neg _ _ ▸ Int.neg_mul _ _ ▸ dvd
 
-/--
-Left Cooper resolution of an upper and lower bound.
--/
-theorem cooper_resolution_left
-    {a b p q : Int} (a_pos : 0 < a) (b_pos : 0 < b) :
-    (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔
-    (∃ k : Int, 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p) := by
-  have h := cooper_resolution_dvd_left
-    a_pos b_pos Int.zero_lt_one (c := 1) (s := 0) (p := p) (q := q)
-  simp only [Int.mul_one, Int.one_mul, Int.mul_zero, Int.add_zero, gcd_one, Int.ofNat_one,
-    Int.ediv_one, lcm_self, Int.natAbs_of_nonneg (Int.le_of_lt a_pos), Int.one_dvd, and_true,
-    and_self] at h
-  exact h
-
-/--
-Right Cooper resolution of an upper and lower bound.
--/
-theorem cooper_resolution_right
-    {a b p q : Int} (a_pos : 0 < a) (b_pos : 0 < b) :
-    (∃ x, p ≤ a * x ∧ b * x ≤ q) ↔
-    (∃ k : Int, 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q) := by
-  have h := cooper_resolution_dvd_right
-    a_pos b_pos Int.zero_lt_one (c := 1) (s := 0) (p := p) (q := q)
-  have : ∀ k : Int, (b ∣ -k + q) ↔ (b ∣ k - q) := by
-    intro k
-    rw [← Int.dvd_neg, Int.neg_add, Int.neg_neg, Int.sub_eq_add_neg]
-  simp only [Int.mul_one, Int.one_mul, Int.mul_zero, Int.add_zero, gcd_one, Int.ofNat_one,
-    Int.ediv_one, lcm_self, Int.natAbs_of_nonneg (Int.le_of_lt b_pos), Int.one_dvd, and_true,
-    and_self, ← Int.neg_eq_neg_one_mul, this] at h
-  exact h
+end Int

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

@@ -21,25 +21,25 @@ and satisfy `x / 0 = 0` and `x % 0 = x`.
 In early versions of Lean, the typeclasses provided by `/` and `%`
 were defined in terms of `tdiv` and `tmod`, and these were named simply as `div` and `mod`.
 
-However we decided it was better to use `ediv` and `emod`,
+However we decided it was better to use `ediv` and `emod` for the default typeclass instances,
 as they are consistent with the conventions used in SMTLib, and Mathlib,
 and often mathematical reasoning is easier with these conventions.
-
 At that time, we did not rename `div` and `mod` to `tdiv` and `tmod` (along with all their lemma).
+
 In September 2024, we decided to do this rename (with deprecations in place),
 and later we intend to rename `ediv` and `emod` to `div` and `mod`, as nearly all users will only
 ever need to use these functions and their associated lemmas.
 
-In December 2024, we removed `tdiv` and `tmod`, but have not yet renamed `ediv` and `emod`.
+In December 2024, we removed `div` and `mod`, but have not yet renamed `ediv` and `emod`.
 -/
 
 /-! ### E-rounding division
-This pair satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`.
+This pair satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`.
 -/
 
 /--
-Integer division. This version of `Int.div` uses the E-rounding convention
-(euclidean division), in which `Int.emod x y` satisfies `0 ≤ mod x y < natAbs y` for `y ≠ 0`
+Integer division. This version of integer division uses the E-rounding convention
+(euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
 and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
 
 This is the function powering the `/` notation on integers.
@@ -71,7 +71,7 @@ def ediv : (@& Int) → (@& Int) → Int
   | -[m+1],  -[n+1]  => ofNat (succ (m / succ n))
 
 /--
-Integer modulus. This version of `Int.mod` uses the E-rounding convention
+Integer modulus. This version of integer modulus uses the E-rounding convention
 (euclidean division), in which `Int.emod x y` satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`
 and `Int.ediv` is the unique function satisfying `emod x y + (ediv x y) * y = x`.
 
@@ -112,9 +112,10 @@ 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
 
@@ -228,7 +229,7 @@ def fdiv : Int → Int → Int
   | -[m+1],  -[n+1]  => ofNat (succ m / succ n)
 
 /--
-Integer modulus. This version of `Int.mod` uses the F-rounding convention
+Integer modulus. This version of integer modulus uses the F-rounding convention
 (flooring division), in which `Int.fdiv x y` satisfies `fdiv x y = floor (x / y)`
 and `Int.fmod` is the unique function satisfying `fmod x y + (fdiv x y) * y = x`.
 
@@ -267,11 +268,14 @@ Balanced mod (and balanced div) are a division and modulus pair such
 that `b * (Int.bdiv a b) + Int.bmod a b = a` and
 `-b/2 ≤ Int.bmod a b < b/2` for all `a : Int` and `b > 0`.
 
-This is used in Omega as well as signed bitvectors.
+Note that unlike `emod`, `fmod`, and `tmod`,
+`bmod` takes a natural number as the second argument, rather than an integer.
+
+This function is used in `omega` as well as signed bitvectors.
 -/
 
 /--
-Balanced modulus.  This version of Integer modulus uses the
+Balanced modulus.  This version of integer modulus uses the
 balanced rounding convention, which guarantees that
 `-m/2 ≤ bmod x m < m/2` for `m ≠ 0` and `bmod x m` is congruent
 to `x` modulo `m`.

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

@@ -18,7 +18,7 @@ open Nat (succ)
 
 namespace Int
 
--- /-! ### dvd  -/
+/-! ### dvd  -/
 
 protected theorem dvd_def (a b : Int) : (a ∣ b) = Exists (fun c => b = a * c) := rfl
 
@@ -67,7 +67,7 @@ protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
 theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
   rw [← natAbs_dvd_natAbs, natAbs_ofNat]
 
-/-! ### *div zero  -/
+/-! ### ediv zero  -/
 
 @[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
   | ofNat _ => show ofNat _ = _ by simp
@@ -77,7 +77,7 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natA
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
-/-! ### mod zero -/
+/-! ### emod zero -/
 
 @[simp] theorem zero_emod (b : Int) : 0 % b = 0 := rfl
 
@@ -89,7 +89,6 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natA
 
 @[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
 
-
 /-! ### mod definitions -/
 
 theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
@@ -106,12 +105,17 @@ where
       ← Int.neg_neg (_-_), Int.neg_sub, Int.sub_sub_self, Int.add_right_comm]
     exact congrArg (fun x => -(ofNat x + 1)) (Nat.mod_add_div ..)
 
+/-- Variant of `emod_add_ediv` with the multiplication written the other way around. -/
 theorem emod_add_ediv' (a b : Int) : a % b + a / b * b = a := by
   rw [Int.mul_comm]; exact emod_add_ediv ..
 
 theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
   rw [Int.add_comm]; exact emod_add_ediv ..
 
+/-- Variant of `ediv_add_emod` with the multiplication written the other way around. -/
+theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
+  rw [Int.mul_comm]; exact ediv_add_emod ..
+
 theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
   rw [← Int.add_sub_cancel (a % b), emod_add_ediv]
 
@@ -154,6 +158,10 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
       apply congrArg negSucc
       rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
 
+theorem add_mul_ediv_left (a : Int) {b : Int}
+    (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c :=
+  Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H
+
 theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
   if h : c = 0 then by simp [h] else by
     let ⟨k, hk⟩ := H
@@ -170,7 +178,7 @@ theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c +
 @[simp] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
   Int.mul_comm .. ▸ Int.mul_ediv_cancel _ H
 
-theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0 := by
+theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a := by
   rw [Int.div_def]
   match b, h with
   | Int.ofNat (b+1), _ =>
@@ -178,6 +186,9 @@ theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0
     norm_cast
     simp
 
+@[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
+abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos
+
 /-! ### emod -/
 
 theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b
@@ -189,16 +200,6 @@ theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
   | ofNat _, _, ⟨_, rfl⟩ => ofNat_lt.2 (Nat.mod_lt _ (Nat.succ_pos _))
   | -[_+1], _, ⟨_, rfl⟩ => Int.sub_lt_self _ (ofNat_lt.2 <| Nat.succ_pos _)
 
-theorem mul_ediv_self_le {x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x :=
-  calc k * (x / k)
-    _ ≤ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
-    _ = x                   := ediv_add_emod _ _
-
-theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
-  calc x
-    _ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
-    _ < k * (x / k) + k     := Int.add_lt_add_left (emod_lt_of_pos x h) _
-
 @[simp] theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
   if cz : c = 0 then by
     rw [cz, Int.mul_zero, Int.add_zero]
@@ -300,6 +301,24 @@ 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⟩)
+
+/-! ### `/` and ordering -/
+
+theorem mul_ediv_self_le {x k : Int} (h : k ≠ 0) : k * (x / k) ≤ x :=
+  calc k * (x / k)
+    _ ≤ k * (x / k) + x % k := Int.le_add_of_nonneg_right (emod_nonneg x h)
+    _ = x                   := ediv_add_emod _ _
+
+theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
+  calc x
+    _ = k * (x / k) + x % k := (ediv_add_emod _ _).symm
+    _ < k * (x / k) + k     := Int.add_lt_add_left (emod_lt_of_pos x h) _
+
 /-! ### bmod -/
 
 @[simp] theorem bmod_emod : bmod x m % m = x % m := by

src/Init/Data/Int/Lemmas.lean

@@ -78,7 +78,7 @@ theorem negSucc_eq (n : Nat) : -[n+1] = -((n : Int) + 1) := rfl
   | succ _ => rfl
   | -[_+1] => rfl
 
-protected theorem neg_inj {a b : Int} : -a = -b ↔ a = b :=
+@[simp] protected theorem neg_inj {a b : Int} : -a = -b ↔ a = b :=
   ⟨fun h => by rw [← Int.neg_neg a, ← Int.neg_neg b, h], congrArg _⟩
 
 @[simp] protected theorem neg_eq_zero : -a = 0 ↔ a = 0 := Int.neg_inj (b := 0)
@@ -341,6 +341,20 @@ 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/LemmasAux.lean

@@ -46,4 +46,35 @@ theorem bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) :
   · rw [Int.emod_eq_of_lt xpos (by omega)]; omega
   · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega
 
+@[simp] theorem natCast_le_zero : {n : Nat} → (n : Int) ≤ 0 ↔ n = 0 := by omega
+
+@[simp] theorem toNat_eq_zero : ∀ {n : Int}, n.toNat = 0 ↔ n ≤ 0 := by omega
+
+theorem eq_zero_of_dvd_of_natAbs_lt_natAbs {d n : Int} (h : d ∣ n) (h₁ : n.natAbs < d.natAbs) :
+    n = 0 := by
+  obtain ⟨a, rfl⟩ := h
+  rw [natAbs_mul] at h₁
+  suffices ¬ 0 < a.natAbs by simp [Int.natAbs_eq_zero.1 (Nat.eq_zero_of_not_pos this)]
+  exact fun h => Nat.lt_irrefl _ (Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_right d.natAbs h) h₁)
+
+theorem bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(m / 2) ≤ n) (hn : n < (m + 1) / 2) :
+    n.bmod m = n := by
+  rw [← Int.sub_eq_zero]
+  have := le_bmod (x := n) (m := m) (by omega)
+  have := bmod_lt (x := n) (m := m) (by omega)
+  apply eq_zero_of_dvd_of_natAbs_lt_natAbs Int.dvd_bmod_sub_self
+  omega
+
+protected theorem sub_eq_iff_eq_add {b a c : Int} : a - b = c ↔ a = c + b := by omega
+protected theorem sub_eq_iff_eq_add' {b a c : Int} : a - b = c ↔ a = b + c := by omega
+
+theorem bmod_bmod_of_dvd {a : Int} {n m : Nat} (hnm : n ∣ m) :
+    (a.bmod m).bmod n = a.bmod n := by
+  rw [← Int.sub_eq_iff_eq_add.2 (bmod_add_bdiv a m).symm]
+  obtain ⟨k, rfl⟩ := hnm
+  simp [Int.mul_assoc]
+
+@[simp] theorem toNat_le {m : Int} {n : Nat} : m.toNat ≤ n ↔ m ≤ n := by omega
+@[simp] theorem toNat_lt' {m : Int} {n : Nat} (hn : 0 < n) : m.toNat < n ↔ m < n := by omega
+
 end Int

src/Init/Data/Int/Order.lean

@@ -133,12 +133,15 @@ protected theorem lt_of_not_ge {a b : Int} (h : ¬a ≤ b) : b < a :=
 protected theorem not_le_of_gt {a b : Int} (h : b < a) : ¬a ≤ b :=
   (Int.lt_iff_le_not_le.mp h).right
 
-protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
+@[simp] protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
   Iff.intro Int.lt_of_not_ge Int.not_le_of_gt
 
-protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
+@[simp] protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
   by rw [← Int.not_le, Decidable.not_not]
 
+protected theorem le_of_not_gt {a b : Int} (h : ¬ a > b) : a ≤ b :=
+  Int.not_lt.mp h
+
 protected theorem lt_trichotomy (a b : Int) : a < b ∨ a = b ∨ b < a :=
   if eq : a = b then .inr <| .inl eq else
   if le : a ≤ b then .inl <| Int.lt_iff_le_and_ne.2 ⟨le, eq⟩ else
@@ -938,6 +941,22 @@ protected theorem mul_self_le_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a ≤ b)
 protected theorem mul_self_lt_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b :=
   Int.mul_lt_mul' (Int.le_of_lt h2) h2 h1 (Int.lt_of_le_of_lt h1 h2)
 
+protected theorem nonneg_of_mul_nonneg_left {a b : Int}
+    (h : 0 ≤ a * b) (hb : 0 < b) : 0 ≤ a :=
+  Int.le_of_not_gt fun ha => Int.not_le_of_gt (Int.mul_neg_of_neg_of_pos ha hb) h
+
+protected theorem nonneg_of_mul_nonneg_right {a b : Int}
+    (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b :=
+  Int.le_of_not_gt fun hb => Int.not_le_of_gt (Int.mul_neg_of_pos_of_neg ha hb) h
+
+protected theorem nonpos_of_mul_nonpos_left {a b : Int}
+    (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0 :=
+  Int.le_of_not_gt fun ha : a > 0 => Int.not_le_of_gt (Int.mul_pos ha hb) h
+
+protected theorem nonpos_of_mul_nonpos_right {a b : Int}
+    (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0 :=
+  Int.le_of_not_gt fun hb : b > 0 => Int.not_le_of_gt (Int.mul_pos ha hb) h
+
 /- ## sign -/
 
 @[simp] theorem sign_zero : sign 0 = 0 := rfl
@@ -1011,11 +1030,22 @@ 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]
 
-theorem mul_sign : ∀ i : Int, i * sign i = natAbs i
+@[simp] theorem mul_sign_self : ∀ 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]
+
+theorem sign_trichotomy (a : Int) : sign a = 1 ∨ sign a = 0 ∨ sign a = -1 := by
+  match a with
+  | 0 => simp
+  | .ofNat (_ + 1) => simp
+  | .negSucc _ => simp
+
 /- ## 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, length_pmap, length_eq_zero]
+  rw [← length_eq_zero_iff, length_pmap, length_eq_zero_iff]
 
 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
@@ -662,6 +662,10 @@ def unattach {α : Type _} {p : α → Prop} (l : List { x // p x }) : List α :
 @[simp] theorem unattach_cons {p : α → Prop} {a : { x // p x }} {l : List { x // p x }} :
   (a :: l).unattach = a.val :: l.unattach := rfl
 
+@[simp] theorem mem_unattach {p : α → Prop} {l : List { x // p x }} {a} :
+    a ∈ l.unattach ↔ ∃ h : p a, ⟨a, h⟩ ∈ l := by
+  simp only [unattach, mem_map, Subtype.exists, exists_and_right, exists_eq_right]
+
 @[simp] theorem length_unattach {p : α → Prop} {l : List { x // p x }} :
     l.unattach.length = l.length := by
   unfold unattach
@@ -766,6 +770,16 @@ and simplifies these to the function directly taking the value.
     simp [hf, find?_cons]
     split <;> simp [ih]
 
+@[simp] theorem all_subtype {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.all f = l.unattach.all g := by
+  simp [all_eq, hf]
+
+@[simp] theorem any_subtype {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool}
+    (hf : ∀ x h, f ⟨x, h⟩ = g x) :
+    l.any f = l.unattach.any g := by
+  simp [any_eq, hf]
+
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
 @[simp] theorem unattach_filter {p : α → Prop} {l : List { x // p x }}

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
 
@@ -1758,10 +1758,10 @@ where
 
 /-! ### removeAll -/
 
-/-- `O(|xs|)`. Computes the "set difference" of lists,
+/-- `O(|xs| * |ys|)`. Computes the "set difference" of lists,
 by filtering out all elements of `xs` which are also in `ys`.
 * `removeAll [1, 1, 5, 1, 2, 4, 5] [1, 2, 2] = [5, 4, 5]`
- -/
+-/
 def removeAll [BEq α] (xs ys : List α) : List α :=
   xs.filter (fun x => !ys.elem x)
 

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
 
@@ -212,6 +212,7 @@ def mapMono (as : List α) (f : α → α) : List α :=
 
 /-! ## Additional lemmas required for bootstrapping `Array`. -/
 
+@[simp]
 theorem getElem_append_left {as bs : List α} (h : i < as.length) {h' : i < (as ++ bs).length} :
     (as ++ bs)[i] = as[i] := by
   induction as generalizing i with
@@ -221,6 +222,7 @@ theorem getElem_append_left {as bs : List α} (h : i < as.length) {h' : i < (as
     | zero => rfl
     | succ i => apply ih
 
+@[simp]
 theorem getElem_append_right {as bs : List α} {i : Nat} (h₁ : as.length ≤ i) {h₂} :
     (as ++ bs)[i]'h₂ =
       bs[i - as.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) := by

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, filter_eq_nil_iff]
+  simp only [countP_eq_length_filter, length_eq_zero_iff, 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] at h
+  · simp only [any_eq_true, length_eq_zero_iff] 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,47 +514,6 @@ 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 α) :
@@ -976,6 +935,71 @@ 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.
@@ -1035,6 +1059,36 @@ 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.
@@ -1060,12 +1114,6 @@ 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,9 +96,15 @@ 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 : length l = 0 ↔ l = [] :=
+@[simp] theorem length_eq_zero_iff : 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 _
 
@@ -123,12 +129,21 @@ theorem exists_cons_of_length_eq_add_one :
     ∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
   | _::_, _ => ⟨_, _, rfl⟩
 
-theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
-  Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)
+theorem length_pos_iff {l : List α} : 0 < length l ↔ l ≠ [] :=
+  Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero_iff)
 
-theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
+@[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] :=
   ⟨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
@@ -284,7 +299,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.mp h) :=
+theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos_iff.mp h) :=
   match l, h with
   | _ :: _, _ => rfl
 
@@ -375,7 +390,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.2 h)
+  exists_mem_of_length_pos (length_pos_iff.2 h)
 
 theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l := by
   cases l <;> simp [-not_or]
@@ -533,7 +548,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]
+  rw [isEmpty_iff, length_eq_zero_iff]
 
 /-! ### any / all -/
 
@@ -910,13 +925,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.mpr h) := by
+theorem head_eq_getElem (l : List α) (h : l ≠ []) : head l h = l[0]'(length_pos_iff.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] using h) := by
+    l[0] = head l (by simpa [length_pos_iff] using h) := by
   cases l with
   | nil => simp at h
   | cons _ _ => simp
@@ -1003,7 +1018,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.mpr h)
+    exact Nat.lt_add_of_pos_left (length_pos_iff.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
@@ -2883,7 +2898,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` is in `Init.Data.List.Nat.Basic`.
+-- `length_leftpad` and `length_rightpad` are in `Init.Data.List.Nat.Basic`.
 
 theorem leftpad_prefix (n : Nat) (a : α) (l : List α) :
     replicate (n - length l) a <+: leftpad n a l := by
@@ -3071,8 +3086,12 @@ 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 {l : List α} (h : !l.elem a) : l.replace a b = l := by
-  induction l <;> simp_all [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 length_replace {l : List α} : (l.replace a b).length = l.length := by
   induction l with
@@ -3155,7 +3174,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 {a b c : α} (h : !b == a) :
+@[simp] theorem replace_replicate_ne [LawfulBEq α] {a b c : α} (h : !b == a) :
     (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all
@@ -3417,7 +3436,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.mp h)
+theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos_iff.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,10 +44,42 @@ theorem tail_dropLast (l : List α) : tail (dropLast l) = dropLast (tail l) := b
 
 /-! ### filter -/
 
-theorem length_filter_lt_length_iff_exists {l} :
-    length (filter p l) < length l ↔ ∃ x ∈ l, ¬p x := by
+@[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 := fun x => ¬p x)
+    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
 
 /-! ### reverse -/
 
@@ -63,10 +95,18 @@ 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 leftpad_length (n : Nat) (a : α) (l : List α) :
+theorem length_leftpad (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, true_and, append_nil]
+    simp_all only [Nat.add_zero, length_eq_zero_iff, 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, true_and, append_nil]
+    simp_all only [Nat.zero_add, length_eq_zero_iff, 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 j : Nat, take i (replicate j a) = replicate (min i j) a
+@[simp] theorem take_replicate (a : α) : ∀ i n : Nat, take i (replicate n a) = replicate (min i n) a
   | n, 0 => by simp [Nat.min_zero]
   | 0, m => by simp [Nat.zero_min]
   | succ n, succ m => by simp [replicate_succ, succ_min_succ, take_replicate]
 
-@[simp] theorem drop_replicate (a : α) : ∀ i j : Nat, drop i (replicate j a) = replicate (j - i) a
+@[simp] theorem drop_replicate (a : α) : ∀ i n : Nat, drop i (replicate n a) = replicate (n - i) a
   | n, 0 => by simp
   | 0, m => by simp
   | succ n, succ m => by simp [replicate_succ, succ_sub_succ, drop_replicate]

src/Init/Data/List/Notation.lean

@@ -11,8 +11,8 @@ import Init.Data.Nat.Div.Basic
 -/
 
 set_option linter.missingDocs true -- keep it documented
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Decidable List
 

src/Init/Data/List/OfFn.lean

@@ -11,8 +11,8 @@ import Init.Data.Fin.Fold
 # Theorems about `List.ofFn`
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Pairwise.lean

@@ -11,8 +11,8 @@ import Init.Data.List.Attach
 # Lemmas about `List.Pairwise` and `List.Nodup`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Perm.lean

@@ -18,8 +18,8 @@ another.
 The notation `~` is used for permutation equivalence.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open Nat
 

src/Init/Data/List/Range.lean

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

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

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

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

@@ -31,8 +31,8 @@ as long as such improvements are carefully validated by benchmarking,
 they can be done without changing the theory, as long as a `@[csimp]` lemma is provided.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 open List
 

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

@@ -21,8 +21,8 @@ import Init.Data.Bool
 
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/Sublist.lean

@@ -11,8 +11,8 @@ import Init.Data.List.TakeDrop
 # Lemmas about `List.Subset`, `List.Sublist`, `List.IsPrefix`, `List.IsSuffix`, and `List.IsInfix`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 

src/Init/Data/List/TakeDrop.lean

@@ -10,8 +10,8 @@ import Init.Data.List.Lemmas
 # Lemmas about `List.take` and `List.drop`.
 -/
 
--- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace List
 
@@ -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.1 (length_drop .. ▸ Nat.sub_eq_zero_of_le h)
+  length_eq_zero_iff.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,6 +44,16 @@ 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]
@@ -77,6 +87,21 @@ 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
 
@@ -514,8 +539,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
 
-@[deprecated toArray_replicate (since := "2024-12-13")]
-abbrev _root_.Array.mkArray_eq_toArray_replicate := @toArray_replicate
+theorem _root_.Array.mkArray_eq_toArray_replicate : mkArray n v = (List.replicate n v).toArray := by
+  simp
 
 @[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
 
@@ -633,4 +658,46 @@ 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,6 +6,7 @@ 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.
@@ -62,4 +63,53 @@ 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,3 +40,20 @@ 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/OfScientific.lean

@@ -80,9 +80,9 @@ instance : OfScientific Float32 where
 def Float32.ofNat (n : Nat) : Float32 :=
   OfScientific.ofScientific n false 0
 
-def Float32.ofInt : Int → Float
-  | Int.ofNat n => Float.ofNat n
-  | Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))
+def Float32.ofInt : Int → Float32
+  | Int.ofNat n => Float32.ofNat n
+  | Int.negSucc n => Float32.neg (Float32.ofNat (Nat.succ n))
 
 instance : OfNat Float32 n   := ⟨Float32.ofNat n⟩
 

src/Init/Data/Option/Basic.lean

@@ -101,6 +101,12 @@ This is similar to `<|>`/`orElse`, but it is strict in the second argument. -/
   | some x,   some y => r x y
   | _, _             => False
 
+@[inline] protected def le (r : α → β → Prop) : Option α → Option β → Prop
+  | none,   some _ => True
+  | none,   none   => True
+  | some _, none   => False
+  | some x, some y => r x y
+
 instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)
   | none,   some _ => isTrue  trivial
   | some x, some y => s x y
@@ -217,18 +223,24 @@ instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where
 @[simp] theorem any_none : Option.any p none = false := rfl
 @[simp] theorem any_some : Option.any p (some x) = p x := rfl
 
-/-- The minimum of two optional values. -/
+/--
+The minimum of two optional values.
+
+Note this treats `none` as the least element,
+so `min none x = min x none = none` for all `x : Option α`.
+Prior to nightly-2025-02-27, we instead had `min none (some x) = min (some x) none = some x`.
+-/
 protected def min [Min α] : Option α → Option α → Option α
   | some x, some y => some (Min.min x y)
-  | some x, none => some x
-  | none, some y => some y
+  | some _, none => none
+  | none, some _ => none
   | none, none => none
 
 instance [Min α] : Min (Option α) where min := Option.min
 
 @[simp] theorem min_some_some [Min α] {a b : α} : min (some a) (some b) = some (min a b) := rfl
-@[simp] theorem min_some_none [Min α] {a : α} : min (some a) none = some a := rfl
-@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = some b := rfl
+@[simp] theorem min_some_none [Min α] {a : α} : min (some a) none = none := rfl
+@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = none := rfl
 @[simp] theorem min_none_none [Min α] : min (none : Option α) none = none := rfl
 
 /-- The maximum of two optional values. -/
@@ -251,6 +263,9 @@ end Option
 instance [LT α] : LT (Option α) where
   lt := Option.lt (· < ·)
 
+instance [LE α] : LE (Option α) where
+  le := Option.le (· ≤ ·)
+
 @[always_inline]
 instance : Functor Option where
   map := Option.map

src/Init/Data/Option/Lemmas.lean

@@ -654,6 +654,11 @@ 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
@@ -668,4 +673,80 @@ theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H)
        o.pelim g (fun a h => g' (f a (H a h))) := by
   cases o <;> simp
 
+/-! ### LT and LE -/
+
+@[simp] theorem not_lt_none [LT α] {a : Option α} : ¬ a < none := by cases a <;> simp [LT.lt, Option.lt]
+@[simp] theorem none_lt_some [LT α] {a : α} : none < some a := by simp [LT.lt, Option.lt]
+@[simp] theorem some_lt_some [LT α] {a b : α} : some a < some b ↔ a < b := by simp [LT.lt, Option.lt]
+
+@[simp] theorem none_le [LE α] {a : Option α} : none ≤ a := by cases a <;> simp [LE.le, Option.le]
+@[simp] theorem not_some_le_none [LE α] {a : α} : ¬ some a ≤ none := by simp [LE.le, Option.le]
+@[simp] theorem some_le_some [LE α] {a b : α} : some a ≤ some b ↔ a ≤ b := by simp [LE.le, Option.le]
+
+/-! ### min and max -/
+
+theorem min_eq_left [LE α] [Min α] (min_eq_left : ∀ x y : α, x ≤ y → min x y = x)
+    {a b : Option α} (h : a ≤ b) : min a b = a := by
+  cases a <;> cases b <;> simp_all
+
+theorem min_eq_right [LE α] [Min α] (min_eq_right : ∀ x y : α, y ≤ x → min x y = y)
+    {a b : Option α} (h : b ≤ a) : min a b = b := by
+  cases a <;> cases b <;> simp_all
+
+theorem min_eq_left_of_lt [LT α] [Min α] (min_eq_left : ∀ x y : α, x < y → min x y = x)
+    {a b : Option α} (h : a < b) : min a b = a := by
+  cases a <;> cases b <;> simp_all
+
+theorem min_eq_right_of_lt [LT α] [Min α] (min_eq_right : ∀ x y : α, y < x → min x y = y)
+    {a b : Option α} (h : b < a) : min a b = b := by
+  cases a <;> cases b <;> simp_all
+
+theorem min_eq_or [LE α] [Min α] (min_eq_or : ∀ x y : α, min x y = x ∨ min x y = y)
+    {a b : Option α} : min a b = a ∨ min a b = b := by
+  cases a <;> cases b <;> simp_all
+
+theorem min_le_left [LE α] [Min α] (min_le_left : ∀ x y : α, min x y ≤ x)
+    {a b : Option α} : min a b ≤ a := by
+  cases a <;> cases b <;> simp_all
+
+theorem min_le_right [LE α] [Min α] (min_le_right : ∀ x y : α, min x y ≤ y)
+    {a b : Option α} : min a b ≤ b := by
+  cases a <;> cases b <;> simp_all
+
+theorem le_min [LE α] [Min α] (le_min : ∀ x y z : α, x ≤ min y z ↔ x ≤ y ∧ x ≤ z)
+    {a b c : Option α} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c := by
+  cases a <;> cases b <;> cases c <;> simp_all
+
+theorem max_eq_left [LE α] [Max α] (max_eq_left : ∀ x y : α, x ≤ y → max x y = y)
+    {a b : Option α} (h : a ≤ b) : max a b = b := by
+  cases a <;> cases b <;> simp_all
+
+theorem max_eq_right [LE α] [Max α] (max_eq_right : ∀ x y : α, y ≤ x → max x y = x)
+    {a b : Option α} (h : b ≤ a) : max a b = a := by
+  cases a <;> cases b <;> simp_all
+
+theorem max_eq_left_of_lt [LT α] [Max α] (max_eq_left : ∀ x y : α, x < y → max x y = y)
+    {a b : Option α} (h : a < b) : max a b = b := by
+  cases a <;> cases b <;> simp_all
+
+theorem max_eq_right_of_lt [LT α] [Max α] (max_eq_right : ∀ x y : α, y < x → max x y = x)
+    {a b : Option α} (h : b < a) : max a b = a := by
+  cases a <;> cases b <;> simp_all
+
+theorem max_eq_or [LE α] [Max α] (max_eq_or : ∀ x y : α, max x y = x ∨ max x y = y)
+    {a b : Option α} : max a b = a ∨ max a b = b := by
+  cases a <;> cases b <;> simp_all
+
+theorem left_le_max [LE α] [Max α] (le_refl : ∀ x : α, x ≤ x) (left_le_max : ∀ x y : α, x ≤ max x y)
+    {a b : Option α} : a ≤ max a b := by
+  cases a <;> cases b <;> simp_all
+
+theorem right_le_max [LE α] [Max α] (le_refl : ∀ x : α, x ≤ x) (right_le_max : ∀ x y : α, y ≤ max x y)
+    {a b : Option α} : b ≤ max a b := by
+  cases a <;> cases b <;> simp_all
+
+theorem max_le [LE α] [Max α] (max_le : ∀ x y z : α, max x y ≤ z ↔ x ≤ z ∧ y ≤ z)
+    {a b c : Option α} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c := by
+  cases a <;> cases b <;> cases c <;> simp_all
+
 end Option

src/Init/Data/SInt.lean

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