feat: track set of added case-splits

.github/workflows/build-template.yml

@@ -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 script/prepare-*
+          git checkout FETCH_HEAD flake.nix flake.lock
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
       - name: Setup emsdk
@@ -99,6 +99,7 @@ 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,21 +139,20 @@ 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/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/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",
@@ -161,23 +160,25 @@ 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/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/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",
-                "check-level": 0,
-                // just a secondary build job for now until false positives can be excluded
+                // just a secondary PR build job for now
+                "check-level": isPr ? 0 : 3,
                 "secondary": true,
                 "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
-                // TODO: importStructure is not compatible with .olean caching
-                // TODO: why does scopedMacros fail?
-                "CTEST_OPTIONS": "-E 'scopedMacros|importStructure'"
+                // TODO: why does this fail?
+                "CTEST_OPTIONS": "-E 'scopedMacros'"
               },
+              */
               {
                 "name": "Linux",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-4x8" : "ubuntu-latest",
@@ -209,7 +210,7 @@ jobs:
                 "release": true,
                 "check-level": 2,
                 "shell": "bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/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
@@ -220,7 +221,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/19.1.2/lean-llvm-aarch64-apple-darwin.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
@@ -241,7 +242,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/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
                 "binary-check": "ldd"
               },
@@ -252,21 +253,20 @@ 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/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*"
               },
-              // Started running out of memory building expensive modules, a 2GB heap is just not that much even before fragmentation
-              //{
-              //  "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": "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,10 +103,40 @@ 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

