fix grind tests

This PR add `@[grind]` annotations for HashMap and variants.

.github/workflows/build-template.yml

@@ -46,7 +46,7 @@ jobs:
       CCACHE_DIR: ${{ github.workspace }}/.ccache
       CCACHE_COMPRESS: true
       # current cache limit
-      CCACHE_MAXSIZE: 600M
+      CCACHE_MAXSIZE: 400M
       # squelch error message about missing nixpkgs channel
       NIX_BUILD_SHELL: bash
       LSAN_OPTIONS: max_leaks=10
@@ -82,7 +82,7 @@ jobs:
       - name: CI Merge Checkout
         run: |
           git fetch --depth=1 origin ${{ github.sha }}
-          git checkout FETCH_HEAD flake.nix flake.lock
+          git checkout FETCH_HEAD flake.nix flake.lock script/prepare-*
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
       - name: Setup emsdk
@@ -99,7 +99,6 @@ jobs:
         if: matrix.cmultilib
       - name: Cache
         id: restore-cache
-        if: matrix.name != 'Linux Lake'
         uses: actions/cache/restore@v4
         with:
           # NOTE: must be in sync with `save` below

.github/workflows/ci.yml

@@ -139,20 +139,21 @@ jobs:
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
             let matrix = [
+              /* TODO: to be updated to new LLVM
               {
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
                 "binary-check": "ldd -v",
                 // foreign code may be linked against more recent glibc
                 // reverse-ffi needs to be updated to link to LLVM libraries
                 "CTEST_OPTIONS": "-E 'foreign|leanlaketest_reverse-ffi'",
                 "CMAKE_OPTIONS": "-DLLVM=ON -DLLVM_CONFIG=${GITHUB_WORKSPACE}/build/llvm-host/bin/llvm-config"
-              },
+              }, */
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
@@ -160,25 +161,23 @@ jobs:
                 "release": true,
                 "check-level": 0,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "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'"
               },
-              // deactivated due to bugs
-              /*
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
-                // just a secondary PR build job for now
-                "check-level": isPr ? 0 : 3,
+                "check-level": 0,
+                // just a secondary build job for now until false positives can be excluded
                 "secondary": true,
                 "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
-                // TODO: why does this fail?
-                "CTEST_OPTIONS": "-E 'scopedMacros'"
+                // TODO: importStructure is not compatible with .olean caching
+                // TODO: why does scopedMacros fail?
+                "CTEST_OPTIONS": "-E 'scopedMacros|importStructure'"
               },
-              */
               {
                 "name": "Linux",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
@@ -210,7 +209,7 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-apple-darwin.tar.zst",
+                "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
@@ -221,7 +220,7 @@ jobs:
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-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
@@ -242,7 +241,7 @@ jobs:
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 // for reasons unknown, interactivetests are flaky on Windows
                 "CTEST_OPTIONS": "--repeat until-pass:2",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
+                "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"
               },
@@ -253,20 +252,21 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
+                "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*"
               },
-              {
-                "name": "Linux 32bit",
-                "os": "ubuntu-latest",
-                // Use 32bit on stage0 and stage1 to keep oleans compatible
-                "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
-                "cmultilib": true,
-                "release": true,
-                "check-level": 2,
-                "cross": true,
-                "shell": "bash -euxo pipefail {0}"
-              }
+              // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation
+              //{
+              //  "name": "Linux 32bit",
+              //  "os": "ubuntu-latest",
+              //  // Use 32bit on stage0 and stage1 to keep oleans compatible
+              //  "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
+              //  "cmultilib": true,
+              //  "release": true,
+              //  "check-level": 2,
+              //  "cross": true,
+              //  "shell": "bash -euxo pipefail {0}"
+              //}
               // {
               //   "name": "Web Assembly",
               //   "os": "ubuntu-latest",

.github/workflows/nix-ci.yml

@@ -73,7 +73,7 @@ jobs:
         with:
           extra-conf: |
             extra-sandbox-paths = /nix/var/cache/ccache?
-            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
+            substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org
       - name: Prepare CCache Cache
         run: |
           sudo mkdir -m0770 -p /nix/var/cache/ccache
@@ -103,40 +103,10 @@ jobs:
           paths: push-test/test-results.xml
         if: always()
         continue-on-error: true
-      - name: Build manual
-        run: |
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc#{lean-mdbook,leanInk,alectryon,inked} -o push-doc
-          nix build $NIX_BUILD_ARGS --update-input lean --no-write-lock-file ./doc
-          # https://github.com/netlify/cli/issues/1809
-          cp -r --dereference ./result ./dist
-        if: matrix.name == 'Nix Linux'
       - name: Rebuild Nix Store Cache
         run: |
           rm -rf nix-store-cache || true
           nix copy ./push-* --to file://$PWD/nix-store-cache?compression=none
-      - id: deploy-info
-        name: Compute Deployment Metadata
-        run: |
-          set -e
-          python3 -c 'import base64; print("alias="+base64.urlsafe_b64encode(bytes.fromhex("${{github.sha}}")).decode("utf-8").rstrip("="))' >> "$GITHUB_OUTPUT"
-          echo "message=`git log -1 --pretty=format:"%s"`" >> "$GITHUB_OUTPUT"
-      - name: Publish manual to Netlify
-        uses: nwtgck/actions-netlify@v3.0
-        id: publish-manual
-        with:
-          publish-dir: ./dist
-          production-branch: master
-          github-token: ${{ secrets.GITHUB_TOKEN }}
-          deploy-message: |
-            ${{ github.event_name == 'pull_request' && format('pr#{0}: {1}', github.event.number, github.event.pull_request.title) || format('ref/{0}: {1}', github.ref_name, steps.deploy-info.outputs.message) }}
-          alias: ${{ steps.deploy-info.outputs.alias }}
-          enable-commit-comment: false
-          enable-pull-request-comment: false
-          github-deployment-environment: "lean-lang.org/lean4/doc"
-          fails-without-credentials: false
-        env:
-          NETLIFY_AUTH_TOKEN: ${{ secrets.NETLIFY_AUTH_TOKEN }}
-          NETLIFY_SITE_ID: "b8e805d2-7e9b-4f80-91fb-a84d72fc4a68"
       - name: Fixup CCache Cache
         run: |
           sudo chown -R $USER /nix/var/cache

CMakeLists.txt

@@ -5,13 +5,15 @@ option(USE_MIMALLOC "use mimalloc" ON)
 # store all variables passed on the command line into CL_ARGS so we can pass them to the stage builds
 # https://stackoverflow.com/a/48555098/161659
 # MUST be done before call to 'project'
-# Use standard release build (discarding LEAN_CXX_EXTRA_FLAGS etc.) for stage0 by default since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..).
+# Use standard release build (discarding LEAN_EXTRA_CXX_FLAGS etc.) for stage0 by default since it is assumed to be "good", but still pass through CMake platform arguments (compiler, toolchain file, ..).
 # Use `STAGE0_` prefix to pass variables to stage0 explicitly.
 get_cmake_property(vars CACHE_VARIABLES)
 foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
   if("${var}" MATCHES "STAGE0_(.*)")
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
+  elseif("${var}" MATCHES "STAGE1_(.*)")
+    list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
     if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
@@ -37,10 +39,14 @@ endif()
 
 # Don't do anything with cadical on wasm
 if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  # On CI Linux, we source cadical from Nix instead; see flake.nix
   find_program(CADICAL cadical)
   if(NOT CADICAL)
     set(CADICAL_CXX c++)
+    if (CADICAL_USE_CUSTOM_CXX)
+      set(CADICAL_CXX ${CMAKE_CXX_COMPILER})
+      set(CADICAL_CXXFLAGS "${LEAN_EXTRA_CXX_FLAGS}")
+      set(CADICAL_LDFLAGS "-Wl,-rpath=\\$$ORIGIN/../lib")
+    endif()
     find_program(CCACHE ccache)
     if(CCACHE)
       set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
@@ -55,8 +61,11 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
       GIT_REPOSITORY https://github.com/arminbiere/cadical
       GIT_TAG rel-2.1.2
       CONFIGURE_COMMAND ""
-      # https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
-      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}
+      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk
+        CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
+        CXX=${CADICAL_CXX}
+        CXXFLAGS=${CADICAL_CXXFLAGS}
+        LDFLAGS=${CADICAL_LDFLAGS}
       BUILD_IN_SOURCE ON
       INSTALL_COMMAND "")
     set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
@@ -77,26 +86,29 @@ if (USE_MIMALLOC)
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-ExternalProject_add(stage0
-  SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
-  SOURCE_SUBDIR src
-  BINARY_DIR stage0
-  # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-  # (however, CI will override this as we need to embed the githash into the stage 1 library built
-  # by stage 0)
-  CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
-  BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
-  INSTALL_COMMAND ""  # skip install
-  DEPENDS ${EXTRA_DEPENDS}
-)
+if (NOT STAGE1_PREV_STAGE)
+  ExternalProject_add(stage0
+    SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
+    SOURCE_SUBDIR src
+    BINARY_DIR stage0
+    # do not rebuild stage0 when git hash changes; it's not from this commit anyway
+    # (however, CI will override this as we need to embed the githash into the stage 1 library built
+    # by stage 0)
+    CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
+    BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
+    INSTALL_COMMAND ""  # skip install
+    DEPENDS ${EXTRA_DEPENDS}
+  )
+  list(APPEND EXTRA_DEPENDS stage0)
+endif()
 ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
