chore: fix statements of HashMap.getKey_insert

This PR adds extensional hash maps and hash sets under the names
`Std.ExtDHashMap`, `Std.ExtHashMap` and `Std.ExtHashSet`. Extensional
hash maps work like regular hash maps, except that they have
extensionality lemmas which make them easier to use in proofs. This
however makes it also impossible to regularly iterate over its entries.

.github/workflows/build-template.yml

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

.github/workflows/ci.yml

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

.github/workflows/nix-ci.yml

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

CMakeLists.txt

@@ -12,6 +12,8 @@ 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")
@@ -77,26 +79,29 @@ if (USE_MIMALLOC)
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-ExternalProject_add(stage0
-  SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
-  SOURCE_SUBDIR src
-  BINARY_DIR stage0
-  # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-  # (however, CI will override this as we need to embed the githash into the stage 1 library built
-  # by stage 0)
-  CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
-  BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
-  INSTALL_COMMAND ""  # skip install
-  DEPENDS ${EXTRA_DEPENDS}
-)
+if (NOT STAGE1_PREV_STAGE)
+  ExternalProject_add(stage0
+    SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
+    SOURCE_SUBDIR src
+    BINARY_DIR stage0
+    # do not rebuild stage0 when git hash changes; it's not from this commit anyway
+    # (however, CI will override this as we need to embed the githash into the stage 1 library built
+    # by stage 0)
+    CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
+    BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
+    INSTALL_COMMAND ""  # skip install
+    DEPENDS ${EXTRA_DEPENDS}
+  )
+  list(APPEND EXTRA_DEPENDS stage0)
+endif()
 ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
-  DEPENDS stage0
+  DEPENDS ${EXTRA_DEPENDS}
   STEP_TARGETS configure
 )
 ExternalProject_add(stage2
@@ -108,6 +113,7 @@ ExternalProject_add(stage2
   INSTALL_COMMAND ""
   DEPENDS stage1
   EXCLUDE_FROM_ALL ON
+  STEP_TARGETS configure
 )
 ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"

CMakePresets.json

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

nix/buildLeanPackage.nix

@@ -194,7 +194,7 @@ with builtins; let
   modCandidates = mapAttrs (mod: header:
     let
       deps = if header.errors == []
-             then map (m: m.module) header.imports
+             then map (m: m.module) header.result.imports
              else abort "errors while parsing imports of ${mod}:\n${lib.concatStringsSep "\n" header.errors}";
     in mkMod mod (map (dep: if modDepsMap ? ${dep} then modCandidates.${dep} else externalModMap.${dep}) deps)) modDepsMap;
   expandGlob = g:
@@ -206,7 +206,7 @@ with builtins; let
   # subset of `modCandidates` that is transitively reachable from `roots`
   mods' = listToAttrs (map (e: { name = e.key; value = modCandidates.${e.key}; }) (genericClosure {
     startSet = map (m: { key = m; }) (concatMap expandGlob roots);
-    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.imports) else [];
+    operator = e: if modDepsMap ? ${e.key} then map (m: { key = m.module; }) (filter (m: modCandidates ? ${m.module}) modDepsMap.${e.key}.result.imports) else [];
   }));
   allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
 

script/benchReelabRss.lean

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

script/prepare-llvm-linux.sh

@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-set -uo pipefail
+set -euxo pipefail
 
 # run from root build directory (from inside nix-shell or otherwise defining GLIBC/ZLIB/GMP) as in
 # ```
@@ -14,6 +14,7 @@ set -uo pipefail
 else
   ln -s llvm llvm-host
 fi
+mkdir -p stage0/lib
 mkdir -p stage1/{bin,lib,lib/glibc,include/clang}
 CP="cp -d"  # preserve symlinks
 # a C compiler!
@@ -25,6 +26,8 @@ cp -L llvm/bin/llvm-ar stage1/bin/
 # dependencies of the above
 $CP llvm/lib/lib{clang-cpp,LLVM}*.so* stage1/lib/
 $CP $ZLIB/lib/libz.so* stage1/lib/