@@ -12,8 +12,6 @@ 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")
@@ -79,29 +77,26 @@ if (USE_MIMALLOC)
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-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(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}
+)
 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} ${STAGE1_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
-  DEPENDS ${EXTRA_DEPENDS}
+  DEPENDS stage0
   STEP_TARGETS configure
 )
 ExternalProject_add(stage2
@@ -113,7 +108,6 @@ 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 assertions enabled",
+      "displayName": "Release with debug info build config",
       "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "RelWithAssert"
+        "CMAKE_BUILD_TYPE": "RelWithDebInfo"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/reldebug"

flake.lock

@@ -1,50 +1,112 @@
 {
   "nodes": {
-    "nixpkgs": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
       "locked": {
-        "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"
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
-        "url": "https://channels.nixos.org/nixos-unstable/nixexprs.tar.xz"
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1710889954,
+        "narHash": "sha256-Pr6F5Pmd7JnNEMHHmspZ0qVqIBVxyZ13ik1pJtm2QXk=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "7872526e9c5332274ea5932a0c3270d6e4724f3b",
+        "type": "github"
+      },
+      "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"
       }
     },
     "nixpkgs-old": {
       "flake": false,
       "locked": {
-        "lastModified": 1582018169,
-        "narHash": "sha256-qv1iK1IchpZKSeWL3NEs4U5Jl5QVyNHDdiMJvLOI4Yc=",
-        "type": "tarball",
-        "url": "https://releases.nixos.org/nixos/19.03/nixos-19.03.173691.34c7eb7545d/nixexprs.tar.xz"
+        "lastModified": 1581379743,
+        "narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
-        "url": "https://channels.nixos.org/nixos-19.03/nixexprs.tar.xz"
+        "owner": "NixOS",
+        "ref": "nixos-19.03",
+        "repo": "nixpkgs",
+        "type": "github"
       }
     },
     "nixpkgs-older": {
       "flake": false,
       "locked": {
-        "lastModified": 1550657948,
-        "narHash": "sha256-BE0XqzNfzvhhtTXv37LyySyq4moL7z1i1hMvwbFNL/I=",
-        "type": "tarball",
-        "url": "https://releases.nixos.org/nixos/18.03/nixos-18.03.133402.cb0e20d6db9/nixexprs.tar.xz"
+        "lastModified": 1523316493,
+        "narHash": "sha256-5qJS+i5ECICPAKA6FhPLIWkhPKDnOZsZbh2PHYF1Kbs=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "0b307aa73804bbd7a7172899e59ae0b8c347a62d",
+        "type": "github"
       },
       "original": {
-        "type": "tarball",
-        "url": "https://channels.nixos.org/nixos-18.03/nixexprs.tar.xz"
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "0b307aa73804bbd7a7172899e59ae0b8c347a62d",
+        "type": "github"
       }
     },
     "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,22 +1,29 @@
 {
   description = "Lean development flake. Not intended for end users.";
 
-  # 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";
+  inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
   # old nixpkgs used for portable release with older glibc (2.27)
-  inputs.nixpkgs-old.url = "https://channels.nixos.org/nixos-19.03/nixexprs.tar.xz";
+  inputs.nixpkgs-old.url = "github:NixOS/nixpkgs/nixos-19.03";
   inputs.nixpkgs-old.flake = false;
   # old nixpkgs used for portable release with older glibc (2.26)
-  inputs.nixpkgs-older.url = "https://channels.nixos.org/nixos-18.03/nixexprs.tar.xz";
+  inputs.nixpkgs-older.url = "github:NixOS/nixpkgs/0b307aa73804bbd7a7172899e59ae0b8c347a62d";
   inputs.nixpkgs-older.flake = false;
+  # for cadical 2.1.2; sync with CMakeLists.txt by taking commit from https://www.nixhub.io/packages/cadical
+  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/199169a2135e6b864a888e89a2ace345703c025d";
+  inputs.flake-utils.url = "github:numtide/flake-utils";
 
-  outputs = inputs: builtins.foldl' inputs.nixpkgs.lib.attrsets.recursiveUpdate {} (builtins.map (system:
+  outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (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 = ./.; };
 
@@ -24,7 +31,7 @@
           stdenv = pkgs.overrideCC pkgs.stdenv lean-packages.llvmPackages.clang;
         } ({
           buildInputs = with pkgs; [
-            cmake gmp libuv ccache pkg-config
+            cmake gmp libuv ccache cadical pkg-config
             lean-packages.llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI
@@ -60,17 +67,15 @@
           GDB = pkgsDist.gdb;
         });
     in {
-      packages.${system} = {
+      packages = {
         # to be removed when Nix CI is not needed anymore
         inherit (lean-packages) cacheRoots test update-stage0-commit ciShell;
         deprecated = lean-packages;
       };
 
-      devShells.${system} = {
-        # The default development shell for working on lean itself
-        default = devShellWithDist pkgs;
-        oldGlibc = devShellWithDist pkgsDist-old;
-        oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
-      };
-    }) ["x86_64-linux" "aarch64-linux"]);
+      # The default development shell for working on lean itself
+      devShells.default = devShellWithDist pkgs;
+      devShells.oldGlibc = devShellWithDist pkgsDist-old;
+      devShells.oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
+    });
 }

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.result.imports
+             then map (m: m.module) header.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}.result.imports) else [];
+    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.imports) else [];
   }));
   allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
 

script/benchReelabRss.lean

@@ -1,5 +1,4 @@
 import Lean.Data.Lsp
-import Lean.Elab.Import
 open Lean
 open Lean.Lsp
 open Lean.JsonRpc
@@ -8,7 +7,9 @@ open Lean.JsonRpc
 Tests language server memory use by repeatedly re-elaborate a given file.
 
 NOTE: only works on Linux for now.
-ot to touch the imports for usual files.
+
+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.
 -/
 
 def main (args : List String) : IO Unit := do
@@ -32,8 +33,6 @@ 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", {
@@ -41,14 +40,15 @@ 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 := headerEndPos
-            «end» := headerEndPos
+            start := pos
+            «end» := pos
           } " "]
         }
         let params := toJson params

script/prepare-llvm-linux.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -euxo pipefail
+set -uo pipefail
 
 # run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
 # ```
@@ -14,7 +14,6 @@ set -euxo 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!
@@ -26,8 +25,6 @@ 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)
@@ -42,18 +39,18 @@ $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 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'
+# 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'
 # 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/ || true