-  DEPENDS stage0
+  DEPENDS ${EXTRA_DEPENDS}
   STEP_TARGETS configure
 )
 ExternalProject_add(stage2
@@ -108,6 +120,7 @@ ExternalProject_add(stage2
   INSTALL_COMMAND ""
   DEPENDS stage1
   EXCLUDE_FROM_ALL ON
+  STEP_TARGETS configure
 )
 ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"

CMakePresets.json

@@ -24,9 +24,9 @@
     },
     {
       "name": "reldebug",
-      "displayName": "Release with debug info build config",
+      "displayName": "Release with assertions enabled",
       "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "RelWithDebInfo"
+        "CMAKE_BUILD_TYPE": "RelWithAssert"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/reldebug"

CODEOWNERS

@@ -7,8 +7,9 @@
 /.github/ @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
+/src/library/compiler/ @zwarich
 /src/lake/ @tydeu
-/src/Lean/Compiler/ @leodemoura
+/src/Lean/Compiler/ @leodemoura @zwarich
 /src/Lean/Data/Lsp/ @mhuisi
 /src/Lean/Elab/Deriving/ @kim-em
 /src/Lean/Elab/Tactic/ @kim-em

doc/dev/release_checklist.md

@@ -144,6 +144,10 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     - Run `script/release_steps.py v4.7.0-rc1 <repo>` (e.g. replacing `<repo>` with `batteries`), which will walk you through the following steps:
       - Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.7.0-rc1`.
       - Merge `origin/bump/v4.7.0` if relevant (i.e. `bump-branch: true` appears in `release_repos.yml`).
+      - Otherwise, you *may* need to merge `origin/nightly-testing`.
+      - Note that for `verso` and `reference-manual` development happens on `nightly-testing`, so
+        we will merge that branch into `bump_to_v4.7.0-rc1`, but it is essential in the GitHub interface that we do a rebase merge,
+        in order to preserve the history.
       - Update the contents of `lean-toolchain` to `leanprover/lean4:v4.7.0-rc1`.
       - In the `lakefile.toml` or `lakefile.lean`, if there are dependencies on `nightly-testing`, `bump/v4.7.0`, or specific version tags, update them to the new tag.
         If they depend on `main` or `master`, don't change this; you've just updated the dependency, so `lake update` will take care of modifying the manifest.
@@ -151,7 +155,7 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
       - Run `lake build && if lake check-test; then lake test; fi` to check things are working.
       - Commit the changes as `chore: bump toolchain to v4.7.0-rc1` and push.
       - Create a PR with title "chore: bump toolchain to v4.7.0-rc1".
-    - Merge the PR once CI completes.
+    - Merge the PR once CI completes. (Recall: for `verso` and `reference-manual` you will need to do a rebase merge.)
     - Re-running `script/release_checklist.py` will then create the tag `v4.7.0-rc1` from `master`/`main` and push it (unless `toolchain-tag: false` in the `release_repos.yml` file)
   - We do this for the same list of repositories as for stable releases, see above for notes about special cases.
     As above, there are dependencies between these, and so the process above is iterative.

flake.lock

@@ -1,112 +1,50 @@
 {
   "nodes": {
-    "flake-utils": {
-      "inputs": {
-        "systems": "systems"
-      },
-      "locked": {
-        "lastModified": 1710146030,
-        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
-        "type": "github"
-      },
-      "original": {
-        "owner": "numtide",
-        "repo": "flake-utils",
-        "type": "github"
-      }
-    },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1710889954,
-        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
-        "type": "github"
+        "lastModified": 1745636243,
+        "narHash": "sha256-kbNvlQZf8wwok3d2X1kM/TlXH/MZ+03ZNv+IPPBx+DM=",
+        "rev": "f771eb401a46846c1aebd20552521b233dd7e18b",
+        "type": "tarball",
+        "url": "https://releases.nixos.org/nixos/unstable/nixos-25.05pre789333.f771eb401a46/nixexprs.tar.xz"
       },
       "original": {
-        "owner": "NixOS",
-        "ref": "nixpkgs-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "nixpkgs-cadical": {
-      "locked": {
-        "lastModified": 1740791350,
-        "narHash": "sha256-igS2Z4tVw5W/x3lCZeeadt0vcU9fxtetZ/RyrqsCRQ0=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
-        "type": "github"
+        "type": "tarball",
+        "url": "https://channels.nixos.org/nixos-unstable/nixexprs.tar.xz"
       }
     },
     "nixpkgs-old": {
       "flake": false,
       "locked": {
-        "lastModified": 1581379743,
-        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
-        "type": "github"
+        "lastModified": 1582018169,
+        "narHash": "sha256-qv1iK1IchpZKSeWL3NEs4U5Jl5QVyNHDdiMJvLOI4Yc=",
+        "type": "tarball",
+        "url": "https://releases.nixos.org/nixos/19.03/nixos-19.03.173691.34c7eb7545d/nixexprs.tar.xz"
       },
       "original": {
-        "owner": "NixOS",
-        "ref": "nixos-19.03",
-        "repo": "nixpkgs",
-        "type": "github"
+        "type": "tarball",
+        "url": "https://channels.nixos.org/nixos-19.03/nixexprs.tar.xz"
       }
     },
     "nixpkgs-older": {
       "flake": false,
       "locked": {
-        "lastModified": 1523316493,
-        "narHash": "sha256-5qJS+i5ECICPAKA6FhPLIWkhPKDnOZsZbh2PHYF1Kbs=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "0b307aa73804bbd7a7172899e59ae0b8c347a62d",
-        "type": "github"
+        "lastModified": 1550657948,
+        "narHash": "sha256-BE0XqzNfzvhhtTXv37LyySyq4moL7z1i1hMvwbFNL/I=",
+        "type": "tarball",
+        "url": "https://releases.nixos.org/nixos/18.03/nixos-18.03.133402.cb0e20d6db9/nixexprs.tar.xz"
       },
       "original": {
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "0b307aa73804bbd7a7172899e59ae0b8c347a62d",
-        "type": "github"
+        "type": "tarball",
+        "url": "https://channels.nixos.org/nixos-18.03/nixexprs.tar.xz"
       }
     },
     "root": {
       "inputs": {
-        "flake-utils": "flake-utils",
         "nixpkgs": "nixpkgs",
-        "nixpkgs-cadical": "nixpkgs-cadical",
         "nixpkgs-old": "nixpkgs-old",
         "nixpkgs-older": "nixpkgs-older"
       }
-    },
-    "systems": {
-      "locked": {
-        "lastModified": 1681028828,
-        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
-        "owner": "nix-systems",
-        "repo": "default",
-        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
-        "type": "github"
-      },
-      "original": {
-        "owner": "nix-systems",
-        "repo": "default",
-        "type": "github"
-      }
     }
   },
   "root": "root",

flake.nix

@@ -1,29 +1,22 @@
 {
   description = "Lean development flake. Not intended for end users.";
 
-  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+  # We use channels so we're not affected by GitHub's rate limits
+  inputs.nixpkgs.url = "https://channels.nixos.org/nixos-unstable/nixexprs.tar.xz";
   # old nixpkgs used for portable release with older glibc (2.27)
-  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
+  inputs.nixpkgs-old.url = "https://channels.nixos.org/nixos-19.03/nixexprs.tar.xz";
   inputs.nixpkgs-old.flake = false;
   # old nixpkgs used for portable release with older glibc (2.26)
-  inputs.nixpkgs-older.url = "github:NixOS/nixpkgs/0b307aa73804bbd7a7172899e59ae0b8c347a62d";
+  inputs.nixpkgs-older.url = "https://channels.nixos.org/nixos-18.03/nixexprs.tar.xz";
   inputs.nixpkgs-older.flake = false;
-  # for cadical 2.1.2; sync with CMakeLists.txt by taking commit from https://www.nixhub.io/packages/cadical
-  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/199169a2135e6b864a888e89a2ace345703c025d";
-  inputs.flake-utils.url = "github:numtide/flake-utils";
 
-  outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system:
+  outputs = inputs: builtins.foldl' inputs.nixpkgs.lib.attrsets.recursiveUpdate {} (builtins.map (system:
     let
       pkgs = import inputs.nixpkgs { inherit system; };
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old = import inputs.nixpkgs-older { inherit system; };
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
-      pkgsCadical = import inputs.nixpkgs-cadical { inherit system; };
-      cadical = if pkgs.stdenv.isLinux then
-        # use statically-linked cadical on Linux to avoid glibc versioning troubles
-        pkgsCadical.pkgsStatic.cadical.overrideAttrs { doCheck = false; }
-      else pkgsCadical.cadical;
 
       lean-packages = pkgs.callPackage (./nix/packages.nix) { src = ./.; };
 
@@ -31,7 +24,7 @@
           stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
-            cmake gmp libuv ccache cadical pkg-config
+            cmake gmp libuv ccache pkg-config
             lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI
@@ -67,15 +60,17 @@
           GDB = pkgsDist.gdb;
         });
     in {
-      packages = {
+      packages.${system} = {
         # to be removed when Nix CI is not needed anymore
         inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
         deprecated = lean-packages;
       };
 
-      # The default development shell for working on lean itself
-      devShells.default = devShellWithDist pkgs;
-      devShells.oldGlibc = devShellWithDist pkgsDist-old;
-      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
-    });
+      devShells.${system} = {
+        # The default development shell for working on lean itself
+        default = devShellWithDist pkgs;
+        oldGlibc = devShellWithDist pkgsDist-old;
+        oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
+      };
+    }) ["x86_64-linux" "aarch64-linux"]);
 }

nix/buildLeanPackage.nix

@@ -194,7 +194,7 @@ with builtins; let
   modCandidates = mapAttrs (mod: header:
     let
       deps = if header.errors == []
-             then map (m: m.module) header.imports
+             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:
@@ -206,7 +206,7 @@ with builtins; let
   # 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}.imports) else [];
+    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;
 

script/benchReelabRss.lean

@@ -1,4 +1,5 @@
 import Lean.Data.Lsp
+import Lean.Elab.Import
 open Lean
 open Lean.Lsp
 open Lean.JsonRpc
@@ -7,9 +8,7 @@ open Lean.JsonRpc
 Tests language server memory use by repeatedly re-elaborate a given file.
 
 NOTE: only works on Linux for now.
-
-HACK: The line that is to be prepended with a space is hard-coded below to be sufficiently far down
-not to touch the imports for usual files.
+ot to touch the imports for usual files.
 -/
 
 def main (args : List String) : IO Unit := do
@@ -33,6 +32,8 @@ def main (args : List String) : IO Unit := do
     Ipc.writeRequest ⟨0, "initialize", { capabilities : InitializeParams }⟩
 
     let text ← IO.FS.readFile file
+    let (_, headerEndPos, _) ← Elab.parseImports text
+    let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
     let mut requestNo : Nat := 1
     let mut versionNo : Nat := 1
     Ipc.writeNotification ⟨"textDocument/didOpen", {
@@ -40,15 +41,14 @@ def main (args : List String) : IO Unit := do
     for i in [0:iters.toNat!] do
       if i > 0 then
         versionNo := versionNo + 1
-        let pos := { line := 19, character := 0 }
         let params : DidChangeTextDocumentParams := {
           textDocument := {
             uri      := uri
             version? := versionNo
           }
           contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
-            start := pos
-            «end» := pos
+            start := headerEndPos
+            «end» := headerEndPos
           } " "]
         }
         let params := toJson params

script/merge_remote.py

@@ -47,10 +47,10 @@ def run_command(command, check=True, capture_output=True):
 
 
 def clone_repo(repo, temp_dir):
-    """Clone the repository to a temporary directory using shallow clone."""
-    print(f"Shallow cloning {repo}...")
-    # Keep the shallow clone for efficiency
-    clone_result = run_command(f"gh repo clone {repo} {temp_dir} -- --depth=1", check=False)
+    """Clone the repository to a temporary directory."""
+    print(f"Cloning {repo}...")
+    # Remove shallow clone for better merge detection
+    clone_result = run_command(f"gh repo clone {repo} {temp_dir}", check=False)
     if clone_result.returncode != 0:
         print(f"Failed to clone repository {repo}.")
         print(f"Error: {clone_result.stderr}")
@@ -95,26 +95,16 @@ def check_and_merge(repo, branch, tag, temp_dir):
     if checkout_result.returncode != 0:
         return False
 
-    # Try merging the tag in a dry-run to check if it can be merged cleanly
-    print(f"Checking if {tag} can be merged cleanly into {branch}...")
-    merge_check = run_command(f"git merge --no-commit --no-ff {tag}", check=False)
+    # Try merging the tag directly
+    print(f"Merging {tag} into {branch}...")
+    merge_result = run_command(f"git merge {tag} --no-edit", check=False)
     
-    if merge_check.returncode != 0:
+    if merge_result.returncode != 0:
         print(f"Cannot merge {tag} cleanly into {branch}.")
         print("Merge conflicts would occur. Aborting merge.")
         run_command("git merge --abort")
         return False
     
-    # Abort the test merge
-    run_command("git reset --hard HEAD")
-    
-    # Now perform the actual merge and push to remote
-    print(f"Merging {tag} into {branch}...")
-    merge_result = run_command(f"git merge {tag} --no-edit")
-    if merge_result.returncode != 0:
-        print(f"Failed to merge {tag} into {branch}.")
-        return False
-    
     print(f"Pushing changes to remote...")
     push_result = run_command(f"git push origin {branch}")
     if push_result.returncode != 0:

script/prepare-llvm-linux.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -uo pipefail
+set -euxo pipefail
 
 # run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
 # ```
@@ -14,6 +14,7 @@ set -uo pipefail
 else
   ln -s llvm llvm-host
 fi
+mkdir -p stage0/lib
 mkdir -p stage1/{bin,lib,lib/glibc,include/clang}
 CP="cp -d"  # preserve symlinks
 # a C compiler!
@@ -25,6 +26,8 @@ cp -L llvm/bin/llvm-ar stage1/bin/
 # dependencies of the above
 $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/
 $CP $ZLIB/lib/libz.so* stage1/lib/
+# also copy USE_LLVM deps into stage 0
+$CP llvm/lib/libLLVM*.so* $ZLIB/lib/libz.so* stage0/lib/
 # general clang++ dependency, breaks cross-library C++ exceptions if linked statically
 $CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/
 # bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run)
@@ -39,20 +42,21 @@ $CP $GLIBC/lib/*crt* stage1/lib/
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/{clang_rt.*.o,libclang_rt.builtins*} ../stage1)
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* $GMP/lib/libgmp.a $LIBUV/lib/libuv.a stage1/lib/
-# LLVM 15 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
-# but clang-15 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
+# LLVM 19 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
+# but clang-19 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* llvm/lib/
 $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/
 # libc++ headers are looked up in the host compiler's root, so copy over target-specific includes
-$CP -r llvm/include/*-*-* llvm-host/include/
+$CP -r llvm/include/*-*-* llvm-host/include/ || true
 # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
 $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
 # libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function.
 $CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc
-for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
+for f in $GLIBC/lib/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
 OPTIONS=()
-echo -n " -DLEAN_STANDALONE=ON"
+# We build cadical using the custom toolchain on Linux to avoid glibc versioning issues
+echo -n " -DLEAN_STANDALONE=ON -DCADICAL_USE_CUSTOM_CXX=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
 echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
 # use target compiler directly when not cross-compiling
@@ -64,7 +68,9 @@ fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+# ld.so is usually included by the libc.so linker script but we discard those. Make sure it is linked to only after `libc.so` like in the original
+# linker script so that no libc symbols are bound to it instead.
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
 # when not using the above flags, link GMP dynamically/as usual
 echo -n " -DLEAN_EXTRA_LINKER_FLAGS='-Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests

script/release_checklist.py

@@ -7,6 +7,7 @@ import base64
 import subprocess
 import sys
 import os
+import re # Import re module
 # Import run_command from merge_remote.py
 from merge_remote import run_command
 
@@ -58,13 +59,29 @@ def release_page_exists(repo_url, tag_name, github_token):
     response = requests.get(api_url, headers=headers)
     return response.status_code == 200
 
-def get_release_notes(repo_url, tag_name, github_token):
-    api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/releases/tags/{tag_name}"
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-    response = requests.get(api_url, headers=headers)
-    if response.status_code == 200:
-        return response.json().get("body", "").strip()
-    return None
+def get_release_notes(tag_name):
+    """Fetch release notes page title from lean-lang.org."""
+    # Strip -rcX suffix if present for the URL
+    base_tag = tag_name.split('-')[0]
+    reference_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
+    try:
+        response = requests.get(reference_url)
+        response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx)
+        
+        # Extract title using regex
+        match = re.search(r"<title>(.*?)</title>", response.text, re.IGNORECASE | re.DOTALL)
+        if match:
+            return match.group(1).strip()
+        else:
+            print(f"  ⚠️ Could not find <title> tag in {reference_url}")
+            return None
+            
+    except requests.exceptions.RequestException as e:
+        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
+        return None
+    except Exception as e:
+        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
+        return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + f"/contents/{file_path}?ref={branch}"
@@ -255,6 +272,7 @@ def main():
     branch_name = f"releases/v{version_major}.{version_minor}.0"
     if not branch_exists(lean_repo_url, branch_name, github_token):
         print(f"  ❌ Branch {branch_name} does not exist")
+        print(f"  🟡 After creating the branch, we'll need to check CMake version settings.")
         lean4_success = False
     else:
         print(f"  ✅ Branch {branch_name} exists")
@@ -274,14 +292,22 @@ def main():
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-        release_notes = get_release_notes(lean_repo_url, toolchain, github_token)
-        if not (release_notes and toolchain in release_notes.splitlines()[0].strip()):
-            previous_minor_version = version_minor - 1
-            previous_release = f"v{version_major}.{previous_minor_version}.0"
-            print(f"  ❌ Release notes not published. Please run `script/release_notes.py --since {previous_release}` on branch `{branch_name}`.")
-            lean4_success = False
-        else:
-            print(f"  ✅ Release notes look good.")
+        
+    # Check the actual release notes page title
+    actual_title = get_release_notes(toolchain)
+    expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1"
+
+    if actual_title is None:
+        # Error already printed by get_release_notes
+        lean4_success = False
+    elif not actual_title.startswith(expected_title_prefix):
+        # Construct URL for the error message (using the base tag)
+        base_tag = toolchain.split('-')[0]
+        check_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
+        print(f"  ❌ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {check_url}")
+        lean4_success = False
+    else:
+        print(f"  ✅ Release notes page title looks good ('{actual_title}').")
 
     repo_status["lean4"] = lean4_success
 
@@ -360,10 +386,24 @@ def main():
         if check_stable and not is_release_candidate(toolchain):
             if not is_merged_into_stable(url, toolchain, "stable", github_token, verbose):
                 org_repo = extract_org_repo_from_url(url)
-                print(f"  ❌ Tag {toolchain} is not merged into stable")
-                print(f"     Run `script/merge_remote.py {org_repo} stable {toolchain}` to merge it")
-                repo_status[name] = False
-                continue
+                if args.dry_run:
+                    print(f"  ❌ Tag {toolchain} is not merged into stable")
+                    print(f"     Run `script/merge_remote.py {org_repo} stable {toolchain}` to merge it")
+                    repo_status[name] = False
+                    continue
+                else:
+                    print(f"  … Tag {toolchain} is not merged into stable. Running `script/merge_remote.py {org_repo} stable {toolchain}`...")
+                    
+                    # Run the script to merge the tag
+                    subprocess.run(["script/merge_remote.py", org_repo, "stable", toolchain])
+                    
+                    # Check again if the tag is merged now
+                    if not is_merged_into_stable(url, toolchain, "stable", github_token, verbose):
+                        print(f"  ❌ Manual intervention required.")
+                        repo_status[name] = False
+                        continue
+            
+            # This will print in all successful cases - whether tag was merged initially or was merged successfully
             print(f"  ✅ Tag {toolchain} is merged into stable")
 
         if check_bump:

script/release_repos.yml

@@ -21,12 +21,19 @@ repositories:
     branch: master
     dependencies: []
 
+  - name: lean4-cli
+    url: https://github.com/leanprover/lean4-cli
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: doc-gen4
     url: https://github.com/leanprover/doc-gen4
     toolchain-tag: true
     stable-branch: false
     branch: main
-    dependencies: []
+    dependencies: [lean4-cli]
 
   - name: verso
     url: https://github.com/leanprover/verso
@@ -42,20 +49,13 @@ repositories:
     branch: main
     dependencies: [verso]
 
-  - name: lean4-cli
-    url: https://github.com/leanprover/lean4-cli
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
   - name: ProofWidgets4
     url: https://github.com/leanprover-community/ProofWidgets4
     toolchain-tag: false
     stable-branch: false
     branch: main
     dependencies:
-      - Batteries
+      - batteries
 
   - name: aesop
     url: https://github.com/leanprover-community/aesop
@@ -63,7 +63,7 @@ repositories:
     stable-branch: true
     branch: master
     dependencies:
-      - Batteries
+      - batteries
 
   - name: import-graph
     url: https://github.com/leanprover-community/import-graph
@@ -71,8 +71,8 @@ repositories:
     stable-branch: false
     branch: main
     dependencies:
-      - Cli
-      - Batteries
+      - lean4-cli
+      - batteries
 
   - name: plausible
     url: https://github.com/leanprover-community/plausible
@@ -88,10 +88,11 @@ repositories:
     branch: master
     bump-branch: true
     dependencies:
-      - Aesop
+      - aesop
       - ProofWidgets4
       - lean4checker
-      - Batteries
+      - batteries
+      - lean4-cli
       - doc-gen4
       - import-graph
       - plausible
@@ -102,4 +103,4 @@ repositories:
     stable-branch: true
     branch: master
     dependencies:
-      - Mathlib
+      - mathlib4

script/release_steps.py

@@ -68,7 +68,7 @@ def generate_script(repo, version, config):
     ]
 
     # Special cases for specific repositories
-    if repo_name == "REPL":
+    if repo_name == "repl":
         script_lines.extend([
             "lake update",
             "cd test/Mathlib",
@@ -79,7 +79,7 @@ def generate_script(repo, version, config):
             "./test.sh"
         ])
     elif dependencies:
-        script_lines.append('echo "Please update the dependencies in lakefile.{lean,toml}"')
+        script_lines.append('perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*')
         script_lines.append("lake update")
 
     script_lines.append("")
@@ -89,13 +89,20 @@ def generate_script(repo, version, config):
         ""
     ])
 
-    if re.search(r'rc\d+$', version) and repo_name in ["Batteries", "Mathlib"]:
+    if re.search(r'rc\d+$', version) and repo_name in ["batteries", "mathlib4"]:
         script_lines.extend([
             "echo 'This repo has nightly-testing infrastructure'",
             f"git merge origin/bump/{version.split('-rc')[0]}",
             "echo 'Please resolve any conflicts.'",
             ""
         ])
+    if re.search(r'rc\d+$', version) and repo_name in ["verso", "reference-manual"]:
+        script_lines.extend([
+            "echo 'This repo does development on nightly-testing: remember to rebase merge the PR.'",
+            f"git merge origin/nightly-testing",
+            "echo 'Please resolve any conflicts.'",
+            ""
+        ])
     if repo_name != "Mathlib":
         script_lines.extend([
             "lake build && if lake check-test; then lake test; fi",
@@ -104,7 +111,7 @@ def generate_script(repo, version, config):
 
     script_lines.extend([
         'gh pr create --title "chore: bump toolchain to ' + version + '" --body ""',
-        "echo 'Please review the PR and merge it.'",
+        "echo 'Please review the PR and merge or rebase it.'",
         ""
     ])
 

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 20)
+set(LEAN_VERSION_MINOR 21)
 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'")
@@ -191,10 +191,11 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
 # Initialize CXXFLAGS.
 set(CMAKE_CXX_FLAGS                "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
-set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG -DLEAN_TRACE")
+set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG")
 set(CMAKE_CXX_FLAGS_MINSIZEREL     "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELEASE        "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-DNDEBUG")
+set(CMAKE_CXX_FLAGS_RELWITHASSERT  "-DLEAN_DEBUG")
 
 # SPLIT_STACK
 if (SPLIT_STACK)
@@ -221,6 +222,7 @@ elseif (MSVC)
     set(CMAKE_CXX_FLAGS_DEBUG          "/Od /Zi ${CMAKE_CXX_FLAGS_DEBUG}")
     set(CMAKE_CXX_FLAGS_MINSIZEREL     "/Os /Zc:inline ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     set(CMAKE_CXX_FLAGS_RELEASE        "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELEASE}")
+    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/O2 /Oi /Zi ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
     set(LEAN_EXTRA_LINKER_FLAGS        "/LTCG:INCREMENTAL ${LEAN_EXTRA_LINKER_FLAGS}")
     set(CMAKE_STATIC_LINKER_FLAGS      "${CMAKE_STATIC_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
@@ -240,11 +242,13 @@ if (NOT MSVC)
       set(CMAKE_CXX_FLAGS_MINSIZEREL     "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     endif ()
     set(CMAKE_CXX_FLAGS_RELEASE        "-O3 ${CMAKE_CXX_FLAGS_RELEASE}")
+    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "-O3 ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 -fno-omit-frame-pointer ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 elseif (MULTI_THREAD)
     set(CMAKE_CXX_FLAGS_DEBUG          "/MTd ${CMAKE_CXX_FLAGS_DEBUG}")
     set(CMAKE_CXX_FLAGS_MINSIZEREL     "/MT ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     set(CMAKE_CXX_FLAGS_RELEASE        "/MT ${CMAKE_CXX_FLAGS_RELEASE}")
+    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "/MT ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/MT ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 endif ()
 
@@ -365,8 +369,8 @@ if(LLVM)
   execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY OUTPUT_VARIABLE LLVM_CONFIG_VERSION ECHO_OUTPUT_VARIABLE OUTPUT_STRIP_TRAILING_WHITESPACE)
   string(REGEX MATCH "^[0-9]*" LLVM_CONFIG_MAJOR_VERSION ${LLVM_CONFIG_VERSION})
   message(STATUS "Found 'llvm-config' at '${LLVM_CONFIG}' with version '${LLVM_CONFIG_VERSION}', major version '${LLVM_CONFIG_MAJOR_VERSION}'")
-  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "15")
-    message(FATAL_ERROR "Unable to find llvm-config version 15. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
+  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "19")
+    message(FATAL_ERROR "Unable to find llvm-config version 19. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
   endif()
   # -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM
   string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM")
@@ -507,7 +511,10 @@ 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")
 elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
-  string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup")
+  # 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
+  # before definition.
+  string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup -Wl,-no_fixup_chains")
 endif()
 # Linux ignores undefined symbols in shared libraries by default
 
@@ -780,12 +787,11 @@ add_custom_target(clean-olean
   DEPENDS clean-stdlib)
 
 install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
-  PATTERN temp
-  PATTERN "*.export"
-  PATTERN "*.hash"
-  PATTERN "*.trace"
-  PATTERN "*.rsp"
-  EXCLUDE)
+  PATTERN temp EXCLUDE
+  PATTERN "*.export" EXCLUDE
+  PATTERN "*.hash" EXCLUDE
+  PATTERN "*.trace" EXCLUDE
+  PATTERN "*.rsp" EXCLUDE)
 
 # symlink source into expected installation location for go-to-definition, if file system allows it
 file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
@@ -844,6 +850,4 @@ endif()
 
 if(USE_LAKE AND STAGE EQUAL 1)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
-  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../tests/lakefile.toml)
-  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../lakefile.toml)
 endif()

src/Init.lean

@@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Prelude
 import Init.Notation

src/Init/BinderNameHint.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner
 -/
 
+module
+
 prelude
 import Init.Prelude
 import Init.Tactics

src/Init/BinderPredicates.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
+module
+
 prelude
 import Init.NotationExtra
 

src/Init/ByCases.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
+module
+
 prelude
 import Init.Classical
 

src/Init/Classical.lean

@@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
+module
+
 prelude
 import Init.PropLemmas
 

src/Init/Coe.lean

@@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
+module
+
 prelude
 import Init.Prelude
 set_option linter.missingDocs true -- keep it documented
@@ -307,9 +309,6 @@ instance boolToSort : CoeSort Bool Prop where
 instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
   coe := decide p
 
-instance optionCoe {α : Type u} : Coe α (Option α) where
-  coe := some
-
 instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeOut (Subtype p) α where
   coe v := v.val
 

src/Init/Control.lean

@@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Control.Basic
 import Init.Control.State

src/Init/Control/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Sebastian Ullrich
 -/
+module
+
 prelude
 import Init.Core
 import Init.BinderNameHint

src/Init/Control/EState.lean

@@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Control.State
 import Init.Control.Except

src/Init/Control/Except.lean

@@ -5,6 +5,8 @@ Authors: Jared Roesch, Sebastian Ullrich
 
 The Except monad transformer.
 -/
+module
+
 prelude
 import Init.Control.Basic
 import Init.Control.Id

src/Init/Control/ExceptCps.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Control.Lawful.Basic
 

src/Init/Control/Id.lean

@@ -5,6 +5,8 @@ Authors: Sebastian Ullrich
 
 The identity Monad.
 -/
+module
+
 prelude
 import Init.Core
 

src/Init/Control/Lawful.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 -/
+module
+
 prelude
 import Init.Control.Lawful.Basic
 import Init.Control.Lawful.Instances

src/Init/Control/Lawful/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 -/
+module
+
 prelude
 import Init.SimpLemmas
 import Init.Meta
@@ -142,6 +144,7 @@ class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplica
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
 attribute [simp] pure_bind bind_assoc bind_pure_comp
+attribute [grind] pure_bind
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
   show x >>= (fun a => pure (id a)) = x

src/Init/Control/Lawful/Instances.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 -/
+module
+
 prelude
 import Init.Control.Lawful.Basic
 import Init.Control.Except

src/Init/Control/Lawful/Lemmas.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Control.Lawful.Basic
 import Init.RCases

src/Init/Control/Option.lean

@@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
+module
+
 prelude
 import Init.Data.Option.Basic
 import Init.Control.Basic
@@ -59,6 +61,9 @@ instance : Monad (OptionT m) where
   pure := OptionT.pure
   bind := OptionT.bind
 
+instance {m : Type u → Type v} [Pure m] : Inhabited (OptionT m α) where
+  default := pure (f:=m) default
+
 /--
 Recovers from failures. Typically used via the `<|>` operator.
 -/
@@ -95,7 +100,7 @@ Handles failures by treating them as exceptions of type `Unit`.
 -/
 @[always_inline, inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   let some a ← x | handle ()
-  pure a
+  pure <| some a
 
 instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail

src/Init/Control/Reader.lean

@@ -5,6 +5,8 @@ Authors: Sebastian Ullrich
 
 The Reader monad transformer for passing immutable State.
 -/
+module
+
 prelude
 import Init.Control.Basic
 import Init.Control.Id

src/Init/Control/State.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 
 The State monad transformer.
 -/
+module
+
 prelude
 import Init.Control.Basic
 import Init.Control.Id

src/Init/Control/StateCps.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Control.Lawful.Basic
 

src/Init/Control/StateRef.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 
 The State monad transformer using IO references.
 -/
+module
+
 prelude
 import Init.System.ST
 

src/Init/Conv.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 
 Notation for operators defined at Prelude.lean
 -/
+module
+
 prelude
 import Init.Tactics
 import Init.Meta
@@ -318,6 +320,25 @@ syntax "repeat " convSeq : conv
 macro_rules
   | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
+/--
+Extracts `let` and `let_fun` expressions from within the target expression.
+This is the conv mode version of the `extract_lets` tactic.
+
+- `extract_lets` extracts all the lets from the target.
+- `extract_lets x y z` extracts all the lets from the target and uses `x`, `y`, and `z` for the first names.
+  Using `_` for a name leaves it unnamed.
+
+Limitation: the extracted local declarations do not persist outside of the `conv` goal.
+See also `lift_lets`, which does not extract lets as local declarations.
+-/
+syntax (name := extractLets) "extract_lets " optConfig (ppSpace colGt (ident <|> hole))* : conv
+
+/--
+Lifts `let` and `let_fun` expressions within the target expression as far out as possible.
+This is the conv mode version of the `lift_lets` tactic.
+-/
+syntax (name := liftLets) "lift_lets " optConfig : conv
+
 /--
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,
 by focusing on particular subexpressions.

src/Init/Core.lean

@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 
 notation, basic datatypes and type classes
 -/
+module
+
 prelude
 import Init.Prelude
 import Init.SizeOf
@@ -21,6 +23,8 @@ which applies to all applications of the function).
 
 theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
+attribute [grind] id
+
 /--
 `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.
@@ -738,6 +742,20 @@ Unlike `x ≠ y` (which is notation for `Ne x y`), this is `Bool` valued instead
 
 recommended_spelling "bne" for "!=" in [bne, «term_!=_»]
 
+/-- `ReflBEq α` says that the `BEq` implementation is reflexive. -/
+class ReflBEq (α) [BEq α] : Prop where
+  /-- `==` is reflexive, that is, `(a == a) = true`. -/
+  protected rfl {a : α} : a == a
+
+@[simp] theorem BEq.rfl [BEq α] [ReflBEq α] {a : α} : a == a := ReflBEq.rfl
+theorem BEq.refl [BEq α] [ReflBEq α] (a : α) : a == a := BEq.rfl
+
+theorem beq_of_eq [BEq α] [ReflBEq α] {a b : α} : a = b → a == b
+  | rfl => BEq.rfl
+
+theorem not_eq_of_beq_eq_false [BEq α] [ReflBEq α] {a b : α} (h : (a == b) = false) : ¬a = b := by
+  intro h'; subst h'; have : true = false := BEq.rfl.symm.trans h; contradiction
+
 /--
 A Boolean equality test coincides with propositional equality.
 
@@ -745,11 +763,9 @@ In other words:
  * `a == b` implies `a = b`.
  * `a == a` is true.
 -/
-class LawfulBEq (α : Type u) [BEq α] : Prop where
+class LawfulBEq (α : Type u) [BEq α] : Prop extends ReflBEq α where
   /-- If `a == b` evaluates to `true`, then `a` and `b` are equal in the logic. -/
   eq_of_beq : {a b : α} → a == b → a = b
-  /-- `==` is reflexive, that is, `(a == a) = true`. -/
-  protected rfl : {a : α} → a == a
 
 export LawfulBEq (eq_of_beq)
 
@@ -761,6 +777,15 @@ instance [DecidableEq α] : LawfulBEq α where
   eq_of_beq := of_decide_eq_true
   rfl := of_decide_eq_self_eq_true _
 
+/--
+Non-instance for `DecidableEq` from `LawfulBEq`.
+To use this, add `attribute [local instance 5] instDecidableEqOfLawfulBEq` at the top of a file.
+-/
+def instDecidableEqOfLawfulBEq [BEq α] [LawfulBEq α] : DecidableEq α := fun x y =>
+  match h : x == y with
+  | false => .isFalse (not_eq_of_beq_eq_false h)
+  | true => .isTrue (eq_of_beq h)
+
 instance : LawfulBEq Char := inferInstance
 
 instance : LawfulBEq String := inferInstance
@@ -855,8 +880,8 @@ theorem Bool.of_not_eq_false : {b : Bool} → ¬ (b = false) → b = true
   | true,  _ => rfl
   | false, h => absurd rfl h
 
-theorem ne_of_beq_false [BEq α] [LawfulBEq α] {a b : α} (h : (a == b) = false) : a ≠ b := by
-  intro h'; subst h'; have : true = false := Eq.trans LawfulBEq.rfl.symm h; contradiction
+theorem ne_of_beq_false [BEq α] [ReflBEq α] {a b : α} (h : (a == b) = false) : a ≠ b :=
+  not_eq_of_beq_eq_false h
 
 theorem beq_false_of_ne [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a == b) = false :=
   have : ¬ (a == b) = true := by
@@ -915,6 +940,34 @@ term.
 theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → HEq (Eq.recOn (motive := fun x _ => φ x) h p) p
   | rfl, p => HEq.refl p
 
+/--
+Heterogenous equality with an `Eq.rec` application on the left is equivalent to a heterogenous
+equality on the original term.
+-/
+theorem eqRec_heq_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
+    {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h} :
+    HEq (@Eq.rec α a motive refl b h) c ↔ HEq refl c :=
+  h.rec (fun _ => ⟨id, id⟩) c
+
+/--
+Heterogenous equality with an `Eq.rec` application on the right is equivalent to a heterogenous
+equality on the original term.
+-/
+theorem heq_eqRec_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
+    {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h} :
+    HEq c (@Eq.rec α a motive refl b h) ↔ HEq c refl :=
+  h.rec (fun _ => ⟨id, id⟩) c
+
+/--
+Moves an cast using `Eq.rec` from the function to the argument.
+Note: because the motive isn't reliably detected by unification,
+it needs to be provided as an explicit parameter.
+-/
+theorem apply_eqRec {α : Sort u} {a : α} (motive : (b : α) → a = b → Sort v)
+    {b : α} {h : a = b} {c : motive a (Eq.refl a) → β} {d : motive b h} :
+    @Eq.rec α a (fun b h => motive b h → β) c b h d = c (h.symm ▸ d) := by
+  cases h; rfl
+
 /--
 If casting a term with `Eq.rec` to another type makes it equal to some other term, then the two
 terms are heterogeneously equal.
@@ -960,7 +1013,7 @@ theorem HEq.comm {a : α} {b : β} : HEq a b ↔ HEq b a := Iff.intro HEq.symm H
 theorem heq_comm {a : α} {b : β} : HEq a b ↔ HEq b a := HEq.comm
 
 @[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
-theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
+theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
 theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm
 
 @[symm] theorem And.symm : a ∧ b → b ∧ a := fun ⟨ha, hb⟩ => ⟨hb, ha⟩
@@ -1125,12 +1178,12 @@ theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) :
   | isTrue _    => rfl
   | isFalse _   => rfl
 
-instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e)  :=
+instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
   match dC with
   | isTrue _   => dT
   | isFalse _  => dE
 
-instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h)  :=
+instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
   match dC with
   | isTrue hc  => dT hc
   | isFalse hc => dE hc
@@ -1296,6 +1349,15 @@ theorem eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a := by
   cases a
   exact rfl
 
+instance {α : Type u} {p : α → Prop} [BEq α] : BEq {x : α // p x} :=
+  ⟨fun x y => x.1 == y.1⟩
+
+instance {α : Type u} {p : α → Prop} [BEq α] [ReflBEq α] : ReflBEq {x : α // p x} where
+  rfl {x} := BEq.refl x.1
+
+instance {α : Type u} {p : α → Prop} [BEq α] [LawfulBEq α] : LawfulBEq {x : α // p x} where
+  eq_of_beq h := Subtype.eq (eq_of_beq h)
+
 instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)
@@ -1564,7 +1626,7 @@ theorem Nat.succ.injEq (u v : Nat) : (u.succ = v.succ) = (u = v) :=
   Eq.propIntro Nat.succ.inj (congrArg Nat.succ)
 
 @[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] {a b : α} : a == b ↔ a = b :=
-  ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
+  ⟨eq_of_beq, beq_of_eq⟩
 
 /-! # Prop lemmas -/
 
@@ -1837,9 +1899,7 @@ protected abbrev hrecOn
     (f : (a : α) → motive (Quot.mk r a))
     (c : (a b : α) → (p : r a b) → HEq (f a) (f b))
     : motive q :=
-  Quot.recOn q f fun a b p => eq_of_heq <|
-    have p₁ : HEq (Eq.ndrec (f a) (sound p)) (f a) := eqRec_heq (sound p) (f a)
-    HEq.trans p₁ (c a b p)
+  Quot.recOn q f fun a b p => eq_of_heq (eqRec_heq_iff.mpr (c a b p))
 
 end
 end Quot
@@ -2202,6 +2262,27 @@ theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
   show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
   exact congrArg extfunApp (Quot.sound h)
 
+/--
+Like `Quot.liftOn q f h` but allows `f a` to "know" that `q = Quot.mk r a`.
+-/
+protected abbrev Quot.pliftOn {α : Sort u} {r : α → α → Prop}
+    (q : Quot r)
+    (f : (a : α) → q = Quot.mk r a → β)
+    (h : ∀ (a b : α) (h h'), r a b → f a h = f b h') : β :=
+  q.rec (motive := fun q' => q = q' → β) f
+    (fun a b p => funext fun h' =>
+      (apply_eqRec (motive := fun b _ => q = b)).trans
+        (@h a b (h'.trans (sound p).symm) h' p)) rfl
+
+/--
+Like `Quotient.liftOn q f h` but allows `f a` to "know" that `q = Quotient.mk s a`.
+-/
+protected abbrev Quotient.pliftOn {α : Sort u} {s : Setoid α}
+    (q : Quotient s)
+    (f : (a : α) → q = Quotient.mk s a → β)
+    (h : ∀ (a b : α) (h h'), a ≈ b → f a h = f b h') : β :=
+  Quot.pliftOn q f h
+
 instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] :
     Subsingleton (∀ a, β a) where
   allEq f g := funext fun a => Subsingleton.elim (f a) (g a)

src/Init/Data.lean

@@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Basic
 import Init.Data.Nat
@@ -34,7 +36,6 @@ import Init.Data.Stream
 import Init.Data.Prod
 import Init.Data.AC
 import Init.Data.Queue
-import Init.Data.Channel
 import Init.Data.Sum
 import Init.Data.BEq
 import Init.Data.Subtype

src/Init/Data/AC.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dany Fabian
 -/
 
+module
+
 prelude
 import Init.Classical
 import Init.ByCases

src/Init/Data/Array.lean

@@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.QSort

src/Init/Data/Array/Attach.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner, Mario Carneiro
 -/
+module
+
 prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
@@ -54,15 +56,15 @@ well-founded recursion mechanism to prove that the function terminates.
 -/
 @[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
 
-@[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
+@[simp, grind =] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
     l.toArray.attachWith P H = (l.attachWith P (by simpa using H)).toArray := by
   simp [attachWith]
 
-@[simp] theorem _root_.List.attach_toArray {l : List α} :
+@[simp, grind =] theorem _root_.List.attach_toArray {l : List α} :
     l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
   simp [attach]
 
-@[simp] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
+@[simp, grind =] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
     l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray := by
   simp [pmap]
 
@@ -525,7 +527,7 @@ theorem countP_attachWith {p : α → Prop} {q : α → Bool} {xs : Array α} {H
   simp
 
 @[simp]
-theorem count_attach [DecidableEq α] {xs : Array α} {a : {x // x ∈ xs}} :
+theorem count_attach [BEq α] {xs : Array α} {a : {x // x ∈ xs}} :
     xs.attach.count a = xs.count ↑a := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.count_toArray]
@@ -534,7 +536,7 @@ theorem count_attach [DecidableEq α] {xs : Array α} {a : {x // x ∈ xs}} :
   rw [List.countP_pmap, List.countP_attach (p := (fun x => x == a.1)), List.count]
 
 @[simp]
-theorem count_attachWith [DecidableEq α] {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) {a : {x // p x}} :
+theorem count_attachWith [BEq α] {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) {a : {x // p x}} :
     (xs.attachWith p H).count a = xs.count ↑a := by
   cases xs
   simp
@@ -588,7 +590,7 @@ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array
   unfold unattach
   simp
 
-@[simp] theorem _root_.List.unattach_toArray {p : α → Prop} {xs : List { x // p x }} :
+@[simp, grind =] theorem _root_.List.unattach_toArray {p : α → Prop} {xs : List { x // p x }} :
     xs.toArray.unattach = xs.unattach.toArray := by
   simp only [unattach, List.map_toArray, List.unattach]
 

src/Init/Data/Array/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.WFTactics
 import Init.Data.Nat.Basic
@@ -38,11 +40,11 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
+@[simp, grind] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
     (set xs i v h).size = xs.size :=
   List.length_set ..
 
-@[simp] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
+@[simp, grind] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
   List.length_concat ..
 
 theorem ext {xs ys : Array α}
@@ -86,11 +88,11 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 @[simp] theorem toArrayAux_eq {as : List α} {acc : Array α} : (as.toArrayAux acc).toList = acc.toList ++ as := by
   induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
 
-@[simp] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl
+@[simp, grind =] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl
 
-@[simp] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
+@[simp, grind =] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
 
-@[simp] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
+@[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
   simp [getElem?_def]
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
@@ -105,10 +107,10 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+@[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[simp] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
+@[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
 
@@ -125,18 +127,18 @@ theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl
 @[deprecated toList_toArray (since := "2025-02-17")]
 abbrev _root_.Array.toList_toArray := @List.toList_toArray
 
-@[simp] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
+@[simp, grind] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
 
 @[deprecated size_toArray (since := "2025-02-17")]
 abbrev _root_.Array.size_toArray := @List.size_toArray
 
-@[simp] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
+@[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := rfl
 
-@[simp] theorem getElem?_toArray {xs : List α} {i : Nat} : xs.toArray[i]? = xs[i]? := by
+@[simp, grind =] theorem getElem?_toArray {xs : List α} {i : Nat} : xs.toArray[i]? = xs[i]? := by
   simp [getElem?_def]
 
-@[simp] theorem getElem!_toArray [Inhabited α] {xs : List α} {i : Nat} :
+@[simp, grind =] theorem getElem!_toArray [Inhabited α] {xs : List α} {i : Nat} :
     xs.toArray[i]! = xs[i]! := by
   simp [getElem!_def]
 
@@ -192,7 +194,7 @@ Examples:
 def pop (xs : Array α) : Array α where
   toList := xs.toList.dropLast
 
-@[simp] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
+@[simp, grind] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
   match xs with
   | ⟨[]⟩ => rfl
   | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
@@ -834,7 +836,7 @@ some 10
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
   for a in as do
     match (← f a) with
-    | some b => return b
+    | some b => return some b
     | _      => pure ⟨⟩
   return none
 
@@ -865,7 +867,7 @@ some 1
 def findM? {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
   for a in as do
     if (← p a) then
-      return a
+      return some a
   return none
 
 /--
@@ -1173,7 +1175,7 @@ def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α :=
   Id.run do
     for a in as do
       if p a then
-        return a
+        return some a
     return none
 
 /--
@@ -2156,13 +2158,15 @@ Examples:
 
 /-! ### Repr and ToString -/
 
+protected def Array.repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
+  let _ : Std.ToFormat α := ⟨repr⟩
+  if xs.size == 0 then
+    "#[]"
+  else
+    Std.Format.bracketFill "#[" (Std.Format.joinSep (toList xs) ("," ++ Std.Format.line)) "]"
+
 instance {α : Type u} [Repr α] : Repr (Array α) where
-  reprPrec xs _ :=
-    let _ : Std.ToFormat α := ⟨repr⟩
-    if xs.size == 0 then
-      "#[]"
-    else
-      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList xs) ("," ++ Std.Format.line)) "]"
+  reprPrec xs _ := Array.repr xs
 
 instance [ToString α] : ToString (Array α) where
   toString xs := "#" ++ toString xs.toList

src/Init/Data/Array/BasicAux.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Nat.Linear

src/Init/Data/Array/BinSearch.lean

@@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Int.DivMod.Lemmas

src/Init/Data/Array/Bootstrap.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
+module
+
 prelude
 import Init.Data.List.TakeDrop
 
@@ -53,12 +55,12 @@ theorem foldlM_toList.aux [Monad m]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-@[simp] theorem foldlM_toList [Monad m]
+@[simp, grind =] theorem foldlM_toList [Monad m]
     {f : β → α → m β} {init : β} {xs : Array α} :
     xs.toList.foldlM f init = xs.foldlM f init := by
   simp [foldlM, foldlM_toList.aux]
 
-@[simp] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} :
+@[simp, grind =] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} :
     xs.toList.foldl f init = xs.foldl f init :=
   List.foldl_eq_foldlM .. ▸ foldlM_toList ..
 
@@ -77,32 +79,32 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init
   match xs, this with | _, .inl rfl => rfl | xs, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-@[simp] theorem foldrM_toList [Monad m]
+@[simp, grind =] theorem foldrM_toList [Monad m]
     {f : α → β → m β} {init : β} {xs : Array α} :
     xs.toList.foldrM f init = xs.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-@[simp] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} :
+@[simp, grind =] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} :
     xs.toList.foldr f init = xs.foldr f init :=
   List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
-@[simp] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
+@[simp, grind =] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
-@[simp] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
+@[simp, grind =] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
   simp [toListAppend, ← foldr_toList]
 
-@[simp] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by
+@[simp, grind =] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by
   simp [toListImpl, ← foldr_toList]
 
-@[simp] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
+@[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
 
 @[deprecated toList_pop (since := "2025-02-17")]
 abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl
 
-@[simp] theorem toList_append {xs ys : Array α} :
+@[simp, grind =] theorem toList_append {xs ys : Array α} :
     (xs ++ ys).toList = xs.toList ++ ys.toList := by
   rw [← append_eq_append]; unfold Array.append
   rw [← foldl_toList]
@@ -110,24 +112,24 @@ abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
-@[simp] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
+@[simp, grind =] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
   apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
 @[deprecated append_empty (since := "2025-01-13")]
 abbrev append_nil := @append_empty
 
-@[simp] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
+@[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
   apply ext'; simp only [toList_append, toList_empty, List.nil_append]
 
 @[deprecated empty_append (since := "2025-01-13")]
 abbrev nil_append := @empty_append
 
-@[simp] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
+@[simp, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
 @[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl
 
-@[simp] theorem toList_appendList {xs : Array α} {l : List α} :
+@[simp, grind =] theorem toList_appendList {xs : Array α} {l : List α} :
     (xs ++ l).toList = xs.toList ++ l := by
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing xs <;> simp [*]

src/Init/Data/Array/Count.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Count
@@ -23,7 +25,7 @@ section countP
 
 variable {p q : α → Bool}
 
-@[simp] theorem _root_.List.countP_toArray {l : List α} : countP p l.toArray = l.countP p := by
+@[simp, grind =] theorem _root_.List.countP_toArray {l : List α} : countP p l.toArray = l.countP p := by
   simp [countP]
   induction l with
   | nil => rfl
@@ -31,7 +33,7 @@ variable {p q : α → Bool}
     simp only [List.foldr_cons, ih, List.countP_cons]
     split <;> simp_all
 
-@[simp] theorem countP_toList {xs : Array α} : xs.toList.countP p = countP p xs := by
+@[simp, grind =] theorem countP_toList {xs : Array α} : xs.toList.countP p = countP p xs := by
   cases xs
   simp
 
@@ -162,10 +164,10 @@ section count
 
 variable [BEq α]
 
-@[simp] theorem _root_.List.count_toArray {l : List α} {a : α} : count a l.toArray = l.count a := by
+@[simp, grind =] theorem _root_.List.count_toArray {l : List α} {a : α} : count a l.toArray = l.count a := by
   simp [count, List.count_eq_countP]
 
-@[simp] theorem count_toList {xs : Array α} {a : α} : xs.toList.count a = xs.count a := by
+@[simp, grind =] theorem count_toList {xs : Array α} {a : α} : xs.toList.count a = xs.count a := by
   cases xs
   simp
 
@@ -257,8 +259,8 @@ theorem filter_beq {xs : Array α} (a : α) : xs.filter (· == a) = replicate (c
   rcases xs with ⟨xs⟩
   simp [List.filter_beq]
 
-theorem filter_eq {α} [DecidableEq α] {xs : Array α} (a : α) : xs.filter (· = a) = replicate (count a xs) a :=
-  filter_beq a
+theorem filter_eq {α} [BEq α] [LawfulBEq α] [DecidableEq α] {xs : Array α} (a : α) : xs.filter (· = a) = replicate (count a xs) a :=
+  funext (Bool.beq_eq_decide_eq · a) ▸ filter_beq a
 
 theorem replicate_count_eq_of_count_eq_size {xs : Array α} (h : count a xs = xs.size) :
     replicate (count a xs) a = xs := by
@@ -273,7 +275,7 @@ abbrev mkArray_count_eq_of_count_eq_size := @replicate_count_eq_of_count_eq_size
   rcases xs with ⟨xs⟩
   simp [List.count_filter, h]
 
-theorem count_le_count_map [DecidableEq β] {xs : Array α} {f : α → β} {x : α} :
+theorem count_le_count_map [BEq β] [LawfulBEq β] {xs : Array α} {f : α → β} {x : α} :
     count x xs ≤ count (f x) (map f xs) := by
   rcases xs with ⟨xs⟩
   simp [List.count_le_count_map, countP_map]
@@ -288,15 +290,25 @@ theorem count_flatMap {α} [BEq β] {xs : Array α} {f : α → Array β} {x :
   rcases xs with ⟨xs⟩
   simp [List.count_flatMap, countP_flatMap, Function.comp_def]
 
--- FIXME these theorems can be restored once `List.erase` and `Array.erase` have been related.
+theorem countP_replace {a b : α} {xs : Array α} {p : α → Bool} :
+    (xs.replace a b).countP p =
+      if xs.contains a then xs.countP p + (if p b then 1 else 0) - (if p a then 1 else 0) else xs.countP p := by
+  rcases xs with ⟨xs⟩
+  simp [List.countP_replace]
 
--- theorem count_erase (a b : α) (l : Array α) : count a (l.erase b) = count a l - if b == a then 1 else 0 := by
---   sorry
+theorem count_replace {a b c : α} {xs : Array α} :
+    (xs.replace a b).count c =
+      if xs.contains a then xs.count c + (if b == c then 1 else 0) - (if a == c then 1 else 0) else xs.count c := by
+  simp [count_eq_countP, countP_replace]
 
--- @[simp] theorem count_erase_self (a : α) (l : Array α) :
---     count a (l.erase a) = count a l - 1 := by rw [count_erase, if_pos (by simp)]
+theorem count_erase (a b : α) (xs : Array α) : count a (xs.erase b) = count a xs - if b == a then 1 else 0 := by
+  rcases xs with ⟨l⟩
+  simp [List.count_erase]
 
--- @[simp] theorem count_erase_of_ne (ab : a ≠ b) (l : Array α) : count a (l.erase b) = count a l := by
---   rw [count_erase, if_neg (by simpa using ab.symm), Nat.sub_zero]
+@[simp] theorem count_erase_self (a : α) (xs : Array α) :
+    count a (xs.erase a) = count a xs - 1 := by rw [count_erase, if_pos (by simp)]
+
+@[simp] theorem count_erase_of_ne (ab : a ≠ b) (xs : Array α) : count a (xs.erase b) = count a xs := by
+  rw [count_erase, if_neg (by simpa using ab.symm), Nat.sub_zero]
 
 end count

src/Init/Data/Array/DecidableEq.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.BEq
@@ -66,7 +68,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
       Bool.not_eq_true]
     simpa [isEqv_iff_rel] using h'
 
-@[simp] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
+@[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
   simp [isEqv_eq_decide, List.isEqv_eq_decide]
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
@@ -97,25 +99,27 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
       decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false := by
   simp [BEq.beq, isEqv_eq_decide]
 
-@[simp] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
+@[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
   simp [beq_eq_decide, List.beq_eq_decide]
 
 end Array
 
 namespace List
 
-@[simp] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by
+@[simp, grind =] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by
   simp [isEqv_eq_decide, Array.isEqv_eq_decide]
 
-@[simp] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by
+@[simp, grind =] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by
   simp [beq_eq_decide, Array.beq_eq_decide]
 
 end List
 
 namespace Array
 
-instance [BEq α] [LawfulBEq α] : LawfulBEq (Array α) where
+instance [BEq α] [ReflBEq α] : ReflBEq (Array α) where
   rfl := by simp [BEq.beq, isEqv_self_beq]
+
+instance [BEq α] [LawfulBEq α] : LawfulBEq (Array α) where
   eq_of_beq := by
     rintro ⟨_⟩ ⟨_⟩ h
     simpa using h

src/Init/Data/Array/Erase.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Erase
@@ -59,7 +61,7 @@ theorem exists_or_eq_self_of_eraseP (p) (xs : Array α) :
 @[simp] theorem size_eraseP_of_mem {xs : Array α} (al : a ∈ xs) (pa : p a) :
     (xs.eraseP p).size = xs.size - 1 := by
   let ⟨_, ys, zs, _, _, e₁, e₂⟩ := exists_of_eraseP al pa
-  rw [e₂]; simp [size_append, e₁]; omega
+  rw [e₂]; simp [size_append, e₁]
 
 theorem size_eraseP {xs : Array α} : (xs.eraseP p).size = if xs.any p then xs.size - 1 else xs.size := by
   split <;> rename_i h

src/Init/Data/Array/Extract.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.TakeDrop

src/Init/Data/Array/FinRange.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
+module
+
 prelude
 import Init.Data.List.FinRange
 import Init.Data.Array.OfFn

src/Init/Data/Array/Find.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.List.Nat.Find
 import Init.Data.Array.Lemmas
@@ -21,6 +23,14 @@ open Nat
 
 /-! ### findSome? -/
 
+@[simp, grind] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
+@[simp, grind] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+  cases xs; simp [List.findSome?_append]
+
+@[grind]
+theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f = f a := by
+  simp
+
 @[simp] theorem findSomeRev?_push_of_isSome {xs : Array α} (h : (f a).isSome) : (xs.push a).findSomeRev? f = f a := by
   cases xs; simp_all
 
@@ -28,7 +38,7 @@ open Nat
   cases xs; simp_all
 
 theorem exists_of_findSome?_eq_some {f : α → Option β} {xs : Array α} (w : xs.findSome? f = some b) :
-    ∃ a, a ∈ xs ∧ f a = b := by
+    ∃ a, a ∈ xs ∧ f a = some b := by
   cases xs; simp_all [List.exists_of_findSome?_eq_some]
 
 @[simp] theorem findSome?_eq_none_iff : findSome? p xs = none ↔ ∀ x ∈ xs, p x = none := by
@@ -129,6 +139,8 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
+@[simp] theorem find?_empty : find? p #[] = none := rfl
+
 @[simp] theorem find?_singleton {a : α} {p : α → Bool} :
     #[a].find? p = if p a then some a else none := by
   simp [singleton_eq_toArray_singleton]
@@ -157,6 +169,9 @@ theorem find?_eq_some_iff_append {xs : Array α} :
     exact ⟨as.toList, ⟨l, by simpa using congrArg Array.toList h'⟩,
       by simpa using h⟩
 
+theorem find?_push {xs : Array α} : (xs.push a).find? p = (xs.find? p).or (if p a then some a else none) := by
+  cases xs; simp
+
 @[simp]
 theorem find?_push_eq_some {xs : Array α} :
     (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
@@ -331,6 +346,11 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 
 /-! ### findIdx -/
 
+@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl
+theorem findIdx_singleton {a : α} {p : α → Bool} :
+    #[a].findIdx p = if p a then 0 else 1 := by
+  simp
+
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
   rcases xs with ⟨xs⟩
   exact List.findIdx_of_getElem?_eq_some (by simpa using w)
@@ -411,6 +431,13 @@ theorem findIdx_append {p : α → Bool} {xs ys : Array α} :
   rcases ys with ⟨ys⟩
   simp [List.findIdx_append]
 
+theorem findIdx_push {xs : Array α} {a : α} {p : α → Bool} :
+    (xs.push a).findIdx p = if xs.findIdx p < xs.size then xs.findIdx p else xs.size + if p a then 0 else 1 := by
+  simp only [push_eq_append, findIdx_append]
+  split <;> rename_i h
+  · rfl
+  · simp [findIdx_singleton, Nat.add_comm]
+
 theorem findIdx_le_findIdx {xs : Array α} {p q : α → Bool} (h : ∀ x ∈ xs, p x → q x) : xs.findIdx q ≤ xs.findIdx p := by
   rcases xs with ⟨xs⟩
   simp_all [List.findIdx_le_findIdx]
@@ -439,6 +466,9 @@ theorem false_of_mem_extract_findIdx {xs : Array α} {p : α → Bool} (h : x
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_empty : (#[] : Array α).findIdx? p = none := by simp
+theorem findIdx?_singleton {a : α} {p : α → Bool} :
+    #[a].findIdx? p = if p a then some 0 else none := by
+  simp
 
 @[simp]
 theorem findIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
@@ -446,11 +476,13 @@ theorem findIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
   rcases xs with ⟨xs⟩
   simp
 
+@[simp]
 theorem findIdx?_isSome {xs : Array α} {p : α → Bool} :
     (xs.findIdx? p).isSome = xs.any p := by
   rcases xs with ⟨xs⟩
   simp [List.findIdx?_isSome]
 
+@[simp]
 theorem findIdx?_isNone {xs : Array α} {p : α → Bool} :
     (xs.findIdx? p).isNone = xs.all (¬p ·) := by
   rcases xs with ⟨xs⟩
@@ -504,6 +536,13 @@ theorem of_findIdx?_eq_none {xs : Array α} {p : α → Bool} (w : xs.findIdx? p
   rcases ys with ⟨ys⟩
   simp [List.findIdx?_append]
 
+theorem findIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
+    (xs.push a).findIdx? p = (xs.findIdx? p).or (if p a then some xs.size else none) := by
+  simp only [push_eq_append, findIdx?_append]
+  split <;> rename_i h
+  · simp only [findIdx?_singleton, if_pos h, Option.map_some, Nat.zero_add]
+  · simp only [findIdx?_singleton, if_neg h, Option.map_none]
+
 theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.findIdx? p =
       (xss.findIdx? (·.any p)).map
@@ -561,6 +600,9 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
+theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
+    #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
+  simp
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -591,6 +633,33 @@ theorem findFinIdx?_eq_some_iff {xs : Array α} {p : α → Bool} {i : Fin xs.si
   · rintro ⟨h, w⟩
     exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
 
+theorem findFinIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
+    (xs.push a).findFinIdx? p =
+      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or (if p a then some ⟨xs.size, by simp⟩ else none) := by
+  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_push, Option.pmap_or]
+  split <;> rename_i h _ <;> split <;> simp [h]
+
+theorem findFinIdx?_append {xs ys : Array α} {p : α → Bool} :
+    (xs ++ ys).findFinIdx? p =
+      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
+        ((ys.findFinIdx? p).map (Fin.natAdd xs.size) |>.map (Fin.cast (by simp))) := by
+  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_append, Option.pmap_or]
+  split <;> rename_i h _
+  · simp [h, Option.pmap_map, Option.map_pmap, Nat.add_comm]
+  · simp [h]
+
+@[simp]
+theorem isSome_findFinIdx? {xs : Array α} {p : α → Bool} :
+    (xs.findFinIdx? p).isSome = xs.any p := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp]
+theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
+    (xs.findFinIdx? p).isNone = xs.all (fun x => ¬ p x) := by
+  rcases xs with ⟨xs⟩
+  simp
+
 @[simp] theorem findFinIdx?_subtype {p : α → Prop} {xs : Array { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     xs.findFinIdx? f = (xs.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
@@ -636,6 +705,20 @@ The lemmas below should be made consistent with those for `findIdx?` (and proved
   rcases xs with ⟨xs⟩
   simp [List.idxOf?_eq_none_iff]
 
+@[simp]
+theorem isSome_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+    (xs.idxOf? a).isSome ↔ a ∈ xs := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp]
+theorem isNone_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+    (xs.idxOf? a).isNone = ¬ a ∈ xs := by
+  rcases xs with ⟨xs⟩
+  simp
+
+
+
 /-! ### finIdxOf?
 
 The verification API for `finIdxOf?` is still incomplete.
@@ -658,4 +741,16 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
   rcases xs with ⟨xs⟩
   simp [List.finIdxOf?_eq_some_iff]
 
+@[simp]
+theorem isSome_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+    (xs.finIdxOf? a).isSome ↔ a ∈ xs := by
+  rcases xs with ⟨xs⟩
+  simp
+
+@[simp]
+theorem isNone_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+    (xs.finIdxOf? a).isNone = ¬ a ∈ xs := by
+  rcases xs with ⟨xs⟩
+  simp
+
 end Array

src/Init/Data/Array/GetLit.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 
+module
+
 prelude
 import Init.Data.Array.Basic
 

src/Init/Data/Array/InsertIdx.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.InsertIdx

src/Init/Data/Array/InsertionSort.lean

@@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 

src/Init/Data/Array/Lex.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lex.Basic
 import Init.Data.Array.Lex.Lemmas

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

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Nat.Lemmas

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

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Lex
@@ -14,11 +16,11 @@ namespace Array
 
 /-! ### Lexicographic ordering -/
 
-@[simp] theorem _root_.List.lt_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
-@[simp] theorem _root_.List.le_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
+@[simp, grind =] theorem _root_.List.lt_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
+@[simp, grind =] theorem _root_.List.le_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
 
-@[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
+@[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
+@[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
 protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
@@ -45,7 +47,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     cases a == b <;> simp
   · simp
 
-@[simp] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
+@[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
   | nil => cases l₂ <;> simp [lex, Id.run]
@@ -55,7 +57,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 
-@[simp] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
+@[simp, grind =] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
     xs.toList.lex ys.toList lt = xs.lex ys lt := by
   cases xs <;> cases ys <;> simp
 
@@ -150,13 +152,13 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
     Std.Total (· ≤ · : Array α → Array α → Prop) where
   total := Array.le_total
 
-@[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
+@[simp] theorem lex_eq_true_iff_lt [BEq α] [LawfulBEq α] [LT α] [DecidableLT α]
     {xs ys : Array α} : lex xs ys = true ↔ xs < ys := by
   cases xs
   cases ys
   simp
 
-@[simp] theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
+@[simp] theorem lex_eq_false_iff_ge [BEq α] [LawfulBEq α] [LT α] [DecidableLT α]
     {xs ys : Array α} : lex xs ys = false ↔ ys ≤ xs := by
   cases xs
   cases ys

src/Init/Data/Array/MapIdx.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
@@ -64,7 +66,7 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz
 
 @[simp] theorem getElem?_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} {i : Nat} :
     (xs.mapFinIdx f)[i]? =
-      xs[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
+      xs[i]?.pbind fun b h => some <| f i b (getElem?_eq_some_iff.1 h).1 := by
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
@@ -109,11 +111,11 @@ end Array
 
 namespace List
 
-@[simp] theorem mapFinIdx_toArray {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+@[simp, grind =] theorem mapFinIdx_toArray {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
   ext <;> simp
 
-@[simp] theorem mapIdx_toArray {f : Nat → α → β} {l : List α} :
+@[simp, grind =] theorem mapIdx_toArray {f : Nat → α → β} {l : List α} :
     l.toArray.mapIdx f = (l.mapIdx f).toArray := by
   ext <;> simp
 
@@ -130,7 +132,7 @@ namespace Array
 @[deprecated getElem_zipIdx (since := "2025-01-21")]
 abbrev getElem_zipWithIndex := @getElem_zipIdx
 
-@[simp] theorem zipIdx_toArray {l : List α} {k : Nat} :
+@[simp, grind =] theorem zipIdx_toArray {l : List α} {k : Nat} :
     l.toArray.zipIdx k = (l.zipIdx k).toArray := by
   ext i hi₁ hi₂ <;> simp [Nat.add_comm]
 
@@ -153,7 +155,7 @@ theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {xs : Array
 /-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
 to avoid the inequality and the subtraction. -/
 theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {xs : Array α} :
-    (x, i) ∈ xs.zipIdx ↔ xs[i]? = x := by
+    (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x := by
   rw [mk_mem_zipIdx_iff_le_and_getElem?_sub]
   simp
 
@@ -452,7 +454,7 @@ end Array
 
 namespace List
 
-theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
+@[grind] theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
     {f : (i : Nat) → α → (h : i < l.length) → m β} :
     l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f := by
   let rec go (i : Nat) (acc : Array β) (inv : i + acc.size = l.length) :
@@ -473,7 +475,7 @@ theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
   simp only [Array.mapFinIdxM, mapFinIdxM]
   exact go _ #[] _
 
-theorem mapIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
+@[grind] theorem mapIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
     {f : Nat → α → m β} :
     l.toArray.mapIdxM f = toArray <$> l.mapIdxM f := by
   let rec go (bs : List α) (acc : Array β) (inv : bs.length + acc.size = l.length) :

src/Init/Data/Array/Mem.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Joachim Breitner
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Nat.Linear

src/Init/Data/Array/Monadic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
@@ -262,7 +264,7 @@ end Array
 
 namespace List
 
-theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
+@[grind =] theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
     l.toArray.filterM p = toArray <$> l.filterM p := by
   simp only [Array.filterM, filterM, foldlM_toArray, bind_pure_comp, Functor.map_map]
   conv => lhs; rw [← reverse_nil]
@@ -282,7 +284,7 @@ theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bo
   subst w
   rw [filterM_toArray]
 
-theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
+@[grind =] theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
     l.toArray.filterRevM p = toArray <$> l.filterRevM p := by
   simp [Array.filterRevM, filterRevM]
   rw [← foldlM_reverse, ← foldlM_toArray, ← Array.filterM, filterM_toArray]
@@ -294,7 +296,7 @@ theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m
   subst w
   rw [filterRevM_toArray]
 
-theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} :
+@[grind =] theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} :
     l.toArray.filterMapM f = toArray <$> l.filterMapM f := by
   simp [Array.filterMapM, filterMapM]
   conv => lhs; rw [← reverse_nil]
@@ -312,7 +314,7 @@ theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m
   subst w
   rw [filterMapM_toArray]
 
-@[simp] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} :
+@[simp, grind =] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} :
     l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a) := by
   simp only [Array.flatMapM, bind_pure_comp, foldlM_toArray, flatMapM]
   conv => lhs; arg 2; change [].reverse.flatten.toArray

src/Init/Data/Array/OfFn.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.OfFn

src/Init/Data/Array/Perm.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.List.Nat.Perm
 import Init.Data.Array.Lemmas
@@ -20,49 +22,111 @@ open List
 This is a wrapper around `List.Perm`, and for now has much less API.
 For more complicated verification, use `perm_iff_toList_perm` and the `List` API.
 -/
-def Perm (as bs : Array α) : Prop :=
-  as.toList ~ bs.toList
+structure Perm (as bs : Array α) : Prop where
+  of_toList_perm ::
+  toList : as.toList ~ bs.toList
 
 @[inherit_doc] scoped infixl:50 " ~ " => Perm
 
-theorem perm_iff_toList_perm {as bs : Array α} : as ~ bs ↔ as.toList ~ bs.toList := Iff.rfl
+theorem perm_iff_toList_perm {as bs : Array α} : as ~ bs ↔ as.toList ~ bs.toList :=
+  ⟨Perm.toList, Perm.of_toList_perm⟩
 
-@[simp] theorem perm_toArray (as bs : List α) : as.toArray ~ bs.toArray ↔ as ~ bs := by
+end Array
+
+namespace List
+
+open Array
+
+theorem perm_iff_toArray_perm {as bs : List α} : as ~ bs ↔ as.toArray ~ bs.toArray := by
   simp [perm_iff_toList_perm]
 
+theorem Perm.of_toArray_perm {as bs : List α} : as.toArray ~ bs.toArray → as ~ bs :=
+  perm_iff_toArray_perm.mpr
+
+theorem Perm.toArray {as bs : List α} : as ~ bs → as.toArray ~ bs.toArray :=
+  perm_iff_toArray_perm.mp
+
+end List
+
+namespace Array
+
+open List
+
 @[simp, refl] protected theorem Perm.refl (xs : Array α) : xs ~ xs := by
   cases xs
-  simp
+  simp [perm_iff_toList_perm]
 
-protected theorem Perm.rfl {xs : List α} : xs ~ xs := .refl _
+protected theorem Perm.rfl {xs : Array α} : xs ~ xs := .refl _
 
 theorem Perm.of_eq {xs ys : Array α} (h : xs = ys) : xs ~ ys := h ▸ .rfl
 
+@[symm]
 protected theorem Perm.symm {xs ys : Array α} (h : xs ~ ys) : ys ~ xs := by
   cases xs; cases ys
-  simp only [perm_toArray] at h
-  simpa using h.symm
+  simp only [perm_iff_toList_perm] at h
+  simpa [perm_iff_toList_perm] using h.symm
 
 protected theorem Perm.trans {xs ys zs : Array α} (h₁ : xs ~ ys) (h₂ : ys ~ zs) : xs ~ zs := by
   cases xs; cases ys; cases zs
-  simp only [perm_toArray] at h₁ h₂
-  simpa using h₁.trans h₂
+  simp only [perm_iff_toList_perm] at h₁ h₂
+  simpa [perm_iff_toList_perm] using h₁.trans h₂
 
 instance : Trans (Perm (α := α)) (Perm (α := α)) (Perm (α := α)) where
   trans h₁ h₂ := Perm.trans h₁ h₂
 
 theorem perm_comm {xs ys : Array α} : xs ~ ys ↔ ys ~ xs := ⟨Perm.symm, Perm.symm⟩
 
-theorem Perm.push (x y : α) {xs ys : Array α} (p : xs ~ ys) :
+theorem Perm.size_eq {xs ys : Array α} (p : xs ~ ys) : xs.size = ys.size := by
+  cases xs; cases ys
+  simp only [perm_iff_toList_perm] at p
+  simpa using p.length_eq
+
+@[deprecated Perm.size_eq (since := "2025-04-17")]
+abbrev Perm.length_eq := @Perm.size_eq
+
+theorem Perm.mem_iff {a : α} {xs ys : Array α} (p : xs ~ ys) : a ∈ xs ↔ a ∈ ys := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp only [perm_iff_toList_perm] at p
+  simpa using p.mem_iff
+
+theorem Perm.append {xs ys as bs : Array α} (p₁ : xs ~ ys) (p₂ : as ~ bs) :
+    xs ++ as ~ ys ++ bs := by
+  cases xs; cases ys; cases as; cases bs
+  simp only [append_toArray, perm_iff_toList_perm] at p₁ p₂ ⊢
+  exact p₁.append p₂
+
+theorem Perm.push (x : α) {xs ys : Array α} (p : xs ~ ys) :
+    xs.push x ~ ys.push x := by
+  rw [push_eq_append_singleton]
+  exact p.append .rfl
+
+theorem Perm.push_comm (x y : α) {xs ys : Array α} (p : xs ~ ys) :
     (xs.push x).push y ~ (ys.push y).push x := by
   cases xs; cases ys
-  simp only [perm_toArray] at p
-  simp only [push_toArray, List.append_assoc, singleton_append, perm_toArray]
-  exact p.append (Perm.swap' _ _ Perm.nil)
+  simp only [perm_iff_toList_perm] at p
+  simp only [push_toArray, List.append_assoc, singleton_append, perm_iff_toList_perm]
+  exact p.append (Perm.swap ..)
 
 theorem swap_perm {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < xs.size) :
     xs.swap i j ~ xs := by
   simp only [swap, perm_iff_toList_perm, toList_set]
   apply set_set_perm
 
+namespace Perm
+
+set_option linter.indexVariables false in
+theorem extract {xs ys : Array α} (h : xs ~ ys) {lo hi : Nat}
+    (wlo : ∀ i, i < lo → xs[i]? = ys[i]?) (whi : ∀ i, hi ≤ i → xs[i]? = ys[i]?) :
+    xs.extract lo hi ~ ys.extract lo hi := by
+  rcases xs with ⟨xs⟩
+  rcases ys with ⟨ys⟩
+  simp_all only [perm_iff_toList_perm, List.getElem?_toArray, List.extract_toArray,
+    List.extract_eq_drop_take]
+  apply List.Perm.take_of_getElem? (w := fun i h => by simpa using whi (lo + i) (by omega))
+  apply List.Perm.drop_of_getElem? (w := wlo)
+  exact h
+
+end Perm
+
 end Array

src/Init/Data/Array/QSort.lean

@@ -1,68 +1,9 @@
 /-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Kim Morrison
 -/
+module
+
 prelude
-import Init.Data.Vector.Basic
-import Init.Data.Ord
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
--- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
-
-namespace Array
-
-private def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
-    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {n : Nat // lo ≤ n} × Vector α n :=
-  let mid := (lo + hi) / 2
-  let as  := if lt as[mid] as[lo] then as.swap lo mid else as
-  let as  := if lt as[hi]  as[lo] then as.swap lo hi  else as
-  let as  := if lt as[mid] as[hi] then as.swap mid hi else as
-  let pivot := as[hi]
-  let rec loop (as : Vector α n) (i j : Nat)
-      (ilo : lo ≤ i := by omega) (jh : j < n := by omega) (w : i ≤ j := by omega) :=
-    if h : j < hi then
-      if lt as[j] pivot then
-        loop (as.swap i j) (i+1) (j+1)
-      else
-        loop as i (j+1)
-    else
-      (⟨i, ilo⟩, as.swap i hi)
-  loop as lo lo
-
-/--
-Sorts an array using the Quicksort algorithm.
-
-The optional parameter `lt` specifies an ordering predicate. It defaults to `LT.lt`, which must be
-decidable to be used for sorting. Use `Array.qsortOrd` to sort the array according to the `Ord α`
-instance.
-
-The optional parameters `low` and `high` delimit the region of the array that is sorted. Both are
-inclusive, and default to sorting the entire array.
--/
-@[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
-    (low := 0) (high := as.size - 1) : Array α :=
-  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
-      (hlo : lo < n := by omega) (hhi : hi < n := by omega) :=
-    if h₁ : lo < hi then
-      let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
-      if h₂ : mid ≥ hi then
-        as
-      else
-        sort (sort as lo mid) (mid+1) hi
-    else as
-  if h : as.size = 0 then
-    as
-  else
-    let low := min low (as.size - 1)
-    let high := min high (as.size - 1)
-    sort ⟨as, rfl⟩ low high |>.toArray
-
-set_option linter.unusedVariables.funArgs false in
-/--
-Sorts an array using the Quicksort algorithm, using `Ord.compare` to compare elements.
--/
-def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
-  xs.qsort fun x y => compare x y |>.isLT
-
-end Array
+import Init.Data.Array.QSort.Basic

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

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+import Init.Data.Vector.Basic
+import Init.Data.Ord
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+-- We do not enable `linter.indexVariables` because it is helpful to name index variables `lo`, `mid`, `hi`, etc.
+
+
+namespace Array
+
+/--
+Internal implementation of `Array.qsort`.
+
+`qpartition as lt lo hi hlo hhi` returns a pair `(⟨m, h₁, h₂⟩, as')` where
+`as'` is a permutation of `as` and `m` is a number such that:
+- `lo ≤ m`
+- `m < n`
+- `∀ i, lo ≤ i → i < m → lt as[i] as[m]`
+- `∀ j, m < j → j < hi → !lt as[j] as[m]`
+
+It does so by first swapping the elements at indices `lo`, `mid := (lo + hi) / 2`, and `hi`
+if necessary so that the middle (pivot) element is at index `hi`.
+We then iterate from `j = lo` to `j = hi`, with a pointer `i` starting at `lo`, and
+swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
+-/
+def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat)
+    (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m < n} × Vector α n :=
+  let mid := (lo + hi) / 2
+  let as  := if lt as[mid] as[lo] then as.swap lo mid else as
+  let as  := if lt as[hi]  as[lo] then as.swap lo hi  else as
+  let as  := if lt as[mid] as[hi] then as.swap mid hi else as
+  let pivot := as[hi]
+  let rec loop (as : Vector α n) (i j : Nat)
+      (ilo : lo ≤ i := by omega) (jh : j < n := by omega) (w : i ≤ j := by omega) :=
+    if h : j < hi then
+      if lt as[j] pivot then
+        loop (as.swap i j) (i+1) (j+1)
+      else
+        loop as i (j+1)
+    else
+      (⟨i, ilo, by omega⟩, as.swap i hi)
+  loop as lo lo
+
+/--
+In-place quicksort.
+
+`qsort as lt low high` sorts the subarray `as[low:high+1]` in-place using `lt` to compare elements.
+-/
+@[inline] def qsort (as : Array α) (lt : α → α → Bool := by exact (· < ·))
+    (low := 0) (high := as.size - 1) : Array α :=
+  let rec @[specialize] sort {n} (as : Vector α n) (lo hi : Nat)
+      (hlo : lo < n := by omega) (hhi : hi < n := by omega) :=
+    if h₁ : lo < hi then
+      let ⟨⟨mid, hmid⟩, as⟩ := qpartition as lt lo hi
+      if h₂ : mid ≥ hi then
+        as
+      else
+        sort (sort as lo mid) (mid+1) hi
+    else as
+  if h : as.size = 0 then
+    as
+  else
+    let low := min low (as.size - 1)
+    let high := min high (as.size - 1)
+    sort as.toVector low high |>.toArray
+
+set_option linter.unusedVariables.funArgs false in
+/--
+Sort an array using `compare` to compare elements.
+-/
+def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
+  xs.qsort fun x y => compare x y |>.isLT
+
+end Array

src/Init/Data/Array/Range.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.OfFn

src/Init/Data/Array/Set.lean

@@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
+module
+
 prelude
 import Init.Tactics
 

src/Init/Data/Array/Subarray.lean

@@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 
@@ -462,8 +464,12 @@ instance : Append (Subarray α) where
    let a := x.toArray ++ y.toArray
    a.toSubarray 0 a.size
 
+/-- `Subarray` representation. -/
+protected def Subarray.repr [Repr α] (s : Subarray α) : Std.Format :=
+  repr s.toArray ++ ".toSubarray"
+
 instance [Repr α] : Repr (Subarray α) where
-  reprPrec s  _ := repr s.toArray ++ ".toSubarray"
+  reprPrec s  _ := Subarray.repr s
 
 instance [ToString α] : ToString (Subarray α) where
   toString s := toString s.toArray

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

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Thrane Christiansen
 -/
 
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.Subarray

src/Init/Data/Array/TakeDrop.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.TakeDrop

src/Init/Data/Array/Zip.lean

@@ -3,6 +3,8 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.TakeDrop
 import Init.Data.List.Zip
@@ -323,7 +325,7 @@ theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option
   simp [List.map_zipWithAll]
 
 @[simp] theorem zipWithAll_replicate {a : α} {b : β} {n : Nat} :
-    zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b) := by
+    zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b)) := by
   simp [← List.toArray_replicate]
 
 @[deprecated zipWithAll_replicate (since := "2025-03-18")]

src/Init/Data/BEq.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Markus Himmel
 -/
+module
+
 prelude
 import Init.Data.Bool
 
@@ -19,21 +21,9 @@ class PartialEquivBEq (α) [BEq α] : Prop where
   /-- Transitivity for `BEq`. If `a == b` and `b == c` then `a == c`. -/
   trans : (a : α) == b → b == c → a == c
 
-/-- `ReflBEq α` says that the `BEq` implementation is reflexive. -/
-class ReflBEq (α) [BEq α] : Prop where
-  /-- Reflexivity for `BEq`. -/
-  refl : (a : α) == a
-
 /-- `EquivBEq` says that the `BEq` implementation is an equivalence relation. -/
 class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 
-@[simp]
-theorem BEq.refl [BEq α] [ReflBEq α] {a : α} : a == a :=
-  ReflBEq.refl
-
-theorem beq_of_eq [BEq α] [ReflBEq α] {a b : α} : a = b → a == b
-  | rfl => BEq.refl
-
 theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
   PartialEquivBEq.symm
 
@@ -66,6 +56,5 @@ theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
   fun h₁ h₂ => Bool.eq_false_iff.2 fun h₃ => Bool.eq_false_iff.1 h₂ (BEq.trans (BEq.symm h₁) h₃)
 
 instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
-  refl := LawfulBEq.rfl
   symm h := beq_iff_eq.2 <| Eq.symm <| beq_iff_eq.1 h
   trans hab hbc := beq_iff_eq.2 <| (beq_iff_eq.1 hab).trans <| beq_iff_eq.1 hbc

src/Init/Data/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Nat.Basic
 import Init.Data.Fin.Basic

src/Init/Data/BitVec.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.BitVec.Basic
 import Init.Data.BitVec.Bitblast

src/Init/Data/BitVec/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed, Siddharth Bhat
 -/
+module
+
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
@@ -197,7 +199,13 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
   t ++ s
 
-instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
+/-- `BitVec` representation. -/
+protected def BitVec.repr (a : BitVec n) : Std.Format :=
+  "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
+
+instance : Repr (BitVec n) where
+  reprPrec a _ := BitVec.repr a
+
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
 end repr_toString
@@ -227,6 +235,20 @@ SMT-LIB name: `bvmul`.
 protected def mul (x y : BitVec n) : BitVec n := BitVec.ofNat n (x.toNat * y.toNat)
 instance : Mul (BitVec n) := ⟨.mul⟩
 
+/--
+Raises a bitvector to a natural number power. Usually accessed via the `^` operator.
+
+Note that this is currently an inefficient implementation,
+and should be replaced via an `@[extern]` with a native implementation.
+See https://github.com/leanprover/lean4/issues/7887.
+-/
+protected def pow (x : BitVec n) (y : Nat) : BitVec n :=
+  match y with
+  | 0 => 1
+  | y + 1 => x.pow y * x
+instance : Pow (BitVec n) Nat where
+  pow x y := x.pow y
+
 /--
 Unsigned division of bitvectors using the Lean convention where division by zero returns zero.
 Usually accessed via the `/` operator.
@@ -753,6 +775,15 @@ SMT-Lib name: `bvnego`.
 def negOverflow {w : Nat} (x : BitVec w) : Bool :=
   x.toInt == - 2 ^ (w - 1)
 
+/--
+Checks whether the signed division of `x` by `y` results in overflow.
+For BitVecs `x` and `y` with nonzero width, this only happens if `x = intMin` and `y = allOnes w`.
+
+SMT-LIB name: `bvsdivo`.
+-/
+def sdivOverflow {w : Nat} (x y : BitVec w) : Bool :=
+  (2 ^ (w - 1) ≤ x.toInt / y.toInt) || (x.toInt / y.toInt <  - 2 ^ (w - 1))
+
 /- ### reverse -/
 
 /-- Reverses the bits in a bitvector. -/

src/Init/Data/BitVec/BasicAux.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed
 -/
+module
+
 prelude
 import Init.Data.Fin.Basic
 

src/Init/Data/BitVec/Bitblast.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 -/
+module
+
 prelude
 import Init.Data.BitVec.Folds
 import Init.Data.Nat.Mod
@@ -566,7 +568,7 @@ theorem ult_eq_msb_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
 theorem slt_eq_not_ult_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
     x.slt y = !x.ult y := by
   simp only [BitVec.slt, toInt_eq_msb_cond, Bool.eq_not_of_ne h, ult_eq_msb_of_msb_neq h]
-  cases y.msb <;> (simp; omega)
+  cases y.msb <;> (simp [-Int.natCast_pow]; omega)
 
 theorem slt_eq_ult {x y : BitVec w} :
     x.slt y = (x.msb != y.msb).xor (x.ult y) := by
@@ -1332,7 +1334,7 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) :
     simp only [← decide_or, msb_eq_toInt, decide_beq_decide, toInt_add, ← decide_not, ← decide_and,
       decide_eq_decide]
     rw_mod_cast [Int.bmod_neg_iff (by omega) (by omega)]
-    simp
+    simp only [Nat.add_one_sub_one, ge_iff_le]
     omega
 
 theorem usubOverflow_eq {w : Nat} (x y : BitVec w) :
@@ -1356,9 +1358,41 @@ theorem negOverflow_eq {w : Nat} (x : BitVec w) :
   rcases w with _|w
   · simp [toInt_of_zero_length, Int.min_eq_right]
   · suffices - 2 ^ w = (intMin (w + 1)).toInt by simp [beq_eq_decide_eq, ← toInt_inj, this]
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod, Int.neg_inj]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod, Int.neg_inj]
     rw_mod_cast [Nat.mod_eq_of_lt (by simp [Nat.pow_lt_pow_succ])]
 
+/--
+  Prove that signed division `x.toInt / y.toInt` only overflows when `x = intMin w` and `y = allOnes w` (for `0 < w`).
+-/
+theorem sdivOverflow_eq {w : Nat} (x y : BitVec w) :
+    (sdivOverflow x y) = (decide (0 < w) && (x = intMin w) && (y = allOnes w)) := by
+  rcases w with _|w
+  · simp [sdivOverflow, of_length_zero]
+  · have yle := le_two_mul_toInt (x := y)
+    have ylt := two_mul_toInt_lt (x := y)
+    -- if y = allOnes (w + 1), thus y.toInt = -1,
+    -- the division overflows iff x = intMin (w + 1), as for negation
+    by_cases hy : y = allOnes (w + 1)
+    · simp [sdivOverflow_eq_negOverflow_of_eq_allOnes, negOverflow_eq, ← hy, beq_eq_decide_eq]
+    · simp only [sdivOverflow, hy, bool_to_prop]
+      have := BitVec.neg_two_pow_le_toInt_ediv (x := x) (y := y)
+      simp only [Nat.add_one_sub_one] at this
+      by_cases hx : 0 ≤ x.toInt
+      · by_cases hy' : 0 ≤ y.toInt
+        · have := BitVec.toInt_ediv_toInt_lt_of_nonneg_of_nonneg
+                (x := x) (y := y) (by omega) (by omega)
+          simp only [Nat.add_one_sub_one] at this; simp; omega
+        · have := BitVec.toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos
+                (x := x) (y := y) (by omega) (by omega)
+          simp; omega
+      · by_cases hy' : 0 ≤ y.toInt
+        · have :=  BitVec.toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg
+                (x := x) (y := y) (by omega) (by omega)
+          simp; omega
+        · have := BitVec.toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one
+                (x := x) (y := y) (by omega) (by rw [← toInt_inj, toInt_allOnes] at hy; omega)
+          simp only [Nat.add_one_sub_one] at this; simp; omega
+
 theorem umulOverflow_eq {w : Nat} (x y : BitVec w) :
     umulOverflow x y =
       (0 < w && BitVec.twoPow (w * 2) w ≤ x.zeroExtend (w * 2) * y.zeroExtend (w * 2)) := by
@@ -1456,7 +1490,6 @@ theorem udiv_intMin_of_msb_false {x : BitVec w} (h : x.msb = false) :
   have wpos : 0 < w := by omega
   have := Nat.two_pow_pos (w-1)
   simp [toNat_eq, wpos]
-  rw [Nat.div_eq_zero_iff_lt (by omega)]
   exact toNat_lt_of_msb_false h
 
 theorem sdiv_intMin {x : BitVec w} :
@@ -1468,7 +1501,6 @@ theorem sdiv_intMin {x : BitVec w} :
   by_cases h : x = intMin w
   · subst h
     simp
-    omega
   · simp only [sdiv_eq, msb_intMin, show 0 < w by omega, h]
     have := Nat.two_pow_pos (w-1)
     by_cases hx : x.msb
@@ -1541,7 +1573,7 @@ theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
 
 theorem toInt_eq_neg_toNat_neg_of_msb_true {x : BitVec w} (h : x.msb = true) :
     x.toInt = -((-x).toNat) := by
-  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.ofNat_emod]
+  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.natCast_emod]
   norm_cast
   rw [Nat.mod_eq_of_lt]
   · omega
@@ -1571,7 +1603,8 @@ theorem intMin_udiv_eq_intMin_iff (x : BitVec w) :
   · intro h
     rw [← toInt_inj, toInt_eq_msb_cond] at h
     have : (intMin w / x).msb = false := by simp [msb_udiv, msb_intMin,  wpos, hx]
-    simp [this, wpos, toInt_intMin] at h
+    simp only [this, false_eq_true, ↓reduceIte, toNat_udiv, toNat_intMin, wpos,
+      Nat.two_pow_pred_mod_two_pow, Int.natCast_ediv, toInt_intMin] at h
     omega
   · intro h
     subst h
@@ -1612,11 +1645,11 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
           Nat.two_pow_pred_mod_two_pow, Int.neg_tdiv, Int.neg_neg]
         rw [Int.tdiv_self (by omega)]
       · by_cases ha_nonneg : 0 ≤ a.toInt
-        · simp [Int.tdiv_eq_zero_of_lt ha_nonneg (by norm_cast at *), ha_intMin]
+        · simp [Int.tdiv_eq_zero_of_lt ha_nonneg (by norm_cast at *), ha_intMin, -Int.natCast_pow]
         · simp only [ne_eq, ← toInt_inj, toInt_intMin, wpos, Nat.two_pow_pred_mod_two_pow] at h
           rw [← Int.neg_tdiv, Int.tdiv_eq_zero_of_lt (by omega)]
           · simp [ha_intMin]
-          · simp [wpos, ← toInt_ne, toInt_intMin] at ha_intMin
+          · simp [wpos, ← toInt_ne, toInt_intMin, -Int.natCast_pow] at ha_intMin
             omega
 
   · by_cases ha : a.msb <;> by_cases hb : b.msb
@@ -1635,7 +1668,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
           (a.sdiv b).toInt = -((-a).toNat / b.toNat) := by
         simp only [sdiv_eq, ha, hb, udiv_eq]
         rw [toInt_eq_neg_toNat_neg_of_nonpos]
-        · rw [neg_neg, toNat_udiv, toNat_neg, Int.ofNat_emod, Int.neg_inj]
+        · rw [neg_neg, toNat_udiv, toNat_neg, Int.natCast_emod, Int.neg_inj]
           norm_cast
         · rw [neg_eq_zero_iff]
           by_cases h' : -a / b = 0#w
@@ -1778,9 +1811,23 @@ theorem extractLsb'_mul {w len} {x y : BitVec w} (hlen : len ≤ w) :
     (x * y).extractLsb' 0 len = (x.extractLsb' 0 len) * (y.extractLsb' 0 len) := by
   simp [← setWidth_eq_extractLsb' hlen, setWidth_mul _ _ hlen]
 
+/-- Adding bitvectors that are zero in complementary positions equals concatenation.
+We add a `no_index` annotation to `HAppend.hAppend` such that the width `v + w`
+does not act as a key in the discrimination tree.
+This is important to allow matching, when the type of the result of append
+`x : BitVec 3` and `y : BitVec 4` has been reduced to `x ++ y : BitVec 7`.
+-/
+theorem append_zero_add_zero_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
+    (HAppend.hAppend (γ := BitVec (no_index _)) x 0#w) +
+    (HAppend.hAppend (γ := BitVec (no_index _)) 0#v y)
+    = x ++ y := by
+  rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
+
 /-- Adding bitvectors that are zero in complementary positions equals concatenation. -/
-theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
-    (x ++ 0#w) + (0#v ++ y) = x ++ y := by
+theorem zero_append_add_append_zero {v w : Nat} {x : BitVec v} {y : BitVec w} :
+  (HAppend.hAppend (γ := BitVec (no_index _)) 0#v y) +
+  (HAppend.hAppend (γ := BitVec (no_index _)) x 0#w)
+  = x ++ y := by
   rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
 
 /-- Heuristically, `y <<< x` is much larger than `x`,
@@ -1796,4 +1843,10 @@ theorem add_shiftLeft_eq_or_shiftLeft {x y : BitVec w} :
   have : i < 2^i := by exact Nat.lt_two_pow_self
   omega
 
+/-- Heuristically, `y <<< x` is much larger than `x`,
+and hence low bits of `y <<< x`. Thus, `(y <<< x) + x = (y <<< x) ||| x.` -/
+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]
+
 end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Harun Khan
 -/
+module
+
 prelude
 import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas

src/Init/Data/BitVec/Lemmas.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth Bhat
 
 -/
+module
+
 prelude
 import Init.Data.Bool
 import Init.Data.BitVec.Basic
@@ -21,6 +23,9 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
+@[simp] theorem mk_zero : BitVec.ofFin (w := w) ⟨0, h⟩ = 0#w := rfl
+@[simp] theorem ofNatLT_zero : BitVec.ofNatLT (w := w) 0 h = 0#w := rfl
+
 @[simp] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
     getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
 
@@ -68,6 +73,9 @@ theorem getElem?_eq_some_iff {l : BitVec w} : l[n]? = some a ↔ ∃ h : n < w,
   · simp_all
   · simp; omega
 
+theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a :=
+  getElem?_eq_some_iff.mp
+
 set_option linter.missingDocs false in
 @[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
 abbrev getElem?_eq_some := @getElem?_eq_some_iff
@@ -133,6 +141,8 @@ theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y :
 @[bitvec_to_nat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat :=
   Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
 
+theorem toNat_inj {x y : BitVec n} : x.toNat = y.toNat ↔ x = y := toNat_eq.symm
+
 @[bitvec_to_nat] theorem toNat_ne {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat := by
   rw [Ne, toNat_eq]
 
@@ -449,7 +459,7 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
 @[simp] theorem sub_add_bmod_cancel {x y : BitVec w} :
     ((((2 ^ w : Nat) - y.toNat) : Int) + x.toNat).bmod (2 ^ w) =
       ((x.toNat : Int) - y.toNat).bmod (2 ^ w) := by
-  rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm, Int.bmod_add_cancel, Int.add_comm,
+  rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm, Int.add_bmod_right, Int.add_comm,
     Int.sub_eq_add_neg]
 
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
@@ -508,6 +518,10 @@ theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
   · rintro rfl
     simp
 
+/-- `0#w = 1#w` iff the width is zero. -/
+@[simp] theorem zero_eq_one_iff (w : Nat) : (0#w = 1#w) ↔ (w = 0) := by
+  rw [← one_eq_zero_iff, eq_comm]
+
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@@ -610,10 +624,10 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
   simp only [toInt_eq_toNat_cond]
   split
   next g =>
-    rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
+    rw [Int.bmod_pos] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
     omega
   next g =>
-    rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
+    rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
     omega
 
 theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by
@@ -629,12 +643,12 @@ theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.t
 @[simp] theorem toInt_one_of_lt {w : Nat} (h : 1 < w) : (1#w).toInt = 1 := by
   rw [toInt_eq_msb_cond]
   simp only [msb_one, show w ≠ 1 by omega, decide_false, Bool.false_eq_true, ↓reduceIte,
-    toNat_ofNat, Int.ofNat_emod]
+    toNat_ofNat, Int.natCast_emod]
   norm_cast
   apply Nat.mod_eq_of_lt
   apply Nat.one_lt_two_pow (by omega)
 
-/-- Prove equality of bitvectors in terms of nat operations. -/
+/-- Prove equality of bitvectors in terms of integer operations. -/
 theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by
   intro eq
   simp only [toInt_eq_toNat_cond] at eq
@@ -655,20 +669,19 @@ theorem toInt_ne {x y : BitVec n} : x.toInt ≠ y.toInt ↔ x ≠ y  := by
   unfold BitVec.ofInt
   simp
 
-theorem toInt_ofNat {n : Nat} (x : Nat) :
-  (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
-  simp [toInt_eq_toNat_bmod]
+theorem toInt_ofNat {n : Nat} (x : Nat) : (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
+  simp [toInt_eq_toNat_bmod, -Int.natCast_pow]
 
 @[simp] theorem toInt_ofInt {n : Nat} (i : Int) :
   (BitVec.ofInt n i).toInt = i.bmod (2^n) := by
   have _ := Nat.two_pow_pos n
   have p : 0 ≤ i % (2^n : Nat) := by omega
-  simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
+  simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p, -Int.natCast_pow]
 
 theorem toInt_ofInt_eq_self {w : Nat} (hw : 0 < w) {n : Int}
     (h : -2 ^ (w - 1) ≤ n) (h' : n < 2 ^ (w - 1)) : (BitVec.ofInt w n).toInt = n := by
   have hw : w = (w - 1) + 1 := by omega
-  rw [toInt_ofInt, Int.bmod_eq_self_of_le] <;> (rw [hw]; simp [Int.natCast_pow]; omega)
+  rw [toInt_ofInt, Int.bmod_eq_of_le] <;> (rw [hw]; simp [Int.natCast_pow]; omega)
 
 @[simp] theorem ofInt_natCast (w n : Nat) :
   BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl
@@ -676,16 +689,13 @@ theorem toInt_ofInt_eq_self {w : Nat} (hw : 0 < w) {n : Int}
 @[simp] theorem ofInt_ofNat (w n : Nat) :
   BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl
 
-@[simp] theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x := by
-  by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [←getLsbD_eq_getElem, getLsbD, h, BitVec.toInt]
-
 theorem toInt_neg_iff {w : Nat} {x : BitVec w} :
     BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by
-  simp [toInt_eq_toNat_cond]; omega
+  simp only [toInt_eq_toNat_cond]; omega
 
 theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
     0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
-  simp [toInt_eq_toNat_cond]; omega
+  simp only [toInt_eq_toNat_cond]; omega
 
 theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
   obtain ⟨a, ha⟩ := a
@@ -777,6 +787,12 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by
     rw [(show w = w - 1 + 1 by omega), Int.pow_succ] at this
     omega
 
+@[simp] theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x := by
+  apply eq_of_toInt_eq
+  rw [toInt_ofInt, Int.bmod_eq_of_le_mul_two]
+  · simpa [Int.mul_comm _ 2] using le_two_mul_toInt
+  · simpa [Int.mul_comm _ 2] using two_mul_toInt_lt
+
 /-! ### sle/slt -/
 
 /--
@@ -795,7 +811,7 @@ theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
     omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/
   · intros h
     simp only [h, ↓reduceIte] at this
-    simp [BitVec.slt, this]
+    simp only [BitVec.slt, this, toInt_zero, decide_eq_true_eq]
     omega
 
 theorem slt_zero_eq_msb {w : Nat} {x : BitVec  w} : x.slt 0#w = x.msb := by
@@ -866,7 +882,7 @@ theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
 
 @[simp] theorem toInt_setWidth (x : BitVec w) :
     (x.setWidth v).toInt = Int.bmod x.toNat (2^v) := by
-  simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]
+  simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod, -Int.natCast_pow]
 
 @[simp] theorem toFin_setWidth {x : BitVec w} :
     (x.setWidth v).toFin = Fin.ofNat' (2^v) x.toNat := by
@@ -1059,7 +1075,7 @@ and the second `setWidth` is a non-trivial extension.
 theorem toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} :
     (setWidth' p x).toInt = if m = n then x.toInt else x.toNat := by
   split
-  case isTrue h   => simp [h, toInt_eq_toNat_bmod]
+  case isTrue h   => simp [h, toInt_eq_toNat_bmod, -Int.natCast_pow]
   case isFalse h  => rw [toInt_setWidth'_of_lt (by omega)]
 
 @[simp] theorem toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
@@ -1267,7 +1283,7 @@ theorem extractLsb'_eq_zero {x : BitVec w} {start : Nat} :
   · subst h
     simp
   · have : 1 < 2 ^ w := by simp [h]
-    simp [BitVec.toInt]
+    simp [BitVec.toInt, -Int.natCast_pow]
     omega
 
 @[simp] theorem toFin_allOnes : (allOnes w).toFin = Fin.ofNat' (2^w) (2^w - 1) := by
@@ -1627,7 +1643,8 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 @[simp] theorem toInt_not {x : BitVec w} :
     (~~~x).toInt = Int.bmod (2^w - 1 - x.toNat) (2^w) := by
   rw_mod_cast [BitVec.toInt, BitVec.toNat_not, Int.bmod_def]
-  simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega]
+  simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega,
+    -Int.natCast_pow]
   rw_mod_cast [Nat.mod_eq_of_lt (by omega)]
   omega
 
@@ -1803,7 +1820,7 @@ theorem not_xor_right {x y : BitVec w} : ~~~ (x ^^^ y) = x ^^^ ~~~ y := by
 @[simp] theorem toInt_shiftLeft {x : BitVec w} :
     (x <<< n).toInt = (x.toNat <<< n : Int).bmod (2^w) := by
   rw [toInt_eq_toNat_bmod, toNat_shiftLeft, Nat.shiftLeft_eq]
-  simp
+  simp [-Int.natCast_pow]
 
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
     (x <<< n).toFin = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
@@ -2032,7 +2049,6 @@ theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) :
       have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le (by decide) (by omega)
       omega
     simp [this] at h
-    omega
 
 /--
 Unsigned shift right by at least one bit makes the interpretations of the bitvector as an `Int` or `Nat` agree,
@@ -2137,8 +2153,8 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) :
     simp only [hxbound, ↓reduceIte, toNat_ofInt, toNat_not, toNat_ushiftRight]
     rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (by omega),
         Nat.pred_eq_sub_one, Int.negSucc_shiftRight,
-        Int.emod_negSucc, Int.natAbs_ofNat, Nat.succ_eq_add_one,
-        Int.subNatNat_of_le (by omega), Int.toNat_ofNat, Nat.mod_eq_of_lt,
+        Int.emod_negSucc, Int.natAbs_natCast, Nat.succ_eq_add_one,
+        Int.subNatNat_of_le (by omega), Int.toNat_natCast, Nat.mod_eq_of_lt,
         Nat.sub_right_comm]
     omega
     · rw [Nat.shiftRight_eq_div_pow]
@@ -2334,7 +2350,7 @@ theorem toInt_sshiftRight {x : BitVec w} {n : Nat} :
     have := @toInt_shiftRight_lt w x n
     have := @le_toInt_shiftRight w x n
     norm_cast at *
-    exact Int.bmod_eq_self_of_le (by omega) (by omega)
+    exact Int.bmod_eq_of_le (by omega) (by omega)
 
 /-! ### sshiftRight reductions from BitVec to Nat -/
 
@@ -2427,9 +2443,9 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
     toNat_setWidth, hmsb, ↓reduceIte]
   norm_cast
   rw [Int.ofNat_sub_ofNat_of_lt, Int.negSucc_emod]
-  simp only [Int.natAbs_ofNat, Nat.succ_eq_add_one]
+  simp only [Int.natAbs_natCast, Nat.succ_eq_add_one]
   rw [Int.subNatNat_of_le]
-  · rw [Int.toNat_ofNat, Nat.add_comm, Nat.sub_add_eq]
+  · rw [Int.toNat_natCast, Nat.add_comm, Nat.sub_add_eq]
   · apply Nat.le_trans
     · apply Nat.succ_le_of_lt
       apply Nat.mod_lt
@@ -2536,10 +2552,10 @@ where
       simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]
       omega
     have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega)
-    simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]
+    simp only [this, toNat_setWidth, Int.natCast_add, Int.natCast_emod, Int.natCast_mul]
     by_cases h : x.msb
     <;> norm_cast
-    <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
+    <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H), -Int.natCast_pow]
     omega
 
 /--
@@ -3314,7 +3330,7 @@ theorem setWidth_add (x y : BitVec w) (h : i ≤ w) :
 
 @[simp, bitvec_to_nat] theorem toInt_add (x y : BitVec w) :
   (x + y).toInt = (x.toInt + y.toInt).bmod (2^w) := by
-  simp [toInt_eq_toNat_bmod]
+  simp [toInt_eq_toNat_bmod, -Int.natCast_pow]
 
 theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
     BitVec.ofInt n x + BitVec.ofInt n y := by
@@ -3344,7 +3360,7 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
 
 @[simp, bitvec_to_nat] theorem toInt_sub {x y : BitVec w} :
     (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w) := by
-  simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
+  simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega), -Int.natCast_pow]
 
 theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
     (x.toInt - y.toInt < - 2 ^ (w - 1))
@@ -3356,7 +3372,7 @@ theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
     simp only [Nat.add_one_sub_one]
     constructor
     · intros h
-      rw_mod_cast [← Int.bmod_add_cancel, Int.bmod_eq_self_of_le]
+      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))
       push_cast at this
@@ -3373,7 +3389,7 @@ theorem twoPow_le_toInt_sub_toInt_iff {x y : BitVec w} :
     constructor
     · intros h
       simp only [show 0 ≤ x.toInt by omega, show y.toInt < 0 by omega, _root_.true_and]
-      rw_mod_cast [← Int.bmod_sub_cancel, Int.bmod_eq_self_of_le (by omega) (by omega)]
+      rw_mod_cast [← Int.sub_bmod_right, Int.bmod_eq_of_le (by omega) (by omega)]
       omega
     · have := Int.bmod_neg_iff (x := x.toInt - y.toInt) (m := 2 ^ (w + 1))
       push_cast at this
@@ -3653,6 +3669,13 @@ theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := b
 @[simp, bitvec_to_nat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
 @[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
 
+theorem ofNat_mul {n} (x y : Nat) : BitVec.ofNat n (x * y) = BitVec.ofNat n x * BitVec.ofNat n y := by
+  apply eq_of_toNat_eq
+  simp [BitVec.ofNat, Fin.ofNat'_mul]
+
+theorem ofNat_mul_ofNat {n} (x y : Nat) : BitVec.ofNat n x * BitVec.ofNat n y = BitVec.ofNat n (x * y) :=
+  (ofNat_mul x y).symm
+
 protected theorem mul_comm (x y : BitVec w) : x * y = y * x := by
   apply eq_of_toFin_eq; simpa using Fin.mul_comm ..
 instance : Std.Commutative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_comm⟩
@@ -3700,7 +3723,7 @@ theorem two_mul {x : BitVec w} : 2#w * x = x + x := by rw [BitVec.mul_comm, mul_
 
 @[simp, bitvec_to_nat] theorem toInt_mul (x y : BitVec w) :
   (x * y).toInt = (x.toInt * y.toInt).bmod (2^w) := by
-  simp [toInt_eq_toNat_bmod]
+  simp [toInt_eq_toNat_bmod, -Int.natCast_pow]
 
 theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
     BitVec.ofInt n x * BitVec.ofInt n y := by
@@ -3746,6 +3769,22 @@ theorem setWidth_mul (x y : BitVec w) (h : i ≤ w) :
   have dvd : 2^i ∣ 2^w := Nat.pow_dvd_pow _ h
   simp [bitvec_to_nat, h, Nat.mod_mod_of_dvd _ dvd]
 
+/-! ### pow -/
+
+@[simp]
+protected theorem pow_zero {x : BitVec w} : x ^ 0 = 1#w := rfl
+
+protected theorem pow_succ {x : BitVec w} : x ^ (n + 1) = x ^ n * x := rfl
+
+@[simp]
+protected theorem pow_one {x : BitVec w} : x ^ 1 = x := by simp [BitVec.pow_succ]
+
+protected theorem pow_add {x : BitVec w} {n m : Nat}: x ^ (n + m) = (x ^ n) * (x ^ m):= by
+  induction m with
+  | zero => simp
+  | succ m ih =>
+    rw [← Nat.add_assoc, BitVec.pow_succ, ih, BitVec.mul_assoc, BitVec.pow_succ]
+
 /-! ### le and lt -/
 
 @[bitvec_to_nat] theorem le_def {x y : BitVec n} :
@@ -3836,7 +3875,7 @@ theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w := by
 theorem lt_one_iff {x : BitVec w} (h : 0 < w) : x < 1#w ↔ x = 0#w := by
   constructor
   · intro h₂
-    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.ofNat_emod, Int.ofNat_one, Int.natCast_pow,
+    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.natCast_emod, Int.ofNat_one, Int.natCast_pow,
       Int.ofNat_two, @Int.emod_eq_of_lt 1 (2^w) (by omega) (by omega)] at h₂
     simp [toNat_eq, show x.toNat = 0 by omega]
   · simp_all
@@ -3958,7 +3997,6 @@ then `x / y` is nonnegative, thus `toInt` and `toNat` coincide.
 theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
     (x / y).toInt = x.toNat / y.toNat := by
   simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]
-  norm_cast
 
 /-! ### umod -/
 
@@ -4116,6 +4154,110 @@ theorem sdiv_self {x : BitVec w} :
       rcases x.msb with msb | msb <;> simp
     · rcases x.msb with msb | msb <;> simp [h]
 
+/-- Unsigned division never overflows. -/
+theorem toNat_div_toNat_lt {w : Nat} {x y : BitVec w} :
+    x.toNat / y.toNat < 2 ^ w := by
+  have hy : y.toNat = 0 ∨ y.toNat = 1 ∨ 1 < y.toNat := by omega
+  rcases hy with hy|hy|hy
+  · simp [hy]; omega
+  · simp [hy]; omega
+  · rw [Nat.div_lt_iff_lt_mul (k := y.toNat) (x := x.toNat) (y := 2 ^ w) (by omega), show x.toNat = x.toNat * 1 by omega]
+    apply Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega)
+
+/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonneg. -/
+theorem toInt_ediv_toInt_lt_of_nonneg_of_nonneg {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : 0 ≤ y.toInt) :
+    x.toInt / y.toInt < 2 ^ (w - 1) := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
+    by_cases hy' : y.toInt = 1
+    · simp [hy', Int.ediv_one]; omega
+    · by_cases hx' : x.toInt = 0
+      · simp only [hx', Int.zero_ediv, Nat.add_one_sub_one, gt_iff_lt]
+        norm_cast
+        exact Nat.two_pow_pos (w := w)
+      · have := Int.ediv_lt_self_of_pos_of_ne_one (x := x.toInt) (y := y.toInt) (by omega) (by omega)
+        simp; omega
+
+/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is nonneg. -/
+theorem toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : 0 ≤ y.toInt) :
+    x.toInt / y.toInt ≤ 0 := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · by_cases hx' : x.toInt = 0
+    · simp [hx']
+    · by_cases hy' : y.toInt = 0
+      · simp [hy']
+      · have := Int.ediv_neg_of_neg_of_pos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
+        simp; omega
+
+/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonpos. -/
+theorem toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : y.toInt ≤ 0) :
+   x.toInt / y.toInt ≤ 0 := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · by_cases hy' : y.toInt = -1
+    · simp [hy']; omega
+    · have := Int.ediv_nonpos_of_nonneg_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
+      simp; omega
+
+/-- Given the definition of ediv/emod for signed integer division (https://dl.acm.org/doi/pdf/10.1145/128861.128862)
+  we have that for two integers `x` and `y`: `x/y = q ↔ x.ediv y = q ↔ r = x.emod y`
+  and in particular: `-1/y = q ↔ -1.ediv y = q ↔ r = -1.emod y`.
+  from which it follows that:
+  (-1)/0 = 0
+  (-1)/y = -1 when 0 < y
+  (-1)/(-5) = 1 when y < 0
+-/
+theorem neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} :
+    (-1) / y.toInt = if y.toInt = 0 then 0 else if 0 < y.toInt then -1 else 1 := by
+  rcases w with _|_|w
+  · simp [of_length_zero]
+  · cases eq_zero_or_eq_one y
+    · case _ h => simp [h]
+    · case _ h => simp [h]
+  · by_cases 0 < y.toInt
+    · simp [Int.sign_eq_one_of_pos (a := y.toInt) (by omega), Int.neg_one_ediv]
+      omega
+    · by_cases hy : y.toInt = 0
+      · simp [hy]
+      · simp [Int.sign_eq_neg_one_of_neg (a := y.toInt) (by omega), Int.neg_one_ediv]
+        omega
+
+/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is less than -1. -/
+theorem toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : y.toInt < -1) :
+    x.toInt / y.toInt < 2 ^ (w - 1) := by
+  rcases w with _|_|w
+  · simp [of_length_zero]
+  · have hy := eq_zero_or_eq_one (a := y)
+    simp [← toInt_inj, toInt_zero, toInt_one] at hy
+    omega
+  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
+    have hx' : x.toInt = 0 ∨ x.toInt = - 1 ∨ x.toInt < - 1 := by omega
+    rcases hx' with hx'|hx'|hx'
+    · simp [hx']; omega
+    · have := BitVec.neg_one_ediv_toInt_eq (y := y)
+      simp only [toInt_allOnes, Nat.lt_add_left_iff_pos, Nat.zero_lt_succ, ↓reduceIte,
+        Int.reduceNeg] at this
+      simp [hx', this]
+      omega
+    · have := Int.ediv_lt_natAbs_self_of_lt_neg_one_of_lt_neg_one (x := x.toInt) (y := y.toInt) (by omega) hy
+      simp; omega
+
+/-- Signed division of (x y : BitVec w) is always -2 ^ w ≤ x.toInt / y.toInt. -/
+theorem neg_two_pow_le_toInt_ediv {x y : BitVec w} :
+    - 2 ^ (w - 1) ≤ x.toInt / y.toInt := by
+  have xlt := @toInt_lt w x; have lex := @le_toInt w x
+  by_cases hx : 0 ≤ x.toInt <;> by_cases hy : 0 ≤ y.toInt
+  · have := Int.ediv_nonneg_of_nonneg_of_nonneg (x := x.toInt) (y := y.toInt) hx hy
+    omega
+  · have := Int.neg_self_le_ediv_of_nonneg_of_nonpos (x := x.toInt) (y := y.toInt) hx (by omega)
+    omega
+  · have := Int.self_le_ediv_of_nonpos_of_nonneg (x := x.toInt) (y := y.toInt) (by omega) hy
+    omega
+  · have := Int.ediv_nonneg_of_nonpos_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
+    omega
+
 /-! ### smtSDiv -/
 
 theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
@@ -4891,7 +5033,6 @@ theorem intMin_eq_zero_iff {w : Nat} : intMin w = 0#w ↔ w = 0 := by
   · constructor
     · have := Nat.two_pow_pos (w - 1)
       simp [toNat_eq, show 0 < w by omega]
-      omega
     · simp [h]
 
 /--
@@ -4919,7 +5060,7 @@ theorem toInt_intMin_le (x : BitVec w) :
   cases w
   case zero => simp [toInt_intMin, @of_length_zero x]
   case succ w =>
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod]
     have : 0 < 2 ^ w := Nat.two_pow_pos w
     rw [Int.emod_eq_of_lt (by omega) (by omega)]
     rw [BitVec.toInt_eq_toNat_bmod]
@@ -5114,6 +5255,22 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
     BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
   omega
 
+theorem sdiv_neg_one {w : Nat} {x : BitVec w} :
+    x.toInt / -1 = -x.toInt := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · simp [toInt_allOnes]
+
+theorem sdivOverflow_eq_negOverflow_of_eq_allOnes {w : Nat} {x y : BitVec w} (hy : y = allOnes w) :
+    sdivOverflow x y = negOverflow x := by
+  rcases w with _|w
+  · simp [sdivOverflow, negOverflow, of_length_zero]
+  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
+    simp only [sdivOverflow, hy, show ¬2 ^ w < x.toInt by omega, negOverflow]
+    by_cases hx : x.toInt = - 2 ^ w
+    · simp [hx]
+    · simp [show ¬x.toInt == -2 ^ w by simp only [beq_iff_eq, hx, not_false_eq_true]]; omega
+
 theorem two_pow_le_toInt_mul_toInt_iff {x y : BitVec w} :
     2 ^ (w - 1) ≤ x.toInt * y.toInt ↔
       (signExtend (w * 2) (intMax w)).slt (signExtend (w * 2) x * signExtend (w * 2) y) := by
@@ -5129,7 +5286,7 @@ theorem two_pow_le_toInt_mul_toInt_iff {x y : BitVec w} :
       toInt_intMax, Nat.add_one_sub_one]
     push_cast
     rw [← Nat.two_pow_pred_add_two_pow_pred (by omega),
-      Int.bmod_eq_self_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega)
+      Int.bmod_eq_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega)
                               (by rw [← Nat.mul_two]; push_cast; omega)]
     omega
 
@@ -5146,19 +5303,27 @@ theorem toInt_mul_toInt_lt_neg_two_pow_iff {x y : BitVec w} :
     simp only [toInt_twoPow, show ¬w + 1 ≤ w by omega, ↓reduceIte]
     push_cast
     rw [← Nat.two_pow_pred_add_two_pow_pred (by omega),
-      Int.bmod_eq_self_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega)
+      Int.bmod_eq_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega)
                               (by rw [← Nat.mul_two]; push_cast; omega)]
 
 /-! ### neg -/
 
 theorem msb_eq_toInt {x : BitVec w}:
     x.msb = decide (x.toInt < 0) := by
-  by_cases h : x.msb <;> simp [h, toInt_eq_msb_cond] <;> omega
+  by_cases h : x.msb <;> simp [h, toInt_eq_msb_cond, -Int.natCast_pow] <;> omega
 
 theorem msb_eq_toNat {x : BitVec w}:
     x.msb = decide (x.toNat ≥ 2 ^ (w - 1)) := by
   simp only [msb_eq_decide, ge_iff_le]
 
+/-- Negating a bitvector created from a natural number equals
+creating a bitvector from the the negative of that number.
+-/
+theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
+    - BitVec.ofNat w x = BitVec.ofInt w (- x) := by
+  apply BitVec.eq_of_toInt_eq
+  simp [BitVec.toInt_neg, BitVec.toInt_ofNat]
+
 /-! ### abs -/
 
 theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl

src/Init/Data/Bool.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 F. G. Dorais. No rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
+module
+
 prelude
 import Init.NotationExtra
 
@@ -690,9 +692,5 @@ def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
 
 /-! ### subtypes -/
 
-@[simp] theorem Subtype.beq_iff {α : Type u} [DecidableEq α] {p : α → Prop} {x y : {a : α // p a}} :
-    (x == y) = (x.1 == y.1) := by
-  cases x
-  cases y
-  rw [Bool.eq_iff_iff]
-  simp [beq_iff_eq]
+@[simp] theorem Subtype.beq_iff {α : Type u} [BEq α] {p : α → Prop} {x y : {a : α // p a}} :
+    (x == y) = (x.1 == y.1) := rfl

src/Init/Data/ByteArray.lean

@@ -3,5 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.ByteArray.Basic

src/Init/Data/ByteArray/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.Subarray

src/Init/Data/Cast.lean

@@ -3,6 +3,8 @@ Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
+module
+
 prelude
 import Init.Coe
 

src/Init/Data/Channel.lean

@@ -1,149 +0,0 @@
-/-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
--/
-prelude
-import Init.Data.Queue
-import Init.System.Promise
-import Init.System.Mutex
-
-set_option linter.deprecated false
-
-namespace IO
-
-/--
-Internal state of an `Channel`.
-
-We maintain the invariant that at all times either `consumers` or `values` is empty.
--/
-@[deprecated "Use Std.Channel.State from Std.Sync.Channel instead" (since := "2024-12-02")]
-structure Channel.State (α : Type) where
-  values : Std.Queue α := ∅
-  consumers : Std.Queue (Promise (Option α)) := ∅
-  closed := false
-  deriving Inhabited
-
-/--
-FIFO channel with unbounded buffer, where `recv?` returns a `Task`.
-
-A channel can be closed.  Once it is closed, all `send`s are ignored, and
-`recv?` returns `none` once the queue is empty.
--/
-@[deprecated "Use Std.Channel from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel (α : Type) : Type := Mutex (Channel.State α)
-
-instance : Nonempty (Channel α) :=
-  inferInstanceAs (Nonempty (Mutex _))
-
-/-- Creates a new `Channel`. -/
-@[deprecated "Use Std.Channel.new from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel.new : BaseIO (Channel α) :=
-  Mutex.new {}
-
-/--
-Sends a message on an `Channel`.
-
-This function does not block.
--/
-@[deprecated "Use Std.Channel.send from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel.send (ch : Channel α) (v : α) : BaseIO Unit :=
-  ch.atomically do
-    let st ← get
-    if st.closed then return
-    if let some (consumer, consumers) := st.consumers.dequeue? then
-      consumer.resolve (some v)
-      set { st with consumers }
-    else
-      set { st with values := st.values.enqueue v }
-
-/--
-Closes an `Channel`.
--/
-@[deprecated "Use Std.Channel.close from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel.close (ch : Channel α) : BaseIO Unit :=
-  ch.atomically do
-    let st ← get
-    for consumer in st.consumers.toArray do consumer.resolve none
-    set { st with closed := true, consumers := ∅ }
-
-/--
-Receives a message, without blocking.
-The returned task waits for the message.
-Every message is only received once.
-
-Returns `none` if the channel is closed and the queue is empty.
--/
-@[deprecated "Use Std.Channel.recv? from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel.recv? (ch : Channel α) : BaseIO (Task (Option α)) :=
-  ch.atomically do
-    let st ← get
-    if let some (a, values) := st.values.dequeue? then
-      set { st with values }
-      return .pure a
-    else if !st.closed then
-      let promise ← Promise.new
-      set { st with consumers := st.consumers.enqueue promise }
-      return promise.result
-    else
-      return .pure none
-
-/--
-`ch.forAsync f` calls `f` for every messages received on `ch`.
-
-Note that if this function is called twice, each `forAsync` only gets half the messages.
--/
-@[deprecated "Use Std.Channel.forAsync from Std.Sync.Channel instead" (since := "2024-12-02")]
-partial def Channel.forAsync (f : α → BaseIO Unit) (ch : Channel α)
-    (prio : Task.Priority := .default) : BaseIO (Task Unit) := do
-  BaseIO.bindTask (prio := prio) (← ch.recv?) fun
-    | none => return .pure ()
-    | some v => do f v; ch.forAsync f prio
-
-/--
-Receives all currently queued messages from the channel.
-
-Those messages are dequeued and will not be returned by `recv?`.
--/
-@[deprecated "Use Std.Channel.recvAllCurrent from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel.recvAllCurrent (ch : Channel α) : BaseIO (Array α) :=
-  ch.atomically do
-    modifyGet fun st => (st.values.toArray, { st with values := ∅ })
-
-/-- Type tag for synchronous (blocking) operations on a `Channel`. -/
-@[deprecated "Use Std.Channel.Sync from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel.Sync := Channel
-
-/--
-Accesses synchronous (blocking) version of channel operations.
-
-For example, `ch.sync.recv?` blocks until the next message,
-and `for msg in ch.sync do ...` iterates synchronously over the channel.
-These functions should only be used in dedicated threads.
--/
-@[deprecated "Use Std.Channel.sync from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel.sync (ch : Channel α) : Channel.Sync α := ch
-
-/--
-Synchronously receives a message from the channel.
-
-Every message is only received once.
-Returns `none` if the channel is closed and the queue is empty.
--/
-@[deprecated "Use Std.Channel.Sync.recv? from Std.Sync.Channel instead" (since := "2024-12-02")]
-def Channel.Sync.recv? (ch : Channel.Sync α) : BaseIO (Option α) := do
-  IO.wait (← Channel.recv? ch)
-
-@[deprecated "Use Std.Channel.Sync.forIn from Std.Sync.Channel instead" (since := "2024-12-02")]
-private partial def Channel.Sync.forIn [Monad m] [MonadLiftT BaseIO m]
-    (ch : Channel.Sync α) (f : α → β → m (ForInStep β)) : β → m β := fun b => do
-  match ← ch.recv? with
-    | some a =>
-      match ← f a b with
-        | .done b => pure b
-        | .yield b => ch.forIn f b
-    | none => pure b
-
-/-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed. -/
-instance [MonadLiftT BaseIO m] : ForIn m (Channel.Sync α) α where
-  forIn ch b f := ch.forIn f b

src/Init/Data/Char.lean

@@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Char.Basic
 import Init.Data.Char.Lemmas

src/Init/Data/Char/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.UInt.BasicAux
 

src/Init/Data/Char/Lemmas.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 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
 -/
+module
+
 prelude
 import Init.Data.Char.Basic
 import Init.Data.UInt.Lemmas

src/Init/Data/Fin.lean

@@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Fin.Log2

src/Init/Data/Fin/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
+module
+
 prelude
 import Init.Data.Nat.Bitwise.Basic
 

src/Init/Data/Fin/Bitwise.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
+module
+
 prelude
 import Init.Data.Nat.Bitwise
 import Init.Data.Fin.Basic

src/Init/Data/Fin/Fold.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 François G. Dorais. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: François G. Dorais
 -/
+module
+
 prelude
 import Init.Data.Nat.Linear
 import Init.Control.Lawful.Basic

src/Init/Data/Fin/Iterate.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix
 -/
+module
+
 prelude
 import Init.PropLemmas
 import Init.Data.Fin.Basic

src/Init/Data/Fin/Lemmas.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Nat.Lemmas
@@ -172,13 +174,13 @@ theorem mk_le_of_le_val {b : Fin n} {a : Nat} (h : a ≤ b) :
 
 @[simp] theorem mk_zero : (⟨0, Nat.succ_pos n⟩ : Fin (n + 1)) = 0 := rfl
 
-@[simp] theorem zero_le (a : Fin (n + 1)) : 0 ≤ a := Nat.zero_le a.val
+@[simp] theorem zero_le [NeZero n] (a : Fin n) : 0 ≤ a := Nat.zero_le a.val
 
 theorem zero_lt_one : (0 : Fin (n + 2)) < 1 := Nat.zero_lt_one
 
-@[simp] theorem not_lt_zero (a : Fin (n + 1)) : ¬a < 0 := nofun
+@[simp] theorem not_lt_zero [NeZero n] (a : Fin n) : ¬a < 0 := nofun
 
-theorem pos_iff_ne_zero {a : Fin (n + 1)} : 0 < a ↔ a ≠ 0 := by
+theorem pos_iff_ne_zero [NeZero n] {a : Fin n} : 0 < a ↔ a ≠ 0 := by
   rw [lt_def, val_zero, Nat.pos_iff_ne_zero, ← val_ne_iff]; rfl
 
 theorem eq_zero_or_eq_succ {n : Nat} : ∀ i : Fin (n + 1), i = 0 ∨ ∃ j : Fin n, i = j.succ
@@ -410,6 +412,14 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 @[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
+@[simp] theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
+    Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) :=
+  Fin.ext (by simp)
+
+@[simp] theorem cast_castLT {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
+    Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) :=
+  Fin.ext (by simp)
+
 @[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
 
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=
@@ -496,17 +506,17 @@ theorem castSucc_inj {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b := by sim
 
 theorem castSucc_lt_last (a : Fin n) : a.castSucc < last n := a.is_lt
 
-@[simp] theorem castSucc_zero : castSucc (0 : Fin (n + 1)) = 0 := rfl
+@[simp] theorem castSucc_zero [NeZero n] : castSucc (0 : Fin n) = 0 := rfl
 
 @[simp] theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := rfl
 
 /-- `castSucc i` is positive when `i` is positive -/
-theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < i.castSucc := by
+theorem castSucc_pos [NeZero n] {i : Fin n} (h : 0 < i) : 0 < i.castSucc := by
   simpa [lt_def] using h
 
-@[simp] theorem castSucc_eq_zero_iff {a : Fin (n + 1)} : a.castSucc = 0 ↔ a = 0 := by simp [Fin.ext_iff]
+@[simp] theorem castSucc_eq_zero_iff [NeZero n] {a : Fin n} : a.castSucc = 0 ↔ a = 0 := by simp [Fin.ext_iff]
 
-theorem castSucc_ne_zero_iff {a : Fin (n + 1)} : a.castSucc ≠ 0 ↔ a ≠ 0 :=
+theorem castSucc_ne_zero_iff [NeZero n] {a : Fin n} : a.castSucc ≠ 0 ↔ a ≠ 0 :=
   not_congr <| castSucc_eq_zero_iff
 
 theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
@@ -976,16 +986,28 @@ theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b
 
 /-! ### mul -/
 
+theorem ofNat'_mul [NeZero n] (x : Nat) (y : Fin n) :
+    Fin.ofNat' n x * y = Fin.ofNat' n (x * y.val) := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.mul_def]
+
+theorem mul_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
+    x * Fin.ofNat' n y = Fin.ofNat' n (x.val * y) := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.mul_def]
+
 theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 
 theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 
-protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
-  match n with
-  | 0 => exact Subsingleton.elim (α := Fin 1) ..
-  | n+1 => simp [Fin.ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
+protected theorem mul_one [i : NeZero n] (k : Fin n) : k * 1 = k := by
+  match n, i with
+  | n + 1, _ =>
+    match n with
+    | 0 => exact Subsingleton.elim (α := Fin 1) ..
+    | n+1 => simp [Fin.ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
 
 protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
   Fin.ext <| by rw [mul_def, mul_def, Nat.mul_comm]
@@ -998,15 +1020,17 @@ protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
   simp only [← Nat.mul_mod, Nat.mul_assoc]
 instance : Std.Associative (α := Fin n) (· * ·) := ⟨Fin.mul_assoc⟩
 
-protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
+protected theorem one_mul [NeZero n] (k : Fin n) : (1 : Fin n) * k = k := by
   rw [Fin.mul_comm, Fin.mul_one]
-instance : Std.LawfulIdentity (α := Fin (n + 1)) (· * ·) 1 where
+
+instance [NeZero n] : Std.LawfulIdentity (α := Fin n) (· * ·) 1 where
   left_id := Fin.one_mul
   right_id := Fin.mul_one
 
-protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [Fin.ext_iff, mul_def]
+protected theorem mul_zero [NeZero n] (k : Fin n) : k * 0 = 0 := by
+  simp [Fin.ext_iff, mul_def]
 
-protected theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0 := by
+protected theorem zero_mul [NeZero n] (k : Fin n) : (0 : Fin n) * k = 0 := by
   simp [Fin.ext_iff, mul_def]
 
 end Fin

src/Init/Data/Fin/Log2.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+module
+
 prelude
 import Init.Data.Nat.Log2
 

src/Init/Data/Float.lean

@@ -3,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Core
 import Init.Data.Int.Basic
@@ -289,8 +291,11 @@ implementation.
 instance : Inhabited Float where
   default := UInt64.toFloat 0
 
+protected def Float.repr (n : Float) (prec : Nat) : Std.Format :=
+  if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
+
 instance : Repr Float where
-  reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
+  reprPrec := Float.repr
 
 instance : ReprAtom Float  := ⟨⟩
 

src/Init/Data/Float32.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 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
 -/
+module
+
 prelude
 import Init.Core
 import Init.Data.Int.Basic
@@ -290,8 +292,11 @@ implementation.
 instance : Inhabited Float32 where
   default := UInt64.toFloat32 0
 
+protected def Float32.repr (n : Float32) (prec : Nat) : Std.Format :=
+  if n < UInt64.toFloat32 0 then Repr.addAppParen (toString n) prec else toString n
+
 instance : Repr Float32 where
-  reprPrec n prec := if n < UInt64.toFloat32 0 then Repr.addAppParen (toString n) prec else toString n
+  reprPrec := Float32.repr
 
 instance : ReprAtom Float32  := ⟨⟩