copy across some Find API to Array

.github/workflows/awaiting-mathlib.yml

@@ -1,20 +0,0 @@
-name: Check awaiting-mathlib label
-
-on:
-  merge_group:
-  pull_request:
-    types: [opened, labeled]
-
-jobs:
-  check-awaiting-mathlib:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Check awaiting-mathlib label
-        if: github.event_name == 'pull_request'
-        uses: actions/github-script@v7
-        with:
-          script: |
-            const { labels } = context.payload.pull_request;
-            if (labels.some(label => label.name == "awaiting-mathlib") && !labels.some(label => label.name == "builds-mathlib")) {
-              core.setFailed('PR is marked "awaiting-mathlib" but "builds-mathlib" label has not been applied yet by the bot');
-            }

.github/workflows/ci.yml

@@ -204,8 +204,7 @@ jobs:
                 "os": "macos-14",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
-                // special cased below
-                // "check-level": 0,
+                "check-level": 0,
                 "shell": "bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@@ -261,21 +260,8 @@ jobs:
               //   "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
               // }
             ];
-            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            const isPr = "${{ github.event_name }}" == "pull_request";
-            const filter = (job) => {
-              if (job["name"] === "macOS aarch64") {
-                // Special handling for MacOS aarch64, we want:
-                // 1. To run it in PRs so Mac devs get PR toolchains
-                // 2. To skip it in merge queues as it takes longer than the Linux build and adds
-                //    little value in the merge queue
-                // 3. To run it in release (obviously)
-                return isPr || level >= 2;
-              } else {
-                return level >= job["check-level"];
-              }
-            };
-            return matrix.filter(filter);
+            console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
+            return matrix.filter((job) => level >= job["check-level"])
 
   build:
     needs: [configure]

.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@v9 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v8 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -155,20 +155,6 @@ 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"
 
@@ -215,12 +201,7 @@ jobs:
             else
               echo "The message already exists in the comment body."
             fi
-
-            if [[ "$FORCE_CI" == "true" ]]; then
-              echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
-            else
-              echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
-            fi
+            echo "mathlib_ready=false" >> "$GITHUB_OUTPUT"
           else
             echo "mathlib_ready=true" >> "$GITHUB_OUTPUT"
           fi
@@ -271,7 +252,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 "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
+            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' tag at Batteries. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 
@@ -335,7 +316,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 "Couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
+            echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
             BASE=nightly-testing
           fi
 

CMakeLists.txt

@@ -47,11 +47,10 @@ 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-2.1.2
+      GIT_TAG rel-1.9.5
       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}

flake.lock

@@ -36,17 +36,17 @@
     },
     "nixpkgs-cadical": {
       "locked": {
-        "lastModified": 1740791350,
-        "narHash": "sha256-igS2Z4tVw5W/x3lCZeeadt0vcU9fxtetZ/RyrqsCRQ0=",
+        "lastModified": 1722221733,
+        "narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
+        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
         "type": "github"
       },
       "original": {
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
+        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
         "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 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";
+  # for cadical 1.9.5; sync with CMakeLists.txt
+  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/12bf09802d77264e441f48e25459c10c93eada2e";
   inputs.flake-utils.url = "github:numtide/flake-utils";
 
   outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system:

script/prepare-llvm-mingw.sh

@@ -25,10 +25,7 @@ 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);
-// 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
+__declspec(dllimport) __stdcall unsigned int SetErrorMode(unsigned int uMode);' > stage1/include/clang/windows.h
 # COFF dependencies
 cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/
 # runtime

script/release_notes.py

@@ -65,21 +65,20 @@ 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 commit_types():
-            if first_line.startswith(f'{commit_type}:'):
-                counts[commit_type] += 1
+        for commit_type in ['feat:', 'fix:', 'refactor:', 'doc:', 'chore:']:
+            if first_line.startswith(commit_type):
+                counts[commit_type.rstrip(':')] += 1
                 break
     
     return counts
@@ -159,9 +158,8 @@ 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"{counts['perf']} performance improvements, {counts['test']} improvements to the test suite "
-          f"and {counts['style'] + counts['chore']} other changes.\n")
+          f"there were {counts['refactor']} refactoring changes, {counts['doc']} documentation improvements "
+          f"and {counts['chore']} chores.\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 19)
+set(LEAN_VERSION_MINOR 18)
 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'")

src/Init/Control/Id.lean

@@ -10,28 +10,6 @@ import Init.Core
 
 universe u
 
-/--
-The identity function on types, used primarily for its `Monad` instance.
-
-The identity monad is useful together with monad transformers to construct monads for particular
-purposes. Additionally, it can be used with `do`-notation in order to use control structures such as
-local mutability, `for`-loops, and early returns in code that does not otherwise use monads.
-
-Examples:
-```lean example
-def containsFive (xs : List Nat) : Bool := Id.run do
-  for x in xs do
-    if x == 5 then return true
-  return false
-```
-
-```lean example
-#eval containsFive [1, 3, 5, 7]
-```
-```output
-true
-```
--/
 def Id (type : Type u) : Type u := type
 
 namespace Id
@@ -42,18 +20,9 @@ instance : Monad Id where
   bind x f := f x
   map f x := f x
 
-/--
-The identity monad has a `bind` operator.
--/
 def hasBind : Bind Id :=
   inferInstance
 
-/--
-Runs a computation in the identity monad.
-
-This function is the identity function. Because its parameter has type `Id α`, it causes
-`do`-notation in its arguments to use the `Monad Id` instance.
--/
 @[always_inline, inline]
 protected def run (x : Id α) : α := x
 

src/Init/Core.lean

@@ -226,9 +226,9 @@ structure PSigma {α : Sort u} (β : α → Sort v) where
   (This will usually require a type ascription to determine `β`
   since it is not determined from `a` and `b` alone.) -/
   mk ::
-  /-- The first component of a dependent pair. If `p : @PSigma α β` then `p.1 : α`. -/
+  /-- The first component of a dependent pair. If `p : @Sigma α β` then `p.1 : α`. -/
   fst : α
-  /-- The second component of a dependent pair. If `p : PSigma β` then `p.2 : β p.1`. -/
+  /-- The second component of a dependent pair. If `p : Sigma β` then `p.2 : β p.1`. -/
   snd : β fst
 
 /--
@@ -1925,6 +1925,10 @@ protected abbrev recOnSubsingleton₂
 end
 end Quotient
 
+section
+variable {α : Type u}
+variable (r : α → α → Prop)
+
 instance Quotient.decidableEq {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)]
     : DecidableEq (Quotient s) :=
   fun (q₁ q₂ : Quotient s) =>

src/Init/Data/Array/Attach.lean

@@ -555,10 +555,6 @@ 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
@@ -680,20 +676,6 @@ 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

@@ -144,8 +144,6 @@ 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
@@ -254,7 +252,7 @@ instance [BEq α] : BEq (Array α) :=
 ```
 ofFn f = #[f 0, f 1, ... , f(n - 1)]
 ``` -/
-def ofFn {n} (f : Fin n → α) : Array α := go 0 (emptyWithCapacity n) where
+def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
   @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
   go (i : Nat) (acc : Array α) : Array α :=
@@ -505,7 +503,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
       else
         pure bs
   decreasing_by simp_wf; decreasing_trivial_pre_omega
-  map 0 (emptyWithCapacity as.size)
+  map 0 (mkEmpty as.size)
 
 @[deprecated mapM (since := "2024-11-11")] abbrev sequenceMap := @mapM
 
@@ -522,7 +520,7 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
       map i (j+1) this (bs.push (← f j as[j] j_lt))
-  map as.size 0 rfl (emptyWithCapacity as.size)
+  map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=

src/Init/Data/Array/Count.lean

@@ -23,18 +23,6 @@ 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
@@ -162,13 +150,6 @@ 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/Erase.lean

@@ -282,10 +282,6 @@ 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/MapIdx.lean

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

src/Init/Data/Array/Monadic.lean

@@ -23,13 +23,6 @@ open Nat
 
 /-! ### mapM -/
 
-@[simp] theorem mapM_pure [Monad m] [LawfulMonad m] (xs : Array α) (f : α → β) :
-    xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by
-  induction xs; simp_all
-
-@[simp] theorem mapM_id {xs : Array α} {f : α → Id β} : xs.mapM f = xs.map f :=
-  mapM_pure _ _
-
 @[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⟩
@@ -231,32 +224,6 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs⟩
   simp
 
-/-! ### allM and anyM -/
-
-@[simp] theorem anyM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Array α) :
-    xs.anyM (m := m) (pure <| p ·) = pure (xs.any p) := by
-  cases xs
-  simp
-
-@[simp] theorem allM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Array α) :
-    xs.allM (m := m) (pure <| p ·) = pure (xs.all p) := by
-  cases xs
-  simp
-
-/-! ### findM? and findSomeM? -/
-
-@[simp]
-theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Array α) :
-    findM? (m := m) (pure <| p ·) xs = pure (xs.find? p) := by
-  cases xs
-  simp
-
-@[simp]
-theorem findSomeM?_pure [Monad m] [LawfulMonad m] (f : α → Option β) (xs : Array α) :
-    findSomeM? (m := m) (pure <| f ·) xs = pure (xs.findSome? f) := by
-  cases xs
-  simp
-
 end Array
 
 namespace List
@@ -387,12 +354,12 @@ and simplifies these to the function directly taking the value.
   simp
   rw [List.foldlM_subtype hf]
 
-@[wf_preprocess] theorem foldlM_wfParam [Monad m] (xs : Array α) (f : β → α → m β) (init : β) :
-    (wfParam xs).foldlM f init = xs.attach.unattach.foldlM f init := by
+@[wf_preprocess] theorem foldlM_wfParam [Monad m] (xs : Array α) (f : β → α → m β) :
+    (wfParam xs).foldlM f = xs.attach.unattach.foldlM f := by
   simp [wfParam]
 
-@[wf_preprocess] theorem foldlM_unattach [Monad m] (P : α → Prop) (xs : Array (Subtype P)) (f : β → α → m β) (init : β) :
-    xs.unattach.foldlM f init = xs.foldlM (init := init) fun b ⟨x, h⟩ =>
+@[wf_preprocess] theorem foldlM_unattach [Monad m] (P : α → Prop) (xs : Array (Subtype P)) (f : β → α → m β) :
+    xs.unattach.foldlM f = xs.foldlM fun b ⟨x, h⟩ =>
       binderNameHint b f <| binderNameHint x (f b) <| binderNameHint h () <|
       f b (wfParam x) := by
   simp [wfParam]
@@ -411,12 +378,12 @@ and simplifies these to the function directly taking the value.
   rw [List.foldrM_subtype hf]
 
 
-@[wf_preprocess] theorem foldrM_wfParam [Monad m] [LawfulMonad m] (xs : Array α) (f : α → β → m β) (init : β) :
-    (wfParam xs).foldrM f init = xs.attach.unattach.foldrM f init := by
+@[wf_preprocess] theorem foldrM_wfParam [Monad m] [LawfulMonad m] (xs : Array α) (f : α → β → m β) :
+    (wfParam xs).foldrM f = xs.attach.unattach.foldrM f := by
   simp [wfParam]
 
-@[wf_preprocess] theorem foldrM_unattach [Monad m] [LawfulMonad m] (P : α → Prop) (xs : Array (Subtype P)) (f : α → β → m β) (init : β):
-    xs.unattach.foldrM f init = xs.foldrM (init := init) fun ⟨x, h⟩ b =>
+@[wf_preprocess] theorem foldrM_unattach [Monad m] [LawfulMonad m] (P : α → Prop) (xs : Array (Subtype P)) (f : α → β → m β) :
+    xs.unattach.foldrM f = xs.foldrM fun ⟨x, h⟩ b =>
       binderNameHint x f <| binderNameHint h () <| binderNameHint b (f x) <|
       f (wfParam x) b := by
   simp [wfParam]

src/Init/Data/Array/OfFn.lean

@@ -16,25 +16,6 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 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/BEq.lean

@@ -49,14 +49,6 @@ 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

@@ -109,12 +109,7 @@ open Nat Bool
 
 namespace Bool
 
-/--
-At least two out of three Booleans are true.
-
-This function is typically used to model addition of binary numbers, to combine a carry bit with two
-addend bits.
--/
+/-- At least two out of three booleans are true. -/
 abbrev atLeastTwo (a b c : Bool) : Bool := a && b || a && c || b && c
 
 @[simp] theorem atLeastTwo_false_left  : atLeastTwo false b c = (b && c) := by simp [atLeastTwo]
@@ -483,36 +478,6 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
         case zero => exact hmsb
         case succ => exact getMsbD_x _ hi (by omega)
 
-/-- This is false if `v < w` and `b = intMin`. See also `signExtend_neg_of_ne_intMin`. -/
-@[simp] theorem signExtend_neg_of_le {v w : Nat} (h : w ≤ v) (b : BitVec v) :
-    (-b).signExtend w = -b.signExtend w := by
-  apply BitVec.eq_of_getElem_eq
-  intro i hi
-  simp only [getElem_signExtend, getElem_neg]
-  rw [dif_pos (by omega), dif_pos (by omega)]
-  simp only [getLsbD_signExtend, Bool.and_eq_true, decide_eq_true_eq, Bool.ite_eq_true_distrib,
-    Bool.bne_right_inj, decide_eq_decide]
-  exact ⟨fun ⟨j, hj₁, hj₂⟩ => ⟨j, ⟨hj₁, ⟨by omega, by rwa [if_pos (by omega)]⟩⟩⟩,
-    fun ⟨j, hj₁, hj₂, hj₃⟩ => ⟨j, hj₁, by rwa [if_pos (by omega)] at hj₃⟩⟩
-
-/-- This is false if `v < w` and `b = intMin`. See also `signExtend_neg_of_le`. -/
-@[simp] theorem signExtend_neg_of_ne_intMin {v w : Nat} (b : BitVec v) (hb : b ≠ intMin v) :
-    (-b).signExtend w = -b.signExtend w := by
-  refine (by omega : w ≤ v ∨ v < w).elim (fun h => signExtend_neg_of_le h b) (fun h => ?_)
-  apply BitVec.eq_of_toInt_eq
-  rw [toInt_signExtend_of_le (by omega), toInt_neg_of_ne_intMin hb, toInt_neg_of_ne_intMin,
-    toInt_signExtend_of_le (by omega)]
-  apply ne_of_apply_ne BitVec.toInt
-  rw [toInt_signExtend_of_le (by omega), toInt_intMin_of_pos (by omega)]
-  have := b.le_two_mul_toInt
-  have : -2 ^ w < -2 ^ v := by
-    apply Int.neg_lt_neg
-    norm_cast
-    rwa [Nat.pow_lt_pow_iff_right (by omega)]
-  have : 2 * b.toInt ≠ -2 ^ w := by omega
-  rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
-  omega
-
 /-! ### abs -/
 
 theorem msb_abs {w : Nat} {x : BitVec w} :
@@ -579,15 +544,6 @@ 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]
@@ -1288,8 +1244,8 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) :
   simp only [saddOverflow]
   rcases w with _|w
   · revert x y; decide
-  · have := le_two_mul_toInt (x := x); have := two_mul_toInt_lt (x := x)
-    have := le_two_mul_toInt (x := y); have := two_mul_toInt_lt (x := y)
+  · have := le_toInt (x := x); have := toInt_lt (x := x)
+    have := le_toInt (x := y); have := toInt_lt (x := y)
     simp only [← decide_or, msb_eq_toInt, decide_beq_decide, toInt_add, ← decide_not, ← decide_and,
       decide_eq_decide]
     rw_mod_cast [Int.bmod_neg_iff (by omega) (by omega)]

src/Init/Data/BitVec/Lemmas.lean

@@ -13,9 +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
-import Init.Data.Int.LemmasAux
 
 set_option linter.missingDocs true
 
@@ -241,16 +239,12 @@ theorem eq_of_getMsbD_eq {x y : BitVec w}
 theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp [← getLsbD_eq_getElem]
 
 theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero]
-theorem toInt_zero_length (x : BitVec 0) : x.toInt = 0 := by simp [of_length_zero]
-
 theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false := by simp
 theorem getMsbD_zero_length (x : BitVec 0) : x.getMsbD i = false := by simp
 theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero]
 
 theorem toNat_of_zero_length (h : w = 0) (x : BitVec w) : x.toNat = 0 := by
   subst h; simp [toNat_zero_length]
-theorem toInt_of_zero_length (h : w = 0) (x : BitVec w) : x.toInt = 0 := by
-  subst h; simp [toInt_zero_length]
 theorem getLsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getLsbD i = false := by
   subst h; simp [getLsbD_zero_length]
 theorem getMsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getMsbD i = false := by
@@ -329,25 +323,8 @@ 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
 
-@[simp] theorem finMk_toNat (x : BitVec w) : Fin.mk x.toNat x.isLt = x.toFin := rfl
-
-@[simp] theorem toFin_ofNatLT {n : Nat} (h : n < 2 ^ w) : (BitVec.ofNatLT n h).toFin = Fin.mk n h := rfl
-
-@[simp] theorem toFin_ofFin (n : Fin (2 ^ w)) : (BitVec.ofFin n).toFin = n := rfl
-@[simp] theorem ofFin_toFin (x : BitVec w) : BitVec.ofFin x.toFin = x := rfl
-
-@[simp] theorem ofNatLT_finVal (n : Fin (2 ^ w)) : BitVec.ofNatLT n.val n.isLt = BitVec.ofFin n := rfl
-
-@[simp] theorem ofNatLT_toNat (x : BitVec w) : BitVec.ofNatLT x.toNat x.isLt = x := rfl
-
-@[simp] theorem ofNat_finVal (n : Fin (2 ^ w)) : BitVec.ofNat w n.val = BitVec.ofFin n := by
-  rw [← BitVec.ofNatLT_eq_ofNat n.isLt, ofNatLT_finVal]
-
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
 -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
 theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
@@ -551,9 +528,6 @@ 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
@@ -564,16 +538,6 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
     rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
 
-theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by
-  simp only [BitVec.toInt]
-  have : 2 * x.toNat ≥ 2 ^ w := msb_eq_true_iff_two_mul_ge.mp h
-  omega
-
-theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.toInt := by
-  simp only [BitVec.toInt]
-  have : 2 * x.toNat < 2 ^ w := msb_eq_false_iff_two_mul_lt.mp h
-  omega
-
 /-- Prove equality of bitvectors in terms of nat operations. -/
 theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by
   intro eq
@@ -605,11 +569,6 @@ 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,7 +604,7 @@ theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by
 `x.toInt` is less than `2^(w-1)`.
 We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used.
 -/
-theorem two_mul_toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by
+theorem toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by
   simp only [BitVec.toInt]
   rcases w with _|w'
   · omega
@@ -653,25 +612,11 @@ theorem two_mul_toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
-theorem two_mul_toInt_le {w : Nat} {x : BitVec w} : 2 * x.toInt ≤ 2 ^ w - 1 :=
-  Int.le_sub_one_of_lt two_mul_toInt_lt
-
-theorem toInt_lt {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by
-  by_cases h : w = 0
-  · subst h
-    simp [eq_nil x]
-  · have := @two_mul_toInt_lt w x
-    rw_mod_cast [← Nat.two_pow_pred_add_two_pow_pred (by omega), Int.mul_comm, Int.natCast_add] at this
-    omega
-
-theorem toInt_le {w : Nat} {x : BitVec w} : x.toInt ≤ 2 ^ (w - 1) - 1 :=
-  Int.le_sub_one_of_lt toInt_lt
-
 /--
 `x.toInt` is greater than or equal to `-2^(w-1)`.
 We phrase the fact in terms of `2^w` to prevent a case split on `w=0` when the lemma is used.
 -/
-theorem le_two_mul_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by
+theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by
   simp only [BitVec.toInt]
   rcases w with _|w'
   · omega
@@ -679,16 +624,6 @@ theorem le_two_mul_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt := by
     simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]
     norm_cast; omega
 
-
-theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by
-  by_cases h : w = 0
-  · subst h
-    simp [BitVec.eq_nil x]
-  · have := le_two_mul_toInt (w := w) (x := x)
-    generalize x.toInt = x at *
-    rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
-    omega
-
 /-! ### slt -/
 
 /--
@@ -710,12 +645,6 @@ 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]
@@ -1067,11 +996,6 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
   apply eq_of_toNat_eq
   simp [extractLsb, show len - 1 + 1 = len by omega]
 