+$CP -r llvm/include/*-*-* llvm-host/include/
 # 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/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
+for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
 OPTIONS=()
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
@@ -67,8 +64,7 @@ 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"
-# ld.so is usually included by the libc.so linker script but we discard those
-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 ROOT/lib/glibc/ld.so -Wl,--no-as-needed -fuse-ld=lld'"
+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'"
 # 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

src/CMakeLists.txt

@@ -191,11 +191,10 @@ 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")
+set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG -DLEAN_TRACE")
 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)
@@ -222,7 +221,6 @@ 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}")
@@ -242,13 +240,11 @@ 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 ()
 
@@ -369,8 +365,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 "19")
-    message(FATAL_ERROR "Unable to find llvm-config version 19. Found invalid 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}'")
   endif()
   # -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM
   string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM")
@@ -784,11 +780,12 @@ add_custom_target(clean-olean
   DEPENDS clean-stdlib)
 
 install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
-  PATTERN temp EXCLUDE
-  PATTERN "*.export" EXCLUDE
-  PATTERN "*.hash" EXCLUDE
-  PATTERN "*.trace" EXCLUDE
-  PATTERN "*.rsp" EXCLUDE)
+  PATTERN temp
+  PATTERN "*.export"
+  PATTERN "*.hash"
+  PATTERN "*.trace"
+  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)
@@ -847,4 +844,6 @@ 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,8 +3,6 @@ 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,8 +4,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -309,6 +307,9 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +5,6 @@ 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,8 +3,6 @@ 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,8 +5,6 @@ Authors: Sebastian Ullrich
 
 The identity Monad.
 -/
-module
-
 prelude
 import Init.Core
 

src/Init/Control/Lawful.lean

@@ -3,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -144,7 +142,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -100,7 +98,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 <| some a
+  pure a
 
 instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail

src/Init/Control/Reader.lean

@@ -5,8 +5,6 @@ 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,8 +5,6 @@ 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,8 +3,6 @@ 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,8 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 
 The State monad transformer using IO references.
 -/
-module
-
 prelude
 import Init.System.ST
 

src/Init/Conv.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura
 
 Notation for operators defined at Prelude.lean
 -/
-module
-
 prelude
 import Init.Tactics
 import Init.Meta
@@ -320,25 +318,6 @@ 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,8 +5,6 @@ Authors: Leonardo de Moura
 
 notation, basic datatypes and type classes
 -/
-module
-
 prelude
 import Init.Prelude
 import Init.SizeOf
@@ -23,8 +21,6 @@ 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.
@@ -742,20 +738,6 @@ 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.
 
@@ -763,9 +745,11 @@ In other words:
  * `a == b` implies `a = b`.
  * `a == a` is true.
 -/
-class LawfulBEq (α : Type u) [BEq α] : Prop extends ReflBEq α where
+class LawfulBEq (α : Type u) [BEq α] : Prop 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)
 
@@ -777,15 +761,6 @@ 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
@@ -880,8 +855,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 α] [ReflBEq α] {a b : α} (h : (a == b) = false) : a ≠ b :=
-  not_eq_of_beq_eq_false 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 beq_false_of_ne [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a == b) = false :=
   have : ¬ (a == b) = true := by
@@ -940,34 +915,6 @@ 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.
@@ -1013,7 +960,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⟩
@@ -1178,12 +1125,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
@@ -1349,15 +1296,6 @@ 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)
@@ -1626,7 +1564,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, beq_of_eq⟩
+  ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩
 
 /-! # Prop lemmas -/
 
@@ -1899,7 +1837,9 @@ 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 (eqRec_heq_iff.mpr (c a b p))
+  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)
 
 end
 end Quot
@@ -2262,27 +2202,6 @@ 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,8 +3,6 @@ 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
@@ -36,6 +34,7 @@ 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,8 +4,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -527,7 +525,7 @@ theorem countP_attachWith {p : α → Prop} {q : α → Bool} {xs : Array α} {H
   simp
 
 @[simp]
-theorem count_attach [BEq α] {xs : Array α} {a : {x // x ∈ xs}} :
+theorem count_attach [DecidableEq α] {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]
@@ -536,7 +534,7 @@ theorem count_attach [BEq α] {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 [BEq α] {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) {a : {x // p x}} :
+theorem count_attachWith [DecidableEq α] {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

src/Init/Data/Array/Basic.lean

@@ -3,8 +3,6 @@ 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
@@ -40,11 +38,11 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp, grind] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
+@[simp] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
     (set xs i v h).size = xs.size :=
   List.length_set ..
 
-@[simp, grind] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
+@[simp] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
   List.length_concat ..
 
 theorem ext {xs ys : Array α}
@@ -110,7 +108,7 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
 @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
+@[simp] 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
 
@@ -194,7 +192,7 @@ Examples:
 def pop (xs : Array α) : Array α where
   toList := xs.toList.dropLast
 
-@[simp, grind] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
+@[simp] 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]
@@ -836,7 +834,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 some b
+    | some b => return b
     | _      => pure ⟨⟩
   return none
 
@@ -867,7 +865,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 some a
+      return a
   return none
 
 /--
@@ -1175,7 +1173,7 @@ def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α :=
   Id.run do
     for a in as do
       if p a then
-        return some a
+        return a
     return none
 
 /--

src/Init/Data/Array/BasicAux.lean

@@ -3,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
-module
-
 prelude
 import Init.Data.List.TakeDrop
 
@@ -112,19 +110,19 @@ abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
-@[simp, grind] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
+@[simp] 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, grind] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
+@[simp] 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, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
+@[simp] 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

src/Init/Data/Array/Count.lean

@@ -3,8 +3,6 @@ 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
@@ -259,8 +257,8 @@ theorem filter_beq {xs : Array α} (a : α) : xs.filter (· == a) = replicate (c
   rcases xs with ⟨xs⟩
   simp [List.filter_beq]
 
-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 filter_eq {α} [DecidableEq α] {xs : Array α} (a : α) : xs.filter (· = a) = replicate (count a xs) 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
@@ -275,7 +273,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 [BEq β] [LawfulBEq β] {xs : Array α} {f : α → β} {x : α} :
+theorem count_le_count_map [DecidableEq β] {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]
@@ -290,25 +288,15 @@ theorem count_flatMap {α} [BEq β] {xs : Array α} {f : α → Array β} {x :
   rcases xs with ⟨xs⟩
   simp [List.count_flatMap, countP_flatMap, Function.comp_def]
 
-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]
+-- FIXME these theorems can be restored once `List.erase` and `Array.erase` have been related.
 
-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]
+-- 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_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_self (a : α) (l : Array α) :
+--     count a (l.erase a) = count a l - 1 := by rw [count_erase, if_pos (by simp)]
 
-@[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]
+-- @[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]
 
 end count

src/Init/Data/Array/DecidableEq.lean

@@ -3,8 +3,6 @@ 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
@@ -116,10 +114,8 @@ end List
 
 namespace Array
 
-instance [BEq α] [ReflBEq α] : ReflBEq (Array α) where
-  rfl := by simp [BEq.beq, isEqv_self_beq]
-
 instance [BEq α] [LawfulBEq α] : LawfulBEq (Array α) where
+  rfl := by simp [BEq.beq, isEqv_self_beq]
   eq_of_beq := by
     rintro ⟨_⟩ ⟨_⟩ h
     simpa using h

src/Init/Data/Array/Erase.lean

@@ -3,8 +3,6 @@ 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
@@ -61,7 +59,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₁]
+  rw [e₂]; simp [size_append, e₁]; omega
 
 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -23,14 +21,6 @@ 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
 
@@ -38,7 +28,7 @@ theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f =
   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 = some b := by
+    ∃ a, a ∈ xs ∧ f a = 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
@@ -139,8 +129,6 @@ 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]
@@ -169,9 +157,6 @@ 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
@@ -346,11 +331,6 @@ 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)
@@ -431,13 +411,6 @@ 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]
@@ -466,9 +439,6 @@ 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} :
@@ -536,13 +506,6 @@ 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
@@ -600,9 +563,6 @@ 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) :
@@ -633,21 +593,6 @@ 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

src/Init/Data/Array/GetLit.lean

@@ -4,8 +4,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -152,13 +150,13 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
     Std.Total (· ≤ · : Array α → Array α → Prop) where
   total := Array.le_total
 
-@[simp] theorem lex_eq_true_iff_lt [BEq α] [LawfulBEq α] [LT α] [DecidableLT α]
+@[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
     {xs ys : Array α} : lex xs ys = true ↔ xs < ys := by
   cases xs
   cases ys
   simp
 
-@[simp] theorem lex_eq_false_iff_ge [BEq α] [LawfulBEq α] [LT α] [DecidableLT α]
+@[simp] theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
     {xs ys : Array α} : lex xs ys = false ↔ ys ≤ xs := by
   cases xs
   cases ys

src/Init/Data/Array/MapIdx.lean

@@ -3,8 +3,6 @@ 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
@@ -66,7 +64,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 => some <| f i b (getElem?_eq_some_iff.1 h).1 := by
+      xs[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
@@ -155,7 +153,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]? = some x := by
+    (x, i) ∈ xs.zipIdx ↔ xs[i]? = x := by
   rw [mk_mem_zipIdx_iff_le_and_getElem?_sub]
   simp
 

src/Init/Data/Array/Mem.lean

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

src/Init/Data/Array/OfFn.lean

@@ -3,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -22,91 +20,45 @@ 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.
 -/
-structure Perm (as bs : Array α) : Prop where
-  of_toList_perm ::
-  toList : as.toList ~ bs.toList
+def Perm (as bs : Array α) : Prop :=
+  as.toList ~ bs.toList
 
 @[inherit_doc] scoped infixl:50 " ~ " => Perm
 
-theorem perm_iff_toList_perm {as bs : Array α} : as ~ bs ↔ as.toList ~ bs.toList :=
-  ⟨Perm.toList, Perm.of_toList_perm⟩
+theorem perm_iff_toList_perm {as bs : Array α} : as ~ bs ↔ as.toList ~ bs.toList := Iff.rfl
 
-end Array
-
-namespace List
-
-open Array
-
-theorem perm_iff_toArray_perm {as bs : List α} : as ~ bs ↔ as.toArray ~ bs.toArray := by
+@[simp] theorem perm_toArray (as bs : List α) : as.toArray ~ bs.toArray ↔ as ~ bs := 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 [perm_iff_toList_perm]
+  simp
 
-protected theorem Perm.rfl {xs : Array α} : xs ~ xs := .refl _
+protected theorem Perm.rfl {xs : List α} : 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_iff_toList_perm] at h
-  simpa [perm_iff_toList_perm] using h.symm
+  simp only [perm_toArray] at h
+  simpa 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_iff_toList_perm] at h₁ h₂
-  simpa [perm_iff_toList_perm] using h₁.trans h₂
+  simp only [perm_toArray] at h₁ h₂
+  simpa 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.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) :
+theorem Perm.push (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_iff_toList_perm] at p
-  simp only [push_toArray, List.append_assoc, singleton_append, perm_iff_toList_perm]
-  exact p.append (Perm.swap ..)
+  simp only [perm_toArray] at p
+  simp only [push_toArray, List.append_assoc, singleton_append, perm_toArray]
+  exact p.append (Perm.swap' _ _ Perm.nil)
 
 theorem swap_perm {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < xs.size) :
     xs.swap i j ~ xs := by
@@ -116,15 +68,15 @@ theorem swap_perm {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < x
 namespace Perm
 
 set_option linter.indexVariables false in
-theorem extract {xs ys : Array α} (h : xs ~ ys) {lo hi : Nat}
+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
+    (xs.extract lo (hi + 1)) ~ (ys.extract lo (hi + 1)) := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp_all only [perm_iff_toList_perm, List.getElem?_toArray, List.extract_toArray,
+  simp_all only [perm_toArray, 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)
+  apply List.Perm.take' (w := fun i h => by simpa using whi (lo + i) (by omega))
+  apply List.Perm.drop' (w := wlo)
   exact h
 
 end Perm

src/Init/Data/Array/QSort.lean

@@ -1,9 +1,68 @@
 /-
-Copyright (c) 2024 Lean FRO. All rights reserved.
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
+Authors: Leonardo de Moura
 -/
-module
-
 prelude
-import Init.Data.Array.QSort.Basic
+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

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

@@ -1,81 +0,0 @@
-/-
-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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
 

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

@@ -4,8 +4,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -325,7 +323,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 (some a) (some b)) := by
+    zipWithAll f (replicate n a) (replicate n b) = replicate n (f a b) := by
   simp [← List.toArray_replicate]
 
 @[deprecated zipWithAll_replicate (since := "2025-03-18")]

src/Init/Data/BEq.lean

@@ -3,8 +3,6 @@ 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
 
@@ -21,9 +19,21 @@ 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
 
@@ -56,5 +66,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -769,15 +767,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -568,7 +566,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 [-Int.natCast_pow]; omega)
+  cases y.msb <;> (simp; omega)
 
 theorem slt_eq_ult {x y : BitVec w} :
     x.slt y = (x.msb != y.msb).xor (x.ult y) := by
@@ -1334,7 +1332,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 only [Nat.add_one_sub_one, ge_iff_le]
+    simp
     omega
 
 theorem usubOverflow_eq {w : Nat} (x y : BitVec w) :
@@ -1358,41 +1356,9 @@ 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.natCast_emod, Int.neg_inj]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_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
@@ -1490,6 +1456,7 @@ 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} :
@@ -1574,7 +1541,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.natCast_emod]
+  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.ofNat_emod]
   norm_cast
   rw [Nat.mod_eq_of_lt]
   · omega
@@ -1604,8 +1571,7 @@ 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 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
+    simp [this, wpos, toInt_intMin] at h
     omega
   · intro h
     subst h
@@ -1646,11 +1612,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, -Int.natCast_pow]
+        · simp [Int.tdiv_eq_zero_of_lt ha_nonneg (by norm_cast at *), ha_intMin]
         · 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, -Int.natCast_pow] at ha_intMin
+          · simp [wpos, ← toInt_ne, toInt_intMin] at ha_intMin
             omega
 
   · by_cases ha : a.msb <;> by_cases hb : b.msb
@@ -1669,7 +1635,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.natCast_emod, Int.neg_inj]
+        · rw [neg_neg, toNat_udiv, toNat_neg, Int.ofNat_emod, Int.neg_inj]
           norm_cast
         · rw [neg_eq_zero_iff]
           by_cases h' : -a / b = 0#w
@@ -1812,23 +1778,9 @@ 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 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
+theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
+    (x ++ 0#w) + (0#v ++ y) = x ++ y := by
   rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
 
 /-- Heuristically, `y <<< x` is much larger than `x`,
@@ -1844,10 +1796,4 @@ 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,8 +3,6 @@ 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,8 +4,6 @@ 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
@@ -23,9 +21,6 @@ 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
 
@@ -73,9 +68,6 @@ 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
@@ -141,8 +133,6 @@ 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]
 
@@ -459,7 +449,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.add_bmod_right, Int.add_comm,
+  rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm, Int.bmod_add_cancel, 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 :=
@@ -620,10 +610,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.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
   next g =>
-    rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
 
 theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by
@@ -639,12 +629,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.natCast_emod]
+    toNat_ofNat, Int.ofNat_emod]
   norm_cast
   apply Nat.mod_eq_of_lt
   apply Nat.one_lt_two_pow (by omega)
 
-/-- Prove equality of bitvectors in terms of integer operations. -/
+/-- Prove equality of bitvectors in terms of nat operations. -/
 theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by
   intro eq
   simp only [toInt_eq_toNat_cond] at eq
@@ -665,19 +655,20 @@ 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, -Int.natCast_pow]
+theorem toInt_ofNat {n : Nat} (x : Nat) :
+  (BitVec.ofNat n x).toInt = (x : Int).bmod (2^n) := by
+  simp [toInt_eq_toNat_bmod]
 
 @[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, -Int.natCast_pow]
+  simp [toInt_eq_toNat_bmod, Int.toNat_of_nonneg p]
 
 theorem toInt_ofInt_eq_self {w : Nat} (hw : 0 < w) {n : Int}
     (h : -2 ^ (w - 1) ≤ n) (h' : n < 2 ^ (w - 1)) : (BitVec.ofInt w n).toInt = n := by
   have hw : w = (w - 1) + 1 := by omega
-  rw [toInt_ofInt, Int.bmod_eq_of_le] <;> (rw [hw]; simp [Int.natCast_pow]; omega)
+  rw [toInt_ofInt, Int.bmod_eq_self_of_le] <;> (rw [hw]; simp [Int.natCast_pow]; omega)
 
 @[simp] theorem ofInt_natCast (w n : Nat) :
   BitVec.ofInt w (n : Int) = BitVec.ofNat w n := rfl
@@ -685,13 +676,16 @@ 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 only [toInt_eq_toNat_cond]; omega
+  simp [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 only [toInt_eq_toNat_cond]; omega
+  simp [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
@@ -783,12 +777,6 @@ 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 -/
 
 /--
@@ -807,7 +795,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 only [BitVec.slt, this, toInt_zero, decide_eq_true_eq]
+    simp [BitVec.slt, this]
     omega
 
 theorem slt_zero_eq_msb {w : Nat} {x : BitVec  w} : x.slt 0#w = x.msb := by
@@ -878,7 +866,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, -Int.natCast_pow]
+  simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]
 
 @[simp] theorem toFin_setWidth {x : BitVec w} :
     (x.setWidth v).toFin = Fin.ofNat' (2^v) x.toNat := by
@@ -1071,7 +1059,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, -Int.natCast_pow]
+  case isTrue h   => simp [h, toInt_eq_toNat_bmod]
   case isFalse h  => rw [toInt_setWidth'_of_lt (by omega)]
 
 @[simp] theorem toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
@@ -1279,7 +1267,7 @@ theorem extractLsb'_eq_zero {x : BitVec w} {start : Nat} :
   · subst h
     simp
   · have : 1 < 2 ^ w := by simp [h]
-    simp [BitVec.toInt, -Int.natCast_pow]
+    simp [BitVec.toInt]
     omega
 
 @[simp] theorem toFin_allOnes : (allOnes w).toFin = Fin.ofNat' (2^w) (2^w - 1) := by
@@ -1639,8 +1627,7 @@ 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,
-    -Int.natCast_pow]
+  simp [show ((2^w : Nat) : Int) - 1 - x.toNat = ((2^w - 1 - x.toNat) : Nat) by omega]
   rw_mod_cast [Nat.mod_eq_of_lt (by omega)]
   omega
 
@@ -1816,7 +1803,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 [-Int.natCast_pow]
+  simp
 
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
     (x <<< n).toFin = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
@@ -2045,6 +2032,7 @@ 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,
@@ -2149,8 +2137,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_natCast, Nat.succ_eq_add_one,
-        Int.subNatNat_of_le (by omega), Int.toNat_natCast, Nat.mod_eq_of_lt,
+        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,
         Nat.sub_right_comm]
     omega
     · rw [Nat.shiftRight_eq_div_pow]
@@ -2346,7 +2334,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_of_le (by omega) (by omega)
+    exact Int.bmod_eq_self_of_le (by omega) (by omega)
 
 /-! ### sshiftRight reductions from BitVec to Nat -/
 
@@ -2439,9 +2427,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_natCast, Nat.succ_eq_add_one]
+  simp only [Int.natAbs_ofNat, Nat.succ_eq_add_one]
   rw [Int.subNatNat_of_le]
-  · rw [Int.toNat_natCast, Nat.add_comm, Nat.sub_add_eq]
+  · rw [Int.toNat_ofNat, Nat.add_comm, Nat.sub_add_eq]
   · apply Nat.le_trans
     · apply Nat.succ_le_of_lt
       apply Nat.mod_lt
@@ -2548,10 +2536,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.natCast_emod, Int.natCast_mul]
+    simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]
     by_cases h : x.msb
     <;> norm_cast
-    <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H), -Int.natCast_pow]
+    <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H)]
     omega
 
 /--
@@ -3326,7 +3314,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, -Int.natCast_pow]
+  simp [toInt_eq_toNat_bmod]
 
 theorem ofInt_add {n} (x y : Int) : BitVec.ofInt n (x + y) =
     BitVec.ofInt n x + BitVec.ofInt n y := by
@@ -3356,7 +3344,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), -Int.natCast_pow]
+  simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
 
 theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
     (x.toInt - y.toInt < - 2 ^ (w - 1))
@@ -3368,7 +3356,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.add_bmod_right, Int.bmod_eq_of_le]
+      rw_mod_cast [← Int.bmod_add_cancel, Int.bmod_eq_self_of_le]
       <;> omega
     · have := Int.bmod_neg_iff (x := x.toInt - y.toInt) (m := 2 ^ (w + 1))
       push_cast at this
@@ -3385,7 +3373,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.sub_bmod_right, Int.bmod_eq_of_le (by omega) (by omega)]
+      rw_mod_cast [← Int.bmod_sub_cancel, Int.bmod_eq_self_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
@@ -3719,7 +3707,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, -Int.natCast_pow]
+  simp [toInt_eq_toNat_bmod]
 
 theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
     BitVec.ofInt n x * BitVec.ofInt n y := by
@@ -3871,7 +3859,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.natCast_emod, Int.ofNat_one, Int.natCast_pow,
+    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.ofNat_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
@@ -3993,6 +3981,7 @@ 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 -/
 
@@ -4150,110 +4139,6 @@ 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 =
@@ -5029,6 +4914,7 @@ 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]
 
 /--
@@ -5056,7 +4942,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.natCast_emod]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_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]
@@ -5251,22 +5137,6 @@ 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
@@ -5282,7 +5152,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_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega)
+      Int.bmod_eq_self_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega)
                               (by rw [← Nat.mul_two]; push_cast; omega)]
     omega
 
@@ -5299,14 +5169,14 @@ 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_of_le_mul_two (by rw [← Nat.mul_two]; push_cast; omega)
+      Int.bmod_eq_self_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, -Int.natCast_pow] <;> omega
+  by_cases h : x.msb <;> simp [h, toInt_eq_msb_cond] <;> omega
 
 theorem msb_eq_toNat {x : BitVec w}:
     x.msb = decide (x.toNat ≥ 2 ^ (w - 1)) := by

src/Init/Data/Bool.lean

@@ -3,8 +3,6 @@ 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
 
@@ -692,5 +690,9 @@ def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
 
 /-! ### subtypes -/
 
-@[simp] theorem Subtype.beq_iff {α : Type u} [BEq α] {p : α → Prop} {x y : {a : α // p a}} :
-    (x == y) = (x.1 == y.1) := rfl
+@[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]

src/Init/Data/ByteArray.lean

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

@@ -0,0 +1,149 @@
+/-
+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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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,8 +3,6 @@ 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
@@ -412,14 +410,6 @@ 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' :=

src/Init/Data/Fin/Log2.lean

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

src/Init/Data/Float32.lean

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

src/Init/Data/FloatArray.lean

@@ -3,7 +3,5 @@ Copyright (c) 2020 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.FloatArray.Basic

src/Init/Data/FloatArray/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 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.Float

src/Init/Data/Format.lean

@@ -3,8 +3,6 @@ Copyright (c) 2018 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.Format.Basic
 import Init.Data.Format.Macro

src/Init/Data/Format/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2018 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.Control.State
 import Init.Data.Int.Basic

src/Init/Data/Format/Instances.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 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.Format.Basic
 import Init.Data.Array.Basic

src/Init/Data/Format/Macro.lean

@@ -3,8 +3,6 @@ Copyright (c) 2020 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.Format.Basic
 import Init.Data.ToString.Macro

src/Init/Data/Format/Syntax.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 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.Format.Macro
 import Init.Data.Format.Instances