chore: fix tests

.github/workflows/build-template.yml

@@ -82,7 +82,7 @@ jobs:
       - name: CI Merge Checkout
         run: |
           git fetch --depth=1 origin ${{ github.sha }}
-          git checkout FETCH_HEAD flake.nix flake.lock script/prepare-*
+          git checkout FETCH_HEAD flake.nix flake.lock
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
       - name: Setup emsdk
@@ -99,6 +99,7 @@ jobs:
         if: matrix.cmultilib
       - name: Cache
         id: restore-cache
+        if: matrix.name != 'Linux Lake'
         uses: actions/cache/restore@v4
         with:
           # NOTE: must be in sync with `save` below

.github/workflows/ci.yml

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

.github/workflows/nix-ci.yml

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

CMakeLists.txt

@@ -12,8 +12,6 @@ foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
   if("${var}" MATCHES "STAGE0_(.*)")
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif("${var}" MATCHES "STAGE1_(.*)")
-    list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
     if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
@@ -79,29 +77,26 @@ if (USE_MIMALLOC)
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-if (NOT STAGE1_PREV_STAGE)
-  ExternalProject_add(stage0
-    SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
-    SOURCE_SUBDIR src
-    BINARY_DIR stage0
-    # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-    # (however, CI will override this as we need to embed the githash into the stage 1 library built
-    # by stage 0)
-    CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
-    BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
-    INSTALL_COMMAND ""  # skip install
-    DEPENDS ${EXTRA_DEPENDS}
-  )
-  list(APPEND EXTRA_DEPENDS stage0)
-endif()
+ExternalProject_add(stage0
+  SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
+  SOURCE_SUBDIR src
+  BINARY_DIR stage0
+  # do not rebuild stage0 when git hash changes; it's not from this commit anyway
+  # (however, CI will override this as we need to embed the githash into the stage 1 library built
+  # by stage 0)
+  CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
+  BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
+  INSTALL_COMMAND ""  # skip install
+  DEPENDS ${EXTRA_DEPENDS}
+)
 ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