+# also copy USE_LLVM deps into stage 0
+$CP llvm/lib/libLLVM*.so* $ZLIB/lib/libz.so* stage0/lib/
 # general clang++ dependency, breaks cross-library C++ exceptions if linked statically
 $CP $GCC_LIB/lib/libgcc_s.so* stage1/lib/
 # bundle libatomic (referenced by LLVM >= 15, and required by the lean executable to run)
@@ -39,18 +42,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 15 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
-# but clang-15 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
+# LLVM 19 appears to ship the dependencies in 'llvm/lib/<target-triple>/' and 'llvm/include/<target-triple>/'
+# but clang-19 that we use to compile is linked against 'llvm/lib/' and 'llvm/include'
 # https://github.com/llvm/llvm-project/issues/54955
 $CP llvm/lib/*/lib{c++,c++abi,unwind}.* llvm/lib/
 $CP llvm-host/lib/*/lib{c++,c++abi,unwind}.* llvm-host/lib/
 # libc++ headers are looked up in the host compiler's root, so copy over target-specific includes
-$CP -r llvm/include/*-*-* llvm-host/include/
+$CP -r llvm/include/*-*-* llvm-host/include/ || true
 # glibc: use for linking (so Lean programs don't embed newer symbol versions), but not for running (because libc.so, librt.so, and ld.so must be compatible)!
 $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc
 # libpthread_nonshared.a must be linked in order to be able to use `pthread_atfork(3)`. LibUV uses this function.
 $CP $GLIBC/lib/libpthread_nonshared.a stage1/lib/glibc
-for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
+for f in $GLIBC/lib/{ld,lib{c,dl,m,rt,pthread}}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done
 OPTIONS=()
 echo -n " -DLEAN_STANDALONE=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
@@ -64,7 +67,8 @@ fi
 # use `-nostdinc` to make sure headers are not visible by default (in particular, not to `#include_next` in the clang headers),
 # but do not change sysroot so users can still link against system libs
 echo -n " -DLEANC_INTERNAL_FLAGS='--sysroot ROOT -nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='--sysroot ROOT -L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a ROOT/lib/glibc/libpthread_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+# ld.so is usually included by the libc.so linker script but we discard those
+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'"
 # 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,10 +191,11 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
 # Initialize CXXFLAGS.
 set(CMAKE_CXX_FLAGS                "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
-set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG -DLEAN_TRACE")
+set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG")
 set(CMAKE_CXX_FLAGS_MINSIZEREL     "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELEASE        "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-DNDEBUG")
+set(CMAKE_CXX_FLAGS_RELWITHASSERT  "-DLEAN_DEBUG")
 
 # SPLIT_STACK
 if (SPLIT_STACK)
@@ -221,6 +222,7 @@ elseif (MSVC)
     set(CMAKE_CXX_FLAGS_DEBUG          "/Od /Zi ${CMAKE_CXX_FLAGS_DEBUG}")
     set(CMAKE_CXX_FLAGS_MINSIZEREL     "/Os /Zc:inline ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     set(CMAKE_CXX_FLAGS_RELEASE        "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELEASE}")
+    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/O2 /Oi /Zi ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
     set(LEAN_EXTRA_LINKER_FLAGS        "/LTCG:INCREMENTAL ${LEAN_EXTRA_LINKER_FLAGS}")
     set(CMAKE_STATIC_LINKER_FLAGS      "${CMAKE_STATIC_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
@@ -240,11 +242,13 @@ if (NOT MSVC)
       set(CMAKE_CXX_FLAGS_MINSIZEREL     "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     endif ()
     set(CMAKE_CXX_FLAGS_RELEASE        "-O3 ${CMAKE_CXX_FLAGS_RELEASE}")
+    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "-O3 ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 -fno-omit-frame-pointer ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 elseif (MULTI_THREAD)
     set(CMAKE_CXX_FLAGS_DEBUG          "/MTd ${CMAKE_CXX_FLAGS_DEBUG}")
     set(CMAKE_CXX_FLAGS_MINSIZEREL     "/MT ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     set(CMAKE_CXX_FLAGS_RELEASE        "/MT ${CMAKE_CXX_FLAGS_RELEASE}")
+    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "/MT ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/MT ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 endif ()
 
@@ -365,8 +369,8 @@ if(LLVM)
   execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY OUTPUT_VARIABLE LLVM_CONFIG_VERSION ECHO_OUTPUT_VARIABLE OUTPUT_STRIP_TRAILING_WHITESPACE)
   string(REGEX MATCH "^[0-9]*" LLVM_CONFIG_MAJOR_VERSION ${LLVM_CONFIG_VERSION})
   message(STATUS "Found 'llvm-config' at '${LLVM_CONFIG}' with version '${LLVM_CONFIG_VERSION}', major version '${LLVM_CONFIG_MAJOR_VERSION}'")
-  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "15")
-    message(FATAL_ERROR "Unable to find llvm-config version 15. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
+  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "19")
+    message(FATAL_ERROR "Unable to find llvm-config version 19. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
   endif()
   # -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM
   string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM")
@@ -780,12 +784,11 @@ add_custom_target(clean-olean
   DEPENDS clean-stdlib)
 
 install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
-  PATTERN temp
-  PATTERN "*.export"
-  PATTERN "*.hash"
-  PATTERN "*.trace"
-  PATTERN "*.rsp"
-  EXCLUDE)
+  PATTERN temp EXCLUDE
+  PATTERN "*.export" EXCLUDE
+  PATTERN "*.hash" EXCLUDE
+  PATTERN "*.trace" EXCLUDE
+  PATTERN "*.rsp" EXCLUDE)
 
 # symlink source into expected installation location for go-to-definition, if file system allows it
 file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
@@ -844,6 +847,4 @@ endif()
 
 if(USE_LAKE AND STAGE EQUAL 1)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
-  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../tests/lakefile.toml)
-  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../lakefile.toml)
 endif()

src/Init.lean

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

src/Init/BinderNameHint.lean

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

src/Init/BinderPredicates.lean

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

src/Init/ByCases.lean

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

src/Init/Classical.lean

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

src/Init/Coe.lean

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

src/Init/Control.lean

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

src/Init/Control/Basic.lean

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

src/Init/Control/EState.lean

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

src/Init/Control/Except.lean

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

src/Init/Control/ExceptCps.lean

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

src/Init/Control/Id.lean

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

src/Init/Control/Lawful.lean

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

src/Init/Control/Lawful/Basic.lean

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

src/Init/Control/Lawful/Instances.lean

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

src/Init/Control/Lawful/Lemmas.lean

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

src/Init/Control/Option.lean

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

src/Init/Control/Reader.lean

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

src/Init/Control/State.lean

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

src/Init/Control/StateCps.lean

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

src/Init/Control/StateRef.lean

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

src/Init/Conv.lean

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

src/Init/Core.lean

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

src/Init/Data.lean

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

src/Init/Data/AC.lean

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

src/Init/Data/Array.lean

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

src/Init/Data/Array/Attach.lean

@@ -3,6 +3,8 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner, Mario Carneiro
 -/
+module
+
 prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
@@ -525,7 +527,7 @@ theorem countP_attachWith {p : α → Prop} {q : α → Bool} {xs : Array α} {H
   simp
 
 @[simp]
-theorem count_attach [DecidableEq α] {xs : Array α} {a : {x // x ∈ xs}} :
+theorem count_attach [BEq α] {xs : Array α} {a : {x // x ∈ xs}} :
     xs.attach.count a = xs.count ↑a := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.count_toArray]
@@ -534,7 +536,7 @@ theorem count_attach [DecidableEq α] {xs : Array α} {a : {x // x ∈ xs}} :
   rw [List.countP_pmap, List.countP_attach (p := (fun x => x == a.1)), List.count]
 
 @[simp]
-theorem count_attachWith [DecidableEq α] {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) {a : {x // p x}} :
+theorem count_attachWith [BEq α] {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) {a : {x // p x}} :
     (xs.attachWith p H).count a = xs.count ↑a := by
   cases xs
   simp

src/Init/Data/Array/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.WFTactics
 import Init.Data.Nat.Basic
@@ -834,7 +836,7 @@ some 10
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
   for a in as do
     match (← f a) with
-    | some b => return b
+    | some b => return some b
     | _      => pure ⟨⟩
   return none
 
@@ -865,7 +867,7 @@ some 1
 def findM? {α : Type} [Monad m] (p : α → m Bool) (as : Array α) : m (Option α) := do
   for a in as do
     if (← p a) then
-      return a
+      return some a
   return none
 
 /--
@@ -1173,7 +1175,7 @@ def find? {α : Type u} (p : α → Bool) (as : Array α) : Option α :=
   Id.run do
     for a in as do
       if p a then
-        return a
+        return some a
     return none
 
 /--

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
+module
+
 prelude
 import Init.Data.List.TakeDrop
 

src/Init/Data/Array/Count.lean

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

src/Init/Data/Array/DecidableEq.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.BEq
@@ -114,8 +116,10 @@ end List
 
 namespace Array
 
-instance [BEq α] [LawfulBEq α] : LawfulBEq (Array α) where
+instance [BEq α] [ReflBEq α] : ReflBEq (Array α) where
   rfl := by simp [BEq.beq, isEqv_self_beq]
+
+instance [BEq α] [LawfulBEq α] : LawfulBEq (Array α) where
   eq_of_beq := by
     rintro ⟨_⟩ ⟨_⟩ h
     simpa using h

src/Init/Data/Array/Erase.lean

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

src/Init/Data/Array/Extract.lean

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

src/Init/Data/Array/FinRange.lean

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

src/Init/Data/Array/Find.lean

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

src/Init/Data/Array/GetLit.lean

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

src/Init/Data/Array/InsertIdx.lean

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

src/Init/Data/Array/InsertionSort.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Nat.Lemmas
 import Init.Data.List.Range
@@ -135,6 +137,9 @@ theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none :=
 theorem getElem?_eq_some_iff {xs : Array α} : xs[i]? = some b ↔ ∃ h : i < xs.size, xs[i] = b := by
   simp [getElem?_def]
 
+theorem getElem_of_getElem? {xs : Array α} : xs[i]? = some a → ∃ h : i < xs.size, xs[i] = a :=
+  getElem?_eq_some_iff.mp
+
 theorem some_eq_getElem?_iff {xs : Array α} : some b = xs[i]? ↔ ∃ h : i < xs.size, xs[i] = b := by
   rw [eq_comm, getElem?_eq_some_iff]
 
@@ -826,9 +831,6 @@ theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α}
 @[deprecated contains_eq_true_of_mem (since := "2024-12-12")]
 abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
 
-instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
-  decidable_of_decidable_of_iff (Iff.intro mem_of_contains_eq_true contains_eq_true_of_mem)
-
 @[simp] theorem elem_eq_contains [BEq α] {a : α} {xs : Array α} :
     elem a xs = xs.contains a := by
   simp [elem]
@@ -839,6 +841,9 @@ theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
 theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     xs.contains a = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
 
+instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
+  decidable_of_decidable_of_iff elem_iff
+
 theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     elem a xs = decide (a ∈ xs) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
@@ -882,7 +887,7 @@ theorem all_push [BEq α] {xs : Array α} {a : α} {p : α → Bool} :
 abbrev getElem_set_eq := @getElem_set_self
 
 @[simp] theorem getElem?_set_self {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} :
-    (xs.set i v)[i]? = v := by simp [getElem?_eq_getElem, h]
+    (xs.set i v)[i]? = some v := by simp [getElem?_eq_getElem, h]
 
 @[deprecated getElem?_set_self (since := "2024-12-11")]
 abbrev getElem?_set_eq := @getElem?_set_self
@@ -1091,33 +1096,23 @@ private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a ==
     apply beq_of_beq_singleton
     simp
   · intro h
-    constructor
-    apply Array.isEqv_self_beq
+    infer_instance
 
 @[simp] theorem lawfulBEq_iff [BEq α] : LawfulBEq (Array α) ↔ LawfulBEq α := by
   constructor
   · intro h
+    have : ReflBEq α := reflBEq_iff.mp inferInstance
     constructor
-    · intro a b h
-      apply singleton_inj.1
-      apply eq_of_beq
-      simpa [instBEq, isEqv, isEqvAux]
-    · intro a
-      apply beq_of_beq_singleton
-      simp
+    intro a b h
+    apply singleton_inj.1
+    apply eq_of_beq
+    simpa [instBEq, isEqv, isEqvAux]
   · intro h
-    constructor
-    · intro xs ys h
-      obtain ⟨hs, hi⟩ := isEqv_iff_rel.mp h
-      ext i h₁ h₂
-      · exact hs
-      · simpa using hi _ h₁
-    · intro xs
-      apply Array.isEqv_self_beq
+    infer_instance
 
 /-! ### isEqv -/
 
-@[simp] theorem isEqv_eq [DecidableEq α] {xs ys : Array α} : xs.isEqv ys (· == ·) = (xs = ys) := by
+@[simp] theorem isEqv_eq [BEq α] [LawfulBEq α] {xs ys : Array α} : xs.isEqv ys (· == ·) = (xs = ys) := by
   cases xs
   cases ys
   simp
@@ -3035,7 +3030,7 @@ theorem foldrM_start_stop {m} [Monad m] {xs : Array α} {f : α → β → m β}
     simp
   | succ i ih =>
     unfold foldrM.fold
-    simp only [beq_iff_eq, Nat.add_right_eq_self, Nat.add_one_ne_zero, ↓reduceIte, Nat.add_eq,
+    simp only [beq_iff_eq, Nat.add_eq_left, Nat.add_one_ne_zero, ↓reduceIte, Nat.add_eq,
       getElem_extract]
     congr
     funext b
@@ -3583,7 +3578,7 @@ theorem back_filter_of_pos {p : α → Bool} {xs : Array α} (w : 0 < xs.size) (
   rw [List.getLast_filter_of_pos _ h]
 
 theorem back_filterMap_of_eq_some {f : α → Option β} {xs : Array α} {w : 0 < xs.size} {b : β} (h : f (xs.back w) = some b) :
-    (filterMap f xs).back (by simpa using ⟨_, by simp, b, h⟩) = some b := by
+    (filterMap f xs).back (by simpa using ⟨_, by simp, b, h⟩) = b := by
   rcases xs with ⟨xs⟩
   simp only [List.back_toArray] at h
   simp only [List.size_toArray, List.filterMap_toArray', List.back_toArray]
@@ -3777,14 +3772,8 @@ variable [LawfulBEq α]
 theorem getElem?_replace {xs : Array α} {i : Nat} :
     (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
   rcases xs with ⟨xs⟩
-  simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, beq_iff_eq,
-    take_eq_extract, List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero,
-    mem_toArray]
-  split <;> rename_i h
-  · rw (occs := [2]) [if_pos]
-    simpa using h
-  · rw [if_neg]
-    simpa using h
+  simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
+    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, mem_toArray]
 
 theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
     (xs.replace a b)[i]? = xs[i]? := by
@@ -4276,11 +4265,9 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
 
 /-! ### contains -/
 
-theorem contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a ↔ a ∈ xs := by
-  rw [mem_def, contains, ← any_toList, List.any_eq_true]; simp [and_comm]
-
-instance [DecidableEq α] (a : α) (xs : Array α) : Decidable (a ∈ xs) :=
-  decidable_of_iff _ contains_def
+@[deprecated contains_iff (since := "2025-04-07")]
+abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a ↔ a ∈ xs :=
+  contains_iff
 
 /-! ### isPrefixOf -/
 

src/Init/Data/Array/Lex.lean

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

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

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

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

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.List.Lex
@@ -150,13 +152,13 @@ instance [DecidableEq α] [LT α] [DecidableLT α]
     Std.Total (· ≤ · : Array α → Array α → Prop) where
   total := Array.le_total
 
-@[simp] theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
+@[simp] theorem lex_eq_true_iff_lt [BEq α] [LawfulBEq α] [LT α] [DecidableLT α]
     {xs ys : Array α} : lex xs ys = true ↔ xs < ys := by
   cases xs
   cases ys
   simp
 
-@[simp] theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
+@[simp] theorem lex_eq_false_iff_ge [BEq α] [LawfulBEq α] [LT α] [DecidableLT α]
     {xs ys : Array α} : lex xs ys = false ↔ ys ≤ xs := by
   cases xs
   cases ys

src/Init/Data/Array/MapIdx.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kim Morrison
 -/
+module
+
 prelude
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
@@ -64,7 +66,7 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz
 
 @[simp] theorem getElem?_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} {i : Nat} :
     (xs.mapFinIdx f)[i]? =
-      xs[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1 := by
+      xs[i]?.pbind fun b h => some <| f i b (getElem?_eq_some_iff.1 h).1 := by
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
@@ -153,7 +155,7 @@ theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {xs : Array
 /-- Variant of `mk_mem_zipIdx_iff_le_and_getElem?_sub` specialized at `k = 0`,
 to avoid the inequality and the subtraction. -/
 theorem mk_mem_zipIdx_iff_getElem? {x : α} {i : Nat} {xs : Array α} :
-    (x, i) ∈ xs.zipIdx ↔ xs[i]? = x := by
+    (x, i) ∈ xs.zipIdx ↔ xs[i]? = some x := by
   rw [mk_mem_zipIdx_iff_le_and_getElem?_sub]
   simp
 

src/Init/Data/Array/Mem.lean

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

src/Init/Data/Array/Monadic.lean

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

src/Init/Data/Array/OfFn.lean

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

src/Init/Data/Array/Perm.lean

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

src/Init/Data/Array/QSort.lean

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

src/Init/Data/Array/Range.lean

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

src/Init/Data/Array/Set.lean

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

src/Init/Data/Array/Subarray.lean

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

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

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

src/Init/Data/Array/TakeDrop.lean

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

src/Init/Data/Array/Zip.lean

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

src/Init/Data/BEq.lean

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

src/Init/Data/Basic.lean

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

src/Init/Data/BitVec.lean

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

src/Init/Data/BitVec/Basic.lean

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

src/Init/Data/BitVec/BasicAux.lean

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

src/Init/Data/BitVec/Bitblast.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 -/
+module
+
 prelude
 import Init.Data.BitVec.Folds
 import Init.Data.Nat.Mod
@@ -566,7 +568,7 @@ theorem ult_eq_msb_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
 theorem slt_eq_not_ult_of_msb_neq {x y : BitVec w} (h : x.msb ≠ y.msb) :
     x.slt y = !x.ult y := by
   simp only [BitVec.slt, toInt_eq_msb_cond, Bool.eq_not_of_ne h, ult_eq_msb_of_msb_neq h]
-  cases y.msb <;> (simp; omega)
+  cases y.msb <;> (simp [-Int.natCast_pow]; omega)
 
 theorem slt_eq_ult {x y : BitVec w} :
     x.slt y = (x.msb != y.msb).xor (x.ult y) := by
@@ -1332,7 +1334,7 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) :
     simp only [← decide_or, msb_eq_toInt, decide_beq_decide, toInt_add, ← decide_not, ← decide_and,
       decide_eq_decide]
     rw_mod_cast [Int.bmod_neg_iff (by omega) (by omega)]
-    simp
+    simp only [Nat.add_one_sub_one, ge_iff_le]
     omega
 
 theorem usubOverflow_eq {w : Nat} (x y : BitVec w) :
@@ -1356,9 +1358,41 @@ theorem negOverflow_eq {w : Nat} (x : BitVec w) :
   rcases w with _|w
   · simp [toInt_of_zero_length, Int.min_eq_right]
   · suffices - 2 ^ w = (intMin (w + 1)).toInt by simp [beq_eq_decide_eq, ← toInt_inj, this]
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod, Int.neg_inj]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod, Int.neg_inj]
     rw_mod_cast [Nat.mod_eq_of_lt (by simp [Nat.pow_lt_pow_succ])]
 
+/--
+  Prove that signed division `x.toInt / y.toInt` only overflows when `x = intMin w` and `y = allOnes w` (for `0 < w`).
+-/
+theorem sdivOverflow_eq {w : Nat} (x y : BitVec w) :
+    (sdivOverflow x y) = (decide (0 < w) && (x = intMin w) && (y = allOnes w)) := by
+  rcases w with _|w
+  · simp [sdivOverflow, of_length_zero]
+  · have yle := le_two_mul_toInt (x := y)
+    have ylt := two_mul_toInt_lt (x := y)
+    -- if y = allOnes (w + 1), thus y.toInt = -1,
+    -- the division overflows iff x = intMin (w + 1), as for negation
+    by_cases hy : y = allOnes (w + 1)
+    · simp [sdivOverflow_eq_negOverflow_of_eq_allOnes, negOverflow_eq, ← hy, beq_eq_decide_eq]
+    · simp only [sdivOverflow, hy, bool_to_prop]
+      have := BitVec.neg_two_pow_le_toInt_ediv (x := x) (y := y)
+      simp only [Nat.add_one_sub_one] at this
+      by_cases hx : 0 ≤ x.toInt
+      · by_cases hy' : 0 ≤ y.toInt
+        · have := BitVec.toInt_ediv_toInt_lt_of_nonneg_of_nonneg
+                (x := x) (y := y) (by omega) (by omega)
+          simp only [Nat.add_one_sub_one] at this; simp; omega
+        · have := BitVec.toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos
+                (x := x) (y := y) (by omega) (by omega)
+          simp; omega
+      · by_cases hy' : 0 ≤ y.toInt
+        · have :=  BitVec.toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg
+                (x := x) (y := y) (by omega) (by omega)
+          simp; omega
+        · have := BitVec.toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one
+                (x := x) (y := y) (by omega) (by rw [← toInt_inj, toInt_allOnes] at hy; omega)
+          simp only [Nat.add_one_sub_one] at this; simp; omega
+
 theorem umulOverflow_eq {w : Nat} (x y : BitVec w) :
     umulOverflow x y =
       (0 < w && BitVec.twoPow (w * 2) w ≤ x.zeroExtend (w * 2) * y.zeroExtend (w * 2)) := by
@@ -1456,7 +1490,6 @@ theorem udiv_intMin_of_msb_false {x : BitVec w} (h : x.msb = false) :
   have wpos : 0 < w := by omega
   have := Nat.two_pow_pos (w-1)
   simp [toNat_eq, wpos]
-  rw [Nat.div_eq_zero_iff_lt (by omega)]
   exact toNat_lt_of_msb_false h
 
 theorem sdiv_intMin {x : BitVec w} :
@@ -1541,7 +1574,7 @@ theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
 
 theorem toInt_eq_neg_toNat_neg_of_msb_true {x : BitVec w} (h : x.msb = true) :
     x.toInt = -((-x).toNat) := by
-  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.ofNat_emod]
+  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.natCast_emod]
   norm_cast
   rw [Nat.mod_eq_of_lt]
   · omega
@@ -1571,7 +1604,8 @@ theorem intMin_udiv_eq_intMin_iff (x : BitVec w) :
   · intro h
     rw [← toInt_inj, toInt_eq_msb_cond] at h
     have : (intMin w / x).msb = false := by simp [msb_udiv, msb_intMin,  wpos, hx]
-    simp [this, wpos, toInt_intMin] at h
+    simp only [this, false_eq_true, ↓reduceIte, toNat_udiv, toNat_intMin, wpos,
+      Nat.two_pow_pred_mod_two_pow, Int.natCast_ediv, toInt_intMin] at h
     omega
   · intro h
     subst h
@@ -1612,11 +1646,11 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
           Nat.two_pow_pred_mod_two_pow, Int.neg_tdiv, Int.neg_neg]
         rw [Int.tdiv_self (by omega)]
       · by_cases ha_nonneg : 0 ≤ a.toInt
-        · simp [Int.tdiv_eq_zero_of_lt ha_nonneg (by norm_cast at *), ha_intMin]
+        · simp [Int.tdiv_eq_zero_of_lt ha_nonneg (by norm_cast at *), ha_intMin, -Int.natCast_pow]
         · simp only [ne_eq, ← toInt_inj, toInt_intMin, wpos, Nat.two_pow_pred_mod_two_pow] at h
           rw [← Int.neg_tdiv, Int.tdiv_eq_zero_of_lt (by omega)]
           · simp [ha_intMin]
-          · simp [wpos, ← toInt_ne, toInt_intMin] at ha_intMin
+          · simp [wpos, ← toInt_ne, toInt_intMin, -Int.natCast_pow] at ha_intMin
             omega
 
   · by_cases ha : a.msb <;> by_cases hb : b.msb
@@ -1635,7 +1669,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
           (a.sdiv b).toInt = -((-a).toNat / b.toNat) := by
         simp only [sdiv_eq, ha, hb, udiv_eq]
         rw [toInt_eq_neg_toNat_neg_of_nonpos]
-        · rw [neg_neg, toNat_udiv, toNat_neg, Int.ofNat_emod, Int.neg_inj]
+        · rw [neg_neg, toNat_udiv, toNat_neg, Int.natCast_emod, Int.neg_inj]
           norm_cast
         · rw [neg_eq_zero_iff]
           by_cases h' : -a / b = 0#w

src/Init/Data/BitVec/Folds.lean

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

src/Init/Data/BitVec/Lemmas.lean

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

src/Init/Data/Bool.lean

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

src/Init/Data/ByteArray.lean

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

src/Init/Data/ByteArray/Basic.lean

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

src/Init/Data/Cast.lean

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

src/Init/Data/Channel.lean

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

src/Init/Data/Char.lean

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

src/Init/Data/Char/Basic.lean

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

src/Init/Data/Char/Lemmas.lean

@@ -3,6 +3,8 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Char.Basic
 import Init.Data.UInt.Lemmas

src/Init/Data/Fin.lean

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

src/Init/Data/Fin/Basic.lean

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

src/Init/Data/Fin/Bitwise.lean

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

src/Init/Data/Fin/Fold.lean

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

src/Init/Data/Fin/Iterate.lean

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

src/Init/Data/Fin/Lemmas.lean

@@ -3,6 +3,8 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Nat.Lemmas
@@ -410,6 +412,14 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 @[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
+@[simp] theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
+    Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) :=
+  Fin.ext (by simp)
+
+@[simp] theorem cast_castLT {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
+    Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) :=
+  Fin.ext (by simp)
+
 @[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
 
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=
@@ -976,6 +986,16 @@ theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b
 
 /-! ### mul -/
 
+theorem ofNat'_mul [NeZero n] (x : Nat) (y : Fin n) :
+    Fin.ofNat' n x * y = Fin.ofNat' n (x * y.val) := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.mul_def]
+
+theorem mul_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
+    x * Fin.ofNat' n y = Fin.ofNat' n (x.val * y) := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.mul_def]
+
 theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 

src/Init/Data/Fin/Log2.lean

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

src/Init/Data/Float.lean

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

src/Init/Data/Float32.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Core
 import Init.Data.Int.Basic

src/Init/Data/FloatArray.lean

@@ -3,5 +3,7 @@ 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,6 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
+module
+
 prelude
 import Init.Data.Array.Basic
 import Init.Data.Float

src/Init/Data/Format.lean

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

src/Init/Data/Format/Basic.lean

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

src/Init/Data/Format/Instances.lean

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

src/Init/Data/Format/Macro.lean

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

src/Init/Data/Format/Syntax.lean

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

src/Init/Data/Function.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 
+module
+
 prelude
 import Init.Core
 

src/Init/Data/Hashable.lean

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

src/Init/Data/Int.lean

@@ -3,9 +3,12 @@ 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.Int.Basic
 import Init.Data.Int.Bitwise
+import Init.Data.Int.Compare
 import Init.Data.Int.DivMod
 import Init.Data.Int.Gcd
 import Init.Data.Int.Lemmas