doc: grind attribute modifiers

This PR adds lemmas about `Nat.fold` and `Nat.foldRev` on sums, to match
the existing theorems about `dfold` and `dfoldRev`.

.github/workflows/build-template.yml

@@ -36,7 +36,7 @@ jobs:
         include: ${{fromJson(inputs.config)}}
       # complete all jobs
       fail-fast: false
-    runs-on: ${{ matrix.os }}
+    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
@@ -69,10 +69,16 @@ 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'
@@ -104,7 +110,7 @@ jobs:
           # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
           path: |
             .ccache
-            ${{ matrix.name == 'Linux Lake (cached)' && 'build/stage1/**/*.trace
+            ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
             build/stage1/**/*.olean*
             build/stage1/**/*.ilean
             build/stage1/**/*.ir
@@ -166,6 +172,24 @@ jobs:
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
           time make $TARGET_STAGE -j$NPROC
+      # 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()
+        uses: actions/cache/save@v4
+        with:
+          # NOTE: must be in sync with `restore` above
+          path: |
+            .ccache
+            ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
+            build/stage1/**/*.olean*
+            build/stage1/**/*.ilean
+            build/stage1/**/*.ir
+            build/stage1/**/*.c
+            build/stage1/**/*.c.o*' || '' }}
+          key: ${{ steps.restore-cache.outputs.cache-primary-key }}
       - name: Install
         run: |
           make -C build/$TARGET_STAGE install
@@ -199,13 +223,13 @@ jobs:
           path: pack/*
       - name: Lean stats
         run: |
-          build/stage1/bin/lean --stats src/Lean.lean -Dexperimental.module=true
+          build/$TARGET_STAGE/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.CTARGET_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
@@ -235,9 +259,13 @@ jobs:
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
+          set -e
           # clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
           # changes yet
-          make -C build update-stage0 && make -C build/stage1 clean-stdlib && make -C build -j$NPROC
+          make -C build update-stage0
+          make -C build/stage1 clean-stdlib
+          time make -C build -j$NPROC
+          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
         if: matrix.check-rebootstrap
       - name: CCache stats
         if: always()
@@ -249,22 +277,3 @@ jobs:
             progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
             echo bt | $GDB/bin/gdb -q $progbin $c || true
           done
-      - name: Save Cache
-        if: always() && steps.restore-cache.outputs.cache-hit != 'true'
-        uses: actions/cache/save@v4
-        with:
-          # NOTE: must be in sync with `restore` above
-          path: |
-            .ccache
-            ${{ matrix.name == 'Linux Lake (cached)' && 'build/stage1/**/*.trace
-            build/stage1/**/*.olean*
-            build/stage1/**/*.ilean
-            build/stage1/**/*.ir
-            build/stage1/**/*.c
-            build/stage1/**/*.c.o*' || '' }}
-          key: ${{ steps.restore-cache.outputs.cache-primary-key }}
-      - name: Upload Build Artifact
-        if: always() && matrix.name == 'Linux Lake (cached)'
-        uses: actions/upload-artifact@v4
-        with:
-          path: build

.github/workflows/ci.yml

@@ -181,24 +181,18 @@ jobs:
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
                 // foreign code may be linked against more recent glibc
-                "CTEST_OPTIONS": "-E 'foreign'"
+                "CTEST_OPTIONS": "-E 'foreign'",
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "check-level": 0,
                 "test": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
                 // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
                 "test-speedcenter": large && level >= 2,
-                "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
-              },
-              {
-                "name": "Linux Lake (cached)",
-                "os": "ubuntu-latest",
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
-                "secondary": true,
+                // made explicit until it can be assumed to have propagated to PRs
                 "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
               },
               {
@@ -228,7 +222,8 @@ jobs:
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
-                "tar": "gtar" // https://github.com/actions/runner-images/issues/2619
+                "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
+                "CTEST_OPTIONS": "-E 'leanlaketest_hello'", // started failing from unpack
               },
               {
                 "name": "macOS aarch64",
@@ -256,7 +251,7 @@ jobs:
                 "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"
+                "binary-check": "ldd",
               },
               {
                 "name": "Linux aarch64",
@@ -266,7 +261,7 @@ jobs:
                 "check-level": 2,
                 "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*"
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
               },
               // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation
               //{
@@ -295,6 +290,12 @@ 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,6 +19,8 @@ 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
@@ -57,9 +59,14 @@ jobs:
       uses: actions/cache/restore@v4
       with:
         # NOTE: must be in sync with `restore-cache` in `build-template.yml`
-        # TODO: actually switch to USE_LAKE once it caches more; for now it just caches more often than any other build type so let's use its cache
         path: |
           .ccache
+          build/stage1/**/*.trace
+          build/stage1/**/*.olean*
+          build/stage1/**/*.ilean
+          build/stage1/**/*.ir
+          build/stage1/**/*.c
+          build/stage1/**/*.c.o*
         key: Linux Lake-build-v3-${{ github.sha }}
         # fall back to (latest) previous cache
         restore-keys: |

CMakeLists.txt

@@ -147,6 +147,10 @@ add_custom_target(test
   COMMAND $(MAKE) -C stage1 test
   DEPENDS stage1)
 
+add_custom_target(clean-stdlib
+  COMMAND $(MAKE) -C stage1 clean-stdlib
+  DEPENDS stage1)
+
 install(CODE "execute_process(COMMAND make -C stage1 install)")
 
 add_custom_target(check-stage3

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/documentation/examples/)
+- [Examples](https://lean-lang.org/lean4/doc/examples.html)
 - [External Contribution Guidelines](CONTRIBUTING.md)
 
 # Installation

doc/dev/bootstrap.md

@@ -1,6 +1,6 @@
 # Lean Build Bootstrapping
 
-Since version 4, Lean is a partially bootstrapped program: most parts of the
+Lean is a bootstrapped program: the
 frontend and compiler are written in Lean itself and thus need to be built before
 building Lean itself - which is needed to again build those parts. This cycle is
 broken by using pre-built C files checked into the repository (which ultimately
@@ -73,6 +73,11 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
 The github repository will automatically update stage0 on `master` once
 `src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
 
+NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
+Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.
+The same is true for further stages except that a rebuild of them is retriggered on any committed change, not just to a specific directory.
+Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
+
 If you have write access to the lean4 repository, you can also manually
 trigger that process, for example to be able to use new features in the compiler itself.
 You can do that on <https://github.com/leanprover/lean4/actions/workflows/update-stage0.yml>
@@ -82,13 +87,13 @@ gh workflow run update-stage0.yml
 ```
 
 Leaving stage0 updates to the CI automation is preferable, but should you need
-to do it locally, you can use `make update-stage0-commit` in `build/release` to
-update `stage0` from `stage1` or `make -C stageN update-stage0-commit` to
+to do it locally, you can use `make -C build/release update-stage0-commit` to
+update `stage0` from `stage1` or `make -C build/release/stageN update-stage0-commit` to
 update from another stage. This command will automatically stage the updated files
-and introduce a commit,so make sure to commit your work before that.
+and introduce a commit, so make sure to commit your work before that.
 
 If you rebased the branch (either onto a newer version of `master`, or fixing
-up some commits prior to the stage0 update, recreate the stage0 update commits.
+up some commits prior to the stage0 update), recreate the stage0 update commits.
 The script `script/rebase-stage0.sh` can be used for that.
 
 The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)

doc/dev/index.md

@@ -9,7 +9,7 @@ You should not edit the `stage0` directory except using the commands described i
 ## Development Setup
 
 You can use any of the [supported editors](../setup.md) for editing the Lean source code.
-If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
+Please see below for specific instructions for VS Code.
 
 ### Dev setup using elan
 
@@ -68,6 +68,10 @@ code lean.code-workspace
 ```
 on the command line.
 
+You can use the `Refresh File Dependencies` command as in other projects to rebuild modules from inside VS Code but be aware that this does not trigger any non-Lake build targets.
+In particular, after updating `stage0/` (or fetching an update to it), you will want to invoke `make` directly to rebuild `stage0/bin/lean` as described in [building Lean](../make/index.md).
+You should then run the `Restart Server` command to update all open files and the server watchdog process as well.
+
 ### `ccache`
 
 Lean's build process uses [`ccache`](https://ccache.dev/) if it is

doc/examples/bintree.lean

@@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    intros le
+    intro le
     exact Nat.lt_of_le_of_ne le ne
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h

doc/make/index.md

@@ -53,11 +53,6 @@ There are also two alternative presets that combine some of these options you ca
   Select the C/C++ compilers to use. Official Lean releases currently use Clang;
   see also `.github/workflows/ci.yml` for the CI config.
 
-* `-DUSE_LAKE=ON`\
-  Experimental option to build the core libraries using Lake instead of `lean.mk`.  Caveats:
-  * As native code compilation is still handled by cmake, changes to stage0/ (such as from `git pull`) are picked up only when invoking the build via `make`, not via `Refresh Dependencies` in the editor.
-  * `USE_LAKE` is not yet compatible with `LAKE_ARTIFACT_CACHE`
-
 Lean will automatically use [CCache](https://ccache.dev/) if available to avoid
 redundant builds, especially after stage 0 has been updated.
 

flake.nix

@@ -18,14 +18,14 @@
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
 
-      lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
+      llvmPackages = pkgs.llvmPackages_15;
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
-          stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
+          stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
             cmake gmp libuv ccache pkg-config
-            lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
+            llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI
           ];
@@ -60,12 +60,6 @@
           GDB = pkgsDist.gdb;
         });
     in {
-      packages.${system} = {
-        # to be removed when Nix CI is not needed anymore
-        inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
-        deprecated = lean-packages;
-      };
-
       devShells.${system} = {
         # The default development shell for working on lean itself
         default = devShellWithDist pkgs;

nix/bareStdenv/setup

@@ -1,7 +0,0 @@
-set -eo pipefail
-
-for pkg in $buildInputs; do
-  export PATH=$PATH:$pkg/bin
-done
-
-: ${outputs:=out}

nix/bootstrap.nix

@@ -1,208 +0,0 @@
-{ src, debug ? false, stage0debug ? false, extraCMakeFlags ? [],
-  stdenv, lib, cmake, pkg-config, gmp, libuv, cadical, git, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, linkFarmFromDrvs,
-  ... } @ args:
-with builtins;
-lib.warn "The Nix-based build is deprecated" rec {
-  inherit stdenv;
-  sourceByRegex = p: rs: lib.sourceByRegex p (map (r: "(/src/)?${r}") rs);
-  buildCMake = args: stdenv.mkDerivation ({
-    nativeBuildInputs = [ cmake pkg-config ];
-    buildInputs = [ gmp libuv llvmPackages.llvm ];
-    # https://github.com/NixOS/nixpkgs/issues/60919
-    hardeningDisable = [ "all" ];
-    dontStrip = (args.debug or debug);
-
-    postConfigure = ''
-      patchShebangs .
-    '';
-  } // args // {
-    src = args.realSrc or (sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]);
-    cmakeFlags = ["-DSMALL_ALLOCATOR=ON" "-DUSE_MIMALLOC=OFF"] ++ (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" "-DCADICAL=${cadical}/bin/cadical" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ];
-    preConfigure = args.preConfigure or "" + ''
-      # ignore absence of submodule
-      sed -i 's!lake/Lake.lean!!' CMakeLists.txt
-    '';
-  });
-  lean-bin-tools-unwrapped = buildCMake {
-    name = "lean-bin-tools";
-    outputs = [ "out" "leanc_src" ];
-    realSrc = sourceByRegex (src + "/src") [ "CMakeLists\.txt" "[a-z].*" ".*\.in" "Leanc\.lean" ];
-    dontBuild = true;
-    installPhase = ''
-      mkdir $out $leanc_src
-      mv bin/ include/ share/ $out/
-      mv leanc.sh $out/bin/leanc
-      mv leanc/Leanc.lean $leanc_src/
-      substituteInPlace $out/bin/leanc --replace '$root' "$out" --replace " sed " " ${gnused}/bin/sed "
-      substituteInPlace $out/bin/leanmake --replace "make" "${gnumake}/bin/make"
-      substituteInPlace $out/share/lean/lean.mk --replace "/usr/bin/env bash" "${bash}/bin/bash"
-    '';
-  };
-  leancpp = buildCMake {
-    name = "leancpp";
-    src = src + "/src";
-    buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "leanshell" "leanmain" ];
-    installPhase = ''
-      mkdir -p $out
-      mv lib/ $out/
-      mv runtime/libleanrt_initial-exec.a $out/lib
-    '';
-  };
-  stage0 = args.stage0 or (buildCMake {
-    name = "lean-stage0";
-    realSrc = src + "/stage0/src";
-    debug = stage0debug;
-    cmakeFlags = [ "-DSTAGE=0" ];
-    extraCMakeFlags = [];
-    preConfigure = ''
-      ln -s ${src + "/stage0/stdlib"} ../stdlib
-    '';
-    installPhase = ''
-      mkdir -p $out/bin $out/lib/lean
-      mv bin/lean $out/bin/
-      mv lib/lean/*.{so,dylib} $out/lib/lean
-    '';
-    meta.mainProgram = "lean";
-  });
-  stage = { stage, prevStage, self }:
-    let
-      desc = "stage${toString stage}";
-      build = args: buildLeanPackage.override {
-        lean = prevStage;
-        leanc = lean-bin-tools-unwrapped;
-        # use same stage for retrieving dependencies
-        lean-leanDeps = stage0;
-        lean-final = self;
-      } ({
-        src = src + "/src";
-        roots = [ { mod = args.name; glob = "andSubmodules"; } ];
-        fullSrc = src;
-        srcPath = "$PWD/src:$PWD/src/lake";
-        inherit debug;
-        leanFlags = [ "-DwarningAsError=true" ];
-      } // args);
-      Init' = build { name = "Init"; deps = []; };
-      Std' = build { name = "Std"; deps = [ Init' ]; };
-      Lean' = build { name = "Lean"; deps = [ Std' ]; };
-      attachSharedLib = sharedLib: pkg: pkg // {
-        inherit sharedLib;
-        mods = mapAttrs (_: m: m // { inherit sharedLib; propagatedLoadDynlibs = []; }) pkg.mods;
-      };
-    in (all: all // all.lean) rec {
-      inherit (Lean) emacs-dev emacs-package vscode-dev vscode-package;
-      Init = attachSharedLib leanshared Init';
-      Std = attachSharedLib leanshared Std' // { allExternalDeps = [ Init ]; };
-      Lean = attachSharedLib leanshared Lean' // { allExternalDeps = [ Std ]; };
-      Lake = build {
-        name = "Lake";
-        sharedLibName = "Lake_shared";
-        src = src + "/src/lake";
-        deps = [ Init Lean ];
-      };
-      Lake-Main = build {
-        name = "LakeMain";
-        roots = [{ glob = "one"; mod = "LakeMain"; }];
-        executableName = "lake";
-        deps = [ Lake ];
-        linkFlags = lib.optional stdenv.isLinux "-rdynamic";
-        src = src + "/src/lake";
-      };
-      stdlib = [ Init Std Lean Lake ];
-      modDepsFiles = symlinkJoin { name = "modDepsFiles"; paths = map (l: l.modDepsFile) (stdlib ++ [ Leanc ]); };
-      depRoots = symlinkJoin { name = "depRoots"; paths = map (l: l.depRoots) stdlib; };
-      iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
-      Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
-      stdlibLinkFlags = "${lib.concatMapStringsSep " " (l: "-L${l.staticLib}") stdlib} -L${leancpp}/lib/lean";
-      libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
-        mkdir $out
-        touch empty.c
-        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
-      '';
-      leanshared_1 = runCommand "leanshared_1" { buildInputs = [ stdenv.cc ]; libName = "leanshared_1${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
-        mkdir $out
-        touch empty.c
-        ${stdenv.cc}/bin/cc -shared -o $out/$libName empty.c
-      '';
-      leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
-        mkdir $out
-        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
-          -Wl,--whole-archive ${leancpp}/lib/temp/libleanshell.a -lInit -lStd -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ \
-          -lm ${stdlibLinkFlags} \
-          $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
-          -o $out/$libName
-      '';
-      mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
-      print-paths = Lean.makePrintPathsFor [] mods;
-      leanc = writeShellScriptBin "leanc" ''
-        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared_1} -L${leanshared} -L${Lake.sharedLib} "$@"
-      '';
-      lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
-        mkdir -p $out/bin
-        ${leanc}/bin/leanc ${leancpp}/lib/temp/libleanmain.a ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* -o $out/bin/lean
-      '';
-      # derivation following the directory layout of the "basic" setup, mostly useful for running tests
-      lean-all = stdenv.mkDerivation {
-        name = "lean-${desc}";
-        buildCommand = ''
-          mkdir -p $out/bin $out/lib/lean
-          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared_1}/* ${leanshared}/* ${Lake.sharedLib}/* $out/lib/lean/
-          # put everything in a single final derivation so `IO.appDir` references work
-          cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
-          # NOTE: `lndir` will not override existing `bin/leanc`
-          ${lndir}/bin/lndir -silent ${lean-bin-tools-unwrapped} $out
-        '';
-        meta.mainProgram = "lean";
-      };
-      cacheRoots = linkFarmFromDrvs "cacheRoots" ([
-        stage0 lean leanc lean-all iTree modDepsFiles depRoots Leanc.src
-      ] ++ map (lib: lib.oTree) stdlib);
-      test = buildCMake {
-        name = "lean-test-${desc}";
-        realSrc = lib.sourceByRegex src [ "src.*" "tests.*" ];
-        buildInputs = [ gmp libuv perl git cadical ];
-        preConfigure = ''
-          cd src
-        '';
-        extraCMakeFlags = [ "-DLLVM=OFF" ];
-        postConfigure = ''
-          patchShebangs ../../tests ../lake
-          rm -r bin lib include share
-          ln -sf ${lean-all}/* .
-        '';
-        buildPhase = ''
-         ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_reverse-ffi|leanruntest_timeIO' -j$NIX_BUILD_CORES
-        '';
-        installPhase = ''
-          mkdir $out
-          mv test-results.xml $out
-        '';
-      };
-      update-stage0 =
-        let cTree = symlinkJoin { name = "cs"; paths = map (lib: lib.cTree) (stdlib ++ [Lake-Main]); }; in
-        writeShellScriptBin "update-stage0" ''
-          CSRCS=${cTree} CP_C_PARAMS="--dereference --no-preserve=all" ${src + "/script/lib/update-stage0"}
-        '';
-      update-stage0-commit = writeShellScriptBin "update-stage0-commit" ''
-        set -euo pipefail
-        ${update-stage0}/bin/update-stage0
-        git commit -m "chore: update stage0"
-      '';
-      link-ilean = writeShellScriptBin "link-ilean" ''
-        dest=''${1:-src}
-        rm -rf $dest/build/lib || true
-        mkdir -p $dest/build/lib
-        ln -s ${iTree}/* $dest/build/lib
-      '';
-      benchmarks =
-        let
-          entries = attrNames (readDir (src + "/tests/bench"));
-          leanFiles = map (n: elemAt n 0) (filter (n: n != null) (map (match "(.*)\.lean") entries));
-        in lib.genAttrs leanFiles (n: (buildLeanPackage {
-          name = n;
-          src = filterSource (e: _: baseNameOf e == "${n}.lean") (src + "/tests/bench");
-        }).executable);
-    };
-  stage1 = stage { stage = 1; prevStage = stage0; self = stage1; };
-  stage2 = stage { stage = 2; prevStage = stage1; self = stage2; };
-  stage3 = stage { stage = 3; prevStage = stage2; self = stage3; };
-}

nix/buildLeanPackage.nix

@@ -1,247 +0,0 @@
-{ lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
-  stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, substituteAll, symlinkJoin, linkFarmFromDrvs,
-  runCommand, darwin, mkShell, ... }:
-let lean-final' = lean-final; in
-lib.makeOverridable (
-{ name, src, fullSrc ? src, srcPrefix ? "", srcPath ? "$PWD/${srcPrefix}",
-  # Lean dependencies. Each entry should be an output of buildLeanPackage.
-  deps ? [ lean.Init lean.Std lean.Lean ],
-  # Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
-  staticLibDeps ? [],
-  # Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
-  groupStaticLibs ? false,
-  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
-  # shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
-  # These libs are also linked to in packages that depend on this one.
-  nativeSharedLibs ? [],
-  # Lean modules to include.
-  # A set of Lean modules names as strings (`"Foo.Bar"`) or attrsets (`{ name = "Foo.Bar"; glob = "one" | "submodules" | "andSubmodules"; }`);
-  # see Lake README for glob meanings. Dependencies of selected modules are always included.
-  roots ? [ name ],
-  # Output from `lean --deps-json` on package source files. Persist the corresponding output attribute to a file and pass it back in here to avoid IFD.
-  # Must be refreshed on any change in `import`s or set of source file names.
-  modDepsFile ? null,
-  # Whether to compile each module into a native shared library that is loaded whenever the module is imported in order to accelerate evaluation
-  precompileModules ? false,
-  # Whether to compile the package into a native shared library that is loaded whenever *any* of the package's modules is imported into another package.
-  # If `precompileModules` is also `true`, the latter only affects imports within the current package.
-  precompilePackage ? precompileModules,
-  # Lean plugin dependencies. Each derivation `plugin` should contain a plugin library at path `${plugin}/${plugin.name}`.
-  pluginDeps ? [],
-  # `overrideAttrs` for `buildMod`
-  overrideBuildModAttrs ? null,
-  debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name, libName ? name, sharedLibName ? libName,
-  srcTarget ? "..#stage0", srcArgs ? "(\${args[*]})", lean-final ? lean-final' }@args:
-with builtins; let
-  # "Init.Core" ~> "Init/Core"
-  modToPath = mod: replaceStrings ["."] ["/"] mod;
-  modToAbsPath = mod: "${src}/${modToPath mod}";
-  # sanitize file name before copying to store, except when already in store
-  copyToStoreSafe = base: suffix: if lib.isDerivation base then base + suffix else
-    builtins.path { name = lib.strings.sanitizeDerivationName (baseNameOf suffix); path = base + suffix; };
-  modToLean = mod: copyToStoreSafe src "/${modToPath mod}.lean";
-  bareStdenv = ./bareStdenv;
-  mkBareDerivation = args: derivation (args // {
-    name = lib.strings.sanitizeDerivationName args.name;
-    stdenv = bareStdenv;
-    inherit (stdenv) system;
-    buildInputs = (args.buildInputs or []) ++ [ coreutils ];
-    builder = stdenv.shell;
-    args = [ "-c" ''
-      source $stdenv/setup
-      set -u
-      ${args.buildCommand}
-    '' ];
-  }) // { overrideAttrs = f: mkBareDerivation (lib.fix (lib.extends f (_: args))); };
-  runBareCommand = name: args: buildCommand: mkBareDerivation (args // { inherit name buildCommand; });
-  runBareCommandLocal = name: args: buildCommand: runBareCommand name (args // {
-    preferLocalBuild = true;
-    allowSubstitutes = false;
-  }) buildCommand;
-  mkSharedLib = name: args: runBareCommand "${name}-dynlib" {
-    buildInputs = [ stdenv.cc ] ++ lib.optional stdenv.isDarwin darwin.cctools;
-    libName = "${name}${stdenv.hostPlatform.extensions.sharedLibrary}";
-  } ''
-    mkdir -p $out
-    ${leanc}/bin/leanc -shared ${args} -o $out/$libName
-  '';
-  depRoot = name: deps: mkBareDerivation {
-    name = "${name}-depRoot";
-    inherit deps;
-    depRoots = map (drv: drv.LEAN_PATH) deps;
-
-    passAsFile = [ "deps" "depRoots" ];
-    buildCommand = ''
-      mkdir -p $out
-      for i in $(cat $depRootsPath); do
-        cp -dru --no-preserve=mode $i/. $out
-      done
-      for i in $(cat $depsPath); do
-        cp -drsu --no-preserve=mode $i/. $out
-      done
-    '';
-  };
-  srcRoot = src;
-
-  # A flattened list of Lean-module dependencies (`deps`)
-  allExternalDeps = lib.unique (lib.foldr (dep: allExternalDeps: allExternalDeps ++ [ dep ] ++ dep.allExternalDeps) [] deps);
-  allNativeSharedLibs =
-    lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
-
-  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
-  # plus every dep module itself: `dep.staticLib`
-  allStaticLibDeps =
-    lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
-
-  pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
-
-  leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${pathOfSharedLib dep}") pluginDeps);
-  loadDynlibsOfDeps = deps: lib.unique (concatMap (d: d.propagatedLoadDynlibs) deps);
-
-  # submodules "Init" = ["Init.List.Basic", "Init.Core", ...]
-  submodules = mod: let
-    dir = readDir (modToAbsPath mod);
-    f = p: t:
-      if t == "directory" then
-        submodules "${mod}.${p}"
-      else
-        let m = builtins.match "(.*)\.lean" p;
-        in lib.optional (m != null) "${mod}.${head m}";
-  in concatLists (lib.mapAttrsToList f dir);
-
-  # conservatively approximate list of source files matched by glob
-  expandGlobAllApprox = g:
-    if typeOf g == "string" then
-      # we can't know the required files without parsing dependencies (which is what we want this
-      # function for), so we approximate to the entire package.
-      let root = (head (split "\\." g));
-      in lib.optional (pathExists (src + "/${modToPath root}.lean")) root ++ lib.optionals (pathExists (modToAbsPath root)) (submodules root)
-    else if g.glob == "one" then expandGlobAllApprox g.mod
-    else if g.glob == "submodules" then submodules g.mod
-    else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
-    else throw "unknown glob kind '${g}'";
-  # list of modules that could potentially be involved in the build
-  candidateMods = lib.unique (concatMap expandGlobAllApprox roots);
-  candidateFiles = map modToLean candidateMods;
-  modDepsFile = args.modDepsFile or mkBareDerivation {
-    name = "${name}-deps.json";
-    candidateFiles = lib.concatStringsSep " " candidateFiles;
-    passAsFile = [ "candidateFiles" ];
-    buildCommand = ''
-      mkdir $out
-      ${lean-leanDeps}/bin/lean --deps-json --stdin < $candidateFilesPath > $out/$name
-    '';
-  };
-  modDeps = fromJSON (
-    # the only possible references to store paths in the JSON should be inside errors, so no chance of missed dependencies from this
-    unsafeDiscardStringContext (readFile "${modDepsFile}/${modDepsFile.name}"));
-  # map from module name to list of imports
-  modDepsMap = listToAttrs (lib.zipListsWith lib.nameValuePair candidateMods modDeps.imports);
-  maybeOverrideAttrs = f: x: if f != null then x.overrideAttrs f else x;
-  # build module (.olean and .c) given derivations of all (immediate) dependencies
-  # TODO: make `rec` parts override-compatible?
-  buildMod = mod: deps: maybeOverrideAttrs overrideBuildModAttrs (mkBareDerivation rec {
-    name = "${mod}";
-    LEAN_PATH = depRoot mod deps;
-    LEAN_ABORT_ON_PANIC = "1";
-    relpath = modToPath mod;
-    buildInputs = [ lean ];
-    leanPath = relpath + ".lean";
-    # should be either single .lean file or directory directly containing .lean file plus dependencies
-    src = copyToStoreSafe srcRoot ("/" + leanPath);
-    outputs = [ "out" "ilean" "c" ];
-    oleanPath = relpath + ".olean";
-    ileanPath = relpath + ".ilean";
-    cPath = relpath + ".c";
-    inherit leanFlags leanPluginFlags;
-    leanLoadDynlibFlags = map (p: "--load-dynlib=${pathOfSharedLib p}") (loadDynlibsOfDeps deps);
-    buildCommand = ''
-      dir=$(dirname $relpath)
-      mkdir -p $dir $out/$dir $ilean/$dir $c/$dir
-      if [ -d $src ]; then cp -r $src/. .; else cp $src $leanPath; fi
-      lean -o $out/$oleanPath -i $out/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
-    '';
-  }) // {
-    inherit deps;
-    propagatedLoadDynlibs = loadDynlibsOfDeps deps;
-  };
-  compileMod = mod: drv: mkBareDerivation {
-    name = "${mod}-cc";
-    buildInputs = [ leanc stdenv.cc ];
-    hardeningDisable = [ "all" ];
-    oPath = drv.relpath + ".o";
-    inherit leancFlags;
-    buildCommand = ''
-      mkdir -p $out/$(dirname ${drv.relpath})
-      # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
-      ln -s ${drv.c}/${drv.cPath} src.c
-      # on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
-      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
-    '';
-  };
-  mkMod = mod: deps:
-    let drv = buildMod mod deps;
-        obj = compileMod mod drv;
-        # this attribute will only be used if any dependent module is precompiled
-        sharedLib = mkSharedLib mod "${obj}/${obj.oPath} ${lib.concatStringsSep " " (map (d: pathOfSharedLib d.sharedLib) deps)}";
-    in drv // {
-      inherit obj sharedLib;
-    } // lib.optionalAttrs precompileModules {
-      propagatedLoadDynlibs = [sharedLib];
-    };
-  externalModMap = lib.foldr (dep: depMap: depMap // dep.mods) {} allExternalDeps;
-  # map from module name to derivation
-  modCandidates = mapAttrs (mod: header:
-    let
-      deps = if header.errors == []
-             then map (m: m.module) header.result.imports
-             else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
-    in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
-  expandGlob = g:
-    if typeOf g == "string" then [g]
-    else if g.glob == "one" then [g.mod]
-    else if g.glob == "submodules" then submodules g.mod
-    else if g.glob == "andSubmodules" then [g.mod] ++ submodules g.mod
-    else throw "unknown glob kind '${g}'";
-  # subset of `modCandidates` that is transitively reachable from `roots`
-  mods' = listToAttrs (map (e: { name = e.key; value = modCandidates.${e.key}; }) (genericClosure {
-    startSet = map (m: { key = m; }) (concatMap expandGlob roots);
-    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
-  }));
-  allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
-
-  objects   = mapAttrs (_: m: m.obj) mods';
-  bintools = if stdenv.isDarwin then darwin.cctools else stdenv.cc.bintools.bintools;
-  staticLib = runCommand "${name}-lib" { buildInputs = [ bintools ]; } ''
-    mkdir -p $out
-    ar Trcs $out/lib${libName}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
-  '';
-
-  staticLibLinkWrapper = libs: if groupStaticLibs && !stdenv.isDarwin
-    then "-Wl,--start-group ${libs} -Wl,--end-group"
-    else "${libs}";
-in rec {
-  inherit name lean deps staticLibDeps allNativeSharedLibs allLinkFlags allExternalDeps src objects staticLib modDepsFile;
-  mods = mapAttrs (_: m:
-      m //
-      # if neither precompilation option was set but a dependent module wants to be precompiled, default to precompiling this package whole
-      lib.optionalAttrs (precompilePackage || !precompileModules) { inherit sharedLib; } //
-      lib.optionalAttrs precompilePackage { propagatedLoadDynlibs = [sharedLib]; })
-    mods';
-  modRoot   = depRoot name (attrValues mods);
-  depRoots  = linkFarmFromDrvs "depRoots" (map (m: m.LEAN_PATH) (attrValues mods));
-  cTree     = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
-  oTree     = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
-  iTree     = symlinkJoin { name = "${name}-iTree"; paths = map (mod: mod.ilean) (attrValues mods); };
-  sharedLib = mkSharedLib "lib${sharedLibName}" ''
-    ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
-    ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
-  executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
-      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
-    in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
-      mkdir -p $out/bin
-      leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \
-        -o $out/bin/${executableName} \
-        ${lib.concatStringsSep " " allLinkFlags}
-    '') {};
-})

nix/lake-dev.in

@@ -1,42 +0,0 @@
-#!@bash@/bin/bash
-
-set -euo pipefail
-
-function pebkac() {
-    echo 'This is just a simple Nix adapter for `lake print-paths|serve`.'
-    exit 1
-}
-
-[[ $# -gt 0 ]] || pebkac
-case $1 in
-    --version)
-        # minimum version for `lake serve` with fallback
-        echo 3.1.0
-        ;;
-    print-paths)
-        shift
-        deps="$@"
-        root=.
-        # fall back to initial package if not in package
-        [[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
-        target="$root#print-paths"
-        args=()
-        # HACK: use stage 0 instead of 1 inside Lean's own `src/`
-        [[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@print-paths" && args=@srcArgs@
-        for dep in $deps; do
-            target="$target.\"$dep\""
-        done
-        echo "Building dependencies..." >&2
-        # -v only has "built ...", but "-vv" is a bit too verbose
-        exec @nix@/bin/nix run "$target" ${args[*]} -v
-        ;;
-    serve)
-        shift
-        [[ ${1:-} == "--" ]] && shift
-        # `link-ilean` puts them there
-        LEAN_PATH=${LEAN_PATH:+$LEAN_PATH:}$PWD/build/lib exec $(dirname $0)/lean --server "$@"
-        ;;
-    *)
-        pebkac
-        ;;
-esac

nix/lean-dev.in

@@ -1,28 +0,0 @@
-#!@bash@/bin/bash
-
-set -euo pipefail
-
-root="."
-# find package root
-while [[ "$root" != / ]]; do
-    [ -f "$root/flake.nix" ] && break
-    root="$(realpath "$root/..")"
-done
-# fall back to initial package if not in package
-[[ ! -f "$root/flake.nix" ]] && root="@srcRoot@"
-
-# use Lean w/ package unless in server mode (which has its own LEAN_PATH logic)
-target="$root#lean-package"
-for arg in "$@"; do
-    case $arg in
-        --server | --worker | -v | --version)
-            target="$root#lean"
-            ;;
-    esac
-done
-
-args=(-- "$@")
-# HACK: use stage 0 instead of 1 inside Lean's own `src/`
-[[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@" && args=@srcArgs@
-
-LEAN_SYSROOT="$(dirname "$0")/.." exec @nix@/bin/nix ${LEAN_NIX_ARGS:-} run "$target" ${args[*]}

nix/packages.nix

@@ -1,52 +0,0 @@
-{ src, pkgs, ... } @ args:
-with pkgs;
-let
-  # https://github.com/NixOS/nixpkgs/issues/130963
-  llvmPackages = if stdenv.isDarwin then llvmPackages_11 else llvmPackages_15;
-  cc = (ccacheWrapper.override rec {
-    cc = llvmPackages.clang;
-    extraConfig = ''
-      export CCACHE_DIR=/nix/var/cache/ccache
-      export CCACHE_UMASK=007
-      export CCACHE_BASE_DIR=$NIX_BUILD_TOP
-      # https://github.com/NixOS/nixpkgs/issues/109033
-      args=("$@")
-      for ((i=0; i<"''${#args[@]}"; i++)); do
-        case ''${args[i]} in
-          -frandom-seed=*) unset args[i]; break;;
-        esac
-      done
-      set -- "''${args[@]}"
-      [ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@"
-    '';
-  }).overrideAttrs (old: {
-    # https://github.com/NixOS/nixpkgs/issues/119779
-    installPhase = builtins.replaceStrings ["use_response_file_by_default=1"] ["use_response_file_by_default=0"] old.installPhase;
-  });
-  stdenv' = if stdenv.isLinux then useGoldLinker stdenv else stdenv;
-  lean = callPackage (import ./bootstrap.nix) (args // {
-    stdenv = overrideCC stdenv' cc;
-    inherit src buildLeanPackage llvmPackages;
-  });
-  makeOverridableLeanPackage = f:
-    let newF = origArgs: f origArgs // {
-      overrideArgs = newArgs: makeOverridableLeanPackage f (origArgs // newArgs);
-    };
-    in lib.setFunctionArgs newF (lib.getFunctionArgs f) // {
-      override = args: makeOverridableLeanPackage (f.override args);
-    };
-  buildLeanPackage = makeOverridableLeanPackage (callPackage (import ./buildLeanPackage.nix) (args // {
-    inherit (lean) stdenv;
-    lean = lean.stage1;
-    inherit (lean.stage1) leanc;
-  }));
-in {
-  inherit cc buildLeanPackage llvmPackages;
-  nixpkgs = pkgs;
-  ciShell = writeShellScriptBin "ciShell" ''
-    set -o pipefail
-    export PATH=${moreutils}/bin:$PATH
-    # prefix lines with cumulative and individual execution time
-    "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
-  '';
-} // lean.stage1

nix/templates/pkg/MyPackage.lean

@@ -1 +0,0 @@
-#eval "Hello, world!"

nix/templates/pkg/flake.nix

@@ -1,21 +0,0 @@
-{
-  description = "My Lean package";
-
-  inputs.lean.url = "github:leanprover/lean4";
-  inputs.flake-utils.url = "github:numtide/flake-utils";
-
-  outputs = { self, lean, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
-    let
-      leanPkgs = lean.packages.${system};
-      pkg = leanPkgs.buildLeanPackage {
-        name = "MyPackage";  # must match the name of the top-level .lean file
-        src = ./.;
-      };
-    in {
-      packages = pkg // {
-        inherit (leanPkgs) lean;
-      };
-
-      defaultPackage = pkg.modRoot;
-    });
-}

script/AnalyzeGrindAnnotations.lean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean
+
+namespace Lean.Meta.Grind.Analyzer
+
+
+/-!
+A simple E-matching annotation analyzer.
+For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
+number of instances created.
+For a theorem of the form `params -> type`, the artificial goal is of the form `params -> type -> False`.
+-/
+
+/--
+`grind` configuration for the analyzer. We disable case-splits and lookahead,
+increase the number of generations, and limit the number of instances generated.
+-/
+def config : Grind.Config := {
+  splits       := 0
+  lookahead    := false
+  mbtc         := false
+  ematch       := 20
+  instances    := 100
+  gen          := 10
+}
+
+structure Config where
+  /-- Minimum number of instantiations to trigger summary report -/
+  min : Nat := 10
+  /-- Minimum number of instantiations to trigger detailed report -/
+  detailed : Nat := 50
+
+def mkParams : MetaM Params := do
+  let params ← Grind.mkParams config
+  let ematch ← getEMatchTheorems
+  let casesTypes ← Grind.getCasesTypes
+  return { params with ematch, casesTypes }
+
+/-- Returns the total number of generated instances.  -/
+private def sum (cs : PHashMap Origin Nat) : Nat := Id.run do
+  let mut r := 0
+  for (_, c) in cs do
+    r := r + c
+  return r
+
+private def thmsToMessageData (thms : PHashMap Origin Nat) : MetaM MessageData := do
+  let data := thms.toArray.filterMap fun (origin, c) =>
+    match origin with
+    | .decl declName => some (declName, c)
+    | _ => none
+  let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
+  let data ← data.mapM fun (declName, counter) =>
+    return .trace { cls := `thm } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
+  return .trace { cls := `thm } "instances" data
+
+/--
+Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type,
+and invokes `grind` on it.
+-/
+def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
+  let info ← getConstInfo declName
+  let mvarId ← forallTelescope info.type fun _ type => do
+    withLocalDeclD `h type fun _ => do
+      return (← mkFreshExprMVar (mkConst ``False)).mvarId!
+  let result ← Grind.main mvarId (← mkParams) (pure ())
+  let thms := result.counters.thm
+  let s := sum thms
+  if s > c.min then
+    IO.println s!"{declName} : {s}"
+  if s > c.detailed then
+    logInfo m!"{declName}\n{← thmsToMessageData thms}"
+
+-- Not sure why this is failing: `down_pure` perhaps has an unnecessary universe parameter?
+run_meta analyzeEMatchTheorem ``Std.Do.SPred.down_pure {}
+
+/-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
+def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
+  let origins := (← getEMatchTheorems).getOrigins
+  let decls := origins.filterMap fun | .decl declName => some declName | _ => none
+  for declName in decls.mergeSort Name.lt do
+    try
+      analyzeEMatchTheorem declName c
+    catch e =>
+      logError m!"{declName} failed with {e.toMessageData}"
+  logInfo m!"Finished analyzing {decls.length} theorems"
+
+/-- Macro for analyzing E-match theorems with unlimited heartbeats -/
+macro "#analyzeEMatchTheorems" : command => `(
+  set_option maxHeartbeats 0 in
+  run_meta analyzeEMatchTheorems
+)
+
+#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 {}

script/bench.sh

@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 set -euxo pipefail
 
-cmake --preset release -DUSE_LAKE=ON 1>&2
+cmake --preset release 1>&2
 
 # We benchmark against stage2/bin to test new optimizations.
 timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 23)
+set(LEAN_VERSION_MINOR 24)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -81,7 +81,7 @@ option(USE_MIMALLOC "use mimalloc" ON)
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
-option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" OFF)
+option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
 
 set(LEAN_EXTRA_MAKE_OPTS  ""                           CACHE STRING "extra options to lean --make")
 set(LEANC_CC              ${CMAKE_C_COMPILER}          CACHE STRING "C compiler to use in `leanc`")
@@ -469,6 +469,7 @@ 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")
@@ -502,7 +503,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_1 -lleanshared")
+  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_2 -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
@@ -589,7 +590,7 @@ endif()
 
 add_subdirectory(initialize)
 add_subdirectory(shell)
-# to be included in `leanshared` but not the smaller `leanshared_1` (as it would pull
+# to be included in `leanshared` but not the smaller `leanshared_*` (as it would pull
 # in the world)
 add_library(leaninitialize STATIC $<TARGET_OBJECTS:initialize>)
 set_target_properties(leaninitialize PROPERTIES
@@ -714,6 +715,7 @@ 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}
   )
@@ -734,7 +736,7 @@ else()
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
     VERBATIM)
 
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared")
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")

src/Init/Control/Lawful/Instances.lean

@@ -7,8 +7,10 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import all Init.Control.Except
-public import all Init.Control.State
+public import Init.Control.Except
+import all Init.Control.Except
+public import Init.Control.State
+import all Init.Control.State
 public import Init.Control.StateRef
 public import Init.Ext
 

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

@@ -6,12 +6,18 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
-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.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 Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.Instances
 

src/Init/Conv.lean

@@ -290,13 +290,17 @@ macro "right" : conv => `(conv| rhs)
 /-- `intro` traverses into binders. Synonym for `ext`. -/
 macro "intro" xs:(ppSpace colGt binderIdent)* : conv => `(conv| ext $xs*)
 
-syntax enterArg := binderIdent <|> argArg
+syntax enterPattern := "in " (occs)? term
+
+syntax enterArg := binderIdent <|> argArg <|> enterPattern
 
 /-- `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/Core.lean

@@ -29,6 +29,29 @@ theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
 attribute [grind] id
 
+/--
+A helper gadget for instructing the kernel to eagerly reduce terms.
+
+When the gadget wraps the argument of an application, then when checking that
+the expected and inferred type of the argument match, the kernel will evaluate terms more eagerly.
+It is often used to wrap `Eq.refl true` proof terms as `eagerReduce (Eq.refl true)`
+when using proof by reflection.
+As an example, consider the theorem:
+```
+theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : (p₁.norm == p₂) = true) :
+  p₁.denote ctx = 0 → p₂.denote ctx = 0
+```
+The argument `h : (p₁.norm == p₂) = true` is a candidate for `eagerReduce`.
+When applying this theorem, we would write:
+
+```
+eq_norm ctx p q (eagerReduce (Eq.refl true)) h
+```
+to instruct the kernel to use eager reduction when establishing that `(p.norm == q) = true` is
+definitionally equal to `true = true`.
+-/
+@[expose] def eagerReduce {α : Sort u} (a : α) : α := a
+
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
 since it can sometimes be used to avoid introducing variables.
@@ -78,6 +101,7 @@ instance : DecidableEq Empty := fun a => a.elim
 /-- Decidable equality for PEmpty -/
 instance : DecidableEq PEmpty := fun a => a.elim
 
+set_option genInjectivity false in
 /--
 Delays evaluation. The delayed code is evaluated at most once.
 
@@ -593,6 +617,7 @@ class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/
   sep : (α → Prop) → γ → γ
 
+set_option genInjectivity false in
 /--
 `Task α` is a primitive for asynchronous computation.
 It represents a computation that will resolve to a value of type `α`,
@@ -2499,12 +2524,17 @@ class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
   antisymm (a b : α) : r a b → r b a → a = b
 
-/-- `Asymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
+/-- `Asymm r` means that the binary relation `r` is asymmetric, that is,
 `r a b → ¬ r b a`. -/
 class Asymm (r : α → α → Prop) : Prop where
   /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
   asymm : ∀ a b, r a b → ¬r b a
 
+/-- `Symm r` means that the binary relation `r` is symmetric, that is, `r a b → r b a`.  -/
+class Symm (r : α → α → Prop) : Prop where
+  /-- A symmetric relation satisfies `r a b → r b a`. -/
+  symm : ∀ a b, r a b → r b a
+
 /-- `Total X r` means that the binary relation `r` on `X` is total, that is, that for any
 `x y : X` we have `r x y` or `r y x`. -/
 class Total (r : α → α → Prop) : Prop where

src/Init/Data.lean

@@ -49,5 +49,8 @@ public import Init.Data.Vector
 public import Init.Data.Iterators
 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,7 +9,8 @@ prelude
 public import Init.Data.Array.Mem
 public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Count
-public import all Init.Data.List.Attach
+public import Init.Data.List.Attach
+import all Init.Data.List.Attach
 
 public section
 

src/Init/Data/Array/Basic.lean

@@ -13,8 +13,10 @@ public import Init.Data.UInt.BasicAux
 public import Init.Data.Repr
 public import Init.Data.ToString.Basic
 public import Init.GetElem
-public import all Init.Data.List.ToArrayImpl
-public import all Init.Data.Array.Set
+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 section
 
@@ -163,7 +165,7 @@ representation of arrays. While this is not provable, `Array.usize` always retur
 the array since the implementation only supports arrays of size less than `USize.size`.
 -/
 @[extern "lean_array_size", simp]
-def usize (a : @& Array α) : USize := a.size.toUSize
+def usize (xs : @& Array α) : USize := xs.size.toUSize
 
 /--
 Low-level indexing operator which is as fast as a C array read.
@@ -171,8 +173,8 @@ Low-level indexing operator which is as fast as a C array read.
 This avoids overhead due to unboxing a `Nat` used as an index.
 -/
 @[extern "lean_array_uget", simp, expose]
-def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
-  a[i.toNat]
+def uget (xs : @& Array α) (i : USize) (h : i.toNat < xs.size) : α :=
+  xs[i.toNat]
 
 /--
 Low-level modification operator which is as fast as a C array write. The modification is performed

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/Bootstrap.lean

@@ -8,7 +8,8 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+import all Init.Data.Array.Basic
 
 public section
 
@@ -34,8 +35,8 @@ the index is in bounds. This is because the tactic itself needs to look up value
 arrays.
 -/
 @[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
-def get {α : Type u} (a : @& Array α) (i : @& Nat) (h : LT.lt i a.size) : α :=
-  a.toList.get ⟨i, h⟩
+def get {α : Type u} (xs : @& Array α) (i : @& Nat) (h : LT.lt i xs.size) : α :=
+  xs.toList.get ⟨i, h⟩
 
 /--
 Use the indexing notation `a[i]!` instead.
@@ -43,8 +44,8 @@ Use the indexing notation `a[i]!` instead.
 Access an element from an array, or panic if the index is out of bounds.
 -/
 @[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17"), expose]
-def get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α :=
-  Array.getD a i default
+def get! {α : Type u} [Inhabited α] (xs : @& Array α) (i : @& Nat) : α :=
+  Array.getD xs i default
 
 theorem foldlM_toList.aux [Monad m]
     {f : β → α → m β} {xs : Array α} {i j} (H : xs.size ≤ i + j) {b} :

src/Init/Data/Array/Count.lean

@@ -6,7 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+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,7 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+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,7 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+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,7 +7,8 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
 public import Init.Data.Array.Range

src/Init/Data/Array/Lemmas.lean

@@ -312,7 +312,7 @@ theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {xs : Array α} (h : xs
     xs = xs.pop.push xs.back! := by
   apply ext
   · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
-  · intros i h h'
+  · intro i h h'
     if hlt : i < xs.pop.size then
       rw [getElem_push_lt (h:=hlt), getElem_pop]
     else
@@ -838,9 +838,10 @@ theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α}
   cases as
   simp
 
-theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true := by
+theorem contains_eq_true_of_mem [BEq α] [ReflBEq α] {a : α} {as : Array α} (h : a ∈ as) :
+    as.contains a = true := by
   cases as
-  simpa using h
+  simpa using List.elem_eq_true_of_mem (Array.mem_toList_iff.mpr h)
 
 @[simp] theorem elem_eq_contains [BEq α] {a : α} {xs : Array α} :
     elem a xs = xs.contains a := by
@@ -2893,14 +2894,14 @@ theorem getElem_extract_loop_ge_aux {xs ys : Array α} {size start : Nat} (hge :
   exact Nat.sub_lt_left_of_lt_add hge h
 
 theorem getElem_extract_loop_ge {xs ys : Array α} {size start : Nat} (hge : i ≥ ys.size)
-    (h : i < (extract.loop xs size start ys).size)
-    (h' := getElem_extract_loop_ge_aux hge h) :
-    (extract.loop xs size start ys)[i] = xs[start + i - ys.size] := by
+    (h : i < (extract.loop xs size start ys).size) :
+    (extract.loop xs size start ys)[i] = xs[start + i - ys.size]'(getElem_extract_loop_ge_aux hge h) := by
   induction size using Nat.recAux generalizing start ys with
   | zero =>
     rw [size_extract_loop, Nat.zero_min, Nat.add_zero] at h
     omega
   | succ size ih =>
+    have h' : start + i - ys.size < xs.size := getElem_extract_loop_ge_aux hge h
     have : start < xs.size := by
       apply Nat.lt_of_le_of_lt (Nat.le_add_right start (i - ys.size))
       rwa [← Nat.add_sub_assoc hge]
@@ -2954,7 +2955,7 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} :
   apply List.ext_getElem
   · simp only [length_toList, size_extract, List.length_take, List.length_drop]
     omega
-  · intros n h₁ h₂
+  · intro n h₁ h₂
     simp
 
 @[simp] theorem extract_size {xs : Array α} : xs.extract 0 xs.size = xs := by

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

@@ -12,9 +12,12 @@ public import Init.Data.Array.Lemmas
 public import Init.Data.List.Lex
 import Init.Data.Range.Polymorphic.Lemmas
 import Init.Data.Range.Polymorphic.NatLemmas
+import Init.Data.Order.Lemmas
 
 public section
 
+open Std
+
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
@@ -28,8 +31,8 @@ namespace Array
 @[simp] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
 @[simp] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
-grind_pattern _root_.List.lt_toArray =>  l₁.toArray < l₂.toArray
-grind_pattern _root_.List.le_toArray =>  l₁.toArray ≤ l₂.toArray
+grind_pattern _root_.List.lt_toArray => l₁.toArray < l₂.toArray
+grind_pattern _root_.List.le_toArray => l₁.toArray ≤ l₂.toArray
 grind_pattern lt_toList => xs.toList < ys.toList
 grind_pattern le_toList => xs.toList ≤ ys.toList
 
@@ -100,6 +103,14 @@ theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[
     xs.toList.lex ys.toList lt = xs.lex ys lt := by
   cases xs <;> cases ys <;> simp
 
+instance [LT α] [LE α] [LawfulOrderLT α] [IsLinearOrder α] : IsLinearOrder (Array α) := by
+  apply IsLinearOrder.of_le
+  · constructor
+    intro _ _ hab hba
+    simpa using Std.le_antisymm (α := List α) hab hba
+  · constructor; exact Std.le_trans (α := List α)
+  · constructor; exact fun _ _ => Std.le_total (α := List α)
+
 protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (xs : Array α) : ¬ xs < xs :=
   List.lt_irrefl xs.toList
 
@@ -131,27 +142,35 @@ instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
     Trans (· < · : Array α → Array α → Prop) (· < ·) (· < ·) where
   trans h₁ h₂ := Array.lt_trans h₁ h₂
 
-protected theorem lt_of_le_of_lt [LT α]
-    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
+protected theorem lt_of_le_of_lt [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α]
+    {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
+  Std.lt_of_le_of_lt (α := List α) h₁ h₂
+
+@[deprecated Array.lt_of_le_of_lt (since := "2025-08-01")]
+protected theorem lt_of_le_of_lt' [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
-  List.lt_of_le_of_lt h₁ h₂
+  letI := LE.ofLT α
+  haveI : IsLinearOrder α := IsLinearOrder.of_lt
+  Array.lt_of_le_of_lt h₁ h₂
 
-protected theorem le_trans [LT α]
-    [Std.Irrefl (· < · : α → α → Prop)]
-    [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)]
-    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
+protected theorem le_trans [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
   fun h₃ => h₁ (Array.lt_of_le_of_lt h₂ h₃)
 
-instance [LT α]
-    [Std.Irrefl (· < · : α → α → Prop)]
-    [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)]
-    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)] :
+@[deprecated Array.le_trans (since := "2025-08-01")]
+protected theorem le_trans' [LT α]
+    [i₁ : Std.Asymm (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
+    [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
+    {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
+  letI := LE.ofLT α
+  haveI : IsLinearOrder α := IsLinearOrder.of_lt
+  Array.le_trans h₁ h₂
+
+instance [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] :
     Trans (· ≤ · : Array α → Array α → Prop) (· ≤ ·) (· ≤ ·) where
   trans h₁ h₂ := Array.le_trans h₁ h₂
 
@@ -165,7 +184,7 @@ instance [LT α]
   asymm _ _ := Array.lt_asymm
 
 protected theorem le_total [LT α]
-    [i : Std.Total (¬ · < · : α → α → Prop)] (xs ys : Array α) : xs ≤ ys ∨ ys ≤ xs :=
+    [i : Std.Asymm (· < · : α → α → Prop)] (xs ys : Array α) : xs ≤ ys ∨ ys ≤ xs :=
   List.le_total xs.toList ys.toList
 
 @[simp] protected theorem not_lt [LT α]
@@ -175,19 +194,22 @@ protected theorem le_total [LT α]
     {xs ys : Array α} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
 
 protected theorem le_of_lt [LT α]
-    [i : Std.Total (¬ · < · : α → α → Prop)]
+    [i : Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} (h : xs < ys) : xs ≤ ys :=
   List.le_of_lt h
 
 protected theorem le_iff_lt_or_eq [LT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
-    [Std.Total (¬ · < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} : xs ≤ ys ↔ xs < ys ∨ xs = ys := by
   simpa using List.le_iff_lt_or_eq (l₁ := xs.toList) (l₂ := ys.toList)
 
-instance [LT α]
-    [Std.Total (¬ · < · : α → α → Prop)] :
+protected theorem le_antisymm [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α]
+    {xs ys : Array α} : xs ≤ ys → ys ≤ xs → xs = ys := by
+  simpa using List.le_antisymm (as := xs.toList) (bs := ys.toList)
+
+instance [LT α] [Std.Asymm (· < · : α → α → Prop)] :
     Std.Total (· ≤ · : Array α → Array α → Prop) where
   total := Array.le_total
 
@@ -266,7 +288,6 @@ protected theorem lt_iff_exists [LT α] {xs ys : Array α} :
   simp [List.lt_iff_exists]
 
 protected theorem le_iff_exists [LT α]
-    [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Array α} :
     xs ≤ ys ↔
@@ -286,7 +307,6 @@ theorem append_left_lt [LT α] {xs ys zs : Array α} (h : ys < zs) :
   simpa using List.append_left_lt h
 
 theorem append_left_le [LT α]
-    [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     {xs ys zs : Array α} (h : ys ≤ zs) :
@@ -310,10 +330,8 @@ protected theorem map_lt [LT α] [LT β]
   simpa using List.map_lt w h
 
 protected theorem map_le [LT α] [LT β]
-    [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
-    [Std.Irrefl (· < · : β → β → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
     [Std.Antisymm (¬ · < · : β → β → Prop)]
     {xs ys : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : xs ≤ ys) :

src/Init/Data/Array/MapIdx.lean

@@ -6,11 +6,13 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+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 all Init.Data.List.MapIdx
+public import Init.Data.List.MapIdx
+import all Init.Data.List.MapIdx
 
 public section
 

src/Init/Data/Array/Monadic.lean

@@ -6,8 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.List.Control
-public import all Init.Data.Array.Basic
+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 Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
 public import Init.Data.List.Monadic

src/Init/Data/Array/OfFn.lean

@@ -6,7 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+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,7 +7,8 @@ module
 
 prelude
 public import Init.Data.List.Nat.Perm
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 
 public section

src/Init/Data/Array/QSort/Basic.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Vector.Basic
-public import Init.Data.Ord
+public import Init.Data.Ord.Basic
 
 public section
 

src/Init/Data/Array/Range.lean

@@ -7,8 +7,10 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
-public import all Init.Data.Array.Basic
-public import all Init.Data.Array.OfFn
+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 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,7 +8,8 @@ module
 
 prelude
 public import Init.Data.Array.Basic
-public import all Init.Data.Array.Subarray
+public import Init.Data.Array.Subarray
+import all Init.Data.Array.Subarray
 public import Init.Omega
 
 public section

src/Init/Data/Array/TakeDrop.lean

@@ -6,7 +6,8 @@ Authors: Markus Himmel
 module
 
 prelude
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+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,7 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-public import all Init.Data.Array.Basic
+public import Init.Data.Array.Basic
+import all Init.Data.Array.Basic
 public import Init.Data.Array.TakeDrop
 public import Init.Data.List.Zip
 
@@ -230,11 +231,9 @@ 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/BEq.lean

@@ -23,11 +23,14 @@ class PartialEquivBEq (α) [BEq α] : Prop where
   /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
   trans : (a : α) == b → b == c → a == c
 
+instance [BEq α] [PartialEquivBEq α] : Std.Symm (α := α) (· == ·) where
+  symm _ _ h := PartialEquivBEq.symm h
+
 /-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
 class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 
-theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
-  PartialEquivBEq.symm
+theorem BEq.symm [BEq α] [Std.Symm (α := α) (· == ·)] {a b : α} : a == b → b == a :=
+  Std.Symm.symm a b (r := (· == ·))
 
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩

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
+public import Init.Data.Int.Bitwise.Basic
 public import Init.Data.BitVec.BasicAux
 
 @[expose] public section

src/Init/Data/BitVec/Bitblast.lean

@@ -6,11 +6,14 @@ Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 module
 
 prelude
-public import all Init.Data.Nat.Bitwise.Basic
+public import Init.Data.Nat.Bitwise.Basic
+import all Init.Data.Nat.Bitwise.Basic
 public import Init.Data.Nat.Mod
-public import all Init.Data.Int.DivMod
+public import Init.Data.Int.DivMod
+import all Init.Data.Int.DivMod
 public import Init.Data.Int.LemmasAux
-public import all Init.Data.BitVec.Basic
+public import Init.Data.BitVec.Basic
+import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
@@ -338,11 +341,11 @@ theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
   · rfl
   · simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false,
     Prod.mk.injEq, and_eq_false_imp]
-    intros i
+    intro i
     replace h : (x &&& y).getLsbD i = (0#w).getLsbD i := by rw [h]
     simp only [getLsbD_and, getLsbD_zero, and_eq_false_imp] at h
     constructor
-    · intros hx
+    · intro hx
       simp_all
     · by_cases hx : x.getLsbD i <;> simp_all
 
@@ -1666,7 +1669,7 @@ private theorem neg_udiv_eq_intMin_iff_eq_intMin_eq_one_of_msb_eq_true
     {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = false) :
     -x / y = intMin w ↔ (x = intMin w ∧ y = 1#w) := by
   constructor
-  · intros h
+  · intro h
     rcases w with _ | w; decide +revert
     have : (-x / y).msb = true := by simp [h, msb_intMin]
     rw [msb_udiv] at this
@@ -1742,7 +1745,7 @@ theorem msb_sdiv_eq_decide {x y : BitVec w} :
         Bool.and_self, ne_zero_of_msb_true, decide_false, Bool.and_true, Bool.true_and, Bool.not_true,
         Bool.false_and, Bool.or_false, bool_to_prop]
       have : x / -y ≠ intMin (w + 1) := by
-        intros h
+        intro h
         have : (x / -y).msb = (intMin (w + 1)).msb := by simp only [h]
         simp only [msb_udiv, msb_intMin, show 0 < w + 1 by omega, decide_true, and_eq_true, beq_iff_eq] at this
         obtain ⟨hcontra, _⟩ := this
@@ -1871,7 +1874,7 @@ theorem toInt_dvd_toInt_iff {x y : BitVec w} :
     y.toInt ∣ x.toInt ↔ (if x.msb then -x else x) % (if y.msb then -y else y) = 0#w := by
   constructor
   <;> by_cases hxmsb : x.msb <;> by_cases hymsb: y.msb
-  <;> intros h
+  <;> intro h
   <;> simp only [hxmsb, hymsb, reduceIte, false_eq_true, toNat_eq, toNat_umod, toNat_ofNat,
         zero_mod, toInt_eq_neg_toNat_neg_of_msb_true, Int.dvd_neg, Int.neg_dvd,
         toInt_eq_toNat_of_msb] at h
@@ -2141,7 +2144,7 @@ theorem add_shiftLeft_eq_or_shiftLeft {x y : BitVec w} :
   ext i hi
   simp only [shiftLeft_eq', getElem_and, getElem_shiftLeft, getElem_zero, and_eq_false_imp,
     not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, Nat.not_lt]
-  intros hxi hxval
+  intro hxi hxval
   have : 2^i ≤ x.toNat := two_pow_le_toNat_of_getElem_eq_true hi hxi
   have : i < 2^i := by exact Nat.lt_two_pow_self
   omega
@@ -2152,4 +2155,238 @@ 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,7 +6,9 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B
 module
 
 prelude
-public import all Init.Data.BitVec.Basic
+public import Init.Data.BitVec.Basic
+import all Init.Data.BitVec.Basic
+import Init.Data.Int.Bitwise.Lemmas
 
 public section
 

src/Init/Data/BitVec/Folds.lean

@@ -6,7 +6,8 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
-public import all Init.Data.BitVec.Basic
+public import Init.Data.BitVec.Basic
+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,8 +7,10 @@ module
 
 prelude
 public import Init.Data.Bool
-public import all Init.Data.BitVec.Basic
-public import all Init.Data.BitVec.BasicAux
+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 Init.Data.Fin.Lemmas
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Nat.Div.Lemmas
@@ -19,9 +21,12 @@ public import Init.Data.Int.LemmasAux
 public import Init.Data.Int.Pow
 public import Init.Data.Int.LemmasAux
 public import Init.Data.BitVec.Bootstrap
+public import Init.Data.Order.Factories
 
 public section
 
+open Std
+
 set_option linter.missingDocs true
 
 namespace BitVec
@@ -238,11 +243,11 @@ theorem eq_of_getLsbD_eq_iff {w : Nat} {x y : BitVec w} :
     x = y ↔ ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i := by
   have iff := @BitVec.eq_of_getElem_eq_iff w x y
   constructor
-  · intros heq i lt
+  · intro heq i lt
     have hext := iff.mp heq i lt
     simp only [← getLsbD_eq_getElem] at hext
     exact hext
-  · intros heq
+  · intro heq
     exact iff.mpr heq
 
 theorem eq_of_getMsbD_eq {x y : BitVec w}
@@ -505,6 +510,18 @@ 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]
@@ -818,14 +835,14 @@ its most significant bit is true.
 theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
   have := toInt_eq_msb_cond x
   constructor
-  · intros h
+  · intro h
     apply Classical.byContradiction
-    intros hmsb
+    intro hmsb
     simp only [Bool.not_eq_true] at hmsb
     simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this
     simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h
     omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/
-  · intros h
+  · intro h
     simp only [h, ↓reduceIte] at this
     simp only [BitVec.slt, this, toInt_zero, decide_eq_true_eq]
     omega
@@ -2094,7 +2111,7 @@ theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) :
     (x >>> n).toInt = x.toNat >>> n := by
   rw [toInt_eq_toNat_cond]
   simp only [toNat_ushiftRight, ite_eq_left_iff, Nat.not_lt]
-  intros h
+  intro h
   by_cases hn : n ≤ w
   · have h1 := Nat.mul_lt_mul_of_pos_left (toNat_ushiftRight_lt x n hn) Nat.two_pos
     simp only [toNat_ushiftRight, Nat.zero_lt_succ, Nat.mul_lt_mul_left] at h1
@@ -2189,8 +2206,7 @@ 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, Int.natCast_shiftRight, ofInt_natCast,
-    toNat_ofNat, toNat_ushiftRight]
+  simp only [hxbound, ↓reduceIte, 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
@@ -2232,7 +2248,7 @@ theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
       omega
     · simp only [hi, decide_false, Bool.not_false, Bool.true_and, Bool.eq_and_self,
         decide_eq_true_eq]
-      intros hlsb
+      intro hlsb
       apply BitVec.lt_of_getLsbD hlsb
   · by_cases hi : i ≥ w
     · simp [hi]
@@ -2286,7 +2302,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
   · simp [hw₀]
   · simp only [show ¬(w ≤ w - 1) by omega, decide_false, Bool.not_false, Bool.true_and,
       ite_eq_right_iff]
-    intros h
+    intro h
     simp [show n = 0 by omega]
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
@@ -2774,7 +2790,7 @@ theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ 0#m).toInt = (2 ^ m) * x.toInt := by
   simp only [toInt_append, beq_iff_eq, toInt_zero, toNat_ofNat, Nat.zero_mod, Int.cast_ofNat_Int, Int.add_zero,
     ite_eq_right_iff]
-  intros h
+  intro h
   subst h
   simp [BitVec.eq_nil x]
 
@@ -2958,7 +2974,7 @@ theorem extractLsb'_append_extractLsb'_eq_extractLsb' {x : BitVec w} (h : start
   ext i h
   simp only [getElem_append, getElem_extractLsb', dite_eq_ite, getElem_cast, ite_eq_left_iff,
     Nat.not_lt]
-  intros hi
+  intro hi
   congr 1
   omega
 
@@ -2985,7 +3001,7 @@ theorem signExtend_eq_append_extractLsb' {w v : Nat} {x : BitVec w} :
   · simp only [hx, signExtend_eq_setWidth_of_msb_false, getElem_setWidth, Bool.false_eq_true,
       ↓reduceIte, getElem_append, getElem_extractLsb', Nat.zero_add, getElem_zero, dite_eq_ite,
       Bool.if_false_right, Bool.eq_and_self, decide_eq_true_eq]
-    intros hi
+    intro hi
     have hw : i < w := lt_of_getLsbD hi
     omega
   · simp [signExtend_eq_not_setWidth_not_of_msb_true hx, getElem_append, Nat.lt_min, hi]
@@ -3033,7 +3049,7 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
     · simp only [hlen, ↓reduceDIte]
       ext i hi
       simp only [getElem_extractLsb', getLsbD_append, ite_eq_left_iff, Nat.not_lt]
-      intros hcontra
+      intro hcontra
       omega
     · simp only [hlen, ↓reduceDIte]
       ext i hi
@@ -3480,7 +3496,7 @@ theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
     have := two_mul_toInt_lt (x := y)
     simp only [Nat.add_one_sub_one]
     constructor
-    · intros h
+    · intro h
       rw_mod_cast [← Int.add_bmod_right, Int.bmod_eq_of_le]
       <;> omega
     · have := Int.bmod_neg_iff (x := x.toInt - y.toInt) (m := 2 ^ (w + 1))
@@ -3496,7 +3512,7 @@ theorem twoPow_le_toInt_sub_toInt_iff {x y : BitVec w} :
     have := le_two_mul_toInt (x := y); have := two_mul_toInt_lt (x := y)
     simp only [Nat.add_one_sub_one]
     constructor
-    · intros h
+    · intro h
       simp only [show 0 ≤ x.toInt by omega, show y.toInt < 0 by omega, _root_.true_and]
       rw_mod_cast [← Int.sub_bmod_right, Int.bmod_eq_of_le (by omega) (by omega)]
       omega
@@ -4015,6 +4031,16 @@ protected theorem ne_of_lt {x y : BitVec n} : x < y → x ≠ y := by
   simp only [lt_def, ne_eq, toNat_eq]
   apply Nat.ne_of_lt
 
+instance instIsLinearOrder : IsLinearOrder (BitVec n) := by
+  apply IsLinearOrder.of_le
+  case le_antisymm => constructor; apply BitVec.le_antisymm
+  case le_trans => constructor; apply BitVec.le_trans
+  case le_total => constructor; apply BitVec.le_total
+
+instance instLawfulOrderLT : LawfulOrderLT (BitVec n) := by
+  apply LawfulOrderLT.of_le
+  simpa using fun _ _ => BitVec.lt_asymm
+
 protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y := by
   simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod]
   apply Nat.mod_lt
@@ -5753,40 +5779,6 @@ 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
@@ -5835,6 +5827,362 @@ 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/ByteArray/Basic.lean

@@ -9,18 +9,22 @@ prelude
 public import Init.Data.Array.Basic
 public import Init.Data.Array.DecidableEq
 public import Init.Data.UInt.Basic
-public import all Init.Data.UInt.BasicAux
+public import Init.Data.UInt.BasicAux
+import all Init.Data.UInt.BasicAux
 public import Init.Data.Option.Basic
 
 @[expose] public section
 universe u
 
+set_option genInjectivity false in
 structure ByteArray where
   data : Array UInt8
 
 attribute [extern "lean_byte_array_mk"] ByteArray.mk
 attribute [extern "lean_byte_array_data"] ByteArray.data
 
+gen_injective_theorems% ByteArray
+
 namespace ByteArray
 
 deriving instance BEq for ByteArray

src/Init/Data/Char.lean

@@ -8,5 +8,6 @@ module
 prelude
 public import Init.Data.Char.Basic
 public import Init.Data.Char.Lemmas
+public import Init.Data.Char.Order
 
 public section

src/Init/Data/Char/Lemmas.lean

@@ -6,7 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import all Init.Data.Char.Basic
+public import Init.Data.Char.Basic
+import all Init.Data.Char.Basic
 public import Init.Data.UInt.Lemmas
 
 public section
@@ -61,6 +62,7 @@ instance leTotal : Std.Total (· ≤ · : Char → Char → Prop) where
   total := Char.le_total
 
 -- This instance is useful while setting up instances for `String`.
+@[deprecated ltAsymm (since := "2025-08-01")]
 def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
   total := fun x y => by simpa using Char.le_total y x
 

src/Init/Data/Char/Order.lean

@@ -0,0 +1,27 @@
+/-
+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.Char.Basic
+import Init.Data.Char.Lemmas
+public import Init.Data.Order.Factories
+
+open Std
+
+namespace Char
+
+public instance instIsLinearOrder : IsLinearOrder Char := by
+  apply IsLinearOrder.of_le
+  case le_antisymm => constructor; apply Char.le_antisymm
+  case le_trans => constructor; apply Char.le_trans
+  case le_total => constructor; apply Char.le_total
+
+public instance : LawfulOrderLT Char where
+  lt_iff a b := by
+    simp [← Char.not_le, Decidable.imp_iff_not_or, Std.Total.total]
+
+end Char

src/Init/Data/Dyadic.lean

@@ -0,0 +1,11 @@
+/-
+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

src/Init/Data/Dyadic/Basic.lean

@@ -0,0 +1,659 @@
+/-
+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_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_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
+
+/--
+Convert a rational number `x` to the greatest dyadic number with precision at most `prec`
+which is less than or equal to `x`.
+-/
+def _root_.Rat.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 _root_.Rat.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_nat,
+      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_nat, 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)]
+
+/--
+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
+      rw [Int.negSucc_eq, Int.eq_neg_comm, Int.neg_sub, eq_comm, Int.sub_eq_iff_eq_add] at h
+      simp only [Int.neg_negSucc, h, ← Int.natCast_add_one, Int.add_comm _ k,
+        Nat.succ_eq_add_one, Int.toNat_natCast, 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, succ_eq_add_one, 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

@@ -0,0 +1,60 @@
+/-
+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/Round.lean

@@ -0,0 +1,77 @@
+/-
+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/Lemmas.lean

@@ -12,9 +12,13 @@ public import Init.Ext
 public import Init.ByCases
 public import Init.Conv
 public import Init.Omega
+public import Init.Data.Order.Factories
+import Init.Data.Order.Lemmas
 
 public section
 
+open Std
+
 namespace Fin
 
 @[simp] theorem ofNat_zero (n : Nat) [NeZero n] : Fin.ofNat n 0 = 0 := rfl
@@ -251,6 +255,16 @@ protected theorem le_antisymm_iff {x y : Fin n} : x = y ↔ x ≤ y ∧ y ≤ x
 protected theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
   Fin.le_antisymm_iff.2 ⟨h1, h2⟩
 
+instance instIsLinearOrder : IsLinearOrder (Fin n) := by
+  apply IsLinearOrder.of_le
+  case le_antisymm => constructor; apply Fin.le_antisymm
+  case le_total => constructor; apply Fin.le_total
+  case le_trans => constructor; apply Fin.le_trans
+
+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 = n - (i + 1) := rfl
 
 @[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := Fin.ext <| by

src/Init/Data/Float.lean

@@ -30,6 +30,7 @@ opaque floatSpec : FloatSpec := {
   decLe := fun _ _ => inferInstanceAs (Decidable True)
 }
 
+set_option genInjectivity false in
 /--
 64-bit floating-point numbers.
 
@@ -500,3 +501,5 @@ This function does not reduce in the kernel.
 -/
 @[extern "lean_float_scaleb"]
 opaque Float.scaleB (x : Float) (i : @& Int) : Float
+
+gen_injective_theorems% Float

src/Init/Data/Float32.lean

@@ -23,6 +23,7 @@ opaque float32Spec : FloatSpec := {
   decLe := fun _ _ => inferInstanceAs (Decidable True)
 }
 
+set_option genInjectivity false in
 /--
 32-bit floating-point numbers.
 
@@ -513,3 +514,5 @@ This may lose precision.
 This function does not reduce in the kernel.
 -/
 @[extern "lean_float_to_float32"] opaque Float.toFloat32 : Float → Float32
+
+gen_injective_theorems% Float32

src/Init/Data/FloatArray/Basic.lean

@@ -15,12 +15,15 @@ public import Init.Data.Array.DecidableEq
 public section
 universe u
 
+set_option genInjectivity false in
 structure FloatArray where
   data : Array Float
 
 attribute [extern "lean_float_array_mk"] FloatArray.mk
 attribute [extern "lean_float_array_data"] FloatArray.data
 
+gen_injective_theorems% FloatArray
+
 namespace FloatArray
 
 deriving instance BEq for FloatArray

src/Init/Data/Int/Basic.lean

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

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

@@ -50,4 +50,21 @@ protected def shiftRight : Int → Nat → Int
 
 instance : HShiftRight Int Nat Int := ⟨.shiftRight⟩
 
+/--
+Bitwise left shift, usually accessed via the `<<<` operator.
+
+Examples:
+ * `1 <<< 2 = 4`
+ * `1 <<< 3 = 8`
+ * `0 <<< 3 = 0`
+ * `0xf1 <<< 4 = 0xf10`
+ * `(-1) <<< 3 = -8`
+-/
+@[expose]
+protected def shiftLeft : Int → Nat → Int
+  | Int.ofNat n, s => Int.ofNat (n <<< s)
+  | Int.negSucc n, s => Int.negSucc (((n + 1) <<< s) - 1)
+
+instance : HShiftLeft Int Nat Int := ⟨.shiftLeft⟩
+
 end Int

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

@@ -7,7 +7,8 @@ module
 
 prelude
 public import Init.Data.Nat.Bitwise.Lemmas
-public import all Init.Data.Int.Bitwise.Basic
+public import Init.Data.Int.Bitwise.Basic
+import all Init.Data.Int.Bitwise.Basic
 public import Init.Data.Int.DivMod.Lemmas
 
 public section
@@ -16,8 +17,8 @@ namespace Int
 
 theorem shiftRight_eq (n : Int) (s : Nat) : n >>> s = Int.shiftRight n s := rfl
 
-@[simp]
-theorem natCast_shiftRight (n s : Nat) : (n : Int) >>> s = n >>> s := rfl
+@[simp, norm_cast]
+theorem natCast_shiftRight (n s : Nat) : n >>> s = (n : Int) >>> s := rfl
 
 @[simp]
 theorem negSucc_shiftRight (m n : Nat) :
@@ -37,11 +38,11 @@ theorem shiftRight_eq_div_pow (m : Int) (n : Nat) :
   · rw [negSucc_ediv _ (by norm_cast; exact Nat.pow_pos (Nat.zero_lt_two))]
     rfl
 
-@[simp]
+@[simp, grind =]
 theorem zero_shiftRight (n : Nat) : (0 : Int) >>> n = 0 := by
   simp [Int.shiftRight_eq_div_pow]
 
-@[simp]
+@[simp, grind =]
 theorem shiftRight_zero (n : Int) : n >>> 0 = n := by
   simp [Int.shiftRight_eq_div_pow]
 
@@ -67,7 +68,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
-      simp
+      rw [ofNat_eq_coe]
       omega
   case _ _ _ m =>
     omega
@@ -88,4 +89,94 @@ 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 _ _ = _
+  match n with
+  | Int.ofNat n
+  | Int.negSucc n => simp [Int.shiftLeft]
+
+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]
+    rw [Nat.shiftLeft_succ, Nat.mul_comm, natCast_mul, ofNat_two]
+  | Int.negSucc m =>
+    dsimp only [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
+  | succ b ih =>
+    rw [shiftLeft_succ, ih, Int.pow_succ, Int.mul_assoc]
+
+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,7 +6,8 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert
 module
 
 prelude
-public import all Init.Data.Ord
+public import Init.Data.Ord.Basic
+import all Init.Data.Ord.Basic
 public import Init.Data.Int.Order
 
 public section

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

@@ -26,6 +26,10 @@ 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⟩
 
@@ -956,6 +960,12 @@ theorem neg_mul_ediv_cancel_left (a b : Int) (h : a ≠ 0) : -(a * b) / a = -b :
 @[simp] theorem emod_one (a : Int) : a % 1 = 0 := by
   simp [emod_def, Int.one_mul, Int.sub_self]
 
+theorem ediv_minus_one (a : Int) : a / (-1) = -a := by
+  simp
+
+theorem emod_minus_one (a : Int) : a % (-1) = 0 := by
+  simp
+
 @[deprecated sub_emod_right (since := "2025-04-11")]
 theorem emod_sub_cancel (x y : Int) : (x - y) % y = x % y :=
   sub_emod_right ..
@@ -1212,6 +1222,26 @@ 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`

src/Init/Data/Int/Lemmas.lean

@@ -361,10 +361,10 @@ theorem negSucc_coe' (n : Nat) : -[n+1] = -↑n - 1 := by
 
 protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = ↑m - ↑n := by
   apply subNatNat_elim m n fun m n i => i = m - n
-  · intros i n
+  · intro i n
     rw [Int.natCast_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
       Int.add_right_neg, Int.add_zero]
-  · intros i n
+  · intro i n
     simp only [negSucc_eq, natCast_add, ofNat_one, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
     rw [Int.add_neg_eq_sub (a := n), ← ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add]
     apply Nat.le_refl
@@ -566,6 +566,9 @@ 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,9 +12,11 @@ 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 all Init.Data.Int.Gcd
+public import Init.Data.Int.Gcd
+import all Init.Data.Int.Gcd
 public import Init.Data.RArray
-public import all Init.Data.AC
+public import Init.Data.AC
+import all Init.Data.AC
 
 public section
 
@@ -37,7 +39,7 @@ inductive Expr where
   | neg (a : Expr)
   | mulL (k : Int) (a : Expr)
   | mulR (a : Expr) (k : Int)
-  deriving Inhabited, BEq
+  deriving Inhabited, @[expose] BEq
 
 @[expose]
 def Expr.denote (ctx : Context) : Expr → Int
@@ -52,7 +54,7 @@ def Expr.denote (ctx : Context) : Expr → Int
 inductive Poly where
   | num (k : Int)
   | add (k : Int) (v : Var) (p : Poly)
-  deriving BEq
+  deriving @[expose] BEq
 
 @[expose]
 protected noncomputable def Poly.beq' (p₁ : Poly) : Poly → Bool :=
@@ -1280,7 +1282,7 @@ noncomputable def diseq_eq_subst_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p
 theorem eq_diseq_subst (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
     : diseq_eq_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
   simp [diseq_eq_subst_cert]
-  intros _ _; subst p₃
+  intro _ _; subst p₃
   intro h₁ h₂
   simp [*]
 
@@ -2121,6 +2123,84 @@ theorem not_le_of_le (ctx : Context) (p₁ p₂ : Poly) : not_le_of_le_cert p₁
   have := not_le_of_le' ctx p₁ p₂ h 0 h₁; simp at this
   simp [*]
 
+theorem natCast_sub (x y : Nat)
+    : (NatCast.natCast (x - y) : Int)
+      =
+      if (NatCast.natCast y : Int) + (-1)*NatCast.natCast x ≤ 0 then
+        (NatCast.natCast x : Int) + -1*NatCast.natCast y
+      else
+        (0 : Int) := by
+  change (↑(x - y) : Int) = if (↑y : Int) + (-1)*↑x ≤ 0 then (↑x : Int) + (-1)*↑y else 0
+  rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.one_mul]
+  rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.one_mul]
+  split
+  next h =>
+    replace h := Int.le_of_sub_nonpos h
+    rw [Int.ofNat_le] at h
+    rw [Int.ofNat_sub h]
+  next h =>
+    have : ¬ (↑y : Int) ≤ ↑x := by
+      intro h
+      replace h := Int.sub_nonpos_of_le h
+      contradiction
+    rw [Int.ofNat_le] at this
+    rw [Lean.Omega.Int.ofNat_sub_eq_zero this]
+
+/-! Helper theorem for linearizing nonlinear terms -/
+
+@[expose] noncomputable def var_eq_cert (x : Var) (k : Int) (p : Poly) : Bool :=
+  Poly.rec (fun _ => false)
+    (fun k₁ x' p' _ => Poly.rec (fun k₂ => k₁ != 0 && x == x' && k == -k₂/k₁) (fun _ _ _ _ => false) p')
+    p
+
+theorem var_eq (ctx : Context) (x : Var) (k : Int) (p : Poly) : var_eq_cert x k p → p.denote' ctx = 0 → x.denote ctx = k := by
+  simp [var_eq_cert]; cases p <;> simp; next k₁ x' p' =>
+  cases p' <;> simp; next k₂ =>
+  intro h₁ _ _; subst x' k; intro h₂
+  replace h₂ := Int.neg_eq_of_add_eq_zero h₂
+  rw [Int.neg_eq_comm] at h₂
+  rw [← h₂]; clear h₂; simp; rw [Int.mul_comm, Int.mul_ediv_cancel]
+  assumption
+
+@[expose] noncomputable def of_var_eq_mul_cert (x : Var) (k : Int) (y : Var) (p : Poly) : Bool :=
+  p.beq' (.add 1 x (.add (-k) y (.num 0)))
+
+theorem of_var_eq_mul (ctx : Context) (x : Var) (k : Int) (y : Var) (p : Poly) : of_var_eq_mul_cert x k y p → x.denote ctx = k * y.denote ctx → p.denote' ctx = 0 := by
+  simp [of_var_eq_mul_cert]; intro _ h; subst p; simp [h]
+  rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.sub_self]
+
+@[expose] noncomputable def of_var_eq_var_cert (x : Var) (y : Var) (p : Poly) : Bool :=
+  p.beq' (.add 1 x (.add (-1) y (.num 0)))
+
+theorem of_var_eq_var (ctx : Context) (x : Var) (y : Var) (p : Poly) : of_var_eq_var_cert x y p → x.denote ctx = y.denote ctx → p.denote' ctx = 0 := by
+  simp [of_var_eq_var_cert]; intro _ h; subst p; simp [h]
+  rw [← Int.sub_eq_add_neg, Int.sub_self]
+
+@[expose] noncomputable def of_var_eq_cert (x : Var) (k : Int) (p : Poly) : Bool :=
+  p.beq' (.add 1 x (.num (-k)))
+
+theorem of_var_eq (ctx : Context) (x : Var) (k : Int) (p : Poly) : of_var_eq_cert x k p → x.denote ctx = k → p.denote' ctx = 0 := by
+  simp [of_var_eq_cert]; intro _ h; subst p; simp [h]
+  rw [← Int.sub_eq_add_neg, Int.sub_self]
+
+theorem eq_one_mul (a : Int) : a = 1*a := by simp
+theorem mul_eq_kk (a b k₁ k₂ k : Int) (h₁ : a = k₁) (h₂ : b = k₂) (h₃ : k₁*k₂ == k) : a*b = k := by simp_all
+theorem mul_eq_kkx (a b k₁ k₂ c k : Int) (h₁ : a = k₁) (h₂ : b = k₂*c) (h₃ : k₁*k₂ == k) : a*b = k*c := by
+  simp at h₃; rw [h₁, h₂, ← Int.mul_assoc, h₃]
+theorem mul_eq_kxk (a b k₁ c k₂ k : Int) (h₁ : a = k₁*c) (h₂ : b = k₂) (h₃ : k₁*k₂ == k) : a*b = k*c := by
+  simp at h₃; rw [h₁, h₂, Int.mul_comm, ← Int.mul_assoc, Int.mul_comm k₂, h₃]
+theorem mul_eq_zero_left (a b : Int) (h : a = 0) : a*b = 0 := by simp [*]
+theorem mul_eq_zero_right (a b : Int) (h : b = 0) : a*b = 0 := by simp [*]
+
+theorem div_eq (a b k : Int) (h : b = k) : a / b = a / k := by simp [*]
+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

@@ -8,9 +8,13 @@ module
 prelude
 public import Init.Data.Int.Lemmas
 public import Init.ByCases
+public import Init.Data.Order.Factories
+import Init.Data.Order.Lemmas
 
 public section
 
+open Std
+
 /-!
 # Results about the order properties of the integers, and the integers as an ordered ring.
 -/
@@ -1415,4 +1419,14 @@ theorem natAbs_eq_iff_mul_eq_zero : natAbs a = n ↔ (a - n) * (a + n) = 0 := by
 @[deprecated natAbs_eq_iff_mul_eq_zero (since := "2025-03-11")]
 abbrev eq_natAbs_iff_mul_eq_zero := @natAbs_eq_iff_mul_eq_zero
 
+instance instIsLinearOrder : IsLinearOrder Int := by
+  apply IsLinearOrder.of_le
+  case le_antisymm => constructor; apply Int.le_antisymm
+  case le_total => constructor; apply Int.le_total
+  case le_trans => constructor; apply Int.le_trans
+
+instance : LawfulOrderLT Int where
+  lt_iff := by
+    simp [← Int.not_le, Decidable.imp_iff_not_or, Std.Total.total]
+
 end Int

src/Init/Data/Int/Pow.lean

@@ -21,6 +21,11 @@ protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
 protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
   rw [Int.mul_comm, Int.pow_succ]
 
+protected theorem pow_add (a : Int) (m n : Nat) : a ^ (m + n) = a ^ m * a ^ n := by
+  induction n with
+  | zero => rw [Nat.add_zero, Int.pow_zero, Int.mul_one]
+  | succ _ ih => rw [Nat.add_succ, Int.pow_succ, Int.pow_succ, ih, Int.mul_assoc]
+
 protected theorem zero_pow {n : Nat} (h : n ≠ 0) : (0 : Int) ^ n = 0 := by
   match n, h with
   | n + 1, _ => simp [Int.pow_succ]
@@ -43,6 +48,8 @@ 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,8 +6,10 @@ Authors: Paul Reichert
 module
 
 prelude
-public import all Init.Data.Iterators.Combinators.Attach
-public import all Init.Data.Iterators.Combinators.Monadic.Attach
+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 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,7 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-public import all Init.Data.Iterators.Combinators.Monadic.Attach
+public import Init.Data.Iterators.Combinators.Monadic.Attach
+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,7 +9,8 @@ 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 all Init.Data.Iterators.Consumers.Monadic.Collect
+public import Init.Data.Iterators.Consumers.Monadic.Collect
+import all Init.Data.Iterators.Consumers.Monadic.Collect
 
 public section
 

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

@@ -6,7 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-public import all Init.Data.Iterators.Combinators.Monadic.ULift
+public import Init.Data.Iterators.Combinators.Monadic.ULift
+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,7 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-public import all Init.Data.Iterators.Combinators.ULift
+public import Init.Data.Iterators.Combinators.ULift
+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,8 +8,10 @@ module
 prelude
 public import Init.Data.Iterators.Lemmas.Basic
 public import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
-public import all Init.Data.Iterators.Consumers.Access
-public import all Init.Data.Iterators.Consumers.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 section
 

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

@@ -8,9 +8,12 @@ module
 prelude
 public import Init.Control.Lawful.MonadLift.Instances
 public import Init.Data.Iterators.Lemmas.Consumers.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 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 section
 

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

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

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

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

src/Init/Data/Iterators/PostconditionMonad.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Data.Subtype
+public import Init.Data.Subtype.Basic
 public import Init.PropLemmas
 
 public section

src/Init/Data/List/Attach.lean

@@ -6,9 +6,10 @@ Authors: Mario Carneiro
 module
 
 prelude
-public import all Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
+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 Init.Data.List.Count
-public import Init.Data.Subtype
+public import Init.Data.Subtype.Basic
 public import Init.BinderNameHint
 
 public section
@@ -123,7 +124,7 @@ theorem attachWith_congr {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Pro
       ⟨x, mem_cons_self⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩ := by
   simp only [attach, attachWith, pmap, map_pmap, cons.injEq, true_and]
   apply pmap_congr_left
-  intros a _ m' _
+  intro a _ m' _
   rfl
 
 @[simp, grind =]

src/Init/Data/List/Basic.lean

@@ -2108,6 +2108,11 @@ def range' : (start len : Nat) → (step : Nat := 1) → List Nat
   | _, 0, _ => []
   | s, n+1, step => s :: range' (s+step) n step
 
+@[simp, grind =] theorem range'_zero : range' s 0 step = [] := rfl
+@[simp, grind =] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
+-- The following theorem is intentionally not a simp lemma.
+theorem range'_succ : range' s (n + 1) step = s :: range' (s + step) n step := rfl
+
 /-! ### zipIdx -/
 
 /--

src/Init/Data/List/Erase.lean

@@ -427,7 +427,7 @@ theorem erase_append_left [LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁
 theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : a ∉ l₁) :
     (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a) := by
   rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right]
-  intros b h' h''; rw [eq_of_beq h''] at h; exact h h'
+  intro b h' h''; rw [eq_of_beq h''] at h; exact h h'
 
 @[grind =]
 theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : List α} :

src/Init/Data/List/FinRange.lean

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

src/Init/Data/List/Find.lean

@@ -11,7 +11,8 @@ 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 all Init.Data.List.Attach
+public import Init.Data.List.Attach
+import all Init.Data.List.Attach
 public import Init.Data.Fin.Lemmas
 
 public section
@@ -1241,9 +1242,9 @@ theorem isNone_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
 /-! ### lookup -/
 
 section lookup
-variable [BEq α] [LawfulBEq α]
+variable [BEq α]
 
-@[simp] theorem lookup_cons_self  {k : α} : ((k,b) :: es).lookup k = some b := by
+@[simp] theorem lookup_cons_self [ReflBEq α] {k : α} : ((k,b) :: es).lookup k = some b := by
   simp [lookup_cons]
 
 @[simp] theorem lookup_singleton {a b : α} : [(a,b)].lookup c = if c == a then some b else none := by
@@ -1262,13 +1263,13 @@ theorem lookup_eq_findSome? {l : List (α × β)} {k : α} :
 
 @[simp, grind =] theorem lookup_eq_none_iff {l : List (α × β)} {k : α} :
     l.lookup k = none ↔ ∀ p ∈ l, k != p.1 := by
-  simp [lookup_eq_findSome?]
+  simp [lookup_eq_findSome?, bne]
 
 @[simp] theorem lookup_isSome_iff {l : List (α × β)} {k : α} :
     (l.lookup k).isSome ↔ ∃ p ∈ l, k == p.1 := by
   simp [lookup_eq_findSome?]
 
-theorem lookup_eq_some_iff {l : List (α × β)} {k : α} {b : β} :
+theorem lookup_eq_some_iff [LawfulBEq α] {l : List (α × β)} {k : α} {b : β} :
     l.lookup k = some b ↔ ∃ l₁ l₂, l = l₁ ++ (k, b) :: l₂ ∧ ∀ p ∈ l₁, k != p.1 := by
   simp only [lookup_eq_findSome?, findSome?_eq_some_iff]
   constructor
@@ -1298,11 +1299,11 @@ theorem lookup_replicate_of_pos {k : α} (h : 0 < n) :
     (replicate n (a, b)).lookup k = if k == a then some b else none := by
   simp [lookup_replicate, Nat.ne_of_gt h]
 
-theorem lookup_replicate_self {a : α} :
+theorem lookup_replicate_self [ReflBEq α] {a : α} :
     (replicate n (a, b)).lookup a = if n = 0 then none else some b := by
   simp [lookup_replicate]
 
-@[simp] theorem lookup_replicate_self_of_pos {a : α} (h : 0 < n) :
+@[simp] theorem lookup_replicate_self_of_pos [ReflBEq α] {a : α} (h : 0 < n) :
     (replicate n (a, b)).lookup a = some b := by
   simp [lookup_replicate_self, Nat.ne_of_gt h]
 

src/Init/Data/List/Lemmas.lean

@@ -9,8 +9,10 @@ module
 prelude
 public import Init.Data.Bool
 public import Init.Data.Option.Lemmas
-public import all Init.Data.List.BasicAux
-public import all Init.Data.List.Control
+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 Init.Control.Lawful.Basic
 public import Init.BinderPredicates
 
@@ -70,7 +72,7 @@ See also
 
 Further results, which first require developing further automation around `Nat`, appear in
 * `Init.Data.List.Nat.Basic`: miscellaneous lemmas
-* `Init.Data.List.Nat.Range`: `List.range` and `List.enum`
+* `Init.Data.List.Nat.Range`: `List.range`, `List.range'` and `List.enum`
 * `Init.Data.List.Nat.TakeDrop`: `List.take` and `List.drop`
 
 Also
@@ -1084,6 +1086,12 @@ theorem getLast?_tail {l : List α} : (tail l).getLast? = if l.length = 1 then n
     rw [if_neg]
     rintro ⟨⟩
 
+@[simp, grind =]
+theorem cons_head_tail (h : l ≠ []) : l.head h :: l.tail = l := by
+  induction l with
+  | nil => contradiction
+  | cons ih => simp_all
+
 /-! ## Basic operations -/
 
 /-! ### map -/
@@ -1851,6 +1859,10 @@ theorem append_eq_map_iff {f : α → β} :
 theorem sum_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
   induction l₁ generalizing l₂ <;> simp_all [Nat.add_assoc]
 
+@[simp, grind =]
+theorem sum_reverse_nat (xs : List Nat) : xs.reverse.sum = xs.sum := by
+  induction xs <;> simp_all [Nat.add_comm]
+
 /-! ### concat
 
 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.

src/Init/Data/List/Lex.lean

@@ -8,9 +8,13 @@ module
 prelude
 public import Init.Data.List.Lemmas
 public import Init.Data.List.Nat.TakeDrop
+public import Init.Data.Order.Factories
+import Init.Data.Order.Lemmas
 
 public section
 
+open Std
+
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
@@ -18,6 +22,11 @@ namespace List
 
 /-! ### Lexicographic ordering -/
 
+instance [LT α] [Std.Asymm (α := List α) (· < ·)] : LawfulOrderLT (List α) where
+  lt_iff := by
+    simp only [LE.le, List.le, Classical.not_not, iff_and_self]
+    apply Std.Asymm.asymm
+
 @[simp] theorem lex_lt [LT α] {l₁ l₂ : List α} : Lex (· < ·) l₁ l₂ ↔ l₁ < l₂ := Iff.rfl
 @[simp] theorem not_lex_lt [LT α] {l₁ l₂ : List α} : ¬ Lex (· < ·) l₁ l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 
@@ -79,7 +88,6 @@ theorem not_cons_lex_cons_iff [DecidableEq α] [DecidableRel r] {a b} {l₁ l₂
   rw [cons_lex_cons_iff, not_or, Decidable.not_and_iff_or_not, and_or_left]
 
 theorem cons_le_cons_iff [LT α]
-    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     {a b} {l₁ l₂ : List α} :
@@ -101,19 +109,22 @@ theorem cons_le_cons_iff [LT α]
         exact ⟨i₂.antisymm _ _ h₃ h₁, h₂⟩
   · rintro (h | ⟨h₁, h₂⟩)
     · left
-      exact ⟨i₁.asymm _ _ h, fun w => i₀.irrefl _ (w ▸ h)⟩
+      exact ⟨i₁.asymm _ _ h, fun w => Irrefl.irrefl _ (w ▸ h)⟩
     · right
-      exact ⟨fun w => i₀.irrefl _ (h₁ ▸ w), h₂⟩
+      exact ⟨fun w => Irrefl.irrefl _ (h₁ ▸ w), h₂⟩
 
 theorem not_lt_of_cons_le_cons [LT α]
-    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
     [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : ¬ b < a := by
   rw [cons_le_cons_iff] at h
   rcases h with h | ⟨rfl, h⟩
   · exact i₁.asymm _ _ h
-  · exact i₀.irrefl _
+  · exact Irrefl.irrefl _
+
+theorem left_le_left_of_cons_le_cons [LT α] [LE α] [IsLinearOrder α]
+    [LawfulOrderLT α] {a b : α} {l₁ l₂ : List α} (h : a :: l₁ ≤ b :: l₂) : a ≤ b := by
+  simpa [not_lt] using not_lt_of_cons_le_cons h
 
 theorem le_of_cons_le_cons [LT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
@@ -165,11 +176,7 @@ instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
 
 
 
-protected theorem lt_of_le_of_lt [LT α]
-    [i₀ : Std.Irrefl (· < · : α → α → Prop)]
-    [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
-    [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
+protected theorem lt_of_le_of_lt [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α]
     {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ := by
   induction h₂ generalizing l₁ with
   | nil => simp_all
@@ -179,11 +186,8 @@ protected theorem lt_of_le_of_lt [LT α]
     | nil => simp_all
     | cons c l₁ =>
       apply Lex.rel
-      replace h₁ := not_lt_of_cons_le_cons h₁
-      apply Classical.byContradiction
-      intro h₂
-      have := i₃.trans h₁ h₂
-      contradiction
+      replace h₁ := left_le_left_of_cons_le_cons h₁
+      exact lt_of_le_of_lt h₁ hab
   | cons w₃ ih =>
     rename_i a as bs
     cases l₁ with
@@ -193,21 +197,34 @@ protected theorem lt_of_le_of_lt [LT α]
       by_cases w₅ : a = c
       · subst w₅
         exact Lex.cons (ih (le_of_cons_le_cons h₁))
-      · exact Lex.rel (Classical.byContradiction fun w₆ => w₅ (i₂.antisymm _ _ w₄ w₆))
+      · simp only [not_lt] at w₄
+        exact Lex.rel (lt_of_le_of_ne w₄ (w₅.imp Eq.symm))
 
-protected theorem le_trans [LT α]
-    [Std.Irrefl (· < · : α → α → Prop)]
+@[deprecated List.lt_of_le_of_lt (since := "2025-08-01")]
+protected theorem lt_of_le_of_lt' [LT α]
+    [Std.Asymm (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
+    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
+    {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ < l₃) : l₁ < l₃ :=
+  letI : LE α := .ofLT α
+  haveI : IsLinearOrder α := IsLinearOrder.of_lt
+  List.lt_of_le_of_lt h₁ h₂
+
+protected theorem le_trans [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α]
+    {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
+  fun h₃ => h₁ (List.lt_of_le_of_lt h₂ h₃)
+
+@[deprecated List.le_trans (since := "2025-08-01")]
+protected theorem le_trans' [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {l₁ l₂ l₃ : List α} (h₁ : l₁ ≤ l₂) (h₂ : l₂ ≤ l₃) : l₁ ≤ l₃ :=
-  fun h₃ => h₁ (List.lt_of_le_of_lt h₂ h₃)
+  letI := LE.ofLT α
+  haveI : IsLinearOrder α := IsLinearOrder.of_lt
+  List.le_trans h₁ h₂
 
-instance [LT α]
-    [Std.Irrefl (· < · : α → α → Prop)]
-    [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Antisymm (¬ · < · : α → α → Prop)]
-    [Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)] :
+instance [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α] :
     Trans (· ≤ · : List α → List α → Prop) (· ≤ ·) (· ≤ ·) where
   trans h₁ h₂ := List.le_trans h₁ h₂
 
@@ -247,14 +264,21 @@ theorem not_lex_total {r : α → α → Prop}
     obtain (_ | _) := not_lex_total h l₁ l₂ <;> contradiction
 
 protected theorem le_total [LT α]
-    [i : Std.Total (¬ · < · : α → α → Prop)] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
-  not_lex_total i.total l₂ l₁
+    [i : Std.Asymm (· < · : α → α → Prop)] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
+  not_lex_total i.total_not.total l₂ l₁
 
-instance [LT α]
-    [Std.Total (¬ · < · : α → α → Prop)] :
+protected theorem le_total_of_asymm [LT α]
+    [i : Std.Asymm (· < · : α → α → Prop)] (l₁ l₂ : List α) : l₁ ≤ l₂ ∨ l₂ ≤ l₁ :=
+  List.le_total l₁ l₂
+
+instance [LT α] [Std.Asymm (· < · : α → α → Prop)] :
     Std.Total (· ≤ · : List α → List α → Prop) where
   total := List.le_total
 
+@[no_expose]
+instance instIsLinearOrder [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α] :
+    IsLinearOrder (List α) := IsLinearOrder.of_le
+
 @[simp] protected theorem not_lt [LT α]
     {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 
@@ -262,7 +286,7 @@ instance [LT α]
     {l₁ l₂ : List α} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Classical.not_not
 
 protected theorem le_of_lt [LT α]
-    [i : Std.Total (¬ · < · : α → α → Prop)]
+    [i : Std.Asymm (· < · : α → α → Prop)]
     {l₁ l₂ : List α} (h : l₁ < l₂) : l₁ ≤ l₂ := by
   obtain (h' | h') := List.le_total l₁ l₂
   · exact h'
@@ -272,7 +296,7 @@ protected theorem le_of_lt [LT α]
 protected theorem le_iff_lt_or_eq [LT α]
     [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
-    [Std.Total (¬ · < · : α → α → Prop)]
+    [Std.Asymm (· < · : α → α → Prop)]
     {l₁ l₂ : List α} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂ := by
   constructor
   · intro h
@@ -456,7 +480,6 @@ protected theorem lt_iff_exists [LT α] {l₁ l₂ : List α} :
   simp
 
 protected theorem le_iff_exists [LT α]
-    [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)] {l₁ l₂ : List α} :
     l₁ ≤ l₂ ↔
@@ -480,7 +503,6 @@ theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
   | cons a l₁ ih => simp [cons_lt_cons_iff, ih]
 
 theorem append_left_le [LT α]
-    [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
     {l₁ l₂ l₃ : List α} (h : l₂ ≤ l₃) :
@@ -514,10 +536,8 @@ protected theorem map_lt [LT α] [LT β]
     simp [cons_lt_cons_iff, w, h]
 
 protected theorem map_le [LT α] [LT β]
-    [Std.Irrefl (· < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     [Std.Antisymm (¬ · < · : α → α → Prop)]
-    [Std.Irrefl (· < · : β → β → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
     [Std.Antisymm (¬ · < · : β → β → Prop)]
     {l₁ l₂ : List α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : l₁ ≤ l₂) :

src/Init/Data/List/MapIdx.lean

@@ -61,7 +61,7 @@ proof that the index is valid.
 `List.mapIdxM` is a variant that does not provide the function with evidence that the index is
 valid.
 -/
-@[inline] def mapFinIdxM [Monad m] (as : List α) (f : (i : Nat) → α → (h : i < as.length) → m β) : m (List β) :=
+@[inline, expose] def mapFinIdxM [Monad m] (as : List α) (f : (i : Nat) → α → (h : i < as.length) → m β) : m (List β) :=
   go as #[] (by simp)
 where
   /-- Auxiliary for `mapFinIdxM`:
@@ -78,7 +78,7 @@ found, returning the list of results.
 `List.mapFinIdxM` is a variant that additionally provides the function with a proof that the index
 is valid.
 -/
-@[inline] def mapIdxM [Monad m] (f : Nat → α → m β) (as : List α) : m (List β) := go as #[] where
+@[inline, expose] def mapIdxM [Monad m] (f : Nat → α → m β) (as : List α) : m (List β) := go as #[] where
   /-- Auxiliary for `mapIdxM`:
   `mapIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]` -/
   @[specialize] go : List α → Array β → m (List β)

src/Init/Data/List/MinMax.lean

@@ -8,9 +8,14 @@ module
 prelude
 public import Init.Data.List.Lemmas
 public import Init.Data.List.Pairwise
+public import Init.Data.Order.Factories
+public import Init.Data.Subtype.Order
+import Init.Data.Order.Lemmas
 
 public section
 
+open Std
+
 /-!
 # Lemmas about `List.min?` and `List.max?.
 -/
@@ -55,7 +60,7 @@ theorem min?_eq_head? {α : Type u} [Min α] {l : List α}
       have hx : min x y = x := rel_of_pairwise_cons h mem_cons_self
       rw [foldl_cons, ih _ (hx.symm ▸ h.sublist (by simp)), hx]
 
-theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
+theorem min?_mem [Min α] [MinEqOr α] :
     {xs : List α} → xs.min? = some a → a ∈ xs := by
   intro xs
   match xs with
@@ -72,13 +77,10 @@ theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b
       have p := ind _ eq
       cases p with
       | inl p =>
-        cases min_eq_or x y with | _ q => simp [p, q]
+        cases MinEqOr.min_eq_or x y with | _ q => simp [p, q]
       | inr p => simp [p, mem_cons]
 
--- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.
-
-theorem le_min?_iff [Min α] [LE α]
-    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) :
+theorem le_min?_iff [Min α] [LE α] [LawfulOrderInf α] :
     {xs : List α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b
   | nil => by simp
   | cons x xs => by
@@ -93,34 +95,64 @@ theorem le_min?_iff [Min α] [LE α]
       simp at eq
       simp [ih _ eq, le_min_iff, and_assoc]
 
--- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
--- and `le_min_iff`.
-theorem min?_eq_some_iff [Min α] [LE α]
-    (le_refl : ∀ a : α, a ≤ a)
-    (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
-    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α}
-    (anti : ∀ a b, a ∈ xs → b ∈ xs → a ≤ b → b ≤ a → a = b := by
-      exact fun a b _ _ => Std.Antisymm.antisymm a b) :
+theorem min?_eq_some_iff [Min α] [LE α] {xs : List α} [IsLinearOrder α] [LawfulOrderMin α] :
     xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
-  refine ⟨fun h => ⟨min?_mem min_eq_or h, (le_min?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩
+  refine ⟨fun h => ⟨min?_mem h, (le_min?_iff h).1 (le_refl _)⟩, ?_⟩
   intro ⟨h₁, h₂⟩
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
-    exact congrArg some <| anti _ _ (min?_mem min_eq_or rfl) h₁
-      ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
-      (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))
+    rw [List.min?]
+    exact congrArg some <| le_antisymm
+      ((le_min?_iff (xs := x :: xs) rfl).1 (le_refl _) _ h₁)
+      (h₂ _ (min?_mem (xs := x :: xs) rfl))
 
-theorem min?_replicate [Min α] {n : Nat} {a : α} (w : min a a = a) :
+private theorem min?_attach [Min α] [MinEqOr α] {xs : List α} :
+    xs.attach.min? = (xs.min?.pmap (fun m hm => ⟨m, min?_mem hm⟩) (fun _ => id)) := by
+  cases xs with
+  | nil => simp
+  | cons x xs =>
+    simp only [min?, attach_cons, Option.some.injEq, Option.pmap_some]
+    rw [foldl_map]
+    simp only [Subtype.ext_iff]
+    rw [← foldl_attach (l := xs)]
+    apply Eq.trans (foldl_hom (f := Subtype.val) ?_).symm
+    · rfl
+    · intros; rfl
+
+theorem min?_eq_min?_attach [Min α] [MinEqOr α] {xs : List α} :
+    xs.min? = (xs.attach.min?.map Subtype.val) := by
+  simp [min?_attach, Option.map_pmap]
+
+theorem min?_eq_some_iff_subtype [Min α] [LE α] {xs : List α}
+    [MinEqOr α] [IsLinearOrder (Subtype (· ∈ xs))] [LawfulOrderMin (Subtype (· ∈ xs))] :
+    xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
+  have := fun a => min?_eq_some_iff (xs := xs.attach) (a := a)
+  rw [min?_eq_min?_attach]
+  simp [min?_eq_some_iff]
+  constructor
+  · rintro ⟨ha, h⟩
+    exact ⟨ha, h⟩
+  · rintro ⟨ha, h⟩
+    exact ⟨ha, h⟩
+
+theorem min?_replicate [Min α] [Std.IdempotentOp (min : α → α → α)] {n : Nat} {a : α} :
     (replicate n a).min? = if n = 0 then none else some a := by
   induction n with
   | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons']
+  | succ n ih => cases n <;> simp_all [replicate_succ, min?_cons', Std.IdempotentOp.idempotent]
 
-@[simp] theorem min?_replicate_of_pos [Min α] {n : Nat} {a : α} (w : min a a = a) (h : 0 < n) :
+@[simp] theorem min?_replicate_of_pos [Min α] [MinEqOr α] {n : Nat} {a : α} (h : 0 < n) :
     (replicate n a).min? = some a := by
-  simp [min?_replicate, Nat.ne_of_gt h, w]
+  simp [min?_replicate, Nat.ne_of_gt h]
 
+/--
+This lemma is also applicable given the following instances:
+
+```
+[LE α] [Min α] [IsLinearOrder α] [LawfulOrderMin α]
+```
+-/
 theorem foldl_min [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
     {l : List α} {a : α} : l.foldl (init := a) min = min a (l.min?.getD a) := by
   cases l <;> simp [min?, foldl_assoc, Std.IdempotentOp.idempotent]
@@ -144,54 +176,124 @@ theorem isSome_max?_of_mem {l : List α} [Max α] {a : α} (h : a ∈ l) :
     l.max?.isSome := by
   cases l <;> simp_all [max?_cons']
 
-theorem max?_mem [Max α] (min_eq_or : ∀ a b : α, max a b = a ∨ max a b = b) :
-    {xs : List α} → xs.max? = some a → a ∈ xs
-  | nil => by simp
-  | cons x xs => by
-    rw [max?]; rintro ⟨⟩
-    induction xs generalizing x with simp at *
-    | cons y xs ih =>
-      rcases ih (max x y) with h | h <;> simp [h]
-      simp [← or_assoc, min_eq_or x y]
-
--- See also `Init.Data.List.Nat.Basic` for specialisations of the next two results to `Nat`.
-
-theorem max?_le_iff [Max α] [LE α]
-    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) :
-    {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b ∈ xs, b ≤ x
-  | nil => by simp
-  | cons x xs => by
-    rw [max?]; rintro ⟨⟩ y
-    induction xs generalizing x with
+theorem max?_eq_head? {α : Type u} [Max α] {l : List α}
+    (h : l.Pairwise (fun a b => max a b = a)) : l.max? = l.head? := by
+  cases l with
+  | nil => rfl
+  | cons x l =>
+    rw [head?_cons, max?_cons', Option.some.injEq]
+    induction l generalizing x with
     | nil => simp
-    | cons y xs ih => simp [ih, max_le_iff, and_assoc]
+    | cons y l ih =>
+      have hx : max x y = x := rel_of_pairwise_cons h mem_cons_self
+      rw [foldl_cons, ih _ (hx.symm ▸ h.sublist (by simp)), hx]
 
--- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
--- and `le_min_iff`.
-theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm (· ≤ · : α → α → Prop)]
-    (le_refl : ∀ a : α, a ≤ a)
-    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
-    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
-    xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
-  refine ⟨fun h => ⟨max?_mem max_eq_or h, (max?_le_iff max_le_iff h).1 (le_refl _)⟩, ?_⟩
+theorem max?_mem [Max α] [MaxEqOr α] :
+    {xs : List α} → xs.max? = some a → a ∈ xs := by
+  intro xs
+  match xs with
+  | nil => simp
+  | x :: xs =>
+    simp only [max?_cons', Option.some.injEq, mem_cons]
+    intro eq
+    induction xs generalizing x with
+    | nil =>
+      simp at eq
+      simp [eq]
+    | cons y xs ind =>
+      simp at eq
+      have p := ind _ eq
+      cases p with
+      | inl p =>
+        cases MaxEqOr.max_eq_or x y with | _ q => simp [p, q]
+      | inr p => simp [p, mem_cons]
+
+theorem max?_le_iff [Max α] [LE α] [LawfulOrderSup α] :
+    {xs : List α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b, b ∈ xs → b ≤ x
+  | nil => by simp
+  | cons x xs => by
+    rw [max?]
+    intro eq y
+    simp only [Option.some.injEq] at eq
+    induction xs generalizing x with
+    | nil =>
+      simp at eq
+      simp [eq]
+    | cons z xs ih =>
+      simp at eq
+      simp [ih _ eq, max_le_iff, and_assoc]
+
+theorem max?_eq_some_iff [Max α] [LE α] {xs : List α} [IsLinearOrder (α)]
+    [LawfulOrderMax α] : xs.max? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → b ≤ a := by
+  refine ⟨fun h => ⟨max?_mem h, (max?_le_iff h).1 (le_refl _)⟩, ?_⟩
   intro ⟨h₁, h₂⟩
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
-    exact congrArg some <| anti.1 _ _
-      (h₂ _ (max?_mem max_eq_or (xs := x::xs) rfl))
-      ((max?_le_iff max_le_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
+    rw [List.max?]
+    exact congrArg some <| le_antisymm
+      (h₂ _ (max?_mem (xs := x :: xs) rfl))
+      ((max?_le_iff (xs := x :: xs) rfl).1 (le_refl _) _ h₁)
 
-theorem max?_replicate [Max α] {n : Nat} {a : α} (w : max a a = a) :
+private theorem max?_attach [Max α] [MaxEqOr α] {xs : List α} :
+    xs.attach.max? = (xs.max?.pmap (fun m hm => ⟨m, max?_mem hm⟩) (fun _ => id)) := by
+  cases xs with
+  | nil => simp
+  | cons x xs =>
+    simp only [max?, attach_cons, Option.some.injEq, Option.pmap_some]
+    rw [foldl_map]
+    simp only [Subtype.ext_iff]
+    rw [← foldl_attach (l := xs)]
+    apply Eq.trans (foldl_hom (f := Subtype.val) ?_).symm
+    · rfl
+    · intros; rfl
+
+theorem max?_eq_max?_attach [Max α] [MaxEqOr α] {xs : List α} :
+    xs.max? = (xs.attach.max?.map Subtype.val) := by
+  simp [max?_attach, Option.map_pmap]
+
+theorem max?_eq_some_iff_subtype [Max α] [LE α] {xs : List α}
+    [MaxEqOr α] [IsLinearOrder (Subtype (· ∈ xs))]
+    [LawfulOrderMax (Subtype (· ∈ xs))] :
+    xs.max? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → b ≤ a := by
+  have := fun a => max?_eq_some_iff (xs := xs.attach) (a := a)
+  rw [max?_eq_max?_attach]
+  simp [max?_eq_some_iff]
+  constructor
+  · rintro ⟨ha, h⟩
+    exact ⟨ha, h⟩
+  · rintro ⟨ha, h⟩
+    exact ⟨ha, h⟩
+
+@[deprecated max?_eq_some_iff (since := "2025-08-01")]
+theorem max?_eq_some_iff_legacy [Max α] [LE α] [anti : Std.Antisymm (· ≤ · : α → α → Prop)]
+    (le_refl : ∀ a : α, a ≤ a)
+    (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
+    (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :
+    xs.max? = some a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a := by
+  haveI : MaxEqOr α := ⟨max_eq_or⟩
+  haveI : LawfulOrderMax α := .of_max_le_iff (fun _ _ _ => max_le_iff _ _ _) max_eq_or
+  haveI : Refl (α := α) (· ≤ ·) := ⟨le_refl⟩
+  haveI : IsLinearOrder α := .of_refl_of_antisymm_of_lawfulOrderMax
+  apply max?_eq_some_iff
+
+theorem max?_replicate [Max α] [Std.IdempotentOp (max : α → α → α)] {n : Nat} {a : α} :
     (replicate n a).max? = if n = 0 then none else some a := by
   induction n with
   | zero => rfl
-  | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons']
+  | succ n ih => cases n <;> simp_all [replicate_succ, max?_cons', Std.IdempotentOp.idempotent]
 
-@[simp] theorem max?_replicate_of_pos [Max α] {n : Nat} {a : α} (w : max a a = a) (h : 0 < n) :
+@[simp] theorem max?_replicate_of_pos [Max α] [MaxEqOr α] {n : Nat} {a : α} (h : 0 < n) :
     (replicate n a).max? = some a := by
-  simp [max?_replicate, Nat.ne_of_gt h, w]
+  simp [max?_replicate, Nat.ne_of_gt h]
 
+/--
+This lemma is also applicable given the following instances:
+
+```
+[LE α] [Min α] [IsLinearOrder α] [LawfulOrderMax α]
+```
+-/
 theorem foldl_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
     {l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a) := by
   cases l <;> simp [max?, foldl_assoc, Std.IdempotentOp.idempotent]

src/Init/Data/List/Monadic.lean

@@ -10,7 +10,8 @@ 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 all Init.Data.List.Control
+public import Init.Data.List.Control
+import all Init.Data.List.Control
 
 public section
 

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

@@ -10,6 +10,7 @@ public import Init.Data.List.Count
 public import Init.Data.List.Find
 public import Init.Data.List.MinMax
 public import Init.Data.Nat.Lemmas
+import Init.Data.Nat.Order
 
 public section
 
@@ -210,12 +211,10 @@ theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃
 /-! ### min? -/
 
 -- A specialization of `min?_eq_some_iff` to Nat.
+@[deprecated min?_eq_some_iff (since := "2025-08-08")]
 theorem min?_eq_some_iff' {xs : List Nat} :
-    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
-  min?_eq_some_iff
-    (le_refl := Nat.le_refl)
-    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
-    (le_min_iff := fun _ _ _ => Nat.le_min)
+    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) := by
+  exact min?_eq_some_iff
 
 theorem min?_get_le_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
     l.min?.get (isSome_min?_of_mem h) ≤ a := by
@@ -237,12 +236,10 @@ theorem min?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) : l.min?.ge
 /-! ### max? -/
 
 -- A specialization of `max?_eq_some_iff` to Nat.
+@[deprecated max?_eq_some_iff (since := "2025-08-08")]
 theorem max?_eq_some_iff' {xs : List Nat} :
     xs.max? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
   max?_eq_some_iff
-    (le_refl := Nat.le_refl)
-    (max_eq_or := fun _ _ => Nat.max_def .. ▸ by split <;> simp)
-    (max_le_iff := fun _ _ _ => Nat.max_le)
 
 theorem le_max?_get_of_mem {l : List Nat} {a : Nat} (h : a ∈ l) :
     a ≤ l.max?.get (isSome_max?_of_mem h) := by

src/Init/Data/List/Nat/Pairwise.lean

@@ -61,10 +61,10 @@ theorem pairwise_iff_getElem {l : List α} : Pairwise R l ↔
     ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
   rw [pairwise_iff_forall_sublist]
   constructor <;> intro h
-  · intros i j hi hj h'
+  · intro i j hi hj h'
     apply h
     simpa [h'] using map_getElem_sublist (is := [⟨i, hi⟩, ⟨j, hj⟩])
-  · intros a b h'
+  · intro a b h'
     have ⟨is, h', hij⟩ := sublist_eq_map_getElem h'
     rcases is with ⟨⟩ | ⟨a', ⟨⟩ | ⟨b', ⟨⟩⟩⟩ <;> simp at h'
     rcases h' with ⟨rfl, rfl⟩

src/Init/Data/List/Nat/Range.lean

@@ -58,7 +58,7 @@ theorem pairwise_lt_range' {s n} (step := 1) (pos : 0 < step := by simp) :
   | s, n + 1, step, pos => by
     simp only [range'_succ, pairwise_cons]
     constructor
-    · intros n m
+    · intro n m
       rw [mem_range'] at m
       omega
     · exact pairwise_lt_range' (s := s + step) step pos
@@ -70,7 +70,7 @@ theorem pairwise_le_range' {s n} (step := 1) :
   | s, n + 1, step => by
     simp only [range'_succ, pairwise_cons]
     constructor
-    · intros n m
+    · intro n m
       rw [mem_range'] at m
       omega
     · exact pairwise_le_range' (s := s + step) step
@@ -90,28 +90,27 @@ theorem map_sub_range' {a s : Nat} (h : a ≤ s) (n : Nat) :
   rintro rfl
   omega
 
-theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k) := by
+theorem range'_eq_append_iff : range' s n step = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k step ∧ ys = range' (s + k * step) (n - k) step := by
   induction n generalizing s xs ys with
   | zero => simp
   | succ n ih =>
     simp only [range'_succ]
     rw [cons_eq_append_iff]
+    have add_mul' (k n m : Nat) : (n + m) * k = m * k + n * k := by rw [Nat.add_mul]; omega
     constructor
     · rintro (⟨rfl, rfl⟩ | ⟨_, rfl, h⟩)
       · exact ⟨0, by simp [range'_succ]⟩
       · simp only [ih] at h
         obtain ⟨k, h, rfl, rfl⟩ := h
         refine ⟨k + 1, ?_⟩
-        simp_all [range'_succ]
-        omega
+        simp_all [range'_succ, Nat.add_assoc]
     · rintro ⟨k, h, rfl, rfl⟩
       cases k with
       | zero => simp [range'_succ]
       | succ k =>
-        simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, range'_inj, exists_eq_left', or_true, and_true, false_or]
+        simp only [range'_succ, reduceCtorEq, false_and, cons.injEq, true_and, ih, exists_eq_left', false_or]
         refine ⟨k, ?_⟩
-        simp_all
-        omega
+        simp_all [Nat.add_assoc]
 
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
@@ -178,6 +177,46 @@ theorem count_range_1' {a s n} :
     specialize h (a - s)
     omega
 
+@[simp, grind =]
+theorem sum_range' : (range' start n step).sum = n * start + n * (n - 1) * step / 2 := by
+  induction n generalizing start with
+  | zero => simp
+  | succ n ih =>
+    simp_all only [List.range'_succ, List.sum_cons, Nat.mul_add, ← Nat.add_assoc,
+      Nat.add_mul, Nat.one_mul, Nat.add_one_sub_one]
+    have : n * step + n * (n - 1) * step / 2 = (n * n * step + n * step) / 2 := by
+      apply Nat.eq_div_of_mul_eq_left (by omega)
+      rw [Nat.add_mul, Nat.div_mul_cancel]
+      · calc  n * step * 2 + n * (n - 1) * step
+          _ = n * step * 2 + n * step * (n - 1) := by simp [Nat.mul_comm, Nat.mul_assoc]
+          _ = n * step + n * step * n := by cases n <;> simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
+          _ = n * n * step + n * step := by simp [Nat.mul_comm, Nat.add_comm, Nat.mul_left_comm]
+      · have : 2 ∣ n ∨ 2 ∣ (n - 1) := by omega
+        apply Nat.dvd_mul_right_of_dvd
+        apply Nat.dvd_mul.mpr
+        cases this with
+        | inl h => exists 2, 1; omega
+        | inr h => exists 1, 2; omega
+    omega
+
+@[simp, grind =]
+theorem drop_range' : (List.range' start n step).drop k = List.range' (start + k * step) (n - k) step := by
+  induction k generalizing start n with
+  | zero => simp
+  | succ => cases n <;> simp [*, List.range'_succ, Nat.add_mul, ← Nat.add_assoc, Nat.add_right_comm]
+
+@[simp, grind =]
+theorem take_range'_of_length_le (h : n ≤ k) : (List.range' start n step).take k = List.range' start n step := by
+  induction n generalizing start k with
+  | zero => simp
+  | succ n ih => cases k <;> simp_all [List.range'_succ]
+
+@[simp, grind =]
+theorem take_range'_of_length_ge (h : n ≥ k) : (List.range' start n step).take k = List.range' start k step := by
+  induction k generalizing start n with
+  | zero => simp
+  | succ k ih => cases n <;> simp_all [List.range'_succ]
+
 /-! ### range -/
 
 theorem reverse_range' : ∀ {s n : Nat}, reverse (range' s n) = map (s + n - 1 - ·) (range n)
@@ -355,9 +394,7 @@ theorem zipIdx_eq_append_iff {l : List α} {k : Nat} :
     simp only [length_range'] at h
     obtain rfl := h
     refine ⟨ws, xs, rfl, ?_⟩
-    simp only [zipIdx_eq_zip_range', length_append, true_and]
-    congr
-    omega
+    simp [zipIdx_eq_zip_range', length_append]
   · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
     simp only [zipIdx_eq_zip_range']
     refine ⟨l₁', l₂', range' k l₁'.length, range' (k + l₁'.length) l₂'.length, ?_⟩

src/Init/Data/List/Perm.lean

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

src/Init/Data/List/Range.lean

@@ -29,30 +29,31 @@ open Nat
 
 /-! ### range' -/
 
-theorem range'_succ {s n step} : range' s (n + 1) step = s :: range' (s + step) n step := by
-  simp [range']
-
-@[simp] theorem length_range' {s step} : ∀ {n : Nat}, length (range' s n step) = n
+@[simp, grind =] theorem length_range' {s step} : ∀ {n : Nat}, length (range' s n step) = n
   | 0 => rfl
   | _ + 1 => congrArg succ length_range'
 
-@[simp] theorem range'_eq_nil_iff : range' s n step = [] ↔ n = 0 := by
+@[simp, grind =] theorem range'_eq_nil_iff : range' s n step = [] ↔ n = 0 := by
   rw [← length_eq_zero_iff, length_range']
 
 theorem range'_ne_nil_iff (s : Nat) {n step : Nat} : range' s n step ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[simp] theorem range'_zero : range' s 0 step = [] := by
-  simp
+theorem range'_eq_cons_iff : range' s n step = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + step) (n - 1) step := by
+  induction n generalizing s with
+  | zero => simp
+  | succ n ih =>
+    simp only [range'_succ]
+    simp only [cons.injEq, and_congr_right_iff]
+    rintro rfl
+    simp [eq_comm]
 
-@[simp] theorem range'_one {s step : Nat} : range' s 1 step = [s] := rfl
-
-@[simp] theorem tail_range' : (range' s n step).tail = range' (s + step) (n - 1) step := by
+@[simp, grind =] theorem tail_range' : (range' s n step).tail = range' (s + step) (n - 1) step := by
   cases n with
   | zero => simp
   | succ n => simp [range'_succ]
 
-@[simp] theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by
+@[simp, grind =] theorem range'_inj : range' s n = range' s' n' ↔ n = n' ∧ (n = 0 ∨ s = s') := by
   constructor
   · intro h
     have h' := congrArg List.length h
@@ -81,14 +82,14 @@ theorem getElem?_range' {s step} :
     exact (getElem?_range' (s := s + step) (by exact succ_lt_succ_iff.mp h)).trans <| by
       simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
 
-@[simp] theorem getElem_range' {n m step} {i} (H : i < (range' n m step).length) :
+@[simp, grind =] theorem getElem_range' {n m step} {i} (H : i < (range' n m step).length) :
     (range' n m step)[i] = n + step * i :=
   (getElem?_eq_some_iff.1 <| getElem?_range' (by simpa using H)).2
 
 theorem head?_range' : (range' s n).head? = if n = 0 then none else some s := by
   induction n <;> simp_all [range'_succ]
 
-@[simp] theorem head_range' (h) : (range' s n).head h = s := by
+@[simp, grind =] theorem head_range' (h) : (range' s n).head h = s := by
   repeat simp_all [head?_range', head_eq_iff_head?_eq_some]
 
 theorem map_add_range' {a} : ∀ s n step, map (a + ·) (range' s n step) = range' (a + s) n step
@@ -107,7 +108,7 @@ theorem range'_append : ∀ {s m n step : Nat},
     simpa [range', Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
       using range'_append (s := s + step)
 
-@[simp] theorem range'_append_1 {s m n : Nat} :
+@[simp, grind =] theorem range'_append_1 {s m n : Nat} :
     range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)
 
 theorem range'_sublist_right {s m n : Nat} : range' s m step <+ range' s n step ↔ m ≤ n :=
@@ -129,15 +130,6 @@ theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ [
 theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ [s + n] := by
   simp [range'_concat]
 
-theorem range'_eq_cons_iff : range' s n = a :: xs ↔ s = a ∧ 0 < n ∧ xs = range' (a + 1) (n - 1) := by
-  induction n generalizing s with
-  | zero => simp
-  | succ n ih =>
-    simp only [range'_succ]
-    simp only [cons.injEq, and_congr_right_iff]
-    rintro rfl
-    simp [eq_comm]
-
 /-! ### range -/
 
 @[simp, grind =] theorem range_one : range 1 = [0] := rfl
@@ -152,7 +144,7 @@ theorem range_eq_range' {n : Nat} : range n = range' 0 n :=
 theorem getElem?_range {i n : Nat} (h : i < n) : (range n)[i]? = some i := by
   simp [range_eq_range', getElem?_range' h]
 
-@[simp] theorem getElem_range (h : j < (range n).length) : (range n)[j] = j := by
+@[simp, grind =] theorem getElem_range (h : j < (range n).length) : (range n)[j] = j := by
   simp [range_eq_range']
 
 theorem range_succ_eq_map {n : Nat} : range (n + 1) = 0 :: map succ (range n) := by
@@ -162,23 +154,23 @@ theorem range_succ_eq_map {n : Nat} : range (n + 1) = 0 :: map succ (range n) :=
 theorem range'_eq_map_range {s n : Nat} : range' s n = map (s + ·) (range n) := by
   rw [range_eq_range', map_add_range']; rfl
 
-@[simp] theorem length_range {n : Nat} : (range n).length = n := by
+@[simp, grind =] theorem length_range {n : Nat} : (range n).length = n := by
   simp only [range_eq_range', length_range']
 
-@[simp] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by
+@[simp, grind =] theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0 := by
   rw [← length_eq_zero_iff, length_range]
 
 theorem range_ne_nil {n : Nat} : range n ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[simp] theorem tail_range : (range n).tail = range' 1 (n - 1) := by
+@[simp, grind =] theorem tail_range : (range n).tail = range' 1 (n - 1) := by
   rw [range_eq_range', tail_range']
 
-@[simp]
+@[simp, grind =]
 theorem range_sublist {m n : Nat} : range m <+ range n ↔ m ≤ n := by
   simp only [range_eq_range', range'_sublist_right]
 
-@[simp]
+@[simp, grind =]
 theorem range_subset {m n : Nat} : range m ⊆ range n ↔ m ≤ n := by
   simp only [range_eq_range', range'_subset_right, lt_succ_self]
 
@@ -196,7 +188,7 @@ theorem head?_range {n : Nat} : (range n).head? = if n = 0 then none else some 0
     simp only [range_succ, head?_append, ih]
     split <;> simp_all
 
-@[simp] theorem head_range {n : Nat} (h) : (range n).head h = 0 := by
+@[simp, grind =] theorem head_range {n : Nat} (h) : (range n).head h = 0 := by
   cases n with
   | zero => simp at h
   | succ n => simp [head?_range, head_eq_iff_head?_eq_some]
@@ -208,7 +200,7 @@ theorem getLast?_range {n : Nat} : (range n).getLast? = if n = 0 then none else
     simp only [range_succ, getLast?_append, ih]
     split <;> simp_all
 
-@[simp] theorem getLast_range {n : Nat} (h) : (range n).getLast h = n - 1 := by
+@[simp, grind =] theorem getLast_range {n : Nat} (h) : (range n).getLast h = n - 1 := by
   cases n with
   | zero => simp at h
   | succ n => simp [getLast?_range, getLast_eq_iff_getLast?_eq_some]

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

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

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

@@ -7,7 +7,8 @@ module
 
 prelude
 public import Init.Data.List.Perm
-public import all Init.Data.List.Sort.Basic
+public import Init.Data.List.Sort.Basic
+import all Init.Data.List.Sort.Basic
 public import Init.Data.List.Nat.Range
 public import Init.Data.Bool
 
@@ -352,7 +353,7 @@ where go : ∀ (i : Nat) (l : List α),
     rw [merge_stable]
     · rw [go, go]
     · simp only [mem_mergeSort, Prod.forall]
-      intros j x k y mx my
+      intro j x k y mx my
       have := mem_zipIdx mx
       have := mem_zipIdx my
       simp_all

src/Init/Data/List/TakeDrop.lean

@@ -6,7 +6,8 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module
 
 prelude
-public import all Init.Data.List.Basic
+public import Init.Data.List.Basic
+import all Init.Data.List.Basic
 public import Init.Data.List.Lemmas
 
 public section
@@ -68,9 +69,9 @@ theorem take_of_length_le {l : List α} (h : l.length ≤ i) : take i l = l := b
 theorem lt_length_of_take_ne_self {l : List α} {i} (h : l.take i ≠ l) : i < l.length :=
   gt_of_not_le (mt take_of_length_le h)
 
-@[simp] theorem drop_length {l : List α} : l.drop l.length = [] := drop_of_length_le (Nat.le_refl _)
+@[simp, grind =] theorem drop_length {l : List α} : l.drop l.length = [] := drop_of_length_le (Nat.le_refl _)
 
-@[simp] theorem take_length {l : List α} : l.take l.length = l := take_of_length_le (Nat.le_refl _)
+@[simp, grind =] theorem take_length {l : List α} : l.take l.length = l := take_of_length_le (Nat.le_refl _)
 
 @[simp]
 theorem getElem_cons_drop : ∀ {l : List α} {i : Nat} (h : i < l.length),