feat: theorems about Nat/Int/Rat needed for dyadics

.github/workflows/build-template.yml

@@ -36,7 +36,7 @@ jobs:
         include: ${{fromJson(inputs.config)}}
       # complete all jobs
       fail-fast: false
-    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
@@ -69,16 +69,10 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
-        if: (!endsWith(matrix.os, '-with-cache'))
         uses: actions/checkout@v4
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
-      - name: Namespace Checkout
-        if: endsWith(matrix.os, '-with-cache')
-        uses: namespacelabs/nscloud-checkout-action@v7
-        with:
-          ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once
         run: true
         if: runner.os == 'Linux'
@@ -175,9 +169,7 @@ jobs:
       # Should be done as early as possible and in particular *before* "Check rebootstrap" which
       # changes the state of stage1/
       - name: Save Cache
-        # Caching on cancellation created some mysterious issues perhaps related to improper build
-        # shutdown
-        if: steps.restore-cache.outputs.cache-hit != 'true' && !cancelled()
+        if: steps.restore-cache.outputs.cache-hit != 'true'
         uses: actions/cache/save@v4
         with:
           # NOTE: must be in sync with `restore` above
@@ -223,13 +215,13 @@ jobs:
           path: pack/*
       - name: Lean stats
         run: |
-          build/$TARGET_STAGE/bin/lean --stats src/Lean.lean -Dexperimental.module=true
+          build/stage1/bin/lean --stats src/Lean.lean -Dexperimental.module=true
         if: ${{ !matrix.cross }}
       - name: Test
         id: test
         run: |
           ulimit -c unlimited  # coredumps
-          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
+          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml
         if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
       - name: Test Summary
         uses: test-summary/action@v2

.github/workflows/ci.yml

@@ -182,10 +182,12 @@ jobs:
                 "binary-check": "ldd -v",
                 // foreign code may be linked against more recent glibc
                 "CTEST_OPTIONS": "-E 'foreign'",
+                // not compatible with `prepare-llvm` currently
+                "CMAKE_OPTIONS": "-DUSE_LAKE=OFF",
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16" : "ubuntu-latest",
                 "check-level": 0,
                 "test": true,
                 "check-rebootstrap": level >= 1,
@@ -200,6 +202,8 @@ jobs:
                 "os": "ubuntu-latest",
                 "check-level": 2,
                 "CMAKE_PRESET": "reldebug",
+                // exclude seriously slow/stackoverflowing tests
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest|bv_bitblast_stress|3807'"
               },
               // TODO: suddenly started failing in CI
               /*{
@@ -221,7 +225,8 @@ jobs:
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
-                "CTEST_OPTIONS": "-E 'leanlaketest_hello'", // started failing from unpack
+                // not compatible with `prepare-llvm` currently
+                "CMAKE_OPTIONS": "-DUSE_LAKE=OFF",
               },
               {
                 "name": "macOS aarch64",
@@ -237,6 +242,8 @@ jobs:
                 // See "Linux release" for release job levels; Grove is not a concern here
                 "check-level": isPr ? 0 : 2,
                 "secondary": isPr,
+                // not compatible with `prepare-llvm` currently
+                "CMAKE_OPTIONS": "-DUSE_LAKE=OFF",
               },
               {
                 "name": "Windows",
@@ -245,9 +252,13 @@ jobs:
                 "check-level": 2,
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
+                // for reasons unknown, interactivetests are flaky on Windows
+                "CTEST_OPTIONS": "--repeat until-pass:2",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
                 "binary-check": "ldd",
+                // not compatible with `prepare-llvm` currently
+                "CMAKE_OPTIONS": "-DUSE_LAKE=OFF",
               },
               {
                 "name": "Linux aarch64",
@@ -258,6 +269,8 @@ jobs:
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
+                // not compatible with `prepare-llvm` currently
+                "CMAKE_OPTIONS": "-DUSE_LAKE=OFF",
               },
               // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation
               //{
@@ -286,12 +299,6 @@ jobs:
               //   "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
               // }
             ];
-            for (const job of matrix) {
-              if (job["prepare-llvm"]) {
-                // `USE_LAKE` is not compatible with `prepare-llvm` currently
-                job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DUSE_LAKE=OFF";
-              }
-            }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
             matrix = matrix.filter((job) => level >= job["check-level"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));

.github/workflows/update-stage0.yml

@@ -19,8 +19,6 @@ concurrency:
 jobs:
   update-stage0:
     runs-on: nscloud-ubuntu-22.04-amd64-8x16
-    env:
-      CCACHE_DIR: ${{ github.workspace }}/.ccache
     steps:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at

README.md

@@ -9,7 +9,7 @@ This is the repository for **Lean 4**.
 - [Documentation Overview](https://lean-lang.org/documentation/)
 - [Language Reference](https://lean-lang.org/doc/reference/latest/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://lean-lang.org/lean4/doc/examples.html)
+- [Examples](https://lean-lang.org/documentation/examples/)
 - [External Contribution Guidelines](CONTRIBUTING.md)
 
 # Installation

doc/dev/index.md

@@ -8,7 +8,7 @@ You should not edit the `stage0` directory except using the commands described i
 
 ## Development Setup
 
-You can use any of the [supported editors](https://lean-lang.org/install/manual/) for editing the Lean source code.
+You can use any of the [supported editors](../setup.md) for editing the Lean source code.
 Please see below for specific instructions for VS Code.
 
 ### Dev setup using elan

doc/make/index.md

@@ -1,6 +1,6 @@
 These are instructions to set up a working development environment for those who wish to make changes to Lean itself. It is part of the [Development Guide](../dev/index.md).
 
-We strongly suggest that new users instead follow the [Installation Instructions](https://lean-lang.org/install/) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
+We strongly suggest that new users instead follow the [Quickstart](../quickstart.md) to get started using Lean, since this sets up an environment that can automatically manage multiple Lean toolchain versions, which is necessary when working within the Lean ecosystem.
 
 Requirements
 ------------

script/AnalyzeGrindAnnotations.lean

@@ -97,36 +97,5 @@ macro "#analyzeEMatchTheorems" : command => `(
 #analyzeEMatchTheorems
 
 -- -- We can analyze specific theorems using commands such as
-set_option trace.grind.ematch.instance true
-
--- 1. grind immediately sees `(#[] : Array α) = ([] : List α).toArray` but probably this should be hidden.
--- 2. `Vector.toArray_empty` keys on `Array.mk []` rather than `#v[].toArray`
--- I guess we could add `(#[].extract _ _).extract _ _` as a stop pattern.
-run_meta analyzeEMatchTheorem ``Array.extract_empty {}
-
--- Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
--- lambdas. So we get crazy things like:
--- `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
--- We could consider replacing `filterMap_some` with
--- `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
--- to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
-run_meta analyzeEMatchTheorem ``Array.filterMap_some {}
-
--- Not entirely certain what is wrong here, but certainly
--- `eq_empty_of_append_eq_empty` is firing too often.
--- Ideally we could instantiate this is we fine `xs ++ ys` in the same equivalence class,
--- note just as soon as we see `xs ++ ys`.
--- I've tried removing this in https://github.com/leanprover/lean4/pull/10162
-run_meta analyzeEMatchTheorem ``Array.range'_succ {}
-
--- Perhaps the same story here.
-run_meta analyzeEMatchTheorem ``Array.range_succ {}
-
--- `zip_map_left` and `zip_map_right` are bad grind lemmas,
--- checking if they can be removed in https://github.com/leanprover/lean4/pull/10163
-run_meta analyzeEMatchTheorem ``Array.zip_map {}
-
--- It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
--- pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
--- I don't think any forbidden subterms can help us here. I don't know what to do. :-(
-run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}
+set_option trace.grind.ematch.instance true in
+run_meta analyzeEMatchTheorem ``List.filterMap_some {}

src/CMakeLists.txt

@@ -469,7 +469,6 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
   string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
   string(APPEND LEANSHARED_1_LINKER_FLAGS " -install_name @rpath/libleanshared_1.dylib")
-  string(APPEND LEANSHARED_2_LINKER_FLAGS " -install_name @rpath/libleanshared_2.dylib")
   string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
   string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -install_name @rpath/libLake_shared.dylib")
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
@@ -503,7 +502,7 @@ endif()
 # are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   # import libraries created by the stdlib.make targets
-  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared")
+  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
 elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
   # The second flag is necessary to even *load* dylibs without resolved symbols, as can happen
   # if a Lake `extern_lib` depends on a symbols defined by the Lean library but is loaded even
@@ -590,7 +589,7 @@ endif()
 
 add_subdirectory(initialize)
 add_subdirectory(shell)
-# to be included in `leanshared` but not the smaller `leanshared_*` (as it would pull
+# to be included in `leanshared` but not the smaller `leanshared_1` (as it would pull
 # in the world)
 add_library(leaninitialize STATIC $<TARGET_OBJECTS:initialize>)
 set_target_properties(leaninitialize PROPERTIES
@@ -715,7 +714,6 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   )
   add_custom_target(leanshared ALL
     DEPENDS Init_shared leancpp
-    COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_2${CMAKE_SHARED_LIBRARY_SUFFIX}
     COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared_1${CMAKE_SHARED_LIBRARY_SUFFIX}
     COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
   )
@@ -736,7 +734,7 @@ else()
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
     VERBATIM)
 
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")

src/Init/Control/EState.lean

@@ -19,8 +19,8 @@ variable {ε σ α : Type u}
 
 instance [ToString ε] [ToString α] : ToString (Result ε σ α) where
   toString
-    | Result.ok a _    => String.Internal.append "ok: " (toString a)
-    | Result.error e _ => String.Internal.append "error: " (toString e)
+    | Result.ok a _    => "ok: " ++ toString a
+    | Result.error e _ => "error: " ++ toString e
 
 instance [Repr ε] [Repr α] : Repr (Result ε σ α) where
   reprPrec

src/Init/Control/Lawful/Instances.lean

@@ -7,10 +7,8 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Control.Except
-import all Init.Control.Except
-public import Init.Control.State
-import all Init.Control.State
+public import all Init.Control.Except
+public import all Init.Control.State
 public import Init.Control.StateRef
 public import Init.Ext
 
@@ -22,24 +20,23 @@ open Function
 
 namespace ExceptT
 
-@[ext, grind ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
+@[ext] theorem ext {x y : ExceptT ε m α} (h : x.run = y.run) : x = y := by
   simp [run] at h
   assumption
 
-@[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
+@[simp] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
 
-@[simp, grind =] theorem run_lift  [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
+@[simp] theorem run_lift  [Monad.{u, v} m] (x : m α) : run (ExceptT.lift x : ExceptT ε m α) = (Except.ok <$> x : m (Except ε α)) := rfl
 
-@[simp, grind =] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
+@[simp] theorem run_throw [Monad m] : run (throw e : ExceptT ε m β) = pure (Except.error e) := rfl
 
-@[simp, grind =] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
+@[simp] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → ExceptT ε m β) : run (ExceptT.lift x >>= f : ExceptT ε m β) = x >>= fun a => run (f a) := by
   simp [ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
 
-@[simp, grind =] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
+@[simp] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → ExceptT ε m β) : (throw e >>= f) = throw e := by
   simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]
 
-@[grind =]
-theorem run_bind [Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β)
+theorem run_bind [Monad m] (x : ExceptT ε m α)
         : run (x >>= f : ExceptT ε m β)
           =
           run x >>= fun
@@ -47,10 +44,10 @@ theorem run_bind [Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β)
                      | Except.error e => pure (Except.error e) :=
   rfl
 
-@[simp, grind =] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
+@[simp] theorem lift_pure [Monad m] [LawfulMonad m] (a : α) : ExceptT.lift (pure a) = (pure a : ExceptT ε m α) := by
   simp [ExceptT.lift, pure, ExceptT.pure]
 
-@[simp, grind =] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
+@[simp] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : ExceptT ε m α)
     : (f <$> x).run = Except.map f <$> x.run := by
   simp [Functor.map, ExceptT.map, ←bind_pure_comp]
   apply bind_congr
@@ -114,28 +111,28 @@ instance : LawfulFunctor (Except ε) := inferInstance
 
 namespace ReaderT
 
-@[ext, grind ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
+@[ext] theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y := by
   simp [run] at h
   exact funext h
 
-@[simp, grind =] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
+@[simp] theorem run_pure [Monad m] (a : α) (ctx : ρ) : (pure a : ReaderT ρ m α).run ctx = pure a := rfl
 
-@[simp, grind =] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
+@[simp] theorem run_bind [Monad m] (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) (ctx : ρ)
     : (x >>= f).run ctx = x.run ctx >>= λ a => (f a).run ctx := rfl
 
-@[simp, grind =] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
+@[simp] theorem run_mapConst [Monad m] (a : α) (x : ReaderT ρ m β) (ctx : ρ)
     : (Functor.mapConst a x).run ctx = Functor.mapConst a (x.run ctx) := rfl
 
-@[simp, grind =] theorem run_map [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ)
+@[simp] theorem run_map [Monad m] (f : α → β) (x : ReaderT ρ m α) (ctx : ρ)
     : (f <$> x).run ctx = f <$> x.run ctx := rfl
 
-@[simp, grind =] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
+@[simp] theorem run_monadLift [MonadLiftT n m] (x : n α) (ctx : ρ)
     : (monadLift x : ReaderT ρ m α).run ctx = (monadLift x : m α) := rfl
 
-@[simp, grind =] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ)
+@[simp] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : ReaderT ρ m α) (ctx : ρ)
     : (monadMap @f x : ReaderT ρ m α).run ctx = monadMap @f (x.run ctx) := rfl
 
-@[simp, grind =] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
+@[simp] theorem run_read [Monad m] (ctx : ρ) : (ReaderT.read : ReaderT ρ m ρ).run ctx = pure ctx := rfl
 
 @[simp] theorem run_seq {α β : Type u} [Monad m] (f : ReaderT ρ m (α → β)) (x : ReaderT ρ m α) (ctx : ρ)
     : (f <*> x).run ctx = (f.run ctx <*> x.run ctx) := rfl
@@ -176,39 +173,38 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) :=
 
 namespace StateT
 
-@[ext, grind ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
+@[ext] theorem ext {x y : StateT σ m α} (h : ∀ s, x.run s = y.run s) : x = y :=
   funext h
 
-@[simp, grind =] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
+@[simp] theorem run'_eq [Monad m] (x : StateT σ m α) (s : σ) : run' x s = (·.1) <$> run x s :=
   rfl
 
-@[simp, grind =] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
+@[simp] theorem run_pure [Monad m] (a : α) (s : σ) : (pure a : StateT σ m α).run s = pure (a, s) := rfl
 
-@[simp, grind =] theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
+@[simp] theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
     : (x >>= f).run s = x.run s >>= λ p => (f p.1).run p.2 := by
   simp [bind, StateT.bind, run]
 
-@[simp, grind =] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
+@[simp] theorem run_map {α β σ : Type u} [Monad m] [LawfulMonad m] (f : α → β) (x : StateT σ m α) (s : σ) : (f <$> x).run s = (fun (p : α × σ) => (f p.1, p.2)) <$> x.run s := by
   simp [Functor.map, StateT.map, run, ←bind_pure_comp]
 
-@[simp, grind =] theorem run_get [Monad m] (s : σ)    : (get : StateT σ m σ).run s = pure (s, s) := rfl
+@[simp] theorem run_get [Monad m] (s : σ)    : (get : StateT σ m σ).run s = pure (s, s) := rfl
 
-@[simp, grind =] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (⟨⟩, s') := rfl
+@[simp] theorem run_set [Monad m] (s s' : σ) : (set s' : StateT σ m PUnit).run s = pure (⟨⟩, s') := rfl
 
-@[simp, grind =] theorem run_modify [Monad m] (f : σ → σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (⟨⟩, f s) := rfl
+@[simp] theorem run_modify [Monad m] (f : σ → σ) (s : σ) : (modify f : StateT σ m PUnit).run s = pure (⟨⟩, f s) := rfl
 
-@[simp, grind =] theorem run_modifyGet [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
+@[simp] theorem run_modifyGet [Monad m] (f : σ → α × σ) (s : σ) : (modifyGet f : StateT σ m α).run s = pure ((f s).1, (f s).2) := by
   simp [modifyGet, MonadStateOf.modifyGet, StateT.modifyGet, run]
 
-@[simp, grind =] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
+@[simp] theorem run_lift {α σ : Type u} [Monad m] (x : m α) (s : σ) : (StateT.lift x : StateT σ m α).run s = x >>= fun a => pure (a, s) := rfl
 
-@[grind =]
 theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s := by
   simp [StateT.lift, StateT.run, bind, StateT.bind]
 
-@[simp, grind =] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
+@[simp] theorem run_monadLift {α σ : Type u} [Monad m] [MonadLiftT n m] (x : n α) (s : σ) : (monadLift x : StateT σ m α).run s = (monadLift x : m α) >>= fun a => pure (a, s) := rfl
 
-@[simp, grind =] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) :
+@[simp] theorem run_monadMap [MonadFunctorT n m] (f : {β : Type u} → n β → n β) (x : StateT σ m α) (s : σ) :
     (monadMap @f x : StateT σ m α).run s = monadMap @f (x.run s) := rfl
 
 @[simp] theorem run_seq {α β σ : Type u} [Monad m] [LawfulMonad m] (f : StateT σ m (α → β)) (x : StateT σ m α) (s : σ) : (f <*> x).run s = (f.run s >>= fun fs => (fun (p : α × σ) => (fs.1 p.1, p.2)) <$> x.run fs.2) := by

src/Init/Control/Lawful/MonadLift/Instances.lean

@@ -6,18 +6,12 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
-public import Init.Control.Option
-import all Init.Control.Option
-public import Init.Control.Except
-import all Init.Control.Except
-public import Init.Control.ExceptCps
-import all Init.Control.ExceptCps
-public import Init.Control.StateRef
-import all Init.Control.StateRef
-public import Init.Control.StateCps
-import all Init.Control.StateCps
-public import Init.Control.Id
-import all Init.Control.Id
+public import all Init.Control.Option
+public import all Init.Control.Except
+public import all Init.Control.ExceptCps
+public import all Init.Control.StateRef
+public import all Init.Control.StateCps
+public import all Init.Control.Id
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.Instances
 

src/Init/Conv.lean

@@ -290,17 +290,13 @@ macro "right" : conv => `(conv| rhs)
 /-- `intro` traverses into binders. Synonym for `ext`. -/
 macro "intro" xs:(ppSpace colGt binderIdent)* : conv => `(conv| ext $xs*)
 
-syntax enterPattern := "in " (occs)? term
-
-syntax enterArg := binderIdent <|> argArg <|> enterPattern
+syntax enterArg := binderIdent <|> argArg
 
 /-- `enter [arg, ...]` is a compact way to describe a path to a subterm.
 It is a shorthand for other conv tactics as follows:
 * `enter [i]` is equivalent to `arg i`.
 * `enter [@i]` is equivalent to `arg @i`.
 * `enter [x]` (where `x` is an identifier) is equivalent to `ext x`.
-* `enter [in e]` (where `e` is a term) is equivalent to `pattern e`.
-  Occurrences can be specified with `enter [in (occs := ...) e]`.
 For example, given the target `f (g a (fun x => x b))`, `enter [1, 2, x, 1]`
 will traverse to the subterm `b`. -/
 syntax (name := enter) "enter" " [" withoutPosition(enterArg,+) "]" : conv

src/Init/Data.lean

@@ -51,6 +51,5 @@ public import Init.Data.Range.Polymorphic
 public import Init.Data.Slice
 public import Init.Data.Order
 public import Init.Data.Rat
-public import Init.Data.Dyadic
 
 public section

src/Init/Data/Array/Attach.lean

@@ -9,8 +9,7 @@ prelude
 public import Init.Data.Array.Mem
 public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Count
-public import Init.Data.List.Attach
-import all Init.Data.List.Attach
+public import all Init.Data.List.Attach
 
 public section
 

src/Init/Data/Array/Basic.lean

@@ -10,11 +10,11 @@ public import Init.WFTactics
 public import Init.Data.Nat.Basic
 public import Init.Data.Fin.Basic
 public import Init.Data.UInt.BasicAux
+public import Init.Data.Repr
+public import Init.Data.ToString.Basic
 public import Init.GetElem
-public import Init.Data.List.ToArrayImpl
-import all Init.Data.List.ToArrayImpl
-public import Init.Data.Array.Set
-import all Init.Data.Array.Set
+public import all Init.Data.List.ToArrayImpl
+public import all Init.Data.Array.Set
 
 public section
 
@@ -162,7 +162,7 @@ This is a low-level version of `Array.size` that directly queries the runtime sy
 representation of arrays. While this is not provable, `Array.usize` always returns the exact size of
 the array since the implementation only supports arrays of size less than `USize.size`.
 -/
-@[extern "lean_array_size", simp, expose]
+@[extern "lean_array_size", simp]
 def usize (xs : @& Array α) : USize := xs.size.toUSize
 
 /--
@@ -441,7 +441,7 @@ def swapAt! (xs : Array α) (i : Nat) (v : α) : α × Array α :=
     swapAt xs i v
   else
     have : Inhabited (α × Array α) := ⟨(v, xs)⟩
-    panic! String.Internal.append (String.Internal.append "index " (toString i)) " out of bounds"
+    panic! ("index " ++ toString i ++ " out of bounds")
 
 /--
 Returns the first `n` elements of an array. The resulting array is produced by repeatedly calling
@@ -2167,7 +2167,7 @@ instance {α : Type u} [Repr α] : Repr (Array α) where
   reprPrec xs _ := Array.repr xs
 
 instance [ToString α] : ToString (Array α) where
-  toString xs := String.Internal.append "#" (toString xs.toList)
+  toString xs := "#" ++ toString xs.toList
 
 end Array
 

src/Init/Data/Array/BasicAux.lean

@@ -6,8 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Nat.Linear
 public import Init.NotationExtra
 

src/Init/Data/Array/Bootstrap.lean

@@ -8,8 +8,7 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 
 public section
 

src/Init/Data/Array/Count.lean

@@ -6,8 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Count
 

src/Init/Data/Array/DecidableEq.lean

@@ -6,8 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.BEq
 public import Init.Data.List.Nat.BEq
 public import Init.ByCases

src/Init/Data/Array/Erase.lean

@@ -6,8 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Basic

src/Init/Data/Array/Find.lean

@@ -7,8 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
 public import Init.Data.Array.Range
@@ -728,7 +727,7 @@ theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
   cases xs
   simp only [List.findFinIdx?_toArray, hf, List.findFinIdx?_subtype]
   rw [findFinIdx?_congr List.unattach_toArray]
-  simp only [Option.map_map, Function.comp_def, Fin.cast_cast]
+  simp only [Option.map_map, Function.comp_def, Fin.cast_trans]
   simp [Array.size]
 
 /-! ### idxOf

src/Init/Data/Array/Lemmas.lean

@@ -15,6 +15,7 @@ public import Init.Data.List.Monadic
 public import Init.Data.List.OfFn
 public import Init.Data.Array.Mem
 public import Init.Data.Array.DecidableEq
+public import Init.Data.Array.Lex.Basic
 public import Init.Data.Range.Lemmas
 public import Init.TacticsExtra
 public import Init.Data.List.ToArray

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

@@ -70,8 +70,8 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     rw [cons_lex_cons.forIn'_congr_aux Std.PRange.toList_eq_match rfl (fun _ _ _ => rfl)]
     simp only [Std.PRange.SupportsUpperBound.IsSatisfied, bind_pure_comp, map_pure]
     rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.PRange.toList_Rox_eq_toList_Rcx_of_isSome_succ? (lo := 0) (h := rfl),
-    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ,
+  simp only [Std.PRange.toList_open_eq_toList_closed_of_isSome_succ? (lo := 0) (h := rfl),
+    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.ClosedOpen.toList_succ_succ,
     Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
     Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
   cases lt a b

src/Init/Data/Array/MapIdx.lean

@@ -6,13 +6,11 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
 public import Init.Data.Array.OfFn
-public import Init.Data.List.MapIdx
-import all Init.Data.List.MapIdx
+public import all Init.Data.List.MapIdx
 
 public section
 

src/Init/Data/Array/Monadic.lean

@@ -6,10 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.List.Control
-import all Init.Data.List.Control
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.List.Control
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
 public import Init.Data.List.Monadic

src/Init/Data/Array/OfFn.lean

@@ -6,8 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Monadic
 public import Init.Data.List.OfFn

src/Init/Data/Array/Perm.lean

@@ -7,8 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Nat.Perm
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 
 public section

src/Init/Data/Array/Range.lean

@@ -7,10 +7,8 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
-public import Init.Data.Array.OfFn
-import all Init.Data.Array.OfFn
+public import all Init.Data.Array.Basic
+public import all Init.Data.Array.OfFn
 public import Init.Data.Array.MapIdx
 public import Init.Data.Array.Zip
 public import Init.Data.List.Nat.Range

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

@@ -8,8 +8,7 @@ module
 
 prelude
 public import Init.Data.Array.Basic
-public import Init.Data.Array.Subarray
-import all Init.Data.Array.Subarray
+public import all Init.Data.Array.Subarray
 public import Init.Omega
 
 public section

src/Init/Data/Array/TakeDrop.lean

@@ -6,8 +6,7 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.TakeDrop
 

src/Init/Data/Array/Zip.lean

@@ -6,8 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
+public import all Init.Data.Array.Basic
 public import Init.Data.Array.TakeDrop
 public import Init.Data.List.Zip
 
@@ -231,9 +230,11 @@ theorem zip_map {f : α → γ} {g : β → δ} {as : Array α} {bs : Array β}
   cases bs
   simp [List.zip_map]
 
+@[grind _=_]
 theorem zip_map_left {f : α → γ} {as : Array α} {bs : Array β} :
     zip (as.map f) bs = (zip as bs).map (Prod.map f id) := by rw [← zip_map, map_id]
 
+@[grind _=_]
 theorem zip_map_right {f : β → γ} {as : Array α} {bs : Array β} :
     zip as (bs.map f) = (zip as bs).map (Prod.map id f) := by rw [← zip_map, map_id]
 

src/Init/Data/BitVec/Basic.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Data.Fin.Basic
 public import Init.Data.Nat.Bitwise.Lemmas
 public import Init.Data.Nat.Power2
-public import Init.Data.Int.Bitwise.Basic
+public import Init.Data.Int.Bitwise
 public import Init.Data.BitVec.BasicAux
 
 @[expose] public section
@@ -206,13 +206,10 @@ Converts a bitvector into a fixed-width hexadecimal number with enough digits to
 
 If `n` is `0`, then one digit is returned. Otherwise, `⌊(n + 3) / 4⌋` digits are returned.
 -/
--- If we ever want to prove something about this, we can avoid having to use the opaque
--- `Internal` string functions by moving this definition out to a separate file that can live
--- downstream of `Init.Data.String.Basic`.
 protected def toHex {n : Nat} (x : BitVec n) : String :=
   let s := (Nat.toDigits 16 x.toNat).asString
-  let t := (List.replicate ((n+3) / 4 - String.Internal.length s) '0').asString
-  String.Internal.append t s
+  let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
+  t ++ s
 
 /-- `BitVec` representation. -/
 protected def BitVec.repr (a : BitVec n) : Std.Format :=

src/Init/Data/BitVec/BasicAux.lean

@@ -21,6 +21,13 @@ namespace BitVec
 
 section Nat
 
+/--
+The bitvector with value `i mod 2^n`.
+-/
+@[expose, match_pattern]
+protected def ofNat (n : Nat) (i : Nat) : BitVec n where
+  toFin := Fin.ofNat (2^n) i
+
 instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 
 /-- Return the bound in terms of toNat. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -6,14 +6,11 @@ Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 module
 
 prelude
-public import Init.Data.Nat.Bitwise.Basic
-import all Init.Data.Nat.Bitwise.Basic
+public import all Init.Data.Nat.Bitwise.Basic
 public import Init.Data.Nat.Mod
-public import Init.Data.Int.DivMod
-import all Init.Data.Int.DivMod
+public import all Init.Data.Int.DivMod
 public import Init.Data.Int.LemmasAux
-public import Init.Data.BitVec.Basic
-import all Init.Data.BitVec.Basic
+public import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
@@ -2155,238 +2152,4 @@ theorem shiftLeft_add_eq_shiftLeft_or {x y : BitVec w} :
     (y <<< x) + x =  (y <<< x) ||| x := by
   rw [BitVec.add_comm, add_shiftLeft_eq_or_shiftLeft, or_comm]
 
-/- ### Fast Circuit For Unsigned Overflow Detection -/
-
-/-!
-# Note [Fast Unsigned Multiplication Overflow Detection]
-
-The fast unsigned multiplication overflow detection circuit is described in
-`Efficient integer multiplication overflow detection circuits` (https://ieeexplore.ieee.org/abstract/document/987767).
-With this circuit, the computation of the overflow flag for the unsigned multiplication of
-two bitvectors `x` and `y` with bitwidth `w` requires:
-· extending the operands by `1` bit and performing the multiplication with the extended operands,
-· computing the preliminary overflow flag, which describes whether `x` and `y` together have at most
-  `w - 2` leading zeros.
-If the most significant bit of the extended operands' multiplication is `true` or if the
-preliminary overflow flag is `true`, overflow happens.
-In particular, the conditions check two different cases:
-· if the most significant bit of the extended operands' multiplication is `true`, the result of the
-  multiplication 2 ^ w ≤ x.toNat * y.toNat < 2 ^ (w + 1),
-· if the preliminary flag is true, then 2 ^ (w + 1) ≤ x.toNat * y.toNat.
-
-The computation of the preliminary overflow flag `resRec` relies on two quantities:
-· `uppcRec`: the unsigned parallel prefix circuit for the bits until a certain `i`,
-· `aandRec`: the conjunction between the parallel prefix circuit at of the first operand until a certain `i`
-  and the `i`-th bit in the second operand.
--/
-
-/--
-  `uppcRec` is the unsigned parallel prefix, `x.uppcRec s = true` iff `x.toNat` is greater or equal
-  than `2 ^ (w - 1 - (s - 1))`.
--/
-def uppcRec {w} (x : BitVec w) (s : Nat) (hs : s < w) : Bool :=
-  match s with
-  | 0 => x.msb
-  | i + 1 =>  x[w - 1 - i] || uppcRec x i (by omega)
-
-/-- The unsigned parallel prefix of `x` at `s` is `true` if and only if x interpreted
-  as a natural number is greater or equal than `2 ^ (w - 1 - (s - 1))`. -/
-@[simp]
-theorem uppcRec_true_iff (x : BitVec w) (s : Nat) (h : s < w) :
-    uppcRec x s h ↔ 2 ^ (w - 1 - (s - 1)) ≤ x.toNat := by
-  rcases w with _|w
-  · omega
-  · induction s
-    · case succ.zero =>
-      simp only [uppcRec, msb_eq_true_iff_two_mul_ge, Nat.pow_add, Nat.pow_one,
-        Nat.mul_comm (2 ^ w) 2, ge_iff_le, Nat.add_one_sub_one, zero_le, Nat.sub_eq_zero_of_le,
-        Nat.sub_zero]
-      apply Nat.mul_le_mul_left_iff (by omega)
-    · case succ.succ s ihs =>
-      simp only [uppcRec, or_eq_true, ihs, Nat.add_one_sub_one]
-      have := Nat.pow_le_pow_of_le (a := 2) ( n := (w - s)) (m := (w - (s - 1))) (by omega) (by omega)
-      constructor
-      · intro h'
-        rcases h' with h'|h'
-        · apply ge_two_pow_of_testBit h'
-        · omega
-      · intro h'
-        by_cases hbit: x[w - s]
-        · simp [hbit]
-        · have := BitVec.le_toNat_iff_getLsbD_eq_true (x := x) (i := w - s) (by omega)
-          simp only [h', true_iff] at this
-          obtain ⟨k, hk⟩ := this
-          by_cases hwk : w - s + k < w + 1
-          · by_cases hk' : 0 < k
-            · have hle := ge_two_pow_of_testBit hk
-              have hpowle := Nat.pow_le_pow_of_le (a := 2) ( n := (w - (s - 1))) (m := (w - s + k)) (by omega) (by omega)
-              omega
-            · rw [getLsbD_eq_getElem (by omega)] at hk
-              simp [hbit, show k = 0 by omega] at hk
-          · simp_all
-
-/--
-  Conjunction for fast umulOverflow circuit
--/
-def aandRec (x y : BitVec w) (s : Nat) (hs : s < w) : Bool :=
-  y[s] && uppcRec x s (by omega)
-
-
-/--
-  Preliminary overflow flag for fast umulOverflow circuit as introduced in
-  `Efficient integer multiplication overflow detection circuits` (https://ieeexplore.ieee.org/abstract/document/987767).
--/
-def resRec (x y : BitVec w) (s : Nat) (hs : s < w) (hslt : 0 < s) : Bool :=
-  match hs0 : s with
-  | 0 => by omega
-  | s' + 1 =>
-    match hs' : s' with
-    | 0 => aandRec x y 1 (by omega)
-    | s'' + 1 =>
-      (resRec x y s' (by omega) (by omega)) || (aandRec x y s (by omega))
-
-/-- The preliminary overflow flag is true for a certain `s` if and only if the conjunction returns true at
-  any `k` smaller than or equal to `s`. -/
-theorem resRec_true_iff (x y : BitVec w) (s : Nat) (hs : s < w) (hs' : 0 < s) :
-    resRec x y s hs hs' = true ↔ ∃ (k : Nat), ∃ (h : k ≤ s), ∃ (_ : 0 < k), aandRec x y k (by omega) := by
-  unfold resRec
-  rcases s with _|s
-  · omega
-  · rcases s
-    · case zero =>
-      constructor
-      · intro ha
-        exists 1, by omega, by omega
-      · intro hr
-        obtain ⟨k, hk, hk', hk''⟩ := hr
-        simp only [show k = 1 by omega] at hk''
-        exact hk''
-    · case succ s =>
-      induction s
-      · case zero =>
-        unfold resRec
-        simp only [Nat.zero_add, Nat.reduceAdd, or_eq_true]
-        constructor
-        · intro h
-          rcases h with h|h
-          · exists 1, by omega, by omega
-          · exists 2, by omega, by omega
-        · intro h
-          obtain ⟨k, hk, hk', hk''⟩ := h
-          have h : k = 1 ∨ k = 2 := by omega
-          rcases h with h|h
-          <;> simp only [h] at hk''
-          <;> simp [hk'']
-      · case succ s ihs =>
-        specialize ihs (by omega) (by omega)
-        unfold resRec
-        simp only [or_eq_true, ihs]
-        constructor
-        · intro h
-          rcases h with h|h
-          · obtain ⟨k, hk, hk', hk''⟩ := h
-            exists k, by omega, by omega
-          · exists s + 1 + 1 + 1, by omega, by omega
-        · intro h
-          obtain ⟨k, hk, hk', hk''⟩ := h
-          by_cases h' : x.aandRec y (s + 1 + 1 + 1) (by omega) = true
-          · simp [h']
-          · simp only [h', false_eq_true, _root_.or_false]
-            by_cases h'' : k ≤ s + 1 + 1
-            · exists k, h'', by omega
-            · have : k = s + 1 + 1 + 1 := by omega
-              simp_all
-
-/-- If the sum of the leading zeroes of two bitvecs with bitwidth `w` is less than or equal to
-  (`w - 2`), then the preliminary overflow flag is true and their unsigned multiplication overflows.
-  The explanation is in `Efficient integer multiplication overflow detection circuits`
-  https://ieeexplore.ieee.org/abstract/document/987767
-  -/
-theorem resRec_of_clz_le {x y : BitVec w} (hw : 1 < w) (hx : x ≠ 0#w) (hy : y ≠ 0#w):
-    (clz x).toNat + (clz y).toNat ≤ w - 2 → resRec x y (w - 1) (by omega) (by omega) := by
-  intro h
-  rw [resRec_true_iff]
-  exists (w - 1 - y.clz.toNat), by omega, by omega
-  simp only [aandRec]
-  by_cases hw0 : w - 1 - y.clz.toNat = 0
-  · have := clz_lt_iff_ne_zero.mpr (by omega)
-    omega
-  · simp only [and_eq_true, getLsbD_true_clz_of_ne_zero (x := y) (by omega) (by omega),
-    getElem_of_getLsbD_eq_true, uppcRec_true_iff,
-    show w - 1 - (w - 1 - y.clz.toNat - 1) = y.clz.toNat + 1 by omega, _root_.true_and]
-    exact Nat.le_trans (Nat.pow_le_pow_of_le (a := 2) (n := y.clz.toNat + 1)
-          (m := w - 1 - x.clz.toNat) (by omega) (by omega))
-          (BitVec.two_pow_sub_clz_le_toNat_of_ne_zero (x := x) (by omega) (by omega))
-
-/--
-  Complete fast overflow detection circuit for unsigned multiplication.
--/
-theorem fastUmulOverflow (x y : BitVec w) :
-    umulOverflow x y = if hw : w ≤ 1 then false
-      else (setWidth (w + 1) x * setWidth (w + 1) y)[w] || x.resRec y (w - 1) (by omega) (by omega) := by
-  rcases w with _|_|w
-  · simp [of_length_zero, umulOverflow]
-  · have hx : x.toNat ≤ 1 := by omega
-    have hy : y.toNat ≤ 1 := by omega
-    have := Nat.mul_le_mul (n₁ := x.toNat) (m₁ := y.toNat) (n₂ := 1) (m₂ := 1) hx hy
-    simp [umulOverflow]
-    omega
-  · by_cases h : umulOverflow x y
-    · simp only [h, Nat.reduceLeDiff, reduceDIte, Nat.add_one_sub_one, true_eq, or_eq_true]
-      simp only [umulOverflow, ge_iff_le, decide_eq_true_eq] at h
-      by_cases h' : x.toNat * y.toNat < 2 ^ (w + 1 + 1 + 1)
-      · have hlt := BitVec.getElem_eq_true_of_lt_of_le
-          (x := (setWidth (w + 1 + 1 + 1) x * setWidth (w + 1 + 1 + 1) y))
-          (k := w + 1 + 1)  (by omega)
-        simp only [toNat_mul, toNat_setWidth, Nat.lt_add_one, toNat_mod_cancel_of_lt,
-          Nat.mod_eq_of_lt (a := x.toNat * y.toNat) (b := 2 ^ (w + 1 + 1 + 1)) (by omega), h', h,
-          forall_const] at hlt
-        simp [hlt]
-      · by_cases hsw : (setWidth (w + 1 + 1 + 1) x * setWidth (w + 1 + 1 + 1) y)[w + 1 + 1] = true
-        · simp [hsw]
-        · simp only [hsw, false_eq_true, _root_.false_or]
-          have := Nat.two_pow_pos (w := w + 1 + 1)
-          have hltx := BitVec.toNat_lt_two_pow_sub_clz (x := x)
-          have hlty := BitVec.toNat_lt_two_pow_sub_clz (x := y)
-          have := Nat.mul_ne_zero_iff (m := y.toNat) (n := x.toNat)
-          simp only [ne_eq, show ¬x.toNat * y.toNat = 0 by omega, not_false_eq_true,
-            true_iff] at this
-          obtain ⟨hxz,hyz⟩ := this
-          apply resRec_of_clz_le (x := x) (y := y) (by omega) (by simp [toNat_eq]; exact hxz) (by simp [toNat_eq]; exact hyz)
-          by_cases hzxy : x.clz.toNat + y.clz.toNat ≤ w
-          · omega
-          · by_cases heq : w + 1 - y.clz.toNat = 0
-            · by_cases heq' : w + 1 + 1 - y.clz.toNat = 0
-              · simp [heq', hyz] at hlty
-              · simp only [show y.clz.toNat = w + 1 by omega, Nat.add_sub_cancel_left,
-                  Nat.pow_one] at hlty
-                simp only [show y.toNat = 1 by omega, Nat.mul_one, Nat.not_lt] at h'
-                omega
-            · by_cases w + 1 < y.clz.toNat
-              · omega
-              · simp only [Nat.not_lt] at h'
-                have := Nat.mul_lt_mul'' (a := x.toNat) (b := y.toNat) (c := 2 ^ (w + 1 + 1 - x.clz.toNat)) (d := 2 ^ (w + 1 + 1 - y.clz.toNat)) hltx hlty
-                simp only [← Nat.pow_add] at this
-                have := Nat.pow_le_pow_of_le (a := 2) (n := w + 1 + 1 - x.clz.toNat + (w + 1 + 1 - y.clz.toNat)) (m := w + 1 + 1 + 1)
-                 (by omega) (by omega)
-                omega
-    · simp only [h, Nat.reduceLeDiff, reduceDIte, Nat.add_one_sub_one, false_eq, or_eq_false_iff]
-      simp only [umulOverflow, ge_iff_le, decide_eq_true_eq, Nat.not_le] at h
-      and_intros
-      · simp only [← getLsbD_eq_getElem, getLsbD_eq_getMsbD, Nat.lt_add_one, decide_true,
-          Nat.add_one_sub_one, Nat.sub_self, ← msb_eq_getMsbD_zero, Bool.true_and,
-          msb_eq_false_iff_two_mul_lt, toNat_mul, toNat_setWidth, toNat_mod_cancel_of_lt]
-        rw [Nat.mod_eq_of_lt (by omega),Nat.pow_add (m := w + 1 + 1) (n := 1)]
-        simp [Nat.mul_comm 2 (x.toNat * y.toNat), h]
-      · apply Classical.byContradiction
-        intro hcontra
-        simp only [not_eq_false, resRec_true_iff, exists_prop, exists_and_left] at hcontra
-        obtain ⟨k,hk,hk',hk''⟩ := hcontra
-        simp only [aandRec, and_eq_true, uppcRec_true_iff, Nat.add_one_sub_one] at hk''
-        obtain ⟨hky, hkx⟩ := hk''
-        have hyle := two_pow_le_toNat_of_getElem_eq_true (x := y) (i := k) (by omega) hky
-        have := Nat.mul_le_mul (n₁ := 2 ^ (w + 1 - (k - 1))) (m₁ := 2 ^ k) (n₂ := x.toNat) (m₂ := y.toNat) hkx hyle
-        simp [← Nat.pow_add, show w + 1 - (k - 1) + k = w + 1 + 1 by omega] at this
-        omega
-
 end BitVec

src/Init/Data/BitVec/Bootstrap.lean

@@ -6,9 +6,7 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B
 module
 
 prelude
-public import Init.Data.BitVec.Basic
-import all Init.Data.BitVec.Basic
-import Init.Data.Int.Bitwise.Lemmas
+public import all Init.Data.BitVec.Basic
 
 public section
 

src/Init/Data/BitVec/Folds.lean

@@ -6,8 +6,7 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
-public import Init.Data.BitVec.Basic
-import all Init.Data.BitVec.Basic
+public import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Fin.Iterate

src/Init/Data/BitVec/Lemmas.lean

@@ -7,10 +7,8 @@ module
 
 prelude
 public import Init.Data.Bool
-public import Init.Data.BitVec.Basic
-import all Init.Data.BitVec.Basic
-public import Init.Data.BitVec.BasicAux
-import all Init.Data.BitVec.BasicAux
+public import all Init.Data.BitVec.Basic
+public import all Init.Data.BitVec.BasicAux
 public import Init.Data.Fin.Lemmas
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Nat.Div.Lemmas
@@ -122,7 +120,7 @@ theorem getElem_of_getLsbD_eq_true {x : BitVec w} {i : Nat} (h : x.getLsbD i = t
 This normalized a bitvec using `ofFin` to `ofNat`.
 -/
 theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
-  simp only [BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
+  simp only [BitVec.ofNat, Fin.ofNat, lt, Nat.mod_eq_of_lt]
 
 /-- Prove nonequality of bitvectors in terms of nat operations. -/
 theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by
@@ -299,7 +297,7 @@ theorem length_pos_of_ne {x y : BitVec w} (h : x ≠ y) : 0 < w :=
 
 theorem ofFin_ofNat (n : Nat) :
     ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
-  simp only [OfNat.ofNat, Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, BitVec.ofNat]
+  simp only [OfNat.ofNat, Fin.ofNat, BitVec.ofNat]
 
 -- We use a `grind_pattern` as `@[grind]` will not use the `no_index` term.
 grind_pattern ofFin_ofNat => ofFin (OfNat.ofNat n : Fin (2^w))
@@ -510,18 +508,6 @@ theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
 @[simp] theorem zero_eq_one_iff (w : Nat) : (0#w = 1#w) ↔ (w = 0) := by
   rw [← one_eq_zero_iff, eq_comm]
 
-/-- A bitvector is equal to 0#w if and only if all bits are `false` -/
-theorem zero_iff_eq_false {x: BitVec w} :
-    x = 0#w ↔ ∀ i, x.getLsbD i = false := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · constructor
-    · intro hzero
-      simp [hzero]
-    · intro hfalse
-      ext j hj
-      simp [← getLsbD_eq_getElem, hfalse]
-
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@@ -2206,7 +2192,8 @@ theorem sshiftRight_eq_of_msb_false {x : BitVec w} {s : Nat} (h : x.msb = false)
   apply BitVec.eq_of_toNat_eq
   rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond]
   have hxbound : 2 * x.toNat < 2 ^ w := BitVec.msb_eq_false_iff_two_mul_lt.mp h
-  simp only [hxbound, ↓reduceIte, toNat_ushiftRight]
+  simp only [hxbound, ↓reduceIte, Int.natCast_shiftRight, ofInt_natCast,
+    toNat_ofNat, toNat_ushiftRight]
   replace hxbound : x.toNat >>> s < 2 ^ w := by
     rw [Nat.shiftRight_eq_div_pow]
     exact Nat.lt_of_le_of_lt (Nat.div_le_self ..) x.isLt
@@ -5779,6 +5766,40 @@ theorem msb_replicate {n w : Nat} {x : BitVec w} :
   simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]
   cases n <;> cases w <;> simp
 
+/-! ### Count leading zeros -/
+
+theorem clzAuxRec_zero (x : BitVec w) :
+    x.clzAuxRec 0 = if x.getLsbD 0 then BitVec.ofNat w (w - 1) else BitVec.ofNat w w := by rfl
+
+theorem clzAuxRec_succ (x : BitVec w) :
+    x.clzAuxRec (n + 1) = if x.getLsbD (n + 1) then BitVec.ofNat w (w - 1 - (n + 1)) else BitVec.clzAuxRec x n := by rfl
+
+theorem clzAuxRec_eq_clzAuxRec_of_le (x : BitVec w) (h : w - 1 ≤ n) :
+    x.clzAuxRec n = x.clzAuxRec (w - 1) := by
+  let k := n - (w - 1)
+  rw [show n = (w - 1) + k by omega]
+  induction k
+  case zero => simp
+  case succ k ihk =>
+    simp [show w - 1 + (k + 1) = (w - 1 + k) + 1 by omega, clzAuxRec_succ, ihk,
+      show x.getLsbD (w - 1 + k + 1) = false by simp only [show w ≤ w - 1 + k + 1 by omega, getLsbD_of_ge]]
+
+theorem clzAuxRec_eq_clzAuxRec_of_getLsbD_false {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) :
+    x.clzAuxRec n = x.clzAuxRec (n + k) := by
+  induction k
+  case zero => simp
+  case succ k ihk =>
+    simp only [show n + (k + 1) = (n + k) + 1 by omega, clzAuxRec_succ]
+    by_cases hxn : x.getLsbD (n + k + 1)
+    · have : ¬ ∀ (i : Nat), n < i → x.getLsbD i = false := by
+        simp only [Classical.not_forall, Bool.not_eq_false]
+        exists n + k + 1
+        simp [show n < n + k + 1 by omega, hxn]
+      contradiction
+    · simp only [hxn, Bool.false_eq_true, ↓reduceIte]
+      exact ihk
+
+
 /-! ### Inequalities (le / lt) -/
 
 theorem ule_eq_not_ult (x y : BitVec w) : x.ule y = !y.ult x := by
@@ -5827,362 +5848,6 @@ theorem sle_eq_ule {x y : BitVec w} : x.sle y = (x.msb != y.msb ^^ x.ule y) := b
 theorem sle_eq_ule_of_msb_eq {x y : BitVec w} (h : x.msb = y.msb) : x.sle y = x.ule y := by
   simp [BitVec.sle_eq_ule, h]
 
-/-- A bitvector interpreted as a natural number is greater than or equal to `2 ^ i` if and only if
-  there exists at least one bit with `true` value at position `i` or higher. -/
-theorem le_toNat_iff_getLsbD_eq_true {x : BitVec w} (hi : i < w ) :
-    (2 ^ i ≤ x.toNat) ↔ (∃ k, x.getLsbD (i + k) = true) := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · constructor
-    · intro hle
-      apply Classical.byContradiction
-      intros hcontra
-      let x' := setWidth (i + 1) x
-      have hx' : setWidth (i + 1) x = x' := by rfl
-      have hcast : w - i + (i + 1) = w + 1 := by omega
-      simp only [not_exists, Bool.not_eq_true] at hcontra
-      have hx'' : x = BitVec.cast hcast (0#(w - i) ++ x') := by
-        ext j
-        by_cases hj : j < i + 1
-        · simp only [← hx', getElem_cast, getElem_append, hj, reduceDIte, getElem_setWidth]
-          rw [getLsbD_eq_getElem]
-        · simp only [getElem_cast, getElem_append, hj, reduceDIte, getElem_zero]
-          let j' := j - i
-          simp only [show j = i + j' by omega]
-          apply hcontra
-      have : x'.toNat < 2 ^ i := by
-        apply Nat.lt_pow_two_of_testBit (n := i) x'.toNat
-        intro j hj
-        let j' := j - i
-        specialize hcontra j'
-        have : x'.getLsbD (i + j') = x.getLsbD (i + j') := by
-          subst x'
-          simp [hcontra]
-        simp [show j = i + j' by omega, testBit_toNat, this, hcontra]
-      have : x'.toNat = x.toNat := by
-        have := BitVec.setWidth_eq_append (w := (w + 1)) (v := i + 1) (x := x')
-        specialize this (by omega)
-        rw [toNat_eq, toNat_setWidth, Nat.mod_eq_of_lt (by omega)] at this
-        simp [hx'']
-      omega
-    · intro h
-      obtain ⟨k, hk⟩ := h
-      by_cases hk' : i + k < w + 1
-      · have := Nat.ge_two_pow_of_testBit hk
-        have := Nat.pow_le_pow_of_le (a := 2) (n := i) (m := i + k) (by omega) (by omega)
-        omega
-      · simp [show w + 1 ≤ i + k by omega] at hk
-
-/-- A bitvector interpreted as a natural number is strictly smaller than `2 ^ i` if and only if
-  all bits at position `i` or higher are false. -/
-theorem toNat_lt_iff_getLsbD_eq_false {x : BitVec w} (i : Nat) (hi : i < w) :
-    x.toNat < 2 ^ i ↔ (∀ k, x.getLsbD (i + k) = false) := by
-  constructor
-  · intro h
-    apply Classical.byContradiction
-    intro hcontra
-    simp only [Classical.not_forall, Bool.not_eq_false] at hcontra
-    obtain ⟨k, hk⟩ := hcontra
-    have hle := Nat.ge_two_pow_of_testBit hk
-    by_cases hlt : i + k < w
-    · have := Nat.pow_le_pow_of_le (a := 2) (n := i) (m := i + k) (by omega) (by omega)
-      omega
-    · simp [show w ≤ i + k by omega] at hk
-  · intro h
-    apply Classical.byContradiction
-    intro hcontra
-    simp [BitVec.le_toNat_iff_getLsbD_eq_true (x := x) (i := i) hi, h] at hcontra
-
-/-- If a bitvector interpreted as a natural number is strictly smaller than `2 ^ (k + 1)` and greater than or
-  equal to 2 ^ k, then the bit at position `k` must be `true` -/
-theorem getElem_eq_true_of_lt_of_le {x : BitVec w} (hk' : k < w) (hlt: x.toNat < 2 ^ (k + 1)) (hle : 2 ^ k ≤ x.toNat) :
-    x[k] = true := by
-  have := le_toNat_iff_getLsbD_eq_true (x := x) (i := k) hk'
-  simp only [hle, true_iff] at this
-  obtain ⟨k',hk'⟩ := this
-  by_cases hkk' : k + k' < w
-  · have := Nat.ge_two_pow_of_testBit hk'
-    by_cases hzk' : k' = 0
-    · simp [hzk'] at hk'; exact hk'
-    · have := Nat.pow_lt_pow_of_lt (a := 2) (n := k) (m := k + k') (by omega) (by omega)
-      have := Nat.pow_le_pow_of_le (a := 2) (n := k + 1) (m := k + k') (by omega) (by omega)
-      omega
-  · simp [show w ≤ k + k' by omega] at hk'
-
-/-! ### Count leading zeros -/
-
-theorem clzAuxRec_zero (x : BitVec w) :
-    x.clzAuxRec 0 = if x.getLsbD 0 then BitVec.ofNat w (w - 1) else BitVec.ofNat w w := by rfl
-
-theorem clzAuxRec_succ (x : BitVec w) :
-    x.clzAuxRec (n + 1) = if x.getLsbD (n + 1) then BitVec.ofNat w (w - 1 - (n + 1)) else BitVec.clzAuxRec x n := by rfl
-
-theorem clzAuxRec_eq_clzAuxRec_of_le {x : BitVec w} (h : w - 1 ≤ n) :
-    x.clzAuxRec n = x.clzAuxRec (w - 1) := by
-  let k := n - (w - 1)
-  rw [show n = (w - 1) + k by omega]
-  induction k
-  · case zero => simp
-  · case succ k ihk =>
-    simp [show w - 1 + (k + 1) = (w - 1 + k) + 1 by omega, clzAuxRec_succ, ihk,
-      show x.getLsbD (w - 1 + k + 1) = false by simp only [show w ≤ w - 1 + k + 1 by omega, getLsbD_of_ge]]
-
-theorem clzAuxRec_eq_clzAuxRec_of_getLsbD_false {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) :
-    x.clzAuxRec n = x.clzAuxRec (n + k) := by
-  induction k
-  · case zero => simp
-  · case succ k ihk =>
-    simp only [show n + (k + 1) = (n + k) + 1 by omega, clzAuxRec_succ]
-    by_cases hxn : x.getLsbD (n + k + 1)
-    · have : ¬ ∀ (i : Nat), n < i → x.getLsbD i = false := by
-        simp only [Classical.not_forall, Bool.not_eq_false]
-        exists n + k + 1
-        simp [show n < n + k + 1 by omega, hxn]
-      contradiction
-    · simp only [hxn, Bool.false_eq_true, ↓reduceIte]
-      exact ihk
-
-theorem clzAuxRec_le {x : BitVec w} (n : Nat) :
-    clzAuxRec x n ≤ w := by
-  have := Nat.lt_pow_self (a := 2) (n := w) (by omega)
-  rcases w with _|w
-  · simp [of_length_zero]
-  · induction n
-    · case zero =>
-      simp only  [clzAuxRec_zero]
-      by_cases hx0 : x.getLsbD 0
-      · simp only [hx0, Nat.add_one_sub_one, reduceIte, natCast_eq_ofNat, ofNat_le_ofNat,
-          Nat.mod_two_pow_self, ge_iff_le, Nat.mod_eq_of_lt (a := w) (b := 2 ^ (w + 1)) (by omega)]
-        omega
-      · simp only [hx0, Bool.false_eq_true, reduceIte, natCast_eq_ofNat, BitVec.le_refl]
-    · case succ n ihn =>
-      simp only [clzAuxRec_succ, Nat.add_one_sub_one, natCast_eq_ofNat, ge_iff_le]
-      by_cases hxn : x.getLsbD (n + 1)
-      · simp [hxn, Nat.mod_eq_of_lt (a := w - (n + 1)) (b := 2 ^(w + 1)) (by omega)]
-        omega
-      · simp only [hxn, Bool.false_eq_true, reduceIte]
-        exact ihn
-
-theorem clzAuxRec_eq_iff_of_getLsbD_false {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) :
-    x.clzAuxRec n = BitVec.ofNat w w ↔ ∀ j, j ≤ n → x.getLsbD j = false := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · have := Nat.lt_pow_self (a := 2) (n := w + 1)
-    induction n
-    · case zero =>
-      simp only [clzAuxRec_zero, Nat.zero_lt_succ, getLsbD_eq_getElem, Nat.add_one_sub_one,
-        ite_eq_right_iff, Nat.le_zero_eq, forall_eq]
-      by_cases hx0 : x.getLsbD 0
-      · simp [hx0, toNat_eq, toNat_ofNat, Nat.mod_eq_of_lt (a := w) (b := 2 ^ (w + 1)) (by omega)]
-      · simp only [Nat.zero_lt_succ, getLsbD_eq_getElem, Bool.not_eq_true] at hx0
-        simp [hx0]
-    · case succ n ihn =>
-      simp only [clzAuxRec_succ, Nat.add_one_sub_one]
-      by_cases hxn : x.getLsbD (n + 1)
-      · simp only [hxn, reduceIte, toNat_eq, toNat_ofNat,
-          Nat.mod_eq_of_lt (a := w - (n + 1)) (b := 2 ^ (w + 1)) (by omega), Nat.mod_two_pow_self,
-          show ¬w - (n + 1) = w + 1 by omega, false_iff, Classical.not_forall,
-          Bool.not_eq_false]
-        exists n + 1, by omega
-      · have : ∀ (i : Nat), n < i → x.getLsbD i = false := by
-          intro i hi
-          by_cases hi' : i = n + 1
-          · simp [hi', hxn]
-          · apply h; omega
-        specialize ihn this
-        simp only [Bool.not_eq_true] at ihn hxn
-        simp only [hxn, Bool.false_eq_true, reduceIte, ihn]
-        constructor
-        <;> intro h' j hj
-        <;> (by_cases hj' : j = n + 1; simp [hj', hxn]; (apply h'; omega))
-
-theorem clz_le {x : BitVec w} :
-    clz x ≤ w := by
-  unfold clz
-  rcases w with _|w
-  · simp [of_length_zero]
-  · exact clzAuxRec_le (n := w)
-
-@[simp]
-theorem clz_eq_iff_eq_zero {x : BitVec w} :
-    clz x = w ↔ x = 0#w := by
-  rcases w with _|w
-  · simp [clz, of_length_zero]
-  · simp only [clz, Nat.add_one_sub_one, natCast_eq_ofNat, zero_iff_eq_false]
-    rw [clzAuxRec_eq_iff_of_getLsbD_false (x := x) (n := w) (w := w + 1) (by intros i hi; simp [show w + 1 ≤ i by omega])]
-    constructor
-    · intro h i
-      by_cases i ≤ w
-      · apply h; omega
-      · simp [show w + 1 ≤ i by omega]
-    · intro h j hj
-      apply h
-
-theorem clzAuxRec_eq_zero_iff {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) (hw : 0 < w) :
-    (x.clzAuxRec n).toNat = 0 ↔ x[w - 1] = true := by
-  have := Nat.lt_pow_self (a := 2) (n := w)
-  induction n
-  · case zero =>
-    simp only [clzAuxRec_zero]
-    by_cases hw1 : w - 1 = 0
-    · by_cases hx0 : x.getLsbD 0
-      · simp [hw1, hx0]
-      · simp [hw1, show ¬ w = 0 by omega, hx0, ← getLsbD_eq_getElem]
-    · by_cases hx0 : x.getLsbD 0
-      · simp only [hx0, ↓reduceIte, toNat_ofNat,
-          Nat.mod_eq_of_lt (a := w - 1) (b := 2 ^ w) (by omega), show ¬w - 1 = 0 by omega, false_iff,
-          Bool.not_eq_true]
-        specialize h (w - 1) (by omega)
-        exact h
-      · simp [hx0, show ¬ w = 0 by omega]
-        specialize h (w - 1) (by omega)
-        exact h
-  · case succ n ihn =>
-    by_cases hxn : x.getLsbD (n + 1)
-    · simp only [clzAuxRec_succ, hxn, reduceIte, toNat_ofNat]
-      rw [Nat.mod_eq_of_lt (by omega)]
-      by_cases hwn : w - 1 - (n + 1) = 0
-      · have := lt_of_getLsbD hxn
-        simp only [show w - 1 = n + 1 by omega, Nat.sub_self, true_iff]
-        exact hxn
-      · simp only [hwn, false_iff, Bool.not_eq_true]
-        specialize h (w - 1) (by omega)
-        exact h
-    · simp only [clzAuxRec_succ, hxn, Bool.false_eq_true, reduceIte]
-      apply ihn
-      intro i hi
-      by_cases hi : i = n + 1
-      · simp [hi, hxn]
-      · apply h; omega
-
-theorem clz_eq_zero_iff {x : BitVec w} (hw : 0 < w) :
-    (clz x).toNat = 0 ↔ 2 ^ (w - 1) ≤ x.toNat := by
-  simp only [clz, clzAuxRec_eq_zero_iff (x := x) (n := w - 1) (by intro i hi; simp [show w ≤ i by omega]) hw]
-  by_cases hxw : x[w - 1]
-  · simp [hxw, two_pow_le_toNat_of_getElem_eq_true (x := x) (i := w - 1) (by omega) hxw]
-  · simp only [hxw, Bool.false_eq_true, false_iff, Nat.not_le]
-    simp only [← getLsbD_eq_getElem, ← msb_eq_getLsbD_last, Bool.not_eq_true] at hxw
-    exact toNat_lt_of_msb_false hxw
-
-/-- The number of leading zeroes is strictly less than the bitwidth iff the bitvector is nonzero. -/
-theorem clz_lt_iff_ne_zero {x : BitVec w} :
-    clz x < w ↔ x ≠ 0#w := by
-  have hle := clz_le (x := x)
-  have heq := clz_eq_iff_eq_zero (x := x)
-  constructor
-  · intro h
-    simp only [natCast_eq_ofNat, BitVec.ne_of_lt (x := x.clz) (y := BitVec.ofNat w w) h,
-      false_iff] at heq
-    simp only [ne_eq, heq, not_false_eq_true]
-  · intro h
-    simp only [natCast_eq_ofNat, h, iff_false] at heq
-    apply BitVec.lt_of_le_ne (x := x.clz) (y := BitVec.ofNat w w) hle heq
-
-theorem getLsbD_false_of_clzAuxRec {x : BitVec w} (h : ∀ i, n < i → x.getLsbD i = false) :
-    ∀ j, x.getLsbD (w - (x.clzAuxRec n).toNat + j) = false := by
-  rcases w with _|w
-  · simp
-  · have := Nat.lt_pow_self (a := 2) (n := w + 1)
-    induction n
-    · case zero =>
-      intro j
-      simp only [clzAuxRec_zero, Nat.zero_lt_succ, getLsbD_eq_getElem, Nat.add_one_sub_one]
-      by_cases hx0 : x[0]
-      · specialize h (1 + j) (by omega)
-        simp [h, hx0, Nat.mod_eq_of_lt (a := w) (b := 2 ^ (w + 1)) (by omega)]
-      · simp only [hx0, Bool.false_eq_true, ↓reduceIte, toNat_ofNat, Nat.mod_two_pow_self,
-          Nat.sub_self, Nat.zero_add]
-        by_cases hj0 : j = 0
-        · simp [hj0, hx0]
-        · specialize h j (by omega)
-          exact h
-    · case succ n ihn =>
-      intro j
-      by_cases hxn : x.getLsbD (n + 1)
-      · have := lt_of_getLsbD hxn
-        specialize h (n + j + 1 + 1) (by omega)
-        simp [h, clzAuxRec_succ, hxn, Nat.mod_eq_of_lt (a := w - (n + 1)) (b := 2 ^ (w + 1)) (by omega),
-          show (w + 1 - (w - (n + 1)) + j) = n + j + 1 + 1 by omega]
-      · simp only [clzAuxRec_succ, hxn, Bool.false_eq_true, reduceIte]
-        apply ihn
-        intro i hi
-        by_cases hin : i = n + 1
-        · simp [hin, hxn]
-        · specialize h i (by omega)
-          exact h
-
-theorem getLsbD_true_of_eq_clzAuxRec_of_ne_zero {x : BitVec w} (hx : ¬ x = 0#w) (hn : ∀ i, n < i → x.getLsbD i = false) :
-    x.getLsbD (w - 1 - (x.clzAuxRec n).toNat) = true := by
-  rcases w with _|w
-  · simp [of_length_zero] at hx
-  · have := Nat.lt_pow_self (a := 2) (n := w + 1)
-    induction n
-    · case zero =>
-      by_cases hx0 : x[0]
-      · simp only [Nat.add_one_sub_one, clzAuxRec_zero, Nat.zero_lt_succ, getLsbD_eq_getElem, hx0,
-          reduceIte, toNat_ofNat, Nat.mod_eq_of_lt (a := w) (b := 2 ^(w + 1)) (by omega), show w - w = 0 by omega]
-      · simp only [zero_iff_eq_false, Classical.not_forall, Bool.not_eq_false] at hx
-        obtain ⟨m,hm⟩ := hx
-        specialize hn m
-        by_cases hm0 : m = 0
-        · simp [hm0, hx0] at hm
-        · simp [show 0 < m by omega, hm] at hn
-    · case succ n ihn =>
-      by_cases hxn : x.getLsbD (n + 1)
-      · have := lt_of_getLsbD hxn
-        simp [clzAuxRec_succ, hxn, toNat_ofNat, Nat.mod_eq_of_lt (a := w - (n + 1)) (b := 2 ^ (w + 1)) (by omega),
-          show w - (w - (n + 1)) = n + 1 by omega]
-      · simp only [Nat.add_one_sub_one, clzAuxRec_succ, hxn, Bool.false_eq_true, reduceIte]
-        simp only [Nat.add_one_sub_one] at ihn
-        apply ihn
-        intro j hj
-        by_cases hjn : j = n + 1
-        · simp [hjn, hxn]
-        · specialize hn j (by omega)
-          exact hn
-
-theorem getLsbD_true_clz_of_ne_zero {x : BitVec w} (hw : 0 < w) (hx : x ≠ 0#w) :
-    x.getLsbD (w - 1 - (clz x).toNat) = true := by
-  unfold clz
-  apply getLsbD_true_of_eq_clzAuxRec_of_ne_zero (x := x) (n := w - 1) (by omega)
-  intro i hi
-  simp [show w ≤ i by omega]
-
-/-- A nonzero bitvector is lower-bounded by its leading zeroes. -/
-theorem two_pow_sub_clz_le_toNat_of_ne_zero {x : BitVec w} (hw : 0 < w) (hx : x ≠ 0#w) :
-    2 ^ (w - 1 - (clz x).toNat) ≤ x.toNat := by
-  by_cases hc0 : x.clz.toNat  = 0
-  · simp [hc0, ← clz_eq_zero_iff (x := x) hw]
-  · have hclz := getLsbD_true_clz_of_ne_zero (x := x) hw hx
-    rw [getLsbD_eq_getElem (by omega)] at hclz
-    have hge := Nat.ge_two_pow_of_testBit hclz
-    push_cast at hge
-    exact hge
-
-/-- A bitvector is upper bounded by the number of leading zeroes. -/
-theorem toNat_lt_two_pow_sub_clz {x : BitVec w} :
-    x.toNat < 2 ^ (w - (clz x).toNat) := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · unfold clz
-    have hlt := toNat_lt_iff_getLsbD_eq_false (x := x)
-    have hzero := clzAuxRec_eq_zero_iff (x := x) (n := w) (by intro i hi; simp [show w + 1 ≤ i by omega]) (by omega)
-    simp only [Nat.add_one_sub_one] at hzero
-    by_cases hxw : x[w]
-    · simp only [hxw, iff_true] at hzero
-      simp only [Nat.add_one_sub_one, hzero, Nat.sub_zero, gt_iff_lt]
-      omega
-    · simp only [hxw, Bool.false_eq_true, iff_false] at hzero
-      rw [hlt]
-      · intro k
-        apply getLsbD_false_of_clzAuxRec (x := x) (n := w)
-        intro i hi
-        by_cases hiw : i = w
-        · simp [hiw, hxw]
-        · simp [show w + 1 ≤ i by omega]
-      · simp; omega
-
-
 /-! ### Deprecations -/
 
 set_option linter.missingDocs false

src/Init/Data/Bool.lean

@@ -10,6 +10,7 @@ public import Init.NotationExtra
 
 public section
 
+
 namespace Bool
 
 /--

src/Init/Data/ByteArray.lean

@@ -7,6 +7,5 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
-public import Init.Data.ByteArray.Extra
 
 public section

src/Init/Data/ByteArray/Basic.lean

@@ -6,10 +6,10 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 public import Init.Data.Array.DecidableEq
 public import Init.Data.UInt.Basic
-public import Init.Data.UInt.BasicAux
-import all Init.Data.UInt.BasicAux
+public import all Init.Data.UInt.BasicAux
 public import Init.Data.Option.Basic
 
 @[expose] public section
@@ -360,3 +360,27 @@ def List.toByteArray (bs : List UInt8) : ByteArray :=
   loop bs ByteArray.empty
 
 instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
+
+/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
+def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 7).toUInt64 <<< 0x38 |||
+  (bs.get! 6).toUInt64 <<< 0x30 |||
+  (bs.get! 5).toUInt64 <<< 0x28 |||
+  (bs.get! 4).toUInt64 <<< 0x20 |||
+  (bs.get! 3).toUInt64 <<< 0x18 |||
+  (bs.get! 2).toUInt64 <<< 0x10 |||
+  (bs.get! 1).toUInt64 <<< 0x8  |||
+  (bs.get! 0).toUInt64
+
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
+  assert! bs.size == 8
+  (bs.get! 0).toUInt64 <<< 0x38 |||
+  (bs.get! 1).toUInt64 <<< 0x30 |||
+  (bs.get! 2).toUInt64 <<< 0x28 |||
+  (bs.get! 3).toUInt64 <<< 0x20 |||
+  (bs.get! 4).toUInt64 <<< 0x18 |||
+  (bs.get! 5).toUInt64 <<< 0x10 |||
+  (bs.get! 6).toUInt64 <<< 0x8  |||
+  (bs.get! 7).toUInt64

src/Init/Data/ByteArray/Extra.lean

@@ -1,34 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-module
-
-prelude
-public import Init.Data.ByteArray.Basic
-import Init.Data.String.Basic
-
-/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
-public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
-  assert! bs.size == 8
-  (bs.get! 7).toUInt64 <<< 0x38 |||
-  (bs.get! 6).toUInt64 <<< 0x30 |||
-  (bs.get! 5).toUInt64 <<< 0x28 |||
-  (bs.get! 4).toUInt64 <<< 0x20 |||
-  (bs.get! 3).toUInt64 <<< 0x18 |||
-  (bs.get! 2).toUInt64 <<< 0x10 |||
-  (bs.get! 1).toUInt64 <<< 0x8  |||
-  (bs.get! 0).toUInt64
-
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
-public def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
-  assert! bs.size == 8
-  (bs.get! 0).toUInt64 <<< 0x38 |||
-  (bs.get! 1).toUInt64 <<< 0x30 |||
-  (bs.get! 2).toUInt64 <<< 0x28 |||
-  (bs.get! 3).toUInt64 <<< 0x20 |||
-  (bs.get! 4).toUInt64 <<< 0x18 |||
-  (bs.get! 5).toUInt64 <<< 0x10 |||
-  (bs.get! 6).toUInt64 <<< 0x8  |||
-  (bs.get! 7).toUInt64

src/Init/Data/Char/Lemmas.lean

@@ -6,8 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Char.Basic
-import all Init.Data.Char.Basic
+public import all Init.Data.Char.Basic
 public import Init.Data.UInt.Lemmas
 
 public section
@@ -66,6 +65,11 @@ instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
 def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
   total := fun x y => by simpa using Char.le_total y x
 
+theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4 := by
+  have := c.utf8Size_pos
+  have := c.utf8Size_le_four
+  omega
+
 @[simp] theorem ofNat_toNat (c : Char) : Char.ofNat c.toNat = c := by
   rw [Char.ofNat, dif_pos]
   rfl

src/Init/Data/Dyadic.lean

@@ -1,12 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-prelude
-
-public import Init.Data.Dyadic.Basic
-public import Init.Data.Dyadic.Instances
-public import Init.Data.Dyadic.Round
-public import Init.Data.Dyadic.Inv

src/Init/Data/Dyadic/Basic.lean

@@ -1,747 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Robin Arnez
--/
-module
-
-prelude
-public import Init.Data.Rat.Lemmas
-import Init.Data.Int.Bitwise.Lemmas
-import Init.Data.Int.DivMod.Lemmas
-
-/-!
-# The dyadic rationals
-
-Constructs the dyadic rationals as an ordered ring, equipped with a compatible embedding into the rationals.
--/
-
-set_option linter.missingDocs true
-
-@[expose] public section
-
-open Nat
-
-namespace Int
-
-/-- The number of trailing zeros in the binary representation of `i`. -/
-def trailingZeros (i : Int) : Nat :=
-  if h : i = 0 then 0 else aux i.natAbs i h (Nat.le_refl _) 0
-where
-  aux (k : Nat) (i : Int) (hi : i ≠ 0) (hk : i.natAbs ≤ k) (acc : Nat) : Nat :=
-    match k, (by omega : k ≠ 0) with
-    | k + 1, _ =>
-      if h : i % 2 = 0 then aux k (i / 2) (by omega) (by omega) (acc + 1)
-      else acc
-
--- TODO: check performance of `trailingZeros` in the kernel and VM.
-
-private theorem trailingZeros_aux_irrel (hi : i ≠ 0) (hk : i.natAbs ≤ k) (hk' : i.natAbs ≤ k') :
-    trailingZeros.aux k i hi hk acc = trailingZeros.aux k' i hi hk' acc := by
-  fun_induction trailingZeros.aux k i hi hk acc generalizing k' <;>
-    fun_cases trailingZeros.aux k' _ _ hk' _
-  · rename_i ih _ _ _ _ _
-    exact ih _
-  · contradiction
-  · contradiction
-  · rfl
-
-private theorem trailingZeros_aux_succ :
-    trailingZeros.aux k i hi hk (acc + 1) = trailingZeros.aux k i hi hk acc + 1 := by
-  fun_induction trailingZeros.aux k i hi hk acc <;> simp_all [trailingZeros.aux]
-
-theorem trailingZeros_zero : trailingZeros 0 = 0 := rfl
-
-theorem trailingZeros_two_mul_add_one (i : Int) :
-    Int.trailingZeros (2 * i + 1) = 0 := by
-  unfold trailingZeros trailingZeros.aux
-  rw [dif_neg (by omega)]
-  split <;> simp_all
-
-theorem trailingZeros_eq_zero_of_mod_eq {i : Int} (h : i % 2 = 1) :
-    Int.trailingZeros i = 0 := by
-  unfold trailingZeros trailingZeros.aux
-  rw [dif_neg (by omega)]
-  split <;> simp_all
-
-theorem trailingZeros_two_mul {i : Int} (h : i ≠ 0) :
-    Int.trailingZeros (2 * i) = Int.trailingZeros i + 1 := by
-  rw [Int.trailingZeros, dif_neg (Int.mul_ne_zero (by decide) h), Int.trailingZeros.aux.eq_def]
-  simp only [ne_eq, mul_emod_right, ↓reduceDIte, Int.reduceEq, not_false_eq_true,
-    mul_ediv_cancel_left, Nat.zero_add]
-  split
-  rw [trailingZeros, trailingZeros_aux_succ, dif_neg h]
-  apply congrArg Nat.succ (trailingZeros_aux_irrel ..) <;> omega
-
-theorem shiftRight_trailingZeros_mod_two {i : Int} (h : i ≠ 0) :
-    (i >>> i.trailingZeros) % 2 = 1 := by
-  rw (occs := .pos [2]) [← Int.emod_add_mul_ediv i 2]
-  rcases i.emod_two_eq with h' | h' <;> rw [h']
-  · rcases Int.dvd_of_emod_eq_zero h' with ⟨a, rfl⟩
-    simp only [ne_eq, Int.mul_eq_zero, Int.reduceEq, false_or] at h
-    rw [Int.zero_add, mul_ediv_cancel_left _ (by decide), trailingZeros_two_mul h, Nat.add_comm,
-      shiftRight_add, shiftRight_eq_div_pow _ 1]
-    simpa using shiftRight_trailingZeros_mod_two h
-  · rwa [Int.add_comm, trailingZeros_two_mul_add_one, shiftRight_zero]
-termination_by i.natAbs
-
-theorem two_pow_trailingZeros_dvd {i : Int} (h : i ≠ 0) :
-    2 ^ i.trailingZeros ∣ i := by
-  rcases i.emod_two_eq with h' | h'
-  · rcases Int.dvd_of_emod_eq_zero h' with ⟨a, rfl⟩
-    simp only [ne_eq, Int.mul_eq_zero, Int.reduceEq, false_or] at h
-    rw [trailingZeros_two_mul h, Int.pow_succ']
-    exact Int.mul_dvd_mul_left _ (two_pow_trailingZeros_dvd h)
-  · rw (occs := .pos [1]) [← Int.emod_add_mul_ediv i 2, h', Int.add_comm, trailingZeros_two_mul_add_one]
-    exact Int.one_dvd _
-termination_by i.natAbs
-
-theorem trailingZeros_shiftLeft {x : Int} (hx : x ≠ 0) (n : Nat) :
-    trailingZeros (x <<< n) = x.trailingZeros + n := by
-  have : NeZero x := ⟨hx⟩
-  induction n <;> simp [Int.shiftLeft_succ', trailingZeros_two_mul (NeZero.ne _), *, Nat.add_assoc]
-
-@[simp]
-theorem trailingZeros_neg (x : Int) : trailingZeros (-x) = x.trailingZeros := by
-  by_cases hx : x = 0
-  · simp [hx]
-  rcases x.emod_two_eq with h | h
-  · rcases Int.dvd_of_emod_eq_zero h with ⟨a, rfl⟩
-    simp only [Int.mul_ne_zero_iff, ne_eq, Int.reduceEq, not_false_eq_true, true_and] at hx
-    rw [← Int.mul_neg, trailingZeros_two_mul hx, trailingZeros_two_mul (Int.neg_ne_zero.mpr hx)]
-    rw [trailingZeros_neg]
-  · simp [trailingZeros_eq_zero_of_mod_eq, h]
-termination_by x.natAbs
-
-end Int
-
-/--
-A dyadic rational is either zero or of the form `n * 2^(-k)` for some (unique) `n k : Int`
-where `n` is odd.
--/
-inductive Dyadic where
-  /-- The dyadic number `0`. -/
-  | zero
-  /-- The dyadic number `n * 2^(-k)` for some odd `n` and integer `k`. -/
-  | ofOdd (n : Int) (k : Int) (hn : n % 2 = 1)
-deriving DecidableEq
-
-namespace Dyadic
-
-/-- Returns the dyadic number representation of `i * 2 ^ (-exp)`. -/
-def ofIntWithPrec (i : Int) (prec : Int) : Dyadic :=
-  if h : i = 0 then .zero
-  else .ofOdd (i >>> i.trailingZeros) (prec - i.trailingZeros) (Int.shiftRight_trailingZeros_mod_two h)
-
-/-- Convert an integer to a dyadic number (which will necessarily have non-positive precision). -/
-def ofInt (i : Int) : Dyadic :=
-  Dyadic.ofIntWithPrec i 0
-
-instance (n : Nat) : OfNat Dyadic n where
-  ofNat := Dyadic.ofInt n
-
-instance : IntCast Dyadic := ⟨ofInt⟩
-instance : NatCast Dyadic := ⟨fun x => ofInt x⟩
-
-/-- Add two dyadic numbers. -/
-protected def add (x y : Dyadic) : Dyadic :=
-  match x, y with
-  | .zero, y => y
-  | x, .zero => x
-  | .ofOdd n₁ k₁ hn₁, .ofOdd n₂ k₂ hn₂ =>
-    match k₁ - k₂ with
-    | 0 => .ofIntWithPrec (n₁ + n₂) k₁
-    -- TODO: these `simp_all` calls where previously factored out into a `where finally` clause,
-    -- but there is apparently a bad interaction with the module system.
-    | (d@hd:(d' + 1) : Nat) => .ofOdd (n₁ + (n₂ <<< d)) k₁ (by simp_all [Int.shiftLeft_eq, Int.pow_succ, ← Int.mul_assoc])
-    | -(d + 1 : Nat) => .ofOdd (n₁ <<< (d + 1) + n₂) k₂ (by simp_all [Int.shiftLeft_eq, Int.pow_succ, ← Int.mul_assoc])
-
-instance : Add Dyadic := ⟨Dyadic.add⟩
-
-/-- Multiply two dyadic numbers. -/
-protected def mul (x y : Dyadic) : Dyadic :=
-  match x, y with
-  | .zero, _ => .zero
-  | _, .zero => .zero
-  | .ofOdd n₁ k₁ hn₁, .ofOdd n₂ k₂ hn₂ =>
-    .ofOdd (n₁ * n₂) (k₁ + k₂) (by rw [Int.mul_emod, hn₁, hn₂]; rfl)
-
-instance : Mul Dyadic := ⟨Dyadic.mul⟩
-
-/-- Multiply two dyadic numbers. -/
-protected def pow (x : Dyadic) (i : Nat) : Dyadic :=
-  match x with
-  | .zero => if i = 0 then 1 else 0
-  | .ofOdd n k hn =>
-    .ofOdd (n ^ i) (k * i) (by induction i <;> simp [Int.pow_succ, Int.mul_emod, *])
-
-instance : Pow Dyadic Nat := ⟨Dyadic.pow⟩
-
-/-- Negate a dyadic number. -/
-protected def neg (x : Dyadic) : Dyadic :=
-  match x with
-  | .zero => .zero
-  | .ofOdd n k hn => .ofOdd (-n) k (by rwa [Int.neg_emod_two])
-
-instance : Neg Dyadic := ⟨Dyadic.neg⟩
-
-/-- Subtract two dyadic numbers. -/
-protected def sub (x y : Dyadic) : Dyadic := x + (- y)
-
-instance : Sub Dyadic := ⟨Dyadic.sub⟩
-
-/-- Shift a dyadic number left by `i` bits. -/
-protected def shiftLeft (x : Dyadic) (i : Int) : Dyadic :=
-  match x with
-  | .zero => .zero
-  | .ofOdd n k hn => .ofOdd n (k - i) hn
-
-/-- Shift a dyadic number right by `i` bits. -/
-protected def shiftRight (x : Dyadic) (i : Int) : Dyadic :=
-  match x with
-  | .zero => .zero
-  | .ofOdd n k hn => .ofOdd n (k + i) hn
-
-instance : HShiftLeft Dyadic Int Dyadic := ⟨Dyadic.shiftLeft⟩
-instance : HShiftRight Dyadic Int Dyadic := ⟨Dyadic.shiftRight⟩
-
-instance : HShiftLeft Dyadic Nat Dyadic := ⟨fun x y => x <<< (y : Int)⟩
-instance : HShiftRight Dyadic Nat Dyadic := ⟨fun x y => x >>> (y : Int)⟩
-
--- TODO: move this
-theorem _root_.Int.natAbs_emod_two (i : Int) : i.natAbs % 2 = (i % 2).natAbs := by omega
-
-/-- Convert a dyadic number to a rational number. -/
-def toRat (x : Dyadic) : Rat :=
-  match x with
-  | .zero => 0
-  | .ofOdd n (k : Nat) hn =>
-    have reduced : n.natAbs.Coprime (2 ^ k) := by
-      apply Coprime.pow_right
-      rw [coprime_iff_gcd_eq_one, Nat.gcd_comm, Nat.gcd_def]
-      simp [hn, Int.natAbs_emod_two]
-    ⟨n, 2 ^ k, Nat.ne_of_gt (Nat.pow_pos (by decide)), reduced⟩
-  | .ofOdd n (-((k : Nat) + 1)) hn =>
-    (n * (2 ^ (k + 1) : Nat) : Int)
-
-@[simp] protected theorem zero_eq : Dyadic.zero = 0 := rfl
-@[simp] protected theorem add_zero (x : Dyadic) : x + 0 = x := by cases x <;> rfl
-@[simp] protected theorem zero_add (x : Dyadic) : 0 + x = x := by cases x <;> rfl
-@[simp] protected theorem neg_zero : (-0 : Dyadic) = 0 := rfl
-@[simp] protected theorem mul_zero (x : Dyadic) : x * 0 = 0 := by cases x <;> rfl
-@[simp] protected theorem zero_mul (x : Dyadic) : 0 * x = 0 := by cases x <;> rfl
-
-@[simp] theorem toRat_zero : toRat 0 = 0 := rfl
-
-theorem _root_.Rat.mkRat_one (x : Int) : mkRat x 1 = x := by
-  rw [← Rat.mk_den_one, Rat.mk_eq_mkRat]
-
-theorem toRat_ofOdd_eq_mkRat :
-    toRat (.ofOdd n k hn) = mkRat (n <<< (-k).toNat) (1 <<< k.toNat) := by
-  cases k
-  · simp [toRat, Rat.mk_eq_mkRat, Int.shiftLeft_eq, Nat.shiftLeft_eq]
-  · simp [toRat, Int.neg_negSucc, Rat.mkRat_one, Int.shiftLeft_eq]
-
-theorem toRat_ofIntWithPrec_eq_mkRat :
-    toRat (.ofIntWithPrec n k) = mkRat (n <<< (-k).toNat) (1 <<< k.toNat) := by
-  simp only [ofIntWithPrec]
-  split
-  · simp_all
-  rw [toRat_ofOdd_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
-  simp only [Int.natCast_shiftLeft, Int.cast_ofNat_Int, Int.shiftLeft_mul_shiftLeft, Int.mul_one]
-  have : (-(k - n.trailingZeros) : Int).toNat + k.toNat =
-      n.trailingZeros + ((-k).toNat + (k - n.trailingZeros).toNat) := by omega
-  rw [this, Int.shiftLeft_add, Int.shiftRight_shiftLeft_cancel]
-  exact Int.two_pow_trailingZeros_dvd ‹_›
-
-theorem toRat_ofIntWithPrec_eq_mul_two_pow : toRat (.ofIntWithPrec n k) = n * 2 ^ (-k) := by
-  rw [toRat_ofIntWithPrec_eq_mkRat, Rat.zpow_neg, Int.shiftLeft_eq, Nat.one_shiftLeft]
-  rw [Rat.mkRat_eq_div, Rat.div_def]
-  have : ((2 : Int) : Rat) ≠ 0 := by decide
-  simp only [Rat.intCast_mul, Rat.intCast_pow, ← Rat.zpow_natCast, ← Rat.intCast_natCast,
-    Int.natCast_pow, Int.cast_ofNat_Int, ← Rat.zpow_neg, Rat.mul_assoc, ne_eq,
-    Rat.intCast_eq_zero_iff, Int.reduceEq, not_false_eq_true, ← Rat.zpow_add]
-  rw [Int.add_neg_eq_sub, ← Int.neg_sub, Int.toNat_sub_toNat_neg]
-  rfl
-
-example : ((3 : Dyadic) >>> 2) + ((3 : Dyadic) >>> 2) = ((3 : Dyadic) >>> 1) := rfl -- 3/4 + 3/4 = 3/2
-example : ((7 : Dyadic) >>> 3) + ((1 : Dyadic) >>> 3) = 1 := rfl -- 7/8 + 1/8 = 1
-example : (12 : Dyadic) + ((3 : Dyadic) >>> 1) = (27 : Dyadic) >>> 1 := rfl -- 12 + 3/2 = 27/2 = (2 * 13 + 1)/2^1
-example : ((3 : Dyadic) >>> 1).add 12 =  (27 : Dyadic) >>> 1 := rfl -- 3/2 + 12 = 27/2 = (2 * 13 + 1)/2^1
-example : (12 : Dyadic).add 12 = 24 := rfl -- 12 + 12 = 24
-
-@[simp]
-theorem toRat_add (x y : Dyadic) : toRat (x + y) = toRat x + toRat y := by
-  match x, y with
-  | .zero, _ => simp [toRat, Rat.zero_add]
-  | _, .zero => simp [toRat, Rat.add_zero]
-  | .ofOdd n₁ k₁ hn₁, .ofOdd n₂ k₂ hn₂ =>
-    change (Dyadic.add _ _).toRat = _
-    rw [Dyadic.add, toRat_ofOdd_eq_mkRat, toRat_ofOdd_eq_mkRat]
-    rw [Rat.mkRat_add_mkRat _ _ (NeZero.ne _) (NeZero.ne _)]
-    split
-    · rename_i h
-      cases Int.sub_eq_zero.mp h
-      rw [toRat_ofIntWithPrec_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
-      simp [Int.shiftLeft_mul_shiftLeft, Int.add_shiftLeft, Int.add_mul, Nat.add_assoc]
-    · rename_i h
-      cases Int.sub_eq_iff_eq_add.mp h
-      rw [toRat_ofOdd_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
-      simp only [succ_eq_add_one, Int.ofNat_eq_coe, Int.add_shiftLeft, ← Int.shiftLeft_add,
-        Int.natCast_mul, Int.natCast_shiftLeft, Int.shiftLeft_mul_shiftLeft, Int.add_mul]
-      congr 2 <;> omega
-    · rename_i h
-      cases Int.sub_eq_iff_eq_add.mp h
-      rw [toRat_ofOdd_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
-      simp only [Int.add_shiftLeft, ← Int.shiftLeft_add, Int.natCast_mul, Int.natCast_shiftLeft,
-        Int.cast_ofNat_Int, Int.shiftLeft_mul_shiftLeft, Int.mul_one, Int.add_mul]
-      congr 2 <;> omega
-
-@[simp]
-theorem toRat_neg (x : Dyadic) : toRat (-x) = - toRat x := by
-  change x.neg.toRat = _
-  cases x
-  · rfl
-  · simp [Dyadic.neg, Rat.neg_mkRat, Int.neg_shiftLeft, toRat_ofOdd_eq_mkRat]
-
-@[simp]
-theorem toRat_sub (x y : Dyadic) : toRat (x - y) = toRat x - toRat y := by
-  change toRat (x + -y) = _
-  simp [Rat.sub_eq_add_neg]
-
-@[simp]
-theorem toRat_mul (x y : Dyadic) : toRat (x * y) = toRat x * toRat y := by
-  match x, y with
-  | .zero, _ => simp
-  | _, .zero => simp
-  | .ofOdd n₁ k₁ hn₁, .ofOdd n₂ k₂ hn₂ =>
-    change (Dyadic.mul _ _).toRat = _
-    rw [Dyadic.mul, toRat_ofOdd_eq_mkRat, toRat_ofOdd_eq_mkRat, toRat_ofOdd_eq_mkRat,
-      Rat.mkRat_mul_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
-    simp only [Int.natCast_mul, Int.natCast_shiftLeft, Int.cast_ofNat_Int,
-      Int.shiftLeft_mul_shiftLeft, Int.mul_one]
-    congr 1; omega
-
-@[simp]
-protected theorem pow_zero (x : Dyadic) : x ^ 0 = 1 := by
-  change x.pow 0 = 1
-  cases x <;> simp [Dyadic.pow] <;> rfl
-
-protected theorem pow_succ (x : Dyadic) (n : Nat) : x ^ (n + 1) = x ^ n * x := by
-  change x.pow (n + 1) = x.pow n * x
-  cases x
-  · simp [Dyadic.pow]
-  · change _ = Dyadic.mul _ _
-    simp [Dyadic.pow, Dyadic.mul, Int.pow_succ, Int.mul_add]
-
-@[simp]
-theorem toRat_pow (x : Dyadic) (n : Nat) : toRat (x ^ n) = toRat x ^ n := by
-  induction n with
-  | zero => simp; rfl
-  | succ k ih => simp [Dyadic.pow_succ, Rat.pow_succ, ih]
-
-@[simp]
-theorem toRat_intCast (x : Int) : (x : Dyadic).toRat = x := by
-  change (ofInt x).toRat = x
-  simp [ofInt, toRat_ofIntWithPrec_eq_mul_two_pow]
-
-@[simp]
-theorem toRat_natCast (x : Nat) : (x : Dyadic).toRat = x := by
-  change (ofInt x).toRat = x
-  simp [ofInt, toRat_ofIntWithPrec_eq_mul_two_pow, Rat.intCast_natCast]
-
-@[simp] theorem of_ne_zero : ofOdd n k hn ≠ 0 := Dyadic.noConfusion
-@[simp] theorem zero_ne_of : 0 ≠ ofOdd n k hn := Dyadic.noConfusion
-
-@[simp]
-theorem toRat_eq_zero_iff {x : Dyadic} : x.toRat = 0 ↔ x = 0 := by
-  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
-  cases x
-  · rfl
-  · simp only [toRat_ofOdd_eq_mkRat, ne_eq, shiftLeft_eq_zero_iff, succ_ne_self, not_false_eq_true,
-      Rat.mkRat_eq_zero, Int.shiftLeft_eq_zero_iff] at h
-    cases h
-    contradiction
-
-theorem ofOdd_eq_ofIntWithPrec : ofOdd n k hn = ofIntWithPrec n k := by
-  simp only [ofIntWithPrec, Dyadic.zero_eq, Int.trailingZeros_eq_zero_of_mod_eq hn,
-    Int.shiftRight_zero, Int.cast_ofNat_Int, Int.sub_zero, right_eq_dite_iff, of_ne_zero, imp_false]
-  intro rfl; contradiction
-
-theorem toRat_ofOdd_eq_mul_two_pow : toRat (.ofOdd n k hn) = n * 2 ^ (-k) := by
-  rw [ofOdd_eq_ofIntWithPrec, toRat_ofIntWithPrec_eq_mul_two_pow]
-
-@[simp]
-theorem ofIntWithPrec_zero {i : Int} : ofIntWithPrec 0 i = 0 := rfl
-
-@[simp]
-theorem neg_ofOdd : -ofOdd n k hn = ofOdd (-n) k (by simpa using hn) := rfl
-
-@[simp]
-theorem neg_ofIntWithPrec {i prec : Int} : -ofIntWithPrec i prec = ofIntWithPrec (-i) prec := by
-  rw [ofIntWithPrec, ofIntWithPrec]
-  simp only [Dyadic.zero_eq, Int.neg_eq_zero, Int.trailingZeros_neg]
-  split
-  · rfl
-  · obtain ⟨a, h⟩ := Int.two_pow_trailingZeros_dvd ‹_›
-    rw [Int.mul_comm, ← Int.shiftLeft_eq] at h
-    conv => enter [1, 1, 1, 1]; rw [h]
-    conv => enter [2, 1, 1]; rw [h]
-    simp only [Int.shiftLeft_shiftRight_cancel, neg_ofOdd, ← Int.neg_shiftLeft]
-
-theorem ofIntWithPrec_shiftLeft_add {n : Nat} :
-    ofIntWithPrec ((x : Int) <<< n) (i + n) = ofIntWithPrec x i := by
-  rw [ofIntWithPrec, ofIntWithPrec]
-  simp only [Int.shiftLeft_eq_zero_iff]
-  split
-  · rfl
-  · simp [Int.trailingZeros_shiftLeft, *, Int.shiftLeft_shiftRight_eq_shiftRight_of_le,
-      Int.add_comm x.trailingZeros n, ← Int.sub_sub]
-
-/-- The "precision" of a dyadic number, i.e. in `n * 2^(-p)` with `n` odd the precision is `p`. -/
--- TODO: If `WithBot` is upstreamed, replace this with `WithBot Int`.
-def precision : Dyadic → Option Int
-  | .zero => none
-  | .ofOdd _ p _ => some p
-
-theorem precision_ofIntWithPrec_le {i : Int} (h : i ≠ 0) (prec : Int) :
-    (ofIntWithPrec i prec).precision ≤ some prec := by
-  simp [ofIntWithPrec, h, precision]
-  omega
-
-@[simp] theorem precision_zero : (0 : Dyadic).precision = none := rfl
-@[simp] theorem precision_neg {x : Dyadic} : (-x).precision = x.precision :=
-  match x with
-  | .zero => rfl
-  | .ofOdd _ _ _ => rfl
-
-end Dyadic
-
-namespace Rat
-
-open Dyadic
-
-/--
-Convert a rational number `x` to the greatest dyadic number with precision at most `prec`
-which is less than or equal to `x`.
--/
-def toDyadic (x : Rat) (prec : Int) : Dyadic :=
-  match prec with
-  | (n : Nat) => .ofIntWithPrec ((x.num <<< n) / x.den) prec
-  | -(n + 1 : Nat) => .ofIntWithPrec (x.num / (x.den <<< (n + 1))) prec
-
-theorem toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) :
-    Rat.toDyadic (mkRat a b) prec =
-      .ofIntWithPrec ((a <<< prec.toNat) / (b <<< (-prec).toNat)) prec := by
-  by_cases hb : b = 0
-  · cases prec <;> simp [hb, Rat.toDyadic]
-  rcases h : mkRat a b with ⟨n, d, hnz, hr⟩
-  obtain ⟨m, hm, rfl, rfl⟩ := Rat.mkRat_num_den hb h
-  cases prec
-  · simp only [Rat.toDyadic, Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_natCast,
-      shiftLeft_zero, Int.natCast_mul]
-    rw [Int.mul_comm d, ← Int.ediv_ediv (by simp), ← Int.shiftLeft_mul,
-      Int.mul_ediv_cancel _ (by simpa using hm)]
-  · simp only [Rat.toDyadic, Int.natCast_shiftLeft, Int.negSucc_eq, ← Int.natCast_add_one,
-      Int.toNat_neg_natCast, Int.shiftLeft_zero, Int.neg_neg, Int.toNat_natCast, Int.natCast_mul]
-    rw [Int.mul_comm d, ← Int.mul_shiftLeft, ← Int.ediv_ediv (by simp),
-      Int.mul_ediv_cancel _ (by simpa using hm)]
-
-theorem toDyadic_eq_ofIntWithPrec (x : Rat) (prec : Int) :
-    x.toDyadic prec = .ofIntWithPrec ((x.num <<< prec.toNat) / (x.den <<< (-prec).toNat)) prec := by
-  conv => lhs; rw [← Rat.mkRat_self x]
-  rw [Rat.toDyadic_mkRat]
-
-/--
-Converting a rational to a dyadic at a given precision and then back to a rational
-gives the same result as taking the floor of the rational at precision `2 ^ prec`.
--/
-theorem toRat_toDyadic (x : Rat) (prec : Int) :
-    (x.toDyadic prec).toRat = (x * 2 ^ prec).floor / 2 ^ prec := by
-  rw [Rat.toDyadic_eq_ofIntWithPrec, toRat_ofIntWithPrec_eq_mul_two_pow, Rat.zpow_neg, Rat.div_def]
-  congr 2
-  rw [Rat.floor_def, Int.shiftLeft_eq, Nat.shiftLeft_eq]
-  match prec with
-  | .ofNat prec =>
-    simp only [Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_natCast, Nat.pow_zero,
-      Nat.mul_one]
-    have : (2 ^ prec : Rat) = ((2 ^ prec : Nat) : Rat) := by simp
-    rw [Rat.zpow_natCast, this, Rat.mul_def']
-    simp only [Rat.num_mkRat, Rat.den_mkRat]
-    simp only [Rat.natCast_pow, Rat.natCast_ofNat, Rat.num_pow, Rat.num_ofNat, Rat.den_pow,
-      Rat.den_ofNat, Nat.one_pow, Nat.mul_one]
-    split
-    · simp_all
-    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
-      congr 1
-      rw [Int.natCast_ediv, Int.mul_ediv_cancel']
-      rw [Int.natCast_dvd_natCast]
-      apply gcd_dvd_left
-  | .negSucc prec =>
-    simp only [Int.toNat_negSucc, Int.pow_zero, Int.mul_one, Int.neg_negSucc, Int.natCast_mul,
-      Int.natCast_pow, Int.cast_ofNat_Int]
-    have : (2 ^ ((prec : Int) + 1)) = ((2 ^ (prec + 1) : Nat) : Rat) := by simp; rfl
-    rw [Int.negSucc_eq, Rat.zpow_neg, this, Rat.mul_def']
-    simp only [Rat.num_mkRat, Rat.den_mkRat]
-    simp only [natCast_pow, natCast_ofNat, den_inv, num_pow, num_ofNat, Int.natAbs_pow,
-      Int.reduceAbs, num_inv, den_pow, den_ofNat, Nat.one_pow, Int.cast_ofNat_Int, Int.mul_one]
-    have : ¬ (2 ^ (prec + 1) : Int) = 0 := NeZero.out
-    simp only [if_neg this]
-    have : (2 ^ (prec + 1) : Int).sign = 1 := by simpa using Int.pow_pos (by decide)
-    simp only [this]
-    have : x.den * 2 ^ (prec + 1) = 0 ↔ x.den = 0 := by
-      rw [Nat.mul_eq_zero]
-      simp_all
-    simp only [this, Int.mul_one]
-    split
-    · simp_all
-    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
-      congr 1
-      rw [Int.natCast_ediv, Int.mul_ediv_cancel']
-      · simp
-      · rw [Int.natCast_dvd_natCast]
-        apply gcd_dvd_left
-
-theorem toRat_toDyadic_le {x : Rat} {prec : Int} : (x.toDyadic prec).toRat ≤ x := by
-  rw [toRat_toDyadic]
-  have : (x * 2 ^ prec).floor ≤ x * 2 ^ prec := Rat.floor_le _
-  apply Rat.le_of_mul_le_mul_right (c := 2 ^ prec)
-  rw [Rat.div_mul_cancel]
-  exact this
-  · apply Rat.ne_of_gt (Rat.zpow_pos (by decide))
-  · exact Rat.zpow_pos (by decide)
-
-theorem lt_toRat_toDyadic_add {x : Rat} {prec : Int} :
-    x < (x.toDyadic prec + ofIntWithPrec 1 prec).toRat := by
-  rw [toRat_add, toRat_toDyadic, toRat_ofIntWithPrec_eq_mul_two_pow]
-  have := Rat.lt_floor_add_one (x * 2 ^ prec)
-  rw [Rat.zpow_neg, Rat.div_def, ← Rat.add_mul]
-  apply Rat.lt_of_mul_lt_mul_right (c := 2 ^ prec)
-  rw [Rat.mul_assoc, Rat.inv_mul_cancel, Rat.mul_one]
-  exact mod_cast this
-  · apply Rat.ne_of_gt (Rat.zpow_pos (by decide))
-  · exact Rat.zpow_nonneg (by decide)
-
--- TODO: `x.toDyadic prec` is the unique dyadic with the given precision satisfying the two inequalities above.
-
-end Rat
-
-namespace Dyadic
-
-/--
-Rounds a dyadic rational `x` down to the greatest dyadic number with precision at most `prec`
-which is less than or equal to `x`.
--/
-def roundDown (x : Dyadic) (prec : Int) : Dyadic :=
-  match x with
-  | .zero => .zero
-  | .ofOdd n k _ =>
-    match k - prec with
-    | .ofNat l => .ofIntWithPrec (n >>> l) prec
-    | .negSucc _ => x
-
-theorem roundDown_eq_self_of_le {x : Dyadic} {prec : Int} (h : x.precision ≤ some prec) :
-    roundDown x prec = x := by
-  rcases x with _ | ⟨n, k, hn⟩
-  · rfl
-  · simp only [precision] at h
-    obtain ⟨a, rfl⟩ := h.dest
-    rcases a with _ | a
-    · simp [roundDown, ofOdd_eq_ofIntWithPrec]
-    · have : k - (k + (a + 1 : Nat)) = Int.negSucc a := by omega
-      simp only [roundDown, this]
-
-@[simp]
-theorem toDyadic_toRat (x : Dyadic) (prec : Int) :
-    x.toRat.toDyadic prec = x.roundDown prec := by
-  rcases x with _ | ⟨n, k, hn⟩
-  · cases prec <;> simp [Rat.toDyadic, roundDown]
-  · simp only [toRat_ofOdd_eq_mkRat, roundDown]
-    rw [Rat.toDyadic_mkRat]
-    simp only [← Int.shiftLeft_add, Int.natCast_shiftLeft, Int.cast_ofNat_Int]
-    rw [Int.shiftLeft_eq' 1, Int.one_mul, ← Int.shiftRight_eq_div_pow]
-    rw [Int.shiftLeft_shiftRight_eq, ← Int.toNat_sub, ← Int.toNat_sub, ← Int.neg_sub]
-    have : ((k.toNat + (-prec).toNat : Nat) - ((-k).toNat + prec.toNat : Nat) : Int) = k - prec := by
-      omega
-    rw [this]
-    cases h : k - prec
-    · simp
-    · simp only [Int.neg_negSucc, Int.natCast_add, Int.cast_ofNat_Int, Int.toNat_natCast_add_one,
-        Int.toNat_negSucc, Int.shiftRight_zero]
-      rw [Int.negSucc_eq, Int.eq_neg_comm, Int.neg_sub, eq_comm, Int.sub_eq_iff_eq_add] at h
-      simp only [h, ← Int.natCast_add_one, Int.add_comm _ k, ofIntWithPrec_shiftLeft_add,
-        ofOdd_eq_ofIntWithPrec]
-
-theorem toRat_inj {x y : Dyadic} : x.toRat = y.toRat ↔ x = y := by
-  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
-  cases x <;> cases y
-  · rfl
-  · simp [eq_comm (a := (0 : Rat))] at h
-  · simp at h
-  · rename_i n₁ k₁ hn₁ n₂ k₂ hn₂
-    replace h := congrArg (·.toDyadic (max k₁ k₂)) h
-    simpa [toDyadic_toRat, roundDown_eq_self_of_le, precision, Int.le_max_left, Int.le_max_right]
-      using h
-
-theorem add_comm (x y : Dyadic) : x + y = y + x := by
-  rw [← toRat_inj, toRat_add, toRat_add, Rat.add_comm]
-
-theorem add_assoc (x y z : Dyadic) : (x + y) + z = x + (y + z) := by
-  rw [← toRat_inj, toRat_add, toRat_add, toRat_add, toRat_add, Rat.add_assoc]
-
-theorem mul_comm (x y : Dyadic) : x * y = y * x := by
-  rw [← toRat_inj, toRat_mul, toRat_mul, Rat.mul_comm]
-
-theorem mul_assoc (x y z : Dyadic) : (x * y) * z = x * (y * z) := by
-  rw [← toRat_inj, toRat_mul, toRat_mul, toRat_mul, toRat_mul, Rat.mul_assoc]
-
-theorem mul_one (x : Dyadic) : x * 1 = x := by
-  rw [← toRat_inj, toRat_mul]
-  exact Rat.mul_one x.toRat
-
-theorem one_mul (x : Dyadic) : 1 * x = x := by
-  rw [← toRat_inj, toRat_mul]
-  exact Rat.one_mul x.toRat
-
-theorem add_mul (x y z : Dyadic) : (x + y) * z = x * z + y * z := by
-  simp [← toRat_inj, Rat.add_mul]
-
-theorem mul_add (x y z : Dyadic) : x * (y + z) = x * y + x * z := by
-  simp [← toRat_inj, Rat.mul_add]
-
-theorem neg_add_cancel (x : Dyadic) : -x + x = 0 := by
-  simp [← toRat_inj, Rat.neg_add_cancel]
-
-theorem neg_mul (x y : Dyadic) : -x * y = -(x * y) := by
-  simp [← toRat_inj, Rat.neg_mul]
-
-/-- Determine if a dyadic rational is strictly less than another. -/
-def blt (x y : Dyadic) : Bool :=
-  match x, y with
-  | .zero, .zero => false
-  | .zero, .ofOdd n₂ _ _ => 0 < n₂
-  | .ofOdd n₁ _ _, .zero => n₁ < 0
-  | .ofOdd n₁ k₁ _, .ofOdd n₂ k₂ _ =>
-    match k₂ - k₁ with
-    | (l : Nat) => (n₁ <<< l) < n₂
-    | -((l+1 : Nat)) => n₁ < (n₂ <<< (l + 1))
-
-/-- Determine if a dyadic rational is less than or equal to another. -/
-def ble (x y : Dyadic) : Bool :=
-  match x, y with
-  | .zero, .zero => true
-  | .zero, .ofOdd n₂ _ _ => 0 ≤ n₂
-  | .ofOdd n₁ _ _, .zero => n₁ ≤ 0
-  | .ofOdd n₁ k₁ _, .ofOdd n₂ k₂ _ =>
-    match k₂ - k₁ with
-    | (l : Nat) => (n₁ <<< l) ≤ n₂
-    | -((l+1 : Nat)) => n₁ ≤ (n₂ <<< (l + 1))
-
-theorem blt_iff_toRat {x y : Dyadic} : blt x y ↔ x.toRat < y.toRat := by
-  rcases x with _ | ⟨n₁, k₁, hn₁⟩ <;> rcases y with _ | ⟨n₂, k₂, hn₂⟩
-  · decide
-  · simp only [blt, decide_eq_true_eq, Dyadic.zero_eq, toRat_zero, toRat_ofOdd_eq_mul_two_pow,
-      Rat.mul_pos_iff_of_pos_right (Rat.zpow_pos (by decide : (0 : Rat) < 2)), Rat.intCast_pos]
-  · simp only [blt, decide_eq_true_eq, Dyadic.zero_eq, toRat_zero, toRat_ofOdd_eq_mul_two_pow,
-      Rat.mul_neg_iff_of_pos_right (Rat.zpow_pos (by decide : (0 : Rat) < 2)), Rat.intCast_neg_iff]
-  · simp only [blt, toRat_ofOdd_eq_mul_two_pow,
-      ← Rat.div_lt_iff (Rat.zpow_pos (by decide : (0 : Rat) < 2)), Rat.div_def, ← Rat.zpow_neg,
-      Int.neg_neg, Rat.mul_assoc, ne_eq, Rat.ofNat_eq_ofNat, reduceCtorEq, not_false_eq_true,
-      ← Rat.zpow_add, Int.shiftLeft_eq]
-    rw [Int.add_comm, Int.add_neg_eq_sub]
-    split
-    · simp [decide_eq_true_eq, ← Rat.intCast_lt_intCast, Rat.zpow_natCast, *]
-    · simp only [decide_eq_true_eq, Int.negSucc_eq, *]
-      rw [Rat.zpow_neg, ← Rat.div_def, Rat.div_lt_iff (Rat.zpow_pos (by decide))]
-      simp [← Rat.intCast_lt_intCast, ← Rat.zpow_natCast, *]
-
-theorem blt_eq_false_iff : blt x y = false ↔ ble y x = true := by
-  cases x <;> cases y
-  · simp [ble, blt]
-  · simp [ble, blt]
-  · simp [ble, blt]
-  · rename_i n₁ k₁ hn₁ n₂ k₂ hn₂
-    simp only [blt, ble]
-    rw [← Int.neg_sub]
-    rcases k₁ - k₂ with (_ | _) | _
-    · simp
-    · simp [← Int.negSucc_eq]
-    · simp only [Int.neg_negSucc, decide_eq_false_iff_not, Int.not_lt,
-        decide_eq_true_eq]
-
-theorem ble_iff_toRat : ble x y ↔ x.toRat ≤ y.toRat := by
-  rw [← blt_eq_false_iff, Bool.eq_false_iff]
-  simp only [ne_eq, blt_iff_toRat, Rat.not_lt]
-
-instance : LT Dyadic where
-  lt x y := blt x y
-
-instance : LE Dyadic where
-  le x y := ble x y
-
-instance : DecidableLT Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
-instance : DecidableLE Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
-
-theorem lt_iff_toRat {x y : Dyadic} : x < y ↔ x.toRat < y.toRat := blt_iff_toRat
-
-theorem le_iff_toRat {x y : Dyadic} : x ≤ y ↔ x.toRat ≤ y.toRat := ble_iff_toRat
-
-@[simp]
-protected theorem not_le {x y : Dyadic} : ¬x < y ↔ y ≤ x := by
-  simp only [· ≤ ·, · < ·, Bool.not_eq_true, blt_eq_false_iff]
-
-@[simp]
-protected theorem not_lt {x y : Dyadic} : ¬x ≤ y ↔ y < x := by
-  rw [← Dyadic.not_le, Decidable.not_not]
-
-@[simp]
-protected theorem le_refl (x : Dyadic) : x ≤ x := by
-  rw [le_iff_toRat]
-  exact Rat.le_refl
-
-protected theorem le_trans {x y z : Dyadic} (h : x ≤ y) (h' : y ≤ z) : x ≤ z := by
-  rw [le_iff_toRat] at h h' ⊢
-  exact Rat.le_trans h h'
-
-protected theorem le_antisymm {x y : Dyadic} (h : x ≤ y) (h' : y ≤ x) : x = y := by
-  rw [le_iff_toRat] at h h'
-  rw [← toRat_inj]
-  exact Rat.le_antisymm h h'
-
-protected theorem le_total (x y : Dyadic) : x ≤ y ∨ y ≤ x := by
-  rw [le_iff_toRat, le_iff_toRat]
-  exact Rat.le_total
-
-instance : Std.LawfulOrderLT Dyadic where
-  lt_iff a b := by rw [← Dyadic.not_lt, iff_and_self]; exact (Dyadic.le_total _ _).resolve_left
-
-instance : Std.IsPreorder Dyadic where
-  le_refl := Dyadic.le_refl
-  le_trans _ _ _ := Dyadic.le_trans
-
-instance : Std.IsPartialOrder Dyadic where
-  le_antisymm _ _ := Dyadic.le_antisymm
-
-instance : Std.IsLinearPreorder Dyadic where
-  le_total := Dyadic.le_total
-
-instance : Std.IsLinearOrder Dyadic where
-
-/-- `roundUp x prec` is the least dyadic number with precision at most `prec` which is greater than or equal to `x`. -/
-def roundUp (x : Dyadic) (prec : Int) : Dyadic :=
-  match x with
-  | .zero => .zero
-  | .ofOdd n k _ =>
-    match k - prec with
-    | .ofNat l => .ofIntWithPrec (-((-n) >>> l)) prec
-    | .negSucc _ => x
-
-theorem roundUp_eq_neg_roundDown_neg (x : Dyadic) (prec : Int) :
-    x.roundUp prec = -((-x).roundDown prec) := by
-  rcases x with _ | ⟨n, k, hn⟩
-  · rfl
-  · change _ = -(ofOdd ..).roundDown prec
-    rw [roundDown, roundUp]
-    split <;> simp
-
-end Dyadic

src/Init/Data/Dyadic/Instances.lean

@@ -1,60 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Robin Arnez
--/
-module
-
-prelude
-public import Init.Data.Dyadic.Basic
-public import Init.Grind.Ring.Basic
-public import Init.Grind.Ordered.Ring
-
-/-! # Internal `grind` algebra instances for `Dyadic`. -/
-
-open Lean.Grind
-
-namespace Dyadic
-
-instance : CommRing Dyadic where
-  nsmul := ⟨(· * ·)⟩
-  zsmul := ⟨(· * ·)⟩
-  add_zero := Dyadic.add_zero
-  add_comm := Dyadic.add_comm
-  add_assoc := Dyadic.add_assoc
-  mul_assoc := Dyadic.mul_assoc
-  mul_one := Dyadic.mul_one
-  one_mul := Dyadic.one_mul
-  zero_mul := Dyadic.zero_mul
-  mul_zero := Dyadic.mul_zero
-  mul_comm := Dyadic.mul_comm
-  pow_zero := Dyadic.pow_zero
-  pow_succ := Dyadic.pow_succ
-  sub_eq_add_neg _ _ := rfl
-  neg_add_cancel := Dyadic.neg_add_cancel
-  neg_zsmul i a := by
-    change ((-i : Int) : Dyadic) * a = -(i * a)
-    simp [← toRat_inj, Rat.neg_mul]
-  left_distrib := Dyadic.mul_add
-  right_distrib := Dyadic.add_mul
-  intCast_neg _ := by simp [← toRat_inj]
-  ofNat_succ n := by
-    change ((n + 1 : Int) : Dyadic) = ((n : Int) : Dyadic) + 1
-    simp [← toRat_inj, Rat.intCast_add]; rfl
-
-instance : IsCharP Dyadic 0 := IsCharP.mk' _ _
-  (ofNat_eq_zero_iff := fun x => by change (x : Dyadic) = 0 ↔ _; simp [← toRat_inj])
-
-instance : NoNatZeroDivisors Dyadic where
-  no_nat_zero_divisors k a b h₁ h₂ := by
-    change k * a = k * b at h₂
-    simp only [← toRat_inj, toRat_mul, toRat_natCast] at h₂ ⊢
-    simpa [← Rat.mul_assoc, Rat.inv_mul_cancel, h₁] using congrArg ((k : Rat)⁻¹ * ·) h₂
-
-instance : OrderedRing Dyadic where
-  zero_lt_one := by decide
-  add_le_left_iff _ := by simp [le_iff_toRat, Rat.add_le_add_right]
-  mul_lt_mul_of_pos_left {_ _ _} := by simpa [lt_iff_toRat] using Rat.mul_lt_mul_of_pos_left
-  mul_lt_mul_of_pos_right {_ _ _} := by simpa [lt_iff_toRat] using Rat.mul_lt_mul_of_pos_right
-
-end Dyadic

src/Init/Data/Dyadic/Inv.lean

@@ -1,80 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-prelude
-import Init.Data.Dyadic.Basic
-import Init.Data.Dyadic.Round
-import Init.Grind.Ordered.Ring
-
-/-!
-# Inversion for dyadic numbers
--/
-
-namespace Dyadic
-
-/--
-Inverts a dyadic number at a given (maximum) precision.
-Returns the greatest dyadic number with precision at most `prec` which is less than or equal to `1/x`.
-For `x = 0`, returns `0`.
--/
-def invAtPrec (x : Dyadic) (prec : Int) : Dyadic :=
-  match x with
-  | .zero => .zero
-  | _ => x.toRat.inv.toDyadic prec
-
-/-- For a positive dyadic `x`, `invAtPrec x prec * x ≤ 1`. -/
-theorem invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) :
-    invAtPrec x prec * x ≤ 1 := by
-  rw [le_iff_toRat]
-  rw [toRat_mul]
-  rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
-  unfold invAtPrec
-  cases x with
-  | zero =>
-    exfalso
-    contradiction
-  | ofOdd n k hn =>
-    simp only
-    have h_le : ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat ≤ (ofOdd n k hn).toRat.inv := Rat.toRat_toDyadic_le
-    have h_pos : 0 ≤ (ofOdd n k hn).toRat := by
-      rw [lt_iff_toRat, toRat_zero] at hx
-      exact Rat.le_of_lt hx
-    calc ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat * (ofOdd n k hn).toRat
-        ≤ (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := Rat.mul_le_mul_of_nonneg_right h_le h_pos
-      _ = 1 := by
-        apply Rat.inv_mul_cancel
-        rw [lt_iff_toRat, toRat_zero] at hx
-        exact Rat.ne_of_gt hx
-
-/-- For a positive dyadic `x`, `1 < (invAtPrec x prec + 2^(-prec)) * x`. -/
-theorem one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) :
-    1 < (invAtPrec x prec + ofIntWithPrec 1 prec) * x := by
-  rw [lt_iff_toRat]
-  rw [toRat_mul]
-  rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
-  unfold invAtPrec
-  cases x with
-  | zero =>
-    exfalso
-    contradiction
-  | ofOdd n k hn =>
-    simp only
-    have h_le : (ofOdd n k hn).toRat.inv < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat :=
-      Rat.lt_toRat_toDyadic_add
-    have h_pos : 0 < (ofOdd n k hn).toRat := by
-      rwa [lt_iff_toRat, toRat_zero] at hx
-    calc
-      1 = (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := by
-        symm
-        apply Rat.inv_mul_cancel
-        rw [lt_iff_toRat, toRat_zero] at hx
-        exact Rat.ne_of_gt hx
-      _ < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat * (ofOdd n k hn).toRat :=
-           Rat.mul_lt_mul_of_pos_right h_le h_pos
-
--- TODO: `invAtPrec` is the unique dyadic with the given precision satisfying the two inequalities above.
-
-end Dyadic

src/Init/Data/Dyadic/Round.lean

@@ -1,77 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-public import Init.Data.Dyadic.Basic
-import all Init.Data.Dyadic.Instances
-import Init.Data.Int.Bitwise.Lemmas
-import Init.Grind.Ordered.Rat
-import Init.Grind.Ordered.Field
-
-namespace Dyadic
-
-/-!
-Theorems about `roundUp` and `roundDown`.
--/
-
-public section
-
-theorem roundDown_le {x : Dyadic} {prec : Int} : roundDown x prec ≤ x :=
-  match x with
-  | .zero => Dyadic.le_refl _
-  | .ofOdd n k _ => by
-    unfold roundDown
-    dsimp
-    match h : k - prec with
-    | .ofNat l =>
-      dsimp
-      rw [ofOdd_eq_ofIntWithPrec, le_iff_toRat]
-      replace h : k = Int.ofNat l + prec := by omega
-      subst h
-      simp only [toRat_ofIntWithPrec_eq_mul_two_pow]
-      rw [Int.neg_add, Rat.zpow_add (by decide), ← Rat.mul_assoc]
-      refine Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_right ?_ (Rat.zpow_nonneg (by decide))
-      rw [Int.shiftRight_eq_div_pow]
-      rw [← Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_right (c := 2^(Int.ofNat l)) (Rat.zpow_pos (by decide))]
-      simp only [Int.natCast_pow, Int.cast_ofNat_Int, Int.ofNat_eq_coe]
-      rw [Rat.mul_assoc, ← Rat.zpow_add (by decide), Int.add_left_neg, Rat.zpow_zero, Rat.mul_one]
-      have : (2 : Rat) ^ (l : Int) = (2 ^ l : Int) := by
-        rw [Rat.zpow_natCast, Rat.intCast_pow, Rat.intCast_ofNat]
-      rw [this, ← Rat.intCast_mul, Rat.intCast_le_intCast]
-      exact Int.ediv_mul_le n (Int.pow_ne_zero (by decide))
-    | .negSucc _ =>
-      apply Dyadic.le_refl
-
-theorem precision_roundDown {x : Dyadic} {prec : Int} : (roundDown x prec).precision ≤ some prec := by
-  unfold roundDown
-  match x with
-  | zero => simp [precision]
-  | ofOdd n k hn =>
-    dsimp
-    split
-    · rename_i n' h
-      by_cases h' : n >>> n' = 0
-      · simp [h']
-      · exact precision_ofIntWithPrec_le h' _
-    · simp [precision]
-      omega
-
--- This theorem would characterize `roundDown` in terms of the order and `precision`.
--- theorem le_roundDown {x y : Dyadic} {prec : Int} (h : y.precision ≤ some prec) (h' : y ≤ x) :
---     y ≤ x.roundDown prec := sorry
-
-theorem le_roundUp {x : Dyadic} {prec : Int} : x ≤ roundUp x prec := by
-  rw [roundUp_eq_neg_roundDown_neg, Lean.Grind.OrderedAdd.le_neg_iff]
-  apply roundDown_le
-
-theorem precision_roundUp {x : Dyadic} {prec : Int} : (roundUp x prec).precision ≤ some prec := by
-  rw [roundUp_eq_neg_roundDown_neg, precision_neg]
-  exact precision_roundDown
-
--- This theorem would characterize `roundUp` in terms of the order and `precision`.
--- theorem roundUp_le {x y : Dyadic} {prec : Int} (h : y.precision ≤ some prec) (h' : x ≤ y) :
---    x.roundUp prec ≤ y := sorry

src/Init/Data/Fin/Basic.lean

@@ -51,11 +51,6 @@ The assumption `NeZero n` ensures that `Fin n` is nonempty.
 @[expose] protected def ofNat (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
 
-@[simp]
-theorem Internal.ofNat_eq_ofNat {n : Nat} {hn} {a : Nat} :
-  letI : NeZero n := ⟨Nat.pos_iff_ne_zero.1 hn⟩
-  Fin.Internal.ofNat n hn a = Fin.ofNat n a := rfl
-
 @[deprecated Fin.ofNat (since := "2025-05-28")]
 protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   Fin.ofNat n a

src/Init/Data/Fin/Lemmas.lean

@@ -25,12 +25,12 @@ namespace Fin
 
 @[deprecated ofNat_zero (since := "2025-05-28")] abbrev ofNat'_zero := @ofNat_zero
 
-theorem mod_def (a m : Fin n) : a % m = Fin.mk (a.val % m.val) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
+theorem mod_def (a m : Fin n) : a % m = Fin.mk (a % m) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
   rfl
 
-theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a.val * b.val) % n) (Nat.mod_lt _ a.pos) := rfl
+theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a * b) % n) (Nat.mod_lt _ a.pos) := rfl
 
-theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b.val) + a.val) % n) (Nat.mod_lt _ a.pos) := rfl
+theorem sub_def (a b : Fin n) : a - b = Fin.mk (((n - b) + a) % n) (Nat.mod_lt _ a.pos) := rfl
 
 theorem pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.pos
 
@@ -81,7 +81,7 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 
 @[deprecated ofNat_self (since := "2025-05-28")] abbrev ofNat'_self := @ofNat_self
 
-@[simp] theorem ofNat_val_eq_self [NeZero n] (x : Fin n) : (Fin.ofNat n x.val) = x := by
+@[simp] theorem ofNat_val_eq_self [NeZero n] (x : Fin n) : (Fin.ofNat n x) = x := by
   ext
   rw [val_ofNat, Nat.mod_eq_of_lt]
   exact x.2
@@ -121,6 +121,8 @@ Non-trivial loops lead to undesirable and counterintuitive elaboration behavior.
 For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
+
+Note: as of 2025-06-03, Mathlib has such a coercion for `Fin n` anyway!
 -/
 @[expose]
 def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
@@ -263,7 +265,7 @@ instance : LawfulOrderLT (Fin n) where
   lt_iff := by
     simp [← Fin.not_le, Decidable.imp_iff_not_or, Std.Total.total]
 
-@[simp, grind =] theorem val_rev (i : Fin n) : (rev i).val = n - (i + 1) := rfl
+@[simp, grind =] theorem val_rev (i : Fin n) : rev i = n - (i + 1) := rfl
 
 @[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by
   rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
@@ -498,11 +500,9 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
   ext
   simp
 
-@[simp, grind =] theorem cast_cast {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
+@[simp] theorem cast_trans {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
     (i.cast h).cast h' = i.cast (Eq.trans h h') := rfl
 
-@[deprecated cast_cast (since := "2025-09-03")] abbrev cast_trans := @cast_cast
-
 theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := rfl
 
 @[simp] theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
@@ -531,7 +531,7 @@ theorem cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
     (i.castAdd m').cast h = i.castAdd m := rfl
 
 theorem castAdd_castAdd {m n p : Nat} (i : Fin m) :
-    (i.castAdd n).castAdd p = (i.castAdd (n + p)).cast (Nat.add_assoc ..).symm := rfl
+    (i.castAdd n).castAdd p = (i.castAdd (n + p)).cast (Nat.add_assoc ..).symm  := rfl
 
 /-- The cast of the successor is the successor of the cast. See `Fin.succ_cast_eq` for rewriting in
 the reverse direction. -/

src/Init/Data/Format/Basic.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Control.State
 public import Init.Data.Int.Basic
-public import Init.Data.String.Bootstrap
+public import Init.Data.String.Basic
 
 public section
 
@@ -168,8 +168,8 @@ private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult
     else
       { foundLine := true }
   | text s,       flatten, _, _ =>
-    let p := String.Internal.posOf s '\n'
-    let off := String.Internal.offsetOfPos s p
+    let p := s.posOf '\n'
+    let off := s.offsetOfPos p
     { foundLine := p != s.endPos, foundFlattenedHardLine := flatten && p != s.endPos, space := off }
   | append f₁ f₂, flatten, m, w => merge w (spaceUptoLine f₁ flatten m w) (spaceUptoLine f₂ flatten m)
   | nest n f,     flatten, m, w => spaceUptoLine f flatten (m - n) w
@@ -263,15 +263,15 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
     | append f₁ f₂ => be w (gs' ({ i with f := f₁, activeTags := 0 }::{ i with f := f₂ }::is))
     | nest n f => be w (gs' ({ i with f, indent := i.indent + n }::is))
     | text s =>
-      let p := String.Internal.posOf s '\n'
+      let p := s.posOf '\n'
       if p == s.endPos then
         pushOutput s
         endTags i.activeTags
         be w (gs' is)
       else
-        pushOutput (String.Internal.extract s {} p)
+        pushOutput (s.extract {} p)
         pushNewline i.indent.toNat
-        let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.endPos) }::is
+        let is := { i with f := text (s.extract (s.next p) s.endPos) }::is
         -- after a hard line break, re-evaluate whether to flatten the remaining group
         -- note that we shouldn't start flattening after a hard break outside a group
         if g.fla == .disallow then
@@ -298,7 +298,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
           pushGroup FlattenBehavior.fill is gs w >>= be w
         -- if preceding fill item fit in a single line, try to fit next one too
         if g.fla.shouldFlatten then
-          let gs'@(g'::_) ← pushGroup FlattenBehavior.fill is gs (w - String.Internal.length " ")
+          let gs'@(g'::_) ← pushGroup FlattenBehavior.fill is gs (w - " ".length)
             | panic "unreachable"
           if g'.fla.shouldFlatten then
             pushOutput " "
@@ -316,7 +316,7 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
       else
         let k ← currColumn
         if k < i.indent then
-          pushOutput (String.Internal.pushn "" ' ' (i.indent - k).toNat)
+          pushOutput ("".pushn ' ' (i.indent - k).toNat)
           endTags i.activeTags
           be w (gs' is)
         else
@@ -350,7 +350,7 @@ Creates a format `l ++ f ++ r` with a flattening group, nesting the contents by
 The group's `FlattenBehavior` is `allOrNone`; for `fill` use `Std.Format.bracketFill`.
 -/
 @[inline] def bracket (l : String) (f : Format) (r : String) : Format :=
-  group (nest (String.Internal.length l) $ l ++ f ++ r)
+  group (nest l.length $ l ++ f ++ r)
 
 /--
 Creates the format `"(" ++ f ++ ")"` with a flattening group, nesting by one space.
@@ -372,7 +372,7 @@ Creates a format `l ++ f ++ r` with a flattening group, nesting the contents by
 The group's `FlattenBehavior` is `fill`; for `allOrNone` use `Std.Format.bracketFill`.
 -/
 @[inline] def bracketFill (l : String) (f : Format) (r : String) : Format :=
-  fill (nest (String.Internal.length l) $ l ++ f ++ r)
+  fill (nest l.length $ l ++ f ++ r)
 
 /-- The default indentation level, which is two spaces. -/
 def defIndent  := 2
@@ -397,8 +397,8 @@ private structure State where
 
 private instance : MonadPrettyFormat (StateM State) where
   -- We avoid a structure instance update, and write these functions using pattern matching because of issue #316
-  pushOutput s       := modify fun ⟨out, col⟩ => ⟨String.Internal.append out s, col + (String.Internal.length s)⟩
-  pushNewline indent := modify fun ⟨out, _⟩ => ⟨String.Internal.append out (String.Internal.pushn "\n" ' ' indent), indent⟩
+  pushOutput s       := modify fun ⟨out, col⟩ => ⟨out ++ s, col + s.length⟩
+  pushNewline indent := modify fun ⟨out, _⟩ => ⟨out ++ "\n".pushn ' ' indent, indent⟩
   currColumn         := return (← get).column
   startTag _         := return ()
   endTags _          := return ()

src/Init/Data/Format/Instances.lean

@@ -9,7 +9,6 @@ prelude
 public import Init.Data.Format.Basic
 public import Init.Data.Array.Basic
 public import Init.Data.ToString.Basic
-import Init.Data.String.Basic
 
 public section
 

src/Init/Data/Format/Syntax.lean

@@ -9,8 +9,6 @@ prelude
 public import Init.Data.Format.Macro
 public import Init.Data.Format.Instances
 public import Init.Meta
-import Init.Data.String.Basic
-import Init.Data.ToString.Name
 
 public section
 

src/Init/Data/Int/Basic.lean

@@ -31,7 +31,6 @@ This file defines the `Int` type as well as
 Division and modulus operations are defined in `Init.Data.Int.DivMod.Basic`.
 -/
 
-set_option genCtorIdx false in
 /--
 The integers.
 
@@ -321,8 +320,6 @@ def natAbs (m : @& Int) : Nat :=
   | ofNat m => m
   | -[m +1] => m.succ
 
-attribute [gen_constructor_elims] Int
-
 /-! ## sign -/
 
 /--

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

@@ -7,8 +7,7 @@ module
 
 prelude
 public import Init.Data.Nat.Bitwise.Lemmas
-public import Init.Data.Int.Bitwise.Basic
-import all Init.Data.Int.Bitwise.Basic
+public import all Init.Data.Int.Bitwise.Basic
 public import Init.Data.Int.DivMod.Lemmas
 
 public section
@@ -17,8 +16,8 @@ namespace Int
 
 theorem shiftRight_eq (n : Int) (s : Nat) : n >>> s = Int.shiftRight n s := rfl
 
-@[simp, norm_cast]
-theorem natCast_shiftRight (n s : Nat) : n >>> s = (n : Int) >>> s := rfl
+@[simp]
+theorem natCast_shiftRight (n s : Nat) : (n : Int) >>> s = n >>> s := rfl
 
 @[simp]
 theorem negSucc_shiftRight (m n : Nat) :
@@ -68,7 +67,7 @@ theorem shiftRight_le_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) : n >>> s ≤
     by_cases hm : m = 0
     · simp [hm]
     · have := Nat.shiftRight_le m s
-      rw [ofNat_eq_coe]
+      simp
       omega
   case _ _ _ m =>
     omega
@@ -89,14 +88,6 @@ theorem shiftRight_le_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : (n >>> s)
     have rl : n / 2 ^ s ≤ 0 := Int.ediv_nonpos_of_nonpos_of_neg (by omega) (by norm_cast at *; omega)
     norm_cast at *
 
-@[simp, norm_cast]
-theorem natCast_shiftLeft (n s : Nat) : n <<< s = (n : Int) <<< s := rfl
-
-@[simp, grind =]
-theorem zero_shiftLeft (n : Nat) : (0 : Int) <<< n = 0 := by
-  change ((0 <<< n : Nat) : Int) = 0
-  simp
-
 @[simp, grind =]
 theorem shiftLeft_zero (n : Int) : n <<< 0 = n := by
   change Int.shiftLeft _ _ = _
@@ -108,17 +99,14 @@ theorem shiftLeft_succ (m : Int) (n : Nat) : m <<< (n + 1) = (m <<< n) * 2 := by
   change Int.shiftLeft _ _ = Int.shiftLeft _ _ * 2
   match m with
   | (m : Nat) =>
-    dsimp only [Int.shiftLeft, Int.ofNat_eq_coe]
+    dsimp [Int.shiftLeft]
     rw [Nat.shiftLeft_succ, Nat.mul_comm, natCast_mul, ofNat_two]
   | Int.negSucc m =>
-    dsimp only [Int.shiftLeft]
+    dsimp [Int.shiftLeft]
     rw [Nat.shiftLeft_succ, Nat.mul_comm, Int.negSucc_eq]
     have := Nat.le_shiftLeft (a := m + 1) (b := n)
     omega
 
-theorem shiftLeft_succ' (m : Int) (n : Nat) : m <<< (n + 1) = 2 * (m <<< n) := by
-  rw [shiftLeft_succ, Int.mul_comm]
-
 theorem shiftLeft_eq (a : Int) (b : Nat) : a <<< b = a * 2 ^ b := by
   induction b with
   | zero => simp
@@ -128,55 +116,4 @@ theorem shiftLeft_eq (a : Int) (b : Nat) : a <<< b = a * 2 ^ b := by
 theorem shiftLeft_eq' (a : Int) (b : Nat) : a <<< b = a * (2 ^ b : Nat) := by
   simp [shiftLeft_eq]
 
-theorem shiftLeft_add (a : Int) (b c : Nat) : a <<< (b + c) = a <<< b <<< c := by
-  simp [shiftLeft_eq, Int.pow_add, Int.mul_assoc]
-
-@[simp]
-theorem shiftLeft_shiftRight_cancel (a : Int) (b : Nat) : a <<< b >>> b = a := by
-  simp [shiftLeft_eq, shiftRight_eq_div_pow, mul_ediv_cancel _ (NeZero.ne _)]
-
-theorem shiftLeft_shiftRight_eq_shiftLeft_of_le {b c : Nat} (h : c ≤ b) (a : Int) :
-    a <<< b >>> c = a <<< (b - c) := by
-  obtain ⟨b, rfl⟩ := h.dest
-  simp [shiftLeft_eq, Int.pow_add, shiftRight_eq_div_pow, Int.mul_left_comm a,
-    Int.mul_ediv_cancel_left _ (NeZero.ne _)]
-
-theorem shiftLeft_shiftRight_eq_shiftRight_of_le {b c : Nat} (h : b ≤ c) (a : Int) :
-    a <<< b >>> c = a >>> (c - b) := by
-  obtain ⟨c, rfl⟩ := h.dest
-  simp [shiftRight_add]
-
-theorem shiftLeft_shiftRight_eq (a : Int) (b c : Nat) :
-    a <<< b >>> c = a <<< (b - c) >>> (c - b) := by
-  rcases Nat.le_total b c with h | h
-  · simp [shiftLeft_shiftRight_eq_shiftRight_of_le h, Nat.sub_eq_zero_of_le h]
-  · simp [shiftLeft_shiftRight_eq_shiftLeft_of_le h, Nat.sub_eq_zero_of_le h]
-
-@[simp]
-theorem shiftRight_shiftLeft_cancel {a : Int} {b : Nat} (h : 2 ^ b ∣ a) : a >>> b <<< b = a := by
-  simp [shiftLeft_eq, shiftRight_eq_div_pow, Int.ediv_mul_cancel h]
-
-theorem add_shiftLeft (a b : Int) (n : Nat) : (a + b) <<< n = a <<< n + b <<< n := by
-  simp [shiftLeft_eq, Int.add_mul]
-
-theorem neg_shiftLeft (a : Int) (n : Nat) : (-a) <<< n = -a <<< n := by
-  simp [Int.shiftLeft_eq, Int.neg_mul]
-
-theorem shiftLeft_mul (a b : Int) (n : Nat) : a <<< n * b = (a * b) <<< n := by
-  simp [shiftLeft_eq, Int.mul_right_comm]
-
-theorem mul_shiftLeft (a b : Int) (n : Nat) : a * b <<< n = (a * b) <<< n := by
-  simp [shiftLeft_eq, Int.mul_assoc]
-
-theorem shiftLeft_mul_shiftLeft (a b : Int) (m n : Nat) :
-    a <<< m * b <<< n = (a * b) <<< (m + n) := by
-  simp [shiftLeft_mul, mul_shiftLeft, shiftLeft_add]
-
-@[simp]
-theorem shiftLeft_eq_zero_iff {a : Int} {n : Nat} : a <<< n = 0 ↔ a = 0 := by
-  simp [shiftLeft_eq, Int.mul_eq_zero, NeZero.ne]
-
-instance {a : Int} {n : Nat} [NeZero a] : NeZero (a <<< n) :=
-  ⟨mt shiftLeft_eq_zero_iff.mp (NeZero.ne _)⟩
-
 end Int

src/Init/Data/Int/Compare.lean

@@ -6,8 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert
 module
 
 prelude
-public import Init.Data.Ord.Basic
-import all Init.Data.Ord.Basic
+public import all Init.Data.Ord.Basic
 public import Init.Data.Int.Order
 
 public section

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

@@ -97,7 +97,7 @@ theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := natCast_emod m n
 
 /-! ### mod definitions -/
 
-theorem emod_add_mul_ediv : ∀ a b : Int, a % b + b * (a / b) = a
+theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
   | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
   | ofNat m, -[n+1] => by
     change (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
@@ -111,35 +111,19 @@ 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 ..)
 
-@[deprecated emod_add_mul_ediv (since := "2025-09-01")]
-def emod_add_ediv := @emod_add_mul_ediv
+/-- 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 emod_add_ediv_mul (a b : Int) : a % b + a / b * b = a := by
-  rw [Int.mul_comm]; exact emod_add_mul_ediv ..
+theorem ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
+  rw [Int.add_comm]; exact emod_add_ediv ..
 
-@[deprecated emod_add_ediv_mul (since := "2025-09-01")]
-def emod_add_ediv' := @emod_add_ediv_mul
-
-theorem mul_ediv_add_emod (a b : Int) : b * (a / b) + a % b = a := by
-  rw [Int.add_comm]; exact emod_add_mul_ediv ..
-
-@[deprecated mul_ediv_add_emod (since := "2025-09-01")]
-def ediv_add_emod := @mul_ediv_add_emod
-
-theorem ediv_mul_add_emod (a b : Int) : a / b * b + a % b = a := by
-  rw [Int.mul_comm]; exact mul_ediv_add_emod ..
-
-@[deprecated ediv_mul_add_emod (since := "2025-09-01")]
-def ediv_add_emod' := @ediv_mul_add_emod
+/-- 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_mul_ediv]
-
-theorem mul_ediv_self (a b : Int) : b * (a / b) = a - a % b := by
-  rw [emod_def, Int.sub_sub_self]
-
-theorem ediv_mul_self (a b : Int) : a / b * b = a - a % b := by
-  rw [Int.mul_comm, emod_def, Int.sub_sub_self]
+  rw [← Int.add_sub_cancel (a % b), emod_add_ediv]
 
 /-! ### `/` ediv -/
 
@@ -242,7 +226,7 @@ theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
 
 @[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
   have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
-  rwa [Int.add_right_comm, emod_add_mul_ediv] at this
+  rwa [Int.add_right_comm, emod_add_ediv] at this
 
 @[simp] theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k := by
   rw [Int.add_comm, emod_add_emod, Int.add_comm]
@@ -268,7 +252,7 @@ theorem emod_add_cancel_right {m n k : Int} (i) : (m + i) % n = (k + i) % n ↔
 
 theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
   conv => lhs; rw [
-    ← emod_add_mul_ediv a n, ← emod_add_ediv_mul b n, Int.add_mul, Int.mul_add, Int.mul_add,
+    ← emod_add_ediv a n, ← emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
     Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
     ← Int.mul_assoc, add_mul_emod_self_right]
 
@@ -277,7 +261,7 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
 
 @[simp] theorem emod_emod_of_dvd (n : Int) {m k : Int}
     (h : m ∣ k) : (n % k) % m = n % m := by
-  conv => rhs; rw [← emod_add_mul_ediv n k]
+  conv => rhs; rw [← emod_add_ediv n k]
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]
 
@@ -291,7 +275,7 @@ theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
 /-! ### properties of `/` and `%` -/
 
 theorem mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : b * (a / b) = a := by
-  have := emod_add_mul_ediv a b; rwa [H, Int.zero_add] at this
+  have := emod_add_ediv a b; rwa [H, Int.zero_add] at this
 
 theorem ediv_mul_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : a / b * b = a := by
   rw [Int.mul_comm, mul_ediv_cancel_of_emod_eq_zero H]
@@ -342,11 +326,11 @@ theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a :
 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                   := mul_ediv_add_emod _ _
+    _ = 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 := (mul_ediv_add_emod _ _).symm
+    _ = 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 -/

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

@@ -26,10 +26,6 @@ namespace Int
 
 @[simp high] theorem natCast_eq_zero {n : Nat} : (n : Int) = 0 ↔ n = 0 := by omega
 
-instance {n : Nat} [NeZero n] : NeZero (n : Int) := ⟨mt Int.natCast_eq_zero.mp (NeZero.ne _)⟩
-instance {n : Nat} [NeZero n] : NeZero (no_index (OfNat.ofNat n) : Int) :=
-  ⟨mt Int.natCast_eq_zero.mp (NeZero.ne _)⟩
-
 protected theorem exists_add_of_le {a b : Int} (h : a ≤ b) : ∃ (c : Nat), b = a + c :=
   ⟨(b - a).toNat, by omega⟩
 
@@ -334,7 +330,7 @@ theorem fdiv_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.fdiv b = a / b := by
 
 /-! ### mod definitions -/
 
-theorem tmod_add_mul_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
+theorem tmod_add_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
   | ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
   | ofNat m, -[n+1] => by
     change (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
@@ -351,37 +347,21 @@ theorem tmod_add_mul_tdiv : ∀ a b : Int, tmod a b + b * (a.tdiv b) = a
     rw [Int.neg_mul, ← Int.neg_add]
     exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
 
-@[deprecated tmod_add_mul_tdiv (since := "2025-09-01")]
-def tmod_add_tdiv := @tmod_add_mul_tdiv
+theorem tdiv_add_tmod (a b : Int) : b * a.tdiv b + tmod a b = a := by
+  rw [Int.add_comm]; apply tmod_add_tdiv ..
 
-theorem mul_tdiv_add_tmod (a b : Int) : b * a.tdiv b + tmod a b = a := by
-  rw [Int.add_comm]; apply tmod_add_mul_tdiv ..
+/-- Variant of `tmod_add_tdiv` with the multiplication written the other way around. -/
+theorem tmod_add_tdiv' (m k : Int) : tmod m k + m.tdiv k * k = m := by
+  rw [Int.mul_comm]; apply tmod_add_tdiv
 
-@[deprecated mul_tdiv_add_tmod (since := "2025-09-01")]
-def tdiv_add_tmod := @mul_tdiv_add_tmod
-
-theorem tmod_add_tdiv_mul (m k : Int) : tmod m k + m.tdiv k * k = m := by
-  rw [Int.mul_comm]; apply tmod_add_mul_tdiv
-
-@[deprecated tmod_add_tdiv_mul (since := "2025-09-01")]
-def tmod_add_tdiv' := @tmod_add_mul_tdiv
-
-theorem tdiv_mul_add_tmod (m k : Int) : m.tdiv k * k + tmod m k = m := by
-  rw [Int.mul_comm]; apply mul_tdiv_add_tmod
-
-@[deprecated tdiv_mul_add_tmod (since := "2025-09-01")]
-def tdiv_add_tmod' := @tdiv_mul_add_tmod
+/-- Variant of `tdiv_add_tmod` with the multiplication written the other way around. -/
+theorem tdiv_add_tmod' (m k : Int) : m.tdiv k * k + tmod m k = m := by
+  rw [Int.mul_comm]; apply tdiv_add_tmod
 
 theorem tmod_def (a b : Int) : tmod a b = a - b * a.tdiv b := by
-  rw [← Int.add_sub_cancel (tmod a b), tmod_add_mul_tdiv]
+  rw [← Int.add_sub_cancel (tmod a b), tmod_add_tdiv]
 
-theorem mul_tdiv_self (a b : Int) : b * (a.tdiv b) = a - a.tmod b := by
-  rw [tmod_def, Int.sub_sub_self]
-
-theorem tdiv_mul_self (a b : Int) : a.tdiv b * b = a - a.tmod b := by
-  rw [Int.mul_comm, tmod_def, Int.sub_sub_self]
-
-theorem fmod_add_mul_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
+theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
   | 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
   | succ _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
   | succ m, -[n+1] => by
@@ -398,35 +378,19 @@ theorem fmod_add_mul_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
     change -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
     rw [← Int.neg_add]; exact congrArg (-ofNat ·) <| Nat.mod_add_div ..
 
-@[deprecated fmod_add_mul_fdiv (since := "2025-09-01")]
-def fmod_add_fdiv := @fmod_add_mul_fdiv
+/-- Variant of `fmod_add_fdiv` with the multiplication written the other way around. -/
+theorem fmod_add_fdiv' (a b : Int) : a.fmod b + (a.fdiv b) * b = a := by
+  rw [Int.mul_comm]; exact fmod_add_fdiv ..
 
-theorem fmod_add_fdiv_mul (a b : Int) : a.fmod b + (a.fdiv b) * b = a := by
-  rw [Int.mul_comm]; exact fmod_add_mul_fdiv ..
+theorem fdiv_add_fmod (a b : Int) : b * a.fdiv b + a.fmod b = a := by
+  rw [Int.add_comm]; exact fmod_add_fdiv ..
 
-@[deprecated fmod_add_fdiv_mul (since := "2025-09-01")]
-def fmod_add_fdiv' := @fmod_add_fdiv_mul
-
-theorem mul_fdiv_add_fmod (a b : Int) : b * a.fdiv b + a.fmod b = a := by
-  rw [Int.add_comm]; exact fmod_add_mul_fdiv ..
-
-@[deprecated mul_fdiv_add_fmod (since := "2025-09-01")]
-def fdiv_add_fmod := @mul_fdiv_add_fmod
-
-theorem fdiv_mul_add_fmod (a b : Int) : (a.fdiv b) * b + a.fmod b = a := by
-  rw [Int.mul_comm]; exact mul_fdiv_add_fmod ..
-
-@[deprecated mul_fdiv_add_fmod (since := "2025-09-01")]
-def fdiv_add_fmod' := @mul_fdiv_add_fmod
+/-- Variant of `fdiv_add_fmod` with the multiplication written the other way around. -/
+theorem fdiv_add_fmod' (a b : Int) : (a.fdiv b) * b + a.fmod b = a := by
+  rw [Int.mul_comm]; exact fdiv_add_fmod ..
 
 theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
-  rw [← Int.add_sub_cancel (a.fmod b), fmod_add_mul_fdiv]
-
-theorem mul_fdiv_self (a b : Int) : b * (a.fdiv b) = a - a.fmod b := by
-  rw [fmod_def, Int.sub_sub_self]
-
-theorem fdiv_mul_self (a b : Int) : a.fdiv b * b = a - a.fmod b := by
-  rw [Int.mul_comm, fmod_def, Int.sub_sub_self]
+  rw [← Int.add_sub_cancel (a.fmod b), fmod_add_fdiv]
 
 /-! ### mod equivalences  -/
 
@@ -805,7 +769,7 @@ protected theorem ediv_emod_unique {a b r q : Int} (h : 0 < b) :
     a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b := by
   constructor
   · intro ⟨rfl, rfl⟩
-    exact ⟨emod_add_mul_ediv a b, emod_nonneg _ (Int.ne_of_gt h), emod_lt_of_pos _ h⟩
+    exact ⟨emod_add_ediv a b, emod_nonneg _ (Int.ne_of_gt h), emod_lt_of_pos _ h⟩
   · intro ⟨rfl, hz, hb⟩
     constructor
     · rw [Int.add_mul_ediv_left r q (Int.ne_of_gt h), ediv_eq_zero_of_lt hz hb]
@@ -829,7 +793,7 @@ theorem neg_ediv {a b : Int} : (-a) / b = -(a / b) - if b ∣ a then 0 else b.si
   if hb : b = 0 then
     simp [hb]
   else
-    conv => lhs; rw [← mul_ediv_add_emod a b]
+    conv => lhs; rw [← ediv_add_emod a b]
     rw [Int.neg_add, ← Int.mul_neg, mul_add_ediv_left _ _ hb, Int.add_comm]
     split <;> rename_i h
     · rw [emod_eq_zero_of_dvd h]
@@ -1119,10 +1083,6 @@ theorem emod_natAbs_of_neg {x : Int} (h : x < 0) {n : Nat} (w : n ≠ 0) :
 protected theorem ediv_mul_le (a : Int) {b : Int} (H : b ≠ 0) : a / b * b ≤ a :=
   Int.le_of_sub_nonneg <| by rw [Int.mul_comm, ← emod_def]; apply emod_nonneg _ H
 
-protected theorem lt_ediv_mul (a : Int) {b : Int} (H : 0 < b) : a - b < a / b * b := by
-  rw [ediv_mul_self, Int.sub_lt_sub_left_iff]
-  exact emod_lt_of_pos a H
-
 theorem le_of_mul_le_mul_left {a b c : Int} (w : a * b ≤ a * c) (h : 0 < a) : b ≤ c := by
   have w := Int.sub_nonneg_of_le w
   rw [← Int.mul_sub] at w
@@ -1213,9 +1173,9 @@ theorem ediv_eq_iff_of_pos {k x y : Int} (h : 0 < k) : x / k = y ↔ y * k ≤ x
 theorem add_ediv_of_pos {a b c : Int} (h : 0 < c) :
     (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0 := by
   have h' : c ≠ 0 := by omega
-  conv => lhs; rw [← Int.mul_ediv_add_emod a c]
+  conv => lhs; rw [← Int.ediv_add_emod a c]
   rw [Int.add_assoc, Int.mul_add_ediv_left _ _ h']
-  conv => lhs; rw [← Int.mul_ediv_add_emod b c]
+  conv => lhs; rw [← Int.ediv_add_emod b c]
   rw [Int.add_comm (a % c), Int.add_assoc, Int.mul_add_ediv_left _ _ h',
     ← Int.add_assoc, Int.add_comm (b % c)]
   congr
@@ -1246,7 +1206,7 @@ theorem not_dvd_iff_lt_mul_succ (m : Int) (hn : 0 < n) :
     ¬n ∣ m ↔ (∃ k, n * k < m ∧ m < n * (k + 1)) := by
   refine ⟨fun h ↦ ?_, ?_⟩
   · rw [dvd_iff_emod_eq_zero, ← Ne] at h
-    rw [← emod_add_mul_ediv m n]
+    rw [← emod_add_ediv m n]
     refine ⟨m / n, Int.lt_add_of_pos_left _ ?_, ?_⟩
     · have := emod_nonneg m (Int.ne_of_gt hn)
       omega
@@ -1258,26 +1218,6 @@ theorem not_dvd_iff_lt_mul_succ (m : Int) (hn : 0 < n) :
     rw [Int.lt_add_one_iff, ← Int.not_lt] at h2k
     exact h2k h1k
 
-private theorem ediv_ediv_of_pos {x y z : Int} (hy : 0 < y) (hz : 0 < z) :
-    x / y / z = x / (y * z) := by
-  rw [eq_comm, Int.ediv_eq_iff_of_pos (Int.mul_pos hy hz)]
-  constructor
-  · rw [Int.mul_comm y, ← Int.mul_assoc]
-    exact Int.le_trans
-      (Int.mul_le_mul_of_nonneg_right (Int.ediv_mul_le _ (Int.ne_of_gt hz)) (Int.le_of_lt hy))
-      (Int.ediv_mul_le x (Int.ne_of_gt hy))
-  · rw [Int.mul_comm y, ← Int.mul_assoc, ← Int.add_mul, Int.mul_comm _ z]
-    exact Int.lt_mul_of_ediv_lt hy (Int.lt_mul_ediv_self_add hz)
-
-theorem ediv_ediv {x y z : Int} (hy : 0 ≤ y) : x / y / z = x / (y * z) := by
-  rcases y with (_ | a) | a
-  · simp
-  · rcases z with (_ | b) | b
-    · simp
-    · simp [ediv_ediv_of_pos]
-    · simp [Int.negSucc_eq, Int.mul_neg, ediv_ediv_of_pos]
-  · simp at hy
-
 /-! ### tdiv -/
 
 -- `tdiv` analogues of `ediv` lemmas from `Bootstrap.lean`
@@ -1521,7 +1461,7 @@ theorem sign_tmod (a b : Int) : sign (tmod a b) = if b ∣ a then 0 else sign a
 -- Analogues of statements about `ediv` and `emod` from `Bootstrap.lean`
 
 theorem mul_tdiv_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : b * (a.tdiv b) = a := by
-  have := tmod_add_mul_tdiv a b; rwa [H, Int.zero_add] at this
+  have := tmod_add_tdiv a b; rwa [H, Int.zero_add] at this
 
 theorem tdiv_mul_cancel_of_tmod_eq_zero {a b : Int} (H : a.tmod b = 0) : a.tdiv b * b = a := by
   rw [Int.mul_comm, mul_tdiv_cancel_of_tmod_eq_zero H]
@@ -2246,7 +2186,7 @@ theorem fmod_add_cancel_right {m n k : Int} (i) : (m + i).fmod n = (k + i).fmod
 
 theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n := by
   conv => lhs; rw [
-    ← fmod_add_mul_fdiv a n, ← fmod_add_fdiv_mul b n, Int.add_mul, Int.mul_add, Int.mul_add,
+    ← fmod_add_fdiv a n, ← fmod_add_fdiv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
     Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_fmod_self_left,
     ← Int.mul_assoc, add_mul_fmod_self_right]
 
@@ -2255,7 +2195,7 @@ theorem mul_fmod (a b n : Int) : (a * b).fmod n = (a.fmod n * b.fmod n).fmod n :
 
 @[simp] theorem fmod_fmod_of_dvd (n : Int) {m k : Int}
     (h : m ∣ k) : (n.fmod k).fmod m = n.fmod m := by
-  conv => rhs; rw [← fmod_add_mul_fdiv n k]
+  conv => rhs; rw [← fmod_add_fdiv n k]
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_fmod_self_left]
 
@@ -2285,7 +2225,7 @@ theorem fmod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.fmod b = a :=
 -- Analogues of properties of `ediv` and `emod` from `Bootstrap.lean`
 
 theorem mul_fdiv_cancel_of_fmod_eq_zero {a b : Int} (H : a.fmod b = 0) : b * (a.fdiv b) = a := by
-  have := fmod_add_mul_fdiv a b; rwa [H, Int.zero_add] at this
+  have := fmod_add_fdiv a b; rwa [H, Int.zero_add] at this
 
 theorem fdiv_mul_cancel_of_fmod_eq_zero {a b : Int} (H : a.fmod b = 0) : (a.fdiv b) * b= a := by
   rw [Int.mul_comm, mul_fdiv_cancel_of_fmod_eq_zero H]
@@ -2527,9 +2467,9 @@ theorem bdiv_add_bmod (x : Int) (m : Nat) : m * bdiv x m + bmod x m = x := by
       ite_self]
   · dsimp only
     split
-    · exact mul_ediv_add_emod x m
+    · exact ediv_add_emod x m
     · rw [Int.mul_add, Int.mul_one, Int.add_assoc, Int.add_comm m, Int.sub_add_cancel]
-      exact mul_ediv_add_emod x m
+      exact ediv_add_emod x m
 
 theorem bmod_add_bdiv (x : Int) (m : Nat) : bmod x m + m * bdiv x m = x := by
   rw [Int.add_comm]; exact bdiv_add_bmod x m
@@ -2786,7 +2726,7 @@ theorem le_bmod {x : Int} {m : Nat} (h : 0 < m) : - (m/2) ≤ Int.bmod x m := by
     · exact Int.ne_of_gt (natCast_pos.mpr h)
   · simp [Int.not_lt] at w
     refine Int.le_trans ?_ (Int.sub_le_sub_right w _)
-    rw [← mul_ediv_add_emod m 2]
+    rw [← ediv_add_emod m 2]
     generalize (m : Int) / 2 = q
     generalize h : (m : Int) % 2 = r at *
     rcases v with rfl | rfl
@@ -2947,7 +2887,7 @@ theorem neg_bmod {a : Int} {b : Nat} :
           simp only [gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_left, Int.natCast_mul,
             cast_ofNat_Int, Int.not_lt] at *
           rw [Int.mul_dvd_mul_iff_left (by omega)]
-          have := mul_ediv_add_emod a (2 * c)
+          have := ediv_add_emod a (2 * c)
           rw [(by omega : a % (2 * c) = c)] at this
           rw [← this]
           apply Int.dvd_add _ (by simp)

src/Init/Data/Int/Lemmas.lean

@@ -40,7 +40,7 @@ theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
 
 theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
 theorem neg_ofNat_succ (n : Nat) : -(succ n : Int) = -[n+1] := rfl
-@[simp] theorem neg_negSucc (n : Nat) : -(-[n+1]) = ((n + 1 : Nat) : Int) := rfl
+theorem neg_negSucc (n : Nat) : -(-[n+1]) = succ n := rfl
 
 theorem negOfNat_eq : negOfNat n = -ofNat n := rfl
 
@@ -566,9 +566,6 @@ protected theorem mul_eq_zero {a b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
 protected theorem mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 :=
   Or.rec a0 b0 ∘ Int.mul_eq_zero.mp
 
-instance {a b : Int} [NeZero a] [NeZero b] : NeZero (a * b) :=
-  ⟨Int.mul_ne_zero (NeZero.ne _) (NeZero.ne _)⟩
-
 @[simp] protected theorem mul_ne_zero_iff {a b : Int} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by
   rw [ne_eq, Int.mul_eq_zero, not_or, ne_eq]
 

src/Init/Data/Int/Linear.lean

@@ -12,11 +12,9 @@ public import Init.Data.Int.Lemmas
 public import Init.Data.Int.LemmasAux
 public import Init.Data.Int.DivMod.Bootstrap
 public import Init.Data.Int.Cooper
-public import Init.Data.Int.Gcd
-import all Init.Data.Int.Gcd
+public import all Init.Data.Int.Gcd
 public import Init.Data.RArray
-public import Init.Data.AC
-import all Init.Data.AC
+public import all Init.Data.AC
 
 public section
 
@@ -39,7 +37,7 @@ inductive Expr where
   | neg (a : Expr)
   | mulL (k : Int) (a : Expr)
   | mulR (a : Expr) (k : Int)
-  deriving Inhabited, @[expose] BEq
+  deriving Inhabited, BEq
 
 @[expose]
 def Expr.denote (ctx : Context) : Expr → Int
@@ -54,7 +52,7 @@ def Expr.denote (ctx : Context) : Expr → Int
 inductive Poly where
   | num (k : Int)
   | add (k : Int) (v : Var) (p : Poly)
-  deriving @[expose] BEq
+  deriving BEq
 
 @[expose]
 protected noncomputable def Poly.beq' (p₁ : Poly) : Poly → Bool :=
@@ -247,7 +245,7 @@ def cmod (a b : Int) : Int :=
 
 theorem cdiv_add_cmod (a b : Int) : b*(cdiv a b) + cmod a b = a := by
   unfold cdiv cmod
-  have := Int.mul_ediv_add_emod (-a) b
+  have := Int.ediv_add_emod (-a) b
   have := congrArg (Neg.neg) this
   simp at this
   conv => rhs; rw[← this]
@@ -272,7 +270,7 @@ private abbrev div_mul_cancel_of_mod_zero :=
 theorem cdiv_eq_div_of_divides {a b : Int} (h : a % b = 0) : a/b = cdiv a b := by
   replace h := div_mul_cancel_of_mod_zero h
   have hz : a % b = 0 := by
-    have := Int.mul_ediv_add_emod a b
+    have := Int.ediv_add_emod a b
     conv at this => rhs; rw [← Int.add_zero a]
     rw [Int.mul_comm, h] at this
     exact Int.add_left_cancel this
@@ -379,11 +377,8 @@ def Poly.mul (p : Poly) (k : Int) : Poly :=
       p₁)
     fuel
 
-@[expose] noncomputable def Poly.combine_mul_k (a b : Int) (p₁ p₂ : Poly) : Poly :=
-  Bool.rec
-    (Bool.rec (combine_mul_k' hugeFuel a b p₁ p₂) (p₁.mul_k a) (Int.beq' b 0))
-    (p₂.mul_k b)
-    (Int.beq' a 0)
+@[expose] noncomputable def Poly.combine_mul_k (a b : Int) : Poly → Poly → Poly :=
+  combine_mul_k' hugeFuel a b
 
 @[simp] theorem Poly.denote_mul (ctx : Context) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
   simp [mul]
@@ -427,36 +422,34 @@ theorem Poly.denote_combine (ctx : Context) (p₁ p₂ : Poly) : (p₁.combine p
 
 theorem Poly.denote_combine_mul_k (ctx : Context) (a b : Int) (p₁ p₂ : Poly) : (p₁.combine_mul_k a b p₂).denote ctx = a * p₁.denote ctx + b * p₂.denote ctx := by
   unfold combine_mul_k
-  cases h₁ : Int.beq' a 0 <;> simp at h₁ <;> simp [*]
-  cases h₂ : Int.beq' b 0 <;> simp at h₂ <;> simp [*]
   generalize hugeFuel = fuel
   induction fuel generalizing p₁ p₂
   next => show ((p₁.mul a).append (p₂.mul b)).denote ctx = _; simp
   next fuel ih =>
-  cases p₁ <;> cases p₂ <;> simp [combine_mul_k']
-  next k₁ k₂ v₂ p₂ =>
-    show _ + (combine_mul_k' fuel a b (.num k₁) p₂).denote ctx = _
-    simp [ih, Int.mul_assoc]
-  next k₁ v₁ p₁ k₂ =>
-    show _ + (combine_mul_k' fuel a b p₁ (.num k₂)).denote ctx = _
-    simp [ih, Int.mul_assoc]
-  next k₁ v₁ p₁ k₂ v₂ p₂ =>
-    cases h₁ : Nat.beq v₁ v₂ <;> simp
-    next =>
-      cases h₂ : Nat.blt v₂ v₁ <;> simp
-      next =>
-        show _ + (combine_mul_k' fuel a b (add k₁ v₁ p₁) p₂).denote ctx = _
-        simp [ih, Int.mul_assoc]
-      next =>
-        show _ + (combine_mul_k' fuel a b p₁ (add k₂ v₂ p₂)).denote ctx = _
-        simp [ih, Int.mul_assoc]
-    next =>
-      simp at h₁; subst v₂
-      cases h₂ : (a * k₁ + b * k₂).beq' 0 <;> simp
-      next =>
+   cases p₁ <;> cases p₂ <;> simp [combine_mul_k']
+   next k₁ k₂ v₂ p₂ =>
+     show _ + (combine_mul_k' fuel a b (.num k₁) p₂).denote ctx = _
+     simp [ih, Int.mul_assoc]
+   next k₁ v₁ p₁ k₂ =>
+     show _ + (combine_mul_k' fuel a b p₁ (.num k₂)).denote ctx = _
+     simp [ih, Int.mul_assoc]
+   next k₁ v₁ p₁ k₂ v₂ p₂ =>
+     cases h₁ : Nat.beq v₁ v₂ <;> simp
+     next =>
+       cases h₂ : Nat.blt v₂ v₁ <;> simp
+       next =>
+         show _ + (combine_mul_k' fuel a b (add k₁ v₁ p₁) p₂).denote ctx = _
+         simp [ih, Int.mul_assoc]
+       next =>
+         show _ + (combine_mul_k' fuel a b p₁ (add k₂ v₂ p₂)).denote ctx = _
+         simp [ih, Int.mul_assoc]
+     next =>
+       simp at h₁; subst v₂
+       cases h₂ : (a * k₁ + b * k₂).beq' 0 <;> simp
+       next =>
         show a * k₁ * v₁.denote ctx + (b * k₂ * v₁.denote ctx + (combine_mul_k' fuel a b p₁ p₂).denote ctx) = _
         simp [ih, Int.mul_assoc]
-      next =>
+       next =>
         simp at h₂
         show (combine_mul_k' fuel a b p₁ p₂).denote ctx = _
         simp [ih, ← Int.mul_assoc, ← Int.add_mul, h₂]
@@ -1758,7 +1751,7 @@ theorem cooper_right_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b :
   intros; subst b p'; simp; assumption
 
 private theorem one_emod_eq_one {a : Int} (h : a > 1) : 1 % a = 1 := by
-  have aux₁ := Int.mul_ediv_add_emod 1 a
+  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
@@ -1785,7 +1778,7 @@ private theorem ex_of_dvd {α β a b d x : Int}
     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.mul_ediv_add_emod x d]
+    conv => lhs; rw [← Int.ediv_add_emod x d]
     rw [Int.mul_comm, this]
   exists x / d
 
@@ -1868,7 +1861,7 @@ theorem cooper_unsat (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (α β :
   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.mul_ediv_add_emod x y, Int.add_comm]
+  rw [Int.add_assoc, Int.ediv_add_emod x y, Int.add_comm]
   simp
   rw [Int.add_neg_eq_sub, Int.sub_self]
 
@@ -2203,9 +2196,6 @@ theorem mod_eq (a b k : Int) (h : b = k) : a % b = a % k := by simp [*]
 theorem div_eq' (a b b' k : Int) (h₁ : b = b') (h₂ : k == a/b') : a / b = k := by simp_all
 theorem mod_eq' (a b b' k : Int) (h₁ : b = b') (h₂ : k == a%b') : a % b = k := by simp_all
 
-theorem pow_eq (a : Int) (b : Nat) (a' b' k : Int) (h₁ : a = a') (h₂ : ↑b = b') (h₃ : k == a'^b'.toNat) : a^b = k := by
-  simp [← h₁, ← h₂] at h₃; simp [h₃]
-
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by

src/Init/Data/Int/Order.lean

@@ -701,13 +701,10 @@ theorem toNat_sub_toNat_neg : ∀ n : Int, ↑n.toNat - ↑(-n).toNat = n
   | (_+1:Nat) => Nat.add_zero _
   | -[_+1] => Nat.zero_add _
 
-@[simp] theorem toNat_neg_natCast : ∀ n : Nat, (-(n : Int)).toNat = 0
+@[simp] theorem toNat_neg_nat : ∀ n : Nat, (-(n : Int)).toNat = 0
   | 0 => rfl
   | _+1 => rfl
 
-@[deprecated toNat_neg_natCast (since := "2025-08-29")]
-theorem toNat_neg_nat : ∀ n : Nat, (-(n : Int)).toNat = 0 := toNat_neg_natCast
-
 /-! ### toNat? -/
 
 theorem mem_toNat? : ∀ {a : Int} {n : Nat}, toNat? a = some n ↔ a = n

src/Init/Data/Int/Pow.lean

@@ -48,8 +48,6 @@ protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := b
   | zero => simp
   | succ m ih => exact fun h => Int.mul_ne_zero (ih h) h
 
-instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := ⟨Int.pow_ne_zero (NeZero.ne _)⟩
-
 @[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
 abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
 

src/Init/Data/Iterators/Lemmas/Combinators/Attach.lean

@@ -6,10 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Combinators.Attach
-import all Init.Data.Iterators.Combinators.Attach
-public import Init.Data.Iterators.Combinators.Monadic.Attach
-import all Init.Data.Iterators.Combinators.Monadic.Attach
+public import all Init.Data.Iterators.Combinators.Attach
+public import all Init.Data.Iterators.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
 public import Init.Data.Array.Attach

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Attach.lean

@@ -6,8 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Combinators.Monadic.Attach
-import all Init.Data.Iterators.Combinators.Monadic.Attach
+public import all Init.Data.Iterators.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 
 public section

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean

@@ -9,8 +9,7 @@ prelude
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic
-public import Init.Data.Iterators.Consumers.Monadic.Collect
-import all Init.Data.Iterators.Consumers.Monadic.Collect
+public import all Init.Data.Iterators.Consumers.Monadic.Collect
 
 public section
 

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.lean

@@ -6,8 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Combinators.Monadic.ULift
-import all Init.Data.Iterators.Combinators.Monadic.ULift
+public import all Init.Data.Iterators.Combinators.Monadic.ULift
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
 
 public section

src/Init/Data/Iterators/Lemmas/Combinators/ULift.lean

@@ -6,8 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Combinators.ULift
-import all Init.Data.Iterators.Combinators.ULift
+public import all Init.Data.Iterators.Combinators.ULift
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
 

src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean

@@ -8,10 +8,8 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Basic
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
-public import Init.Data.Iterators.Consumers.Access
-import all Init.Data.Iterators.Consumers.Access
-public import Init.Data.Iterators.Consumers.Collect
-import all Init.Data.Iterators.Consumers.Collect
+public import all Init.Data.Iterators.Consumers.Access
+public import all Init.Data.Iterators.Consumers.Collect
 
 public section
 

src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean

@@ -8,12 +8,9 @@ module
 prelude
 public import Init.Control.Lawful.MonadLift.Instances
 public import Init.Data.Iterators.Lemmas.Consumers.Collect
-public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
-import all Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
-public import Init.Data.Iterators.Consumers.Loop
-import all Init.Data.Iterators.Consumers.Loop
-public import Init.Data.Iterators.Consumers.Monadic.Collect
-import all Init.Data.Iterators.Consumers.Monadic.Collect
+public import all Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
+public import all Init.Data.Iterators.Consumers.Loop
+public import all Init.Data.Iterators.Consumers.Monadic.Collect
 
 public section
 

src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean

@@ -8,8 +8,7 @@ module
 prelude
 public import Init.Data.Array.Lemmas
 public import Init.Data.Iterators.Lemmas.Monadic.Basic
-public import Init.Data.Iterators.Consumers.Monadic.Collect
-import all Init.Data.Iterators.Consumers.Monadic.Collect
+public import all Init.Data.Iterators.Consumers.Monadic.Collect
 
 public section
 

src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean

@@ -7,8 +7,7 @@ module
 
 prelude
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
-public import Init.Data.Iterators.Consumers.Monadic.Loop
-import all Init.Data.Iterators.Consumers.Monadic.Loop
+public import all Init.Data.Iterators.Consumers.Monadic.Loop
 
 public section
 

src/Init/Data/List/Attach.lean

@@ -6,8 +6,7 @@ Authors: Mario Carneiro
 module
 
 prelude
-public import Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
-import all Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
+public import all Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
 public import Init.Data.List.Count
 public import Init.Data.Subtype.Basic
 public import Init.BinderNameHint

src/Init/Data/List/FinRange.lean

@@ -6,8 +6,7 @@ Authors: François G. Dorais
 module
 
 prelude
-public import Init.Data.List.OfFn
-import all Init.Data.List.OfFn
+public import all Init.Data.List.OfFn
 public import Init.Data.List.Monadic
 
 public section

src/Init/Data/List/Find.lean

@@ -11,8 +11,7 @@ public import Init.Data.List.Lemmas
 public import Init.Data.List.Sublist
 public import Init.Data.List.Range
 public import Init.Data.List.Impl
-public import Init.Data.List.Attach
-import all Init.Data.List.Attach
+public import all Init.Data.List.Attach
 public import Init.Data.Fin.Lemmas
 
 public section

src/Init/Data/List/Lemmas.lean

@@ -9,10 +9,8 @@ module
 prelude
 public import Init.Data.Bool
 public import Init.Data.Option.Lemmas
-public import Init.Data.List.BasicAux
-import all Init.Data.List.BasicAux
-public import Init.Data.List.Control
-import all Init.Data.List.Control
+public import all Init.Data.List.BasicAux
+public import all Init.Data.List.Control
 public import Init.Control.Lawful.Basic
 public import Init.BinderPredicates
 

src/Init/Data/List/Monadic.lean

@@ -10,8 +10,7 @@ public import Init.Data.List.TakeDrop
 public import Init.Data.List.Attach
 public import Init.Data.List.OfFn
 public import Init.Data.Array.Bootstrap
-public import Init.Data.List.Control
-import all Init.Data.List.Control
+public import all Init.Data.List.Control
 
 public section
 

src/Init/Data/List/Perm.lean

@@ -9,8 +9,7 @@ prelude
 public import Init.Data.List.Pairwise
 public import Init.Data.List.Erase
 public import Init.Data.List.Find
-public import Init.Data.List.Attach
-import all Init.Data.List.Attach
+public import all Init.Data.List.Attach
 
 public section
 

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

@@ -6,8 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.List.Sort.Basic
-import all Init.Data.List.Sort.Basic
+public import all Init.Data.List.Sort.Basic
 public import Init.Data.List.Sort.Lemmas
 
 public section

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

@@ -7,8 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Perm
-public import Init.Data.List.Sort.Basic
-import all Init.Data.List.Sort.Basic
+public import all Init.Data.List.Sort.Basic
 public import Init.Data.List.Nat.Range
 public import Init.Data.Bool
 

src/Init/Data/List/TakeDrop.lean

@@ -6,8 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module
 
 prelude
-public import Init.Data.List.Basic
-import all Init.Data.List.Basic
+public import all Init.Data.List.Basic
 public import Init.Data.List.Lemmas
 
 public section

src/Init/Data/List/ToArray.lean

@@ -6,16 +6,14 @@ Authors: Mario Carneiro
 module
 
 prelude
-public import Init.Data.List.Control
-import all Init.Data.List.Control
+public import all Init.Data.List.Control
 public import Init.Data.List.Impl
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Monadic
 public import Init.Data.List.Nat.InsertIdx
-public import Init.Data.Array.Basic
-import all Init.Data.Array.Basic
-public import Init.Data.Array.Set
-import all Init.Data.Array.Set
+public import Init.Data.Array.Lex.Basic
+public import all Init.Data.Array.Basic
+public import all Init.Data.Array.Set
 
 public section
 

src/Init/Data/List/Zip.lean

@@ -274,9 +274,11 @@ theorem zip_map {f : α → γ} {g : β → δ} :
   | _, [] => by simp only [map, zip_nil_right]
   | _ :: _, _ :: _ => by simp only [map, zip_cons_cons, zip_map, Prod.map]
 
+@[grind _=_]
 theorem zip_map_left {f : α → γ} {l₁ : List α} {l₂ : List β} :
     zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
 
+@[grind _=_]
 theorem zip_map_right {f : β → γ} {l₁ : List α} {l₂ : List β} :
     zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
 

src/Init/Data/Nat/Basic.lean

@@ -257,6 +257,8 @@ attribute [simp] Nat.le_refl
 
 theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ
 
+theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
+
 theorem le_of_lt_add_one {n m : Nat} : n < m + 1 → n ≤ m := le_of_succ_le_succ
 
 theorem lt_add_one_of_le {n m : Nat} : n ≤ m → n < m + 1 := succ_le_succ
@@ -269,15 +271,37 @@ theorem not_add_one_le_self : (n : Nat) → ¬ n + 1 ≤ n := Nat.not_succ_le_se
 
 theorem add_one_pos (n : Nat) : 0 < n + 1 := Nat.zero_lt_succ n
 
+theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+  induction m with
+  | zero      => exact rfl
+  | succ m ih => apply congrArg pred ih
+
+theorem pred_le : ∀ (n : Nat), pred n ≤ n
+  | zero   => Nat.le.refl
+  | succ _ => le_succ _
+
 theorem pred_lt : ∀ {n : Nat}, n ≠ 0 → pred n < n
   | zero,   h => absurd rfl h
   | succ _, _ => lt_succ_of_le (Nat.le_refl _)
 
 theorem sub_one_lt : ∀ {n : Nat}, n ≠ 0 → n - 1 < n := pred_lt
 
+@[simp] theorem sub_le (n m : Nat) : n - m ≤ n := by
+  induction m with
+  | zero      => exact Nat.le_refl (n - 0)
+  | succ m ih => apply Nat.le_trans (pred_le (n - m)) ih
+
 theorem sub_lt_of_lt {a b c : Nat} (h : a < c) : a - b < c :=
   Nat.lt_of_le_of_lt (Nat.sub_le _ _) h
 
+theorem sub_lt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n
+  | 0,   _,   h1, _  => absurd h1 (Nat.lt_irrefl 0)
+  | _+1, 0,   _, h2  => absurd h2 (Nat.lt_irrefl 0)
+  | n+1, m+1, _,  _  =>
+    Eq.symm (succ_sub_succ_eq_sub n m) ▸
+      show n - m < succ n from
+      lt_succ_of_le (sub_le n m)
+
 theorem sub_succ (n m : Nat) : n - succ m = pred (n - m) := rfl
 
 theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
@@ -292,6 +316,9 @@ theorem sub_add_eq (a b c : Nat) : a - (b + c) = a - b - c := by
   | zero => simp
   | succ c ih => simp only [Nat.add_succ, Nat.sub_succ, ih]
 
+protected theorem lt_of_lt_of_le {n m k : Nat} : n < m → m ≤ k → n < k :=
+  Nat.le_trans
+
 protected theorem lt_of_lt_of_eq {n m k : Nat} : n < m → m = k → n < k :=
   fun h₁ h₂ => h₂ ▸ h₁
 
@@ -329,10 +356,12 @@ protected theorem pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n := (eq_zero_or_po
 
 theorem pos_of_neZero (n : Nat) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero.ne _)
 
-attribute [simp] Nat.lt_add_one
-
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
+theorem lt_succ_self (n : Nat) : n < succ n := lt.base n
+
+@[simp] protected theorem lt_add_one (n : Nat) : n < n + 1 := lt.base n
+
 protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
   match Nat.lt_or_ge m n with
   | Or.inl h => Or.inl (Nat.le_of_lt h)
@@ -428,6 +457,7 @@ protected theorem le_lt_asymm : ∀{a b : Nat}, a ≤ b → ¬(b < a) := flip Na
 
 theorem gt_of_not_le {n m : Nat} (h : ¬ n ≤ m) : n > m := (Nat.lt_or_ge m n).resolve_right h
 protected theorem lt_of_not_ge : ∀{a b : Nat}, ¬(b ≥ a) → b < a := Nat.gt_of_not_le
+protected theorem lt_of_not_le : ∀{a b : Nat}, ¬(a ≤ b) → b < a := Nat.gt_of_not_le
 
 theorem ge_of_not_lt {n m : Nat} (h : ¬ n < m) : n ≥ m := (Nat.lt_or_ge n m).resolve_left h
 protected theorem le_of_not_gt : ∀{a b : Nat}, ¬(b > a) → b ≤ a := Nat.ge_of_not_lt
@@ -740,6 +770,10 @@ protected theorem mul_lt_mul_of_pos_left {n m k : Nat} (h : n < m) (hk : k > 0)
 protected theorem mul_lt_mul_of_pos_right {n m k : Nat} (h : n < m) (hk : k > 0) : n * k < m * k :=
   Nat.mul_comm k m ▸ Nat.mul_comm k n ▸ Nat.mul_lt_mul_of_pos_left h hk
 
+protected theorem mul_pos {n m : Nat} (ha : n > 0) (hb : m > 0) : n * m > 0 :=
+  have h : 0 * m < n * m := Nat.mul_lt_mul_of_pos_right ha hb
+  Nat.zero_mul m ▸ h
+
 protected theorem le_of_mul_le_mul_left {a b c : Nat} (h : c * a ≤ c * b) (hc : 0 < c) : a ≤ b :=
   Nat.ge_of_not_lt fun hlt : b < a =>
     have h' : c * b < c * a := Nat.mul_lt_mul_of_pos_left hlt hc
@@ -799,6 +833,11 @@ set_option linter.missingDocs false in
 @[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
 abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
 
+protected theorem pow_pos (h : 0 < a) : 0 < a^n :=
+  match n with
+  | 0 => Nat.zero_lt_one
+  | _ + 1 => Nat.mul_pos (Nat.pow_pos h) h
+
 set_option linter.missingDocs false in
 @[deprecated Nat.pow_pos (since := "2025-02-17")]
 abbrev pos_pow_of_pos := @Nat.pow_pos
@@ -1160,8 +1199,6 @@ protected theorem sub_eq_iff_eq_add {c : Nat} (h : b ≤ a) : a - b = c ↔ a =
 protected theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c := by
   rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h]
 
-attribute [simp] sub_le
-
 protected theorem sub_one_sub_lt_of_lt (h : a < b) : b - 1 - a < b := by
   rw [← Nat.sub_add_eq]
   exact sub_lt (zero_lt_of_lt h) (Nat.lt_add_right a Nat.one_pos)

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

@@ -9,8 +9,7 @@ module
 prelude
 public import Init.Data.Bool
 public import Init.Data.Int.Pow
-public import Init.Data.Nat.Bitwise.Basic
-import all Init.Data.Nat.Bitwise.Basic
+public import all Init.Data.Nat.Bitwise.Basic
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Nat.Simproc
 public import Init.TacticsExtra
@@ -845,12 +844,6 @@ theorem shiftLeft_add_eq_or_of_lt {b : Nat} (b_lt : b < 2^i) (a : Nat) :
   rw [shiftLeft_eq, Nat.mul_comm]
   rw [two_pow_add_eq_or_of_lt b_lt]
 
-@[simp]
-theorem shiftLeft_eq_zero_iff {a n : Nat} : a <<< n = 0 ↔ a = 0 := by
-  simp [shiftLeft_eq, mul_eq_zero]
-
-instance {a n : Nat} [NeZero a] : NeZero (a <<< n) := ⟨mt shiftLeft_eq_zero_iff.mp (NeZero.ne _)⟩
-
 /-! ### le -/
 
 theorem le_of_testBit {n m : Nat} (h : ∀ i, n.testBit i = true → m.testBit i = true) : n ≤ m := by

src/Init/Data/Nat/Compare.lean

@@ -6,8 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 module
 
 prelude
-public import Init.Data.Ord.Basic
-import all Init.Data.Ord.Basic
+public import all Init.Data.Ord.Basic
 
 public section
 

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

@@ -24,6 +24,47 @@ there is some `c` such that `b = a * c`.
 instance : Dvd Nat where
   dvd a b := Exists (fun c => b = a * c)
 
+theorem div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
+  fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
+
+theorem div_rec_fuel_lemma {x y fuel : Nat} (hy : 0 < y) (hle : y ≤ x) (hfuel : x < fuel + 1) :
+    x - y < fuel :=
+  Nat.lt_of_lt_of_le (div_rec_lemma ⟨hy, hle⟩) (Nat.le_of_lt_succ hfuel)
+
+/--
+Division of natural numbers, discarding the remainder. Division by `0` returns `0`. Usually accessed
+via the `/` operator.
+
+This operation is sometimes called “floor division.”
+
+This function is overridden at runtime with an efficient implementation. This definition is
+the logical model.
+
+Examples:
+ * `21 / 3 = 7`
+ * `21 / 5 = 4`
+ * `0 / 22 = 0`
+ * `5 / 0 = 0`
+-/
+@[extern "lean_nat_div", irreducible]
+protected def div (x y : @& Nat) : Nat :=
+  if hy : 0 < y then
+    let rec
+      go (fuel : Nat) (x : Nat) (hfuel : x < fuel) : Nat :=
+      match fuel with
+      | 0 => by contradiction
+      | succ fuel =>
+        if h : y ≤ x then
+          go fuel (x - y) (div_rec_fuel_lemma hy h hfuel) + 1
+        else
+          0
+      termination_by structural fuel
+    go (x + 1) x (Nat.lt_succ_self _)
+  else
+    0
+
+instance instDiv : Div Nat := ⟨Nat.div⟩
+
 private theorem div.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2) :
     Nat.div.go y hy fuel1 x h1 = Nat.div.go y hy fuel2 x h2 := by
   match fuel1, fuel2 with
@@ -113,6 +154,36 @@ protected def divExact (x y : @& Nat) (h : y ∣ x) : Nat :=
 @[simp]
 theorem divExact_eq_div {x y : Nat} (h : y ∣ x) : x.divExact y h = x / y := rfl
 
+/--
+The modulo operator, which computes the remainder when dividing one natural number by another.
+Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
+than an error.
+
+This is the core implementation of `Nat.mod`. It computes the correct result for any two closed
+natural numbers, but it does not have some convenient [definitional
+reductions](lean-manual://section/type-system) when the `Nat`s contain free variables. The wrapper
+`Nat.mod` handles those cases specially and then calls `Nat.modCore`.
+
+This function is overridden at runtime with an efficient implementation. This definition is the
+logical model.
+-/
+@[extern "lean_nat_mod", irreducible]
+protected noncomputable def modCore (x y : Nat) : Nat :=
+  if hy : 0 < y then
+    let rec
+      go (fuel : Nat) (x : Nat) (hfuel : x < fuel) : Nat :=
+      match fuel with
+      | 0 => by contradiction
+      | succ fuel =>
+        if h : y ≤ x then
+          go fuel (x - y) (div_rec_fuel_lemma hy h hfuel)
+        else
+          x
+      termination_by structural fuel
+    go (x + 1) x (Nat.lt_succ_self _)
+  else
+    x
+
 private theorem modCore.go.fuel_congr (x y fuel1 fuel2 : Nat) (hy : 0 < y) (h1 : x < fuel1) (h2 : x < fuel2) :
     Nat.modCore.go y hy fuel1 x h1 = Nat.modCore.go y hy fuel2 x h2 := by
   match fuel1, fuel2 with
@@ -143,6 +214,51 @@ protected theorem modCore_eq (x y : Nat) : Nat.modCore x y =
   next =>
     simp only [false_and, ↓reduceIte, *]
 
+
+/--
+The modulo operator, which computes the remainder when dividing one natural number by another.
+Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
+than an error.
+
+`Nat.mod` is a wrapper around `Nat.modCore` that special-cases two situations, giving better
+definitional reductions:
+ * `Nat.mod 0 m` should reduce to `m`, for all terms `m : Nat`.
+ * `Nat.mod n (m + n + 1)` should reduce to `n` for concrete `Nat` literals `n`.
+
+These reductions help `Fin n` literals work well, because the `OfNat` instance for `Fin` uses
+`Nat.mod`. In particular, `(0 : Fin (n + 1)).val` should reduce definitionally to `0`. `Nat.modCore`
+can handle all numbers, but its definitional reductions are not as convenient.
+
+This function is overridden at runtime with an efficient implementation. This definition is the
+logical model.
+
+Examples:
+ * `7 % 2 = 1`
+ * `9 % 3 = 0`
+ * `5 % 7 = 5`
+ * `5 % 0 = 5`
+ * `show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl`
+ * `show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl`
+-/
+@[extern "lean_nat_mod"]
+protected def mod : @& Nat → @& Nat → Nat
+  /-
+  Nat.modCore is defined with fuel and thus does not reduce with open terms very well.
+  Nevertheless it is desirable for trivial `Nat.mod` calculations, namely
+  * `Nat.mod 0 m` for all `m`
+  * `Nat.mod n (m + n + 1)` for concrete literals `n`,
+  to reduce definitionally.
+  This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by
+  definition.
+   -/
+  | 0, _ => 0
+  | n@(_ + 1), m =>
+    if m ≤ n -- NB: if n < m does not reduce as well as `m ≤ n`!
+    then Nat.modCore n m
+    else n
+
+instance instMod : Mod Nat := ⟨Nat.mod⟩
+
 protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by
   change Nat.modCore n m = Nat.mod n m
   match n, m with
@@ -199,6 +315,24 @@ theorem mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b :=
   | Or.inl h₁ => h₁.symm ▸ (Nat.sub_zero a).symm ▸ rfl
   | Or.inr h₁ => (mod_eq a b).symm ▸ if_pos ⟨h₁, h⟩
 
+theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
+  induction x, y using mod.inductionOn with
+  | base x y h₁ =>
+    intro h₂
+    have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Decidable.not_and_iff_or_not.mp h₁
+    match h₁ with
+    | Or.inl h₁ => exact absurd h₂ h₁
+    | Or.inr h₁ =>
+      have hgt : y > x := gt_of_not_le h₁
+      have heq : x % y = x := mod_eq_of_lt hgt
+      rw [← heq] at hgt
+      exact hgt
+  | ind x y h h₂ =>
+    intro h₃
+    have ⟨_, h₁⟩ := h
+    rw [mod_eq_sub_mod h₁]
+    exact h₂ h₃
+
 @[simp] protected theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a := by
   rw [Nat.sub_add_cancel]
   cases a with

src/Init/Data/Nat/Fold.lean

@@ -128,12 +128,6 @@ theorem fold_congr {α : Type u} {n m : Nat} (w : n = m)
   subst m
   rfl
 
-theorem foldRev_congr {α : Type u} {n m : Nat} (w : n = m)
-     (f : (i : Nat) → i < n → α → α) (init : α) :
-     foldRev n f init = foldRev m (fun i h => f i (by omega)) init := by
-  subst m
-  rfl
-
 private theorem foldTR_loop_congr {α : Type u} {n m : Nat} (w : n = m)
      (f : (i : Nat) → i < n → α → α) (j : Nat) (h : j ≤ n) (init : α) :
      foldTR.loop n f j h init = foldTR.loop m (fun i h => f i (by omega)) j (by omega) init := by
@@ -276,16 +270,6 @@ def dfoldRev (n : Nat) {α : (i : Nat) → (h : i ≤ n := by omega) → Type u}
   | succ n ih =>
     simp [ih, List.finRange_succ_last, List.foldl_map]
 
-theorem fold_add
-    {α n m} (f : (i : Nat) → i < n + m → α → α) (init : α) :
-    fold (n + m) f init =
-      fold m (fun i h => f (n + i) (by omega))
-        (fold n (fun i h => f i (by omega)) init) := by
-  induction m with
-  | zero => simp; rfl
-  | succ m ih =>
-    simp [fold_congr (Nat.add_assoc n m 1).symm, ih]
-
 /-! ### `foldRev` -/
 
 @[simp] theorem foldRev_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
@@ -301,17 +285,6 @@ theorem fold_add
   | zero => simp
   | succ n ih => simp [ih, List.finRange_succ_last, List.foldr_map]
 
-theorem foldRev_add
-    {α n m} (f : (i : Nat) → i < n + m → α → α) (init : α) :
-    foldRev (n + m) f init =
-      foldRev n (fun i h => f i (by omega))
-        (foldRev m (fun i h => f (n + i) (by omega)) init) := by
-  induction m generalizing init with
-  | zero => simp; rfl
-  | succ m ih =>
-    rw [foldRev_congr (Nat.add_assoc n m 1).symm]
-    simp [ih]
-
 /-! ### `any` -/
 
 @[simp] theorem any_zero {f : (i : Nat) → i < 0 → Bool} : any 0 f = false := by simp [any]

src/Init/Data/Nat/Lemmas.lean

@@ -6,11 +6,9 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Floris van Doorn
 module
 
 prelude
-public import Init.Data.Nat.Bitwise.Basic
-import all Init.Data.Nat.Bitwise.Basic
+public import all Init.Data.Nat.Bitwise.Basic
 public import Init.Data.Nat.MinMax
-public import Init.Data.Nat.Log2
-import all Init.Data.Nat.Log2
+public import all Init.Data.Nat.Log2
 public import Init.Data.Nat.Power2
 public import Init.Data.Nat.Mod
 
@@ -264,6 +262,9 @@ protected theorem pos_of_lt_add_left : n < k + n → 0 < k := by
 protected theorem add_pos_left (h : 0 < m) (n) : 0 < m + n :=
   Nat.lt_of_lt_of_le h (Nat.le_add_right ..)
 
+protected theorem add_pos_right (m) (h : 0 < n) : 0 < m + n :=
+  Nat.lt_of_lt_of_le h (Nat.le_add_left ..)
+
 protected theorem add_self_ne_one : ∀ n, n + n ≠ 1
   | n+1, h => by rw [Nat.succ_add, Nat.succ.injEq] at h; contradiction
 
@@ -1312,13 +1313,13 @@ theorem pow_eq_self_iff {a b : Nat} (ha : 1 < a) : a ^ b = a ↔ b = 1 := by
 
 @[simp]
 theorem log2_zero : Nat.log2 0 = 0 := by
-  simp [Nat.log2_def]
+  simp [Nat.log2]
 
 theorem le_log2 (h : n ≠ 0) : k ≤ n.log2 ↔ 2 ^ k ≤ n := by
   match k with
   | 0 => simp [show 1 ≤ n from Nat.pos_of_ne_zero h]
   | k+1 =>
-    rw [log2_def]; split
+    rw [log2]; split
     · have n0 : 0 < n / 2 := (Nat.le_div_iff_mul_le (by decide)).2 ‹_›
       simp only [Nat.add_le_add_iff_right, le_log2 (Nat.ne_of_gt n0),
         Nat.pow_succ]

src/Init/Data/Nat/Log2.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Robin Arnez
+Authors: Gabriel Ebner
 -/
 module
 
@@ -37,38 +37,11 @@ Examples:
 -/
 @[extern "lean_nat_log2"]
 def log2 (n : @& Nat) : Nat :=
-  -- Lean "assembly"
-  n.rec (fun _ => nat_lit 0) (fun _ ih n =>
-    ((nat_lit 2).ble n).rec (nat_lit 0) ((ih (n.div (nat_lit 2))).succ)) n
-
-private theorem log2_rec_irrel {n k k' : Nat} (hk : n ≤ k) (hk' : n ≤ k') :
-    (k.rec (fun _ => 0) (fun _ ih n => ((2).ble n).rec 0 ((ih (n / 2)).succ)) n : Nat) =
-      k'.rec (fun _ => 0) (fun _ ih n => ((2).ble n).rec 0 ((ih (n / 2)).succ)) n := by
-  induction k generalizing n k' with
-  | zero => cases hk; cases k' <;> rfl
-  | succ k ih =>
-    cases k'
-    · cases hk'; rfl
-    · dsimp only
-      cases h : ble 2 n
-      · rfl
-      · have hn : n / 2 < n := log2_terminates n (Nat.le_of_ble_eq_true h)
-        exact congrArg Nat.succ (ih (Nat.le_of_lt_add_one (Nat.lt_of_lt_of_le hn hk))
-          (Nat.le_of_lt_add_one (Nat.lt_of_lt_of_le hn hk')))
-
-theorem log2_def (n : Nat) : n.log2 = if 2 ≤ n then (n / 2).log2 + 1 else 0 := by
-  rw [Nat.log2, Nat.log2]
-  cases n
-  · rfl
-  split
-  · rename_i n h
-    simp only [ble_eq_true_of_le h]
-    exact congrArg Nat.succ
-      (log2_rec_irrel (Nat.le_of_lt_add_one (log2_terminates _ h)) (Nat.le_refl _))
-  · simp only [mt le_of_ble_eq_true ‹_›]
+  if n ≥ 2 then log2 (n / 2) + 1 else 0
+decreasing_by exact log2_terminates _ ‹_›
 
 theorem log2_le_self (n : Nat) : Nat.log2 n ≤ n := by
-  rw [log2_def]; split
+  unfold Nat.log2; split
   next h =>
     have := log2_le_self (n / 2)
     exact Nat.lt_of_le_of_lt this (Nat.div_lt_self (Nat.le_of_lt h) (by decide))

src/Init/Data/Option/Array.lean

@@ -8,8 +8,7 @@ module
 prelude
 public import Init.Data.Array.Lemmas
 public import Init.Data.Option.List
-public import Init.Data.Option.Instances
-import all Init.Data.Option.Instances
+public import all Init.Data.Option.Instances
 
 public section
 

src/Init/Data/Option/Lemmas.lean

@@ -6,10 +6,8 @@ Authors: Mario Carneiro
 module
 
 prelude
-public import Init.Data.Option.BasicAux
-import all Init.Data.Option.BasicAux
-public import Init.Data.Option.Instances
-import all Init.Data.Option.Instances
+public import all Init.Data.Option.BasicAux
+public import all Init.Data.Option.Instances
 public import Init.Data.BEq
 public import Init.Classical
 public import Init.Ext
@@ -797,7 +795,7 @@ theorem get_merge {o o' : Option α} {f : α → α → α} {i : α} [Std.Lawful
     (o.merge f o').get h = f (o.getD i) (o'.getD i) := by
   cases o <;> cases o' <;> simp [Std.LawfulLeftIdentity.left_id, Std.LawfulRightIdentity.right_id]
 
-@[simp, grind =] theorem elim_none (x : β) (f : α → β) : Option.elim none x f = x := rfl
+@[simp, grind =] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
 
 @[simp, grind =] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
 

src/Init/Data/Option/List.lean

@@ -7,10 +7,8 @@ module
 
 prelude
 public import Init.Data.List.Lemmas
-public import Init.Data.List.Control
-import all Init.Data.List.Control
-public import Init.Data.Option.Instances
-import all Init.Data.Option.Instances
+public import all Init.Data.List.Control
+public import all Init.Data.Option.Instances
 
 public section
 

src/Init/Data/Option/Monadic.lean

@@ -7,8 +7,7 @@ module
 
 prelude
 
-public import Init.Data.Option.Instances
-import all Init.Data.Option.Instances
+public import all Init.Data.Option.Instances
 public import Init.Data.Option.Attach
 public import Init.Control.Lawful.Basic
 

src/Init/Data/Ord/Basic.lean

@@ -9,8 +9,7 @@ prelude
 public import Init.Data.String.Basic
 public import Init.Data.Array.Basic
 public import Init.Data.SInt.Basic
-public import Init.Data.Vector.Basic
-import all Init.Data.Vector.Basic
+public import all Init.Data.Vector.Basic
 
 public section
 
@@ -531,7 +530,7 @@ instance [Ord α] : Ord (Option α) where
   | some x, some y => compare x y
 
 instance : Ord Ordering where
-  compare := compareOn (·.ctorIdx)
+  compare := compareOn (·.toCtorIdx)
 
 namespace List
 

src/Init/Data/Order/Ord.lean

@@ -37,10 +37,6 @@ namespace ReflCmp
 theorem cmp_eq_of_eq {α : Type u} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {a b : α} : a = b → cmp a b = .eq := by
   intro h; subst a; apply compare_self
 
-theorem ne_of_cmp_ne_eq {α : Type u} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {a b : α} :
-    cmp a b ≠ .eq → a ≠ b :=
-  mt cmp_eq_of_eq
-
 end ReflCmp
 
 /-- A typeclasses for ordered types for which `compare a a = .eq` for all `a`. -/

src/Init/Data/Order/PackageFactories.lean

@@ -67,20 +67,20 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact _root_.Classical.Order.instLT
+    | exact Classical.Order.instLT
   beq :
     let := le; let := decidableLE
     BEq α := by
     extract_lets
     first
     | infer_instance
-    | exact _root_.Std.FactoryInstances.beqOfDecidableLE
+    | exact FactoryInstances.beqOfDecidableLE
   lt_iff :
       let := le; let := lt
       ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a := by
     extract_lets
     first
-    | exact _root_.Std.LawfulOrderLT.lt_iff
+    | exact LawfulOrderLT.lt_iff
     | fail "Failed to automatically prove that the `LE` and `LT` instances are compatible. \
             Please ensure that a `LawfulOrderLT` instance can be synthesized or \
             manually provide the field `lt_iff`."
@@ -89,10 +89,10 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       have := lt_iff
       DecidableLT α := by
     extract_lets
-    haveI := @_root_.Std.LawfulOrderLT.mk (lt_iff := by assumption) ..
+    haveI := @LawfulOrderLT.mk (lt_iff := by assumption) ..
     first
     | infer_instance
-    | exact _root_.Std.FactoryInstances.decidableLTOfLE
+    | exact FactoryInstances.decidableLTOfLE
     | fail "Failed to automatically derive that `LT` is decidable. \
             Please ensure that a `DecidableLT` instance can be synthesized or \
             manually provide the field `decidableLT`."
@@ -101,7 +101,7 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       ∀ a b : α, a == b ↔ a ≤ b ∧ b ≤ a := by
     extract_lets
     first
-      | exact _root_.Std.LawfulOrderBEq.beq_iff_le_and_ge
+      | exact LawfulOrderBEq.beq_iff_le_and_ge
       | fail "Failed to automatically prove that the `LE` and `BEq` instances are compatible. \
               Please ensure that a `LawfulOrderBEq` instance can be synthesized or \
               manually provide the field `beq_iff_le_and_ge`."
@@ -110,7 +110,7 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       ∀ a : α, a ≤ a := by
     extract_lets
     first
-    | exact _root_.Std.Refl.refl (r := (· ≤ ·))
+    | exact Std.Refl.refl (r := (· ≤ ·))
     | fail "Failed to automatically prove that the `LE` instance is reflexive. \
             Please ensure that a `Refl` instance can be synthesized or \
             manually provide the field `le_refl`."
@@ -119,7 +119,7 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c := by
     extract_lets
     first
-    | exact fun _ _ _ hab hbc => _root_.Trans.trans (r := (· ≤ ·)) (s := (· ≤ ·)) (t := (· ≤ ·)) hab hbc
+    | exact fun _ _ _ hab hbc => Trans.trans (r := (· ≤ ·)) (s := (· ≤ ·)) (t := (· ≤ ·)) hab hbc
     | fail "Failed to automatically prove that the `LE` instance is transitive. \
             Please ensure that a `Trans` instance can be synthesized or \
             manually provide the field `le_trans`."
@@ -202,7 +202,7 @@ public structure Packages.PartialOrderOfLEArgs (α : Type u) extends Packages.Pr
       ∀ a b : α, a ≤ b → b ≤ a → a = b := by
     extract_lets
     first
-    | exact _root_.Std.Antisymm.antisymm
+    | exact Antisymm.antisymm
     | fail "Failed to automatically prove that the `LE` instance is antisymmetric. \
             Please ensure that a `Antisymm` instance can be synthesized or \
             manually provide the field `le_antisymm`."
@@ -310,11 +310,11 @@ public structure Packages.LinearPreorderOfLEArgs (α : Type u) extends
     extract_lets
     first
     | infer_instance
-    | exact _root_.Std.FactoryInstances.instOrdOfDecidableLE
+    | exact FactoryInstances.instOrdOfDecidableLE
   le_total :
       ∀ a b : α, a ≤ b ∨ b ≤ a := by
     first
-    | exact _root_.Std.Total.total
+    | exact Total.total
     | fail "Failed to automatically prove that the `LE` instance is total. \
             Please ensure that a `Total` instance can be synthesized or \
             manually provide the field `le_total`."
@@ -324,7 +324,7 @@ public structure Packages.LinearPreorderOfLEArgs (α : Type u) extends
       ∀ a b : α, (compare a b).isLE ↔ a ≤ b := by
     extract_lets
     first
-    | exact _root_.Std.LawfulOrderOrd.isLE_compare
+    | exact LawfulOrderOrd.isLE_compare
     | fail "Failed to automatically prove that `(compare a b).isLE` is equivalent to `a ≤ b`. \
             Please ensure that a `LawfulOrderOrd` instance can be synthesized or \
             manually provide the field `isLE_compare`."
@@ -333,7 +333,7 @@ public structure Packages.LinearPreorderOfLEArgs (α : Type u) extends
       ∀ a b : α, (compare a b).isGE ↔ b ≤ a := by
     extract_lets
     first
-    | exact _root_.Std.LawfulOrderOrd.isGE_compare
+    | exact LawfulOrderOrd.isGE_compare
     | fail "Failed to automatically prove that `(compare a b).isGE` is equivalent to `b ≤ a`. \
             Please ensure that a `LawfulOrderOrd` instance can be synthesized or \
             manually provide the field `isGE_compare`."
@@ -411,20 +411,20 @@ public structure Packages.LinearOrderOfLEArgs (α : Type u) extends
     extract_lets
     first
     | infer_instance
-    | exact _root_.Min.leftLeaningOfLE _
+    | exact Min.leftLeaningOfLE _
   max :
       let := le; let := decidableLE
       Max α := by
     extract_lets
     first
     | infer_instance
-    | exact _root_.Max.leftLeaningOfLE _
+    | exact Max.leftLeaningOfLE _
   min_eq :
       let := le; let := decidableLE; let := min
       ∀ a b : α, Min.min a b = if a ≤ b then a else b := by
     extract_lets
     first
-    | exact fun a b => _root_.Std.min_eq_if (a := a) (b := b)
+    | exact fun a b => Std.min_eq_if (a := a) (b := b)
     | fail "Failed to automatically prove that `min` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \
             manually provide the field `min_eq`."
@@ -433,7 +433,7 @@ public structure Packages.LinearOrderOfLEArgs (α : Type u) extends
       ∀ a b : α, Max.max a b = if b ≤ a then a else b := by
     extract_lets
     first
-    | exact fun a b => _root_.Std.max_eq_if (a := a) (b := b)
+    | exact fun a b => Std.max_eq_if (a := a) (b := b)
     | fail "Failed to automatically prove that `max` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \
             manually provide the field `max_eq`."
@@ -538,7 +538,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact _root_.LE.ofOrd _
+    | exact LE.ofOrd _
   lawfulOrderOrd :
       let := ord; let := transOrd; let := le
       LawfulOrderOrd α := by
@@ -554,7 +554,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact _root_.DecidableLE.ofOrd _
+    | exact DecidableLE.ofOrd _
     | fail "Failed to automatically derive that `LE` is decidable.\
             Please ensure that a `DecidableLE` instance can be synthesized or \
             manually provide the field `decidableLE`."
@@ -570,7 +570,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
       ∀ a b : α, a < b ↔ compare a b = .lt := by
     extract_lets
     first
-    | exact fun _ _ => _root_.Std.compare_eq_lt.symm
+    | exact fun _ _ => Std.compare_eq_lt.symm
     | fail "Failed to automatically derive that `LT` and `Ord` are compatible. \
             Please ensure that a `LawfulOrderLT` instance can be synthesized or \
             manually provide the field `lt_iff`."
@@ -580,7 +580,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact _root_DecidableLT.ofOrd _
+    | exact DecidableLT.ofOrd _
     | fail "Failed to automatically derive that `LT` is decidable. \
             Please ensure that a `DecidableLT` instance can be synthesized or \
             manually provide the field `decidableLT`."
@@ -589,7 +589,7 @@ public structure Packages.LinearPreorderOfOrdArgs (α : Type u) where
     extract_lets
     first
     | infer_instance
-    | exact _root_.BEq.ofOrd _
+    | exact BEq.ofOrd _
   beq_iff :
       let := ord; let := le; have := lawfulOrderOrd; let := beq
       ∀ a b : α, a == b ↔ compare a b = .eq := by
@@ -708,7 +708,7 @@ public structure Packages.LinearOrderOfOrdArgs (α : Type u) extends
       ∀ a b : α, compare a b = .eq → a = b := by
     extract_lets
     first
-    | exact fun _ _ => _root_.Std.LawfulEqOrd.eq_of_compare
+    | exact LawfulEqOrd.eq_of_compare
     | fail "Failed to derive a `LawfulEqOrd` instance. \
             Please make sure that it can be synthesized or \
             manually provide the field `eq_of_compare`."
@@ -718,20 +718,20 @@ public structure Packages.LinearOrderOfOrdArgs (α : Type u) extends
     extract_lets
     first
     | infer_instance
-    | exact _root_.Std.FactoryInstances.instMinOfOrd
+    | exact FactoryInstances.instMinOfOrd
   max :
       let := ord
       Max α := by
     extract_lets
     first
     | infer_instance
-    | exact _root_.Std.FactoryInstances.instMaxOfOrd
+    | exact FactoryInstances.instMaxOfOrd
   min_eq :
       let := ord; let := le; let := min; have := lawfulOrderOrd
       ∀ a b : α, Min.min a b = if (compare a b).isLE then a else b := by
     extract_lets
     first
-    | exact fun a b => _root_.Std.min_eq_if_isLE_compare (a := a) (b := b)
+    | exact fun a b => Std.min_eq_if_isLE_compare (a := a) (b := b)
     | fail "Failed to automatically prove that `min` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMin` instance can be synthesized or \
             manually provide the field `min_eq`."
@@ -740,7 +740,7 @@ public structure Packages.LinearOrderOfOrdArgs (α : Type u) extends
       ∀ a b : α, Max.max a b = if (compare a b).isGE then a else b := by
     extract_lets
     first
-    | exact fun a b => _root_.Std.max_eq_if_isGE_compare (a := a) (b := b)
+    | exact fun a b => Std.max_eq_if_isGE_compare (a := a) (b := b)
     | fail "Failed to automatically prove that `max` is left-leaning. \
             Please ensure that a `LawfulOrderLeftLeaningMax` instance can be synthesized or \
             manually provide the field `max_eq`."

src/Init/Data/Random.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.System.IO
-import Init.Data.ByteArray.Extra
 
 public section
 universe u

src/Init/Data/Range/Lemmas.lean

@@ -6,8 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Range.Basic
-import all Init.Data.Range.Basic
+public import all Init.Data.Range.Basic
 public import Init.Data.List.Range
 public import Init.Data.List.Monadic
 public import Init.Data.Nat.Div.Lemmas

src/Init/Data/Range/Polymorphic.lean

@@ -11,7 +11,6 @@ public import Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Range.Polymorphic.Stream
 public import Init.Data.Range.Polymorphic.Lemmas
 public import Init.Data.Range.Polymorphic.Nat
-public import Init.Data.Range.Polymorphic.Int
 public import Init.Data.Range.Polymorphic.NatLemmas
 public import Init.Data.Range.Polymorphic.GetElemTactic
 

src/Init/Data/Range/Polymorphic/Instances.lean

@@ -24,14 +24,14 @@ namespace Std.PRange
 instance [LE α] [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [LawfulOrderLT α] : LawfulUpwardEnumerableLT α where
   lt_iff a b := by
-    simp only [LawfulOrderLT.lt_iff, UpwardEnumerable.le_iff]
+    simp only [LawfulOrderLT.lt_iff, LawfulUpwardEnumerableLE.le_iff]
     constructor
     · intro h
       obtain ⟨n, hn⟩ := h.1
       cases n
       · apply h.2.elim
         refine ⟨0, ?_⟩
-        simpa [succMany?_zero] using hn.symm
+        simpa [UpwardEnumerable.succMany?_zero] using hn.symm
       exact ⟨_, hn⟩
     · intro h
       constructor
@@ -41,60 +41,63 @@ instance [LE α] [LT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
 instance [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] :
     LawfulUpwardEnumerableLowerBound .closed α where
   isSatisfied_iff a l := by
-    simp [SupportsLowerBound.IsSatisfied, init?, UpwardEnumerable.le_iff]
+    simp [SupportsLowerBound.IsSatisfied, BoundedUpwardEnumerable.init?,
+      LawfulUpwardEnumerableLE.le_iff]
 
 instance [LE α] [DecidableLE α] [UpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Trans (α := α) (· ≤ ·) (· ≤ ·) (· ≤ ·)]:
     LawfulUpwardEnumerableUpperBound .closed α where
   isSatisfied_of_le u a b hub hab := by
-    simp only [SupportsUpperBound.IsSatisfied, ← UpwardEnumerable.le_iff] at hub hab ⊢
+    simp only [SupportsUpperBound.IsSatisfied, ← LawfulUpwardEnumerableLE.le_iff] at hub hab ⊢
     exact Trans.trans hab hub
 
 instance [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] :
     LawfulUpwardEnumerableLowerBound .open α where
   isSatisfied_iff a l := by
-    simp only [SupportsLowerBound.IsSatisfied, init?, UpwardEnumerable.lt_iff]
+    simp only [SupportsLowerBound.IsSatisfied, BoundedUpwardEnumerable.init?,
+      LawfulUpwardEnumerableLT.lt_iff]
     constructor
     · rintro ⟨n, hn⟩
-      simp only [succMany?_succ?_eq_succ?_bind_succMany?] at hn
-      cases h : succ? l
+      simp only [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] at hn
+      cases h : UpwardEnumerable.succ? l
       · simp [h] at hn
       · exact ⟨_, rfl, n, by simpa [h] using hn⟩
     · rintro ⟨init, hi, n, hn⟩
-      exact ⟨n, by simpa [succMany?_succ?_eq_succ?_bind_succMany?, hi] using hn⟩
+      exact ⟨n, by simpa [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, hi] using hn⟩
 
 instance [LT α] [DecidableLT α] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLT α] :
     LawfulUpwardEnumerableUpperBound .open α where
   isSatisfied_of_le u a b hub hab := by
-    simp only [SupportsUpperBound.IsSatisfied, UpwardEnumerable.lt_iff] at hub ⊢
+    simp only [SupportsUpperBound.IsSatisfied, LawfulUpwardEnumerableLT.lt_iff] at hub ⊢
     exact UpwardEnumerable.lt_of_le_of_lt hab hub
 
 instance [UpwardEnumerable α] [Least? α] [LawfulUpwardEnumerableLeast? α] :
     LawfulUpwardEnumerableLowerBound .unbounded α where
   isSatisfied_iff a l := by
-    simpa [SupportsLowerBound.IsSatisfied, init?] using UpwardEnumerable.least?_le
+    simpa [SupportsLowerBound.IsSatisfied, BoundedUpwardEnumerable.init?] using
+      LawfulUpwardEnumerableLeast?.eq_succMany?_least? a
 
 instance [LE α] [Total (α := α) (· ≤ ·)] [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] :
     LinearlyUpwardEnumerable α where
   eq_of_succ?_eq a b hab := by
     cases Total.total (α := α) (r := (· ≤ ·)) a b <;> rename_i h <;>
-      simp only [UpwardEnumerable.le_iff] at h
+      simp only [LawfulUpwardEnumerableLE.le_iff] at h
     · obtain ⟨n, hn⟩ := h
       cases n
-      · simpa [succMany?_zero] using hn
+      · simpa [UpwardEnumerable.succMany?_zero] using hn
       · exfalso
-        rw [succMany?_succ?_eq_succ?_bind_succMany?, hab,
-          ← succMany?_succ?_eq_succ?_bind_succMany?] at hn
+        rw [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, hab,
+          ← LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] at hn
         exact UpwardEnumerable.lt_irrefl ⟨_, hn⟩
     · obtain ⟨n, hn⟩ := h
       cases n
-      · simpa [succMany?_zero] using hn.symm
+      · simpa [UpwardEnumerable.succMany?_zero] using hn.symm
       · exfalso
-        rw [succMany?_succ?_eq_succ?_bind_succMany?, hab.symm,
-          ← succMany?_succ?_eq_succ?_bind_succMany?] at hn
+        rw [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, hab.symm,
+          ← LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] at hn
         exact UpwardEnumerable.lt_irrefl ⟨_, hn⟩
 
 instance [UpwardEnumerable α] : LawfulUpwardEnumerableUpperBound .unbounded α where
@@ -119,24 +122,24 @@ instance LawfulRangeSize.open_of_closed [UpwardEnumerable α] [LE α] [Decidable
     simp only [SupportsUpperBound.IsSatisfied] at h
     simp only [RangeSize.size]
     by_cases h' : a ≤ bound
-    · match hs : succ? a with
+    · match hs : UpwardEnumerable.succ? a with
       | none => rw [LawfulRangeSize.size_eq_one_of_succ?_eq_none (h := h') (h' := by omega)]
       | some b =>
         rw [LawfulRangeSize.size_eq_succ_of_succ?_eq_some (h := h') (h' := hs)]
         have : ¬ b ≤ bound := by
           intro hb
           have : a < b := by
-            rw [UpwardEnumerable.lt_iff]
-            exact ⟨0, by simpa [succMany?_one] using hs⟩
+            rw [LawfulUpwardEnumerableLT.lt_iff]
+            exact ⟨0, by simpa [UpwardEnumerable.succMany?_one] using hs⟩
           exact h (lt_of_lt_of_le this hb)
         rw [LawfulRangeSize.size_eq_zero_of_not_isSatisfied (h := this)]
     · suffices RangeSize.size (shape := .closed) bound a = 0 by omega
       exact LawfulRangeSize.size_eq_zero_of_not_isSatisfied _ _ h'
   size_eq_one_of_succ?_eq_none bound a h h' := by
     exfalso
-    simp only [SupportsUpperBound.IsSatisfied, UpwardEnumerable.lt_iff] at h
+    simp only [SupportsUpperBound.IsSatisfied, LawfulUpwardEnumerableLT.lt_iff] at h
     obtain ⟨n, hn⟩ := h
-    simp [succMany?_succ?_eq_succ?_bind_succMany?, h'] at hn
+    simp [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, h'] at hn
   size_eq_succ_of_succ?_eq_some bound a a' h h' := by
     simp only [SupportsUpperBound.IsSatisfied] at h
     simp only [RangeSize.size, Nat.pred_eq_succ_iff]
@@ -145,10 +148,10 @@ instance LawfulRangeSize.open_of_closed [UpwardEnumerable α] [LE α] [Decidable
     · omega
     · simp only [Nat.succ_le_iff, LawfulRangeSize.size_pos_iff_isSatisfied,
         SupportsUpperBound.IsSatisfied]
-      rw [UpwardEnumerable.le_iff]
-      rw [UpwardEnumerable.lt_iff] at h
+      rw [LawfulUpwardEnumerableLE.le_iff]
+      rw [LawfulUpwardEnumerableLT.lt_iff] at h
       refine ⟨h.choose, ?_⟩
-      simpa [succMany?_succ?_eq_succ?_bind_succMany?, h'] using h.choose_spec
+      simpa [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, h'] using h.choose_spec
 
 instance LawfulRangeSize.instHasFiniteRanges [UpwardEnumerable α] [LawfulUpwardEnumerable α]
     [RangeSize su α] [SupportsUpperBound su α] [LawfulRangeSize su α] : HasFiniteRanges su α where
@@ -158,11 +161,11 @@ instance LawfulRangeSize.instHasFiniteRanges [UpwardEnumerable α] [LawfulUpward
     induction n generalizing init with
     | zero =>
       simp only [LawfulRangeSize.size_eq_zero_iff_not_isSatisfied] at hn
-      simp [succMany?_zero, hn]
+      simp [UpwardEnumerable.succMany?_zero, hn]
     | succ =>
       rename_i n ih
-      rw [succMany?_succ?_eq_succ?_bind_succMany?]
-      match hs : succ? init with
+      rw [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?]
+      match hs : UpwardEnumerable.succ? init with
       | none => simp
       | some a =>
         simp only [Option.bind_some]

src/Init/Data/Range/Polymorphic/Int.lean

@@ -1,56 +0,0 @@
-/-
-Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Range.Polymorphic.Instances
-public import Init.Data.Order.Classes
-import Init.Omega
-
-public section
-
-namespace Std.PRange
-
-instance : UpwardEnumerable Int where
-  succ? x := some (x + 1)
-  succMany? n x := some (x + n)
-
-instance : LawfulUpwardEnumerable Int where
-  ne_of_lt := by
-    simp only [UpwardEnumerable.LT, UpwardEnumerable.succMany?, Option.some.injEq]
-    omega
-  succMany?_zero := by simp [UpwardEnumerable.succMany?]
-  succMany?_succ := by
-    simp only [UpwardEnumerable.succMany?, UpwardEnumerable.succ?,
-      Option.bind_some, Option.some.injEq]
-    omega
-
-instance : InfinitelyUpwardEnumerable Int where
-  isSome_succ? x := by simp [UpwardEnumerable.succ?]
-
-instance : LawfulUpwardEnumerableLE Int where
-  le_iff x y := by
-    simp [UpwardEnumerable.LE, UpwardEnumerable.succMany?, Int.le_def, Int.nonneg_def,
-      Int.sub_eq_iff_eq_add', eq_comm (a := y)]
-
-instance : RangeSize .closed Int where
-  size bound a := (bound + 1 - a).toNat
-
-instance : RangeSize .open Int := RangeSize.openOfClosed
-
-instance : LawfulRangeSize .closed Int where
-  size_eq_zero_of_not_isSatisfied bound x := by
-    simp only [SupportsUpperBound.IsSatisfied, RangeSize.size]
-    omega
-  size_eq_one_of_succ?_eq_none bound x := by
-    simp [SupportsUpperBound.IsSatisfied, RangeSize.size, UpwardEnumerable.succ?]
-
-  size_eq_succ_of_succ?_eq_some bound init x := by
-    simp only [SupportsUpperBound.IsSatisfied, UpwardEnumerable.succ?, RangeSize.size,
-      Option.some.injEq]
-    omega
-
-end Std.PRange