-/-- Extracting all the bits of a bitvector is an identity operation. -/
-@[simp] theorem extractLsb'_eq_self {x : BitVec w} : x.extractLsb' 0 w = x := by
-  apply eq_of_toNat_eq
-  simp [extractLsb']
-
 /-! ### allOnes -/
 
 @[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by
@@ -1543,16 +1467,6 @@ 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
@@ -1821,7 +1735,7 @@ theorem toInt_ushiftRight {x : BitVec w} {n : Nat} :
     simp [hn]
 
 @[simp]
-theorem toFin_ushiftRight {x : BitVec w} {n : Nat} :
+theorem toFin_uShiftRight {x : BitVec w} {n : Nat} :
     (x >>> n).toFin = x.toFin / (Fin.ofNat' (2^w) (2^n)) := by
   apply Fin.eq_of_val_eq
   by_cases hn : n < w
@@ -2027,118 +1941,11 @@ theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
         by_cases h₄ : n + (w - 1 - i) < w <;> (simp only [h₄, ↓reduceIte]; congr; omega)
   · simp [h]
 
-theorem toInt_shiftRight_lt {x : BitVec w} {n : Nat} :
-    x.toInt >>> n < 2 ^ (w - 1) := by
-  have := @Int.shiftRight_le_of_nonneg x.toInt n
-  have := @Int.shiftRight_le_of_nonpos x.toInt n
-  have := @BitVec.toInt_lt w x
-  have := @Nat.one_le_two_pow (w-1)
-  norm_cast at *
-  omega
-
-theorem le_toInt_shiftRight {x : BitVec w} {n : Nat} :
-    -(2 ^ (w - 1)) ≤ x.toInt >>> n := by
-  have := @Int.le_shiftRight_of_nonpos x.toInt n
-  have := @Int.le_shiftRight_of_nonneg x.toInt n
-  have := @BitVec.le_toInt w x
-  have := @Nat.one_le_two_pow (w-1)
-  norm_cast at *
-  omega
-
-theorem toNat_sshiftRight_of_msb_true {x : BitVec w} {n : Nat} (h : x.msb = true) :
-    (x.sshiftRight n).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n := by
-  simp [sshiftRight_eq_of_msb_true, h]
-
-theorem toNat_sshiftRight_of_msb_false {x : BitVec w} {n : Nat} (h : x.msb = false) :
-    (x.sshiftRight n).toNat = x.toNat >>> n := by
-  simp [sshiftRight_eq_of_msb_false, h]
-
-theorem toNat_sshiftRight {x : BitVec w} {n : Nat} :
-    (x.sshiftRight n).toNat =
-      if x.msb
-      then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n
-      else x.toNat >>> n := by
-  by_cases h : x.msb
-  · simp [toNat_sshiftRight_of_msb_true, h]
-  · rw [Bool.not_eq_true] at h
-    simp [toNat_sshiftRight_of_msb_false, h]
-
-theorem toFin_sshiftRight_of_msb_true {x : BitVec w} {n : Nat} (h : x.msb = true) :
-    (x.sshiftRight n).toFin = Fin.ofNat' (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n) := by
-  apply Fin.eq_of_val_eq
-  simp only [val_toFin, toNat_sshiftRight, h, ↓reduceIte, Fin.val_ofNat']
-  rw [Nat.mod_eq_of_lt]
-  have := x.isLt
-  have ineq : ∀ y, 2 ^ w - 1 - y < 2 ^ w := by omega
-  exact ineq ((2 ^ w - 1 - x.toNat) >>> n)
-
-theorem toFin_sshiftRight_of_msb_false {x : BitVec w} {n : Nat} (h : x.msb = false) :
-    (x.sshiftRight n).toFin = Fin.ofNat' (2^w) (x.toNat >>> n) := by
-  apply Fin.eq_of_val_eq
-  simp only [val_toFin, toNat_sshiftRight, h, Bool.false_eq_true, ↓reduceIte, Fin.val_ofNat']
-  have := Nat.shiftRight_le x.toNat n
-  rw [Nat.mod_eq_of_lt (by omega)]
-
-theorem toFin_sshiftRight {x : BitVec w} {n : Nat} :
-    (x.sshiftRight n).toFin =
-      if x.msb
-      then Fin.ofNat' (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n)
-      else Fin.ofNat' (2^w) (x.toNat >>> n) := by
-  by_cases h : x.msb
-  · simp [toFin_sshiftRight_of_msb_true, h]
-  · simp [toFin_sshiftRight_of_msb_false, h]
-
-@[simp]
-theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
-    (x.sshiftRight n).toInt = x.toInt >>> n := by
-  by_cases h : w = 0
-  · subst h
-    simp [BitVec.eq_nil x]
-  · rw [sshiftRight, toInt_ofInt, ←Nat.two_pow_pred_add_two_pow_pred (by omega)]
-    have := @toInt_shiftRight_lt w x n
-    have := @le_toInt_shiftRight w x n
-    norm_cast at *
-    exact Int.bmod_eq_self_of_le (by omega) (by omega)
-
 /-! ### sshiftRight reductions from BitVec to Nat -/
 
 @[simp]
 theorem sshiftRight_eq' (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat := rfl
 
-theorem toNat_sshiftRight'_of_msb_true {x y : BitVec w} (h : x.msb = true) :
-    (x.sshiftRight' y).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat := by
-  rw [sshiftRight_eq', toNat_sshiftRight_of_msb_true h]
-
-theorem toNat_sshiftRight'_of_msb_false {x y : BitVec w} (h : x.msb = false) :
-    (x.sshiftRight' y).toNat = x.toNat >>> y.toNat := by
-  rw [sshiftRight_eq', toNat_sshiftRight_of_msb_false h]
-
-theorem toNat_sshiftRight' {x y : BitVec w} :
-    (x.sshiftRight' y).toNat =
-      if x.msb
-      then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat
-      else x.toNat >>> y.toNat := by
-  rw [sshiftRight_eq', toNat_sshiftRight]
-
-theorem toFin_sshiftRight'_of_msb_true {x y : BitVec w} (h : x.msb = true) :
-    (x.sshiftRight' y).toFin = Fin.ofNat' (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat) := by
-  rw [sshiftRight_eq', toFin_sshiftRight_of_msb_true h]
-
-theorem toFin_sshiftRight'_of_msb_false {x y : BitVec w} (h : x.msb = false) :
-    (x.sshiftRight' y).toFin = Fin.ofNat' (2^w) (x.toNat >>> y.toNat) := by
-  rw [sshiftRight_eq', toFin_sshiftRight_of_msb_false h]
-
-theorem toFin_sshiftRight' {x y : BitVec w} :
-    (x.sshiftRight' y).toFin =
-      if x.msb
-      then Fin.ofNat' (2^w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat)
-      else Fin.ofNat' (2^w) (x.toNat >>> y.toNat) := by
-  rw [sshiftRight_eq', toFin_sshiftRight]
-
-theorem toInt_sshiftRight' {x y : BitVec w} :
-    (x.sshiftRight' y).toInt = x.toInt >>> y.toNat := by
-  rw [sshiftRight_eq', toInt_sshiftRight]
-
 -- This should not be a `@[simp]` lemma as the left hand side is not in simp normal form.
 theorem getLsbD_sshiftRight' {x y : BitVec w} {i : Nat} :
     getLsbD (x.sshiftRight' y) i =
@@ -2229,18 +2036,14 @@ theorem msb_signExtend {x : BitVec w} :
   · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
 
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
-theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
+theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
   ext i h
   simp [getElem_signExtend, show i < w by omega]
 
-@[deprecated signExtend_eq_setWidth_of_le (since := "2025-03-07")]
-theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w) :
-  x.signExtend v = x.setWidth v := signExtend_eq_setWidth_of_le x hv
-
 /-- Sign extending to the same bitwidth is a no op. -/
-@[simp] theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
-  rw [signExtend_eq_setWidth_of_le _ (Nat.le_refl _), setWidth_eq]
+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.
 If the msb is false, then the result equals the original value.
@@ -2277,65 +2080,47 @@ theorem toNat_signExtend (x : BitVec w) {v : Nat} :
     (x.signExtend v).toNat = (x.setWidth v).toNat + if x.msb then 2^v - 2^w else 0 := by
   by_cases h : v ≤ w
   · have : 2^v ≤ 2^w := Nat.pow_le_pow_right Nat.two_pos h
-    simp [signExtend_eq_setWidth_of_le x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]
+    simp [signExtend_eq_setWidth_of_lt x h, toNat_setWidth, Nat.sub_eq_zero_of_le this]
   · 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_le {x : BitVec w} (h : w ≤ v) :
+theorem toInt_signExtend_of_lt {x : BitVec w} (hv : w < v):
     (x.signExtend v).toInt = x.toInt := by
-  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)]
+  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_eq_toNat_bmod_of_le {x : BitVec w} (hv : v ≤ w) :
+theorem toInt_signExtend_of_le {x : BitVec w} (hv : v ≤ w) :
     (x.signExtend v).toInt = Int.bmod x.toNat (2^v) := by
-  simp [signExtend_eq_setWidth_of_le _ hv]
+  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). See `toInt_signExtend` for a version stated
-in terms of `toInt` instead of `toNat`.
+computes `x % 2^v` (where `%` is the balanced mod).
 -/
-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_eq_toNat_bmod_of_le hv, Nat.min_eq_left hv]
-  · simp only [Nat.not_le] at hv
-    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]
+    (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 only [Nat.not_le] at hv
+    rw [toInt_signExtend_of_lt hv, Nat.min_eq_right (by omega), toInt_eq_toNat_bmod]
 
 /-! ### append -/
 
@@ -2480,42 +2265,6 @@ theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
     (x <<< n).msb = x.getMsbD n := by
   simp [BitVec.msb]
 
-/--
-A `(x : BitVec v)` set to width `w` equals `(v - w)` zeros,
-followed by the low `(min v w) bits of `x`
--/
-theorem setWidth_eq_append_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} :
-    x.setWidth w = ((0#(w - v)) ++ x.extractLsb' 0 (min v w)).cast (by omega) := by
-  ext i hi
-  simp only [getElem_cast, getElem_append]
-  by_cases hiv : i < v
-  · simp [hi]
-    omega
-  · simp [getLsbD_ge x i (by omega)]
-
-/--
-A `(x : BitVec v)` set to a width `w ≥ v` equals `(w - v)` zeros, followed by `x`.
--/
-theorem setWidth_eq_append {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) :
-    x.setWidth w = ((0#(w - v)) ++ x).cast (by omega) := by
-  rw [setWidth_eq_append_extractLsb']
-  ext i hi
-  simp only [getElem_cast, getElem_append]
-  by_cases hiv : i < v
-  · simp [hiv]
-    omega
-  · simp [hiv, getLsbD_ge x i (by omega)]
-
-theorem setWidth_eq_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) :
-    x.setWidth w = (x.extractLsb' 0 w).cast (by omega) := by
-  rw [setWidth_eq_append_extractLsb']
-  ext i hi
-  simp only [getElem_cast, getElem_append]
-  by_cases hiv : i < v
-  · simp [hi]
-    omega
-  · simp [getLsbD_ge x i (by omega)]
-
 theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
     x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega) := by
   ext i hi
@@ -2533,29 +2282,6 @@ theorem shiftLeft_eq_concat_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
   · simp [hi']
   · simp [hi', show i - n < w by omega]
 
-/-- Combine adjacent `extractLsb'` operations into a single `extractLsb'`. -/
-theorem extractLsb'_append_extractLsb'_eq_extractLsb' {x : BitVec w} (h : start₂ = start₁ + len₁) :
-    ((x.extractLsb' start₂ len₂) ++ (x.extractLsb' start₁ len₁)) =
-    (x.extractLsb' start₁ (len₁ + len₂)).cast (by omega) := by
-  ext i h
-  simp only [getElem_append, getElem_extractLsb', dite_eq_ite, getElem_cast, ite_eq_left_iff,
-    Nat.not_lt]
-  intros hi
-  congr 1
-  omega
-
-/-- Combine adjacent `~~~ (extractLsb _)'` operations into a single `~~~ (extractLsb _)'`. -/
-theorem not_extractLsb'_append_not_extractLsb'_eq_not_extractLsb' {x : BitVec w} (h : start₂ = start₁ + len₁) :
-    (~~~ (x.extractLsb' start₂ len₂) ++ ~~~ (x.extractLsb' start₁ len₁)) =
-    (~~~ x.extractLsb' start₁ (len₁ + len₂)).cast (by omega) := by
-  ext i h
-  simp only [getElem_cast, getElem_not, getElem_extractLsb', getElem_append]
-  by_cases hi : i < len₁
-  · simp [hi]
-  · simp only [hi, ↓reduceDIte, Bool.not_eq_eq_eq_not, Bool.not_not]
-    congr 1
-    omega
-
 /-! ### rev -/
 
 theorem getLsbD_rev (x : BitVec w) (i : Fin w) :
@@ -2967,9 +2693,6 @@ 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
@@ -3428,7 +3151,6 @@ then `x / y` is nonnegative, thus `toInt` and `toNat` coincide.
 theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
     (x / y).toInt = x.toNat / y.toNat := by
   simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]
-  norm_cast
 
 /-! ### umod -/
 
@@ -4228,6 +3950,7 @@ theorem toNat_intMin : (intMin w).toNat = 2 ^ (w - 1) % 2 ^ w := by
 /--
 The RHS is zero in case `w = 0` which is modeled by wrapping the expression in `... % 2 ^ w`.
 -/
+@[simp]
 theorem toInt_intMin {w : Nat} :
     (intMin w).toInt = -((2 ^ (w - 1) % 2 ^ w) : Nat) := by
   by_cases h : w = 0
@@ -4239,16 +3962,10 @@ theorem toInt_intMin {w : Nat} :
     rw [Nat.mul_comm]
     simp [w_pos]
 
-theorem toInt_intMin_of_pos {v : Nat} (hv : 0 < v) : (intMin v).toInt = -2 ^ (v - 1) := by
-  rw [toInt_intMin, Nat.mod_eq_of_lt]
-  · simp [Int.natCast_pow]
-  · rw [Nat.pow_lt_pow_iff_right (by omega)]
-    omega
-
 theorem toInt_intMin_le (x : BitVec w) :
     (intMin w).toInt ≤ x.toInt := by
   cases w
-  case zero => simp [toInt_intMin, @of_length_zero x]
+  case zero => simp [@of_length_zero x]
   case succ w =>
     simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
     have : 0 < 2 ^ w := Nat.two_pow_pos w
@@ -4392,7 +4109,9 @@ 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
@@ -4627,9 +4346,6 @@ instance instDecidableExistsBitVec :
 
 set_option linter.missingDocs false
 
-@[deprecated toFin_uShiftRight (since := "2025-02-18")]
-abbrev toFin_uShiftRight := @toFin_ushiftRight
-
 @[deprecated signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")]
 abbrev signExtend_eq_not_setWidth_not_of_msb_false := @signExtend_eq_setWidth_of_msb_false
 
@@ -4742,7 +4458,7 @@ abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_setWidth
 abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true
 
 @[deprecated signExtend_eq_setWidth_of_lt (since := "2024-09-18")]
-abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_le
+abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_lt
 
 @[deprecated truncate_append (since := "2024-09-18")]
 abbrev truncate_append := @setWidth_append

src/Init/Data/Bool.lean

@@ -9,19 +9,7 @@ import Init.NotationExtra
 
 namespace Bool
 
-/--
-Boolean “exclusive or”. `xor x y` can be written `x ^^ y`.
-
-`x ^^ y` is `true` when precisely one of `x` or `y` is `true`. Unlike `and` and `or`, it does not
-have short-circuiting behavior, because one argument's value never determines the final value. Also
-unlike `and` and `or`, there is no commonly-used corresponding propositional connective.
-
-Examples:
- * `false ^^ false = false`
- * `true ^^ false = true`
- * `false ^^ true = true`
- * `true ^^ true = false`
--/
+/-- Boolean exclusive or -/
 abbrev xor : Bool → Bool → Bool := bne
 
 @[inherit_doc] infixl:33 " ^^ " => xor
@@ -379,9 +367,7 @@ theorem and_or_inj_left_iff :
 
 /-! ## toNat -/
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
+/-- convert a `Bool` to a `Nat`, `false -> 0`, `true -> 1` -/
 def toNat (b : Bool) : Nat := cond b 1 0
 
 @[simp, bitvec_to_nat] theorem toNat_false : false.toNat = 0 := rfl
@@ -402,9 +388,7 @@ theorem toNat_lt (b : Bool) : b.toNat < 2 :=
 
 /-! ## toInt -/
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
+/-- convert a `Bool` to an `Int`, `false -> 0`, `true -> 1` -/
 def toInt (b : Bool) : Int := cond b 1 0
 
 @[simp] theorem toInt_false : false.toInt = 0 := rfl
@@ -555,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  {α : 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
+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
 
 @[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/ByteArray/Basic.lean

@@ -18,13 +18,10 @@ attribute [extern "lean_byte_array_data"] ByteArray.data
 
 namespace ByteArray
 @[extern "lean_mk_empty_byte_array"]
-def emptyWithCapacity (c : @& Nat) : ByteArray :=
+def mkEmpty (c : @& Nat) : ByteArray :=
   { data := #[] }
 
-@[deprecated emptyWithCapacity (since := "2025-03-12")]
-abbrev mkEmpty := emptyWithCapacity
-
-def empty : ByteArray := emptyWithCapacity 0
+def empty : ByteArray := mkEmpty 0
 
 instance : Inhabited ByteArray where
   default := empty

src/Init/Data/Char/Basic.lean

@@ -15,15 +15,7 @@ Note that values in `[0xd800, 0xdfff]` are reserved for [UTF-16 surrogate pairs]
 
 namespace Char
 
-/--
-One character is less than another if its code point is strictly less than the other's.
--/
 protected def lt (a b : Char) : Prop := a.val < b.val
-
-/--
-One character is less than or equal to another if its code point is less than or equal to the
-other's.
--/
 protected def le (a b : Char) : Prop := a.val ≤ b.val
 
 instance : LT Char := ⟨Char.lt⟩
@@ -35,10 +27,7 @@ instance (a b : Char) :  Decidable (a < b) :=
 instance (a b : Char) : Decidable (a ≤ b) :=
   UInt32.decLe _ _
 
-/--
-True for natural numbers that are valid [Unicode scalar
-values](https://www.unicode.org/glossary/#unicode_scalar_value).
--/
+/-- Determines if the given nat is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).-/
 abbrev isValidCharNat (n : Nat) : Prop :=
   n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
 
@@ -61,93 +50,55 @@ theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValid
 theorem isValidChar_zero : isValidChar 0 :=
   Or.inl (by decide)
 
-/--
-The character's Unicode code point as a `Nat`.
--/
+/-- Underlying unicode code point as a `Nat`. -/
 @[inline] def toNat (c : Char) : Nat :=
   c.val.toNat
 
-/--
-Converts a character into a `UInt8` that contains its code point.
-
-If the code point is larger than 255, it is truncated (reduced modulo 256).
--/
+/-- Convert a character into a `UInt8`, by truncating (reducing modulo 256) if necessary. -/
 @[inline] def toUInt8 (c : Char) : UInt8 :=
   c.val.toUInt8
 
-/--
-Converts an 8-bit unsigned integer into a character.
-
-The integer's value is interpreted as a Unicode code point.
--/
+/-- The numbers from 0 to 256 are all valid UTF-8 characters, so we can embed one in the other. -/
 def ofUInt8 (n : UInt8) : Char := ⟨n.toUInt32, .inl (Nat.lt_trans n.toBitVec.isLt (by decide))⟩
 
 instance : Inhabited Char where
   default := 'A'
 
-/--
-Returns `true` if the character is a space `(' ', U+0020)`, a tab `('\t', U+0009)`, a carriage
-return `('\r', U+000D)`, or a newline `('\n', U+000A)`.
--/
+/-- Is the character a space (U+0020) a tab (U+0009), a carriage return (U+000D) or a newline (U+000A)? -/
 @[inline] def isWhitespace (c : Char) : Bool :=
   c = ' ' || c = '\t' || c = '\r' || c = '\n'
 
-/--
-Returns `true` if the character is a uppercase ASCII letter.
-
-The uppercase ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZ`.
--/
+/-- Is the character in `ABCDEFGHIJKLMNOPQRSTUVWXYZ`? -/
 @[inline] def isUpper (c : Char) : Bool :=
   c.val ≥ 65 && c.val ≤ 90
 
-/--
-Returns `true` if the character is a lowercase ASCII letter.
-
-The lowercase ASCII letters are the following: `abcdefghijklmnopqrstuvwxyz`.
--/
+/-- Is the character in `abcdefghijklmnopqrstuvwxyz`? -/
 @[inline] def isLower (c : Char) : Bool :=
   c.val ≥ 97 && c.val ≤ 122
 
-/--
-Returns `true` if the character is an ASCII letter.
-
-The ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz`.
--/
+/-- Is the character in `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz`? -/
 @[inline] def isAlpha (c : Char) : Bool :=
   c.isUpper || c.isLower
 
-/--
-Returns `true` if the character is an ASCII digit.
-
-The ASCII digits are the following: `0123456789`.
--/
+/-- Is the character in `0123456789`? -/
 @[inline] def isDigit (c : Char) : Bool :=
   c.val ≥ 48 && c.val ≤ 57
 
-/--
-Returns `true` if the character is an ASCII letter or digit.
-
-The ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz`.
-The ASCII digits are the following: `0123456789`.
--/
+/-- Is the character in `ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789`? -/
 @[inline] def isAlphanum (c : Char) : Bool :=
   c.isAlpha || c.isDigit
 
-/--
-Converts an uppercase ASCII letter to the corresponding lowercase letter. Letters outside the ASCII
-alphabet are returned unchanged.
+/-- Convert an upper case character to its lower case character.
 
-The uppercase ASCII letters are the following: `ABCDEFGHIJKLMNOPQRSTUVWXYZ`.
+Only works on basic latin letters.
 -/
 def toLower (c : Char) : Char :=
   let n := toNat c;
   if n >= 65 ∧ n <= 90 then ofNat (n + 32) else c
 
-/--
-Converts a lowercase ASCII letter to the corresponding uppercase letter. Letters outside the ASCII
-alphabet are returned unchanged.
+/-- Convert a lower case character to its upper case character.
 
-The lowercase ASCII letters are the following: `abcdefghijklmnopqrstuvwxyz`.
+Only works on basic latin letters.
 -/
 def toUpper (c : Char) : Char :=
   let n := toNat c;

src/Init/Data/Fin/Lemmas.lean

@@ -45,7 +45,6 @@ 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
 
@@ -56,14 +55,6 @@ 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/FloatArray/Basic.lean

@@ -17,14 +17,11 @@ attribute [extern "lean_float_array_data"] FloatArray.data
 
 namespace FloatArray
 @[extern "lean_mk_empty_float_array"]
-def emptyWithCapacity (c : @& Nat) : FloatArray :=
+def mkEmpty (c : @& Nat) : FloatArray :=
   { data := #[] }
 
-@[deprecated emptyWithCapacity (since := "2025-03-12")]
-abbrev mkEmpty := emptyWithCapacity
-
 def empty : FloatArray :=
-  emptyWithCapacity 0
+  mkEmpty 0
 
 instance : Inhabited FloatArray where
   default := empty

src/Init/Data/Int.lean

@@ -14,4 +14,3 @@ import Init.Data.Int.Order
 import Init.Data.Int.Pow
 import Init.Data.Int.Cooper
 import Init.Data.Int.Linear
-import Init.Data.Int.OfNat

src/Init/Data/Int/Basic.lean

@@ -17,12 +17,10 @@ open Nat
 This file defines the `Int` type as well as
 
 * coercions, conversions, and compatibility with numeric literals,
-* basic arithmetic operations add/sub/mul/pow,
+* basic arithmetic operations add/sub/mul/div/mod/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/Bitwise/Lemmas.lean

@@ -27,7 +27,7 @@ theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
     m >>> n = m / ((2 ^ n) : Nat) := by
   simp only [shiftRight_eq, Int.shiftRight, Nat.shiftRight_eq_div_pow]
   split
-  · simp; norm_cast
+  · simp
   · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]
     rfl
 
@@ -39,47 +39,4 @@ theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
 theorem shiftRight_zero (n : Int) : n >>> 0 = n := by
   simp [Int.shiftRight_eq_div_pow]
 
-theorem le_shiftRight_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : n ≤ n >>> s := by
-  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
-  split
-  case _ _ _ m =>
-    simp only [ofNat_eq_coe] at h
-    by_cases hm : m = 0
-    · simp [hm]
-    · omega
-  case _ _ _ m =>
-    by_cases hm : m = 0
-    · simp [hm]
-    · have := Nat.shiftRight_le m s
-      omega
-
-theorem shiftRight_le_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) : n >>> s ≤ n := by
-  simp only [Int.shiftRight_eq, Int.shiftRight, Int.ofNat_eq_coe]
-  split
-  case _ _ _ m =>
-    simp only [Int.ofNat_eq_coe] at h
-    by_cases hm : m = 0
-    · simp [hm]
-    · have := Nat.shiftRight_le m s
-      simp
-      omega
-  case _ _ _ m =>
-    omega
-
-theorem le_shiftRight_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) : 0 ≤ (n >>> s) := by
-  rw [Int.shiftRight_eq_div_pow]
-  by_cases h' : s = 0
-  · simp [h', h]
-  · have := @Nat.pow_pos 2 s (by omega)
-    have := @Int.ediv_nonneg n (2^s) h (by norm_cast at *; omega)
-    norm_cast at *
-
-theorem shiftRight_le_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : (n >>> s) ≤ 0 := by
-  rw [Int.shiftRight_eq_div_pow]
-  by_cases h' : s = 0
-  · simp [h', h]
-  · have : 1 < 2 ^ s := Nat.one_lt_two_pow (by omega)
-    have rl : n / 2 ^ s ≤ 0 := Int.ediv_nonpos_of_nonpos_of_neg (by omega) (by norm_cast at *; omega)
-    norm_cast at *
-
 end Int

src/Init/Data/Int/Cooper.lean

@@ -227,4 +227,33 @@ theorem cooper_resolution_dvd_right
     · exact Int.mul_neg _ _ ▸ Int.neg_le_of_neg_le lower
     · exact Int.mul_neg _ _ ▸ Int.neg_mul _ _ ▸ dvd
 
-end Int
+/--
+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

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

@@ -21,28 +21,26 @@ 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` for the default typeclass instances,
+However we decided it was better to use `ediv` and `emod`,
 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).
 
+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 `div` and `mod`, but have not yet renamed `ediv` and `emod`.
+In December 2024, we removed `tdiv` and `tmod`, but have not yet renamed `ediv` and `emod`.
 -/
 
 /-! ### E-rounding division
-This pair satisfies `0 ≤ emod x y < natAbs y` for `y ≠ 0`.
+This pair 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` for `y ≠ 0`.
-
-This means that `Int.ediv x y = floor (x / y)` when `y > 0` and `Int.ediv x y = ceil (x / y)` when `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`
+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.
 
@@ -73,7 +71,7 @@ def ediv : (@& Int) → (@& Int) → Int
   | -[m+1],  -[n+1]  => ofNat (succ (m / succ n))
 
 /--
-Integer modulus. This version of integer modulus uses the E-rounding convention
+Integer modulus. This version of `Int.mod` 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`.
 
@@ -111,7 +109,7 @@ instance : Div Int where
 instance : Mod Int where
   mod := Int.emod
 
-@[norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+@[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]
@@ -167,9 +165,6 @@ def tdiv : (@& Int) → (@& Int) → Int
   unconditionally (see [`Int.tmod_add_tdiv`][theo tmod_add_tdiv]). In
   particular, `a % 0 = a`.
 
-  `tmod` satisfies `natAbs (tmod a b) = natAbs a % natAbs b`,
-  and when `b` does not divide `a`, `tmod a b` has the same sign as `a`.
-
   [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
   [theo tmod_add_tdiv]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.tmod_add_tdiv#doc
 
@@ -234,7 +229,7 @@ def fdiv : Int → Int → Int
   | -[m+1],  -[n+1]  => ofNat (succ m / succ n)
 
 /--
-Integer modulus. This version of integer modulus uses the F-rounding convention
+Integer modulus. This version of `Int.mod` 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`.
 
@@ -273,14 +268,11 @@ 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`.
 
-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.
+This 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
 
@@ -53,7 +53,7 @@ protected theorem dvd_mul_left (a b : Int) : b ∣ a * b := ⟨_, Int.mul_comm .
   constructor <;> exact fun ⟨k, e⟩ =>
     ⟨-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
 
-@[simp] protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
+protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
   constructor <;> exact fun ⟨k, e⟩ =>
     ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
 
@@ -67,7 +67,7 @@ protected theorem dvd_mul_left (a b : Int) : b ∣ a * b := ⟨_, Int.mul_comm .
 theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
   rw [← natAbs_dvd_natAbs, natAbs_ofNat]
 
-/-! ### ediv zero  -/
+/-! ### *div 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
 
-/-! ### emod zero -/
+/-! ### mod zero -/
 
 @[simp] theorem zero_emod (b : Int) : 0 % b = 0 := rfl
 
@@ -89,6 +89,7 @@ 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
@@ -105,23 +106,18 @@ 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]
 
 /-! ### `/` ediv -/
 
-@[simp] theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
+@[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat _, -[_+1] => (Int.neg_neg _).symm
   | ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl
@@ -158,10 +154,6 @@ 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
@@ -178,14 +170,13 @@ 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 ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a := by
+theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0 := by
   rw [Int.div_def]
   match b, h with
   | Int.ofNat (b+1), _ =>
     rcases a with ⟨a⟩ <;> simp [Int.ediv]
-
-@[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
-abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos
+    norm_cast
+    simp
 
 /-! ### emod -/
 
@@ -198,6 +189,16 @@ 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]
@@ -305,18 +306,6 @@ theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a :
   · 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
 
-@[simp] protected theorem neg_inj {a b : Int} : -a = -b ↔ a = b :=
+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)
@@ -91,7 +91,7 @@ theorem add_neg_one (i : Int) : i + -1 = i - 1 := rfl
 
 /- ## basic properties of subNatNat -/
 
-@[elab_as_elim]
+-- @[elabAsElim] -- TODO(Mario): unexpected eliminator resulting type
 theorem subNatNat_elim (m n : Nat) (motive : Nat → Nat → Int → Prop)
     (hp : ∀ i n, motive (n + i) n i)
     (hn : ∀ i m, motive m (m + i + 1) -[i+1]) :
@@ -269,17 +269,6 @@ protected theorem add_left_cancel {a b c : Int} (h : a + b = a + c) : b = c := b
   rw [Int.add_right_neg, Int.add_comm a, ← Int.add_assoc, Int.add_assoc b,
     Int.add_right_neg, Int.add_zero, Int.add_right_neg]
 
-/--
-If a predicate on the integers is invariant under negation,
-then it is sufficient to prove it for the nonnegative integers.
--/
-theorem wlog_sign {P : Int → Prop} (inv : ∀ a, P a ↔ P (-a)) (w : ∀ n : Nat, P n) (a : Int) : P a := by
-  cases a with
-  | ofNat n => exact w n
-  | negSucc n =>
-    rw [negSucc_eq, ← inv, ← ofNat_succ]
-    apply w
-
 /- ## subtraction -/
 
 @[simp] theorem negSucc_sub_one (n : Nat) : -[n+1] - 1 = -[n + 1 +1] := rfl

src/Init/Data/Int/LemmasAux.lean

@@ -46,52 +46,4 @@ 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
-
-@[simp] protected theorem neg_nonpos_iff (i : Int) : -i ≤ 0 ↔ 0 ≤ i := by omega
-
-@[simp] theorem zero_le_ofNat (n : Nat) : 0 ≤ ((no_index (OfNat.ofNat n)) : Int) :=
-  ofNat_nonneg _
-
-@[simp] theorem neg_natCast_le_natCast (n m : Nat) : -(n : Int) ≤ (m : Int) :=
-  Int.le_trans (by simp) (ofNat_zero_le m)
-
-@[simp] theorem neg_natCast_le_ofNat (n m : Nat) : -(n : Int) ≤ (no_index (OfNat.ofNat m)) :=
-  Int.le_trans (by simp) (ofNat_zero_le m)
-
-@[simp] theorem neg_ofNat_le_ofNat (n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (no_index (OfNat.ofNat m)) :=
-  Int.le_trans (by simp) (ofNat_zero_le m)
-
-@[simp] theorem neg_ofNat_le_natCast (n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (m : Int) :=
-  Int.le_trans (by simp) (ofNat_zero_le m)
-
 end Int

src/Init/Data/Int/Linear.lean

@@ -9,7 +9,6 @@ import Init.Data.Prod
 import Init.Data.Int.Lemmas
 import Init.Data.Int.LemmasAux
 import Init.Data.Int.DivMod.Bootstrap
-import Init.Data.Int.Cooper
 import Init.Data.Int.Gcd
 import Init.Data.RArray
 import Init.Data.AC
@@ -187,13 +186,14 @@ theorem cmod_gt_of_pos (a : Int) {b : Int} (h : 0 < b) : cmod a b > -b :=
 
 theorem cmod_nonpos (a : Int) {b : Int} (h : b ≠ 0) : cmod a b ≤ 0 := by
   have := Int.neg_le_neg (Int.emod_nonneg (-a) h)
-  simpa [cmod] using this
+  simp at this
+  assumption
 
 theorem cmod_eq_zero_iff_emod_eq_zero (a b : Int) : cmod a b = 0 ↔ a%b = 0 := by
   unfold cmod
   have := @Int.emod_eq_emod_iff_emod_sub_eq_zero  b b a
   simp at this
-  simp [Int.neg_emod_eq_sub_emod, ← this, Eq.comm]
+  simp [Int.neg_emod, ← this, Eq.comm]
 
 private abbrev div_mul_cancel_of_mod_zero :=
   @Int.ediv_mul_cancel_of_emod_eq_zero
@@ -250,24 +250,14 @@ def Poly.divCoeffs (k : Int) : Poly → Bool
 /--
 `p.mul k` multiplies all coefficients and constant of the polynomial `p` by `k`.
 -/
-def Poly.mul' (p : Poly) (k : Int) : Poly :=
+def Poly.mul (p : Poly) (k : Int) : Poly :=
   match p with
   | .num k' => .num (k*k')
-  | .add k' v p => .add (k*k') v (mul' p k)
-
-def Poly.mul (p : Poly) (k : Int) : Poly :=
-  if k == 0 then
-    .num 0
-  else
-    p.mul' k
+  | .add k' v p => .add (k*k') v (mul p k)
 
 @[simp] theorem Poly.denote_mul (ctx : Context) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
-  simp [mul]
-  split
-  next => simp [*, denote]
-  next =>
-    induction p <;> simp [mul', denote, *]
-    rw [Int.mul_assoc, Int.mul_add]
+  induction p <;> simp [mul, denote, *]
+  rw [Int.mul_assoc, Int.mul_add]
 
 attribute [local simp] Int.add_comm Int.add_assoc Int.add_left_comm Int.add_mul Int.mul_add
 attribute [local simp] Poly.insert Poly.denote Poly.norm Poly.addConst
@@ -541,9 +531,8 @@ def Poly.isValidLe (p : Poly) : Bool :=
   | .num k => k ≤ 0
   | _ => false
 
-attribute [-simp] Int.not_le in
 theorem le_eq_false (ctx : Context) (lhs rhs : Expr) : (lhs.sub rhs).norm.isUnsatLe → (lhs.denote ctx ≤ rhs.denote ctx) = False := by
-  simp only [Poly.isUnsatLe] <;> split <;> simp
+  simp [Poly.isUnsatLe] <;> split <;> simp
   next p k h =>
     intro h'
     replace h := congrArg (Poly.denote ctx) h
@@ -831,7 +820,7 @@ def le_neg_cert (p₁ p₂ : Poly) : Bool :=
 theorem le_neg (ctx : Context) (p₁ p₂ : Poly) : le_neg_cert p₁ p₂ → ¬ p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
   simp [le_neg_cert]
   intro; subst p₂; simp; intro h
-  replace h : _ + 1 ≤ -0 := Int.neg_lt_neg h
+  replace h : _ + 1 ≤ -0 := Int.neg_lt_neg <| Int.lt_of_not_ge h
   simp at h
   exact h
 
@@ -855,28 +844,11 @@ theorem le_combine (ctx : Context) (p₁ p₂ p₃ : Poly)
   · rw [← Int.zero_mul (Poly.denote ctx p₂)]; apply Int.mul_le_mul_of_nonpos_right <;> simp [*]
   · rw [← Int.zero_mul (Poly.denote ctx p₁)]; apply Int.mul_le_mul_of_nonpos_right <;> simp [*]
 
-def le_combine_coeff_cert (p₁ p₂ p₃ : Poly) (k : Int) : Bool :=
-  let a₁ := p₁.leadCoeff.natAbs
-  let a₂ := p₂.leadCoeff.natAbs
-  let p  := p₁.mul a₂ |>.combine (p₂.mul a₁)
-  k > 0 && (p.divCoeffs k && p₃ == p.div k)
-
-theorem le_combine_coeff (ctx : Context) (p₁ p₂ p₃ : Poly) (k : Int)
-    : le_combine_coeff_cert p₁ p₂ p₃ k → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
-  simp only [le_combine_coeff_cert, gt_iff_lt, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, and_imp]
-  let a₁ := p₁.leadCoeff.natAbs
-  let a₂ := p₂.leadCoeff.natAbs
-  generalize h : (p₁.mul a₂ |>.combine (p₂.mul a₁)) = p
-  intro h₁ h₂ h₃ h₄ h₅
-  have := le_combine ctx p₁ p₂ p
-  simp only [le_combine_cert, beq_iff_eq] at this
-  have aux₁ := this h.symm h₄ h₅
-  have := le_coeff ctx p p₃ k
-  simp only [le_coeff_cert, gt_iff_lt, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, and_imp] at this
-  exact this h₁ h₂ h₃ aux₁
-
 theorem le_unsat (ctx : Context) (p : Poly) : p.isUnsatLe → p.denote' ctx ≤ 0 → False := by
   simp [Poly.isUnsatLe]; split <;> simp
+  intro h₁ h₂
+  have := Int.lt_of_le_of_lt h₂ h₁
+  simp at this
 
 theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm == p₂) : p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
   simp at h
@@ -1018,7 +990,7 @@ theorem eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly)
   intro h
   intro; subst p₃
   intro h₁ h₂
-  simp [*, -Int.neg_nonpos_iff]
+  simp [*]
   replace h₂ := Int.mul_le_mul_of_nonpos_left h₂ h; simp at h₂; clear h
   rw [← Int.neg_zero]
   apply Int.neg_le_neg
@@ -1034,715 +1006,6 @@ theorem eq_of_core (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
   intro; subst p₃; simp
   intro h; rw [h, ←Int.sub_eq_add_neg, Int.sub_self]
 
-def Poly.isUnsatDiseq (p : Poly) : Bool :=
-  match p with
-  | .num 0 => true
-  | _ => false
-
-theorem diseq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm == p₂) : p₁.denote' ctx ≠ 0 → p₂.denote' ctx ≠ 0 := by
-  simp at h
-  replace h := congrArg (Poly.denote ctx) h
-  simp at h
-  simp [*]
-
-theorem diseq_coeff (ctx : Context) (p p' : Poly) (k : Int) : eq_coeff_cert p p' k → p.denote' ctx ≠ 0 → p'.denote' ctx ≠ 0 := by
-  simp [eq_coeff_cert]
-  intro _ _; simp [mul_eq_zero_iff, *]
-
-theorem diseq_neg (ctx : Context) (p p' : Poly) : p' == p.mul (-1) → p.denote' ctx ≠ 0 → p'.denote' ctx ≠ 0 := by
-  simp; intro _ _; simp [mul_eq_zero_iff, *]
-
-theorem diseq_unsat (ctx : Context) (p : Poly) : p.isUnsatDiseq → p.denote' ctx ≠ 0 → False := by
-  simp [Poly.isUnsatDiseq] <;> split <;> simp
-
-def diseq_eq_subst_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
-  let a := p₁.coeff x
-  let b := p₂.coeff x
-  a != 0 && p₃ == (p₁.mul b |>.combine (p₂.mul (-a)))
-
-theorem eq_diseq_subst (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
-    : diseq_eq_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
-  simp [diseq_eq_subst_cert]
-  intros _ _; subst p₃
-  intro h₁ h₂
-  simp [*]
-
-theorem diseq_of_core (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
-    : eq_of_core_cert p₁ p₂ p₃ → p₁.denote' ctx ≠ p₂.denote' ctx → p₃.denote' ctx ≠ 0 := by
-  simp [eq_of_core_cert]
-  intro; subst p₃; simp
-  intro h; rw [← Int.sub_eq_zero] at h
-  rw [←Int.sub_eq_add_neg]; assumption
-
-def eq_of_le_ge_cert (p₁ p₂ : Poly) : Bool :=
-  p₂ == p₁.mul (-1)
-
-theorem eq_of_le_ge (ctx : Context) (p₁ : Poly) (p₂ : Poly)
-    : eq_of_le_ge_cert p₁ p₂ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₁.denote' ctx = 0 := by
-  simp [eq_of_le_ge_cert]
-  intro; subst p₂; simp [-Int.neg_nonpos_iff]
-  intro h₁ h₂
-  replace h₂ := Int.neg_le_of_neg_le h₂; simp at h₂
-  simp [Int.eq_iff_le_and_ge, *]
-
-def le_of_le_diseq_cert (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
-  -- Remark: we can generate two different certificates in the future, and avoid the `||` in the certificate.
-  (p₂ == p₁ || p₂ == p₁.mul (-1)) &&
-  p₃ == p₁.addConst 1
-
-theorem le_of_le_diseq (ctx : Context) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
-    : le_of_le_diseq_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≤ 0 := by
-  simp [le_of_le_diseq_cert]
-  have (a : Int) : a ≤ 0 → ¬ a = 0 → 1 + a ≤ 0 := by
-    intro h₁ h₂; cases (Int.lt_or_gt_of_ne h₂)
-    next => apply Int.le_of_lt_add_one; rw [Int.add_comm, Int.add_lt_add_iff_right]; assumption
-    next h => have := Int.lt_of_le_of_lt h₁ h; simp at this
-  intro h; cases h <;> intro <;> subst p₂ p₃ <;> simp <;> apply this
-
-def diseq_split_cert (p₁ p₂ p₃ : Poly) : Bool :=
-  p₂ == p₁.addConst 1 &&
-  p₃ == (p₁.mul (-1)).addConst 1
-
-theorem diseq_split (ctx : Context) (p₁ p₂ p₃ : Poly)
-    : diseq_split_cert p₁ p₂ p₃ → p₁.denote' ctx ≠ 0 → p₂.denote' ctx ≤ 0 ∨ p₃.denote' ctx ≤ 0 := by
-  simp [diseq_split_cert]
-  intro _ _; subst p₂ p₃; simp
-  generalize p₁.denote ctx = p
-  intro h; cases Int.lt_or_gt_of_ne h
-  next h => have := Int.add_one_le_of_lt h; rw [Int.add_comm]; simp [*]
-  next h => have := Int.add_one_le_of_lt (Int.neg_lt_neg h); simp at this; simp [*]
-
-theorem diseq_split_resolve (ctx : Context) (p₁ p₂ p₃ : Poly)
-    : diseq_split_cert p₁ p₂ p₃ → p₁.denote' ctx ≠ 0 → ¬p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
-  intro h₁ h₂ h₃
-  exact (diseq_split ctx p₁ p₂ p₃ h₁ h₂).resolve_left h₃
-
-def OrOver (n : Nat) (p : Nat → Prop) : Prop :=
-  match n with
-  | 0 => False
-  | n+1 => p n ∨ OrOver n p
-
-theorem orOver_one {p} : OrOver 1 p → p 0 := by simp [OrOver]
-
-theorem orOver_resolve {n p} : OrOver (n+1) p → ¬ p n → OrOver n p := by
-  intro h₁ h₂
-  rw [OrOver] at h₁
-  cases h₁
-  · contradiction
-  · assumption
-
-def OrOver_cases_type (n : Nat) (p : Nat → Prop) : Prop :=
-  match n with
-  | 0 => p 0
-  | n+1 => ¬ p (n+1) → OrOver_cases_type n p
-
-theorem orOver_cases {n p} : OrOver (n+1) p → OrOver_cases_type n p := by
-  induction n <;> simp [OrOver_cases_type]
-  next => exact orOver_one
-  next n ih => intro h₁ h₂; exact ih (orOver_resolve h₁ h₂)
-
-private theorem orOver_of_p {i n p} (h₁ : i < n) (h₂ : p i) : OrOver n p := by
-  induction n
-  next => simp at h₁
-  next n ih =>
-    simp [OrOver]
-    cases Nat.eq_or_lt_of_le <| Nat.le_of_lt_add_one h₁
-    next h => subst i; exact Or.inl h₂
-    next h => exact Or.inr (ih h)
-
-private theorem orOver_of_exists {n p} : (∃ k, k < n ∧ p k) → OrOver n p := by
-  intro ⟨k, h₁, h₂⟩
-  apply orOver_of_p h₁ h₂
-
-private theorem ofNat_toNat {a : Int} : a ≥ 0 → Int.ofNat a.toNat = a := by cases a <;> simp
-private theorem cast_toNat {a : Int} : a ≥ 0 → a.toNat = a := by cases a <;> simp
-private theorem ofNat_lt {a : Int} {n : Nat} : a ≥ 0 → a < Int.ofNat n → a.toNat < n := by cases a <;> simp
-@[local simp] private theorem lcm_neg_left (a b : Int) : Int.lcm (-a) b = Int.lcm a b := by simp [Int.lcm]
-@[local simp] private theorem lcm_neg_right (a b : Int) : Int.lcm a (-b) = Int.lcm a b := by simp [Int.lcm]
-@[local simp] private theorem gcd_neg_left (a b : Int) : Int.gcd (-a) b = Int.gcd a b := by simp [Int.gcd]
-@[local simp] private theorem gcd_neg_right (a b : Int) : Int.gcd a (-b) = Int.gcd a b := by simp [Int.gcd]
-@[local simp] private theorem gcd_zero (a : Int) : Int.gcd a 0 = a.natAbs := by simp [Int.gcd]
-@[local simp] private theorem lcm_one (a : Int) : Int.lcm a 1 = a.natAbs := by simp [Int.lcm]
-
-private theorem cooper_dvd_left_core
-    {a b c d s p q x : Int} (a_neg : a < 0) (b_pos : 0 < b) (d_pos : 0 < d)
-    (h₁ : a * x + p ≤ 0)
-    (h₂ : b * x + q ≤ 0)
-    (h₃ : d ∣ c * x + s)
-    : OrOver (Int.lcm a (a * d / Int.gcd (a * d) c)) fun k =>
-        b * p + (-a) * q + b * k ≤ 0 ∧
-        a ∣ p + k ∧
-        a * d ∣ c * p + (-a) * s + c * k := by
-  have a_pos' : 0 < -a := by apply Int.neg_pos_of_neg; assumption
-  have h₁'    : p ≤ (-a)*x := by rw [Int.neg_mul, ← Lean.Omega.Int.add_le_zero_iff_le_neg']; assumption
-  have h₂'    : b * x ≤ -q := by rw [← Lean.Omega.Int.add_le_zero_iff_le_neg', Int.add_comm]; assumption
-  have ⟨k, h₁, h₂, h₃, h₄, h₅⟩ := Int.cooper_resolution_dvd_left a_pos' b_pos d_pos |>.mp ⟨x, h₁', h₂', h₃⟩
-  rw [Int.neg_mul] at h₂
-  simp only [Int.neg_mul, neg_gcd, lcm_neg_left, Int.mul_neg, Int.neg_neg, Int.neg_dvd] at *
-  rw [Int.neg_ediv_of_dvd Int.gcd_dvd_left] at h₂
-  simp only [lcm_neg_right] at h₂
-  have : c * k + c * p + -(a * s) = c * p + -(a * s) + c * k := by ac_rfl
-  rw [this] at h₅; clear this
-  rw [← ofNat_toNat h₁] at h₃ h₄ h₅
-  rw [Int.add_comm] at h₄
-  have := ofNat_lt h₁ h₂
-  apply orOver_of_exists
-  replace h₃ := Int.add_le_add_right h₃ (-(a*q)); rw [Int.add_right_neg] at h₃
-  have : b * Int.ofNat k.toNat + b * p + -(a * q) = b * p + -(a * q) + b * Int.ofNat k.toNat := by ac_rfl
-  rw [this] at h₃
-  exists k.toNat
-
-def cooper_dvd_left_cert (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : Bool :=
-  p₁.casesOn (fun _ => false) fun a x _ =>
-  p₂.casesOn (fun _ => false) fun b y _ =>
-  p₃.casesOn (fun _ => false) fun c z _ =>
-   .and (x == y) <| .and (x == z) <|
-   .and (a < 0)  <| .and (b > 0)  <|
-   .and (d > 0)  <| n == Int.lcm a (a * d / Int.gcd (a * d) c)
-
-def Poly.tail (p : Poly) : Poly :=
-  match p with
-  | .add _ _ p => p
-  | _ => p
-
-def cooper_dvd_left_split (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) : Prop :=
-  let p  := p₁.tail
-  let q  := p₂.tail
-  let s  := p₃.tail
-  let a  := p₁.leadCoeff
-  let b  := p₂.leadCoeff
-  let c  := p₃.leadCoeff
-  let p₁ := p.mul b |>.combine (q.mul (-a))
-  let p₂ := p.mul c |>.combine (s.mul (-a))
-  (p₁.addConst (b*k)).denote' ctx ≤ 0
-  ∧ a ∣ (p.addConst k).denote' ctx
-  ∧ a*d ∣ (p₂.addConst (c*k)).denote' ctx
-
-private theorem denote'_mul_combine_mul_addConst_eq (ctx : Context) (p q : Poly) (a b c : Int)
-    : ((p.mul b |>.combine (q.mul a)).addConst c).denote' ctx = b*p.denote ctx + a*q.denote ctx + c := by
-  simp
-
-private theorem denote'_addConst_eq (ctx : Context) (p : Poly) (a : Int)
-    : (p.addConst a).denote' ctx = p.denote ctx + a := by
-  simp
-
-theorem cooper_dvd_left (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat)
-    : cooper_dvd_left_cert p₁ p₂ p₃ d n
-      → p₁.denote' ctx ≤ 0
-      → p₂.denote' ctx ≤ 0
-      → d ∣ p₃.denote' ctx
-      → OrOver n (cooper_dvd_left_split ctx p₁ p₂ p₃ d) := by
- unfold cooper_dvd_left_split
- cases p₁ <;> cases p₂ <;> cases p₃ <;> simp [cooper_dvd_left_cert, Poly.tail, -Poly.denote'_eq_denote]
- next a x p b y q c z s =>
- intro _ _; subst y z
- intro ha hb hd
- intro; subst n
- simp only [Poly.denote'_add, Poly.leadCoeff]
- intro h₁ h₂ h₃
- simp only [denote'_mul_combine_mul_addConst_eq]
- simp only [denote'_addConst_eq]
- exact cooper_dvd_left_core ha hb hd h₁ h₂ h₃
-
-def cooper_dvd_left_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (b : Int) (p' : Poly) : Bool :=
-  let p  := p₁.tail
-  let q  := p₂.tail
-  let a  := p₁.leadCoeff
-  let p₁ := p.mul b |>.combine (q.mul (-a))
-  p₂.leadCoeff == b && p' == p₁.addConst (b*k)
-
-theorem cooper_dvd_left_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (b : Int) (p' : Poly)
-    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_ineq_cert p₁ p₂ k b p' → p'.denote' ctx ≤ 0 := by
-  simp [cooper_dvd_left_split_ineq_cert, cooper_dvd_left_split]
-  intros; subst p' b; simp [denote'_mul_combine_mul_addConst_eq]; assumption
-
-def cooper_dvd_left_split_dvd1_cert (p₁ p' : Poly) (a : Int) (k : Int) : Bool :=
-  a == p₁.leadCoeff && p' == p₁.tail.addConst k
-
-theorem cooper_dvd_left_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (a : Int) (p' : Poly)
-    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_dvd1_cert p₁ p' a k → a ∣ p'.denote' ctx := by
-  simp [cooper_dvd_left_split_dvd1_cert, cooper_dvd_left_split]
-  intros; subst a p'; simp; assumption
-
-def cooper_dvd_left_split_dvd2_cert (p₁ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly): Bool :=
-  let p  := p₁.tail
-  let s  := p₃.tail
-  let a  := p₁.leadCoeff
-  let c  := p₃.leadCoeff
-  let p₂ := p.mul c |>.combine (s.mul (-a))
-  d' == a*d && p' == p₂.addConst (c*k)
-
-theorem cooper_dvd_left_split_dvd2 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly)
-    : cooper_dvd_left_split ctx p₁ p₂ p₃ d k → cooper_dvd_left_split_dvd2_cert p₁ p₃ d k d' p' → d' ∣ p'.denote' ctx := by
-  simp [cooper_dvd_left_split_dvd2_cert, cooper_dvd_left_split]
-  intros; subst d' p'; simp; assumption
-
-private theorem cooper_left_core
-    {a b p q x : Int} (a_neg : a < 0) (b_pos : 0 < b)
-    (h₁ : a * x + p ≤ 0)
-    (h₂ : b * x + q ≤ 0)
-    : OrOver a.natAbs fun k =>
-        b * p + (-a) * q + b * k ≤ 0 ∧
-        a ∣ p + k := by
-  have d_pos : (0 : Int) < 1 := by decide
-  have h₃ : 1 ∣ 0*x + 0 := Int.one_dvd _
-  have h := cooper_dvd_left_core a_neg b_pos d_pos h₁ h₂ h₃
-  simp only [Int.mul_one, gcd_zero, ofNat_natAbs_of_nonpos (Int.le_of_lt a_neg), Int.ediv_neg,
-    Int.ediv_self (Int.ne_of_lt a_neg), Int.reduceNeg, lcm_neg_right, lcm_one,
-    Int.add_left_comm, Int.zero_mul, Int.mul_zero, Int.add_zero, Int.dvd_zero,
-    and_true] at h
-  assumption
-
-def cooper_left_cert (p₁ p₂ : Poly) (n : Nat) : Bool :=
-  p₁.casesOn (fun _ => false) fun a x _ =>
-  p₂.casesOn (fun _ => false) fun b y _ =>
-   .and (x == y) <| .and (a < 0)  <| .and (b > 0)  <|
-   n == a.natAbs
-
-def cooper_left_split (ctx : Context) (p₁ p₂ : Poly) (k : Nat) : Prop :=
-  let p  := p₁.tail
-  let q  := p₂.tail
-  let a  := p₁.leadCoeff
-  let b  := p₂.leadCoeff
-  let p₁ := p.mul b |>.combine (q.mul (-a))
-  (p₁.addConst (b*k)).denote' ctx ≤ 0
-  ∧ a ∣ (p.addConst k).denote' ctx
-
-theorem cooper_left (ctx : Context) (p₁ p₂ : Poly) (n : Nat)
-    : cooper_left_cert p₁ p₂ n
-      → p₁.denote' ctx ≤ 0
-      → p₂.denote' ctx ≤ 0
-      → OrOver n (cooper_left_split ctx p₁ p₂) := by
- unfold cooper_left_split
- cases p₁ <;> cases p₂ <;> simp [cooper_left_cert, Poly.tail, -Poly.denote'_eq_denote]
- next a x p b y q =>
- intro; subst y
- intro ha hb
- intro; subst n
- simp only [Poly.denote'_add, Poly.leadCoeff]
- intro h₁ h₂
- have := cooper_left_core ha hb h₁ h₂
- simp only [denote'_mul_combine_mul_addConst_eq]
- simp only [denote'_addConst_eq]
- assumption
-
-def cooper_left_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (b : Int) (p' : Poly) : Bool :=
-  let p  := p₁.tail
-  let q  := p₂.tail
-  let a  := p₁.leadCoeff
-  let p₁ := p.mul b |>.combine (q.mul (-a))
-  p₂.leadCoeff == b && p' == p₁.addConst (b*k)
-
-theorem cooper_left_split_ineq (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b : Int) (p' : Poly)
-    : cooper_left_split ctx p₁ p₂ k → cooper_left_split_ineq_cert p₁ p₂ k b p' → p'.denote' ctx ≤ 0 := by
-  simp [cooper_left_split_ineq_cert, cooper_left_split]
-  intros; subst p' b; simp [denote'_mul_combine_mul_addConst_eq]; assumption
-
-def cooper_left_split_dvd_cert (p₁ p' : Poly) (a : Int) (k : Int) : Bool :=
-  a == p₁.leadCoeff && p' == p₁.tail.addConst k
-
-theorem cooper_left_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (a : Int) (p' : Poly)
-    : cooper_left_split ctx p₁ p₂ k → cooper_left_split_dvd_cert p₁ p' a k → a ∣ p'.denote' ctx := by
-  simp [cooper_left_split_dvd_cert, cooper_left_split]
-  intros; subst a p'; simp; assumption
-
-private theorem cooper_dvd_right_core
-    {a b c d s p q x : Int} (a_neg : a < 0) (b_pos : 0 < b) (d_pos : 0 < d)
-    (h₁ : a * x + p ≤ 0)
-    (h₂ : b * x + q ≤ 0)
-    (h₃ : d ∣ c * x + s)
-    : OrOver (Int.lcm b (b * d / Int.gcd (b * d) c)) fun k =>
-      b * p + (-a) * q + (-a) * k ≤ 0 ∧
-      b ∣ q + k ∧
-      b * d ∣ (-c) * q + b * s + (-c) * k := by
-  have a_pos' : 0 < -a := by apply Int.neg_pos_of_neg; assumption
-  have h₁'    : p ≤ (-a)*x := by rw [Int.neg_mul, ← Lean.Omega.Int.add_le_zero_iff_le_neg']; assumption
-  have h₂'    : b * x ≤ -q := by rw [← Lean.Omega.Int.add_le_zero_iff_le_neg', Int.add_comm]; assumption
-  have ⟨k, h₁, h₂, h₃, h₄, h₅⟩ := Int.cooper_resolution_dvd_right a_pos' b_pos d_pos |>.mp ⟨x, h₁', h₂', h₃⟩
-  simp only [Int.neg_mul, neg_gcd, lcm_neg_left, Int.mul_neg, Int.neg_neg, Int.neg_dvd] at *
-  apply orOver_of_exists
-  have hlt := ofNat_lt h₁ h₂
-  replace h₃ := Int.add_le_add_right h₃ (-(a*q)); rw [Int.add_right_neg] at h₃
-  have : -(a * k) + b * p + -(a * q) = b * p + -(a * q) + -(a * k) := by ac_rfl
-  rw [this] at h₃; clear this
-  rw [Int.sub_neg, Int.add_comm] at h₄
-  have : -(c * k) + -(c * q) + b * s = -(c * q) + b * s + -(c * k) := by ac_rfl
-  rw [this] at h₅; clear this
-  exists k.toNat
-  simp only [hlt, true_and, and_true, cast_toNat h₁, h₃, h₄, h₅]
-
-def cooper_dvd_right_cert (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : Bool :=
-  p₁.casesOn (fun _ => false) fun a x _ =>
-  p₂.casesOn (fun _ => false) fun b y _ =>
-  p₃.casesOn (fun _ => false) fun c z _ =>
-   .and (x == y) <| .and (x == z) <|
-   .and (a < 0)  <| .and (b > 0)  <|
-   .and (d > 0)  <| n == Int.lcm b (b * d / Int.gcd (b * d) c)
-
-def cooper_dvd_right_split (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) : Prop :=
-  let p  := p₁.tail
-  let q  := p₂.tail
-  let s  := p₃.tail
-  let a  := p₁.leadCoeff
-  let b  := p₂.leadCoeff
-  let c  := p₃.leadCoeff
-  let p₁ := p.mul b |>.combine (q.mul (-a))
-  let p₂ := q.mul (-c) |>.combine (s.mul b)
-  (p₁.addConst ((-a)*k)).denote' ctx ≤ 0
-  ∧ b ∣ (q.addConst k).denote' ctx
-  ∧ b*d ∣ (p₂.addConst ((-c)*k)).denote' ctx
-
-theorem cooper_dvd_right (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat)
-    : cooper_dvd_right_cert p₁ p₂ p₃ d n
-      → p₁.denote' ctx ≤ 0
-      → p₂.denote' ctx ≤ 0
-      → d ∣ p₃.denote' ctx
-      → OrOver n (cooper_dvd_right_split ctx p₁ p₂ p₃ d) := by
- unfold cooper_dvd_right_split
- cases p₁ <;> cases p₂ <;> cases p₃ <;> simp [cooper_dvd_right_cert, Poly.tail, -Poly.denote'_eq_denote]
- next a x p b y q c z s =>
- intro _ _; subst y z
- intro ha hb hd
- intro; subst n
- simp only [Poly.denote'_add, Poly.leadCoeff]
- intro h₁ h₂ h₃
- have := cooper_dvd_right_core ha hb hd h₁ h₂ h₃
- simp only [denote'_mul_combine_mul_addConst_eq]
- simp only [denote'_addConst_eq, ←Int.neg_mul]
- exact cooper_dvd_right_core ha hb hd h₁ h₂ h₃
-
-def cooper_dvd_right_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (a : Int) (p' : Poly) : Bool :=
-  let p  := p₁.tail
-  let q  := p₂.tail
-  let b  := p₂.leadCoeff
-  let p₂ := p.mul b |>.combine (q.mul (-a))
-  p₁.leadCoeff == a && p' == p₂.addConst ((-a)*k)
-
-theorem cooper_dvd_right_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (a : Int) (p' : Poly)
-    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_ineq_cert p₁ p₂ k a p' → p'.denote' ctx ≤ 0 := by
-  simp [cooper_dvd_right_split_ineq_cert, cooper_dvd_right_split]
-  intros; subst a p'; simp [denote'_mul_combine_mul_addConst_eq]; assumption
-
-def cooper_dvd_right_split_dvd1_cert (p₂ p' : Poly) (b : Int) (k : Int) : Bool :=
-  b == p₂.leadCoeff && p' == p₂.tail.addConst k
-
-theorem cooper_dvd_right_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (b : Int) (p' : Poly)
-    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd1_cert p₂ p' b k → b ∣ p'.denote' ctx := by
-  simp [cooper_dvd_right_split_dvd1_cert, cooper_dvd_right_split]
-  intros; subst b p'; simp; assumption
-
-def cooper_dvd_right_split_dvd2_cert (p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly): Bool :=
-  let q  := p₂.tail
-  let s  := p₃.tail
-  let b  := p₂.leadCoeff
-  let c  := p₃.leadCoeff
-  let p₂ := q.mul (-c) |>.combine (s.mul b)
-  d' == b*d && p' == p₂.addConst ((-c)*k)
-
-theorem cooper_dvd_right_split_dvd2 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly)
-    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd2_cert p₂ p₃ d k d' p' → d' ∣ p'.denote' ctx := by
-  simp [cooper_dvd_right_split_dvd2_cert, cooper_dvd_right_split]
-  intros; subst d' p'; simp; assumption
-
-private theorem cooper_right_core
-    {a b p q x : Int} (a_neg : a < 0) (b_pos : 0 < b)
-    (h₁ : a * x + p ≤ 0)
-    (h₂ : b * x + q ≤ 0)
-    : OrOver b.natAbs fun k =>
-      b * p + (-a) * q + (-a) * k ≤ 0 ∧
-      b ∣ q + k := by
-  have d_pos : (0 : Int) < 1 := by decide
-  have h₃ : 1 ∣ 0*x + 0 := Int.one_dvd _
-  have h := cooper_dvd_right_core a_neg b_pos d_pos h₁ h₂ h₃
-  simp only [Int.mul_one, gcd_zero, Int.natAbs_of_nonneg (Int.le_of_lt b_pos), Int.ediv_neg,
-    Int.ediv_self (Int.ne_of_gt b_pos), Int.reduceNeg, lcm_neg_right, lcm_one,
-    Int.add_left_comm, Int.zero_mul, Int.mul_zero, Int.add_zero, Int.dvd_zero,
-    and_true, Int.neg_zero] at h
-  assumption
-
-def cooper_right_cert (p₁ p₂ : Poly) (n : Nat) : Bool :=
-  p₁.casesOn (fun _ => false) fun a x _ =>
-  p₂.casesOn (fun _ => false) fun b y _ =>
-  .and (x == y) <| .and (a < 0)  <| .and (b > 0) <| n == b.natAbs
-
-def cooper_right_split (ctx : Context) (p₁ p₂ : Poly) (k : Nat) : Prop :=
-  let p  := p₁.tail
-  let q  := p₂.tail
-  let a  := p₁.leadCoeff
-  let b  := p₂.leadCoeff
-  let p₁ := p.mul b |>.combine (q.mul (-a))
-  (p₁.addConst ((-a)*k)).denote' ctx ≤ 0
-  ∧ b ∣ (q.addConst k).denote' ctx
-
-theorem cooper_right (ctx : Context) (p₁ p₂ : Poly) (n : Nat)
-    : cooper_right_cert p₁ p₂ n
-      → p₁.denote' ctx ≤ 0
-      → p₂.denote' ctx ≤ 0
-      → OrOver n (cooper_right_split ctx p₁ p₂) := by
- unfold cooper_right_split
- cases p₁ <;> cases p₂ <;> simp [cooper_right_cert, Poly.tail, -Poly.denote'_eq_denote]
- next a x p b y q =>
- intro; subst y
- intro ha hb
- intro; subst n
- simp only [Poly.denote'_add, Poly.leadCoeff]
- intro h₁ h₂
- have := cooper_right_core ha hb h₁ h₂
- simp only [denote'_mul_combine_mul_addConst_eq]
- simp only [denote'_addConst_eq, ←Int.neg_mul]
- assumption
-
-def cooper_right_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (a : Int) (p' : Poly) : Bool :=
-  let p  := p₁.tail
-  let q  := p₂.tail
-  let b  := p₂.leadCoeff
-  let p₂ := p.mul b |>.combine (q.mul (-a))
-  p₁.leadCoeff == a && p' == p₂.addConst ((-a)*k)
-
-theorem cooper_right_split_ineq (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (a : Int) (p' : Poly)
-    : cooper_right_split ctx p₁ p₂ k → cooper_right_split_ineq_cert p₁ p₂ k a p' → p'.denote' ctx ≤ 0 := by
-  simp [cooper_right_split_ineq_cert, cooper_right_split]
-  intros; subst a p'; simp [denote'_mul_combine_mul_addConst_eq]; assumption
-
-def cooper_right_split_dvd_cert (p₂ p' : Poly) (b : Int) (k : Int) : Bool :=
-  b == p₂.leadCoeff && p' == p₂.tail.addConst k
-
-theorem cooper_right_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b : Int) (p' : Poly)
-    : cooper_right_split ctx p₁ p₂ k → cooper_right_split_dvd_cert p₂ p' b k → b ∣ p'.denote' ctx := by
-  simp [cooper_right_split_dvd_cert, cooper_right_split]
-  intros; subst b p'; simp; assumption
-
-private theorem one_emod_eq_one {a : Int} (h : a > 1) : 1 % a = 1 := by
-  have aux₁ := Int.ediv_add_emod 1 a
-  have : 1 / a = 0 := Int.ediv_eq_zero_of_lt (by decide) h
-  simp [this] at aux₁
-  assumption
-
-private theorem ex_of_dvd {α β a b d x : Int}
-    (h₀ : d > 1)
-    (h₁ : d ∣ a*x + b)
-    (h₂ : α * a + β * d = 1)
-    : ∃ k, x = k * d + (- α * b) % d := by
-  have ⟨k, h₁⟩ := h₁
-  have aux₁ : (α * a) % d = 1 := by
-    replace h₂ := congrArg (· % d) h₂; simp at h₂
-    rw [one_emod_eq_one h₀] at h₂
-    assumption
-  have : ((α * a) * x) % d = (- α * b) % d := by
-    replace h₁ := congrArg (α * ·) h₁; simp only at h₁
-    rw [Int.mul_add] at h₁
-    replace h₁ := congrArg (· - α * b) h₁; simp only [Int.add_sub_cancel] at h₁
-    rw [← Int.mul_assoc, Int.mul_left_comm, Int.sub_eq_add_neg] at h₁
-    replace h₁ := congrArg (· % d) h₁; simp only at h₁
-    rw [Int.add_emod, Int.mul_emod_right, Int.zero_add, Int.emod_emod, ← Int.neg_mul] at h₁
-    assumption
-  have : x % d = (- α * b) % d := by
-    rw [Int.mul_emod, aux₁, Int.one_mul, Int.emod_emod] at this
-    assumption
-  have : x = (x / d)*d + (- α * b) % d := by
-    conv => lhs; rw [← Int.ediv_add_emod x d]
-    rw [Int.mul_comm, this]
-  exists x / d
-
-private theorem cdiv_le {a d k : Int} : d > 0 → a ≤ k * d → cdiv a d ≤ k := by
-  intro h₁ h₂
-  simp [cdiv]
-  replace h₂ := Int.neg_le_neg h₂
-  rw [← Int.neg_mul] at h₂
-  replace h₂ := Int.le_ediv_of_mul_le h₁ h₂
-  replace h₂ := Int.neg_le_neg h₂
-  simp at h₂
-  assumption
-
-private theorem cooper_unsat'_helper {a b d c k x : Int}
-    (d_pos : d > 0)
-    (h₁ : x = k * d + c)
-    (h₂ : a ≤ x)
-    (h₃ : x ≤ b)
-    : ¬ b < (cdiv (a - c) d) * d + c := by
-  intro h₄
-  have aux₁ : cdiv (a - c) d ≤ k := by
-    rw [h₁] at h₂
-    replace h₂ := Int.sub_right_le_of_le_add h₂
-    exact cdiv_le d_pos h₂
-  have aux₂ : cdiv (a - c) d * d ≤ k * d := Int.mul_le_mul_of_nonneg_right aux₁ (Int.le_of_lt d_pos)
-  have aux₃ : cdiv (a - c) d * d + c ≤ k * d + c := Int.add_le_add_right aux₂ _
-  have aux₄ : cdiv (a - c) d * d + c ≤ x := by rw [←h₁] at aux₃; assumption
-  have aux₅ : cdiv (a - c) d * d + c ≤ b := Int.le_trans aux₄ h₃
-  have := Int.lt_of_le_of_lt aux₅ h₄
-  exact Int.lt_irrefl _ this
-
-private theorem cooper_unsat' {a c b d e α β x : Int}
-    (h₁ : d > 1)
-    (h₂ : d ∣ c*x + e)
-    (h₃ : α * c + β * d = 1)
-    (h₄ : (-1)*x + a ≤ 0)
-    (h₅ : x + b ≤ 0)
-    (h₆ : -b < cdiv (a - -α * e % d) d * d + -α * e % d)
-    : False := by
-  have ⟨k, h⟩ := ex_of_dvd h₁ h₂ h₃
-  have d_pos : d > 0 := Int.lt_trans (by decide) h₁
-  replace h₄ := Int.le_neg_add_of_add_le h₄; simp at h₄
-  replace h₅ := Int.neg_le_neg (Int.le_neg_add_of_add_le h₅); simp at h₅
-  have := cooper_unsat'_helper d_pos h h₄ h₅
-  exact this h₆
-
-abbrev Poly.casesOnAdd (p : Poly) (k : Int → Var → Poly → Bool) : Bool :=
-  p.casesOn (fun _  => false) k
-
-abbrev Poly.casesOnNum (p : Poly) (k : Int → Bool) : Bool :=
-  p.casesOn k (fun _ _ _ => false)
-
-def cooper_unsat_cert (p₁ p₂ p₃ : Poly) (d : Int) (α β : Int) : Bool :=
-  p₁.casesOnAdd fun k₁ x p₁ =>
-  p₂.casesOnAdd fun k₂ y p₂ =>
-  p₃.casesOnAdd fun c z p₃ =>
-  p₁.casesOnNum fun a =>
-  p₂.casesOnNum fun b =>
-  p₃.casesOnNum fun e =>
-  (k₁ == -1) |>.and (k₂ == 1) |>.and
-  (x == y) |>.and (x == z) |>.and
-  (d > 1) |>.and (α * c + β * d == 1) |>.and
-  (-b < cdiv (a - -α * e % d) d * d + -α * e % d)
-
-theorem cooper_unsat (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (α β : Int)
-   : cooper_unsat_cert p₁ p₂ p₃ d α β →
-     p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → d ∣ p₃.denote' ctx → False := by
-  unfold cooper_unsat_cert <;> cases p₁ <;> cases p₂ <;> cases p₃ <;> simp only [Poly.casesOnAdd,
-    Bool.false_eq_true, Poly.denote'_add, mul_def, add_def, false_implies]
-  next k₁ x p₁ k₂ y p₂ c z p₃ =>
-  cases p₁ <;> cases p₂ <;> cases p₃ <;> simp only [Poly.casesOnNum, Int.reduceNeg,
-    Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq, and_imp, Bool.false_eq_true,
-    mul_def, add_def, false_implies, Poly.denote]
-  next a b e =>
-  intro _ _ _ _; subst k₁ k₂ y z
-  intro h₁ h₃ h₆; generalize Var.denote ctx x = x'
-  intro h₄ h₅ h₂
-  rw [Int.one_mul] at h₅
-  exact cooper_unsat' h₁ h₂ h₃ h₄ h₅ h₆
-
-theorem ediv_emod (x y : Int) : -1 * x + y * (x / y) + x % y = 0 := by
-  rw [Int.add_assoc, Int.ediv_add_emod x y, Int.add_comm]
-  simp
-  rw [← Int.sub_eq_add_neg, Int.sub_self]
-
-theorem emod_nonneg (x y : Int) : y != 0 → -1 * (x % y) ≤ 0 := by
-  simp; intro h
-  have := Int.neg_le_neg (Int.emod_nonneg x h)
-  simp at this
-  assumption
-
-def emod_le_cert (y n : Int) : Bool :=
-  y != 0 && n == 1 - y.natAbs
-
-theorem emod_le (x y : Int) (n : Int) : emod_le_cert y n → x % y + n ≤ 0 := by
-  simp [emod_le_cert]
-  intro h₁
-  cases Int.lt_or_gt_of_ne h₁
-  next h =>
-    rw [Int.ofNat_natAbs_of_nonpos (Int.le_of_lt h)]
-    simp only [Int.sub_neg]
-    intro; subst n
-    rw [Int.add_assoc, Int.add_left_comm]
-    apply Int.add_le_of_le_sub_left
-    rw [Int.zero_sub, Int.add_comm]
-    have : 0 < -y := by
-      have := Int.neg_lt_neg h
-      rw [Int.neg_zero] at this
-      assumption
-    have := Int.emod_lt_of_pos x this
-    rw [Int.emod_neg] at this
-    exact this
-  next h =>
-    rw [Int.natAbs_of_nonneg (Int.le_of_lt h)]
-    intro; subst n
-    rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm]
-    apply Int.add_le_of_le_sub_left
-    simp only [Int.add_comm, Int.sub_neg, Int.add_zero]
-    exact Int.emod_lt_of_pos x h
-
-theorem natCast_nonneg (x : Nat) : (-1:Int) * NatCast.natCast x ≤ 0 := by
-  simp
-
-private theorem dvd_le_tight' {d p b₁ b₂ : Int} (hd : d > 0) (h₁ : d ∣ p + b₁) (h₂ : p + b₂ ≤ 0)
-    : p + (b₁ - d*((b₁-b₂) / d)) ≤ 0 := by
-  have ⟨k, h⟩ := h₁
-  replace h₁ : p = d*k - b₁ := by
-    replace h := congrArg (· - b₁) h
-    simp only [Int.add_sub_cancel] at h
-    assumption
-  replace h₂ : d*k - b₁ + b₂ ≤ 0 := by
-    rw [h₁] at h₂; assumption
-  have : d*k ≤ b₁ - b₂ := by
-    rw [Int.sub_eq_add_neg, Int.add_assoc, Lean.Omega.Int.add_le_zero_iff_le_neg,
-        Int.neg_add, Int.neg_neg, ← Int.sub_eq_add_neg] at h₂
-    assumption
-  replace this : k ≤ (b₁ - b₂)/d := by
-    rw [Int.mul_comm] at this; exact Int.le_ediv_of_mul_le hd this
-  replace this := Int.mul_le_mul_of_nonneg_left this (Int.le_of_lt hd)
-  rw [←h] at this
-  replace this := Int.sub_nonpos_of_le this
-  rw [Int.add_sub_assoc] at this
-  exact this
-
-private theorem eq_neg_addConst_add (ctx : Context) (p : Poly)
-    : p.denote' ctx = (p.addConst (-p.getConst)).denote' ctx + p.getConst := by
-  simp only [Poly.denote'_eq_denote, Poly.denote_addConst, Int.add_comm, Int.add_left_comm]
-  rw [Int.add_right_neg]
-  simp
-
-def dvd_le_tight_cert (d : Int) (p₁ p₂ p₃ : Poly) : Bool :=
-  let b₁ := p₁.getConst
-  let b₂ := p₂.getConst
-  let p  := p₁.addConst (-b₁)
-  d > 0 && (p₂ == p.addConst b₂ && p₃ == p.addConst (b₁ - d*((b₁ - b₂)/d)))
-
-theorem dvd_le_tight (ctx : Context) (d : Int) (p₁ p₂ p₃ : Poly)
-    : dvd_le_tight_cert d p₁ p₂ p₃ → d ∣ p₁.denote' ctx → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
-  simp only [dvd_le_tight_cert, gt_iff_lt, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, and_imp]
-  generalize p₂.getConst = b₂
-  intro hd _ _; subst p₂ p₃
-  have := eq_neg_addConst_add ctx p₁
-  revert this
-  generalize p₁.getConst = b₁
-  generalize p₁.addConst (-b₁) = p
-  intro h₁; rw [h₁]; clear h₁
-  simp only [denote'_addConst_eq]
-  simp only [Poly.denote'_eq_denote]
-  exact dvd_le_tight' hd
-
-def dvd_neg_le_tight_cert (d : Int) (p₁ p₂ p₃ : Poly) : Bool :=
-  let b₁ := p₁.getConst
-  let b₂ := p₂.getConst
-  let p  := p₁.addConst (-b₁)
-  let b₁ := -b₁
-  let p  := p.mul (-1)
-  d > 0 && (p₂ == p.addConst b₂ && p₃ == p.addConst (b₁ - d*((b₁ - b₂)/d)))
-
-theorem Poly.mul_minus_one_getConst_eq (p : Poly) : (p.mul (-1)).getConst = -p.getConst := by
-  simp [Poly.mul, Poly.getConst]
-  induction p <;> simp [Poly.mul', Poly.getConst, *]
-
-theorem dvd_neg_le_tight (ctx : Context) (d : Int) (p₁ p₂ p₃ : Poly)
-    : dvd_neg_le_tight_cert d p₁ p₂ p₃ → d ∣ p₁.denote' ctx → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
-  simp only [dvd_neg_le_tight_cert, gt_iff_lt, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, and_imp]
-  generalize p₂.getConst = b₂
-  intro hd _ _; subst p₂ p₃
-  simp only [Poly.denote'_eq_denote, Int.reduceNeg, Poly.denote_addConst, Poly.denote_mul,
-    Int.mul_add, Int.neg_mul, Int.one_mul, Int.mul_neg, Int.neg_neg, Int.add_comm, Int.add_assoc]
-  intro h₁ h₂
-  replace h₁ := Int.dvd_neg.mpr h₁
-  have := eq_neg_addConst_add ctx (p₁.mul (-1))
-  simp [Poly.mul_minus_one_getConst_eq] at this
-  rw [← Int.add_assoc] at this
-  rw [this] at h₁; clear this
-  rw [← Int.add_assoc]
-  revert h₁ h₂
-  generalize -Poly.denote ctx p₁ + p₁.getConst = p
-  generalize -p₁.getConst = b₁
-  intro h₁ h₂; rw [Int.add_comm] at h₁
-  exact dvd_le_tight' hd h₂ h₁
-
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by

src/Init/Data/Int/OfNat.lean

@@ -1,64 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Data.Int.Lemmas
-import Init.Data.Int.DivMod
-import Init.Data.RArray
-
-namespace Int.OfNat
-/-!
-Helper definitions and theorems for converting `Nat` expressions into `Int` one.
-We use them to implement the arithmetic theories in `grind`
--/
-
-abbrev Var := Nat
-abbrev Context := Lean.RArray Nat
-def Var.denote (ctx : Context) (v : Var) : Nat :=
-  ctx.get v
-
-inductive Expr where
-  | num  (v : Nat)
-  | var  (i : Var)
-  | add  (a b : Expr)
-  | mul  (a b : Expr)
-  | div  (a b : Expr)
-  | mod  (a b : Expr)
-
-def Expr.denote (ctx : Context) : Expr → Nat
-  | .num k    => k
-  | .var v    => v.denote ctx
-  | .add a b  => Nat.add (denote ctx a) (denote ctx b)
-  | .mul a b  => Nat.mul (denote ctx a) (denote ctx b)
-  | .div a b  => Nat.div (denote ctx a) (denote ctx b)
-  | .mod a b  => Nat.mod (denote ctx a) (denote ctx b)
-
-def Expr.denoteAsInt (ctx : Context) : Expr → Int
-  | .num k    => Int.ofNat k
-  | .var v    => Int.ofNat (v.denote ctx)
-  | .add a b  => Int.add (denoteAsInt ctx a) (denoteAsInt ctx b)
-  | .mul a b  => Int.mul (denoteAsInt ctx a) (denoteAsInt ctx b)
-  | .div a b  => Int.ediv (denoteAsInt ctx a) (denoteAsInt ctx b)
-  | .mod a b  => Int.emod (denoteAsInt ctx a) (denoteAsInt ctx b)
-
-@[local simp] private theorem fold_div (a b : Nat) : a.div b = a / b := rfl
-@[local simp] private theorem fold_mod (a b : Nat) : a.mod b = a % b := rfl
-
-theorem Expr.denoteAsInt_eq (ctx : Context) (e : Expr) : e.denoteAsInt ctx = e.denote ctx := by
-  induction e <;> simp [denote, denoteAsInt, Int.ofNat_ediv, *] <;> rfl
-
-theorem Expr.eq (ctx : Context) (lhs rhs : Expr)
-    : (lhs.denote ctx = rhs.denote ctx) = (lhs.denoteAsInt ctx = rhs.denoteAsInt ctx) := by
-  simp [denoteAsInt_eq, Int.ofNat_inj]
-
-theorem Expr.le (ctx : Context) (lhs rhs : Expr)
-    : (lhs.denote ctx ≤ rhs.denote ctx) = (lhs.denoteAsInt ctx ≤ rhs.denoteAsInt ctx) := by
-  simp [denoteAsInt_eq, Int.ofNat_le]
-
-theorem Expr.dvd (ctx : Context) (lhs rhs : Expr)
-    : (lhs.denote ctx ∣ rhs.denote ctx) = (lhs.denoteAsInt ctx ∣ rhs.denoteAsInt ctx) := by
-  simp [denoteAsInt_eq, Int.ofNat_dvd]
-
-end Int.OfNat

src/Init/Data/Int/Order.lean

@@ -133,15 +133,12 @@ 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
 
-@[simp] protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
+protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
   Iff.intro Int.lt_of_not_ge Int.not_le_of_gt
 
-@[simp] protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
+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
@@ -361,10 +358,6 @@ protected theorem sub_lt_self (a : Int) {b : Int} (h : 0 < b) : a - b < a :=
 
 theorem add_one_le_of_lt {a b : Int} (H : a < b) : a + 1 ≤ b := H
 
-protected theorem le_iff_lt_add_one {a b : Int} : a ≤ b ↔ a < b + 1 := by
-  rw [Int.lt_iff_add_one_le]
-  exact (Int.add_le_add_iff_right 1).symm
-
 /- ### Order properties and multiplication -/
 
 
@@ -432,7 +425,7 @@ protected theorem mul_le_mul_of_nonpos_left {a b c : Int}
 
 /- ## natAbs -/
 
-@[simp, norm_cast] theorem natAbs_ofNat (n : Nat) : natAbs ↑n = n := rfl
+@[simp] theorem natAbs_ofNat (n : Nat) : natAbs ↑n = n := rfl
 @[simp] theorem natAbs_negSucc (n : Nat) : natAbs -[n+1] = n.succ := rfl
 @[simp] theorem natAbs_zero : natAbs (0 : Int) = (0 : Nat) := rfl
 @[simp] theorem natAbs_one : natAbs (1 : Int) = (1 : Nat) := rfl
@@ -477,13 +470,6 @@ theorem natAbs_of_nonneg {a : Int} (H : 0 ≤ a) : (natAbs a : Int) = a :=
 theorem ofNat_natAbs_of_nonpos {a : Int} (H : a ≤ 0) : (natAbs a : Int) = -a := by
   rw [← natAbs_neg, natAbs_of_nonneg (Int.neg_nonneg_of_nonpos H)]
 
-theorem natAbs_sub_of_nonneg_of_le {a b : Int} (h₁ : 0 ≤ b) (h₂ : b ≤ a) :
-    (a - b).natAbs = a.natAbs - b.natAbs := by
-  rw [← Int.ofNat_inj]
-  rw [natAbs_of_nonneg, ofNat_sub, natAbs_of_nonneg (Int.le_trans h₁ h₂), natAbs_of_nonneg h₁]
-  · rwa [← Int.ofNat_le, natAbs_of_nonneg h₁, natAbs_of_nonneg (Int.le_trans h₁ h₂)]
-  · exact Int.sub_nonneg_of_le h₂
-
 /-! ### toNat -/
 
 theorem toNat_eq_max : ∀ a : Int, (toNat a : Int) = max a 0
@@ -952,22 +938,6 @@ 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
@@ -1051,12 +1021,6 @@ theorem sign_eq_neg_one_iff_neg {a : Int} : sign a = -1 ↔ a < 0 :=
 @[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

@@ -662,10 +662,6 @@ 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
@@ -770,16 +766,6 @@ 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

@@ -1758,10 +1758,10 @@ where
 
 /-! ### removeAll -/
 
-/-- `O(|xs| * |ys|)`. Computes the "set difference" of lists,
+/-- `O(|xs|)`. 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

@@ -212,7 +212,6 @@ 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
@@ -222,7 +221,6 @@ 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

@@ -227,19 +227,14 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
     | false => findM? p as
 
 @[simp]
-theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
-    findM? (m := m) (pure <| p ·) as = pure (as.find? p) := by
+theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p := by
   induction as with
   | nil => rfl
   | cons a as ih =>
     simp only [findM?, find?]
     cases p a with
-    | true  => simp
-    | false => simp [ih]
-
-@[simp]
-theorem findM?_id (p : α → Bool) (as : List α) : findM? (m := Id) p as = as.find? p :=
-  findM?_pure _ _
+    | true  => rfl
+    | false => rw [ih]; rfl
 
 @[specialize]
 def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)
@@ -250,19 +245,14 @@ def findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f
     | none   => findSomeM? f as
 
 @[simp]
-theorem findSomeM?_pure [Monad m] [LawfulMonad m] (f : α → Option β) (as : List α) :
-    findSomeM? (m := m) (pure <| f ·) as = pure (as.findSome? f) := by
+theorem findSomeM?_id (f : α → Option β) (as : List α) : findSomeM? (m := Id) f as = as.findSome? f := by
   induction as with
   | nil => rfl
   | cons a as ih =>
     simp only [findSomeM?, findSome?]
     cases f a with
-    | some b => simp
-    | none   => simp [ih]
-
-@[simp]
-theorem findSomeM?_id (f : α → Option β) (as : List α) : findSomeM? (m := Id) f as = as.findSome? f :=
-  findSomeM?_pure _ _
+    | some b => rfl
+    | none   => rw [ih]; rfl
 
 theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
     as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none := by

src/Init/Data/List/Lemmas.lean

@@ -2535,14 +2535,6 @@ theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.fla
   simp only [foldrM]
   induction l <;> simp_all
 
-@[simp] theorem foldlM_pure [Monad m] [LawfulMonad m] (f : β → α → β) (b) (l : List α) :
-    l.foldlM (m := m) (pure <| f · ·) b = pure (l.foldl f b) := by
-  induction l generalizing b <;> simp [*]
-
-@[simp] theorem foldrM_pure [Monad m] [LawfulMonad m] (f : α → β → β) (b) (l : List α) :
-    l.foldrM (m := m) (pure <| f · ·) b = pure (l.foldr f b) := by
-  induction l generalizing b <;> simp [*]
-
 theorem foldl_eq_foldlM (f : β → α → β) (b) (l : List α) :
     l.foldl f b = l.foldlM (m := Id) f b := by
   induction l generalizing b <;> simp [*, foldl]

src/Init/Data/List/Monadic.lean

@@ -56,13 +56,9 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α)
 @[simp] theorem mapM_cons [Monad m] [LawfulMonad m] (f : α → m β) :
     (a :: l).mapM f = (return (← f a) :: (← l.mapM f)) := by simp [← mapM'_eq_mapM, mapM']
 
-@[simp] theorem mapM_pure [Monad m] [LawfulMonad m] (l : List α) (f : α → β) :
-    l.mapM (m := m) (pure <| f ·) = pure (l.map f) := by
+@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f := by
   induction l <;> simp_all
 
-@[simp] theorem mapM_id {l : List α} {f : α → Id β} : l.mapM f = l.map f :=
-  mapM_pure _ _
-
 @[simp] theorem mapM_append [Monad m] [LawfulMonad m] (f : α → m β) {l₁ l₂ : List α} :
     (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f)) := by induction l₁ <;> simp [*]
 
@@ -399,7 +395,7 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
     forIn (l.map g) init f = forIn l init fun a y => f (g a) y := by
   induction l generalizing init <;> simp_all
 
-/-! ### allM and anyM -/
+/-! ### allM -/
 
 theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
     allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
@@ -411,18 +407,6 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as :
     funext b
     split <;> simp_all
 
-@[simp] theorem anyM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
-    as.anyM (m := m) (pure <| p ·) = pure (as.any p) := by
-  induction as with
-  | nil => simp
-  | cons a as ih =>
-    simp only [anyM, ih, pure_bind, all_cons]
-    split <;> simp_all
-
-@[simp] theorem allM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
-    as.allM (m := m) (pure <| p ·) = pure (as.all p) := by
-  simp [allM_eq_not_anyM_not, all_eq_not_any_not]
-
 /-! ### Recognizing higher order functions using a function that only depends on the value. -/
 
 /--
@@ -438,12 +422,12 @@ and simplifies these to the function directly taking the value.
   | nil => simp
   | cons a l ih => simp [ih, hf]
 
-@[wf_preprocess] theorem foldlM_wfParam [Monad m] (xs : List α) (f : β → α → m β) (init : β) :
-    (wfParam xs).foldlM f init = xs.attach.unattach.foldlM f init := by
+@[wf_preprocess] theorem foldlM_wfParam [Monad m] (xs : List α) (f : β → α → m β) :
+    (wfParam xs).foldlM f = xs.attach.unattach.foldlM f := by
   simp [wfParam]
 
-@[wf_preprocess] theorem foldlM_unattach [Monad m] (P : α → Prop) (xs : List (Subtype P)) (f : β → α → m β) (init : β):
-    xs.unattach.foldlM f init = xs.foldlM (init := init) fun b ⟨x, h⟩ =>
+@[wf_preprocess] theorem foldlM_unattach [Monad m] (P : α → Prop) (xs : List (Subtype P)) (f : β → α → m β) :
+    xs.unattach.foldlM f = xs.foldlM fun b ⟨x, h⟩ =>
       binderNameHint b f <| binderNameHint x (f b) <| binderNameHint h () <|
       f b (wfParam x) := by
   simp [wfParam]
@@ -465,12 +449,12 @@ and simplifies these to the function directly taking the value.
     funext b
     simp [hf]
 
-@[wf_preprocess] theorem foldrM_wfParam [Monad m] [LawfulMonad m] (xs : List α) (f : α → β → m β) (init : β) :
-    (wfParam xs).foldrM f init = xs.attach.unattach.foldrM f init := by
+@[wf_preprocess] theorem foldrM_wfParam [Monad m] [LawfulMonad m] (xs : List α) (f : α → β → m β) :
+    (wfParam xs).foldrM f = xs.attach.unattach.foldrM f := by
   simp [wfParam]
 
-@[wf_preprocess] theorem foldrM_unattach [Monad m] [LawfulMonad m] (P : α → Prop) (xs : List (Subtype P)) (f : α → β → m β) (init : β) :
-    xs.unattach.foldrM f init = xs.foldrM (init := init) fun ⟨x, h⟩ b =>
+@[wf_preprocess] theorem foldrM_unattach [Monad m] [LawfulMonad m] (P : α → Prop) (xs : List (Subtype P)) (f : α → β → m β) :
+    xs.unattach.foldrM f = xs.foldrM fun ⟨x, h⟩ b =>
       binderNameHint x f <| binderNameHint h () <| binderNameHint b (f x) <|
       f (wfParam x) b := by
   simp [wfParam]

src/Init/Data/List/Perm.lean

@@ -47,14 +47,6 @@ instance : Trans (Perm (α := α)) (Perm (α := α)) (Perm (α := α)) where
 
 theorem perm_comm {l₁ l₂ : List α} : l₁ ~ l₂ ↔ l₂ ~ l₁ := ⟨Perm.symm, Perm.symm⟩
 
-protected theorem Perm.congr_left {l₁ l₂ : List α} (h : l₁ ~ l₂) (l₃ : List α) :
-    l₁ ~ l₃ ↔ l₂ ~ l₃ :=
-  ⟨h.symm.trans, h.trans⟩
-
-protected theorem Perm.congr_right {l₁ l₂ : List α} (h : l₁ ~ l₂) (l₃ : List α) :
-    l₃ ~ l₁ ↔ l₃ ~ l₂ :=
-  ⟨fun h' => h'.trans h, fun h' => h'.trans h.symm⟩
-
 theorem Perm.swap' (x y : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) : y :: x :: l₁ ~ x :: y :: l₂ :=
   (swap ..).trans <| p.cons _ |>.cons _
 

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

@@ -74,10 +74,6 @@ theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
 theorem shiftRight_eq_zero (m n : Nat) (hn : m < 2^n) : m >>> n = 0 := by
   simp [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt hn]
 
-theorem shiftRight_le (m n : Nat) : m >>> n ≤ m := by
-  simp only [shiftRight_eq_div_pow]
-  apply Nat.div_le_self
-
 /-!
 ### testBit
 We define an operation for testing individual bits in the binary representation

src/Init/Data/Nat/Div/Lemmas.lean

@@ -27,8 +27,8 @@ theorem div_le_iff_le_mul (h : 0 < k) : x / k ≤ y ↔ x ≤ y * k + k - 1 := b
   omega
 
 -- TODO: reprove `div_eq_of_lt_le` in terms of this:
-protected theorem div_eq_iff (h : 0 < k) : x / k = y ↔ y * k ≤ x ∧ x ≤ y * k + k - 1 := by
-  rw [Nat.eq_iff_le_and_ge, and_comm, le_div_iff_mul_le h, Nat.div_le_iff_le_mul h]
+protected theorem div_eq_iff (h : 0 < k) : x / k = y ↔ x ≤ y * k + k - 1 ∧ y * k ≤ x := by
+  rw [Nat.eq_iff_le_and_ge, le_div_iff_mul_le h, Nat.div_le_iff_le_mul h]
 
 theorem lt_of_div_eq_zero (h : 0 < k) (h' : x / k = 0) : x < k := by
   rw [Nat.div_eq_iff h] at h'
@@ -98,34 +98,18 @@ theorem succ_div_of_not_dvd {a b : Nat} (h : ¬ b ∣ a + 1) :
     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]
-      have : (a + 1) % (b + 1) < b + 1 := Nat.mod_lt _ (by simp)
       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])]
 
-protected theorem succ_div {a b : Nat} : (a + 1) / b = a / b + if b ∣ a + 1 then 1 else 0 := by
+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]
 
-protected theorem add_div {a b c : Nat} (h : 0 < c) :
-    (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0 := by
-  conv => lhs; rw [← Nat.div_add_mod a c]
-  rw [Nat.add_assoc, mul_add_div h]
-  conv => lhs; rw [← Nat.div_add_mod b c]
-  rw [Nat.add_comm (a % c), Nat.add_assoc, mul_add_div h, ← Nat.add_assoc, Nat.add_comm (b % c)]
-  congr
-  rw [Nat.div_eq_iff h]
-  constructor
-  · split <;> rename_i h
-    · simpa using h
-    · simp
-  · have := mod_lt a h
-    have := mod_lt b h
-    split <;> · simp; omega
-
 end Nat

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 → Float32
-  | Int.ofNat n => Float32.ofNat n
-  | Int.negSucc n => Float32.neg (Float32.ofNat (Nat.succ n))
+def Float32.ofInt : Int → Float
+  | Int.ofNat n => Float.ofNat n
+  | Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))
 
 instance : OfNat Float32 n   := ⟨Float32.ofNat n⟩
 

src/Init/Data/Option/Basic.lean

@@ -101,12 +101,6 @@ 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
@@ -223,24 +217,18 @@ 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.
-
-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`.
--/
+/-- The minimum of two optional values. -/
 protected def min [Min α] : Option α → Option α → Option α
   | some x, some y => some (Min.min x y)
-  | some _, none => none
-  | none, some _ => none
+  | some x, none => some x
+  | none, some y => some y
   | 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 = none := rfl
-@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = none := 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_none_none [Min α] : min (none : Option α) none = none := rfl
 
 /-- The maximum of two optional values. -/
@@ -263,9 +251,6 @@ 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

@@ -673,80 +673,4 @@ theorem pmap_map (o : Option α) (f : α → β) {p : β → Prop} (g : ∀ b, p
        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/Repr.lean

@@ -251,14 +251,6 @@ where
     let d1 := n % 16;
     hexDigitRepr d2 ++ hexDigitRepr d1
 
-/--
-Quotes the character to its representation as a character literal, surrounded by single quotes and
-escaped as necessary.
-
-Examples:
- * `'L'.quote = "'L'"`
- * `'"'.quote = "'\\\"'"`
--/
 def Char.quote (c : Char) : String :=
   "'" ++ Char.quoteCore c ++ "'"
 

src/Init/Data/SInt.lean

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

src/Init/Data/SInt/Basic.lean

@@ -77,9 +77,6 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int8
 -/
 @[inline] def Int8.toBitVec (x : Int8) : BitVec 8 := x.toUInt8.toBitVec
 
-theorem Int8.toBitVec.inj : {x y : Int8} → x.toBitVec = y.toBitVec → x = y
-  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
-
 /-- Obtains the `Int8` that is 2's complement equivalent to the `UInt8`. -/
 @[inline] def UInt8.toInt8 (i : UInt8) : Int8 := Int8.ofUInt8 i
 @[inline, deprecated UInt8.toInt8 (since := "2025-02-13"), inherit_doc UInt8.toInt8]
@@ -113,8 +110,8 @@ instance : ReprAtom Int8 := ⟨⟩
 instance : Hashable Int8 where
   hash i := i.toUInt8.toUInt64
 
-instance Int8.instOfNat : OfNat Int8 n := ⟨Int8.ofNat n⟩
-instance Int8.instNeg : Neg Int8 where
+instance : OfNat Int8 n := ⟨Int8.ofNat n⟩
+instance : Neg Int8 where
   neg := Int8.neg
 
 /-- The maximum value an `Int8` may attain, that is, `2^7 - 1 = 127`. -/
@@ -192,9 +189,6 @@ instance : ShiftLeft Int8   := ⟨Int8.shiftLeft⟩
 instance : ShiftRight Int8  := ⟨Int8.shiftRight⟩
 instance : DecidableEq Int8 := Int8.decEq
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_int8"]
 def Bool.toInt8 (b : Bool) : Int8 := if b then 1 else 0
 
@@ -219,9 +213,6 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int1
 -/
 @[inline] def Int16.toBitVec (x : Int16) : BitVec 16 := x.toUInt16.toBitVec
 
-theorem Int16.toBitVec.inj : {x y : Int16} → x.toBitVec = y.toBitVec → x = y
-  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
-
 /-- Obtains the `Int16` that is 2's complement equivalent to the `UInt16`. -/
 @[inline] def UInt16.toInt16 (i : UInt16) : Int16 := Int16.ofUInt16 i
 @[inline, deprecated UInt16.toInt16 (since := "2025-02-13"), inherit_doc UInt16.toInt16]
@@ -259,8 +250,8 @@ instance : ReprAtom Int16 := ⟨⟩
 instance : Hashable Int16 where
   hash i := i.toUInt16.toUInt64
 
-instance Int16.instOfNat : OfNat Int16 n := ⟨Int16.ofNat n⟩
-instance Int16.instNeg : Neg Int16 where
+instance : OfNat Int16 n := ⟨Int16.ofNat n⟩
+instance : Neg Int16 where
   neg := Int16.neg
 
 /-- The maximum value an `Int16` may attain, that is, `2^15 - 1 = 32767`. -/
@@ -338,9 +329,6 @@ instance : ShiftLeft Int16   := ⟨Int16.shiftLeft⟩
 instance : ShiftRight Int16  := ⟨Int16.shiftRight⟩
 instance : DecidableEq Int16 := Int16.decEq
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_int16"]
 def Bool.toInt16 (b : Bool) : Int16 := if b then 1 else 0
 
@@ -365,9 +353,6 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int3
 -/
 @[inline] def Int32.toBitVec (x : Int32) : BitVec 32 := x.toUInt32.toBitVec
 
-theorem Int32.toBitVec.inj : {x y : Int32} → x.toBitVec = y.toBitVec → x = y
-  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
-
 /-- Obtains the `Int32` that is 2's complement equivalent to the `UInt32`. -/
 @[inline] def UInt32.toInt32 (i : UInt32) : Int32 := Int32.ofUInt32 i
 @[inline, deprecated UInt32.toInt32 (since := "2025-02-13"), inherit_doc UInt32.toInt32]
@@ -409,8 +394,8 @@ instance : ReprAtom Int16 := ⟨⟩
 instance : Hashable Int32 where
   hash i := i.toUInt32.toUInt64
 
-instance Int32.instOfNat : OfNat Int32 n := ⟨Int32.ofNat n⟩
-instance Int32.instNeg : Neg Int32 where
+instance : OfNat Int32 n := ⟨Int32.ofNat n⟩
+instance : Neg Int32 where
   neg := Int32.neg
 
 /-- The maximum value an `Int32` may attain, that is, `2^31 - 1 = 2147483647`. -/
@@ -488,9 +473,6 @@ instance : ShiftLeft Int32   := ⟨Int32.shiftLeft⟩
 instance : ShiftRight Int32  := ⟨Int32.shiftRight⟩
 instance : DecidableEq Int32 := Int32.decEq
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_int32"]
 def Bool.toInt32 (b : Bool) : Int32 := if b then 1 else 0
 
@@ -515,9 +497,6 @@ Obtain the `BitVec` that contains the 2's complement representation of the `Int6
 -/
 @[inline] def Int64.toBitVec (x : Int64) : BitVec 64 := x.toUInt64.toBitVec
 
-theorem Int64.toBitVec.inj : {x y : Int64} → x.toBitVec = y.toBitVec → x = y
-  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
-
 /-- Obtains the `Int64` that is 2's complement equivalent to the `UInt64`. -/
 @[inline] def UInt64.toInt64 (i : UInt64) : Int64 := Int64.ofUInt64 i
 @[inline, deprecated UInt64.toInt64 (since := "2025-02-13"), inherit_doc UInt64.toInt64]
@@ -563,8 +542,8 @@ instance : ReprAtom Int64 := ⟨⟩
 instance : Hashable Int64 where
   hash i := i.toUInt64
 
-instance Int64.instOfNat : OfNat Int64 n := ⟨Int64.ofNat n⟩
-instance Int64.instNeg : Neg Int64 where
+instance : OfNat Int64 n := ⟨Int64.ofNat n⟩
+instance : Neg Int64 where
   neg := Int64.neg
 
 /-- The maximum value an `Int64` may attain, that is, `2^63 - 1 = 9223372036854775807`. -/
@@ -642,9 +621,6 @@ instance : ShiftLeft Int64   := ⟨Int64.shiftLeft⟩
 instance : ShiftRight Int64  := ⟨Int64.shiftRight⟩
 instance : DecidableEq Int64 := Int64.decEq
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_int64"]
 def Bool.toInt64 (b : Bool) : Int64 := if b then 1 else 0
 
@@ -669,9 +645,6 @@ Obtain the `BitVec` that contains the 2's complement representation of the `ISiz
 -/
 @[inline] def ISize.toBitVec (x : ISize) : BitVec System.Platform.numBits := x.toUSize.toBitVec
 
-theorem ISize.toBitVec.inj : {x y : ISize} → x.toBitVec = y.toBitVec → x = y
-  | ⟨⟨_⟩⟩, ⟨⟨_⟩⟩, rfl => rfl
-
 /-- Obtains the `ISize` that is 2's complement equivalent to the `USize`. -/
 @[inline] def USize.toISize (i : USize) : ISize := ISize.ofUSize i
 @[inline, deprecated USize.toISize (since := "2025-02-13"), inherit_doc USize.toISize]
@@ -727,8 +700,8 @@ instance : ReprAtom ISize := ⟨⟩
 instance : Hashable ISize where
   hash i := i.toUSize.toUInt64
 
-instance ISize.instOfNat : OfNat ISize n := ⟨ISize.ofNat n⟩
-instance ISize.instNeg : Neg ISize where
+instance : OfNat ISize n := ⟨ISize.ofNat n⟩
+instance : Neg ISize where
   neg := ISize.neg
 
 /-- The maximum value an `ISize` may attain, that is, `2^(System.Platform.numBits - 1) - 1`. -/
@@ -807,9 +780,6 @@ instance : ShiftLeft ISize   := ⟨ISize.shiftLeft⟩
 instance : ShiftRight ISize  := ⟨ISize.shiftRight⟩
 instance : DecidableEq ISize := ISize.decEq
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_isize"]
 def Bool.toISize (b : Bool) : ISize := if b then 1 else 0
 

src/Init/Data/SInt/Bitwise.lean

@@ -1,57 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-prelude
-import Init.Data.SInt.Lemmas
-
-set_option hygiene false in
-macro "declare_bitwise_int_theorems" typeName:ident bits:term:arg : command =>
-`(
-namespace $typeName
-
-@[simp, int_toBitVec] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_div {a b : $typeName} : (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec.srem b.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec.smod $bits) := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec.sshiftRight' (b.toBitVec.smod $bits) := rfl
-@[simp, int_toBitVec] protected theorem toBitVec_abs (a : $typeName) : a.abs.toBitVec = a.toBitVec.abs := rfl
-
-end $typeName
-)
-declare_bitwise_int_theorems Int8 8
-declare_bitwise_int_theorems Int16 16
-declare_bitwise_int_theorems Int32 32
-declare_bitwise_int_theorems Int64 64
-declare_bitwise_int_theorems ISize System.Platform.numBits
-
-@[simp, int_toBitVec]
-theorem Bool.toBitVec_toInt8 {b : Bool} : b.toInt8.toBitVec = (BitVec.ofBool b).setWidth 8 := by
-  cases b <;> simp [toInt8]
-
-@[simp, int_toBitVec]
-theorem Bool.toBitVec_toInt16 {b : Bool} : b.toInt16.toBitVec = (BitVec.ofBool b).setWidth 16 := by
-  cases b <;> simp [toInt16]
-
-@[simp, int_toBitVec]
-theorem Bool.toBitVec_toInt32 {b : Bool} : b.toInt32.toBitVec = (BitVec.ofBool b).setWidth 32 := by
-  cases b <;> simp [toInt32]
-
-@[simp, int_toBitVec]
-theorem Bool.toBitVec_toInt64 {b : Bool} : b.toInt64.toBitVec = (BitVec.ofBool b).setWidth 64 := by
-  cases b <;> simp [toInt64]
-
-@[simp, int_toBitVec]
-theorem Bool.toBitVec_toISize {b : Bool} :
-    b.toISize.toBitVec = (BitVec.ofBool b).setWidth System.Platform.numBits := by
-  cases b
-  · simp [toISize]
-  · apply BitVec.eq_of_toNat_eq
-    simp [toISize]

src/Init/Data/String/Basic.lean

@@ -1169,13 +1169,6 @@ end String
 
 namespace Char
 
-/--
-Constructs a singleton string that contains only the provided character.
-
-Examples:
- * `'L'.toString = "L"`
- * `'"'.toString = "\""`
--/
 @[inline] protected def toString (c : Char) : String :=
   String.singleton c
 

src/Init/Data/UInt/Basic.lean

@@ -65,9 +65,6 @@ instance : Xor UInt8       := ⟨UInt8.xor⟩
 instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_uint8"]
 def Bool.toUInt8 (b : Bool) : UInt8 := if b then 1 else 0
 
@@ -140,9 +137,6 @@ instance : Xor UInt16       := ⟨UInt16.xor⟩
 instance : ShiftLeft UInt16  := ⟨UInt16.shiftLeft⟩
 instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_uint16"]
 def Bool.toUInt16 (b : Bool) : UInt16 := if b then 1 else 0
 
@@ -217,9 +211,6 @@ instance : Xor UInt32       := ⟨UInt32.xor⟩
 instance : ShiftLeft UInt32  := ⟨UInt32.shiftLeft⟩
 instance : ShiftRight UInt32 := ⟨UInt32.shiftRight⟩
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_uint32"]
 def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
 
@@ -279,9 +270,6 @@ instance : Xor UInt64       := ⟨UInt64.xor⟩
 instance : ShiftLeft UInt64  := ⟨UInt64.shiftLeft⟩
 instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_uint64"]
 def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
 
@@ -388,9 +376,6 @@ instance : Xor USize        := ⟨USize.xor⟩
 instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
-/--
-Converts `true` to `1` and `false` to `0`.
--/
 @[extern "lean_bool_to_usize"]
 def Bool.toUSize (b : Bool) : USize := if b then 1 else 0
 

src/Init/Data/Vector/Attach.lean

@@ -7,8 +7,8 @@ prelude
 import Init.Data.Vector.Lemmas
 import Init.Data.Array.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 Vector
 
@@ -473,10 +473,6 @@ def unattach {α : Type _} {p : α → Prop} (xs : Vector { x // p x } n) : Vect
     (xs.push a).unattach = xs.unattach.push a.1 := by
   simp only [unattach, Vector.map_push]
 
-@[simp] theorem mem_unattach {p : α → Prop} {xs : Vector { x // p x } n} {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 unattach_mk {p : α → Prop} {xs : Array { x // p x }} {h : xs.size = n} :
     (mk xs h).unattach = mk xs.unattach (by simpa using h) := by
   simp [unattach]
@@ -556,18 +552,6 @@ and simplifies these to the function directly taking the value.
   simp
   rw [Array.find?_subtype hf]
 
-@[simp] theorem all_subtype {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool}
-    (hf : ∀ x h, f ⟨x, h⟩ = g x) :
-    xs.all f = xs.unattach.all g := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [hf]
-
-@[simp] theorem any_subtype {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool}
-    (hf : ∀ x h, f ⟨x, h⟩ = g x) :
-    xs.any f = xs.unattach.any g := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [hf]
-
 /-! ### Simp lemmas pushing `unattach` inwards. -/
 
 @[simp] theorem unattach_reverse {p : α → Prop} {xs : Vector { x // p x } n} :

src/Init/Data/Vector/Basic.lean

@@ -8,7 +8,6 @@ prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.MapIdx
 import Init.Data.Array.InsertIdx
-import Init.Data.Array.Range
 import Init.Data.Range
 import Init.Data.Stream
 
@@ -18,8 +17,8 @@ import Init.Data.Stream
 `Vector α n` is a thin wrapper around `Array α` for arrays of fixed size `n`.
 -/
 
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 /-- `Vector α n` is an `Array α` with size `n`. -/
 structure Vector (α : Type u) (n : Nat) extends Array α where
@@ -59,10 +58,7 @@ def elimAsList {motive : Vector α n → Sort u}
   | ⟨⟨xs⟩, ha⟩ => mk xs ha
 
 /-- Make an empty vector with pre-allocated capacity. -/
-@[inline] def emptyWithCapacity (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
-
-@[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
-abbrev mkEmpty := @emptyWithCapacity
+@[inline] def mkEmpty (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
 
 /-- Makes a vector of size `n` with all cells containing `v`. -/
 @[inline] def mkVector (n) (v : α) : Vector α n := ⟨mkArray n v, by simp⟩

src/Init/Data/Vector/Find.lean

@@ -15,8 +15,8 @@ import Init.Data.Array.Find
 We are still missing results about `idxOf?`, `findIdx`, and `findIdx?`.
 -/
 
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
 namespace Vector
 

src/Init/Data/Vector/Lemmas.lean

@@ -13,8 +13,8 @@ import Init.Data.Array.Find
 Lemmas about `Vector α n`
 -/
 
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+-- 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
 
@@ -277,11 +277,8 @@ abbrev zipWithIndex_mk := @zipIdx_mk
 
 @[simp] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
 
-@[simp] theorem toArray_emptyWithCapacity (cap) :
-    (Vector.emptyWithCapacity (α := α) cap).toArray = Array.emptyWithCapacity cap := rfl
-
-@[deprecated toArray_emptyWithCapacity (since := "2025-03-12")]
-abbrev toArray_mkEmpty := @toArray_emptyWithCapacity
+@[simp] theorem toArray_mkEmpty (cap) :
+    (Vector.mkEmpty (α := α) cap).toArray = Array.mkEmpty cap := rfl
 
 @[simp] theorem toArray_eraseIdx (xs : Vector α n) (i) (h) :
     (xs.eraseIdx i h).toArray = xs.toArray.eraseIdx i (by simp [h]) := rfl
@@ -512,11 +509,8 @@ theorem toList_append (xs : Vector α m) (ys : Vector α n) :
 
 theorem toList_empty : (#v[] : Vector α 0).toArray = #[] := by simp
 
-theorem toList_emptyWithCapacity (cap) :
-    (Vector.emptyWithCapacity (α := α) cap).toList = [] := rfl
-
-@[deprecated toList_emptyWithCapacity (since := "2025-03-12")]
-abbrev toList_mkEmpty := @toList_emptyWithCapacity
+theorem toList_mkEmpty (cap) :
+    (Vector.mkEmpty (α := α) cap).toList = [] := rfl
 
 theorem toList_eraseIdx (xs : Vector α n) (i) (h) :
     (xs.eraseIdx i h).toList = xs.toList.eraseIdx i := by simp
@@ -1598,11 +1592,9 @@ theorem getElem_append (xs : Vector α n) (ys : Vector α m) (i : Nat) (hi : i <
   rcases ys with ⟨ys, rfl⟩
   simp [Array.getElem_append, hi]
 
-@[simp]
 theorem getElem_append_left {xs : Vector α n} {ys : Vector α m} {i : Nat} (hi : i < n) :
     (xs ++ ys)[i] = xs[i] := by simp [getElem_append, hi]
 
-@[simp]
 theorem getElem_append_right {xs : Vector α n} {ys : Vector α m} {i : Nat} (h : i < n + m) (hi : n ≤ i) :
     (xs ++ ys)[i] = ys[i - n] := by
   rw [getElem_append, dif_neg (by omega)]
@@ -2076,12 +2068,6 @@ theorem flatMap_mkArray {β} (f : α → Vector β m) : (mkVector n a).flatMap f
   rcases xs with ⟨xs, rfl⟩
   simp
 
-theorem getElem_eq_getElem_reverse {xs : Vector α n} {i} (h : i < n) :
-    xs[i] = xs.reverse[n - 1 - i] := by
-  rw [getElem_reverse]
-  congr
-  omega
-
 /-- Variant of `getElem?_reverse` with a hypothesis giving the linear relation between the indices. -/
 theorem getElem?_reverse' {xs : Vector α n} (i j) (h : i + j + 1 = n) : xs.reverse[i]? = xs[j]? := by
   rcases xs with ⟨xs, rfl⟩
@@ -2195,16 +2181,6 @@ theorem extract_empty (start stop : Nat) :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp]
-theorem foldlM_pure [Monad m] [LawfulMonad m] (f : β → α → β) (b) (xs : Vector α n) :
-    xs.foldlM (m := m) (pure <| f · ·) b = pure (xs.foldl f b) :=
-  Array.foldlM_pure _ _ _
-
-@[simp]
-theorem foldrM_pure [Monad m] [LawfulMonad m] (f : α → β → β) (b) (xs : Vector α n) :
-    xs.foldrM (m := m) (pure <| f · ·) b = pure (xs.foldr f b) :=
-  Array.foldrM_pure _ _ _
-
 theorem foldl_eq_foldlM (f : β → α → β) (b) (xs : Vector α n) :
     xs.foldl f b = xs.foldlM (m := Id) f b := by
   rcases xs with ⟨xs, rfl⟩
@@ -2498,14 +2474,6 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-/--
-Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
-defeq issues in the implicit size argument.
--/
-@[simp] theorem getElem_pop' (xs : Vector α (n + 1)) (i : Nat) (h : i < n + 1 - 1) :
-    @getElem (Vector α n) Nat α (fun _ i => i < n) instGetElemNatLt xs.pop i h = xs[i] :=
-  getElem_pop h
-
 theorem getElem?_pop (xs : Vector α n) (i : Nat) :
     xs.pop[i]? = if i < n - 1 then xs[i]? else none := by
   rcases xs with ⟨xs, rfl⟩
@@ -2617,161 +2585,6 @@ theorem replace_extract {xs : Vector α n} {i : Nat} :
 
 end replace
 
-/-! ## Logic -/
-
-/-! ### any / all -/
-
-theorem not_any_eq_all_not (xs : Vector α n) (p : α → Bool) : (!xs.any p) = xs.all fun a => !p a := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.not_any_eq_all_not]
-
-theorem not_all_eq_any_not (xs : Vector α n) (p : α → Bool) : (!xs.all p) = xs.any fun a => !p a := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.not_all_eq_any_not]
-
-theorem and_any_distrib_left (xs : Vector α n) (p : α → Bool) (q : Bool) :
-    (q && xs.any p) = xs.any fun a => q && p a := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.and_any_distrib_left]
-
-theorem and_any_distrib_right (xs : Vector α n) (p : α → Bool) (q : Bool) :
-    (xs.any p && q) = xs.any fun a => p a && q := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.and_any_distrib_right]
-
-theorem or_all_distrib_left (xs : Vector α n) (p : α → Bool) (q : Bool) :
-    (q || xs.all p) = xs.all fun a => q || p a := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.or_all_distrib_left]
-
-theorem or_all_distrib_right (xs : Vector α n) (p : α → Bool) (q : Bool) :
-    (xs.all p || q) = xs.all fun a => p a || q := by
-  rcases xs with ⟨xs, rfl⟩
-  simp [Array.or_all_distrib_right]
-
-theorem any_eq_not_all_not (xs : Vector α n) (p : α → Bool) : xs.any p = !xs.all (!p .) := by
-  simp only [not_all_eq_any_not, Bool.not_not]
-
-@[simp] theorem any_map {xs : Vector α n} {p : β → Bool} : (xs.map f).any p = xs.any (p ∘ f) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem all_map {xs : Vector α n} {p : β → Bool} : (xs.map f).all p = xs.all (p ∘ f) := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem any_filter {xs : Vector α n} {p q : α → Bool} :
-    (xs.filter p).any q = xs.any fun a => p a && q a := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem all_filter {xs : Vector α n} {p q : α → Bool} :
-    (xs.filter p).all q = xs.all fun a => p a → q a := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem any_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool} :
-    (xs.filterMap f).any p = xs.any fun a => match f a with | some b => p b | none => false := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-  rfl
-
-@[simp] theorem all_filterMap {xs : Vector α n} {f : α → Option β} {p : β → Bool} :
-    (xs.filterMap f).all p = xs.all fun a => match f a with | some b => p b | none => true := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-  rfl
-
-@[simp] theorem any_append {xs : Vector α n} {ys : Vector α m} :
-    (xs ++ ys).any f = (xs.any f || ys.any f) := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp
-
-@[simp] theorem all_append {xs : Vector α n} {ys : Vector α m} :
-    (xs ++ ys).all f = (xs.all f && ys.all f) := by
-  rcases xs with ⟨xs, rfl⟩
-  rcases ys with ⟨ys, rfl⟩
-  simp
-
-@[congr] theorem anyM_congr [Monad m]
-    {xs ys : Vector α n} (w : xs = ys) {p q : α → m Bool} (h : ∀ a, p a = q a) :
-    xs.anyM p = ys.anyM q := by
-  have : p = q := by funext a; apply h
-  subst this
-  subst w
-  rfl
-
-@[congr] theorem any_congr
-    {xs ys : Vector α n} (w : xs = ys) {p q : α → Bool} (h : ∀ a, p a = q a) :
-    xs.any p = ys.any q := by
-  unfold any
-  apply anyM_congr w h
-
-@[congr] theorem allM_congr [Monad m]
-    {xs ys : Vector α n} (w : xs = ys) {p q : α → m Bool} (h : ∀ a, p a = q a) :
-    xs.allM p = ys.allM q := by
-  have : p = q := by funext a; apply h
-  subst this
-  subst w
-  rfl
-
-@[congr] theorem all_congr
-    {xs ys : Vector α n} (w : xs = ys) {p q : α → Bool} (h : ∀ a, p a = q a) :
-    xs.all p = ys.all q := by
-  unfold all
-  apply allM_congr w h
-
-@[simp] theorem any_flatten {xss : Vector (Vector α n) m} : xss.flatten.any f = xss.any (any · f) := by
-  cases xss using vector₂_induction
-  simp
-
-@[simp] theorem all_flatten {xss : Vector (Vector α n) m} : xss.flatten.all f = xss.all (all · f) := by
-  cases xss using vector₂_induction
-  simp
-
-@[simp] theorem any_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
-    (xs.flatMap f).any p = xs.any fun a => (f a).any p := by
-  rcases xs with ⟨xs⟩
-  simp only [flatMap_mk, any_mk, Array.size_flatMap, size_toArray, Array.any_flatMap']
-  congr
-  funext
-  congr
-  simp [Vector.size_toArray]
-
-@[simp] theorem all_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
-    (xs.flatMap f).all p = xs.all fun a => (f a).all p := by
-  rcases xs with ⟨xs⟩
-  simp only [flatMap_mk, all_mk, Array.size_flatMap, size_toArray, Array.all_flatMap']
-  congr
-  funext
-  congr
-  simp [Vector.size_toArray]
-
-@[simp] theorem any_reverse {xs : Vector α n} : xs.reverse.any f  = xs.any f := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem all_reverse {xs : Vector α n} : xs.reverse.all f = xs.all f := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem any_cast {xs : Vector α n} : (xs.cast h).any f = xs.any f := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem all_cast {xs : Vector α n} : (xs.cast h).all f = xs.all f := by
-  rcases xs with ⟨xs, rfl⟩
-  simp
-
-@[simp] theorem any_mkVector {n : Nat} {a : α} :
-    (mkVector n a).any f = if n = 0 then false else f a := by
-  induction n <;> simp_all [mkVector_succ']
-
-@[simp] theorem all_mkVector {n : Nat} {a : α} :
-    (mkVector n a).all f = if n = 0 then true else f a := by
-  induction n <;> simp_all +contextual [mkVector_succ']
-
 /-! Content below this point has not yet been aligned with `List` and `Array`. -/
 
 set_option linter.indexVariables false in
@@ -2779,6 +2592,14 @@ set_option linter.indexVariables false in
   rcases xs with ⟨xs, rfl⟩
   simp
 
+/--
+Variant of `getElem_pop` that will sometimes fire when `getElem_pop` gets stuck because of
+defeq issues in the implicit size argument.
+-/
+@[simp] theorem getElem_pop' (xs : Vector α (n + 1)) (i : Nat) (h : i < n + 1 - 1) :
+    @getElem (Vector α n) Nat α (fun _ i => i < n) instGetElemNatLt xs.pop i h = xs[i] :=
+  getElem_pop h
+
 @[simp] theorem push_pop_back (xs : Vector α (n + 1)) : xs.pop.push xs.back = xs := by
   ext i
   by_cases h : i < n
@@ -2842,6 +2663,11 @@ theorem swap_comm (xs : Vector α n) {i j : Nat} {hi hj} :
   simp only [swap_mk, mk.injEq]
   rw [Array.swap_comm]
 
+/-! ### range -/
+
+@[simp] theorem getElem_range (i : Nat) (hi : i < n) : (Vector.range n)[i] = i := by
+  simp [Vector.range]
+
 /-! ### take -/
 
 @[simp] theorem getElem_take (xs : Vector α n) (j : Nat) (hi : i < min n j) :

src/Init/Data/Vector/Monadic.lean

@@ -29,12 +29,6 @@ open Nat
 
 /-! ### mapM -/
 
-@[simp]
-theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
-    xs.mapM (m := m) (pure <| f ·) = pure (xs.map f) := by
-  apply map_toArray_inj.mp
-  simp
-
 @[congr] theorem mapM_congr [Monad m] {xs ys : Vector α n} (w : xs = ys)
     {f : α → m β} :
     xs.mapM f = ys.mapM f := by
@@ -221,30 +215,4 @@ theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
   rcases xs with ⟨xs, rfl⟩
   simp
 
-
-/-! ### allM and anyM -/
-
-@[simp] theorem anyM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Vector α n) :
-    xs.anyM (m := m) (pure <| p ·) = pure (xs.any p) := by
-  cases xs
-  simp
-
-@[simp] theorem allM_pure [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Vector α n) :
-    xs.allM (m := m) (pure <| p ·) = pure (xs.all p) := by
-  cases xs
-  simp
-
-/-! ### findM? and findSomeM? -/
-
-theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (xs : Vector α n) :
-    findM? (m := m) (pure <| p ·) xs = pure (xs.find? p) := by
-  cases xs
-  simp
-
-@[simp]
-theorem findSomeM?_pure [Monad m] [LawfulMonad m] (f : α → Option β) (xs : Vector α n) :
-    findSomeM? (m := m) (pure <| f ·) xs = pure (xs.findSome? f) := by
-  cases xs
-  simp
-
 end Vector

src/Init/Data/Vector/Range.lean

@@ -115,9 +115,6 @@ theorem range'_eq_append_iff : range' s (n + m) = xs ++ ys ↔ xs = range' s n
 
 /-! ### range -/
 
-@[simp] theorem getElem_range (i : Nat) (hi : i < n) : (Vector.range n)[i] = i := by
-  simp [Vector.range]
-
 theorem range_eq_range' (n : Nat) : range n = range' 0 n := by
   simp [range, range', Array.range_eq_range']
 

src/Init/Grind/Lemmas.lean

@@ -69,11 +69,6 @@ theorem eq_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a = b) = a := by s
 theorem eq_congr  {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) : (a₁ = b₁) = (a₂ = b₂) := by simp [*]
 theorem eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) : (a₁ = b₁) = (a₂ = b₂) := by rw [h₁, h₂, Eq.comm (a := a₂)]
 
-/-! Ne -/
-
-theorem ne_of_ne_of_eq_left {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c := by simp [*]
-theorem ne_of_ne_of_eq_right {α : Sort u} {a b c : α} (h₁ : a = c) (h₂ : b ≠ c) : b ≠ a := by simp [*]
-
 /-! Bool.and -/
 
 theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b := by simp [h]

src/Init/Grind/Norm.lean

@@ -123,11 +123,10 @@ init_grind_norm
   Nat.add_eq Nat.sub_eq Nat.mul_eq Nat.zero_eq Nat.le_eq
   -- Int
   Int.lt_eq
-  Int.emod_neg Int.ediv_zero Int.emod_zero
   -- GT GE
   ge_eq gt_eq
   -- Int op folding
-  Int.add_def Int.mul_def Int.ofNat_eq_coe
+  Int.add_def Int.mul_def
   Int.Linear.sub_fold Int.Linear.neg_fold
   -- Int divides
   Int.one_dvd Int.zero_dvd

src/Init/Grind/Tactics.lean

@@ -69,11 +69,6 @@ structure Config where
   verbose : Bool := true
   /-- If `clean` is `true`, `grind` uses `expose_names` and only generates accessible names. -/
   clean : Bool := true
-  /--
-  If `qlia` is `true`, `grind` may generate counterexamples for integer constraints
-  using rational numbers, and ignoring divisibility constraints.
-  This approach is cheaper but incomplete. -/
-  qlia : Bool := false
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Init/Grind/Util.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Core
-import Init.Classical
 
 namespace Lean.Grind
 
@@ -78,23 +77,5 @@ def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
   | `($_ $lhs:term $rhs:term) => `($lhs + $rhs)
   | _ => throw ()
 
-/--
-A marker to indicate that a proposition has already been normalized and should not
-be processed again.
-
-This prevents issues when case-splitting on the condition `c` of an if-then-else
-expression. Without this marker, the negated condition `¬c` might be rewritten into
-an alternative form `c'`, which `grind` may not recognize as equivalent to `¬c`.
-As a result, `grind` could fail to propagate that `if c then a else b` simplifies to `b`
-in the `¬c` branch.
--/
-def alreadyNorm (p : Prop) : Prop := p
-
-/--
-`Classical.em` variant where disjuncts are marked with `alreadyNorm` gadget.
-See comment at `alreadyNorm`
--/
-theorem em (p : Prop) : alreadyNorm p ∨ alreadyNorm (¬ p) :=
-  Classical.em p
 
 end Lean.Grind

src/Init/Omega/Constraint.lean

@@ -111,7 +111,9 @@ def isExact : Constraint → Bool
 
 theorem not_sat_of_isImpossible (h : isImpossible c) {t} : ¬ c.sat t := by
   rcases c with ⟨_ | l, _ | u⟩ <;> simp [isImpossible, sat] at h ⊢
-  exact Int.lt_of_lt_of_le h
+  intro w
+  rw [Int.not_le]
+  exact Int.lt_of_lt_of_le h w
 
 /--
 Scale a constraint by multiplying by an integer.
@@ -137,14 +139,17 @@ theorem scale_sat {c : Constraint} (k) (w : c.sat t) : (scale k c).sat (k * t) :
   · rcases c with ⟨_ | l, _ | u⟩ <;> split <;> rename_i h <;> simp_all [sat, flip, map]
     · replace h := Int.le_of_lt h
       exact Int.mul_le_mul_of_nonneg_left w h
-    · exact Int.mul_le_mul_of_nonpos_left h w
+    · rw [Int.not_lt] at h
+      exact Int.mul_le_mul_of_nonpos_left h w
     · replace h := Int.le_of_lt h
       exact Int.mul_le_mul_of_nonneg_left w h
-    · exact Int.mul_le_mul_of_nonpos_left h w
+    · rw [Int.not_lt] at h
+      exact Int.mul_le_mul_of_nonpos_left h w
     · constructor
       · exact Int.mul_le_mul_of_nonneg_left w.1 (Int.le_of_lt h)
       · exact Int.mul_le_mul_of_nonneg_left w.2 (Int.le_of_lt h)
-    · constructor
+    · replace h := Int.not_lt.mp h
+      constructor
       · exact Int.mul_le_mul_of_nonpos_left h w.2
       · exact Int.mul_le_mul_of_nonpos_left h w.1
 
@@ -176,13 +181,13 @@ theorem combo_sat (a) (w₁ : c₁.sat x₁) (b) (w₂ : c₂.sat x₂) :
 
 /-- The conjunction of two constraints. -/
 def combine (x y : Constraint) : Constraint where
-  lowerBound := Option.merge max x.lowerBound y.lowerBound
-  upperBound := Option.merge min x.upperBound y.upperBound
+  lowerBound := max x.lowerBound y.lowerBound
+  upperBound := min x.upperBound y.upperBound
 
 theorem combine_sat : (c : Constraint) → (c' : Constraint) → (t : Int) →
     (c.combine c').sat t = (c.sat t ∧ c'.sat t) := by
   rintro ⟨_ | l₁, _ | u₁⟩ <;> rintro ⟨_ | l₂, _ | u₂⟩ t
-    <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le, Option.merge] at *
+    <;> simp [sat, LowerBound.sat, UpperBound.sat, combine, Int.le_min, Int.max_le] at *
   · rw [And.comm]
   · rw [← and_assoc, And.comm (a := l₂ ≤ t), and_assoc]
   · rw [and_assoc]
@@ -205,19 +210,21 @@ theorem div_sat (c : Constraint) (t : Int) (k : Nat) (n : k ≠ 0) (h : (k : Int
   · simp_all [sat, div]
   · simp [sat, div] at w ⊢
     apply Int.le_of_sub_nonneg
-    rw [← Int.sub_ediv_of_dvd _ h, Int.ediv_nonneg_iff_of_pos n]
+    rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n]
     exact Int.sub_nonneg_of_le w
   · simp [sat, div] at w ⊢
     apply Int.le_of_sub_nonneg
-    rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, Int.ediv_nonneg_iff_of_pos n]
+    rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le,
+      Int.div_nonneg_iff_of_pos n]
     exact Int.sub_nonneg_of_le w
   · simp [sat, div] at w ⊢
     constructor
     · apply Int.le_of_sub_nonneg
-      rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, Int.ediv_nonneg_iff_of_pos n]
+      rw [Int.sub_neg, ← Int.add_ediv_of_dvd_left h, ← ge_iff_le,
+        Int.div_nonneg_iff_of_pos n]
       exact Int.sub_nonneg_of_le w.1
     · apply Int.le_of_sub_nonneg
-      rw [← Int.sub_ediv_of_dvd _ h, Int.ediv_nonneg_iff_of_pos n]
+      rw [← Int.sub_ediv_of_dvd _ h, ← ge_iff_le, Int.div_nonneg_iff_of_pos n]
       exact Int.sub_nonneg_of_le w.2
 
 /--

src/Init/Prelude.lean

@@ -561,17 +561,16 @@ theorem Or.neg_resolve_left  (h : Or (Not a) b) (ha : a) : b := h.elim (absurd h
 theorem Or.neg_resolve_right (h : Or a (Not b)) (nb : b) : a := h.elim id (absurd nb)
 
 /--
-The Boolean values, `true` and `false`.
-
-Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
-important for programming: both propositions and their proofs are erased in the code generator,
-while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
-bit of run-time information.
+`Bool` is the type of boolean values, `true` and `false`. Classically,
+this is equivalent to `Prop` (the type of propositions), but the distinction
+is important for programming, because values of type `Prop` are erased in the
+code generator, while `Bool` corresponds to the type called `bool` or `boolean`
+in most programming languages.
 -/
 inductive Bool : Type where
-  /-- The Boolean value `false`, not to be confused with the proposition `False`. -/
+  /-- The boolean value `false`, not to be confused with the proposition `False`. -/
   | false : Bool
-  /-- The Boolean value `true`, not to be confused with the proposition `True`. -/
+  /-- The boolean value `true`, not to be confused with the proposition `True`. -/
   | true : Bool
 
 export Bool (false true)
@@ -901,12 +900,7 @@ theorem of_decide_eq_self_eq_true [inst : DecidableEq α] (a : α) : Eq (decide
   | isTrue  _  => rfl
   | isFalse h₁ => absurd rfl h₁
 
-/--
-Decides whether two Booleans are equal.
-
-This function should normally be called via the `DecidableEq Bool` instance that it exists to
-support.
--/
+/-- Decidable equality for Bool -/
 @[inline] def Bool.decEq (a b : Bool) : Decidable (Eq a b) :=
    match a, b with
    | false, false => isTrue rfl
@@ -1008,34 +1002,22 @@ instance [dp : Decidable p] : Decidable (Not p) :=
 /-! # Boolean operators -/
 
 /--
-The conditional function.
-
-`cond c x y` is the same as `if c then x else y`, but optimized for a Boolean condition rather than
-a decidable proposition. It can also be written using the notation `bif c then x else y`.
-
-Just like `ite`, `cond` is declared `@[macro_inline]`, which causes applications of `cond` to be
-unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and
-only the selected branch is evaluated.
+`cond b x y` is the same as `if b then x else y`, but optimized for a
+boolean condition. It can also be written as `bif b then x else y`.
+This is `@[macro_inline]` because `x` and `y` should not
+be eagerly evaluated (see `ite`).
 -/
-@[macro_inline] def cond {α : Sort u} (c : Bool) (x y : α) : α :=
+@[macro_inline] def cond {α : Type u} (c : Bool) (x y : α) : α :=
   match c with
   | true  => x
   | false => y
 
 
 /--
-The dependent conditional function, in which each branch is provided with a local assumption about
-the condition's value. This allows the value to be used in proofs as well as for control flow.
-
-`dcond c (fun h => x) (fun h => y)` is the same as `if h : c then x else y`, but optimized for a
-Boolean condition rather than a decidable proposition. Unlike the non-dependent version `cond`,
-there is no special notation for `dcond`.
-
-Just like `ite`, `dite`, and `cond`, `dcond` is declared `@[macro_inline]`, which causes
-applications of `dcond` to be unfolded. As a result, `x` and `y` are not evaluated at runtime until
-one of them is selected, and only the selected branch is evaluated. `dcond` is intended for
-metaprogramming use, rather than for use in verified programs, so behavioral lemmas are not
-provided.
+`Bool.dcond b (fun h => x) (fun h => y)` is the same as `if h _ : b then x else y`,
+but optimized for a boolean condition. It can also be written as `bif b then x else y`.
+This is `@[macro_inline]` because `x` and `y` should not be eagerly evaluated (see `dite`).
+This definition intendend for metaprogramming use, and does not come with a suitable API.
 -/
 @[macro_inline]
 protected def Bool.dcond {α : Sort u} (c : Bool) (x : Eq c true → α) (y : Eq c false → α) : α :=
@@ -1044,13 +1026,10 @@ protected def Bool.dcond {α : Sort u} (c : Bool) (x : Eq c true → α) (y : Eq
   | false => y rfl
 
 /--
-Boolean “or”, also known as disjunction. `or x y` can be written `x || y`.
-
-The corresponding propositional connective is `Or : Prop → Prop → Prop`, written with the `∨`
-operator.
-
-The Boolean `or` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
-if `x` is `true` then `y` is not evaluated at runtime.
+`or x y`, or `x || y`, is the boolean "or" operation (not to be confused
+with `Or : Prop → Prop → Prop`, which is the propositional connective).
+It is `@[macro_inline]` because it has C-like short-circuiting behavior:
+if `x` is true then `y` is not evaluated.
 -/
 @[macro_inline] def Bool.or (x y : Bool) : Bool :=
   match x with
@@ -1058,13 +1037,10 @@ if `x` is `true` then `y` is not evaluated at runtime.
   | false => y
 
 /--
-Boolean “and”, also known as conjunction. `and x y` can be written `x && y`.
-
-The corresponding propositional connective is `And : Prop → Prop → Prop`, written with the `∧`
-operator.
-
-The Boolean `and` is a `@[macro_inline]` function in order to give it short-circuiting evaluation:
-if `x` is `false` then `y` is not evaluated at runtime.
+`and x y`, or `x && y`, is the boolean "and" operation (not to be confused
+with `And : Prop → Prop → Prop`, which is the propositional connective).
+It is `@[macro_inline]` because it has C-like short-circuiting behavior:
+if `x` is false then `y` is not evaluated.
 -/
 @[macro_inline] def Bool.and (x y : Bool) : Bool :=
   match x with
@@ -1072,10 +1048,8 @@ if `x` is `false` then `y` is not evaluated at runtime.
   | true  => y
 
 /--
-Boolean negation, also known as Boolean complement. `not x` can be written `!x`.
-
-This is a function that maps the value `true` to `false` and the value `false` to `true`. The
-propositional connective is `Not : Prop → Prop`.
+`not x`, or `!x`, is the boolean "not" operation (not to be confused
+with `Not : Prop → Prop`, which is the propositional connective).
 -/
 @[inline] def Bool.not : Bool → Bool
   | true  => false
@@ -2249,13 +2223,12 @@ it is also not a "surrogate" character (the range `0xd800` to `0xdfff` inclusive
 abbrev UInt32.isValidChar (n : UInt32) : Prop :=
   n.toNat.isValidChar
 
-/--
-Characters are Unicode [scalar values](http://www.unicode.org/glossary/#unicode_scalar_value).
--/
+/-- The `Char` Type represents an unicode scalar value.
+    See http://www.unicode.org/glossary/#unicode_scalar_value). -/
 structure Char where
-  /-- The underlying Unicode scalar value as a `UInt32`. -/
+  /-- The underlying unicode scalar value as a `UInt32`. -/
   val   : UInt32
-  /-- The value must be a legal scalar value. -/
+  /-- The value must be a legal codepoint. -/
   valid : val.isValidChar
 
 private theorem isValidChar_UInt32 {n : Nat} (h : n.isValidChar) : LT.lt n UInt32.size :=
@@ -2272,8 +2245,8 @@ def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
   { val := ⟨BitVec.ofNatLT n (isValidChar_UInt32 h)⟩, valid := h }
 
 /--
-Converts a `Nat` into a `Char`. If the `Nat` does not encode a valid Unicode scalar value, `'\0'` is
-returned instead.
+Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scalar value,
+`'\0'` is returned instead.
 -/
 @[noinline, match_pattern]
 def Char.ofNat (n : Nat) : Char :=
@@ -2652,15 +2625,12 @@ attribute [nospecialize] Inhabited
 `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
 with elements from `α`. This type has special support in the runtime.
 
-Arrays perform best when unshared; as long
+An array has a size and a capacity; the size is `Array.size` but the capacity
+is not observable from Lean code. Arrays perform best when unshared; as long
 as they are used "linearly" all updates will be performed destructively on the
 array, so it has comparable performance to mutable arrays in imperative
 programming languages.
 
-An array has a size and a capacity; the size is `Array.size` but the capacity
-is not observable from Lean code. `Array.emptyWithCapacity n` creates an array which is equal to `#[]`,
-but internally allocates an array of capacity `n`.
-
 From the point of view of proofs `Array α` is just a wrapper around `List α`.
 -/
 structure Array (α : Type u) where
@@ -2692,22 +2662,13 @@ list.
 @[match_pattern]
 abbrev List.toArray (xs : List α) : Array α := .mk xs
 
-/-- Construct a new empty array with initial capacity `c`.
-
-This will be deprecated in favor of `Array.emptyWithCapacity` in the future.
--/
+/-- Construct a new empty array with initial capacity `c`. -/
 @[extern "lean_mk_empty_array_with_capacity"]
 def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α where
   toList := List.nil
 
-
-set_option linter.unusedVariables false in
-/-- Construct a new empty array with initial capacity `c`. -/
-def Array.emptyWithCapacity {α : Type u} (c : @& Nat) : Array α where
-  toList := List.nil
-
 /-- Construct a new empty array. -/
-def Array.empty {α : Type u} : Array α := emptyWithCapacity 0
+def Array.empty {α : Type u} : Array α := mkEmpty 0
 
 /-- Get the size of an array. This is a cached value, so it is O(1) to access. -/
 @[reducible, extern "lean_array_get_size"]
@@ -2751,39 +2712,39 @@ def Array.push {α : Type u} (a : Array α) (v : α) : Array α where
 
 /-- Create array `#[]` -/
 def Array.mkArray0 {α : Type u} : Array α :=
-  emptyWithCapacity 0
+  mkEmpty 0
 
 /-- Create array `#[a₁]` -/
 def Array.mkArray1 {α : Type u} (a₁ : α) : Array α :=
-  (emptyWithCapacity 1).push a₁
+  (mkEmpty 1).push a₁
 
 /-- Create array `#[a₁, a₂]` -/
 def Array.mkArray2 {α : Type u} (a₁ a₂ : α) : Array α :=
-  ((emptyWithCapacity 2).push a₁).push a₂
+  ((mkEmpty 2).push a₁).push a₂
 
 /-- Create array `#[a₁, a₂, a₃]` -/
 def Array.mkArray3 {α : Type u} (a₁ a₂ a₃ : α) : Array α :=
-  (((emptyWithCapacity 3).push a₁).push a₂).push a₃
+  (((mkEmpty 3).push a₁).push a₂).push a₃
 
 /-- Create array `#[a₁, a₂, a₃, a₄]` -/
 def Array.mkArray4 {α : Type u} (a₁ a₂ a₃ a₄ : α) : Array α :=
-  ((((emptyWithCapacity 4).push a₁).push a₂).push a₃).push a₄
+  ((((mkEmpty 4).push a₁).push a₂).push a₃).push a₄
 
 /-- Create array `#[a₁, a₂, a₃, a₄, a₅]` -/
 def Array.mkArray5 {α : Type u} (a₁ a₂ a₃ a₄ a₅ : α) : Array α :=
-  (((((emptyWithCapacity 5).push a₁).push a₂).push a₃).push a₄).push a₅
+  (((((mkEmpty 5).push a₁).push a₂).push a₃).push a₄).push a₅
 
 /-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆]` -/
 def Array.mkArray6 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ : α) : Array α :=
-  ((((((emptyWithCapacity 6).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆
+  ((((((mkEmpty 6).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆
 
 /-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆, a₇]` -/
 def Array.mkArray7 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ : α) : Array α :=
-  (((((((emptyWithCapacity 7).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇
+  (((((((mkEmpty 7).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇
 
 /-- Create array `#[a₁, a₂, a₃, a₄, a₅, a₆, a₇, a₈]` -/
 def Array.mkArray8 {α : Type u} (a₁ a₂ a₃ a₄ a₅ a₆ a₇ a₈ : α) : Array α :=
-  ((((((((emptyWithCapacity 8).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇).push a₈
+  ((((((((mkEmpty 8).push a₁).push a₂).push a₃).push a₄).push a₅).push a₆).push a₇).push a₈
 
 /-- Slower `Array.append` used in quotations. -/
 protected def Array.appendCore {α : Type u}  (as : Array α) (bs : Array α) : Array α :=
@@ -2810,7 +2771,7 @@ def Array.extract (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : A
         | Nat.succ i' => loop i' (hAdd j 1) (bs.push (as.getInternal j hlt)))
       (fun _ => bs)
   let sz' := Nat.sub (min stop as.size) start
-  loop sz' start (emptyWithCapacity sz')
+  loop sz' start (mkEmpty sz')
 
 /-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/
 class Bind (m : Type u → Type v) where

src/Init/System/IO.lean

@@ -57,11 +57,6 @@ def EIO.catchExceptions (act : EIO ε α) (h : ε → BaseIO α) : BaseIO α :=
   | EStateM.Result.ok a s     => EStateM.Result.ok a s
   | EStateM.Result.error ex s => h ex s
 
-def EIO.ofExcept (e : Except ε α) : EIO ε α :=
-  match e with
-  | Except.ok a    => pure a
-  | Except.error e => throw e
-
 open IO (Error) in
 abbrev IO : Type → Type := EIO Error
 
@@ -645,7 +640,7 @@ def readBinFile (fname : FilePath) : IO ByteArray := do
     if size > 0 then
       handle.read mdata.byteSize.toUSize
     else
-      pure <| ByteArray.emptyWithCapacity 0
+      pure <| ByteArray.mkEmpty 0
   handle.readBinToEndInto buf
 
 def readFile (fname : FilePath) : IO String := do

src/Init/System/IOError.lean

@@ -48,9 +48,7 @@ inductive IO.Error where
 
   | unexpectedEof
   | userError (msg : String)
-
-instance : Inhabited IO.Error where
-  default := .userError "(`Inhabited.default` for `IO.Error`)"
+  deriving Inhabited
 
 @[export lean_mk_io_user_error]
 def IO.userError (s : String) : IO.Error :=

src/Init/System/Platform.lean

@@ -26,11 +26,9 @@ def target : String := getTarget ()
 theorem numBits_pos : 0 < numBits := by
   cases numBits_eq <;> next h => simp [h]
 
-@[simp]
 theorem le_numBits : 32 ≤ numBits := by
   cases numBits_eq <;> next h => simp [h]
 
-@[simp]
 theorem numBits_le : numBits ≤ 64 := by
   cases numBits_eq <;> next h => simp [h]
 

src/Init/System/Promise.lean

@@ -73,12 +73,5 @@ def Promise.result := @Promise.result!
 /--
 Like `Promise.result`, but resolves to `dflt` if the promise is dropped without ever being resolved.
 -/
-@[macro_inline] def Promise.resultD (promise : Promise α) (dflt : α) : Task α :=
+def Promise.resultD (promise : Promise α) (dflt : α): Task α :=
   promise.result?.map (sync := true) (·.getD dflt)
-
-/--
-Checks whether the promise has already been resolved, i.e. whether access to `result*` will return
-immediately.
--/
-def Promise.isResolved (promise : Promise α) : BaseIO Bool :=
-  IO.hasFinished promise.result?

src/Init/Tactics.lean

@@ -461,14 +461,11 @@ syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
 /-- The `*` location refers to all hypotheses and the goal. -/
 syntax locationWildcard := " *"
 
-/-- The `⊢` location refers to the current goal. -/
-syntax locationType := patternIgnore(atomic("|" noWs "-") <|> "⊢")
-
 /--
-A sequence of one or more locations at which a tactic should operate. These can include local
-hypotheses and `⊢`, which denotes the goal.
+A hypothesis location specification consists of 1 or more hypothesis references
+and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (ppSpace colGt (term:max <|> locationType))+
+syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
 
 /--
 Location specifications are used by many tactics that can operate on either the
@@ -1350,7 +1347,7 @@ syntax (name := omega) "omega" optConfig : tactic
 Currently the preprocessor is implemented as `try simp only [bitvec_to_nat] at *`.
 `bitvec_to_nat` is a `@[simp]` attribute that you can (cautiously) add to more theorems.
 -/
-macro "bv_omega" : tactic => `(tactic| (try simp -implicitDefEqProofs only [bitvec_to_nat] at *) <;> omega)
+macro "bv_omega" : tactic => `(tactic| (try simp only [bitvec_to_nat] at *) <;> omega)
 
 /-- Implementation of `ac_nf` (the full `ac_nf` calls `trivial` afterwards). -/
 syntax (name := acNf0) "ac_nf0" (location)? : tactic

src/Lean.lean

@@ -39,4 +39,3 @@ import Lean.AddDecl
 import Lean.Replay
 import Lean.PrivateName
 import Lean.PremiseSelection
-import Lean.Namespace

src/Lean/AddDecl.lean

@@ -5,10 +5,15 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.CoreM
-import Lean.Namespace
 
 namespace Lean
 
+register_builtin_option debug.skipKernelTC : Bool := {
+  defValue := false
+  group    := "debug"
+  descr    := "skip kernel type checker. WARNING: setting this option to true may compromise soundness because your proofs will not be checked by the Lean kernel"
+}
+
 /-- Adds given declaration to the environment, respecting `debug.skipKernelTC`. -/
 def Kernel.Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
     (cancelTk? : Option IO.CancelToken := none) : Except Exception Environment :=
@@ -47,9 +52,9 @@ where go env
 def addDecl (decl : Declaration) : CoreM Unit := do
   -- register namespaces for newly added constants; this used to be done by the kernel itself
   -- but that is incompatible with moving it to a separate task
-  -- NOTE: we do not use `getTopLevelNames` here so that inductive types are registered as
-  -- namespaces
   modifyEnv (decl.getNames.foldl registerNamePrefixes)
+  if let .inductDecl _ _ types _ := decl then
+    modifyEnv (types.foldl (registerNamePrefixes · <| ·.name ++ `rec))
 
   if !Elab.async.get (← getOptions) then
     return (← doAdd)
@@ -80,9 +85,9 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t, cancelTk? := cancelTk }
 where doAdd := do
   profileitM Exception "type checking" (← getOptions) do
-    withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getNames}") do
       if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
+        logWarning m!"declaration uses 'sorry'"
       let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
         |> ofExceptKernelException
       setEnv env

src/Lean/Attributes.lean

@@ -252,13 +252,6 @@ def registerEnumAttributes (attrDescrs : List (Name × String × α))
       let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[]
       r.qsort (fun a b => Name.quickLt a.1 b.1)
     statsFn         := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
-    -- We assume (and check below) that, if used asynchronously, enum attributes are set only in the
-    -- same context in which the tagged declaration was created
-    asyncMode       := .async
-    replay?         := some fun _ newState consts st => consts.foldl (init := st) fun st c =>
-      match newState.find? c with
-      | some v => st.insert c v
-      | _      => st
   }
   let attrs := attrDescrs.map fun (name, descr, val) => {
     ref             := ref
@@ -286,16 +279,15 @@ def getValue [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl
     match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default) (fun a b => Name.quickLt a.1 b.1) with
     | some (_, val) => some val
     | none          => none
-  | none        => (attr.ext.findStateAsync env decl).find? decl
+  | none        => (attr.ext.getState env).find? decl
 
-def setValue (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment := do
+def setValue (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment :=
   if (env.getModuleIdxFor? decl).isSome then
-    throw s!"invalid '{attrs.ext.name}'.setValue, declaration is in an imported module"
-  if !env.asyncMayContain decl then
-    throw s!"invalid '{attrs.ext.name}'.setValue, declaration is not from this async context"
-  if ((attrs.ext.findStateAsync env decl).find? decl).isSome then
-    throw s!"invalid '{attrs.ext.name}'.setValue, attribute has already been set"
-  return attrs.ext.addEntry env (decl, val)
+    Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, declaration is in an imported module")
+  else if ((attrs.ext.getState env).find? decl).isSome then
+    Except.error ("invalid '" ++ toString attrs.ext.name ++ "'.setValue, attribute has already been set")
+  else
+    Except.ok (attrs.ext.addEntry env (decl, val))
 
 end EnumAttributes
 

src/Lean/Compiler/ClosedTermCache.lean

@@ -11,17 +11,10 @@ namespace Lean
 structure ClosedTermCache where
   map        : PHashMap Expr Name := {}
   constNames : NameSet := {}
-  -- used for `replay?` only
-  revExprs   : List Expr := []
   deriving Inhabited
 
 builtin_initialize closedTermCacheExt : EnvExtension ClosedTermCache ←
   registerEnvExtension (pure {}) (asyncMode := .sync)  -- compilation is non-parallel anyway
-    (replay? := some fun oldState newState _ s =>
-      let newExprs := newState.revExprs.take (newState.revExprs.length - oldState.revExprs.length)
-      newExprs.foldl (init := s) fun s e =>
-        let c := newState.map.find! e
-        { s with map := s.map.insert e c, constNames := s.constNames.insert c, revExprs := e :: s.revExprs })
 
 @[export lean_cache_closed_term_name]
 def cacheClosedTermName (env : Environment) (e : Expr) (n : Name) : Environment :=

src/Lean/Compiler/IR/CompilerM.lean

@@ -94,7 +94,6 @@ builtin_initialize declMapExt : SimplePersistentEnvExtension Decl DeclMap ←
     -- share a name prefix with the top-level Lean declaration being compiled, e.g. from
     -- specialization.
     asyncMode     := .sync
-    replay?       := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·.name) (fun s d => s.insert d.name d)
   }
 
 @[export lean_ir_find_env_decl]

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -143,7 +143,6 @@ builtin_initialize functionSummariesExt : SimplePersistentEnvExtension (FunId ×
     addEntryFn := fun s ⟨e, n⟩ => s.insert e n
     toArrayFn := fun s => sortEntries s.toArray
     asyncMode := .sync  -- compilation is non-parallel anyway
-    replay? := some <| SimplePersistentEnvExtension.replayOfFilter (!·.contains ·.1) (fun s ⟨e, n⟩ => s.insert e n)
   }
 
 def addFunctionSummary (env : Environment) (fid : FunId) (v : Value) : Environment :=

src/Lean/Compiler/IR/EmitC.lean

@@ -155,7 +155,6 @@ def emitMainFn : M Unit := do
   int main(int argc, char ** argv) {
   #if defined(WIN32) || defined(_WIN32)
   SetErrorMode(SEM_FAILCRITICALERRORS);
-  SetConsoleOutputCP(CP_UTF8);
   #endif
   lean_object* in; lean_object* res;";
     if usesLeanAPI then

src/Lean/Compiler/LCNF/ElimDeadBranches.lean

@@ -514,9 +514,7 @@ def inferStep : InterpM Bool := do
     let currentVal ← getFunVal idx
     withReader (fun ctx => { ctx with currFnIdx := idx }) do
       decl.params.forM fun p => updateVarAssignment p.fvarId .top
-      match decl.value with
-      | .code code .. => interpCode code
-      | .extern .. => updateCurrFnSummary .top
+      decl.value.forCodeM interpCode
     let newVal ← getFunVal idx
     if currentVal != newVal then
       return true

src/Lean/Compiler/LCNF/ReduceArity.lean

@@ -149,10 +149,8 @@ def Decl.reduceArity (decl : Decl) : CompilerM (Array Decl) := do
   match decl.value with
   | .code code =>
     let used ← collectUsedParams decl
-    if used.size == decl.params.size || used.size == 0 then
-      -- Do nothing if all params were used, or if no params were used. In the latter case,
-      -- this would promote the decl to a constant, which could execute unreachable code.
-      return #[decl]
+    if used.size == decl.params.size then
+      return #[decl] -- Declarations uses all parameters
     else
       trace[Compiler.reduceArity] "{decl.name}, used params: {used.toList.map mkFVar}"
       let mask   := decl.params.map fun param => used.contains param.fvarId

src/Lean/Compiler/Specialize.lean

@@ -111,9 +111,6 @@ builtin_initialize specExtension : SimplePersistentEnvExtension SpecEntry SpecSt
     addEntryFn    := SpecState.addEntry,
     addImportedFn := fun es => (mkStateFromImportedEntries SpecState.addEntry {} es).switch
     asyncMode     := .sync  -- compilation is non-parallel anyway
-    replay?       := some <| SimplePersistentEnvExtension.replayOfFilter (fun
-      | s, .info n _ => !s.specInfo.contains n
-      | s, .cache key _ => !s.cache.contains key) SpecState.addEntry
   }
 
 @[export lean_add_specialization_info]

src/Lean/CoreM.lean

@@ -44,13 +44,6 @@ register_builtin_option Elab.async : Bool := {
       `Lean.Command.State.snapshotTasks`."
 }
 
-/-- Performance option used by cmdline driver. -/
-register_builtin_option internal.cmdlineSnapshots : Bool := {
-  defValue := false
-  descr    := "reduce information stored in snapshots to the minimum necessary \
-    for the cmdline driver: diagnostics per command and final full snapshot"
-}
-
 /--
 If the `diagnostics` option is not already set, gives a message explaining this option.
 Begins with a `\n\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.
@@ -201,7 +194,7 @@ protected def withFreshMacroScope (x : CoreM α) : CoreM α := do
 
 instance : MonadQuotation CoreM where
   getCurrMacroScope   := return (← read).currMacroScope
-  getMainModule       := return (← getEnv).mainModule
+  getMainModule       := return (← get).env.mainModule
   withFreshMacroScope := Core.withFreshMacroScope
 
 instance : Elab.MonadInfoTree CoreM where
@@ -372,16 +365,6 @@ for incremental reporting during elaboration of a single command.
 def getAndEmptyMessageLog : CoreM MessageLog :=
   modifyGet fun s => (s.messages, { s with messages := s.messages.markAllReported })
 
-/--
-Returns the current set of tasks added by `logSnapshotTask` and then resets it. When
-saving/restoring state of an action that may have logged such tasks during incremental reuse, this
-function must be used to store them in the corresponding snapshot tree; otherwise, they will leak
-outside and may be cancelled by a later step, potentially leading to inconsistent state being
-reused.
--/
-def getAndEmptySnapshotTasks : CoreM (Array (Language.SnapshotTask Language.SnapshotTree)) :=
-  modifyGet fun s => (s.snapshotTasks, { s with snapshotTasks := #[] })
-
 instance : MonadLog CoreM where
   getRef      := getRef
   getFileMap  := return (← read).fileMap
@@ -430,26 +413,6 @@ register_builtin_option stderrAsMessages : Bool := {
   descr    := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message"
 }
 
-/--
-Creates snapshot reporting given `withIsolatedStreams` output and diagnostics and traces from the
-given state.
--/
-def mkSnapshot (output : String) (ctx : Context) (st : State)
-    (desc : String := by exact decl_name%.toString) : BaseIO Language.SnapshotTree := do
-  let mut msgs := st.messages
-  if !output.isEmpty then
-    msgs := msgs.add {
-      fileName := ctx.fileName
-      severity := MessageSeverity.information
-      pos      := ctx.fileMap.toPosition <| ctx.ref.getPos?.getD 0
-      data     := output
-    }
-  return .mk {
-    desc
-    diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog msgs)
-    traces := st.traceState
-  } st.snapshotTasks
-
 open Language in
 /--
 Wraps the given action for use in `BaseIO.asTask` etc., discarding its final state except for
@@ -480,7 +443,20 @@ def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (cancelTk? : Option IO.Cance
   let ctx ← readThe Core.Context
   return do
     match (← t.toBaseIO) with
-    | .ok (output, st) => mkSnapshot output ctx st desc
+    | .ok (output, st) =>
+      let mut msgs := st.messages
+      if !output.isEmpty then
+        msgs := msgs.add {
+          fileName := ctx.fileName
+          severity := MessageSeverity.information
+          pos      := ctx.fileMap.toPosition <| ctx.ref.getPos?.getD 0
+          data     := output
+        }
+      return .mk {
+        desc
+        diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog msgs)
+        traces := st.traceState
+      } st.snapshotTasks
     -- interrupt or abort exception as `try catch` above should have caught any others
     | .error _ => default
 
@@ -552,9 +528,7 @@ opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List N
 -- `ref?` is used for error reporting if available
 partial def compileDecls (decls : List Name) (ref? : Option Declaration := none)
     (logErrors := true) : CoreM Unit := do
-  -- When inside `realizeConst`, do compilation synchronously so that `_cstage*` constants are found
-  -- by the replay code
-  if !Elab.async.get (← getOptions) || (← getEnv).isRealizing then
+  if !Elab.async.get (← getOptions) then
     doCompile
     return
   let env ← getEnv
@@ -672,11 +646,6 @@ def logMessageKind (kind : Name) : CoreM Bool := do
     modify fun s => { s with messages.loggedKinds := s.messages.loggedKinds.insert kind }
     return true
 
-@[inherit_doc Environment.enableRealizationsForConst]
-def enableRealizationsForConst (n : Name) : CoreM Unit := do
-  let env ← (← getEnv).enableRealizationsForConst (← getOptions) n
-  setEnv env
-
 builtin_initialize
   registerTraceClass `Elab.async
   registerTraceClass `Elab.block

src/Lean/Data/Lsp/Capabilities.lean

@@ -59,29 +59,12 @@ structure WorkspaceClientCapabilities where
   workspaceEdit? : Option WorkspaceEditClientCapabilities := none
   deriving ToJson, FromJson
 
-structure LeanClientCapabilities where
-  /--
-  Whether the client supports `DiagnosticWith.isSilent = true`.
-  If `none` or `false`, silent diagnostics will not be served to the client.
-  -/
-  silentDiagnosticSupport? : Option Bool := none
-  deriving ToJson, FromJson
-
 structure ClientCapabilities where
   textDocument? : Option TextDocumentClientCapabilities := none
   window?       : Option WindowClientCapabilities       := none
   workspace?    : Option WorkspaceClientCapabilities    := none
-  /-- Capabilties for Lean language server extensions. -/
-  lean?         : Option LeanClientCapabilities         := none
   deriving ToJson, FromJson
 
-def ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool := Id.run do
-  let some lean := c.lean?
-    | return false
-  let some silentDiagnosticSupport := lean.silentDiagnosticSupport?
-    | return false
-  return silentDiagnosticSupport
-
 -- TODO largely unimplemented
 structure ServerCapabilities where
   textDocumentSync?         : Option TextDocumentSyncOptions := none

src/Lean/Data/Lsp/Diagnostics.lean

@@ -66,42 +66,13 @@ inductive DiagnosticTag where
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
-  | Except.ok 1  => return DiagnosticTag.unnecessary
-  | Except.ok 2  => return DiagnosticTag.deprecated
-  | _            => throw "unknown DiagnosticTag"⟩
+  | Except.ok 1 => return DiagnosticTag.unnecessary
+  | Except.ok 2 => return DiagnosticTag.deprecated
+  | _      => throw "unknown DiagnosticTag"⟩
 
 instance : ToJson DiagnosticTag := ⟨fun
-  | DiagnosticTag.unnecessary   => (1 : Nat)
-  | DiagnosticTag.deprecated    => (2 : Nat)⟩
-
-/--
-Custom diagnostic tags provided by the language server.
-We use a separate diagnostic field for this to avoid confusing LSP clients with our custom tags.
--/
-inductive LeanDiagnosticTag where
-  /--
-  Diagnostics representing an "unsolved goals" error.
-  Corresponds to `MessageData.tagged `Tactic.unsolvedGoals ..`.
-  -/
-  | unsolvedGoals
-  /--
-  Diagnostics representing a "goals accomplished" silent message.
-  Corresponds to `MessageData.tagged `goalsAccomplished ..`.
-  -/
-  | goalsAccomplished
-  deriving Inhabited, BEq, Ord
-
-instance : FromJson LeanDiagnosticTag where
-  fromJson? j :=
-    match j.getNat? with
-    | .ok 1 => return LeanDiagnosticTag.unsolvedGoals
-    | .ok 2 => return LeanDiagnosticTag.goalsAccomplished
-    | _     => throw "unknown LeanDiagnosticTag"
-
-instance : ToJson LeanDiagnosticTag where
-  toJson
-  | .unsolvedGoals => (1 : Nat)
-  | .goalsAccomplished => (2 : Nat)
+  | DiagnosticTag.unnecessary => (1 : Nat)
+  | DiagnosticTag.deprecated  => (2 : Nat)⟩
 
 /-- Represents a related message and source code location for a diagnostic.
     This should be used to point to code locations that cause or are related to
@@ -123,13 +94,6 @@ structure DiagnosticWith (α : Type) where
   /-- Extension: preserve semantic range of errors when truncating them for display purposes. -/
   fullRange? : Option Range := some range
   severity? : Option DiagnosticSeverity := none
-  /--
-  Extension: whether this diagnostic should not be displayed as a regular diagnostic in the editor.
-  In VS Code, this means that the diagnostic does not have a squiggly and is not displayed in
-  the InfoView under 'All Messages', but it is still displayed under 'Messages'.
-  Defaults to `false`.
-  -/
-  isSilent? : Option Bool := none
   /-- The diagnostic's code, which might appear in the user interface. -/
   code? : Option DiagnosticCode := none
   /-- A human-readable string describing the source of this diagnostic, e.g. 'typescript' or 'super lint'. -/
@@ -140,8 +104,6 @@ structure DiagnosticWith (α : Type) where
   message : α
   /-- Additional metadata about the diagnostic. -/
   tags? : Option (Array DiagnosticTag) := none
-  /-- Additional Lean-specific metadata about the diagnostic. -/
-  leanTags? : Option (Array LeanDiagnosticTag) := none
   /-- An array of related diagnostic information, e.g. when symbol-names within a scope collide all definitions can be marked via this property. -/
   relatedInformation? : Option (Array DiagnosticRelatedInformation) := none
   /-- A data entry field that is preserved between a `textDocument/publishDiagnostics` notification and `textDocument/codeAction` request. -/

src/Lean/Data/Lsp/Internal.lean

@@ -7,7 +7,6 @@ Authors: Joscha Mennicken
 prelude
 import Lean.Expr
 import Lean.Data.Lsp.Basic
-import Std.Data.TreeMap
 
 set_option linter.missingDocs true -- keep it documented
 
@@ -30,7 +29,7 @@ inductive RefIdent where
   | const (moduleName : String) (identName : String) : RefIdent
   /-- Unnamed identifier. These are used for all local references. -/
   | fvar (moduleName : String) (id : String) : RefIdent
-  deriving BEq, Hashable, Inhabited, Ord
+  deriving BEq, Hashable, Inhabited
 
 namespace RefIdent
 
@@ -155,13 +154,7 @@ instance : FromJson RefInfo where
     pure { definition?, usages }
 
 /-- References from a single module/file -/
-def ModuleRefs := Std.TreeMap RefIdent RefInfo
-  deriving EmptyCollection
-
-instance : ForIn m ModuleRefs (RefIdent × RefInfo) where
-  forIn map init f :=
-    let map : Std.TreeMap RefIdent RefInfo := map
-    forIn map init f
+def ModuleRefs := Std.HashMap RefIdent RefInfo
 
 instance : ToJson ModuleRefs where
   toJson m := Json.mkObj <| m.toList.map fun (ident, info) => (ident.toJson.compress, toJson info)
@@ -169,7 +162,7 @@ instance : ToJson ModuleRefs where
 instance : FromJson ModuleRefs where
   fromJson? j := do
     let node ← j.getObj?
-    node.foldM (init := ∅) fun m k v =>
+    node.foldM (init := Std.HashMap.empty) fun m k v =>
       return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v)
 
 /--

src/Lean/Data/Lsp/Utf16.lean

@@ -15,7 +15,6 @@ to interact with Lean strings using UTF-16 indices. -/
 
 namespace Char
 
-/-- Returns the number of bytes required to encode this `Char` in UTF-16. -/
 def utf16Size (c : Char) : UInt32 :=
   if c.val ≤ 0xFFFF then 1 else 2
 

src/Lean/Data/Name.lean

@@ -132,7 +132,6 @@ def isInternalDetail : Name → Bool
       || matchPrefix s "eq_"
       || matchPrefix s "match_"
       || matchPrefix s "proof_"
-      || matchPrefix s "omega_"
       || p.isInternalOrNum
   | .num _ _     => true
   | p            => p.isInternalOrNum

src/Lean/Declaration.lean

@@ -194,22 +194,8 @@ def Declaration.definitionVal! : Declaration → DefinitionVal
   | _ => panic! "Expected a `Declaration.defnDecl`."
 
 /--
-Returns all top-level names to be defined by adding this declaration to the environment, i.e.
-excluding nested helper declarations generated automatically.
--/
-def Declaration.getTopLevelNames : Declaration → List Name
-  | .axiomDecl val          => [val.name]
-  | .defnDecl val           => [val.name]
-  | .thmDecl val            => [val.name]
-  | .opaqueDecl val         => [val.name]
-  | .quotDecl               => [``Quot]
-  | .mutualDefnDecl defns   => defns.map (·.name)
-  | .inductDecl _ _ types _ => types.map (·.name)
-
-/--
-Returns all names to be defined by adding this declaration to the environment. This does not include
-auxiliary definitions such as projections added by the elaborator, nor auxiliary recursors computed
-by the kernel for nested inductive types.
+Returns all top-level names to be defined by adding this declaration to the environment. This does
+not include auxiliary definitions such as projections.
 -/
 def Declaration.getNames : Declaration → List Name
   | .axiomDecl val          => [val.name]
@@ -218,7 +204,7 @@ def Declaration.getNames : Declaration → List Name
   | .opaqueDecl val         => [val.name]
   | .quotDecl               => [``Quot, ``Quot.mk, ``Quot.lift, ``Quot.ind]
   | .mutualDefnDecl defns   => defns.map (·.name)
-  | .inductDecl _ _ types _ => types.flatMap fun t => t.name :: (t.name.appendCore `rec) :: t.ctors.map (·.name)
+  | .inductDecl _ _ types _ => types.map (·.name)
 
 @[specialize] def Declaration.foldExprM {α} {m : Type → Type} [Monad m] (d : Declaration) (f : α → Expr → m α) (a : α) : m α :=
   match d with

src/Lean/DeclarationRange.lean

@@ -20,7 +20,8 @@ def addBuiltinDeclarationRanges (declName : Name) (declRanges : DeclarationRange
   builtinDeclRanges.modify (·.insert declName declRanges)
 
 def addDeclarationRanges [Monad m] [MonadEnv m] (declName : Name) (declRanges : DeclarationRanges) : m Unit := do
-  modifyEnv fun env => declRangeExt.insert env declName declRanges
+  unless declRangeExt.contains (← getEnv) declName do
+    modifyEnv fun env => declRangeExt.insert env declName declRanges
 
 def findDeclarationRangesCore? [Monad m] [MonadEnv m] (declName : Name) : m (Option DeclarationRanges) :=
   return declRangeExt.find? (← getEnv) declName

src/Lean/Elab/App.lean

@@ -1215,7 +1215,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     let fullName := Name.mkStr structName fieldName
     for localDecl in (← getLCtx) do
       if localDecl.isAuxDecl then
-        if let some localDeclFullName := (← getLCtx).auxDeclToFullName.find? localDecl.fvarId then
+        if let some localDeclFullName := (← read).auxDeclToFullName.find? localDecl.fvarId then
           if fullName == (privateToUserName? localDeclFullName).getD localDeclFullName then
             /- LVal notation is being used to make a "local" recursive call. -/
             return LValResolution.localRec structName fullName localDecl.toExpr

src/Lean/Elab/BuiltinNotation.lean

@@ -201,27 +201,12 @@ private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do
 
 @[builtin_macro Lean.Parser.Term.assert]  def expandAssert : Macro
   | `(assert! $cond; $body) =>
+    -- TODO: support for disabling runtime assertions
     match cond.raw.reprint with
     | some code => `(if $cond then $body else panic! ("assertion violation: " ++ $(quote code)))
     | none => `(if $cond then $body else panic! ("assertion violation"))
   | _ => Macro.throwUnsupported
 
-register_builtin_option debugAssertions : Bool := {
-  defValue := false
-  descr := "enable `debug_assert!` statements\
-    \n\
-    \nDefaults to `false` unless the Lake `buildType` is `debug`."
-}
-
-@[builtin_term_elab Lean.Parser.Term.debugAssert]  def elabDebugAssert : TermElab :=
-  adaptExpander fun
-    | `(Parser.Term.debugAssert| debug_assert! $cond; $body) => do
-      if debugAssertions.get (← getOptions) then
-        `(assert! $cond; $body)
-      else
-        return body
-    | _ => throwUnsupportedSyntax
-
 @[builtin_macro Lean.Parser.Term.dbgTrace]  def expandDbgTrace : Macro
   | `(dbg_trace $arg:interpolatedStr; $body) => `(dbgTrace (s! $arg) fun _ => $body)
   | `(dbg_trace $arg:term; $body)            => `(dbgTrace (toString $arg) fun _ => $body)

src/Lean/Elab/Command.lean

@@ -491,8 +491,6 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                   -- check absence of traces; see Note [Incremental Macros]
                   guard <| !oldSnap.hasTraces && !hasTraces
                   return oldSnap
-                if snap.old?.isSome && oldSnap?.isNone then
-                  snap.old?.forM (·.val.cancelRec)
                 let oldCmds? := oldSnap?.map fun old =>
                   if old.newStx.isOfKind nullKind then old.newStx.getArgs else #[old.newStx]
                 let cmdPromises ← cmds.mapM fun _ => IO.Promise.new
@@ -521,8 +519,6 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
                       let old ← oldSnap?
                       return { stx := (← oldCmd?), val := (← old.next[i]?) }
                   } }) do
-                    if oldSnap?.isSome && (← read).snap?.isNone then
-                      oldSnap?.bind (·.next[i]?) |>.forM (·.cancelRec)
                     elabCommand cmd
                     -- Resolve promise for commands not supporting incrementality; waiting for
                     -- `withAlwaysResolvedPromises` to do this could block reporting by later

src/Lean/Elab/DefView.lean

@@ -49,11 +49,9 @@ structure BodyProcessedSnapshot extends Language.Snapshot where
   state : Term.SavedState
   /-- Elaboration result. -/
   value : Expr
-  /-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation. -/
-  moreSnaps : Array (SnapshotTask SnapshotTree)
 deriving Nonempty
 instance : Language.ToSnapshotTree BodyProcessedSnapshot where
-  toSnapshotTree s := ⟨s.toSnapshot, s.moreSnaps⟩
+  toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
 
 /-- Snapshot after elaboration of a definition header. -/
 structure HeaderProcessedSnapshot extends Language.Snapshot where
@@ -69,15 +67,13 @@ structure HeaderProcessedSnapshot extends Language.Snapshot where
   bodyStx : Syntax
   /-- Result of body elaboration. -/
   bodySnap : SnapshotTask (Option BodyProcessedSnapshot)
-  /-- Untyped snapshots from `logSnapshotTask`, saved at this level for cancellation. -/
-  moreSnaps : Array (SnapshotTask SnapshotTree)
 deriving Nonempty
 instance : Language.ToSnapshotTree HeaderProcessedSnapshot where
   toSnapshotTree s := ⟨s.toSnapshot,
     (match s.tacSnap? with
       | some tac => #[tac.map (sync := true) toSnapshotTree]
       | none     => #[]) ++
-    #[s.bodySnap.map (sync := true) toSnapshotTree] ++ s.moreSnaps⟩
+    #[s.bodySnap.map (sync := true) toSnapshotTree]⟩
 
 /-- State before elaboration of a mutual definition. -/
 structure DefParsed where

src/Lean/Elab/Deriving/DecEq.lean

@@ -134,7 +134,7 @@ partial def mkEnumOfNat (declName : Name) : MetaM Unit := do
   let enumType := mkConst declName
   let ctors := indVal.ctors.toArray
   withLocalDeclD `n (mkConst ``Nat) fun n => do
-    let cond := mkConst ``cond [1]
+    let cond := mkConst ``cond [levelZero]
     let rec mkDecTree (low high : Nat) : Expr :=
       if low + 1 == high then
         mkConst ctors[low]!