-  DEPENDS ${EXTRA_DEPENDS}
+  DEPENDS stage0
   STEP_TARGETS configure
 )
 ExternalProject_add(stage2

CMakePresets.json

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

nix/buildLeanPackage.nix

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

script/benchReelabRss.lean

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

script/prepare-llvm-linux.sh

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

src/CMakeLists.txt

@@ -191,11 +191,10 @@ set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
 # Initialize CXXFLAGS.
 set(CMAKE_CXX_FLAGS                "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
-set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG")
+set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG -DLEAN_TRACE")
 set(CMAKE_CXX_FLAGS_MINSIZEREL     "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELEASE        "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-DNDEBUG")
-set(CMAKE_CXX_FLAGS_RELWITHASSERT  "-DLEAN_DEBUG")
 
 # SPLIT_STACK
 if (SPLIT_STACK)
@@ -222,7 +221,6 @@ elseif (MSVC)
     set(CMAKE_CXX_FLAGS_DEBUG          "/Od /Zi ${CMAKE_CXX_FLAGS_DEBUG}")
     set(CMAKE_CXX_FLAGS_MINSIZEREL     "/Os /Zc:inline ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     set(CMAKE_CXX_FLAGS_RELEASE        "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELEASE}")
-    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "/O2 /Oi /Oy /Zc:inline ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/O2 /Oi /Zi ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
     set(LEAN_EXTRA_LINKER_FLAGS        "/LTCG:INCREMENTAL ${LEAN_EXTRA_LINKER_FLAGS}")
     set(CMAKE_STATIC_LINKER_FLAGS      "${CMAKE_STATIC_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
@@ -242,13 +240,11 @@ if (NOT MSVC)
       set(CMAKE_CXX_FLAGS_MINSIZEREL     "-Os ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     endif ()
     set(CMAKE_CXX_FLAGS_RELEASE        "-O3 ${CMAKE_CXX_FLAGS_RELEASE}")
-    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "-O3 ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g3 -fno-omit-frame-pointer ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 elseif (MULTI_THREAD)
     set(CMAKE_CXX_FLAGS_DEBUG          "/MTd ${CMAKE_CXX_FLAGS_DEBUG}")
     set(CMAKE_CXX_FLAGS_MINSIZEREL     "/MT ${CMAKE_CXX_FLAGS_MINSIZEREL}")
     set(CMAKE_CXX_FLAGS_RELEASE        "/MT ${CMAKE_CXX_FLAGS_RELEASE}")
-    set(CMAKE_CXX_FLAGS_RELWITHASSERT  "/MT ${CMAKE_CXX_FLAGS_RELWITHASSERT}")
     set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "/MT ${CMAKE_CXX_FLAGS_RELWITHDEBINFO}")
 endif ()
 
@@ -369,8 +365,8 @@ if(LLVM)
   execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY OUTPUT_VARIABLE LLVM_CONFIG_VERSION ECHO_OUTPUT_VARIABLE OUTPUT_STRIP_TRAILING_WHITESPACE)
   string(REGEX MATCH "^[0-9]*" LLVM_CONFIG_MAJOR_VERSION ${LLVM_CONFIG_VERSION})
   message(STATUS "Found 'llvm-config' at '${LLVM_CONFIG}' with version '${LLVM_CONFIG_VERSION}', major version '${LLVM_CONFIG_MAJOR_VERSION}'")
-  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "19")
-    message(FATAL_ERROR "Unable to find llvm-config version 19. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
+  if (NOT LLVM_CONFIG_MAJOR_VERSION STREQUAL "15")
+    message(FATAL_ERROR "Unable to find llvm-config version 15. Found invalid version '${LLVM_CONFIG_MAJOR_VERSION}'")
   endif()
   # -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM
   string(APPEND CMAKE_CXX_FLAGS " -D LEAN_LLVM")
@@ -847,4 +843,6 @@ endif()
 
 if(USE_LAKE AND STAGE EQUAL 1)
   configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/lakefile.toml)
+  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../tests/lakefile.toml)
+  configure_file(${LEAN_SOURCE_DIR}/lakefile.toml.in ${LEAN_SOURCE_DIR}/../lakefile.toml)
 endif()

src/Init.lean

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

src/Init/BinderNameHint.lean

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

src/Init/BinderPredicates.lean

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

src/Init/ByCases.lean

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

src/Init/Classical.lean

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

src/Init/Coe.lean

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

src/Init/Control.lean

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

src/Init/Control/Basic.lean

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

src/Init/Control/EState.lean

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

src/Init/Control/Except.lean

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

src/Init/Control/ExceptCps.lean

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

src/Init/Control/Id.lean

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

src/Init/Control/Lawful.lean

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

src/Init/Control/Lawful/Basic.lean

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

src/Init/Control/Lawful/Instances.lean

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

src/Init/Control/Lawful/Lemmas.lean

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

src/Init/Control/Option.lean

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

src/Init/Control/Reader.lean

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

src/Init/Control/State.lean

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

src/Init/Control/StateCps.lean

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

src/Init/Control/StateRef.lean

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

src/Init/Conv.lean

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

src/Init/Core.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura
 
 notation, basic datatypes and type classes
 -/
-module
-
 prelude
 import Init.Prelude
 import Init.SizeOf
@@ -938,34 +936,6 @@ term.
 theorem eqRec_heq {α : Sort u} {φ : α → Sort v} {a a' : α} : (h : a = a') → (p : φ a) → HEq (Eq.recOn (motive := fun x _ => φ x) h p) p
   | rfl, p => HEq.refl p
 
-/--
-Heterogenous equality with an `Eq.rec` application on the left is equivalent to a heterogenous
-equality on the original term.
--/
-theorem eqRec_heq_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
-    {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h} :
-    HEq (@Eq.rec α a motive refl b h) c ↔ HEq refl c :=
-  h.rec (fun _ => ⟨id, id⟩) c
-
-/--
-Heterogenous equality with an `Eq.rec` application on the right is equivalent to a heterogenous
-equality on the original term.
--/
-theorem heq_eqRec_iff {α : Sort u} {a : α} {motive : (b : α) → a = b → Sort v}
-    {b : α} {refl : motive a (Eq.refl a)} {h : a = b} {c : motive b h} :
-    HEq c (@Eq.rec α a motive refl b h) ↔ HEq c refl :=
-  h.rec (fun _ => ⟨id, id⟩) c
-
-/--
-Moves an cast using `Eq.rec` from the function to the argument.
-Note: because the motive isn't reliably detected by unification,
-it needs to be provided as an explicit parameter.
--/
-theorem apply_eqRec {α : Sort u} {a : α} (motive : (b : α) → a = b → Sort v)
-    {b : α} {h : a = b} {c : motive a (Eq.refl a) → β} {d : motive b h} :
-    @Eq.rec α a (fun b h => motive b h → β) c b h d = c (h.symm ▸ d) := by
-  cases h; rfl
-
 /--
 If casting a term with `Eq.rec` to another type makes it equal to some other term, then the two
 terms are heterogeneously equal.
@@ -1011,7 +981,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⟩
@@ -1176,12 +1146,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
@@ -1897,7 +1867,9 @@ protected abbrev hrecOn
     (f : (a : α) → motive (Quot.mk r a))
     (c : (a b : α) → (p : r a b) → HEq (f a) (f b))
     : motive q :=
-  Quot.recOn q f fun a b p => eq_of_heq (eqRec_heq_iff.mpr (c a b p))
+  Quot.recOn q f fun a b p => eq_of_heq <|
+    have p₁ : HEq (Eq.ndrec (f a) (sound p)) (f a) := eqRec_heq (sound p) (f a)
+    HEq.trans p₁ (c a b p)
 
 end
 end Quot
@@ -2260,27 +2232,6 @@ theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
   show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
   exact congrArg extfunApp (Quot.sound h)
 
-/--
-Like `Quot.liftOn q f h` but allows `f a` to "know" that `q = Quot.mk r a`.
--/
-protected abbrev Quot.pliftOn {α : Sort u} {r : α → α → Prop}
-    (q : Quot r)
-    (f : (a : α) → q = Quot.mk r a → β)
-    (h : ∀ (a b : α) (h h'), r a b → f a h = f b h') : β :=
-  q.rec (motive := fun q' => q = q' → β) f
-    (fun a b p => funext fun h' =>
-      (apply_eqRec (motive := fun b _ => q = b)).trans
-        (@h a b (h'.trans (sound p).symm) h' p)) rfl
-
-/--
-Like `Quotient.liftOn q f h` but allows `f a` to "know" that `q = Quotient.mk s a`.
--/
-protected abbrev Quotient.pliftOn {α : Sort u} {s : Setoid α}
-    (q : Quotient s)
-    (f : (a : α) → q = Quotient.mk s a → β)
-    (h : ∀ (a b : α) (h h'), a ≈ b → f a h = f b h') : β :=
-  Quot.pliftOn q f h
-
 instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] :
     Subsingleton (∀ a, β a) where
   allEq f g := funext fun a => Subsingleton.elim (f a) (g a)

src/Init/Data.lean

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

src/Init/Data/AC.lean

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

src/Init/Data/Array.lean

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

src/Init/Data/Array/Attach.lean

@@ -3,8 +3,6 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joachim Breitner, Mario Carneiro
 -/
-module
-
 prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas

src/Init/Data/Array/Basic.lean

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

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

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

src/Init/Data/Array/Count.lean

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

src/Init/Data/Array/DecidableEq.lean

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

src/Init/Data/Array/Erase.lean

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

src/Init/Data/Array/Extract.lean

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

src/Init/Data/Array/FinRange.lean

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

src/Init/Data/Array/Find.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.List.Nat.Find
 import Init.Data.Array.Lemmas
@@ -23,13 +21,6 @@ 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
 
@@ -37,7 +28,7 @@ theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f =
   cases xs; simp_all
 
 theorem exists_of_findSome?_eq_some {f : α → Option β} {xs : Array α} (w : xs.findSome? f = some b) :
-    ∃ a, a ∈ xs ∧ f a = some b := by
+    ∃ a, a ∈ xs ∧ f a = b := by
   cases xs; simp_all [List.exists_of_findSome?_eq_some]
 
 @[simp] theorem findSome?_eq_none_iff : findSome? p xs = none ↔ ∀ x ∈ xs, p x = none := by
@@ -138,8 +129,6 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
-@[simp] theorem find?_empty : find? p #[] = none := rfl
-
 @[simp] theorem find?_singleton {a : α} {p : α → Bool} :
     #[a].find? p = if p a then some a else none := by
   simp [singleton_eq_toArray_singleton]
@@ -168,9 +157,6 @@ theorem find?_eq_some_iff_append {xs : Array α} :
     exact ⟨as.toList, ⟨l, by simpa using congrArg Array.toList h'⟩,
       by simpa using h⟩
 
-theorem find?_push {xs : Array α} : (xs.push a).find? p = (xs.find? p).or (if p a then some a else none) := by
-  cases xs; simp
-
 @[simp]
 theorem find?_push_eq_some {xs : Array α} :
     (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
@@ -345,11 +331,6 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 
 /-! ### findIdx -/
 
-@[simp] theorem findIdx_empty : findIdx p #[] = 0 := rfl
-theorem findIdx_singleton {a : α} {p : α → Bool} :
-    #[a].findIdx p = if p a then 0 else 1 := by
-  simp
-
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
   rcases xs with ⟨xs⟩
   exact List.findIdx_of_getElem?_eq_some (by simpa using w)
@@ -430,13 +411,6 @@ theorem findIdx_append {p : α → Bool} {xs ys : Array α} :
   rcases ys with ⟨ys⟩
   simp [List.findIdx_append]
 
-theorem findIdx_push {xs : Array α} {a : α} {p : α → Bool} :
-    (xs.push a).findIdx p = if xs.findIdx p < xs.size then xs.findIdx p else xs.size + if p a then 0 else 1 := by
-  simp only [push_eq_append, findIdx_append]
-  split <;> rename_i h
-  · rfl
-  · simp [findIdx_singleton, Nat.add_comm]
-
 theorem findIdx_le_findIdx {xs : Array α} {p q : α → Bool} (h : ∀ x ∈ xs, p x → q x) : xs.findIdx q ≤ xs.findIdx p := by
   rcases xs with ⟨xs⟩
   simp_all [List.findIdx_le_findIdx]
@@ -465,9 +439,6 @@ theorem false_of_mem_extract_findIdx {xs : Array α} {p : α → Bool} (h : x
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_empty : (#[] : Array α).findIdx? p = none := by simp
-theorem findIdx?_singleton {a : α} {p : α → Bool} :
-    #[a].findIdx? p = if p a then some 0 else none := by
-  simp
 
 @[simp]
 theorem findIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
@@ -535,13 +506,6 @@ theorem of_findIdx?_eq_none {xs : Array α} {p : α → Bool} (w : xs.findIdx? p
   rcases ys with ⟨ys⟩
   simp [List.findIdx?_append]
 
-theorem findIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
-    (xs.push a).findIdx? p = (xs.findIdx? p).or (if p a then some xs.size else none) := by
-  simp only [push_eq_append, findIdx?_append]
-  split <;> rename_i h
-  · simp only [findIdx?_singleton, if_pos h, Option.map_some, Nat.zero_add]
-  · simp only [findIdx?_singleton, if_neg h, Option.map_none]
-
 theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.findIdx? p =
       (xss.findIdx? (·.any p)).map
@@ -599,9 +563,6 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[simp] theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
-theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
-    #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -632,21 +593,6 @@ theorem findFinIdx?_eq_some_iff {xs : Array α} {p : α → Bool} {i : Fin xs.si
   · rintro ⟨h, w⟩
     exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
 
-theorem findFinIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
-    (xs.push a).findFinIdx? p =
-      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or (if p a then some ⟨xs.size, by simp⟩ else none) := by
-  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_push, Option.pmap_or]
-  split <;> rename_i h _ <;> split <;> simp [h]
-
-theorem findFinIdx?_append {xs ys : Array α} {p : α → Bool} :
-    (xs ++ ys).findFinIdx? p =
-      ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
-        ((ys.findFinIdx? p).map (Fin.natAdd xs.size) |>.map (Fin.cast (by simp))) := by
-  simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_append, Option.pmap_or]
-  split <;> rename_i h _
-  · simp [h, Option.pmap_map, Option.map_pmap, Nat.add_comm]
-  · simp [h]
-
 @[simp]
 theorem isSome_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isSome = xs.any p := by

src/Init/Data/Array/GetLit.lean

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

src/Init/Data/Array/InsertIdx.lean

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

src/Init/Data/Array/InsertionSort.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kim Morrison
 -/
-module
-
 prelude
 import Init.Data.Nat.Lemmas
 import Init.Data.List.Range
@@ -887,7 +885,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]? = some v := by simp [getElem?_eq_getElem, h]
+    (xs.set i v)[i]? = v := by simp [getElem?_eq_getElem, h]
 
 @[deprecated getElem?_set_self (since := "2024-12-11")]
 abbrev getElem?_set_eq := @getElem?_set_self
@@ -3578,7 +3576,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⟩) = b := by
+    (filterMap f xs).back (by simpa using ⟨_, by simp, b, h⟩) = some b := by
   rcases xs with ⟨xs⟩
   simp only [List.back_toArray] at h
   simp only [List.size_toArray, List.filterMap_toArray', List.back_toArray]

src/Init/Data/Array/Lex.lean

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

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

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

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

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

src/Init/Data/Array/MapIdx.lean

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

src/Init/Data/Array/Mem.lean

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

src/Init/Data/Array/Monadic.lean

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

src/Init/Data/Array/OfFn.lean

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

src/Init/Data/Array/Perm.lean

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

src/Init/Data/Array/QSort.lean

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

src/Init/Data/Array/Range.lean

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

src/Init/Data/Array/Set.lean

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

src/Init/Data/Array/Subarray.lean

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

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

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

src/Init/Data/Array/TakeDrop.lean

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

src/Init/Data/Array/Zip.lean

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

src/Init/Data/BEq.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Markus Himmel
 -/
-module
-
 prelude
 import Init.Data.Bool
 

src/Init/Data/Basic.lean

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

src/Init/Data/BitVec.lean

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

src/Init/Data/BitVec/Basic.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer, Harun Khan, Abdalrhman M Mohamed, Siddharth Bhat
 -/
-module
-
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
@@ -769,15 +767,6 @@ SMT-Lib name: `bvnego`.
 def negOverflow {w : Nat} (x : BitVec w) : Bool :=
   x.toInt == - 2 ^ (w - 1)
 
-/--
-Checks whether the signed division of `x` by `y` results in overflow.
-For BitVecs `x` and `y` with nonzero width, this only happens if `x = intMin` and `y = allOnes w`.
-
-SMT-LIB name: `bvsdivo`.
--/
-def sdivOverflow {w : Nat} (x y : BitVec w) : Bool :=
-  (2 ^ (w - 1) ≤ x.toInt / y.toInt) || (x.toInt / y.toInt <  - 2 ^ (w - 1))
-
 /- ### reverse -/
 
 /-- Reverses the bits in a bitvector. -/

src/Init/Data/BitVec/BasicAux.lean

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

src/Init/Data/BitVec/Bitblast.lean

@@ -3,8 +3,6 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 -/
-module
-
 prelude
 import Init.Data.BitVec.Folds
 import Init.Data.Nat.Mod
@@ -1358,41 +1356,9 @@ theorem negOverflow_eq {w : Nat} (x : BitVec w) :
   rcases w with _|w
   · simp [toInt_of_zero_length, Int.min_eq_right]
   · suffices - 2 ^ w = (intMin (w + 1)).toInt by simp [beq_eq_decide_eq, ← toInt_inj, this]
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod, Int.neg_inj]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod, Int.neg_inj]
     rw_mod_cast [Nat.mod_eq_of_lt (by simp [Nat.pow_lt_pow_succ])]
 
-/--
-  Prove that signed division `x.toInt / y.toInt` only overflows when `x = intMin w` and `y = allOnes w` (for `0 < w`).
--/
-theorem sdivOverflow_eq {w : Nat} (x y : BitVec w) :
-    (sdivOverflow x y) = (decide (0 < w) && (x = intMin w) && (y = allOnes w)) := by
-  rcases w with _|w
-  · simp [sdivOverflow, of_length_zero]
-  · have yle := le_two_mul_toInt (x := y)
-    have ylt := two_mul_toInt_lt (x := y)
-    -- if y = allOnes (w + 1), thus y.toInt = -1,
-    -- the division overflows iff x = intMin (w + 1), as for negation
-    by_cases hy : y = allOnes (w + 1)
-    · simp [sdivOverflow_eq_negOverflow_of_eq_allOnes, negOverflow_eq, ← hy, beq_eq_decide_eq]
-    · simp only [sdivOverflow, hy, bool_to_prop]
-      have := BitVec.neg_two_pow_le_toInt_ediv (x := x) (y := y)
-      simp only [Nat.add_one_sub_one] at this
-      by_cases hx : 0 ≤ x.toInt
-      · by_cases hy' : 0 ≤ y.toInt
-        · have := BitVec.toInt_ediv_toInt_lt_of_nonneg_of_nonneg
-                (x := x) (y := y) (by omega) (by omega)
-          simp only [Nat.add_one_sub_one] at this; simp; omega
-        · have := BitVec.toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos
-                (x := x) (y := y) (by omega) (by omega)
-          simp; omega
-      · by_cases hy' : 0 ≤ y.toInt
-        · have :=  BitVec.toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg
-                (x := x) (y := y) (by omega) (by omega)
-          simp; omega
-        · have := BitVec.toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one
-                (x := x) (y := y) (by omega) (by rw [← toInt_inj, toInt_allOnes] at hy; omega)
-          simp only [Nat.add_one_sub_one] at this; simp; omega
-
 theorem umulOverflow_eq {w : Nat} (x y : BitVec w) :
     umulOverflow x y =
       (0 < w && BitVec.twoPow (w * 2) w ≤ x.zeroExtend (w * 2) * y.zeroExtend (w * 2)) := by
@@ -1574,7 +1540,7 @@ theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
 
 theorem toInt_eq_neg_toNat_neg_of_msb_true {x : BitVec w} (h : x.msb = true) :
     x.toInt = -((-x).toNat) := by
-  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.natCast_emod]
+  simp only [toInt_eq_msb_cond, h, ↓reduceIte, toNat_neg, Int.ofNat_emod]
   norm_cast
   rw [Nat.mod_eq_of_lt]
   · omega
@@ -1669,7 +1635,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
           (a.sdiv b).toInt = -((-a).toNat / b.toNat) := by
         simp only [sdiv_eq, ha, hb, udiv_eq]
         rw [toInt_eq_neg_toNat_neg_of_nonpos]
-        · rw [neg_neg, toNat_udiv, toNat_neg, Int.natCast_emod, Int.neg_inj]
+        · rw [neg_neg, toNat_udiv, toNat_neg, Int.ofNat_emod, Int.neg_inj]
           norm_cast
         · rw [neg_eq_zero_iff]
           by_cases h' : -a / b = 0#w

src/Init/Data/BitVec/Folds.lean

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

src/Init/Data/BitVec/Lemmas.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth Bhat
 
 -/
-module
-
 prelude
 import Init.Data.Bool
 import Init.Data.BitVec.Basic
@@ -23,9 +21,6 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
-@[simp] theorem mk_zero : BitVec.ofFin (w := w) ⟨0, h⟩ = 0#w := rfl
-@[simp] theorem ofNatLT_zero : BitVec.ofNatLT (w := w) 0 h = 0#w := rfl
-
 @[simp] theorem getLsbD_ofFin (x : Fin (2^n)) (i : Nat) :
     getLsbD (BitVec.ofFin x) i = x.val.testBit i := rfl
 
@@ -141,8 +136,6 @@ theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y :
 @[bitvec_to_nat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat :=
   Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
 
-theorem toNat_inj {x y : BitVec n} : x.toNat = y.toNat ↔ x = y := toNat_eq.symm
-
 @[bitvec_to_nat] theorem toNat_ne {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat := by
   rw [Ne, toNat_eq]
 
@@ -620,10 +613,10 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
   simp only [toInt_eq_toNat_cond]
   split
   next g =>
-    rw [Int.bmod_pos] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_pos] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
   next g =>
-    rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_neg] <;> simp only [←Int.ofNat_emod, toNat_mod_cancel]
     omega
 
 theorem toInt_neg_of_msb_true {x : BitVec w} (h : x.msb = true) : x.toInt < 0 := by
@@ -639,12 +632,12 @@ theorem toInt_nonneg_of_msb_false {x : BitVec w} (h : x.msb = false) : 0 ≤ x.t
 @[simp] theorem toInt_one_of_lt {w : Nat} (h : 1 < w) : (1#w).toInt = 1 := by
   rw [toInt_eq_msb_cond]
   simp only [msb_one, show w ≠ 1 by omega, decide_false, Bool.false_eq_true, ↓reduceIte,
-    toNat_ofNat, Int.natCast_emod]
+    toNat_ofNat, Int.ofNat_emod]
   norm_cast
   apply Nat.mod_eq_of_lt
   apply Nat.one_lt_two_pow (by omega)
 
-/-- Prove equality of bitvectors in terms of integer operations. -/
+/-- Prove equality of bitvectors in terms of nat operations. -/
 theorem eq_of_toInt_eq {x y : BitVec n} : x.toInt = y.toInt → x = y := by
   intro eq
   simp only [toInt_eq_toNat_cond] at eq
@@ -2548,7 +2541,7 @@ where
       simp [getElem_signExtend, Nat.le_sub_one_of_lt hv]
       omega
     have H : 2^w ≤ 2^v := Nat.pow_le_pow_right (by omega) (by omega)
-    simp only [this, toNat_setWidth, Int.natCast_add, Int.natCast_emod, Int.natCast_mul]
+    simp only [this, toNat_setWidth, Int.natCast_add, Int.ofNat_emod, Int.natCast_mul]
     by_cases h : x.msb
     <;> norm_cast
     <;> simp [h, Nat.mod_eq_of_lt (Nat.lt_of_lt_of_le x.isLt H), -Int.natCast_pow]
@@ -3871,7 +3864,7 @@ theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w := by
 theorem lt_one_iff {x : BitVec w} (h : 0 < w) : x < 1#w ↔ x = 0#w := by
   constructor
   · intro h₂
-    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.natCast_emod, Int.ofNat_one, Int.natCast_pow,
+    rw [lt_def, toNat_ofNat, ← Int.ofNat_lt, Int.ofNat_emod, Int.ofNat_one, Int.natCast_pow,
       Int.ofNat_two, @Int.emod_eq_of_lt 1 (2^w) (by omega) (by omega)] at h₂
     simp [toNat_eq, show x.toNat = 0 by omega]
   · simp_all
@@ -4150,110 +4143,6 @@ theorem sdiv_self {x : BitVec w} :
       rcases x.msb with msb | msb <;> simp
     · rcases x.msb with msb | msb <;> simp [h]
 
-/-- Unsigned division never overflows. -/
-theorem toNat_div_toNat_lt {w : Nat} {x y : BitVec w} :
-    x.toNat / y.toNat < 2 ^ w := by
-  have hy : y.toNat = 0 ∨ y.toNat = 1 ∨ 1 < y.toNat := by omega
-  rcases hy with hy|hy|hy
-  · simp [hy]; omega
-  · simp [hy]; omega
-  · rw [Nat.div_lt_iff_lt_mul (k := y.toNat) (x := x.toNat) (y := 2 ^ w) (by omega), show x.toNat = x.toNat * 1 by omega]
-    apply Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega)
-
-/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonneg. -/
-theorem toInt_ediv_toInt_lt_of_nonneg_of_nonneg {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : 0 ≤ y.toInt) :
-    x.toInt / y.toInt < 2 ^ (w - 1) := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
-    by_cases hy' : y.toInt = 1
-    · simp [hy', Int.ediv_one]; omega
-    · by_cases hx' : x.toInt = 0
-      · simp only [hx', Int.zero_ediv, Nat.add_one_sub_one, gt_iff_lt]
-        norm_cast
-        exact Nat.two_pow_pos (w := w)
-      · have := Int.ediv_lt_self_of_pos_of_ne_one (x := x.toInt) (y := y.toInt) (by omega) (by omega)
-        simp; omega
-
-/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is nonneg. -/
-theorem toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : 0 ≤ y.toInt) :
-    x.toInt / y.toInt ≤ 0 := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · by_cases hx' : x.toInt = 0
-    · simp [hx']
-    · by_cases hy' : y.toInt = 0
-      · simp [hy']
-      · have := Int.ediv_neg_of_neg_of_pos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
-        simp; omega
-
-/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonpos. -/
-theorem toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : y.toInt ≤ 0) :
-   x.toInt / y.toInt ≤ 0 := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · by_cases hy' : y.toInt = -1
-    · simp [hy']; omega
-    · have := Int.ediv_nonpos_of_nonneg_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
-      simp; omega
-
-/-- Given the definition of ediv/emod for signed integer division (https://dl.acm.org/doi/pdf/10.1145/128861.128862)
-  we have that for two integers `x` and `y`: `x/y = q ↔ x.ediv y = q ↔ r = x.emod y`
-  and in particular: `-1/y = q ↔ -1.ediv y = q ↔ r = -1.emod y`.
-  from which it follows that:
-  (-1)/0 = 0
-  (-1)/y = -1 when 0 < y
-  (-1)/(-5) = 1 when y < 0
--/
-theorem neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} :
-    (-1) / y.toInt = if y.toInt = 0 then 0 else if 0 < y.toInt then -1 else 1 := by
-  rcases w with _|_|w
-  · simp [of_length_zero]
-  · cases eq_zero_or_eq_one y
-    · case _ h => simp [h]
-    · case _ h => simp [h]
-  · by_cases 0 < y.toInt
-    · simp [Int.sign_eq_one_of_pos (a := y.toInt) (by omega), Int.neg_one_ediv]
-      omega
-    · by_cases hy : y.toInt = 0
-      · simp [hy]
-      · simp [Int.sign_eq_neg_one_of_neg (a := y.toInt) (by omega), Int.neg_one_ediv]
-        omega
-
-/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is less than -1. -/
-theorem toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : y.toInt < -1) :
-    x.toInt / y.toInt < 2 ^ (w - 1) := by
-  rcases w with _|_|w
-  · simp [of_length_zero]
-  · have hy := eq_zero_or_eq_one (a := y)
-    simp [← toInt_inj, toInt_zero, toInt_one] at hy
-    omega
-  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
-    have hx' : x.toInt = 0 ∨ x.toInt = - 1 ∨ x.toInt < - 1 := by omega
-    rcases hx' with hx'|hx'|hx'
-    · simp [hx']; omega
-    · have := BitVec.neg_one_ediv_toInt_eq (y := y)
-      simp only [toInt_allOnes, Nat.lt_add_left_iff_pos, Nat.zero_lt_succ, ↓reduceIte,
-        Int.reduceNeg] at this
-      simp [hx', this]
-      omega
-    · have := Int.ediv_lt_natAbs_self_of_lt_neg_one_of_lt_neg_one (x := x.toInt) (y := y.toInt) (by omega) hy
-      simp; omega
-
-/-- Signed division of (x y : BitVec w) is always -2 ^ w ≤ x.toInt / y.toInt. -/
-theorem neg_two_pow_le_toInt_ediv {x y : BitVec w} :
-    - 2 ^ (w - 1) ≤ x.toInt / y.toInt := by
-  have xlt := @toInt_lt w x; have lex := @le_toInt w x
-  by_cases hx : 0 ≤ x.toInt <;> by_cases hy : 0 ≤ y.toInt
-  · have := Int.ediv_nonneg_of_nonneg_of_nonneg (x := x.toInt) (y := y.toInt) hx hy
-    omega
-  · have := Int.neg_self_le_ediv_of_nonneg_of_nonpos (x := x.toInt) (y := y.toInt) hx (by omega)
-    omega
-  · have := Int.self_le_ediv_of_nonpos_of_nonneg (x := x.toInt) (y := y.toInt) (by omega) hy
-    omega
-  · have := Int.ediv_nonneg_of_nonpos_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
-    omega
-
 /-! ### smtSDiv -/
 
 theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
@@ -5056,7 +4945,7 @@ theorem toInt_intMin_le (x : BitVec w) :
   cases w
   case zero => simp [toInt_intMin, @of_length_zero x]
   case succ w =>
-    simp only [toInt_intMin, Nat.add_one_sub_one, Int.natCast_emod]
+    simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod]
     have : 0 < 2 ^ w := Nat.two_pow_pos w
     rw [Int.emod_eq_of_lt (by omega) (by omega)]
     rw [BitVec.toInt_eq_toNat_bmod]
@@ -5251,22 +5140,6 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
     BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
   omega
 
-theorem sdiv_neg_one {w : Nat} {x : BitVec w} :
-    x.toInt / -1 = -x.toInt := by
-  rcases w with _|w
-  · simp [of_length_zero]
-  · simp [toInt_allOnes]
-
-theorem sdivOverflow_eq_negOverflow_of_eq_allOnes {w : Nat} {x y : BitVec w} (hy : y = allOnes w) :
-    sdivOverflow x y = negOverflow x := by
-  rcases w with _|w
-  · simp [sdivOverflow, negOverflow, of_length_zero]
-  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
-    simp only [sdivOverflow, hy, show ¬2 ^ w < x.toInt by omega, negOverflow]
-    by_cases hx : x.toInt = - 2 ^ w
-    · simp [hx]
-    · simp [show ¬x.toInt == -2 ^ w by simp only [beq_iff_eq, hx, not_false_eq_true]]; omega
-
 theorem two_pow_le_toInt_mul_toInt_iff {x y : BitVec w} :
     2 ^ (w - 1) ≤ x.toInt * y.toInt ↔
       (signExtend (w * 2) (intMax w)).slt (signExtend (w * 2) x * signExtend (w * 2) y) := by

src/Init/Data/Bool.lean

@@ -3,8 +3,6 @@ Copyright (c) 2023 F. G. Dorais. No rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
-module
-
 prelude
 import Init.NotationExtra
 

src/Init/Data/ByteArray.lean

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

src/Init/Data/ByteArray/Basic.lean

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

src/Init/Data/Cast.lean

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

src/Init/Data/Char.lean

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

src/Init/Data/Char/Basic.lean

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

src/Init/Data/Char/Lemmas.lean

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

src/Init/Data/Fin.lean

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

src/Init/Data/Fin/Basic.lean

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

src/Init/Data/Fin/Bitwise.lean

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

src/Init/Data/Fin/Fold.lean

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

src/Init/Data/Fin/Iterate.lean

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

src/Init/Data/Fin/Lemmas.lean

@@ -3,8 +3,6 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Leonardo de Moura
 -/
-module
-
 prelude
 import Init.Data.Fin.Basic
 import Init.Data.Nat.Lemmas
@@ -412,14 +410,6 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 @[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
-@[simp] theorem cast_castLE {k m n} (km : k ≤ m) (mn : m = n) (i : Fin k) :
-    Fin.cast mn (i.castLE km) = i.castLE (mn ▸ km) :=
-  Fin.ext (by simp)
-
-@[simp] theorem cast_castLT {k m n} (i : Fin k) (h : (i : Nat) < m) (mn : m = n) :
-    Fin.cast mn (i.castLT h) = i.castLT (mn ▸ h) :=
-  Fin.ext (by simp)
-
 @[simp] theorem cast_zero [NeZero n] [NeZero m] (h : n = m) : Fin.cast h 0 = 0 := rfl
 
 @[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=

src/Init/Data/Fin/Log2.lean

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

src/Init/Data/Float.lean

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

src/Init/Data/Float32.lean

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

src/Init/Data/FloatArray.lean

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

src/Init/Data/FloatArray/Basic.lean

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

src/Init/Data/Format.lean

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

src/Init/Data/Format/Basic.lean

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

src/Init/Data/Format/Instances.lean

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

src/Init/Data/Format/Macro.lean

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

src/Init/Data/Format/Syntax.lean

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

src/Init/Data/Function.lean

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

src/Init/Data/Int.lean

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

src/Init/Data/Int/Basic.lean

@@ -5,8 +5,6 @@ Authors: Jeremy Avigad, Leonardo de Moura
 
 The integers, with addition, multiplication, and subtraction.
 -/
-module
-
 prelude
 import Init.Data.Cast
 import Init.Data.Nat.Div.Basic