feat: BitVec simprocs

.github/workflows/check-prelude.yml

@@ -1,26 +0,0 @@
-name: Check for modules that should use `prelude`
-
-on: [pull_request]
-
-jobs:
-  check-prelude:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v4
-        with:
-          # the default is to use a virtual merge commit between the PR and master: just use the PR
-          ref: ${{ github.event.pull_request.head.sha }}
-          sparse-checkout: src/Lean
-      - name: Check Prelude
-        run: |
-          failed_files=""
-          while IFS= read -r -d '' file; do
-            if ! grep -q "^prelude$" "$file"; then
-              failed_files="$failed_files$file\n"
-            fi
-          done < <(find src/Lean -name '*.lean' -print0)
-          if [ -n "$failed_files" ]; then
-            echo -e "The following files should use 'prelude':\n$failed_files"
-            exit 1
-          fi

.github/workflows/ci.yml

@@ -410,8 +410,7 @@ jobs:
         run: |
           cd build
           ulimit -c unlimited # coredumps
-          # clean rebuild in case of Makefile changes
-          make update-stage0 && rm -rf ./stage* && make -j4
+          make update-stage0 && make -j4
         if: matrix.name == 'Linux' && needs.configure.outputs.quick == 'false'
       - name: CCache stats
         run: ccache -s
@@ -422,21 +421,19 @@ jobs:
             progbin="$(file $c | sed "s/.*execfn: '\([^']*\)'.*/\1/")"
             echo bt | $GDB/bin/gdb -q $progbin $c || true
           done
-      # has not been used in a long while, would need to be adapted to new
-      # shared libs
-      #- name: Upload coredumps
-      #  uses: actions/upload-artifact@v3
-      #  if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
-      #  with:
-      #    name: coredumps-${{ matrix.name }}
-      #    path: |
-      #      ./coredumps
-      #      ./build/stage0/bin/lean
-      #      ./build/stage0/lib/lean/libleanshared.so
-      #      ./build/stage1/bin/lean
-      #      ./build/stage1/lib/lean/libleanshared.so
-      #      ./build/stage2/bin/lean
-      #      ./build/stage2/lib/lean/libleanshared.so
+      - name: Upload coredumps
+        uses: actions/upload-artifact@v3
+        if: ${{ failure() && matrix.os == 'ubuntu-latest' }}
+        with:
+          name: coredumps-${{ matrix.name }}
+          path: |
+            ./coredumps
+            ./build/stage0/bin/lean
+            ./build/stage0/lib/lean/libleanshared.so
+            ./build/stage1/bin/lean
+            ./build/stage1/lib/lean/libleanshared.so
+            ./build/stage2/bin/lean
+            ./build/stage2/lib/lean/libleanshared.so
 
   # This job collects results from all the matrix jobs
   # This can be made the “required” job, instead of listing each

.github/workflows/copyright-header.yml

@@ -1,20 +0,0 @@
-name: Check for copyright header
-
-on: [pull_request]
-
-jobs:
-  check-lean-files:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v4
-
-    - name: Verify .lean files start with a copyright header.
-      run: |
-        FILES=$(find . -type d \( -path "./tests" -o -path "./doc" -o -path "./src/lake/examples" -o -path "./src/lake/tests" -o -path "./build" -o -path "./nix" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
-        if [ -n "$FILES" ]; then
-          echo "Found .lean files which do not have a copyright header:"
-          echo "$FILES"
-          exit 1
-        else
-          echo "All copyright headers present."
-        fi

.github/workflows/pr-release.yml

@@ -151,7 +151,7 @@ jobs:
             echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
             git -C lean4.git log -10 origin/master
 
-            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_SHA\`."
+            MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch."
           fi
 
           if [[ -n "$MESSAGE" ]]; then

doc/dev/index.md

@@ -74,9 +74,3 @@ Lean's build process uses [`ccache`](https://ccache.dev/) if it is
 installed to speed up recompilation of the generated C code. Without
 `ccache`, you'll likely spend more time than necessary waiting on
 rebuilds - it's a good idea to make sure it's installed.
-
-### `prelude`
-Unlike most Lean projects, all submodules of the `Lean` module begin with the
-`prelude` keyword. This disables the automated import of `Init`, meaning that
-developers need to figure out their own subset of `Init` to import. This is done
-such that changing files in `Init` doesn't force a full rebuild of `Lean`.

doc/monads/except.lean

@@ -33,7 +33,7 @@ convert the pure non-monadic value `x / y` into the required `Except` object.  S
 
 Now this return typing would get tedious if you had to include it everywhere that you call this
 function, however, Lean type inference can clean this up. For example, you can define a test
-function that calls the `divide` function and you don't need to say anything here about the fact that
+function can calls the `divide` function and you don't need to say anything here about the fact that
 it might throw an error, because that is inferred:
 -/
 def test := divide 5 0

nix/bootstrap.nix

@@ -65,7 +65,12 @@ rec {
     installPhase = ''
       mkdir -p $out/bin $out/lib/lean
       mv bin/lean $out/bin/
-      mv lib/lean/*.so $out/lib/lean
+      mv lib/lean/libleanshared.* $out/lib/lean
+   '' + lib.optionalString stdenv.isDarwin ''
+      for lib in $(otool -L $out/bin/lean | tail -n +2 | cut -d' ' -f1); do
+        if [[ "$lib" == *lean* ]]; then install_name_tool -change "$lib" "$out/lib/lean/$(basename $lib)" $out/bin/lean; fi
+      done
+      otool -L $out/bin/lean
     '';
     meta.mainProgram = "lean";
   });
@@ -115,35 +120,29 @@ rec {
       iTree = symlinkJoin { name = "ileans"; paths = map (l: l.iTree) stdlib; };
       Leanc = build { name = "Leanc"; src = lean-bin-tools-unwrapped.leanc_src; deps = stdlib; roots = [ "Leanc" ]; };
       stdlibLinkFlags = "-L${Init.staticLib} -L${Lean.staticLib} -L${Lake.staticLib} -L${leancpp}/lib/lean";
-      libInit_shared = runCommand "libInit_shared" { buildInputs = [ stdenv.cc ]; libName = "libInit_shared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
-        mkdir $out
-        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
-          -Wl,--whole-archive -lInit ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
-          $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
-          -o $out/$libName
-      '';
       leanshared = runCommand "leanshared" { buildInputs = [ stdenv.cc ]; libName = "libleanshared${stdenv.hostPlatform.extensions.sharedLibrary}"; } ''
         mkdir $out
-        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared -Wl,-Bsymbolic \
-          ${libInit_shared}/* -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lstdc++ -lm ${stdlibLinkFlags} \
+        LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Wl,-Bsymbolic"} \
+          ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++"
+            else "-Wl,--whole-archive -lInit -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \
           $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \
           -o $out/$libName
       '';
       mods = foldl' (mods: pkg: mods // pkg.mods) {} stdlib;
       print-paths = Lean.makePrintPathsFor [] mods;
       leanc = writeShellScriptBin "leanc" ''
-        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${libInit_shared} -L${leanshared} "$@"
+        LEAN_CC=${stdenv.cc}/bin/cc ${Leanc.executable}/bin/leanc -I${lean-bin-tools-unwrapped}/include ${stdlibLinkFlags} -L${leanshared} "$@"
       '';
       lean = runCommand "lean" { buildInputs = lib.optional stdenv.isDarwin darwin.cctools; } ''
         mkdir -p $out/bin
-        ${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${libInit_shared}/* ${leanshared}/* -o $out/bin/lean
+        ${leanc}/bin/leanc ${leancpp}/lib/lean.cpp.o ${leanshared}/* -o $out/bin/lean
       '';
       # derivation following the directory layout of the "basic" setup, mostly useful for running tests
       lean-all = stdenv.mkDerivation {
         name = "lean-${desc}";
         buildCommand = ''
           mkdir -p $out/bin $out/lib/lean
-          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${libInit_shared}/* ${leanshared}/* $out/lib/lean/
+          ln -sf ${leancpp}/lib/lean/* ${lib.concatMapStringsSep " " (l: "${l.modRoot}/* ${l.staticLib}/*") (lib.reverseList stdlib)} ${leanshared}/* $out/lib/lean/
           # put everything in a single final derivation so `IO.appDir` references work
           cp ${lean}/bin/lean ${leanc}/bin/leanc ${Lake-Main.executable}/bin/lake $out/bin
           # NOTE: `lndir` will not override existing `bin/leanc`

nix/buildLeanPackage.nix

@@ -10,7 +10,7 @@ lib.makeOverridable (
   staticLibDeps ? [],
   # Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
   groupStaticLibs ? false,
-  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
+  # Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a 
   # shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
   # These libs are also linked to in packages that depend on this one.
   nativeSharedLibs ? [],
@@ -88,9 +88,9 @@ with builtins; let
   allNativeSharedLibs =
     lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
 
-  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
+  # A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`, 
   # plus every dep module itself: `dep.staticLib`
-  allStaticLibDeps =
+  allStaticLibDeps = 
     lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
 
   pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
@@ -249,7 +249,7 @@ in rec {
     ${if stdenv.isDarwin then "-Wl,-force_load,${staticLib}/lib${libName}.a" else "-Wl,--whole-archive ${staticLib}/lib${libName}.a -Wl,--no-whole-archive"} \
     ${lib.concatStringsSep " " (map (d: "${d.sharedLib}/*") deps)}'';
   executable = lib.makeOverridable ({ withSharedStdlib ? true }: let
-      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.libInit_shared}/* ${lean-final.leanshared}/*";
+      objPaths = map (drv: "${drv}/${drv.oPath}") (attrValues objects) ++ lib.optional withSharedStdlib "${lean-final.leanshared}/*";
     in runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
       mkdir -p $out/bin
       leanc ${staticLibLinkWrapper (lib.concatStringsSep " " (objPaths ++ map (d: "${d}/*.a") allStaticLibDeps))} \

script/apply.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
 import Lean.Runtime
 
 abbrev M := ReaderT IO.FS.Stream IO
@@ -21,7 +16,7 @@ def mkTypedefFn (i : Nat) : M Unit := do
   emit s!"typedef obj* (*fn{i})({args}); // NOLINT\n"
   emit s!"#define FN{i}(f) reinterpret_cast<fn{i}>(lean_closure_fun(f))\n"
 
-def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String :=
+def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String := 
   List.range n |>.map f |>.intersperse sep |> .join
 
 -- make string: "obj* a1, obj* a2, ..., obj* an"

script/prepare-llvm-linux.sh

@@ -25,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/
-# 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)
 $CP $GCC_LIB/lib/libatomic.so* stage1/lib/
 
@@ -62,7 +60,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='-nostdinc -isystem ROOT/include/clang' -DLEANC_CC=ROOT/bin/clang"
-echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld'"
+echo -n " -DLEANC_INTERNAL_LINKER_FLAGS='-L ROOT/lib -L ROOT/lib/glibc ROOT/lib/glibc/libc_nonshared.a -Wl,--as-needed -static-libgcc -Wl,-Bstatic -lgmp -lunwind -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 -Wl,--no-as-needed'"
 # do not set `LEAN_CC` for tests

src/CMakeLists.txt

@@ -299,12 +299,13 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
     cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH)
     string(APPEND LEANSHARED_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}")
   endif()
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
+  string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt")
+  string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt")
 else()
-  string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
+  string(APPEND LEANC_STATIC_LINKER_FLAGS " -Wl,--start-group -lleancpp -lLean -Wl,--end-group -Wl,--start-group -lInit -lleanrt -Wl,--end-group")
 endif()
+string(APPEND LEANC_STATIC_LINKER_FLAGS " -lLake")
 
 set(LEAN_CXX_STDLIB "-lstdc++" CACHE STRING "C++ stdlib linker flags")
 
@@ -312,11 +313,8 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEAN_CXX_STDLIB "-lc++")
 endif()
 
-string(APPEND TOOLCHAIN_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
-string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
-
-# flags for user binaries = flags for toolchain binaries + Lake
-string(APPEND LEANC_STATIC_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} -lLake")
+string(APPEND LEANC_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
+string(APPEND LEANSHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}")
 
 if (LLVM)
   string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}")
@@ -344,9 +342,9 @@ endif()
 
 # get rid of unused parts of C++ stdlib
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-dead_strip")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-dead_strip")
 elseif(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,--gc-sections")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--gc-sections")
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
@@ -356,20 +354,26 @@ endif()
 if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
   if(BSYMBOLIC)
     string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
-    string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
+    string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
   endif()
   string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
   string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
-  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
-  string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
   string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   string(APPEND CMAKE_CXX_FLAGS " -fPIC")
   string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+  # We do not use dynamic linking via leanshared for Emscripten to keep things
+  # simple. (And we are not interested in `Lake` anyway.) To use dynamic
+  # linking, we would probably have to set MAIN_MODULE=2 on `leanshared`,
+  # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js".
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,--whole-archive -lInit -lLean -lleancpp -lleanrt ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1")
+elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
@@ -395,7 +399,7 @@ endif()
 # are already loaded) and probably fail unless we set up LD_LIBRARY_PATH.
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   # import library created by the `leanshared` target
-  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared")
+  string(APPEND LEANC_SHARED_LINKER_FLAGS " -lleanshared")
 elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
   string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup")
 endif()
@@ -502,31 +506,13 @@ string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 else()
-  string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive")
-  if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-    string(APPEND INIT_SHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
-  endif()
-endif()
-
-if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
-  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a")
-else()
-  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
   if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
     string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
   endif()
 endif()
-string(APPEND LEANSHARED_LINKER_FLAGS " -lInit_shared")
-
-if (${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  # We do not use dynamic linking via leanshared for Emscripten to keep things
-  # simple. (And we are not interested in `Lake` anyway.) To use dynamic
-  # linking, we would probably have to set MAIN_MODULE=2 on `leanshared`,
-  # SIDE_MODULE=2 on `lean`, and set CMAKE_SHARED_LIBRARY_SUFFIX to ".js".
-  string(APPEND LEAN_EXE_LINKER_FLAGS " ${TOOLCHAIN_STATIC_LINKER_FLAGS} ${EMSCRIPTEN_SETTINGS} -lnodefs.js -s EXIT_RUNTIME=1 -s MAIN_MODULE=1 -s LINKABLE=1 -s EXPORT_ALL=1")
-endif()
 
 # Build the compiler using the bootstrapped C sources for stage0, and use
 # the LLVM build for stage1 and further.
@@ -534,6 +520,10 @@ if (LLVM AND ${STAGE} GREATER 0)
   set(EXTRA_LEANMAKE_OPTS "LLVM=1")
 endif()
 
+# Escape for `make`. Yes, twice.
+string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
+string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
+configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
 add_custom_target(make_stdlib ALL
   WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
@@ -551,33 +541,13 @@ endif()
 # We declare these as separate custom targets so they use separate `make` invocations, which makes `make` recompute which dependencies
 # (e.g. `libLean.a`) are now newer than the target file
 
-if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  # dummy targets, see `MAIN_MODULE` discussion above
-  add_custom_target(Init_shared ALL
-    DEPENDS make_stdlib leanrt_initial-exec
-    COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
-  )
-  add_custom_target(leanshared ALL
-    DEPENDS Init_shared leancpp
-    COMMAND touch ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}
-  )
-else()
-  add_custom_target(Init_shared ALL
-    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
-    DEPENDS make_stdlib leanrt_initial-exec
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init_shared
-    VERBATIM)
+add_custom_target(leanshared ALL
+  WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
+  DEPENDS make_stdlib leancpp leanrt_initial-exec
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
+  VERBATIM)
 
-  add_custom_target(leanshared ALL
-    WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
-    DEPENDS Init_shared leancpp
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanshared
-    VERBATIM)
-
-  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lInit_shared -lleanshared")
-endif()
-
-if(${STAGE} GREATER 0 AND NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
+if(${STAGE} GREATER 0)
   if(NOT EXISTS ${LEAN_SOURCE_DIR}/lake/Lake.lean)
     message(FATAL_ERROR "src/lake does not exist. Please check out the Lake submodule using `git submodule update --init src/lake`.")
   endif()
@@ -598,7 +568,7 @@ endif()
 
 # use Bash version for building, use Lean version in bin/ for tests & distribution
 configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/leanc.sh" @ONLY)
-if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean AND NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
+if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean)
   configure_file("${LEAN_SOURCE_DIR}/Leanc.lean" "${CMAKE_BINARY_DIR}/leanc/Leanc.lean" @ONLY)
   add_custom_target(leanc ALL
     WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
@@ -649,8 +619,3 @@ if(LEAN_INSTALL_PREFIX)
   set(LEAN_INSTALL_SUFFIX "-${LOWER_SYSTEM_NAME}" CACHE STRING "If LEAN_INSTALL_PREFIX is set, append this value to CMAKE_INSTALL_PREFIX")
   set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
 endif()
-
-# Escape for `make`. Yes, twice.
-string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
-string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
-configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)

src/Init/ByCases.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Copyright (c) 2024 Lean FRO. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/

src/Init/Conv.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Notation for operators defined at Prelude.lean
 -/
 prelude
-import Init.Meta
+import Init.NotationExtra
 
 namespace Lean.Parser.Tactic.Conv
 
@@ -308,7 +308,4 @@ Basic forms:
 -- refer to the syntax category instead of this syntax
 syntax (name := conv) "conv" (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
 
-/-- `norm_cast` tactic in `conv` mode. -/
-syntax (name := normCast) "norm_cast" : conv
-
 end Lean.Parser.Tactic.Conv

src/Init/Data.lean

@@ -32,5 +32,3 @@ import Init.Data.Prod
 import Init.Data.AC
 import Init.Data.Queue
 import Init.Data.Channel
-import Init.Data.Cast
-import Init.Data.Sum

src/Init/Data/Array/Mem.lean

@@ -8,6 +8,16 @@ import Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.Data.List.BasicAux
 
+theorem List.sizeOf_get_lt [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
+  match as, i with
+  | [],    i      => apply Fin.elim0 i
+  | a::as, ⟨0, _⟩ => simp_arith [get]
+  | a::as, ⟨i+1, h⟩ =>
+    simp [get]
+    have h : i < as.length := Nat.lt_of_succ_lt_succ h
+    have ih := sizeOf_get_lt as ⟨i, h⟩
+    exact Nat.lt_of_lt_of_le ih (Nat.le_add_left ..)
+
 namespace Array
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
@@ -19,6 +29,10 @@ structure Mem (a : α) (as : Array α) : Prop where
 instance : Membership α (Array α) where
   mem a as := Mem a as
 
+theorem sizeOf_get_lt [SizeOf α] (as : Array α) (i : Fin as.size) : sizeOf (as.get i) < sizeOf as := by
+  cases as with | _ as =>
+  exact Nat.lt_trans (List.sizeOf_get_lt as i) (by simp_arith)
+
 theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   cases as with | _ as =>
   exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)

src/Init/Data/Array/Subarray.lean

@@ -143,7 +143,6 @@ def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Suba
      else
        { as := as, start := as.size, stop := as.size, h₁ := Nat.le_refl _, h₂ := Nat.le_refl _ }
 
-@[coe]
 def ofSubarray (s : Subarray α) : Array α := Id.run do
   let mut as := mkEmpty (s.stop - s.start)
   for a in s do

src/Init/Data/BitVec.lean

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

src/Init/Data/BitVec/Basic.lean

@@ -1,5 +1,6 @@
 /-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Copyright (c) 2022 by the authors listed in the file AUTHORS and their
+institutional affiliations. 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
 -/
@@ -8,6 +9,8 @@ import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 
+namespace Std
+
 /-!
 We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
 (Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
@@ -20,10 +23,8 @@ of SMT-LIBv2.
 -/
 
 /--
-A bitvector of the specified width.
-
-This is represented as the underlying `Nat` number in both the runtime
-and the kernel, inheriting all the special support for `Nat`.
+A bitvector of the specified width. This is represented as the underlying `Nat` number
+in both the runtime and the kernel, inheriting all the special support for `Nat`.
 -/
 structure BitVec (w : Nat) where
   /-- Construct a `BitVec w` from a number less than `2^w`.
@@ -32,38 +33,20 @@ structure BitVec (w : Nat) where
   /-- Interpret a bitvector as a number less than `2^w`.
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
-
-@[deprecated] abbrev Std.BitVec := _root_.BitVec
-
--- We manually derive the `DecidableEq` instances for `BitVec` because
--- we want to have builtin support for bit-vector literals, and we
--- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.
-def BitVec.decEq (a b : BitVec n) : Decidable (a = b) :=
-  match a, b with
-  | ⟨n⟩, ⟨m⟩ =>
-    if h : n = m then
-      isTrue (h ▸ rfl)
-    else
-      isFalse (fun h' => BitVec.noConfusion h' (fun h' => absurd h' h))
-
-instance : DecidableEq (BitVec n) := BitVec.decEq
+  deriving DecidableEq
 
 namespace BitVec
 
-section Nat
+/-- `cast eq i` embeds `i` into an equal `BitVec` type. -/
+@[inline] def cast (eq : n = m) (i : BitVec n) : BitVec m :=
+  .ofFin (Fin.cast (congrArg _ eq) i.toFin)
 
-/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
-@[match_pattern]
-protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2^n) : BitVec n where
-  toFin := ⟨i, p⟩
-
-/-- The `BitVec` with value `i mod 2^n`. -/
-@[match_pattern]
+/-- The `BitVec` with value `i mod 2^n`. Treated as an operation on bitvectors,
+this is truncation of the high bits when downcasting and zero-extension when upcasting. -/
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
   toFin := Fin.ofNat' i (Nat.two_pow_pos n)
 
-instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
-instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
+instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
 /-- Given a bitvector `a`, return the underlying `Nat`. This is O(1) because `BitVec` is a
 (zero-cost) wrapper around a `Nat`. -/
@@ -72,43 +55,6 @@ protected def toNat (a : BitVec n) : Nat := a.toFin.val
 /-- Return the bound in terms of toNat. -/
 theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
 
-/-- Theorem for normalizing the bit vector literal representation. -/
--- TODO: This needs more usage data to assess which direction the simp should go.
-@[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl
-
--- Note. Mathlib would like this to go the other direction.
-@[simp] theorem natCast_eq_ofNat (w x : Nat) : @Nat.cast (BitVec w) _ x = .ofNat w x := rfl
-
-end Nat
-
-section subsingleton
-
-/-- All empty bitvectors are equal -/
-instance : Subsingleton (BitVec 0) where
-  allEq := by intro ⟨0, _⟩ ⟨0, _⟩; rfl
-
-/-- The empty bitvector -/
-abbrev nil : BitVec 0 := 0
-
-/-- Every bitvector of length 0 is equal to `nil`, i.e., there is only one empty bitvector -/
-theorem eq_nil (x : BitVec 0) : x = nil := Subsingleton.allEq ..
-
-end subsingleton
-
-section zero_allOnes
-
-/-- Return a bitvector `0` of size `n`. This is the bitvector with all zero bits. -/
-protected def zero (n : Nat) : BitVec n := .ofNatLt 0 (Nat.two_pow_pos n)
-instance : Inhabited (BitVec n) where default := .zero n
-
-/-- Bit vector of size `n` where all bits are `1`s -/
-def allOnes (n : Nat) : BitVec n :=
-  .ofNatLt (2^n - 1) (Nat.le_of_eq (Nat.sub_add_cancel (Nat.two_pow_pos n)))
-
-end zero_allOnes
-
-section getXsb
-
 /-- Return the `i`-th least significant bit or `false` if `i ≥ w`. -/
 @[inline] def getLsb (x : BitVec w) (i : Nat) : Bool := x.toNat.testBit i
 
@@ -118,60 +64,43 @@ section getXsb
 /-- Return most-significant bit in bitvector. -/
 @[inline] protected def msb (a : BitVec n) : Bool := getMsb a 0
 
-end getXsb
-
-section Int
-
 /-- Interpret the bitvector as an integer stored in two's complement form. -/
 protected def toInt (a : BitVec n) : Int :=
   if a.msb then Int.ofNat a.toNat - Int.ofNat (2^n) else a.toNat
 
-/-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
-protected def ofInt (n : Nat) (i : Int) : BitVec n :=
-  match i with
-  | Int.ofNat x => .ofNat n x
-  | Int.negSucc x => BitVec.ofNatLt (2^n - x % 2^n - 1) (by omega)
+/-- Return a bitvector `0` of size `n`. This is the bitvector with all zero bits. -/
+protected def zero (n : Nat) : BitVec n := ⟨0, Nat.two_pow_pos n⟩
 
-instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
+instance : Inhabited (BitVec n) where default := .zero n
 
-end Int
-
-section Syntax
+instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
 
 /-- Notation for bit vector literals. `i#n` is a shorthand for `BitVec.ofNat n i`. -/
 scoped syntax:max term:max noWs "#" noWs term:max : term
 macro_rules | `($i#$n) => `(BitVec.ofNat $n $i)
 
+/- Support for `i#n` notation in patterns.  -/
+attribute [match_pattern] BitVec.ofNat
+
 /-- Unexpander for bit vector literals. -/
 @[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
   | `($(_) $n $i) => `($i#$n)
   | _ => throw ()
 
-/-- Notation for bit vector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLt i lt`. -/
-scoped syntax:max term:max noWs "#'" noWs term:max : term
-macro_rules | `($i#'$p) => `(BitVec.ofNatLt $i $p)
-
-/-- Unexpander for bit vector literals without truncation. -/
-@[app_unexpander BitVec.ofNatLt] def unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander
-  | `($(_) $i $p) => `($i#'$p)
-  | _ => throw ()
-
-end Syntax
-
-section repr_toString
-
 /-- Convert bitvector into a fixed-width hex number. -/
 protected def toHex {n : Nat} (x : BitVec n) : String :=
   let s := (Nat.toDigits 16 x.toNat).asString
   let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
   t ++ s
 
-instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Format) ++ "#" ++ repr n
+
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
-end repr_toString
-
-section arithmetic
+/-- Theorem for normalizing the bit vector literal representation. -/
+-- TODO: This needs more usage data to assess which direction the simp should go.
+@[simp] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = BitVec.ofNat n i := rfl
+@[simp] theorem natCast_eq_ofNat : Nat.cast x = x#w := rfl
 
 /--
 Addition for bit vectors. This can be interpreted as either signed or unsigned addition
@@ -179,14 +108,14 @@ modulo `2^n`.
 
 SMT-Lib name: `bvadd`.
 -/
-protected def add (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + y.toNat)
+protected def add (x y : BitVec n) : BitVec n where toFin := x.toFin + y.toFin
 instance : Add (BitVec n) := ⟨BitVec.add⟩
 
 /--
 Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
 modulo `2^n`.
 -/
-protected def sub (x y : BitVec n) : BitVec n := .ofNat n (x.toNat + (2^n - y.toNat))
+protected def sub (x y : BitVec n) : BitVec n where toFin := x.toFin - y.toFin
 instance : Sub (BitVec n) := ⟨BitVec.sub⟩
 
 /--
@@ -195,9 +124,12 @@ modulo `2^n`.
 
 SMT-Lib name: `bvneg`.
 -/
-protected def neg (x : BitVec n) : BitVec n := .ofNat n (2^n - x.toNat)
+protected def neg (x : BitVec n) : BitVec n := .sub 0 x
 instance : Neg (BitVec n) := ⟨.neg⟩
 
+/-- Bit vector of size `n` where all bits are `1`s -/
+def allOnes (n : Nat) : BitVec n := -1
+
 /--
 Return the absolute value of a signed bitvector.
 -/
@@ -209,14 +141,13 @@ modulo `2^n`.
 
 SMT-Lib name: `bvmul`.
 -/
-protected def mul (x y : BitVec n) : BitVec n := BitVec.ofNat n (x.toNat * y.toNat)
+protected def mul (x y : BitVec n) : BitVec n := ofFin <| x.toFin * y.toFin
 instance : Mul (BitVec n) := ⟨.mul⟩
 
 /--
 Unsigned division for bit vectors using the Lean convention where division by zero returns zero.
 -/
-def udiv (x y : BitVec n) : BitVec n :=
-  (x.toNat / y.toNat)#'(Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
+def udiv (x y : BitVec n) : BitVec n := ofFin <| x.toFin / y.toFin
 instance : Div (BitVec n) := ⟨.udiv⟩
 
 /--
@@ -224,8 +155,7 @@ Unsigned modulo for bit vectors.
 
 SMT-Lib name: `bvurem`.
 -/
-def umod (x y : BitVec n) : BitVec n :=
-  (x.toNat % y.toNat)#'(Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
+def umod (x y : BitVec n) : BitVec n := ofFin <| x.toFin % y.toFin
 instance : Mod (BitVec n) := ⟨.umod⟩
 
 /--
@@ -235,7 +165,7 @@ where division by zero returns the `allOnes` bitvector.
 
 SMT-Lib name: `bvudiv`.
 -/
-def smtUDiv (x y : BitVec n) : BitVec n := if y = 0 then allOnes n else udiv x y
+def smtUDiv (x y : BitVec n) : BitVec n := if y = 0 then -1 else .udiv x y
 
 /--
 Signed t-division for bit vectors using the Lean convention where division
@@ -288,54 +218,35 @@ SMT_Lib name: `bvsmod`.
 -/
 def smod (s t : BitVec m) : BitVec m :=
   match s.msb, t.msb with
-  | false, false => umod s t
+  | false, false => .umod s t
   | false, true =>
-    let u := umod s (.neg t)
-    (if u = .zero m then u else .add u t)
+    let u := .umod s (.neg t)
+    (if u = BitVec.ofNat m 0 then u else .add u t)
   | true, false =>
-    let u := umod (.neg s) t
-    (if u = .zero m then u else .sub t u)
-  | true, true => .neg (umod (.neg s) (.neg t))
-
-end arithmetic
-
-
-section bool
-
-/-- Turn a `Bool` into a bitvector of length `1` -/
-def ofBool (b : Bool) : BitVec 1 := cond b 1 0
-
-@[simp] theorem ofBool_false : ofBool false = 0 := by trivial
-@[simp] theorem ofBool_true  : ofBool true  = 1 := by trivial
-
-/-- Fills a bitvector with `w` copies of the bit `b`. -/
-def fill (w : Nat) (b : Bool) : BitVec w := bif b then -1 else 0
-
-end bool
-
-section relations
+    let u := .umod (.neg s) t
+    (if u = BitVec.ofNat m 0 then u else .sub t u)
+  | true, true => .neg (.umod (.neg s) (.neg t))
 
 /--
 Unsigned less-than for bit vectors.
 
 SMT-Lib name: `bvult`.
 -/
-protected def ult (x y : BitVec n) : Bool := x.toNat < y.toNat
-
-instance : LT (BitVec n) where lt := (·.toNat < ·.toNat)
+protected def ult (x y : BitVec n) : Bool := x.toFin < y.toFin
+instance : LT (BitVec n) where lt x y := x.toFin < y.toFin
 instance (x y : BitVec n) : Decidable (x < y) :=
-  inferInstanceAs (Decidable (x.toNat < y.toNat))
+  inferInstanceAs (Decidable (x.toFin < y.toFin))
 
 /--
 Unsigned less-than-or-equal-to for bit vectors.
 
 SMT-Lib name: `bvule`.
 -/
-protected def ule (x y : BitVec n) : Bool := x.toNat ≤ y.toNat
+protected def ule (x y : BitVec n) : Bool := x.toFin ≤ y.toFin
 
-instance : LE (BitVec n) where le := (·.toNat ≤ ·.toNat)
+instance : LE (BitVec n) where le x y := x.toFin ≤ y.toFin
 instance (x y : BitVec n) : Decidable (x ≤ y) :=
-  inferInstanceAs (Decidable (x.toNat ≤ y.toNat))
+  inferInstanceAs (Decidable (x.toFin ≤ y.toFin))
 
 /--
 Signed less-than for bit vectors.
@@ -355,87 +266,6 @@ SMT-Lib name: `bvsle`.
 -/
 protected def sle (x y : BitVec n) : Bool := x.toInt ≤ y.toInt
 
-end relations
-
-section cast
-
-/-- `cast eq i` embeds `i` into an equal `BitVec` type. -/
-@[inline] def cast (eq : n = m) (i : BitVec n) : BitVec m := .ofNatLt i.toNat (eq ▸ i.isLt)
-
-@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
-    cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by
-  subst h; rfl
-
-@[simp] theorem cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
-    cast h₂ (cast h₁ x) = cast (h₁ ▸ h₂) x :=
-  rfl
-
-@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) : cast h x = x := rfl
-
-/--
-Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to yield a
-new bitvector of size `len`. If `start + len > n`, then the vector will be zero-padded in the
-high bits.
--/
-def extractLsb' (start len : Nat) (a : BitVec n) : BitVec len := .ofNat _ (a.toNat >>> start)
-
-/--
-Extraction of bits `hi` (inclusive) down to `lo` (inclusive) from a bit vector of size `n` to
-yield a new bitvector of size `hi - lo + 1`.
-
-SMT-Lib name: `extract`.
--/
-def extractLsb (hi lo : Nat) (a : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ a
-
-/--
-A version of `zeroExtend` that requires a proof, but is a noop.
--/
-def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n)  : BitVec w :=
-  x.toNat#'(by
-    apply Nat.lt_of_lt_of_le x.isLt
-    exact Nat.pow_le_pow_of_le_right (by trivial) le)
-
-/--
-`shiftLeftZeroExtend x n` returns `zeroExtend (w+n) x <<< n` without
-needing to compute `x % 2^(2+n)`.
--/
-def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w+m) :=
-  let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w+m) := by
-        simp [Nat.shiftLeft_eq, Nat.pow_add]
-        apply Nat.mul_lt_mul_of_pos_right p
-        exact (Nat.two_pow_pos m)
-  (msbs.toNat <<< m)#'(shiftLeftLt msbs.isLt m)
-
-/--
-Zero extend vector `x` of length `w` by adding zeros in the high bits until it has length `v`.
-If `v < w` then it truncates the high bits instead.
-
-SMT-Lib name: `zero_extend`.
--/
-def zeroExtend (v : Nat) (x : BitVec w) : BitVec v :=
-  if h : w ≤ v then
-    zeroExtend' h x
-  else
-    .ofNat v x.toNat
-
-/--
-Truncate the high bits of bitvector `x` of length `w`, resulting in a vector of length `v`.
-If `v > w` then it zero-extends the vector instead.
--/
-abbrev truncate := @zeroExtend
-
-/--
-Sign extend a vector of length `w`, extending with `i` additional copies of the most significant
-bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
-
-SMT-Lib name: `sign_extend`.
--/
-def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
-
-end cast
-
-section bitwise
-
 /--
 Bitwise AND for bit vectors.
 
@@ -445,8 +275,8 @@ Bitwise AND for bit vectors.
 
 SMT-Lib name: `bvand`.
 -/
-protected def and (x y : BitVec n) : BitVec n :=
-  (x.toNat &&& y.toNat)#'(Nat.and_lt_two_pow x.toNat y.isLt)
+protected def and (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat &&& y.toNat, Nat.and_lt_two_pow x.toNat y.isLt⟩
 instance : AndOp (BitVec w) := ⟨.and⟩
 
 /--
@@ -458,8 +288,8 @@ Bitwise OR for bit vectors.
 
 SMT-Lib name: `bvor`.
 -/
-protected def or (x y : BitVec n) : BitVec n :=
-  (x.toNat ||| y.toNat)#'(Nat.or_lt_two_pow x.isLt y.isLt)
+protected def or (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat ||| y.toNat, Nat.or_lt_two_pow x.isLt y.isLt⟩
 instance : OrOp (BitVec w) := ⟨.or⟩
 
 /--
@@ -471,8 +301,8 @@ instance : OrOp (BitVec w) := ⟨.or⟩
 
 SMT-Lib name: `bvxor`.
 -/
-protected def xor (x y : BitVec n) : BitVec n :=
-  (x.toNat ^^^ y.toNat)#'(Nat.xor_lt_two_pow x.isLt y.isLt)
+protected def xor (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat ^^^ y.toNat, Nat.xor_lt_two_pow x.isLt y.isLt⟩
 instance : Xor (BitVec w) := ⟨.xor⟩
 
 /--
@@ -483,16 +313,25 @@ Bitwise NOT for bit vectors.
 ```
 SMT-Lib name: `bvnot`.
 -/
-protected def not (x : BitVec n) : BitVec n := allOnes n ^^^ x
+protected def not (x : BitVec n) : BitVec n :=
+  allOnes n ^^^ x
 instance : Complement (BitVec w) := ⟨.not⟩
 
+/-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
+protected def ofInt (n : Nat) (i : Int) : BitVec n :=
+  match i with
+  | Int.ofNat a => .ofNat n a
+  | Int.negSucc a => ~~~.ofNat n a
+
+instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
+
 /--
 Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is
 equivalent to `a * 2^s`, modulo `2^n`.
 
 SMT-Lib name: `bvshl` except this operator uses a `Nat` shift value.
 -/
-protected def shiftLeft (a : BitVec n) (s : Nat) : BitVec n := (a.toNat <<< s)#n
+protected def shiftLeft (a : BitVec n) (s : Nat) : BitVec n := .ofNat n (a.toNat <<< s)
 instance : HShiftLeft (BitVec w) Nat (BitVec w) := ⟨.shiftLeft⟩
 
 /--
@@ -502,11 +341,11 @@ As a numeric operation, this is equivalent to `a / 2^s`, rounding down.
 SMT-Lib name: `bvlshr` except this operator uses a `Nat` shift value.
 -/
 def ushiftRight (a : BitVec n) (s : Nat) : BitVec n :=
-  (a.toNat >>> s)#'(by
+  ⟨a.toNat >>> s, by
   let ⟨a, lt⟩ := a
   simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.two_pow_pos s)]
   rw [←Nat.mul_one a]
-  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1))
+  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1)⟩
 
 instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩
 
@@ -544,6 +383,25 @@ SMT-Lib name: `rotate_right` except this operator uses a `Nat` shift amount.
 -/
 def rotateRight (x : BitVec w) (n : Nat) : BitVec w := x >>> n ||| x <<< (w - n)
 
+/--
+A version of `zeroExtend` that requires a proof, but is a noop.
+-/
+def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n)  : BitVec w :=
+  ⟨x.toNat, by
+    apply Nat.lt_of_lt_of_le x.isLt
+    exact Nat.pow_le_pow_of_le_right (by trivial) le⟩
+
+/--
+`shiftLeftZeroExtend x n` returns `zeroExtend (w+n) x <<< n` without
+needing to compute `x % 2^(2+n)`.
+-/
+def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w+m) :=
+  let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w+m) := by
+        simp [Nat.shiftLeft_eq, Nat.pow_add]
+        apply Nat.mul_lt_mul_of_pos_right p
+        exact (Nat.two_pow_pos m)
+  ⟨msbs.toNat <<< m, shiftLeftLt msbs.isLt m⟩
+
 /--
 Concatenation of bitvectors. This uses the "big endian" convention that the more significant
 input is on the left, so `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
@@ -555,6 +413,21 @@ def append (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n+m) :=
 
 instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := ⟨.append⟩
 
+/--
+Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to yield a
+new bitvector of size `len`. If `start + len > n`, then the vector will be zero-padded in the
+high bits.
+-/
+def extractLsb' (start len : Nat) (a : BitVec n) : BitVec len := .ofNat _ (a.toNat >>> start)
+
+/--
+Extraction of bits `hi` (inclusive) down to `lo` (inclusive) from a bit vector of size `n` to
+yield a new bitvector of size `hi - lo + 1`.
+
+SMT-Lib name: `extract`.
+-/
+def extractLsb (hi lo : Nat) (a : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ a
+
 -- TODO: write this using multiplication
 /-- `replicate i x` concatenates `i` copies of `x` into a new vector of length `w*i`. -/
 def replicate : (i : Nat) → BitVec w → BitVec (w*i)
@@ -564,6 +437,70 @@ def replicate : (i : Nat) → BitVec w → BitVec (w*i)
       rw [Nat.mul_add, Nat.add_comm, Nat.mul_one]
     hEq ▸ (x ++ replicate n x)
 
+/-- Fills a bitvector with `w` copies of the bit `b`. -/
+def fill (w : Nat) (b : Bool) : BitVec w := bif b then -1 else 0
+
+/--
+Zero extend vector `x` of length `w` by adding zeros in the high bits until it has length `v`.
+If `v < w` then it truncates the high bits instead.
+
+SMT-Lib name: `zero_extend`.
+-/
+def zeroExtend (v : Nat) (x : BitVec w) : BitVec v :=
+  if h : w ≤ v then
+    zeroExtend' h x
+  else
+    .ofNat v x.toNat
+
+/--
+Truncate the high bits of bitvector `x` of length `w`, resulting in a vector of length `v`.
+If `v > w` then it zero-extends the vector instead.
+-/
+abbrev truncate := @zeroExtend
+
+/--
+Sign extend a vector of length `w`, extending with `i` additional copies of the most significant
+bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
+
+SMT-Lib name: `sign_extend`.
+-/
+def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
+
+/-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
+@[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl
+@[simp] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
+@[simp] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
+@[simp] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
+@[simp] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
+@[simp] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
+@[simp] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
+@[simp] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
+@[simp] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
+@[simp] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
+@[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
+@[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
+
+@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
+    cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by
+  subst h; rfl
+
+@[simp] theorem cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
+    cast h₂ (cast h₁ x) = cast (h₁ ▸ h₂) x :=
+  rfl
+
+@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) :
+    cast h x = x :=
+  rfl
+
+/-- Turn a `Bool` into a bitvector of length `1` -/
+def ofBool (b : Bool) : BitVec 1 := cond b 1 0
+
+@[simp] theorem ofBool_false : ofBool false = 0 := by trivial
+@[simp] theorem ofBool_true  : ofBool true  = 1 := by trivial
+
+/-- The empty bitvector -/
+abbrev nil : BitVec 0 := 0
+
 /-!
 ### Cons and Concat
 We give special names to the operations of adding a single bit to either end of a bitvector.
@@ -581,6 +518,14 @@ def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool
 def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) :=
   ((ofBool msb) ++ lsbs).cast (Nat.add_comm ..)
 
+/-- All empty bitvectors are equal -/
+instance : Subsingleton (BitVec 0) where
+  allEq := by intro ⟨0, _⟩ ⟨0, _⟩; rfl
+
+/-- Every bitvector of length 0 is equal to `nil`, i.e., there is only one empty bitvector -/
+theorem eq_nil : ∀ (x : BitVec 0), x = nil
+  | ofFin ⟨0, _⟩ => rfl
+
 theorem append_ofBool (msbs : BitVec w) (lsb : Bool) :
     msbs ++ ofBool lsb = concat msbs lsb :=
   rfl
@@ -588,23 +533,3 @@ theorem append_ofBool (msbs : BitVec w) (lsb : Bool) :
 theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
     ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
   rfl
-
-end bitwise
-
-section normalization_eqs
-/-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
-@[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl
-@[simp] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
-@[simp] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
-@[simp] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
-@[simp] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
-@[simp] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
-@[simp] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
-@[simp] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
-@[simp] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
-@[simp] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
-@[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
-@[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
-end normalization_eqs
-
-end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -1,5 +1,6 @@
 /-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix
 -/
@@ -29,23 +30,9 @@ https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
 
 open Nat Bool
 
-namespace Bool
-
-/-- At least two out of three booleans are true. -/
-abbrev atLeastTwo (a b c : Bool) : Bool := a && b || a && c || b && c
-
-@[simp] theorem atLeastTwo_false_left  : atLeastTwo false b c = (b && c) := by simp [atLeastTwo]
-@[simp] theorem atLeastTwo_false_mid   : atLeastTwo a false c = (a && c) := by simp [atLeastTwo]
-@[simp] theorem atLeastTwo_false_right : atLeastTwo a b false = (a && b) := by simp [atLeastTwo]
-@[simp] theorem atLeastTwo_true_left   : atLeastTwo true b c  = (b || c) := by cases b <;> cases c <;> simp [atLeastTwo]
-@[simp] theorem atLeastTwo_true_mid    : atLeastTwo a true c  = (a || c) := by cases a <;> cases c <;> simp [atLeastTwo]
-@[simp] theorem atLeastTwo_true_right  : atLeastTwo a b true  = (a || b) := by cases a <;> cases b <;> simp [atLeastTwo]
-
-end Bool
-
 /-! ### Preliminaries -/
 
-namespace BitVec
+namespace Std.BitVec
 
 private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
     testBit x i = decide (x ≥ 2^i) := by
@@ -89,29 +76,18 @@ private theorem mod_two_pow_succ (x i : Nat) :
     have not_j_ge_i : ¬(j ≥ i) := Nat.not_le_of_lt j_lt_i
     simp [j_lt_i, j_le_i, not_j_ge_i, j_le_i_succ]
 
-private theorem mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ
-     (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by
-  have : c.toNat ≤ 1 := Bool.toNat_le c
-  rw [Nat.pow_succ]
-  omega
+private theorem mod_two_pow_lt (x i : Nat) : x % 2 ^ i < 2^i := Nat.mod_lt _ (Nat.two_pow_pos _)
 
 /-! ### Addition -/
 
-/-- carry i x y c returns true if the `i` carry bit is true when computing `x + y + c`. -/
-def carry (i : Nat) (x y : BitVec w) (c : Bool) : Bool :=
-  decide (x.toNat % 2^i + y.toNat % 2^i + c.toNat ≥ 2^i)
+/-- carry w x y c returns true if the `w` carry bit is true when computing `x + y + c`. -/
+def carry (w x y : Nat) (c : Bool) : Bool := decide (x % 2^w + y % 2^w + c.toNat ≥ 2^w)
 
 @[simp] theorem carry_zero : carry 0 x y c = c := by
   cases c <;> simp [carry, mod_one]
 
-theorem carry_succ (i : Nat) (x y : BitVec w) (c : Bool) :
-    carry (i+1) x y c = atLeastTwo (x.getLsb i) (y.getLsb i) (carry i x y c) := by
-  simp only [carry, mod_two_pow_succ, atLeastTwo, getLsb]
-  simp only [Nat.pow_succ']
-  have sum_bnd : x.toNat%2^i + (y.toNat%2^i + c.toNat) < 2*2^i := by
-    simp only [← Nat.pow_succ']
-    exact mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ ..
-  cases x.toNat.testBit i <;> cases y.toNat.testBit i <;> (simp; omega)
+/-- At least two out of three booleans are true. -/
+abbrev atLeastTwo (a b c : Bool) : Bool := a && b || a && c || b && c
 
 /-- Carry function for bitwise addition. -/
 def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xor y c))
@@ -120,9 +96,25 @@ def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xo
 def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
   iunfoldr fun (i : Fin w) c => adcb (x.getLsb i) (y.getLsb i) c
 
+theorem adc_overflow_limit (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by
+  have : c.toNat ≤ 1 := Bool.toNat_le_one c
+  rw [Nat.pow_succ]
+  omega
+
+theorem carry_succ (w x y : Nat) (c : Bool) :
+    carry (succ w) x y c = atLeastTwo (x.testBit w) (y.testBit w) (carry w x y c) := by
+  simp only [carry, mod_two_pow_succ, atLeastTwo]
+  simp only [Nat.pow_succ']
+  generalize testBit x w = xh
+  generalize testBit y w = yh
+  have sum_bnd : x%2^w + (y%2^w + c.toNat) < 2*2^w := by
+          simp only [← Nat.pow_succ']
+          exact adc_overflow_limit x y w c
+  cases xh <;> cases yh <;> (simp; omega)
+
 theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
     getLsb (x + y + zeroExtend w (ofBool c)) i =
-      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x y c)) := by
+      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x.toNat y.toNat c)) := by
   let ⟨x, x_lt⟩ := x
   let ⟨y, y_lt⟩ := y
   simp only [getLsb, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
@@ -137,27 +129,33 @@ theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool)
       Bool.true_and,
       Nat.add_assoc,
       Nat.add_left_comm (_%_) (_ * _) _,
-      testBit_limit (mod_two_pow_add_mod_two_pow_add_bool_lt_two_pow_succ x y i c)
+      testBit_limit (adc_overflow_limit x y i c)
     ]
   simp [testBit_to_div_mod, carry, Nat.add_assoc]
 
 theorem getLsb_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
     getLsb (x + y) i =
-      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x y false)) := by
+      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x.toNat y.toNat false)) := by
   simpa using getLsb_add_add_bool i_lt x y false
 
 theorem adc_spec (x y : BitVec w) (c : Bool) :
-    adc x y c = (carry w x y c, x + y + zeroExtend w (ofBool c)) := by
+    adc x y c = (carry w x.toNat y.toNat c, x + y + zeroExtend w (ofBool c)) := by
   simp only [adc]
   apply iunfoldr_replace
-          (fun i => carry i x y c)
+          (fun i => carry i x.toNat y.toNat c)
           (x + y + zeroExtend w (ofBool c))
           c
   case init =>
     simp [carry, Nat.mod_one]
     cases c <;> rfl
   case step =>
-    simp [adcb, Prod.mk.injEq, carry_succ, getLsb_add_add_bool]
+    intro ⟨i, lt⟩
+    simp only [adcb, Prod.mk.injEq, carry_succ]
+    apply And.intro
+    case left =>
+      rw [testBit_toNat, testBit_toNat]
+    case right =>
+      simp [getLsb_add_add_bool lt]
 
 theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := by
   simp [adc_spec]
@@ -173,5 +171,3 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 /-- Subtracting `x` from the all ones bitvector is equivalent to taking its complement -/
 theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
   rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]
-
-end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -8,7 +8,7 @@ import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate
 
-namespace BitVec
+namespace Std.BitVec
 
 /--
 iunfoldr is an iterative operation that applies a function `f` repeatedly.
@@ -57,5 +57,3 @@ theorem iunfoldr_replace
     (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
-
-end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,7 @@ import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 
-namespace BitVec
+namespace Std.BitVec
 
 /--
 This normalized a bitvec using `ofFin` to `ofNat`.
@@ -23,12 +23,9 @@ theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j
 
 @[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
 
-@[bv_toNat] theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
+theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
   Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
 
-@[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
-  rw [Ne, toNat_eq]
-
 theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.toFin.2
 
 theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
@@ -81,8 +78,6 @@ theorem eq_of_getMsb_eq {x y : BitVec w}
     have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
-@[simp] theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp
-
 theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
@@ -95,15 +90,9 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  b
 theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
   decide
 
-@[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
+@[simp] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
-@[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
-
-@[simp] theorem getLsb_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
-  getLsb (x#'lt) i = x.testBit i := by
-  simp [getLsb, BitVec.ofNatLt]
-
-@[simp, bv_toNat] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
+@[simp] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
   simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
 
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
@@ -112,9 +101,7 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
   getLsb (x#n) i = (i < n && x.testBit i) := by
   simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
 
-@[simp, deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
-
-@[simp] theorem getLsb_zero : (0#w).getLsb i = false := by simp [getLsb]
+@[deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
 
 @[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
   Nat.mod_eq_of_lt x.isLt
@@ -122,20 +109,23 @@ theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
   Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
 
+@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : x.toNat#m = truncate m x := by
+  let ⟨x, lt_n⟩ := x
+  unfold truncate
+  unfold zeroExtend
+  if h : n ≤ m then
+    unfold zeroExtend'
+    have lt_m : x < 2 ^ m := lt_two_pow_of_le lt_n h
+    simp [h, lt_m, Nat.mod_eq_of_lt, BitVec.toNat, BitVec.ofNat, Fin.ofNat']
+  else
+    simp [h]
+
+
 /-! ### msb -/
 
-@[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsb]
-
-theorem msb_eq_getLsb_last (x : BitVec w) :
-    x.msb = x.getLsb (w - 1) := by
-  simp [BitVec.msb, getMsb, getLsb]
-  rcases w  with rfl | w
-  · simp [BitVec.eq_nil x]
-  · simp
-
-@[bv_toNat] theorem getLsb_last (x : BitVec (w + 1)) :
-    x.getLsb w = decide (2 ^ w ≤ x.toNat) := by
-  simp only [Nat.zero_lt_succ, decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
+theorem msb_eq_decide (x : BitVec (Nat.succ w)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
+  simp only [BitVec.msb, getMsb, Nat.zero_lt_succ,
+    decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
     Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
   rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
   · simp [Nat.div_eq_of_lt h, h]
@@ -145,12 +135,9 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
     · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
       omega
 
-@[bv_toNat] theorem msb_eq_decide (x : BitVec (w + 1)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
-  simp [msb_eq_getLsb_last, getLsb_last]
-
 /-! ### cast -/
 
-@[simp, bv_toNat] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
+@[simp] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
 @[simp] theorem toFin_cast (h : w = v) (x : BitVec w) :
     (cast h x).toFin = x.toFin.cast (by rw [h]) :=
   rfl
@@ -165,12 +152,12 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
 
 /-! ### zeroExtend and truncate -/
 
-@[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
+@[simp] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
     (zeroExtend' p x).toNat = x.toNat := by
   unfold zeroExtend'
   simp [p, x.isLt, Nat.mod_eq_of_lt]
 
-@[bv_toNat] theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
+theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
     BitVec.toNat (zeroExtend i x) = x.toNat % 2^i := by
   let ⟨x, lt_n⟩ := x
   simp only [zeroExtend]
@@ -180,9 +167,6 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
   else
     simp [n_le_i, toNat_ofNat]
 
-@[simp, bv_toNat] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
-  toNat_zeroExtend i x
-
 @[simp] theorem zeroExtend_eq (x : BitVec n) : zeroExtend n x = x := by
   apply eq_of_toNat_eq
   let ⟨x, lt_n⟩ := x
@@ -194,9 +178,8 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
 
 @[simp] theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
 
-@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : x.toNat#m = truncate m x := by
-  apply eq_of_toNat_eq
-  simp
+@[simp] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
+  toNat_zeroExtend i x
 
 @[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
     getLsb (zeroExtend' ge x) i = getLsb x i := by
@@ -210,23 +193,6 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
     getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
   getLsb_zeroExtend m x i
 
-@[simp] theorem zeroExtend_zeroExtend_of_le (x : BitVec w) (h : k ≤ l) :
-    (x.zeroExtend l).zeroExtend k = x.zeroExtend k := by
-  ext i
-  simp only [getLsb_zeroExtend, Fin.is_lt, decide_True, Bool.true_and]
-  have p := lt_of_getLsb x i
-  revert p
-  cases getLsb x i <;> simp; omega
-
-@[simp] theorem truncate_truncate_of_le (x : BitVec w) (h : k ≤ l) :
-    (x.truncate l).truncate k = x.truncate k :=
-  zeroExtend_zeroExtend_of_le x h
-
-theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) && x.getLsb (v - 1)) := by
-  rw [msb_eq_getLsb_last]
-  simp only [getLsb_zeroExtend]
-  cases getLsb x (v - 1) <;> simp; omega
-
 /-! ## extractLsb -/
 
 @[simp]
@@ -253,12 +219,31 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 /-! ### allOnes -/
 
+private theorem allOnes_def :
+    allOnes v = .ofFin (⟨0, Nat.two_pow_pos v⟩ - ⟨1 % 2^v, Nat.mod_lt _ (Nat.two_pow_pos v)⟩) := by
+  rfl
+
 @[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by
-  unfold allOnes
-  simp
+  simp only [allOnes_def, toNat_ofFin, Fin.coe_sub, Nat.zero_add]
+  by_cases h : v = 0
+  · subst h
+    rfl
+  · rw [Nat.mod_eq_of_lt (Nat.one_lt_two_pow h), Nat.mod_eq_of_lt]
+    exact Nat.pred_lt_self (Nat.two_pow_pos v)
 
 @[simp] theorem getLsb_allOnes : (allOnes v).getLsb i = decide (i < v) := by
-  simp [allOnes]
+  simp only [allOnes_def, getLsb_ofFin, Fin.coe_sub, Nat.zero_add, Nat.testBit_mod_two_pow]
+  if h : i < v then
+    simp only [h, decide_True, Bool.true_and]
+    match i, v, h with
+    | i, (v + 1), h =>
+      rw [Nat.mod_eq_of_lt (by simp), Nat.testBit_two_pow_sub_one]
+      simp [h]
+  else
+    simp [h]
+
+@[simp] theorem negOne_eq_allOnes : -1#w = allOnes w :=
+  rfl
 
 /-! ### or -/
 
@@ -267,9 +252,10 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 @[simp] theorem toFin_or (x y : BitVec v) :
     BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y := by
-  apply Fin.eq_of_val_eq
+  simp only [HOr.hOr, OrOp.or, BitVec.or, Fin.lor, val_toFin, Fin.mk.injEq]
   exact (Nat.mod_eq_of_lt <| Nat.or_lt_two_pow x.isLt y.isLt).symm
 
+
 @[simp] theorem getLsb_or {x y : BitVec v} : (x ||| y).getLsb i = (x.getLsb i || y.getLsb i) := by
   rw [← testBit_toNat, getLsb, getLsb]
   simp
@@ -281,7 +267,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 @[simp] theorem toFin_and (x y : BitVec v) :
     BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y := by
-  apply Fin.eq_of_val_eq
+  simp only [HAnd.hAnd, AndOp.and, BitVec.and, Fin.land, val_toFin, Fin.mk.injEq]
   exact (Nat.mod_eq_of_lt <| Nat.and_lt_two_pow _ y.isLt).symm
 
 @[simp] theorem getLsb_and {x y : BitVec v} : (x &&& y).getLsb i = (x.getLsb i && y.getLsb i) := by
@@ -295,7 +281,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 @[simp] theorem toFin_xor (x y : BitVec v) :
     BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y := by
-  apply Fin.eq_of_val_eq
+  simp only [HXor.hXor, Xor.xor, BitVec.xor, Fin.xor, val_toFin, Fin.mk.injEq]
   exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
 
 @[simp] theorem getLsb_xor {x y : BitVec v} :
@@ -307,7 +293,7 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 
-@[simp, bv_toNat] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by
+@[simp] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by
   rw [Nat.sub_sub, Nat.add_comm, not_def, toNat_xor]
   apply Nat.eq_of_testBit_eq
   intro i
@@ -337,7 +323,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 
 /-! ### shiftLeft -/
 
-@[simp, bv_toNat] theorem toNat_shiftLeft {x : BitVec v} :
+@[simp] theorem toNat_shiftLeft {x : BitVec v} :
     BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
   BitVec.toNat_ofNat _ _
 
@@ -373,7 +359,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
 
 /-! ### ushiftRight -/
 
-@[simp, bv_toNat] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
+@[simp] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
     (x >>> i).toNat = x.toNat >>> i := rfl
 
 @[simp] theorem getLsb_ushiftRight (x : BitVec n) (i j : Nat) :
@@ -443,30 +429,6 @@ theorem truncate_succ (x : BitVec w) :
     have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
-/-! ### concat -/
-
-@[simp] theorem toNat_concat (x : BitVec w) (b : Bool) :
-    (concat x b).toNat = x.toNat * 2 + b.toNat := by
-  apply Nat.eq_of_testBit_eq
-  simp only [concat, toNat_append, Nat.shiftLeft_eq, Nat.pow_one, toNat_ofBool, Nat.testBit_or]
-  cases b
-  · simp
-  · rintro (_ | i)
-    <;> simp [Nat.add_mod, Nat.add_comm, Nat.add_mul_div_right]
-
-theorem getLsb_concat (x : BitVec w) (b : Bool) (i : Nat) :
-    (concat x b).getLsb i = if i = 0 then b else x.getLsb (i - 1) := by
-  simp only [concat, getLsb, toNat_append, toNat_ofBool, Nat.testBit_or, Nat.shiftLeft_eq]
-  cases i
-  · simp [Nat.mod_eq_of_lt b.toNat_lt]
-  · simp [Nat.div_eq_of_lt b.toNat_lt]
-
-@[simp] theorem getLsb_concat_zero : (concat x b).getLsb 0 = b := by
-  simp [getLsb_concat]
-
-@[simp] theorem getLsb_concat_succ : (concat x b).getLsb (i + 1) = x.getLsb i := by
-  simp [getLsb_concat]
-
 /-! ### add -/
 
 theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
@@ -474,7 +436,7 @@ theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := r
 /--
 Definition of bitvector addition as a nat.
 -/
-@[simp, bv_toNat] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
+@[simp] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
 @[simp] theorem toFin_add (x y : BitVec w) : (x + y).toFin = toFin x + toFin y := rfl
 @[simp] theorem ofFin_add (x : Fin (2^n)) (y : BitVec n) :
   .ofFin x + y = .ofFin (x + y.toFin) := rfl
@@ -498,7 +460,7 @@ protected theorem add_comm (x y : BitVec n) : x + y = y + x := by
 
 theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n (x.toNat + (2^n - y.toNat)) := by rfl
 
-@[simp, bv_toNat] theorem toNat_sub {n} (x y : BitVec n) :
+@[simp] theorem toNat_sub {n} (x y : BitVec n) :
   (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := rfl
 @[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
 
@@ -520,7 +482,7 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : x#n - y#n = .ofNat n (x + (2^n - y % 2
   · simp
   · exact Nat.le_of_lt x.isLt
 
-@[simp, bv_toNat] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
+@[simp] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
   simp [Neg.neg, BitVec.neg]
 
 theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
@@ -535,44 +497,16 @@ theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
   rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
     Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
 
-theorem negOne_eq_allOnes : -1#w = allOnes w := by
-  apply eq_of_toNat_eq
-  if g : w = 0 then
-    simp [g]
-  else
-    have q : 1 < 2^w := by simp [g]
-    have r : (2^w - 1) < 2^w := by omega
-    simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
-
 /-! ### mul -/
 
 theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
 
-@[simp, bv_toNat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
+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
 
-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⟩
-
-protected theorem mul_assoc (x y z : BitVec w) : x * y * z = x * (y * z) := by
-  apply eq_of_toFin_eq; simpa using Fin.mul_assoc ..
-instance : Std.Associative (fun (x y : BitVec w) => x * y) := ⟨BitVec.mul_assoc⟩
-
-@[simp] protected theorem mul_one (x : BitVec w) : x * 1#w = x := by
-  cases w
-  · apply Subsingleton.elim
-  · apply eq_of_toNat_eq; simp [Nat.mod_eq_of_lt]
-
-@[simp] protected theorem one_mul (x : BitVec w) : 1#w * x = x := by
-  rw [BitVec.mul_comm, BitVec.mul_one]
-
-instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
-  right_id := BitVec.mul_one
-
 /-! ### le and lt -/
 
-@[bv_toNat] theorem le_def (x y : BitVec n) :
+theorem le_def (x y : BitVec n) :
   x ≤ y ↔ x.toNat ≤ y.toNat := Iff.rfl
 
 @[simp] theorem le_ofFin (x : BitVec n) (y : Fin (2^n)) :
@@ -582,7 +516,7 @@ instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
 @[simp] theorem ofNat_le_ofNat {n} (x y : Nat) : (x#n) ≤ (y#n) ↔ x % 2^n ≤ y % 2^n := by
   simp [le_def]
 
-@[bv_toNat] theorem lt_def (x y : BitVec n) :
+theorem lt_def (x y : BitVec n) :
   x < y ↔ x.toNat < y.toNat := Iff.rfl
 
 @[simp] theorem lt_ofFin (x : BitVec n) (y : Fin (2^n)) :
@@ -598,5 +532,3 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   let ⟨y, lt⟩ := y
   simp
   exact Nat.lt_of_le_of_ne
-
-end BitVec

src/Init/Data/Bool.lean

@@ -48,11 +48,6 @@ theorem ne_false_iff : {b : Bool} → b ≠ false ↔ b = true := by decide
 
 theorem eq_iff_iff {a b : Bool} : a = b ↔ (a ↔ b) := by cases b <;> simp
 
-@[simp] theorem decide_eq_true {b : Bool} : decide (b = true) = b := by cases b <;> simp
-@[simp] theorem decide_eq_false {b : Bool} : decide (b = false) = !b := by cases b <;> simp
-@[simp] theorem decide_true_eq {b : Bool} : decide (true = b) = b := by cases b <;> simp
-@[simp] theorem decide_false_eq {b : Bool} : decide (false = b) = !b := by cases b <;> simp
-
 /-! ### and -/
 
 @[simp] theorem not_and_self : ∀ (x : Bool), (!x && x) = false := by decide
@@ -217,19 +212,9 @@ def toNat (b:Bool) : Nat := cond b 1 0
 
 @[simp] theorem toNat_true : true.toNat = 1 := rfl
 
-theorem toNat_le (c : Bool) : c.toNat ≤ 1 := by
+theorem toNat_le_one (c:Bool) : c.toNat ≤ 1 := by
   cases c <;> trivial
 
-@[deprecated toNat_le] abbrev toNat_le_one := toNat_le
-
-theorem toNat_lt (b : Bool) : b.toNat < 2 :=
-  Nat.lt_succ_of_le (toNat_le _)
-
-@[simp] theorem toNat_eq_zero (b : Bool) : b.toNat = 0 ↔ b = false := by
-  cases b <;> simp
-@[simp] theorem toNat_eq_one (b : Bool) : b.toNat = 1 ↔ b = true := by
-  cases b <;> simp
-
 end Bool
 
 /-! ### cond -/

src/Init/Data/Fin/Basic.lean

@@ -156,19 +156,6 @@ def natAdd (n) (i : Fin m) : Fin (n + m) := ⟨n + i, Nat.add_lt_add_left i.2 _
 @[inline] def pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n :=
   subNat 1 i <| Nat.pos_of_ne_zero <| mt (Fin.eq_of_val_eq (j := 0)) h
 
-theorem val_inj {a b : Fin n} : a.1 = b.1 ↔ a = b := ⟨Fin.eq_of_val_eq, Fin.val_eq_of_eq⟩
-
-theorem val_congr {n : Nat} {a b : Fin n} (h : a = b) : (a : Nat) = (b : Nat) :=
-  Fin.val_inj.mpr h
-
-theorem val_le_of_le {n : Nat} {a b : Fin n} (h : a ≤ b) : (a : Nat) ≤ (b : Nat) := h
-
-theorem val_le_of_ge {n : Nat} {a b : Fin n} (h : a ≥ b) : (b : Nat) ≤ (a : Nat) := h
-
-theorem val_add_one_le_of_lt {n : Nat} {a b : Fin n} (h : a < b) : (a : Nat) + 1 ≤ (b : Nat) := h
-
-theorem val_add_one_le_of_gt {n : Nat} {a b : Fin n} (h : a > b) : (b : Nat) + 1 ≤ (a : Nat) := h
-
 end Fin
 
 instance [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where

src/Init/Data/Fin/Iterate.lean

@@ -1,5 +1,6 @@
 /-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix
 -/

src/Init/Data/Fin/Lemmas.lean

@@ -36,6 +36,8 @@ theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
 
 @[ext] theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
 
+theorem val_inj {a b : Fin n} : a.1 = b.1 ↔ a = b := ⟨Fin.eq_of_val_eq, Fin.val_eq_of_eq⟩
+
 theorem ext_iff {a b : Fin n} : a = b ↔ a.1 = b.1 := val_inj.symm
 
 theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
@@ -793,12 +795,6 @@ protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
 protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
   ext <| by rw [mul_def, mul_def, Nat.mul_comm]
 
-protected theorem mul_assoc (a b c : Fin n) : a * b * c = a * (b * c) := by
-  apply eq_of_val_eq
-  simp only [val_mul]
-  rw [← Nat.mod_eq_of_lt a.isLt, ← Nat.mod_eq_of_lt b.isLt, ← Nat.mod_eq_of_lt c.isLt]
-  simp only [← Nat.mul_mod, Nat.mul_assoc]
-
 protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
   rw [Fin.mul_comm, Fin.mul_one]
 

src/Init/Data/Int/DivModLemmas.lean

@@ -22,7 +22,7 @@ namespace Int
 
 /-! ### `/`  -/
 
-@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+@[simp] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
 @[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
   | ofNat _ => show ofNat _ = _ by simp
@@ -102,7 +102,7 @@ theorem ofNat_mod (m n : Nat) : (↑(m % n) : Int) = mod m n := rfl
 
 theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl
 
-@[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
+@[simp] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
 
 @[simp] theorem zero_emod (b : Int) : 0 % b = 0 := by simp [mod_def', emod]
 
@@ -260,7 +260,7 @@ protected theorem dvd_sub : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b -
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d - e, by rw [Int.mul_sub]⟩
 
 
-@[norm_cast] theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by
+theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by
   refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩
   match Int.le_total a 0 with
   | .inl h =>

src/Init/Data/Int/Lemmas.lean

@@ -22,8 +22,8 @@ theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat
 
 @[simp] protected theorem neg_zero : -(0:Int) = 0 := rfl
 
-@[norm_cast] theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl
-@[norm_cast] theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
+theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl
+theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
 theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
 
 @[local simp] theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
@@ -53,7 +53,7 @@ theorem negOfNat_eq : negOfNat n = -ofNat n := rfl
 
 /- ## some basic functions and properties -/
 
-@[norm_cast] theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩
+theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩
 
 theorem ofNat_eq_zero : ((n : Nat) : Int) = 0 ↔ n = 0 := ofNat_inj
 
@@ -67,7 +67,7 @@ theorem negSucc_eq (n : Nat) : -[n+1] = -((n : Int) + 1) := rfl
 
 @[simp] theorem zero_ne_negSucc (n : Nat) : 0 ≠ -[n+1] := nofun
 
-@[simp, norm_cast] theorem Nat.cast_ofNat_Int :
+@[simp] theorem Nat.cast_ofNat_Int :
   (Nat.cast (no_index (OfNat.ofNat n)) : Int) = OfNat.ofNat n := rfl
 
 /- ## neg -/
@@ -295,7 +295,7 @@ protected theorem sub_neg (a b : Int) : a - -b = a + b := by simp [Int.sub_eq_ad
 protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
   rw [Int.sub_eq_add_neg, Int.add_assoc, ← Int.sub_eq_add_neg]
 
-@[norm_cast] theorem ofNat_sub (h : m ≤ n) : ((n - m : Nat) : Int) = n - m := by
+theorem ofNat_sub (h : m ≤ n) : ((n - m : Nat) : Int) = n - m := by
   match m with
   | 0 => rfl
   | succ m =>
@@ -478,10 +478,6 @@ theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a ≠ 0) (H : b * a = a)
 theorem eq_one_of_mul_eq_self_right {a b : Int} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 :=
   Int.eq_of_mul_eq_mul_left Hpos <| by rw [Int.mul_one, H]
 
-protected theorem pow_succ (b : Int) (e : Nat) : b ^ (e+1) = (b ^ e) * b := rfl
-protected theorem pow_succ' (b : Int) (e : Nat) : b ^ (e+1) = b * (b ^ e) := by
-  rw [Int.mul_comm, Int.pow_succ]
-
 /-! NatCast lemmas -/
 
 /-!

src/Init/Data/Int/Order.lean

@@ -48,7 +48,7 @@ protected theorem le_total (a b : Int) : a ≤ b ∨ b ≤ a :=
   (nonneg_or_nonneg_neg (b - a)).imp_right fun H => by
     rwa [show -(b - a) = a - b by simp [Int.add_comm, Int.sub_eq_add_neg]] at H
 
-@[simp, norm_cast] theorem ofNat_le {m n : Nat} : (↑m : Int) ≤ ↑n ↔ m ≤ n :=
+@[simp] theorem ofNat_le {m n : Nat} : (↑m : Int) ≤ ↑n ↔ m ≤ n :=
   ⟨fun h =>
     let ⟨k, hk⟩ := le.dest h
     Nat.le.intro <| Int.ofNat.inj <| (Int.ofNat_add m k).trans hk,
@@ -74,10 +74,10 @@ theorem lt.intro {a b : Int} {n : Nat} (h : a + Nat.succ n = b) : a < b :=
 theorem lt.dest {a b : Int} (h : a < b) : ∃ n : Nat, a + Nat.succ n = b :=
   let ⟨n, h⟩ := le.dest h; ⟨n, by rwa [Int.add_comm, Int.add_left_comm] at h⟩
 
-@[simp, norm_cast] theorem ofNat_lt {n m : Nat} : (↑n : Int) < ↑m ↔ n < m := by
+@[simp] theorem ofNat_lt {n m : Nat} : (↑n : Int) < ↑m ↔ n < m := by
   rw [lt_iff_add_one_le, ← ofNat_succ, ofNat_le]; rfl
 
-@[simp, norm_cast] theorem ofNat_pos {n : Nat} : 0 < (↑n : Int) ↔ 0 < n := ofNat_lt
+@[simp] theorem ofNat_pos {n : Nat} : 0 < (↑n : Int) ↔ 0 < n := ofNat_lt
 
 theorem ofNat_nonneg (n : Nat) : 0 ≤ (n : Int) := ⟨_⟩
 

src/Init/Data/List/BasicAux.lean

@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Linear
-import Init.Data.Array.Basic
 import Init.Data.List.Basic
 import Init.Util
 
@@ -208,23 +207,4 @@ if the result of each `f a` is a pointer equal value `a`.
 def mapMono (as : List α) (f : α → α) : List α :=
   Id.run <| as.mapMonoM f
 
-/--
-Monadic generalization of `List.partition`.
-
-This uses `Array.toList` and which isn't imported by `Init.Data.List.Basic`.
--/
-@[inline] def partitionM [Monad m] (p : α → m Bool) (l : List α) : m (List α × List α) :=
-  go l #[] #[]
-where
-  /-- Auxiliary for `partitionM`:
-  `partitionM.go p l acc₁ acc₂` returns `(acc₁.toList ++ left, acc₂.toList ++ right)`
-  if `partitionM p l` returns `(left, right)`. -/
-  @[specialize] go : List α → Array α → Array α → m (List α × List α)
-  | [], acc₁, acc₂ => pure (acc₁.toList, acc₂.toList)
-  | x :: xs, acc₁, acc₂ => do
-    if ← p x then
-      go xs (acc₁.push x) acc₂
-    else
-      go xs acc₁ (acc₂.push x)
-
 end List

src/Init/Data/List/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 prelude
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
-import Init.Data.Nat.Lemmas
 import Init.PropLemmas
 import Init.Control.Lawful
 import Init.Hints
@@ -106,11 +105,6 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s
 @[simp] theorem append_eq_nil : p ++ q = [] ↔ p = [] ∧ q = [] := by
   cases p <;> simp
 
-theorem get_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length),
-    (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩
-| a :: l, _, 0, h => rfl
-| a :: l, _, n+1, h => by simp only [get, cons_append]; apply get_append
-
 /-! ### map -/
 
 @[simp] theorem map_nil {f : α → β} : map f [] = [] := rfl
@@ -210,12 +204,6 @@ theorem get?_eq_some : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
   | _ :: _, 0 => rfl
   | _ :: l, n+1 => get?_map f l n
 
-theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
-  (l₁ ++ l₂).get? n = l₁.get? n := by
-  have hn' : n < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <|
-    length_append .. ▸ Nat.le_add_right ..
-  rw [get?_eq_get hn, get?_eq_get hn', get_append]
-
 @[simp] theorem get?_concat_length : ∀ (l : List α) (a : α), (l ++ [a]).get? l.length = some a
   | [], a => rfl
   | b :: l, a => by rw [cons_append, length_cons]; simp only [get?, get?_concat_length]
@@ -242,31 +230,6 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1)
 @[simp] theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
   simp [getLast?_eq_get?, Nat.succ_sub_succ]
 
-theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a
-  | [], _, _ => rfl
-  | _a::_, 0, _ => rfl
-  | _::l, _+1, _ => getD_eq_get? (l := l) ..
-
-theorem get?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
-  (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
-| [], _, n, _ => rfl
-| a :: l, _, n+1, h₁ => by rw [cons_append]; simp [get?_append_right (Nat.lt_succ.1 h₁)]
-
-theorem get?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
-    get? l.reverse i = get? l j
-  | [], _, _, _ => rfl
-  | a::l, i, 0, h => by simp at h; simp [h, get?_append_right]
-  | a::l, i, j+1, h => by
-    have := Nat.succ.inj h; simp at this ⊢
-    rw [get?_append, get?_reverse' _ j this]
-    rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _)
-
-theorem get?_reverse {l : List α} (i) (h : i < length l) :
-    get? l.reverse i = get? l (l.length - 1 - i) :=
-  get?_reverse' _ _ <| by
-    rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
-      Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
-
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l

src/Init/Data/Nat/Bitwise.lean

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

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

@@ -1,5 +1,6 @@
 /-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joe Hendrix
 -/

src/Init/Data/Nat/Dvd.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
--/
 prelude
 import Init.Data.Nat.Div
 
@@ -90,6 +85,7 @@ theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by
   rw [dvd_iff_mod_eq_zero] at h
   exact Nat.pos_of_ne_zero h
 
+
 protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m := by
   have := mod_add_div m n
   rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this

src/Init/Data/Nat/MinMax.lean

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

src/Init/Data/String/Basic.lean

@@ -290,40 +290,17 @@ where go (acc : String) (s : String) : List String → String
   | a :: as => go (acc ++ s ++ a) s as
   | []      => acc
 
-/-- Iterator over the characters (`Char`) of a `String`.
-
-Typically created by `s.iter`, where `s` is a `String`.
-
-An iterator is *valid* if the position `i` is *valid* for the string `s`, meaning `0 ≤ i ≤ s.endPos`
-and `i` lies on a UTF8 byte boundary. If `i = s.endPos`, the iterator is at the end of the string.
-
-Most operations on iterators return arbitrary values if the iterator is not valid. The functions in
-the `String.Iterator` API should rule out the creation of invalid iterators, with two exceptions:
-
-- `Iterator.next iter` is invalid if `iter` is already at the end of the string (`iter.atEnd` is
-  `true`), and
-- `Iterator.forward iter n`/`Iterator.nextn iter n` is invalid if `n` is strictly greater than the
-  number of remaining characters.
--/
+/-- Iterator for `String`. That is, a `String` and a position in that string. -/
 structure Iterator where
-  /-- The string the iterator is for. -/
   s : String
-  /-- The current position.
-
-  This position is not necessarily valid for the string, for instance if one keeps calling
-  `Iterator.next` when `Iterator.atEnd` is true. If the position is not valid, then the
-  current character is `(default : Char)`, similar to `String.get` on an invalid position. -/
   i : Pos
   deriving DecidableEq
 
-/-- Creates an iterator at the beginning of a string. -/
 def mkIterator (s : String) : Iterator :=
   ⟨s, 0⟩
 
-@[inherit_doc mkIterator]
 abbrev iter := mkIterator
 
-/-- The size of a string iterator is the number of bytes remaining. -/
 instance : SizeOf String.Iterator where
   sizeOf i := i.1.utf8ByteSize - i.2.byteIdx
 
@@ -331,90 +308,55 @@ theorem Iterator.sizeOf_eq (i : String.Iterator) : sizeOf i = i.1.utf8ByteSize -
   rfl
 
 namespace Iterator
-@[inherit_doc Iterator.s]
-def toString := Iterator.s
+def toString : Iterator → String
+  | ⟨s, _⟩ => s
 
-/-- Number of bytes remaining in the iterator. -/
 def remainingBytes : Iterator → Nat
   | ⟨s, i⟩ => s.endPos.byteIdx - i.byteIdx
 
-@[inherit_doc Iterator.i]
-def pos := Iterator.i
+def pos : Iterator → Pos
+  | ⟨_, i⟩ => i
 
-/-- The character at the current position.
-
-On an invalid position, returns `(default : Char)`. -/
 def curr : Iterator → Char
   | ⟨s, i⟩ => get s i
 
-/-- Moves the iterator's position forward by one character, unconditionally.
-
-It is only valid to call this function if the iterator is not at the end of the string, *i.e.*
-`Iterator.atEnd` is `false`; otherwise, the resulting iterator will be invalid. -/
 def next : Iterator → Iterator
   | ⟨s, i⟩ => ⟨s, s.next i⟩
 
-/-- Decreases the iterator's position.
-
-If the position is zero, this function is the identity. -/
 def prev : Iterator → Iterator
   | ⟨s, i⟩ => ⟨s, s.prev i⟩
 
-/-- True if the iterator is past the string's last character. -/
 def atEnd : Iterator → Bool
   | ⟨s, i⟩ => i.byteIdx ≥ s.endPos.byteIdx
 
-/-- True if the iterator is not past the string's last character. -/
 def hasNext : Iterator → Bool
   | ⟨s, i⟩ => i.byteIdx < s.endPos.byteIdx
 
-/-- True if the position is not zero. -/
 def hasPrev : Iterator → Bool
   | ⟨_, i⟩ => i.byteIdx > 0
 
-/-- Replaces the current character in the string.
-
-Does nothing if the iterator is at the end of the string. If the iterator contains the only
-reference to its string, this function will mutate the string in-place instead of allocating a new
-one. -/
 def setCurr : Iterator → Char → Iterator
   | ⟨s, i⟩, c => ⟨s.set i c, i⟩
 
-/-- Moves the iterator's position to the end of the string.
-
-Note that `i.toEnd.atEnd` is always `true`. -/
 def toEnd : Iterator → Iterator
   | ⟨s, _⟩ => ⟨s, s.endPos⟩
 
-/-- Extracts the substring between the positions of two iterators.
-
-Returns the empty string if the iterators are for different strings, or if the position of the first
-iterator is past the position of the second iterator. -/
 def extract : Iterator → Iterator → String
   | ⟨s₁, b⟩, ⟨s₂, e⟩ =>
     if s₁ ≠ s₂ || b > e then ""
     else s₁.extract b e
 
-/-- Moves the iterator's position several characters forward.
-
-The resulting iterator is only valid if the number of characters to skip is less than or equal to
-the number of characters left in the iterator. -/
 def forward : Iterator → Nat → Iterator
   | it, 0   => it
   | it, n+1 => forward it.next n
 
-/-- The remaining characters in an iterator, as a string. -/
 def remainingToString : Iterator → String
   | ⟨s, i⟩ => s.extract i s.endPos
 
-@[inherit_doc forward]
 def nextn : Iterator → Nat → Iterator
   | it, 0   => it
   | it, i+1 => nextn it.next i
 
-/-- Moves the iterator's position several characters back.
-
-If asked to go back more characters than available, stops at the beginning of the string. -/
 def prevn : Iterator → Nat → Iterator
   | it, 0   => it
   | it, i+1 => prevn it.prev i

src/Init/Data/String/Extra.lean

@@ -4,7 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
+import Init.Control.Except
 import Init.Data.ByteArray
+import Init.SimpLemmas
+import Init.Data.Nat.Linear
+import Init.Util
+import Init.WFTactics
 
 namespace String
 

src/Init/Data/Sum.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Yury G. Kudryashov
--/
-prelude
-import Init.Core
-
-namespace Sum
-
-deriving instance DecidableEq for Sum
-deriving instance BEq for Sum
-
-/-- Check if a sum is `inl` and if so, retrieve its contents. -/
-def getLeft? : α ⊕ β → Option α
-  | inl a => some a
-  | inr _ => none
-
-/-- Check if a sum is `inr` and if so, retrieve its contents. -/
-def getRight? : α ⊕ β → Option β
-  | inr b => some b
-  | inl _ => none
-
-end Sum

src/Init/Meta.lean

@@ -9,7 +9,6 @@ prelude
 import Init.MetaTypes
 import Init.Data.Array.Basic
 import Init.Data.Option.BasicAux
-import Init.Data.String.Extra
 
 namespace Lean
 
@@ -106,42 +105,6 @@ def idEndEscape   := '»'
 def isIdBeginEscape (c : Char) : Bool := c = idBeginEscape
 def isIdEndEscape (c : Char) : Bool := c = idEndEscape
 
-private def findLeadingSpacesSize (s : String) : Nat :=
-  let it := s.iter
-  let it := it.find (· == '\n') |>.next
-  consumeSpaces it 0 s.length
-where
-  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
-    else if it.curr == '\n' then findNextLine it.next min
-    else findNextLine it.next (Nat.min curr min)
-  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
-    if it.atEnd then min
-    else if it.curr == '\n' then consumeSpaces it.next 0 min
-    else findNextLine it.next min
-
-private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
-  consumeSpaces n s.iter ""
-where
-  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
-     match n with
-     | 0 => saveLine it r
-     | n+1 =>
-       if it.atEnd then r
-       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
-       else saveLine it r
-  termination_by (it, 1)
-  saveLine (it : String.Iterator) (r : String) : String :=
-    if it.atEnd then r
-    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
-    else saveLine it.next (r.push it.curr)
-  termination_by (it, 0)
-
-def removeLeadingSpaces (s : String) : String :=
-  let n := findLeadingSpacesSize s
-  if n == 0 then s else removeNumLeadingSpaces n s
-
 namespace Name
 
 def getRoot : Name → Name
@@ -1298,11 +1261,6 @@ def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term
   let r ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
   `(($r : $type))
 
-def getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
-  match stx.raw[1] with
-  | Syntax.atom _ val => val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => ""
-
 end TSyntax
 
 namespace Meta
@@ -1364,9 +1322,7 @@ end Omega
 
 end Meta
 
-namespace Parser
-
-namespace Tactic
+namespace Parser.Tactic
 
 /-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`.
 This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`
@@ -1427,8 +1383,6 @@ This will rewrite with all equation lemmas, which can be used to
 partially evaluate many definitions. -/
 declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean.Meta.DSimp.Config) => { c with autoUnfold := true }
 
-end Tactic
-
-end Parser
+end Parser.Tactic
 
 end Lean

src/Init/Notation.lean

@@ -484,9 +484,6 @@ instance : Coe Syntax (TSyntax `rawStx) where
 /-- `with_annotate_term stx e` annotates the lexical range of `stx : Syntax` with term info for `e`. -/
 scoped syntax (name := withAnnotateTerm) "with_annotate_term " rawStx ppSpace term : term
 
-/-- Normalize casts in an expression using the same method as the `norm_cast` tactic. -/
-syntax (name := modCast) "mod_cast " term : term
-
 /--
 The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in
@@ -503,25 +500,6 @@ applications of this function as `↑` when printing expressions.
 -/
 syntax (name := Attr.coe) "coe" : attr
 
-/--
-This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
-
-* `@[command_code_action kind]`: This is a code action which applies to applications of the command
-  `kind` (a command syntax kind), which can replace the command or insert things before or after it.
-
-* `@[command_code_action kind₁ kind₂]`: shorthand for
-  `@[command_code_action kind₁, command_code_action kind₂]`.
-
-* `@[command_code_action]`: This is a command code action that applies to all commands.
-  Use sparingly.
--/
-syntax (name := command_code_action) "command_code_action" (ppSpace ident)* : attr
-
-/--
-Builtin command code action. See `command_code_action`.
--/
-syntax (name := builtin_command_code_action) "builtin_command_code_action" (ppSpace ident)* : attr
-
 /--
 When `parent_dir` contains the current Lean file, `include_str "path" / "to" / "file"` becomes
 a string literal with the contents of the file at `"parent_dir" / "path" / "to" / "file"`. If this
@@ -551,65 +529,3 @@ except that it doesn't print an empty diagnostic.
 (This is effectively a synonym for `run_elab`.)
 -/
 syntax (name := runMeta) "run_meta " doSeq : command
-
-/-- Element that can be part of a `#guard_msgs` specification. -/
-syntax guardMsgsSpecElt := &"drop"? (&"info" <|> &"warning" <|> &"error" <|> &"all")
-
-/-- Specification for `#guard_msgs` command. -/
-syntax guardMsgsSpec := "(" guardMsgsSpecElt,* ")"
-
-/--
-`#guard_msgs` captures the messages generated by another command and checks that they
-match the contents of the docstring attached to the `#guard_msgs` command.
-
-Basic example:
-```lean
-/--
-error: unknown identifier 'x'
--/
-#guard_msgs in
-example : α := x
-```
-This checks that there is such an error and then consumes the message entirely.
-
-By default, the command intercepts all messages, but there is a way to specify which types
-of messages to consider. For example, we can select only warnings:
-```lean
-/--
-warning: declaration uses 'sorry'
--/
-#guard_msgs(warning) in
-example : α := sorry
-```
-or only errors
-```lean
-#guard_msgs(error) in
-example : α := sorry
-```
-In this last example, since the message is not intercepted there is a warning on `sorry`.
-We can drop the warning completely with
-```lean
-#guard_msgs(error, drop warning) in
-example : α := sorry
-```
-
-Syntax description:
-```
-#guard_msgs (drop? info|warning|error|all,*)? in cmd
-```
-
-If there is no specification, `#guard_msgs` intercepts all messages.
-Otherwise, if there is one, the specification is considered in left-to-right order, and the first
-that applies chooses the outcome of the message:
-- `info`, `warning`, `error`: intercept a message with the given severity level.
-- `all`: intercept any message (so `#guard_msgs in cmd` and `#guard_msgs (all) in cmd`
-  are equivalent).
-- `drop info`, `drop warning`, `drop error`: intercept a message with the given severity
-  level and then drop it. These messages are not checked.
-- `drop all`: intercept a message and drop it.
-
-For example, `#guard_msgs (error, drop all) in cmd` means to check warnings and then drop
-everything else.
--/
-syntax (name := guardMsgsCmd)
-  (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command

src/Init/NotationExtra.lean

@@ -460,25 +460,3 @@ macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
   `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))
 
 end Lean
-
-syntax "{" term,+ "}" : term
-
-macro_rules
-  | `({$x:term}) => `(singleton $x)
-  | `({$x:term, $xs:term,*}) => `(insert $x {$xs:term,*})
-
-namespace Lean
-
-/-- Unexpander for the `{ x }` notation. -/
-@[app_unexpander singleton]
-def singletonUnexpander : Lean.PrettyPrinter.Unexpander
-  | `($_ $a) => `({ $a:term })
-  | _ => throw ()
-
-/-- Unexpander for the `{ x, y, ... }` notation. -/
-@[app_unexpander insert]
-def insertUnexpander : Lean.PrettyPrinter.Unexpander
-  | `($_ $a { $ts:term,* }) => `({$a:term, $ts,*})
-  | _ => throw ()
-
-end Lean

src/Init/Omega.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
--/
 prelude
 import Init.Omega.Int
 import Init.Omega.IntList

src/Init/Omega/Coeffs.lean

@@ -20,7 +20,7 @@ There is an equivalent file setting up `Coeffs` as a type synonym for `AssocList
 currently in a private branch.
 Not all the theorems about the algebraic operations on that representation have been proved yet.
 When they are ready, we can replace the implementation in `omega` simply by importing
-`Init.Omega.IntDict` instead of `Init.Omega.IntList`.
+`Std.Tactic.Omega.Coeffs.IntDict` instead of `Std.Tactic.Omega.Coeffs.IntList`.
 
 For small problems, the sparse representation is actually slightly slower,
 so it is not urgent to make this replacement.

src/Init/Omega/Int.lean

@@ -5,14 +5,12 @@ Authors: Scott Morrison
 -/
 prelude
 import Init.Data.Int.Order
-import Init.Data.Int.DivModLemmas
-import Init.Data.Nat.Lemmas
 
 /-!
-# Lemmas about `Nat`, `Int`, and `Fin` needed internally by `omega`.
+# Lemmas about `Nat` and `Int` needed internally by `omega`.
 
 These statements are useful for constructing proof expressions,
-but unlikely to be widely useful, so are inside the `Lean.Omega` namespace.
+but unlikely to be widely useful, so are inside the `Std.Tactic.Omega` namespace.
 
 If you do find a use for them, please move them into the appropriate file and namespace!
 -/
@@ -45,12 +43,6 @@ theorem ofNat_lt_of_lt {x y : Nat} (h : x < y) : (x : Int) < (y : Int) :=
 theorem ofNat_le_of_le {x y : Nat} (h : x ≤ y) : (x : Int) ≤ (y : Int) :=
   Int.ofNat_le.mpr h
 
-theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y : Nat) := by
-  simp [Nat.shiftLeft_eq]
-
-theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by
-  simp [Nat.shiftRight_eq_div_pow]
-
 -- FIXME these are insane:
 theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
 theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
@@ -163,38 +155,6 @@ theorem le_of_ge {x y : Nat} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h
 
 end Nat
 
-namespace Fin
-
-theorem ne_iff_lt_or_gt {i j : Fin n} : i ≠ j ↔ i < j ∨ i > j := by
-  cases i; cases j; simp only [ne_eq, Fin.mk.injEq, Nat.ne_iff_lt_or_gt, gt_iff_lt]; rfl
-
-protected theorem lt_or_gt_of_ne {i j : Fin n} (h : i ≠ j) : i < j ∨ i > j := Fin.ne_iff_lt_or_gt.mp h
-
-theorem not_le {i j : Fin n} : ¬ i ≤ j ↔ j < i := by
-  cases i; cases j; exact Nat.not_le
-
-theorem not_lt {i j : Fin n} : ¬ i < j ↔ j ≤ i := by
-  cases i; cases j; exact Nat.not_lt
-
-protected theorem lt_of_not_le {i j : Fin n} (h : ¬ i ≤ j) : j < i := Fin.not_le.mp h
-protected theorem le_of_not_lt {i j : Fin n} (h : ¬ i < j) : j ≤ i := Fin.not_lt.mp h
-
-theorem ofNat_val_add {x y : Fin n} :
-    (((x + y : Fin n)) : Int) = ((x : Int) + (y : Int)) % n := rfl
-
-theorem ofNat_val_sub {x y : Fin n} :
-    (((x - y : Fin n)) : Int) = ((x : Int) + ((n - y : Nat) : Int)) % n := rfl
-
-theorem ofNat_val_mul {x y : Fin n} :
-    (((x * y : Fin n)) : Int) = ((x : Int) * (y : Int)) % n := rfl
-
-theorem ofNat_val_natCast {n x y : Nat} (h : y = x % (n + 1)):
-    @Nat.cast Int instNatCastInt (@Fin.val (n + 1) (OfNat.ofNat x)) = OfNat.ofNat y := by
-  rw [h]
-  rfl
-
-end Fin
-
 namespace Prod
 
 theorem of_lex (w : Prod.Lex r s p q) : r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd :=

src/Init/Omega/Logic.lean

@@ -9,7 +9,7 @@ import Init.PropLemmas
 # Specializations of basic logic lemmas
 
 These are useful for `omega` while constructing proofs, but not considered generally useful
-so are hidden in the `Lean.Omega` namespace.
+so are hidden in the `Std.Tactic.Omega` namespace.
 
 If you find yourself needing them elsewhere, please move them first to another file.
 -/

src/Init/Prelude.lean

@@ -947,8 +947,7 @@ return `t` or `e` depending on whether `c` is true or false. The explicit argume
 determines how to evaluate `c` to true or false. Write `if h : c then t else e`
 instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
 that `c` is true/false.
--/
-/-
+
 Because Lean uses a strict (call-by-value) evaluation strategy, the signature of this
 function is problematic in that it would require `t` and `e` to be evaluated before
 calling the `ite` function, which would cause both sides of the `if` to be evaluated.
@@ -1815,8 +1814,6 @@ structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.2` is a proof that `i.1 < n`. -/
   isLt : LT.lt val n
 
-attribute [coe] Fin.val
-
 theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
@@ -2381,9 +2378,6 @@ Codepoint positions (counting the Unicode codepoints rather than bytes)
 are represented by plain `Nat`s instead.
 Indexing a `String` by a byte position is constant-time, while codepoint
 positions need to be translated internally to byte positions in linear-time.
-
-A byte position `p` is *valid* for a string `s` if `0 ≤ p ≤ s.endPos` and `p`
-lies on a UTF8 byte boundary.
 -/
 structure String.Pos where
   /-- Get the underlying byte index of a `String.Pos` -/

src/Init/PropLemmas.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Copyright (c) 2024 Lean FRO.  All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Mario Carneiro
 

src/Init/SimpLemmas.lean

@@ -84,7 +84,6 @@ theorem dite_congr {_ : Decidable b} [Decidable c]
   | inr h => rw [dif_neg h]; subst b; rw [dif_neg h]; exact h₃ h
 
 @[simp] theorem ne_eq (a b : α) : (a ≠ b) = ¬(a = b) := rfl
-norm_cast_add_elim ne_eq
 @[simp] theorem ite_true (a b : α) : (if True then a else b) = a := rfl
 @[simp] theorem ite_false (a b : α) : (if False then a else b) = b := rfl
 @[simp] theorem dite_true {α : Sort u} {t : True → α} {e : ¬ True → α} : (dite True t e) = t True.intro := rfl

src/Init/System/Uri.lean

@@ -5,7 +5,6 @@ Authors: Chris Lovett
 -/
 prelude
 import Init.Data.String.Extra
-import Init.Data.Nat.Linear
 import Init.System.FilePath
 
 namespace System

src/Init/Tactics.lean

@@ -584,43 +584,6 @@ def dsimpArg := simpErase.binary `orelse simpLemma
 /-- A dsimp args list is a list of `dsimpArg`. This is the main argument to `dsimp`. -/
 syntax dsimpArgs := " [" dsimpArg,* "]"
 
-/-- The common arguments of `simp?` and `simp?!`. -/
-syntax simpTraceArgsRest := (config)? (discharger)? (&" only")? (simpArgs)? (ppSpace location)?
-
-/--
-`simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
-that would be sufficient to close the goal. This is useful for reducing the size of the simp
-set in a local invocation to speed up processing.
-```
-example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
-  simp? -- prints "Try this: simp only [ite_true]"
-```
-
-This command can also be used in `simp_all` and `dsimp`.
--/
-syntax (name := simpTrace) "simp?" "!"? simpTraceArgsRest : tactic
-
-@[inherit_doc simpTrace]
-macro tk:"simp?!" rest:simpTraceArgsRest : tactic => `(tactic| simp?%$tk ! $rest)
-
-/-- The common arguments of `simp_all?` and `simp_all?!`. -/
-syntax simpAllTraceArgsRest := (config)? (discharger)? (&" only")? (dsimpArgs)?
-
-@[inherit_doc simpTrace]
-syntax (name := simpAllTrace) "simp_all?" "!"? simpAllTraceArgsRest : tactic
-
-@[inherit_doc simpTrace]
-macro tk:"simp_all?!" rest:simpAllTraceArgsRest : tactic => `(tactic| simp_all?%$tk ! $rest)
-
-/-- The common arguments of `dsimp?` and `dsimp?!`. -/
-syntax dsimpTraceArgsRest := (config)? (&" only")? (dsimpArgs)? (ppSpace location)?
-
-@[inherit_doc simpTrace]
-syntax (name := dsimpTrace) "dsimp?" "!"? dsimpTraceArgsRest : tactic
-
-@[inherit_doc simpTrace]
-macro tk:"dsimp?!" rest:dsimpTraceArgsRest : tactic => `(tactic| dsimp?%$tk ! $rest)
-
 /-- The arguments to the `simpa` family tactics. -/
 syntax simpaArgsRest := (config)? (discharger)? &" only "? (simpArgs)? (" using " term)?
 
@@ -1055,6 +1018,7 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
 macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
 
+
 /--
 The `omega` tactic, for resolving integer and natural linear arithmetic problems.
 
@@ -1088,224 +1052,6 @@ Currently, all of these are on by default.
 -/
 syntax (name := omega) "omega" (config)? : tactic
 
-/--
-`bv_omega` is `omega` with an additional preprocessor that turns statements about `BitVec` into statements about `Nat`.
-Currently the preprocessor is implemented as `try simp only [bv_toNat] at *`.
-`bv_toNat` is a `@[simp]` attribute that you can (cautiously) add to more theorems.
--/
-macro "bv_omega" : tactic => `(tactic| (try simp only [bv_toNat] at *) <;> omega)
-
-/-- Implementation of `norm_cast` (the full `norm_cast` calls `trivial` afterwards). -/
-syntax (name := normCast0) "norm_cast0" (location)? : tactic
-
-/-- `assumption_mod_cast` is a variant of `assumption` that solves the goal
-using a hypothesis. Unlike `assumption`, it first pre-processes the goal and
-each hypothesis to move casts as far outwards as possible, so it can be used
-in more situations.
-
-Concretely, it runs `norm_cast` on the goal. For each local hypothesis `h`, it also
-normalizes `h` with `norm_cast` and tries to use that to close the goal. -/
-macro "assumption_mod_cast" : tactic => `(tactic| norm_cast0 at * <;> assumption)
-
-/--
-The `norm_cast` family of tactics is used to normalize casts inside expressions.
-It is basically a `simp` tactic with a specific set of lemmas to move casts
-upwards in the expression.
-Therefore even in situations where non-terminal `simp` calls are discouraged (because of fragility),
-`norm_cast` is considered safe.
-It also has special handling of numerals.
-
-For instance, given an assumption
-```lean
-a b : ℤ
-h : ↑a + ↑b < (10 : ℚ)
-```
-
-writing `norm_cast at h` will turn `h` into
-```lean
-h : a + b < 10
-```
-
-There are also variants of `exact`, `apply`, `rw`, and `assumption` that
-work modulo `norm_cast` - in other words, they apply `norm_cast` to make
-them more flexible. They are called `exact_mod_cast`, `apply_mod_cast`,
-`rw_mod_cast`, and `assumption_mod_cast`, respectively.
-Writing `exact_mod_cast h` and `apply_mod_cast h` will normalize casts
-in the goal and `h` before using `exact h` or `apply h`.
-Writing `assumption_mod_cast` will normalize casts in the goal and, for
-every hypothesis `h` in the context, it will try to normalize casts in `h` and use
-`exact h`.
-`rw_mod_cast` acts like the `rw` tactic but it applies `norm_cast` between steps.
-
-See also `push_cast`, which moves casts inwards rather than lifting them outwards.
--/
-macro "norm_cast" loc:(location)? : tactic =>
-  `(tactic| norm_cast0 $[$loc]? <;> try trivial)
-
-/--
-`push_cast` rewrites the goal to move casts inward, toward the leaf nodes.
-This uses `norm_cast` lemmas in the forward direction.
-For example, `↑(a + b)` will be written to `↑a + ↑b`.
-It is equivalent to `simp only with push_cast`.
-It can also be used at hypotheses with `push_cast at h`
-and with extra simp lemmas with `push_cast [int.add_zero]`.
-
-```lean
-example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
-  ((a + b : ℕ) : ℤ) = 10 :=
-begin
-  push_cast,
-  push_cast at h1,
-  push_cast [int.add_zero] at h2,
-end
-```
--/
-syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
-  (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
-
-/--
-`norm_cast_add_elim foo` registers `foo` as an elim-lemma in `norm_cast`.
--/
-syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
-
-/--
-* `symm` applies to a goal whose target has the form `t ~ u` where `~` is a symmetric relation,
-  that is, a relation which has a symmetry lemma tagged with the attribute [symm].
-  It replaces the target with `u ~ t`.
-* `symm at h` will rewrite a hypothesis `h : t ~ u` to `h : u ~ t`.
--/
-syntax (name := symm) "symm" (location)? : tactic
-
-/-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
-add a hypothesis `h_symm : b ~ a`. -/
-syntax (name := symmSaturate) "symm_saturate" : tactic
-
-namespace SolveByElim
-
-/-- Syntax for omitting a local hypothesis in `solve_by_elim`. -/
-syntax erase := "-" term:max
-/-- Syntax for including all local hypotheses in `solve_by_elim`. -/
-syntax star := "*"
-/-- Syntax for adding or removing a term, or `*`, in `solve_by_elim`. -/
-syntax arg := star <|> erase <|> term
-/-- Syntax for adding and removing terms in `solve_by_elim`. -/
-syntax args := " [" SolveByElim.arg,* "]"
-/-- Syntax for using all lemmas labelled with an attribute in `solve_by_elim`. -/
-syntax using_ := " using " ident,*
-
-end SolveByElim
-
-section SolveByElim
-open SolveByElim (args using_)
-
-/--
-`solve_by_elim` calls `apply` on the main goal to find an assumption whose head matches
-and then repeatedly calls `apply` on the generated subgoals until no subgoals remain,
-performing at most `maxDepth` (defaults to 6) recursive steps.
-
-`solve_by_elim` discharges the current goal or fails.
-
-`solve_by_elim` performs backtracking if subgoals can not be solved.
-
-By default, the assumptions passed to `apply` are the local context, `rfl`, `trivial`,
-`congrFun` and `congrArg`.
-
-The assumptions can be modified with similar syntax as for `simp`:
-* `solve_by_elim [h₁, h₂, ..., hᵣ]` also applies the given expressions.
-* `solve_by_elim only [h₁, h₂, ..., hᵣ]` does not include the local context,
-  `rfl`, `trivial`, `congrFun`, or `congrArg` unless they are explicitly included.
-* `solve_by_elim [-h₁, ... -hₙ]` removes the given local hypotheses.
-* `solve_by_elim using [a₁, ...]` uses all lemmas which have been labelled
-  with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).
-
-`solve_by_elim*` tries to solve all goals together, using backtracking if a solution for one goal
-makes other goals impossible.
-(Adding or removing local hypotheses may not be well-behaved when starting with multiple goals.)
-
-Optional arguments passed via a configuration argument as `solve_by_elim (config := { ... })`
-- `maxDepth`: number of attempts at discharging generated subgoals
-- `symm`: adds all hypotheses derived by `symm` (defaults to `true`).
-- `exfalso`: allow calling `exfalso` and trying again if `solve_by_elim` fails
-  (defaults to `true`).
-- `transparency`: change the transparency mode when calling `apply`. Defaults to `.default`,
-  but it is often useful to change to `.reducible`,
-  so semireducible definitions will not be unfolded when trying to apply a lemma.
-
-See also the doc-comment for `Std.Tactic.BacktrackConfig` for the options
-`proc`, `suspend`, and `discharge` which allow further customization of `solve_by_elim`.
-Both `apply_assumption` and `apply_rules` are implemented via these hooks.
--/
-syntax (name := solveByElim)
-  "solve_by_elim" "*"? (config)? (&" only")? (args)? (using_)? : tactic
-
-/--
-`apply_assumption` looks for an assumption of the form `... → ∀ _, ... → head`
-where `head` matches the current goal.
-
-You can specify additional rules to apply using `apply_assumption [...]`.
-By default `apply_assumption` will also try `rfl`, `trivial`, `congrFun`, and `congrArg`.
-If you don't want these, or don't want to use all hypotheses, use `apply_assumption only [...]`.
-You can use `apply_assumption [-h]` to omit a local hypothesis.
-You can use `apply_assumption using [a₁, ...]` to use all lemmas which have been labelled
-with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).
-
-`apply_assumption` will use consequences of local hypotheses obtained via `symm`.
-
-If `apply_assumption` fails, it will call `exfalso` and try again.
-Thus if there is an assumption of the form `P → ¬ Q`, the new tactic state
-will have two goals, `P` and `Q`.
-
-You can pass a further configuration via the syntax `apply_rules (config := {...}) lemmas`.
-The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
--/
-syntax (name := applyAssumption)
-  "apply_assumption" (config)? (&" only")? (args)? (using_)? : tactic
-
-/--
-`apply_rules [l₁, l₂, ...]` tries to solve the main goal by iteratively
-applying the list of lemmas `[l₁, l₂, ...]` or by applying a local hypothesis.
-If `apply` generates new goals, `apply_rules` iteratively tries to solve those goals.
-You can use `apply_rules [-h]` to omit a local hypothesis.
-
-`apply_rules` will also use `rfl`, `trivial`, `congrFun` and `congrArg`.
-These can be disabled, as can local hypotheses, by using `apply_rules only [...]`.
-
-You can use `apply_rules using [a₁, ...]` to use all lemmas which have been labelled
-with the attributes `aᵢ` (these attributes must be created using `register_label_attr`).
-
-You can pass a further configuration via the syntax `apply_rules (config := {...})`.
-The options supported are the same as for `solve_by_elim` (and include all the options for `apply`).
-
-`apply_rules` will try calling `symm` on hypotheses and `exfalso` on the goal as needed.
-This can be disabled with `apply_rules (config := {symm := false, exfalso := false})`.
-
-You can bound the iteration depth using the syntax `apply_rules (config := {maxDepth := n})`.
-
-Unlike `solve_by_elim`, `apply_rules` does not perform backtracking, and greedily applies
-a lemma from the list until it gets stuck.
--/
-syntax (name := applyRules) "apply_rules" (config)? (&" only")? (args)? (using_)? : tactic
-end SolveByElim
-
-/--
-Searches environment for definitions or theorems that can solve the goal using `exact`
-with conditions resolved by `solve_by_elim`.
-
-The optional `using` clause provides identifiers in the local context that must be
-used by `exact?` when closing the goal.  This is most useful if there are multiple
-ways to resolve the goal, and one wants to guide which lemma is used.
--/
-syntax (name := exact?) "exact?" (" using " (colGt ident),+)? : tactic
-
-/--
-Searches environment for definitions or theorems that can refine the goal using `apply`
-with conditions resolved when possible with `solve_by_elim`.
-
-The optional `using` clause provides identifiers in the local context that must be
-used when closing the goal.
--/
-syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
-
 end Tactic
 
 namespace Attr
@@ -1353,59 +1099,6 @@ If there are several with the same priority, it is uses the "most recent one". E
 ```
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
-
-
-/-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
-syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
-
-/--
-The `norm_cast` attribute should be given to lemmas that describe the
-behaviour of a coercion with respect to an operator, a relation, or a particular
-function.
-
-It only concerns equality or iff lemmas involving `↑`, `⇑` and `↥`, describing the behavior of
-the coercion functions.
-It does not apply to the explicit functions that define the coercions.
-
-Examples:
-```lean
-@[norm_cast] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n
-
-@[norm_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1
-
-@[norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
-
-@[norm_cast] theorem coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n
-
-@[norm_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n
-
-@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
-```
-
-Lemmas tagged with `@[norm_cast]` are classified into three categories: `move`, `elim`, and
-`squash`. They are classified roughly as follows:
-
-* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
-* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
-* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
-
-`norm_cast` uses `move` and `elim` lemmas to factor coercions toward the root of an expression
-and to cancel them from both sides of an equation or relation. It uses `squash` lemmas to clean
-up the result.
-
-It is typically not necessary to specify these categories, as `norm_cast` lemmas are
-automatically classified by default. The automatic classification can be overridden by
-giving an optional `elim`, `move`, or `squash` parameter to the attribute.
-
-```lean
-@[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n := by
-  rw [← of_real_nat_cast, of_real_re]
-```
-
-Don't do this unless you understand what you are doing.
--/
-syntax (name := norm_cast) "norm_cast" (ppSpace normCastLabel)? (ppSpace num)? : attr
-
 end Attr
 
 end Parser
@@ -1457,9 +1150,3 @@ macro_rules | `($x[$i]) => `(getElem $x $i (by get_elem_tactic))
 @[inherit_doc getElem]
 syntax term noWs "[" withoutPosition(term) "]'" term:max : term
 macro_rules | `($x[$i]'$h) => `(getElem $x $i $h)
-
-/--
-Searches environment for definitions or theorems that can be substituted in
-for `exact?% to solve the goal.
- -/
-syntax (name := Lean.Parser.Syntax.exact?) "exact?%" : term

src/Init/TacticsExtra.lean

@@ -63,24 +63,4 @@ macro_rules
     | 0 => `(tactic| skip)
     | n+1 => `(tactic| ($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq)
 
-/--
-Rewrites with the given rules, normalizing casts prior to each step.
--/
-syntax "rw_mod_cast" (config)? rwRuleSeq (location)? : tactic
-macro_rules
-  | `(tactic| rw_mod_cast $[$config]? [$rules,*] $[$loc]?) => do
-    let tacs ← rules.getElems.mapM fun rule =>
-      `(tactic| (norm_cast at *; rw $[$config]? [$rule] $[$loc]?))
-    `(tactic| ($[$tacs]*))
-
-/--
-Normalize casts in the goal and the given expression, then close the goal with `exact`.
--/
-macro "exact_mod_cast " e:term : tactic => `(tactic| exact mod_cast ($e : _))
-
-/--
-Normalize casts in the goal and the given expression, then `apply` the expression to the goal.
--/
-macro "apply_mod_cast " e:term : tactic => `(tactic| apply mod_cast ($e : _))
-
 end Lean.Parser.Tactic

src/Lean.lean

@@ -35,4 +35,3 @@ import Lean.Widget
 import Lean.Log
 import Lean.Linter
 import Lean.SubExpr
-import Lean.LabelAttribute

src/Lean/Data/Json/Basic.lean

@@ -8,7 +8,6 @@ prelude
 import Init.Data.List.Control
 import Init.Data.Range
 import Init.Data.OfScientific
-import Init.Data.Hashable
 import Lean.Data.RBMap
 namespace Lean
 
@@ -16,7 +15,7 @@ namespace Lean
 structure JsonNumber where
   mantissa : Int
   exponent : Nat
-  deriving DecidableEq, Hashable
+  deriving DecidableEq
 
 namespace JsonNumber
 
@@ -206,19 +205,6 @@ private partial def beq' : Json → Json → Bool
 instance : BEq Json where
   beq := beq'
 
-private partial def hash' : Json → UInt64
-  | null   => 11
-  | bool b => mixHash 13 <| hash b
-  | num n  => mixHash 17 <| hash n
-  | str s  => mixHash 19 <| hash s
-  | arr elems =>
-    mixHash 23 <| elems.foldl (init := 7) fun r a => mixHash r (hash' a)
-  | obj kvPairs =>
-    mixHash 29 <| kvPairs.fold (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v)
-
-instance : Hashable Json where
-  hash := hash'
-
 -- HACK(Marc): temporary ugliness until we can use RBMap for JSON objects
 def mkObj (o : List (String × Json)) : Json :=
   obj <| Id.run do

src/Lean/Data/Json/Elab.lean

@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2022 E.W.Ayers. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: E.W.Ayers, Wojciech Nawrocki
+ Copyright (c) 2022 E.W.Ayers. All rights reserved.
+ Released under Apache 2.0 license as described in the file LICENSE.
+ Authors: E.W.Ayers, Wojciech Nawrocki
 -/
 prelude
 import Lean.Data.Json.FromToJson

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -47,19 +47,19 @@ structure CompletionItem where
   documentation? : Option MarkupContent := none
   kind?          : Option CompletionItemKind := none
   textEdit?      : Option InsertReplaceEdit := none
-  sortText?      : Option String := none
-  data?          : Option Json := none
   /-
   tags? : CompletionItemTag[]
   deprecated? : boolean
   preselect? : boolean
+  sortText? : string
   filterText? : string
   insertText? : string
   insertTextFormat? : InsertTextFormat
   insertTextMode? : InsertTextMode
   additionalTextEdits? : TextEdit[]
   commitCharacters? : string[]
-  command? : Command -/
+  command? : Command
+  data? : any -/
   deriving FromJson, ToJson, Inhabited
 
 structure CompletionList where
@@ -274,7 +274,7 @@ structure CallHierarchyItem where
   uri            : DocumentUri
   range          : Range
   selectionRange : Range
-  data?          : Option Json := none
+  -- data? : Option unknown
   deriving FromJson, ToJson, BEq, Hashable, Inhabited
 
 structure CallHierarchyIncomingCallsParams where

src/Lean/Data/Lsp/Utf16.lean

@@ -86,10 +86,6 @@ def leanPosToLspPos (text : FileMap) : Lean.Position → Lsp.Position
 def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
   text.leanPosToLspPos (text.toPosition pos)
 
-/-- Gets the LSP range from a `String.Range`. -/
-def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
-  { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
-
 end FileMap
 end Lean
 

src/Lean/Data/RBMap.lean

@@ -5,8 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Ord
-import Init.Data.Nat.Linear
-
 namespace Lean
 universe u v w w'
 

src/Lean/Data/Xml.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2021 Daniel Fabian. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Daniel Fabian
--/
 prelude
 import Lean.Data.Xml.Basic
 import Lean.Data.Xml.Parser

src/Lean/Data/Xml/Basic.lean

@@ -1,3 +1,4 @@
+
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -37,3 +38,4 @@ private partial def cToString : Content → String
 end
 instance : ToString Element := ⟨eToString⟩
 instance : ToString Content := ⟨cToString⟩
+

src/Lean/DocString.lean

@@ -12,6 +12,42 @@ namespace Lean
 private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {}
 private builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension
 
+private def findLeadingSpacesSize (s : String) : Nat :=
+  let it := s.iter
+  let it := it.find (· == '\n') |>.next
+  consumeSpaces it 0 s.length
+where
+  consumeSpaces (it : String.Iterator) (curr min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == ' ' || it.curr == '\t' then consumeSpaces it.next (curr + 1) min
+    else if it.curr == '\n' then findNextLine it.next min
+    else findNextLine it.next (Nat.min curr min)
+  findNextLine (it : String.Iterator) (min : Nat) : Nat :=
+    if it.atEnd then min
+    else if it.curr == '\n' then consumeSpaces it.next 0 min
+    else findNextLine it.next min
+
+private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
+  consumeSpaces n s.iter ""
+where
+  consumeSpaces (n : Nat) (it : String.Iterator) (r : String) : String :=
+     match n with
+     | 0 => saveLine it r
+     | n+1 =>
+       if it.atEnd then r
+       else if it.curr == ' ' || it.curr == '\t' then consumeSpaces n it.next r
+       else saveLine it r
+  termination_by (it, 1)
+  saveLine (it : String.Iterator) (r : String) : String :=
+    if it.atEnd then r
+    else if it.curr == '\n' then consumeSpaces n it.next (r.push '\n')
+    else saveLine it.next (r.push it.curr)
+  termination_by (it, 0)
+
+def removeLeadingSpaces (s : String) : String :=
+  let n := findLeadingSpacesSize s
+  if n == 0 then s else removeNumLeadingSpaces n s
+
 def addBuiltinDocString (declName : Name) (docString : String) : IO Unit :=
   builtinDocStrings.modify (·.insert declName (removeLeadingSpaces docString))
 
@@ -55,4 +91,9 @@ def getDocStringText [Monad m] [MonadError m] [MonadRef m] (stx : TSyntax `Lean.
   | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
   | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
 
+def TSyntax.getDocString (stx : TSyntax `Lean.Parser.Command.docComment) : String :=
+  match stx.raw[1] with
+  | Syntax.atom _ val => val.extract 0 (val.endPos - ⟨2⟩)
+  | _                 => ""
+
 end Lean

src/Lean/Elab.lean

@@ -47,4 +47,3 @@ import Lean.Elab.Eval
 import Lean.Elab.Calc
 import Lean.Elab.InheritDoc
 import Lean.Elab.ParseImportsFast
-import Lean.Elab.GuardMsgs

src/Lean/Elab/BuiltinCommand.lean

@@ -534,10 +534,10 @@ open Meta
 def elabCheckCore (ignoreStuckTC : Bool) : CommandElab
   | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do
     -- show signature for `#check id`/`#check @id`
-    if let `($id:ident) := term then
+    if let `($_:ident) := term then
       try
         for c in (← resolveGlobalConstWithInfos term) do
-          addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
+          addCompletionInfo <| .id term c (danglingDot := false) {} none
           logInfoAt tk <| .ofPPFormat { pp := fun
             | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
             | none     => return f!"{c}"  -- should never happen

src/Lean/Elab/BuiltinTerm.lean

@@ -158,10 +158,7 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
 @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
 
-@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun stx expectedType? => do
-  if stx[0].getAtomVal == "." then
-    -- Users may input bad cdots because they are trying to auto-complete them using the expected type
-    addCompletionInfo <| CompletionInfo.dotId stx .anonymous (← getLCtx) expectedType?
+@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun _ _ =>
   throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
 
 @[builtin_term_elab str] def elabStrLit : TermElab := fun stx _ => do

src/Lean/Elab/Declaration.lean

@@ -347,21 +347,7 @@ def elabMutual : CommandElab := fun stx => do
   let attrs ← elabAttrs attrInsts
   let idents := stx[4].getArgs
   for ident in idents do withRef ident <| liftTermElabM do
-    /-
-    HACK to allow `attribute` command to disable builtin simprocs.
-    TODO: find a better solution. Example: have some "fake" declaration
-    for builtin simprocs.
-    -/
-    let declNames ←
-       try
-         resolveGlobalConst ident
-       catch _ =>
-         let name := ident.getId.eraseMacroScopes
-         if (← Simp.isBuiltinSimproc name) then
-           pure [name]
-         else
-           throwUnknownConstant name
-    let declName ← ensureNonAmbiguous ident declNames
+    let declName ← resolveGlobalConstNoOverloadWithInfo ident
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName

src/Lean/Elab/GuardMsgs.lean

@@ -1,136 +0,0 @@
-/-
-Copyright (c) 2023 Kyle Miller. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
--/
-prelude
-import Lean.Server.CodeActions.Attr
-
-/-! `#guard_msgs` command for testing commands
-
-This module defines a command to test that another command produces the expected messages.
-See the docstring on the `#guard_msgs` command.
--/
-
-open Lean Parser.Tactic Elab Command
-
-namespace Lean.Elab.Tactic.GuardMsgs
-
-/-- Gives a string representation of a message without source position information.
-Ensures the message ends with a '\n'. -/
-private def messageToStringWithoutPos (msg : Message) : IO String := do
-  let mut str ← msg.data.toString
-  unless msg.caption == "" do
-    str := msg.caption ++ ":\n" ++ str
-  if !("\n".isPrefixOf str) then str := " " ++ str
-  match msg.severity with
-  | MessageSeverity.information => str := "info:" ++ str
-  | MessageSeverity.warning     => str := "warning:" ++ str
-  | MessageSeverity.error       => str := "error:" ++ str
-  if str.isEmpty || str.back != '\n' then
-    str := str ++ "\n"
-  return str
-
-/-- The decision made by a specification for a message. -/
-inductive SpecResult
-  /-- Capture the message and check it matches the docstring. -/
-  | check
-  /-- Drop the message and delete it. -/
-  | drop
-  /-- Do not capture the message. -/
-  | passthrough
-
-/-- Parses a `guardMsgsSpec`.
-- No specification: check everything.
-- With a specification: interpret the spec, and if nothing applies pass it through. -/
-def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) :
-    CommandElabM (Message → SpecResult) := do
-  if let some spec := spec? then
-    match spec with
-    | `(guardMsgsSpec| ($[$elts:guardMsgsSpecElt],*)) => do
-      let mut p : Message → SpecResult := fun _ => .passthrough
-      let pushP (s : MessageSeverity) (drop : Bool) (p : Message → SpecResult)
-          (msg : Message) : SpecResult :=
-        if msg.severity == s then if drop then .drop else .check
-        else p msg
-      for elt in elts.reverse do
-        match elt with
-        | `(guardMsgsSpecElt| $[drop%$drop?]? info)    => p := pushP .information drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? warning) => p := pushP .warning drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? error)   => p := pushP .error drop?.isSome p
-        | `(guardMsgsSpecElt| $[drop%$drop?]? all) =>
-          p := fun _ => if drop?.isSome then .drop else .check
-        | _ => throwErrorAt elt "Invalid #guard_msgs specification element"
-      return p
-    | _ => throwErrorAt spec "Invalid #guard_msgs specification"
-  else
-    return fun _ => .check
-
-/-- An info tree node corresponding to a failed `#guard_msgs` invocation,
-used for code action support. -/
-structure GuardMsgFailure where
-  /-- The result of the nested command -/
-  res : String
-deriving TypeName
-
-@[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
-  | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
-    let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trim
-    let specFn ← parseGuardMsgsSpec spec?
-    let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
-    elabCommandTopLevel cmd
-    let msgs := (← get).messages
-    let mut toCheck : MessageLog := .empty
-    let mut toPassthrough : MessageLog := .empty
-    for msg in msgs.toList do
-      match specFn msg with
-      | .check       => toCheck := toCheck.add msg
-      | .drop        => pure ()
-      | .passthrough => toPassthrough := toPassthrough.add msg
-    let res := "---\n".intercalate (← toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
-    -- We do some whitespace normalization here to allow users to break long lines.
-    if expected.replace "\n" " " == res.replace "\n" " " then
-      -- Passed. Only put toPassthrough messages back on the message log
-      modify fun st => { st with messages := initMsgs ++ toPassthrough }
-    else
-      -- Failed. Put all the messages back on the message log and add an error
-      modify fun st => { st with messages := initMsgs ++ msgs }
-      logErrorAt tk m!"❌ Docstring on `#guard_msgs` does not match generated message:\n\n{res}"
-      pushInfoLeaf (.ofCustomInfo { stx := ← getRef, value := Dynamic.mk (GuardMsgFailure.mk res) })
-  | _ => throwUnsupportedSyntax
-
-open CodeAction Server RequestM in
-/-- A code action which will update the doc comment on a `#guard_msgs` invocation. -/
-@[builtin_command_code_action guardMsgsCmd]
-def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
-  let .node _ ts := node | return #[]
-  let res := ts.findSome? fun
-    | .node (.ofCustomInfo { stx, value }) _ => return (stx, (← value.get? GuardMsgFailure).res)
-    | _ => none
-  let some (stx, res) := res | return #[]
-  let doc ← readDoc
-  let eager := {
-    title := "Update #guard_msgs with tactic output"
-    kind? := "quickfix"
-    isPreferred? := true
-  }
-  pure #[{
-    eager
-    lazy? := some do
-      let some start := stx.getPos? true | return eager
-      let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager
-      let newText := if res.isEmpty then
-        ""
-      else if res.length ≤ 100-7 && !res.contains '\n' then -- TODO: configurable line length?
-        s!"/-- {res} -/\n"
-      else
-        s!"/--\n{res}\n-/\n"
-      pure { eager with
-        edit? := some <|.ofTextEdit doc.versionedIdentifier {
-          range := doc.meta.text.utf8RangeToLspRange ⟨start, tail⟩
-          newText
-        }
-      }
-  }]
-
-end Lean.Elab.Tactic.GuardMsgs

src/Lean/Elab/InfoTree/Main.lean

@@ -49,25 +49,14 @@ def PartialContextInfo.mergeIntoOuter?
     some { outer with parentDecl? := innerParentDecl }
 
 def CompletionInfo.stx : CompletionInfo → Syntax
-  | dot i ..          => i.stx
-  | id stx ..         => stx
-  | dotId stx ..      => stx
-  | fieldId stx ..    => stx
-  | namespaceId stx   => stx
-  | option stx        => stx
+  | dot i .. => i.stx
+  | id stx .. => stx
+  | dotId stx .. => stx
+  | fieldId stx .. => stx
+  | namespaceId stx => stx
+  | option stx => stx
   | endSection stx .. => stx
-  | tactic stx ..     => stx
-
-/--
-Obtains the `LocalContext` from this `CompletionInfo` if available and yields an empty context
-otherwise.
--/
-def CompletionInfo.lctx : CompletionInfo → LocalContext
-  | dot i ..            => i.lctx
-  | id _ _ _ lctx ..    => lctx
-  | dotId _ _ lctx ..   => lctx
-  | fieldId _ _ lctx .. => lctx
-  | _                   => .empty
+  | tactic stx .. => stx
 
 def CustomInfo.format : CustomInfo → Format
   | i => f!"CustomInfo({i.value.typeName})"

src/Lean/Elab/Match.lean

@@ -473,7 +473,7 @@ partial def normalize (e : Expr) : M Expr := do
         let p ← normalize p
         addVar h
         return mkApp4 e.getAppFn (e.getArg! 0) x p h
-      else if (← isMatchValue e) then
+      else if isMatchValue e then
         return e
       else if e.isFVar then
         if (← isExplicitPatternVar e) then
@@ -571,8 +571,8 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
         | _,           _           => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
-      else if (← isMatchValue e) then
-        return Pattern.val (← normLitValue e)
+      else if isMatchValue e then
+        return Pattern.val e
       else if e.isFVar then
         return Pattern.var e.fvarId!
       else

src/Lean/Elab/MutualDef.lean

@@ -214,7 +214,7 @@ private def expandWhereStructInst : Macro
         `(structInstField|$id:ident := $val)
       | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
       | _ => Macro.throwUnsupported
-    let body ← `(structInst| { $structInstFields,* })
+    let body ← `({ $structInstFields,* })
     match whereDecls? with
     | some whereDecls => expandWhereDecls whereDecls body
     | none => return body

src/Lean/Elab/Notation.lean

@@ -107,10 +107,22 @@ def mkUnexpander (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Mac
   -- The reference is attached to the syntactic representation of the called function itself, not the entire function application
   let lhs ← `($$f:ident)
   let lhs := Syntax.mkApp lhs (.mk args)
+  -- allow over-application, avoiding nested `app` nodes
+  let lhsWithMoreArgs := flattenApp (← `($lhs $$moreArgs*))
+  let patWithMoreArgs := flattenApp (← `($pat $$moreArgs*))
   `(@[$attrKind app_unexpander $(mkIdent c)]
     aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
       | `($lhs)             => withRef f `($pat)
+      -- must be a separate case as the LHS and RHS above might not be `app` nodes
+      | `($lhsWithMoreArgs) => withRef f `($patWithMoreArgs)
       | _                   => throw ())
+where
+  -- NOTE: we consider only one nesting level here
+  flattenApp : Term → Term
+    | stx@`($f $xs*) => match f with
+      | `($f' $xs'*) => Syntax.mkApp f' (xs' ++ xs)
+      | _            => stx
+    | stx            => stx
 
 private def expandNotationAux (ref : Syntax) (currNamespace : Name)
     (doc? : Option (TSyntax ``docComment))

src/Lean/Elab/PatternVar.lean

@@ -159,19 +159,6 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
     discard <| processVar h
     ``(_root_.namedPattern $id $pat $h)
   else if k == ``Lean.Parser.Term.binop then
-    /-
-    We support `binop%` syntax in patterns because we
-    wanted to support `x+1` in patterns.
-    Recall that the `binop%` syntax was added to improve elaboration of some binary operators: `+` is one of them.
-    Recall that `HAdd.hAdd` is marked as `[match_pattern]`
-    TODO for a distant future: make this whole procedure extensible.
-    -/
-    -- Check whether the `binop%` operator is marked with `[match_pattern]`,
-    -- We must check that otherwise Lean will accept operators that are not tagged with this annotation.
-    let some (.const fName _) ← resolveId? stx[1] "pattern"
-      | throwCtorExpected
-    unless hasMatchPatternAttribute (← getEnv) fName do
-      throwCtorExpected
     let lhs ← collect stx[2]
     let rhs ← collect stx[3]
     return stx.setArg 2 lhs |>.setArg 3 rhs

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Util.HasConstCache
-import Lean.Meta.Match.MatcherApp.Transform
+import Lean.Meta.Match.Match
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -37,12 +37,12 @@ where
       return ()
     else if (← tryContradiction mvarId) then
       return ()
-    else if let some mvarId ← whnfReducibleLHS? mvarId then
-      go mvarId
     else if let some mvarId ← simpMatch? mvarId then
       go mvarId
     else if let some mvarId ← simpIf? mvarId then
       go mvarId
+    else if let some mvarId ← whnfReducibleLHS? mvarId then
+      go mvarId
     else match (← simpTargetStar mvarId {} (simprocs := {})).1 with
       | TacticResultCNM.closed => return ()
       | TacticResultCNM.modified mvarId => go mvarId

src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Meta.Match.MatcherApp.Basic
 
 namespace Lean.Elab.Structural
 open Meta

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -5,7 +5,7 @@ Authors: Joachim Breitner
 -/
 prelude
 import Lean.Util.HasConstCache
-import Lean.Meta.Match.MatcherApp.Transform
+import Lean.Meta.Match.Match
 import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Refl
 import Lean.Elab.Quotation

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -68,14 +68,7 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
     for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
       let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
       mvarId.withContext do
-        let errorMsgHeader? := if preDefs.size > 1 then
-          "The termination argument types differ for the different functions, or depend on the " ++
-          "function's varying parameters. Try using `sizeOf` explicitly:\nThe termination argument"
-        else
-          "The termination argument depends on the function's varying parameters. Try using " ++
-          "`sizeOf` explicitly:\nThe termination argument"
         let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
-            (errorMsgHeader? := errorMsgHeader?)
         mvarId.assign value
     let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
     wfRelMVarId.assign wfRelVal

src/Lean/Elab/StructInst.lean

@@ -77,27 +77,9 @@ where
         go sources (sourcesNew.push source)
       else
         withFreshMacroScope do
-          /-
-          Recall that local variables starting with `__` are treated as impl detail.
-          See `LocalContext.lean`.
-          Moreover, implementation detail let-vars are unfolded by `simp`
-          even when `zetaDelta := false`.
-          Motivation: the following failure when `zetaDelta := true`
-          ```
-          structure A where
-            a : Nat
-          structure B extends A where
-            b : Nat
-            w : a = b
-          def x : A where a := 37
-          @[simp] theorem x_a : x.a = 37 := rfl
-
-          def y : B := { x with b := 37, w := by simp }
-          ```
-          -/
-          let sourceNew ← `(__src)
+          let sourceNew ← `(src)
           let r ← go sources (sourcesNew.push sourceNew)
-          `(let __src := $source; $r)
+          `(let src := $source; $r)
 
 structure ExplicitSourceInfo where
   stx        : Syntax

src/Lean/Elab/Tactic.lean

@@ -13,7 +13,6 @@ import Lean.Elab.Tactic.Injection
 import Lean.Elab.Tactic.Match
 import Lean.Elab.Tactic.Rewrite
 import Lean.Elab.Tactic.Location
-import Lean.Elab.Tactic.SimpTrace
 import Lean.Elab.Tactic.Simp
 import Lean.Elab.Tactic.Simproc
 import Lean.Elab.Tactic.BuiltinTactic
@@ -33,7 +32,3 @@ import Lean.Elab.Tactic.Change
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Elab.Tactic.Omega
 import Lean.Elab.Tactic.Simpa
-import Lean.Elab.Tactic.NormCast
-import Lean.Elab.Tactic.Symm
-import Lean.Elab.Tactic.SolveByElim
-import Lean.Elab.Tactic.LibrarySearch

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -1,81 +0,0 @@
-/-
-Copyright (c) 2021-2024 Gabriel Ebner and Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner, Joe Hendrix, Scott Morrison
--/
-prelude
-import Lean.Meta.Tactic.LibrarySearch
-import Lean.Meta.Tactic.TryThis
-import Lean.Elab.Tactic.ElabTerm
-
-namespace Lean.Elab.LibrarySearch
-
-open Lean Meta LibrarySearch
-open Elab Tactic Term TryThis
-
-/--
-Implementation of the `exact?` tactic.
-
-* `ref` contains the input syntax and is used for locations in error reporting.
-* `required` contains an optional list of terms that should be used in closing the goal.
-* `requireClose` indicates if the goal must be closed.
-  It is `true` for `exact?` and `false` for `apply?`.
--/
-def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) :
-    TacticM Unit := do
-  let mvar ← getMainGoal
-  let (_, goal) ← (← getMainGoal).intros
-  goal.withContext do
-    let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar
-    let tactic := fun exfalso =>
-          solveByElim required (exfalso := exfalso) (maxDepth := 6)
-    let allowFailure := fun g => do
-      let g ← g.withContext (instantiateMVars (.mvar g))
-      return required.all fun e => e.occurs g
-    match ← librarySearch goal tactic allowFailure with
-    -- Found goal that closed problem
-    | none =>
-      addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta
-    -- Found suggestions
-    | some suggestions =>
-      if requireClose then throwError
-        "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
-      reportOutOfHeartbeats `library_search ref
-      for (_, suggestionMCtx) in suggestions do
-        withMCtx suggestionMCtx do
-          addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)
-      if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas"
-      admitGoal goal
-
-@[builtin_tactic Lean.Parser.Tactic.exact?]
-def evalExact : Tactic := fun stx => do
-  let `(tactic| exact? $[using $[$required],*]?) := stx
-        | throwUnsupportedSyntax
-  exact? (← getRef) required true
-
-
-@[builtin_tactic Lean.Parser.Tactic.apply?]
-def evalApply : Tactic := fun stx => do
-  let `(tactic| apply? $[using $[$required],*]?) := stx
-        | throwUnsupportedSyntax
-  exact? (← getRef) required false
-
-@[builtin_term_elab Lean.Parser.Syntax.exact?]
-def elabExact?Term : TermElab := fun stx expectedType? => do
-  let `(exact?%) := stx | throwUnsupportedSyntax
-  withExpectedType expectedType? fun expectedType => do
-    let goal ← mkFreshExprMVar expectedType
-    let (_, introdGoal) ← goal.mvarId!.intros
-    introdGoal.withContext do
-      if let some suggestions ← librarySearch introdGoal then
-        reportOutOfHeartbeats `library_search stx
-        for suggestion in suggestions do
-          withMCtx suggestion.2 do
-            addTermSuggestion stx (← instantiateMVars goal).headBeta
-        if suggestions.isEmpty then logError "exact?# didn't find any relevant lemmas"
-        mkSorry expectedType (synthetic := true)
-      else
-        addTermSuggestion stx (← instantiateMVars goal).headBeta
-        instantiateMVars goal
-
-end Lean.Elab.LibrarySearch

src/Lean/Elab/Tactic/NormCast.lean

@@ -1,274 +0,0 @@
-/-
-Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
--/
-prelude
-import Lean.Meta.Tactic.NormCast
-import Lean.Elab.Tactic.Conv.Simp
-import Lean.Elab.ElabRules
-
-/-!
-# The `norm_cast` family of tactics.
-
-A full description of the tactic, and the use of each theorem category, can be found at
-<https://arxiv.org/abs/2001.10594>.
--/
-namespace Lean.Elab.Tactic.NormCast
-open Lean Meta Simp NormCast
-
--- TODO: trace name consistency
-builtin_initialize registerTraceClass `Tactic.norm_cast
-
-/-- Proves `a = b` using the given simp set. -/
-def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) := do
-  let go : SimpM (Option Simp.Result) := do
-    let a' ← Simp.simp a
-    let b' ← Simp.simp b
-    unless ← isDefEq a'.expr b'.expr do return none
-    a'.mkEqTrans (← b'.mkEqSymm b)
-  withReducible do
-    (go (← Simp.mkDefaultMethods).toMethodsRef
-      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
-
-/-- Proves `a = b` by simplifying using move and squash lemmas. -/
-def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
-  withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} proving: {← mkEq a b}") do
-  proveEqUsing (← normCastExt.down.getTheorems) a b
-
-/-- Constructs the expression `(e : ty)`. -/
-def mkCoe (e : Expr) (ty : Expr) : MetaM Expr := do
-  let .some e' ← coerce? e ty | failure
-  return e'
-
-/--
-Checks whether an expression is the coercion of some other expression,
-and if so returns that expression.
--/
-def isCoeOf? (e : Expr) : MetaM (Option Expr) := do
-  if let Expr.const fn .. := e.getAppFn then
-    if let some info ← getCoeFnInfo? fn then
-      if e.getAppNumArgs == info.numArgs then
-        return e.getArg! info.coercee
-  return none
-
-/--
-Checks whether an expression is a numeral in some type,
-and if so returns that type and the natural number.
--/
-def isNumeral? (e : Expr) : Option (Expr × Nat) :=
-  -- TODO: cleanup, and possibly remove duplicate
-  if e.isConstOf ``Nat.zero then
-    (mkConst ``Nat, 0)
-  else if let Expr.app (Expr.app (Expr.app (Expr.const ``OfNat.ofNat ..) α ..)
-      (Expr.lit (Literal.natVal n) ..) ..) .. := e then
-    some (α, n)
-  else
-    none
-
-/--
-This is the main heuristic used alongside the elim and move lemmas.
-The goal is to help casts move past operators by adding intermediate casts.
-An expression of the shape:
-```
-op (↑(x : α) : γ) (↑(y : β) : γ)
-```
-is rewritten to:
-```
-op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ)
-```
-when
-```
-(↑(↑(x : α) : β) : γ) = (↑(x : α) : γ)
-```
-can be proven with a squash lemma
--/
-def splittingProcedure (expr : Expr) : MetaM Simp.Result := do
-  let Expr.app (Expr.app op x ..) y .. := expr | return {expr}
-
-  let Expr.forallE _ γ (Expr.forallE _ γ' ty ..) .. ← inferType op | return {expr}
-  if γ'.hasLooseBVars || ty.hasLooseBVars then return {expr}
-  unless ← isDefEq γ γ' do return {expr}
-
-  let msg := m!"splitting {expr}"
-  let msg
-    | .error _ => return m!"{bombEmoji} {msg}"
-    | .ok r => return if r.expr == expr then m!"{crossEmoji} {msg}" else
-      m!"{checkEmoji} {msg} to {r.expr}"
-  withTraceNode `Tactic.norm_cast msg do
-
-  try
-    let some x' ← isCoeOf? x | failure
-    let some y' ← isCoeOf? y | failure
-    let α ← inferType x'
-    let β ← inferType y'
-
-    -- TODO: fast timeout
-    (try
-      let x2 ← mkCoe (← mkCoe x' β) γ
-      let some x_x2 ← proveEqUsingDown x x2 | failure
-      Simp.mkCongrFun (← Simp.mkCongr {expr := op} x_x2) y
-    catch _ =>
-      let y2 ← mkCoe (← mkCoe y' α) γ
-      let some y_y2 ← proveEqUsingDown y y2 | failure
-      Simp.mkCongr {expr := mkApp op x} y_y2)
-  catch _ => try
-    let some (_, n) := isNumeral? y | failure
-    let some x' ← isCoeOf? x | failure
-    let α ← inferType x'
-    let y2 ← mkCoe (← mkNumeral α n) γ
-    let some y_y2 ← proveEqUsingDown y y2 | failure
-    Simp.mkCongr {expr := mkApp op x} y_y2
-  catch _ => try
-    let some (_, n) := isNumeral? x | failure
-    let some y' ← isCoeOf? y | failure
-    let β ← inferType y'
-    let x2 ← mkCoe (← mkNumeral β n) γ
-    let some x_x2 ← proveEqUsingDown x x2 | failure
-    Simp.mkCongrFun (← Simp.mkCongr {expr := op} x_x2) y
-  catch _ =>
-    return {expr}
-
-/--
-Discharging function used during simplification in the "squash" step.
--/
--- TODO: normCast takes a list of expressions to use as lemmas for the discharger
--- TODO: a tactic to print the results the discharger fails to prove
-def prove (e : Expr) : SimpM (Option Expr) := do
-  withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} discharging: {e}") do
-  return (← findLocalDeclWithType? e).map mkFVar
-
-/--
-Core rewriting function used in the "squash" step, which moves casts upwards
-and eliminates them.
-
-It tries to rewrite an expression using the elim and move lemmas.
-On failure, it calls the splitting procedure heuristic.
--/
-partial def upwardAndElim (up : SimpTheorems) (e : Expr) : SimpM Simp.Step := do
-  let r ← withDischarger prove do
-    Simp.rewrite? e up.post up.erased (tag := "squash") (rflOnly := false)
-  let r := r.getD { expr := e }
-  let r ← r.mkEqTrans (← splittingProcedure r.expr)
-  if r.expr == e then return Simp.Step.done {expr := e}
-  return Simp.Step.visit r
-
-/--
-If possible, rewrites `(n : α)` to `(Nat.cast n : α)` where `n` is a numeral and `α ≠ ℕ`.
-Returns a pair of the new expression and proof that they are equal.
--/
-def numeralToCoe (e : Expr) : MetaM Simp.Result := do
-  let some (α, n) := isNumeral? e | failure
-  if (← whnf α).isConstOf ``Nat then failure
-  let newE ← mkAppOptM ``Nat.cast #[α, none, toExpr n]
-  let some pr ← proveEqUsingDown e newE | failure
-  return pr
-
-/--
-The core simplification routine of `normCast`.
--/
-def derive (e : Expr) : MetaM Simp.Result := do
-  withTraceNode `Tactic.norm_cast (fun _ => return m!"{e}") do
-  let e ← instantiateMVars e
-
-  let config : Simp.Config := {
-    zeta := false
-    beta := false
-    eta  := false
-    proj := false
-    iota := false
-  }
-  let congrTheorems ← Meta.getSimpCongrTheorems
-
-  let r : Simp.Result := { expr := e }
-
-  let withTrace phase := withTraceNode `Tactic.norm_cast fun
-    | .ok r => return m!"{r.expr} (after {phase})"
-    | .error _ => return m!"{bombEmoji} {phase}"
-
-  -- step 1: pre-processing of numerals
-  let r ← withTrace "pre-processing numerals" do
-    let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
-    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
-
-  -- step 2: casts are moved upwards and eliminated
-  let r ← withTrace "moving upward, splitting and eliminating" do
-    let post := upwardAndElim (← normCastExt.up.getTheorems)
-    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
-
-  -- step 3: casts are squashed
-  let r ← withTrace "squashing" do
-    let simpTheorems := #[← normCastExt.squash.getTheorems]
-    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems }).1
-
-  return r
-
-open Term
-@[builtin_term_elab modCast] def elabModCast : TermElab := fun stx expectedType? => do
-  match stx with
-  | `(mod_cast $e:term) =>
-    withExpectedType expectedType? fun expectedType => do
-    if (← instantiateMVars expectedType).hasExprMVar then tryPostpone
-    let expectedType' ← derive expectedType
-    let e ← Term.elabTerm e expectedType'.expr
-    synthesizeSyntheticMVars
-    let eTy ← instantiateMVars (← inferType e)
-    if eTy.hasExprMVar then tryPostpone
-    let eTy' ← derive eTy
-    unless ← isDefEq eTy'.expr expectedType'.expr do
-      throwTypeMismatchError "mod_cast" expectedType'.expr eTy'.expr e
-    let eTy_eq_expectedType ← eTy'.mkEqTrans (← expectedType'.mkEqSymm expectedType )
-    eTy_eq_expectedType.mkCast e
-  | _ => throwUnsupportedSyntax
-
-/-- Implementation of the `norm_cast` tactic when operating on the main goal. -/
-def normCastTarget : TacticM Unit :=
-  liftMetaTactic1 fun goal => do
-    let tgt ← instantiateMVars (← goal.getType)
-    let prf ← derive tgt
-    applySimpResultToTarget goal tgt prf
-
-/-- Implementation of the `norm_cast` tactic when operating on a hypothesis. -/
-def normCastHyp (fvarId : FVarId) : TacticM Unit :=
-  liftMetaTactic1 fun goal => do
-    let hyp ← instantiateMVars (← fvarId.getDecl).type
-    let prf ← derive hyp
-    return (← applySimpResultToLocalDecl goal fvarId prf false).map (·.snd)
-
-@[builtin_tactic normCast0]
-def evalNormCast0 : Tactic := fun stx => do
-  match stx with
-  | `(tactic| norm_cast0 $[$loc?]?) =>
-    let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
-    withMainContext do
-      match loc with
-      | Location.targets hyps target =>
-        if target then normCastTarget
-        (← getFVarIds hyps).forM normCastHyp
-      | Location.wildcard =>
-        normCastTarget
-        (← (← getMainGoal).getNondepPropHyps).forM normCastHyp
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic Lean.Parser.Tactic.Conv.normCast]
-def evalConvNormCast : Tactic :=
-  open Elab.Tactic.Conv in fun _ => withMainContext do
-    applySimpResult (← derive (← getLhs))
-
-@[builtin_tactic pushCast]
-def evalPushCast : Tactic := fun stx => do
-  let { ctx, simprocs, dischargeWrapper } ← withMainContext do
-    mkSimpContext (simpTheorems := pushCastExt.getTheorems) stx (eraseLocal := false)
-  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
-  dischargeWrapper.with fun discharge? =>
-    discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
-
-open Command in
-@[builtin_command_elab Parser.Tactic.normCastAddElim] def elabAddElim : CommandElab := fun stx => do
-  match stx with
-  | `(norm_cast_add_elim $id:ident) =>
-    Elab.Command.liftCoreM do MetaM.run' do
-     addElim (← resolveGlobalConstNoOverload id)
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic.NormCast

src/Lean/Elab/Tactic/Omega.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
 import Lean.Elab.Tactic.Omega.Frontend
 
 /-!

src/Lean/Elab/Tactic/Omega/Core.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: Scott Morrison
 -/
-prelude
-import Init.Omega.Constraint
 import Lean.Elab.Tactic.Omega.OmegaM
 import Lean.Elab.Tactic.Omega.MinNatAbs
 
@@ -505,37 +503,29 @@ Decides which variable to run Fourier-Motzkin elimination on, and returns the as
 We prefer eliminations which introduce no new inequalities, or otherwise exact eliminations,
 and break ties by the number of new inequalities introduced.
 -/
-def fourierMotzkinSelect (data : Array FourierMotzkinData) : MetaM FourierMotzkinData := do
+def fourierMotzkinSelect (data : Array FourierMotzkinData) : FourierMotzkinData := Id.run do
   let data := data.filter fun d => ¬ d.isEmpty
-  trace[omega] "Selecting variable to eliminate from (idx, size, exact) triples:\n\
-    {data.map fun d => (d.var, d.size, d.exact)}"
   let mut bestIdx := 0
   let mut bestSize := data[0]!.size
   let mut bestExact := data[0]!.exact
-  if bestSize = 0 then
-    trace[omega] "Selected variable {data[0]!.var}."
-    return data[0]!
+  if bestSize = 0 then return data[0]!
   for i in [1:data.size] do
     let exact := data[i]!.exact
     let size := data[i]!.size
-    if size = 0 || !bestExact && exact || (bestExact == exact) && size < bestSize then
-      if size = 0 then
-        trace[omega] "Selected variable {data[i]!.var}"
-        return data[i]!
+    if size = 0 || !bestExact && exact || size < bestSize then
+      if size = 0 then return data[i]!
       bestIdx := i
       bestExact := exact
       bestSize := size
-  trace[omega] "Selected variable {data[bestIdx]!.var}."
   return data[bestIdx]!
 
 /--
 Run Fourier-Motzkin elimination on one variable.
 -/
--- This is only in MetaM to enable tracing.
-def fourierMotzkin (p : Problem) : MetaM Problem := do
+def fourierMotzkin (p : Problem) : Problem := Id.run do
   let data := p.fourierMotzkinData
   -- Now perform the elimination.
-  let ⟨_, irrelevant, lower, upper, _, _⟩ ← fourierMotzkinSelect data
+  let ⟨_, irrelevant, lower, upper, _, _⟩ := fourierMotzkinSelect data
   let mut r : Problem := { assumptions := p.assumptions, eliminations := p.eliminations }
   for f in irrelevant do
     r := r.insertConstraint f
@@ -564,7 +554,7 @@ partial def elimination (p : Problem) : OmegaM Problem :=
       return p
     else do
       trace[omega] "Running Fourier-Motzkin elimination on:\n{p}"
-      runOmega (← p.fourierMotzkin)
+      runOmega p.fourierMotzkin
   else
     return p
 

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Meta.Tactic.Cases
@@ -24,13 +23,6 @@ Allow elaboration of `OmegaConfig` arguments to tactics.
 -/
 declare_config_elab elabOmegaConfig Lean.Meta.Omega.OmegaConfig
 
-/-- Match on the two defeq expressions for successor: `n+1`, `n.succ`. -/
-def succ? (e : Expr) : Option Expr :=
-  match e.getAppFnArgs with
-  | (``Nat.succ, #[n]) => some n
-  | (``HAdd.hAdd, #[_, _, _, _, a, b]) => do
-     if b == toExpr (1 : Nat) then some a else none
-  | _ => none
 
 /--
 A partially processed `omega` context.
@@ -84,6 +76,13 @@ def mkAtomLinearCombo (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet
   let (n, facts) ← lookup e
   return ⟨LinearCombo.coordinate n, mkCoordinateEvalAtomsEq e n, facts.getD ∅⟩
 
+-- This has been PR'd as
+-- https://github.com/leanprover/lean4/pull/2900
+-- and can be removed when that is merged.
+@[inherit_doc mkAppN]
+local macro_rules
+  | `(mkAppN $f #[$xs,*]) => (xs.getElems.foldlM (fun x e => `(Expr.app $x $e)) f : MacroM Term)
+
 mutual
 
 /--
@@ -122,7 +121,7 @@ We also transform the expression as we descend into it:
 -/
 partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet Expr) := do
   trace[omega] "processing {e}"
-  match groundInt? e with
+  match e.int? with
   | some i =>
     let lc := {const := i}
     return ⟨lc, mkEvalRflProof e lc, ∅⟩
@@ -185,20 +184,17 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
     | some r => pure r
     | none => mkAtomLinearCombo e
   | (``HMod.hMod, #[_, _, _, _, n, k]) =>
-    match groundNat? k with
-    | some k' => do
-      let k' := toExpr (k' : Int)
-      rewrite (← mkAppM ``HMod.hMod #[n, k']) (mkApp2 (.const ``Int.emod_def []) n k')
+    match natCast? k with
+    | some _ => rewrite e (mkApp2 (.const ``Int.emod_def []) n k)
     | none => mkAtomLinearCombo e
   | (``HDiv.hDiv, #[_, _, _, _, x, z]) =>
-    match groundInt? z with
+    match intCast? z with
     | some 0 => rewrite e (mkApp (.const ``Int.ediv_zero []) x)
-    | some i => do
-      let e' ← mkAppM ``HDiv.hDiv #[x, toExpr i]
+    | some i =>
       if i < 0 then
-        rewrite e' (mkApp2 (.const ``Int.ediv_neg []) x (toExpr (-i)))
+        rewrite e (mkApp2 (.const ``Int.ediv_neg []) x (toExpr (-i)))
       else
-        mkAtomLinearCombo e'
+        mkAtomLinearCombo e
     | _ => mkAtomLinearCombo e
   | (``Min.min, #[_, _, a, b]) =>
     if (← cfg).splitMinMax then
@@ -210,15 +206,39 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
       rewrite e (mkApp2 (.const ``Int.max_def []) a b)
     else
       mkAtomLinearCombo e
-  | (``HPow.hPow, #[_, _, _, _, b, k]) =>
-    match succ? k with /- match for `e+1` and `e.succ` -/
-    | none => mkAtomLinearCombo e
-    | some k' =>
-        match groundInt? b with
-        | some _ => rewrite e (mkApp2 (.const ``Int.pow_succ []) b k')
-        | none => mkAtomLinearCombo e
   | (``Nat.cast, #[.const ``Int [], i, n]) =>
-      handleNatCast e i n
+    match n with
+    | .fvar h =>
+      if let some v ← h.getValue? then
+        rewrite e (← mkEqReflWithExpectedType e
+          (mkApp3 (.const ``Nat.cast [0]) (.const ``Int []) i v))
+      else
+        mkAtomLinearCombo e
+    | _ => match n.getAppFnArgs with
+    | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n)
+    | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_add []) a b)
+    | (``HMul.hMul, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
+    | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b)
+    | (``OfNat.ofNat, #[_, n, _]) => rewrite e (.app (.const ``Int.natCast_ofNat []) n)
+    | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_emod []) a b)
+    | (``HSub.hSub, #[_, _, _, _, mkAppN (.const ``HSub.hSub _) #[_, _, _, _, a, b], c]) =>
+      rewrite e (mkApp3 (.const ``Int.ofNat_sub_sub []) a b c)
+    | (``Prod.fst, #[_, β, p]) => match p with
+      | .app (.app (.app (.app (.const ``Prod.mk [0, v]) _) _) x) y =>
+        rewrite e (mkApp3 (.const ``Int.ofNat_fst_mk [v]) β x y)
+      | _ => mkAtomLinearCombo e
+    | (``Prod.snd, #[α, _, p]) => match p with
+      | .app (.app (.app (.app (.const ``Prod.mk [u, 0]) _) _) x) y =>
+        rewrite e (mkApp3 (.const ``Int.ofNat_snd_mk [u]) α x y)
+      | _ => mkAtomLinearCombo e
+    | (``Min.min, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_min []) a b)
+    | (``Max.max, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_max []) a b)
+    | (``Int.natAbs, #[n]) =>
+      if (← cfg).splitNatAbs then
+        rewrite e (mkApp (.const ``Int.ofNat_natAbs []) n)
+      else
+        mkAtomLinearCombo e
+    | _ => mkAtomLinearCombo e
   | (``Prod.fst, #[α, β, p]) => match p with
     | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y =>
       rewrite e (mkApp4 (.const ``Prod.fst_mk [u, v]) α x β y)
@@ -241,78 +261,6 @@ where
       let prf' : OmegaM Expr := do mkEqTrans rw (← prf)
       pure (lc, prf', facts)
     | none => panic! "Invalid rewrite rule in 'asLinearCombo'"
-  handleNatCast (e i n : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet Expr) := do
-    match n with
-    | .fvar h =>
-      if let some v ← h.getValue? then
-        rewrite e (← mkEqReflWithExpectedType e
-          (mkApp3 (.const ``Nat.cast [0]) (.const ``Int []) i v))
-      else
-        mkAtomLinearCombo e
-    | _ => match n.getAppFnArgs with
-    | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n)
-    | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_add []) a b)
-    | (``HMul.hMul, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
-    | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b)
-    | (``OfNat.ofNat, #[_, n, _]) => rewrite e (.app (.const ``Int.natCast_ofNat []) n)
-    | (``HMod.hMod, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_emod []) a b)
-    | (``HSub.hSub, #[_, _, _, _, mkApp6 (.const ``HSub.hSub _) _ _ _ _ a b, c]) =>
-      rewrite e (mkApp3 (.const ``Int.ofNat_sub_sub []) a b c)
-    | (``HPow.hPow, #[_, _, _, _, a, b]) =>
-      match groundNat? a with
-      | some _ => rewrite e (mkApp2 (.const ``Int.ofNat_pow []) a b)
-      | none => mkAtomLinearCombo e
-    | (``Prod.fst, #[_, β, p]) => match p with
-      | .app (.app (.app (.app (.const ``Prod.mk [0, v]) _) _) x) y =>
-        rewrite e (mkApp3 (.const ``Int.ofNat_fst_mk [v]) β x y)
-      | _ => mkAtomLinearCombo e
-    | (``Prod.snd, #[α, _, p]) => match p with
-      | .app (.app (.app (.app (.const ``Prod.mk [u, 0]) _) _) x) y =>
-        rewrite e (mkApp3 (.const ``Int.ofNat_snd_mk [u]) α x y)
-      | _ => mkAtomLinearCombo e
-    | (``Min.min, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_min []) a b)
-    | (``Max.max, #[_, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_max []) a b)
-    | (``HShiftLeft.hShiftLeft, #[_, _, _, _, a, b]) =>
-      rewrite e (mkApp2 (.const ``Int.ofNat_shiftLeft_eq []) a b)
-    | (``HShiftRight.hShiftRight, #[_, _, _, _, a, b]) =>
-      rewrite e (mkApp2 (.const ``Int.ofNat_shiftRight_eq_div_pow []) a b)
-    | (``Int.natAbs, #[n]) =>
-      if (← cfg).splitNatAbs then
-        rewrite e (mkApp (.const ``Int.ofNat_natAbs []) n)
-      else
-        mkAtomLinearCombo e
-    | (``Fin.val, #[n, x]) =>
-      handleFinVal e i n x
-    | _ => mkAtomLinearCombo e
-  handleFinVal (e i n x : Expr) : OmegaM (LinearCombo × OmegaM Expr × HashSet Expr) := do
-    match x with
-    | .fvar h =>
-      if let some v ← h.getValue? then
-        rewrite e (← mkEqReflWithExpectedType e
-          (mkApp3 (.const ``Nat.cast [0]) (.const ``Int []) i (mkApp2 (.const ``Fin.val []) n v)))
-      else
-        mkAtomLinearCombo e
-    | _ => match x.getAppFnArgs, n.nat? with
-      | (``HAdd.hAdd, #[_, _, _, _, a, b]), _ =>
-        rewrite e (mkApp3 (.const ``Fin.ofNat_val_add []) n a b)
-      | (``HMul.hMul, #[_, _, _, _, a, b]), _ =>
-        rewrite e (mkApp3 (.const ``Fin.ofNat_val_mul []) n a b)
-      | (``HSub.hSub, #[_, _, _, _, a, b]), some _ =>
-        -- Only do this rewrite if `n` is a numeral.
-        rewrite e (mkApp3 (.const ``Fin.ofNat_val_sub []) n a b)
-      | (``OfNat.ofNat, #[_, y, _]), some m =>
-        -- Only do this rewrite if `n` is a nonzero numeral.
-        if m = 0 then
-          mkAtomLinearCombo e
-        else
-          match y with
-          | .lit (.natVal y) =>
-            rewrite e (mkApp4 (.const ``Fin.ofNat_val_natCast [])
-              (toExpr (m - 1)) (toExpr y) (.lit (.natVal (y % m))) (← mkEqRefl (toExpr (y % m))))
-          | _ =>
-            -- This shouldn't happen, we obtained `y` from `OfNat.ofNat`
-            mkAtomLinearCombo e
-      | _, _ => mkAtomLinearCombo e
 
 end
 namespace MetaProblem
@@ -375,17 +323,11 @@ def pushNot (h P : Expr) : MetaM (Option Expr) := do
       return some (mkApp3 (.const ``Nat.le_of_not_lt []) x y h)
     | (``LE.le, #[.const ``Nat [], _, x, y]) =>
       return some (mkApp3 (.const ``Nat.lt_of_not_le []) x y h)
-    | (``LT.lt, #[.app (.const ``Fin []) n, _, x, y]) =>
-      return some (mkApp4 (.const ``Fin.le_of_not_lt []) n x y h)
-    | (``LE.le, #[.app (.const ``Fin []) n, _, x, y]) =>
-      return some (mkApp4 (.const ``Fin.lt_of_not_le []) n x y h)
     | (``Eq, #[.const ``Nat [], x, y]) =>
       return some (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h)
     | (``Eq, #[.const ``Int [], x, y]) =>
       return some (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h)
     | (``Prod.Lex, _) => return some (← mkAppM ``Prod.of_not_lex #[h])
-    | (``Eq, #[.app (.const ``Fin []) n, x, y]) =>
-      return some (mkApp4 (.const ``Fin.lt_or_gt_of_ne []) n x y h)
     | (``Dvd.dvd, #[.const ``Nat [], _, k, x]) =>
       return some (mkApp3 (.const ``Nat.emod_pos_of_not_dvd []) k x h)
     | (``Dvd.dvd, #[.const ``Int [], _, k, x]) =>
@@ -460,16 +402,6 @@ partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) :
         p.addFact (mkApp3 (.const ``Nat.mod_eq_zero_of_dvd []) k x h)
       | (``Dvd.dvd, #[.const ``Int [], _, k, x]) =>
         p.addFact (mkApp3 (.const ``Int.emod_eq_zero_of_dvd []) k x h)
-      | (``Eq, #[.app (.const ``Fin []) n, x, y]) =>
-        p.addFact (mkApp4 (.const ``Fin.val_congr []) n x y h)
-      | (``LE.le, #[.app (.const ``Fin []) n, _, x, y]) =>
-        p.addFact (mkApp4 (.const ``Fin.val_le_of_le []) n x y h)
-      | (``LT.lt, #[.app (.const ``Fin []) n, _, x, y]) =>
-        p.addFact (mkApp4 (.const ``Fin.val_add_one_le_of_lt []) n x y h)
-      | (``GE.ge, #[.app (.const ``Fin []) n, _, x, y]) =>
-        p.addFact (mkApp4 (.const ``Fin.val_le_of_ge []) n x y h)
-      | (``GT.gt, #[.app (.const ``Fin []) n, _, x, y]) =>
-        p.addFact (mkApp4 (.const ``Fin.val_add_one_le_of_gt []) n x y h)
       | (``And, #[t₁, t₂]) => do
           let (p₁, n₁) ← p.addFact (mkApp3 (.const ``And.left []) t₁ t₂ h)
           let (p₂, n₂) ← p₁.addFact (mkApp3 (.const ``And.right []) t₁ t₂ h)
@@ -573,6 +505,7 @@ partial def omegaImpl (m : MetaProblem) (g : MVarId) : OmegaM Unit := g.withCont
     trace[omega] "Justification:\n{p'.explanation?.get}"
     let prf ← instantiateMVars (← prf)
     trace[omega] "omega found a contradiction, proving {← inferType prf}"
+    trace[omega] "{prf}"
     g.assign prf
 
 end
@@ -598,7 +531,7 @@ def omegaTactic (cfg : OmegaConfig) : TacticM Unit := do
 
 /-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
 `TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
-the tactic call `aesop (add 50% tactic Lean.Omega.omegaDefault)`. -/
+the tactic call `aesop (add 50% tactic Std.Tactic.Omega.omegaDefault)`. -/
 def omegaDefault : TacticM Unit := omegaTactic {}
 
 @[builtin_tactic Lean.Parser.Tactic.omega]
@@ -607,7 +540,3 @@ def evalOmega : Tactic := fun
     let cfg ← elabOmegaConfig (mkOptionalNode cfg)
     omegaTactic cfg
   | _ => throwUnsupportedSyntax
-
-builtin_initialize bvOmegaSimpExtension : SimpExtension ←
-  registerSimpAttr `bv_toNat
-    "simp lemmas converting `BitVec` goals to `Nat` goals, for the `bv_omega` preprocessor"

src/Lean/Elab/Tactic/Omega/MinNatAbs.lean

@@ -3,10 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
-import Init.BinderPredicates
-import Init.Data.List
-import Init.Data.Option
 
 /-!
 # `List.nonzeroMinimum`, `List.minNatAbs`, `List.maxNatAbs`

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -3,11 +3,6 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-prelude
-import Init.Omega.LinearCombo
-import Init.Omega.Int
-import Init.Omega.Logic
-import Init.Data.BitVec
 import Lean.Meta.AppBuilder
 
 /-!
@@ -113,45 +108,6 @@ def intCast? (n : Expr) : Option Int :=
   | (``Nat.cast, #[_, _, n]) => n.nat?
   | _ => n.int?
 
-/--
-If `groundNat? e = some n`, then `e` is definitionally equal to `OfNat.ofNat n`.
--/
--- We may want to replace this with an implementation using
--- the internals of `simp (config := {ground := true})`
-partial def groundNat? (e : Expr) : Option Nat :=
-  match e.getAppFnArgs with
-  | (``Nat.cast, #[_, _, n]) => groundNat? n
-  | (``HAdd.hAdd, #[_, _, _, _, x, y]) => op (· + ·) x y
-  | (``HMul.hMul, #[_, _, _, _, x, y]) => op (· * ·) x y
-  | (``HSub.hSub, #[_, _, _, _, x, y]) => op (· - ·) x y
-  | (``HDiv.hDiv, #[_, _, _, _, x, y]) => op (· / ·) x y
-  | (``HPow.hPow, #[_, _, _, _, x, y]) => op (· ^ ·) x y
-  | _ => e.nat?
-where op (f : Nat → Nat → Nat) (x y : Expr) : Option Nat :=
-  match groundNat? x, groundNat? y with
-    | some x', some y' => some (f x' y')
-    | _, _ => none
-
-/--
-If `groundInt? e = some i`,
-then `e` is definitionally equal to the standard expression for `i`.
--/
-partial def groundInt? (e : Expr) : Option Int :=
-  match e.getAppFnArgs with
-  | (``Nat.cast, #[_, _, n]) => groundNat? n
-  | (``HAdd.hAdd, #[_, _, _, _, x, y]) => op (· + ·) x y
-  | (``HMul.hMul, #[_, _, _, _, x, y]) => op (· * ·) x y
-  | (``HSub.hSub, #[_, _, _, _, x, y]) => op (· - ·) x y
-  | (``HDiv.hDiv, #[_, _, _, _, x, y]) => op (· / ·) x y
-  | (``HPow.hPow, #[_, _, _, _, x, y]) => match groundInt? x, groundNat? y with
-    | some x', some y' => some (x' ^ y')
-    | _, _ => none
-  | _ => e.int?
-where op (f : Int → Int → Int) (x y : Expr) : Option Int :=
-  match groundNat? x, groundNat? y with
-    | some x', some y' => some (f x' y')
-    | _, _ => none
-
 /-- Construct the term with type hint `(Eq.refl a : a = b)`-/
 def mkEqReflWithExpectedType (a b : Expr) : MetaM Expr := do
   mkExpectedTypeHint (← mkEqRefl a) (← mkEq a b)
@@ -174,8 +130,6 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
         r := r.insert (mkApp (.const ``Int.neg_le_natAbs []) x)
       | _, (``Fin.val, #[n, i]) =>
         r := r.insert (mkApp2 (.const ``Fin.isLt []) n i)
-      | _, (``BitVec.toNat, #[n, x]) =>
-        r := r.insert (mkApp2 (.const ``BitVec.toNat_lt []) n x)
       | _, _ => pure ()
     return r
   | (``HDiv.hDiv, #[_, _, _, _, x, k]) => match natCast? k with

src/Lean/Elab/Tactic/Simp.lean

@@ -178,24 +178,13 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             -- We use `eraseCore` because the simp theorem for the hypothesis was not added yet
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
-            let id := arg[1]
-            let declNames? ← try pure (some (← resolveGlobalConst id)) catch _ => pure none
-            if let some declNames := declNames? then
-              let declName ← ensureNonAmbiguous id declNames
-              if (← Simp.isSimproc declName) then
-                simprocs := simprocs.erase declName
-              else if ctx.config.autoUnfold then
-                thms := thms.eraseCore (.decl declName)
-              else
-                thms ← thms.erase (.decl declName)
+            let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
+            if (← Simp.isSimproc declName) then
+              simprocs := simprocs.erase declName
+            else if ctx.config.autoUnfold then
+              thms := thms.eraseCore (.decl declName)
             else
-              -- If `id` could not be resolved, we should check whether it is a builtin simproc.
-              -- before returning error.
-              let name := id.getId.eraseMacroScopes
-              if (← Simp.isBuiltinSimproc name) then
-                simprocs := simprocs.erase name
-              else
-                throwUnknownConstant name
+              thms ← thms.erase (.decl declName)
         else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
           let post :=
             if arg[0].isNone then
@@ -459,22 +448,3 @@ where
   dsimpLocation ctx (expandOptLocation stx[5])
 
 end Lean.Elab.Tactic
-
-/-!
-The following parsers for `simp` arguments are not actually used at present in the
-implementation of `simp` above, but are useful for further tactics which need
-to parse `simp` arguments.
--/
-namespace Lean.Parser.Tactic
-
-/-- Extract the arguments from a `simpArgs` syntax as an array of syntaxes -/
-def getSimpArgs? : Syntax → Option (Array Syntax)
-  | `(simpArgs| [$args,*]) => pure args.getElems
-  | _ => none
-
-/-- Extract the arguments from a `dsimpArgs` syntax as an array of syntaxes -/
-def getDSimpArgs? : Syntax → Option (Array Syntax)
-  | `(dsimpArgs| [$args,*]) => pure args.getElems
-  | _                       => none
-
-end Lean.Parser.Tactic

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -1,91 +0,0 @@
-/-
-Copyright (c) 2022 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro
--/
-prelude
-import Lean.Elab.ElabRules
-import Lean.Elab.Tactic.Simp
-import Lean.Meta.Tactic.TryThis
-
-/-!
-# `simp?` tactic
-
-The `simp?` tactic is a simple wrapper around the simp with trace behavior.
--/
-namespace Lean.Elab.Tactic
-open Lean Elab Parser Tactic Meta Simp Tactic.TryThis
-
-open TSyntax.Compat in
-/-- Constructs the syntax for a simp call, for use with `simp?`. -/
-def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tactic) := do
-  let stx := stx.unsetTrailing
-  mkSimpOnly stx usedSimps
-
-@[builtin_tactic simpTrace] def evalSimpTrace : Tactic := fun stx =>
-  match stx with
-  | `(tactic|
-      simp?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
-    let stx ← if bang.isSome then
-      `(tactic| simp!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    else
-      `(tactic| simp%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    let { ctx, simprocs, dischargeWrapper } ←
-      withMainContext <| mkSimpContext stx (eraseLocal := false)
-    let usedSimps ← dischargeWrapper.with fun discharge? =>
-      simpLocation ctx (simprocs := simprocs) discharge? <|
-        (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx usedSimps
-    addSuggestion tk stx (origSpan? := ← getRef)
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx =>
-  match stx with
-  | `(tactic| simp_all?%$tk $[!%$bang]? $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?) => do
-    let stx ← if bang.isSome then
-      `(tactic| simp_all!%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
-    else
-      `(tactic| simp_all%$tk $(config)? $(discharger)? $[only%$o]? $[[$args,*]]?)
-    let { ctx, .. } ← mkSimpContext stx (eraseLocal := true)
-      (kind := .simpAll) (ignoreStarArg := true)
-    let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
-    match result? with
-    | none => replaceMainGoal []
-    | some mvarId => replaceMainGoal [mvarId]
-    let stx ← mkSimpCallStx stx usedSimps
-    addSuggestion tk stx (origSpan? := ← getRef)
-  | _ => throwUnsupportedSyntax
-
-/-- Implementation of `dsimp?`. -/
-def dsimpLocation' (ctx : Simp.Context) (loc : Location) : TacticM Simp.UsedSimps := do
-  match loc with
-  | Location.targets hyps simplifyTarget =>
-    withMainContext do
-      let fvarIds ← getFVarIds hyps
-      go fvarIds simplifyTarget
-  | Location.wildcard =>
-    withMainContext do
-      go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
-where
-  /-- Implementation of `dsimp?`. -/
-  go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
-    let mvarId ← getMainGoal
-    let (result?, usedSimps) ←
-      dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp)
-    match result? with
-    | none => replaceMainGoal []
-    | some mvarId => replaceMainGoal [mvarId]
-    pure usedSimps
-
-@[builtin_tactic dsimpTrace] def evalDSimpTrace : Tactic := fun stx =>
-  match stx with
-  | `(tactic| dsimp?%$tk $[!%$bang]? $(config)? $[only%$o]? $[[$args,*]]? $(loc)?) => do
-    let stx ← if bang.isSome then
-      `(tactic| dsimp!%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    else
-      `(tactic| dsimp%$tk $(config)? $[only%$o]? $[[$args,*]]? $(loc)?)
-    let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-    let usedSimps ← dsimpLocation' ctx <| (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx usedSimps
-    addSuggestion tk stx (origSpan? := ← getRef)
-  | _ => throwUnsupportedSyntax

src/Lean/Elab/Tactic/Simpa.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Gabriel Ebner, Mario Carneiro
 -/
-prelude
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Tactic.Simp

src/Lean/Elab/Tactic/SolveByElim.lean

@@ -1,113 +0,0 @@
-/-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison, David Renshaw
--/
-prelude
-import Lean.Meta.Tactic.SolveByElim
-import Lean.Elab.Tactic.Config
-
-namespace Lean.Elab.Tactic.SolveByElim
-open Meta
-
-open Lean.Parser.Tactic
-open Lean.Parser.Tactic.SolveByElim
-
-open Lean.Meta.SolveByElim (SolveByElimConfig mkAssumptionSet)
-
-/--
-Allow elaboration of `Config` arguments to tactics.
--/
-declare_config_elab elabConfig Lean.Meta.SolveByElim.SolveByElimConfig
-
-/--
-Allow elaboration of `ApplyRulesConfig` arguments to tactics.
--/
-declare_config_elab elabApplyRulesConfig Lean.Meta.SolveByElim.ApplyRulesConfig
-
-/--
-Parse the lemma argument of a call to `solve_by_elim`.
-The first component should be true if `*` appears at least once.
-The second component should contain each term `t`in the arguments.
-The third component should contain `t` for each `-t` in the arguments.
--/
-def parseArgs (s : Option (TSyntax ``args)) :
-    Bool × List Term × List Term :=
-  let args : Array (TSyntax ``arg) := match s with
-  | some s => match s with
-    | `(args| [$args,*]) => args.getElems
-    | _ => #[]
-  | none => #[]
-  let args : Array (Option (Term ⊕ Term)) := args.map fun t => match t with
-    | `(arg| $_:star) => none
-    | `(arg| - $t:term) => some (Sum.inr t)
-    | `(arg| $t:term) => some (Sum.inl t)
-    | _ => panic! "Unreachable parse of solve_by_elim arguments."
-  let args := args.toList
-  (args.contains none,
-    args.filterMap fun o => o.bind Sum.getLeft?,
-    args.filterMap fun o => o.bind Sum.getRight?)
-
-/-- Parse the `using ...` argument for `solve_by_elim`. -/
-def parseUsing (s : Option (TSyntax ``using_)) : Array Ident :=
-  match s with
-  | some s => match s with
-    | `(using_ | using $ids,*) => ids.getElems
-    | _ => #[]
-  | none => #[]
-
-/-- Wrapper for `solveByElim` that processes a list of `Term`s
-that specify the lemmas to use. -/
-def processSyntax (cfg : SolveByElimConfig := {}) (only star : Bool) (add remove : List Term)
-    (use : Array Ident) (goals : List MVarId) : MetaM (List MVarId) := do
-  if !remove.isEmpty && goals.length > 1 then
-    throwError "Removing local hypotheses is not supported when operating on multiple goals."
-  let ⟨lemmas, ctx⟩ ← mkAssumptionSet only star add remove use
-  SolveByElim.solveByElim cfg lemmas ctx goals
-
-@[builtin_tactic Lean.Parser.Tactic.applyAssumption]
-def evalApplyAssumption : Tactic := fun stx =>
-  match stx with
-  | `(tactic| apply_assumption $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
-    let (star, add, remove) := parseArgs t
-    let use := parseUsing use
-    let cfg ← elabConfig (mkOptionalNode cfg)
-    let cfg := { cfg with
-      backtracking := false
-      maxDepth := 1 }
-    replaceMainGoal (← processSyntax cfg o.isSome star add remove use [← getMainGoal])
-  | _ => throwUnsupportedSyntax
-
-/--
-Elaborator for apply_rules.
-
-See `Lean.MVarId.applyRules` for a `MetaM` level analogue of this tactic.
--/
-@[builtin_tactic Lean.Parser.Tactic.applyRules]
-def evalApplyRules : Tactic := fun stx =>
-  match stx with
-  | `(tactic| apply_rules $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
-    let (star, add, remove) := parseArgs t
-    let use := parseUsing use
-    let cfg ← elabApplyRulesConfig (mkOptionalNode cfg)
-    let cfg := { cfg with backtracking := false }
-    liftMetaTactic fun g => processSyntax cfg o.isSome star add remove use [g]
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic Lean.Parser.Tactic.solveByElim]
-def evalSolveByElim : Tactic := fun stx =>
-  match stx with
-  | `(tactic| solve_by_elim $[*%$s]? $[$cfg]? $[only%$o]? $[$t:args]? $[$use:using_]?) => do
-    let (star, add, remove) := parseArgs t
-    let use := parseUsing use
-    let goals ← if s.isSome then
-      getGoals
-    else
-      pure [← getMainGoal]
-    let cfg ← elabConfig (mkOptionalNode cfg)
-    let [] ← processSyntax cfg o.isSome star add remove use goals |
-      throwError "solve_by_elim unexpectedly returned subgoals"
-    pure ()
-  | _ => throwUnsupportedSyntax
-
-end Lean.Elab.Tactic.SolveByElim

src/Lean/Elab/Tactic/Symm.lean

@@ -1,27 +0,0 @@
-/-
-Copyright (c) 2022 Siddhartha Gadgil. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Siddhartha Gadgil, Mario Carneiro, Scott Morrison
--/
-prelude
-import Lean.Meta.Tactic.Symm
-import Lean.Elab.Tactic.Location
-
-namespace Lean.Elab.Tactic
-
-@[builtin_tactic Lean.Parser.Tactic.symm]
-def evalSymm : Tactic := fun stx =>
-  match stx with
-  | `(tactic| symm $(loc?)?) => do
-    let atHyp h := liftMetaTactic1 fun g => g.applySymmAt h
-    let atTarget := liftMetaTactic1 fun g => g.applySymm
-    let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
-    withLocation loc atHyp atTarget fun _ => throwError "symm made no progress"
-  | _ => throwUnsupportedSyntax
-
-@[builtin_tactic Lean.Parser.Tactic.symmSaturate]
-def evalSymmSaturate : Tactic := fun stx =>
-  match stx with
-  | `(tactic| symm_saturate) => do
-    liftMetaTactic1 fun g => g.symmSaturate
-  | _ => throwUnsupportedSyntax

src/Lean/Expr.lean

@@ -799,7 +799,7 @@ def isType0 : Expr → Bool
   | sort (.succ .zero) => true
   | _ => false
 
-/-- Return `true` if the given expression is `.sort .zero` -/
+/-- Return `true` if the given expression is a `.sort .zero` -/
 def isProp : Expr → Bool
   | sort (.zero ..) => true
   | _ => false
@@ -912,7 +912,7 @@ def litValue! : Expr → Literal
   | lit v => v
   | _     => panic! "literal expected"
 
-def isRawNatLit : Expr → Bool
+def isNatLit : Expr → Bool
   | lit (Literal.natVal _) => true
   | _                      => false
 
@@ -925,7 +925,7 @@ def isStringLit : Expr → Bool
   | _                      => false
 
 def isCharLit : Expr → Bool
-  | app (const c _) a => c == ``Char.ofNat && a.isRawNatLit
+  | app (const c _) a => c == ``Char.ofNat && a.isNatLit
   | _                 => false
 
 def constName! : Expr → Name
@@ -1037,14 +1037,6 @@ def getAppFn : Expr → Expr
   | app f _ => getAppFn f
   | e         => e
 
-/--
-Similar to `getAppFn`, but skips `mdata`
--/
-def getAppFn' : Expr → Expr
-  | app f _   => getAppFn' f
-  | mdata _ a => getAppFn' a
-  | e         => e
-
 /-- Given `f a₀ a₁ ... aₙ`, returns true if `f` is a constant with name `n`. -/
 def isAppOf (e : Expr) (n : Name) : Bool :=
   match e.getAppFn with
@@ -1215,21 +1207,10 @@ def getRevArg! : Expr → Nat → Expr
   | app f _, i+1 => getRevArg! f i
   | _,       _   => panic! "invalid index"
 
-/-- Similar to `getRevArg!` but skips `mdata` -/
-def getRevArg!' : Expr → Nat → Expr
-  | mdata _ a, i => getRevArg!' a i
-  | app _ a, 0   => a
-  | app f _, i+1 => getRevArg!' f i
-  | _,       _   => panic! "invalid index"
-
 /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or panics if out of bounds. -/
 @[inline] def getArg! (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
   getRevArg! e (n - i - 1)
 
-/-- Similar to `getArg!`, but skips mdata -/
-@[inline] def getArg!' (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
-  getRevArg!' e (n - i - 1)
-
 /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or returns `v₀` if out of bounds. -/
 @[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
   getRevArgD e (n - i - 1) v₀

src/Lean/LabelAttribute.lean

@@ -1,96 +0,0 @@
-/-
-Copyright (c) 2023 Scott Morrison. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
--/
-prelude
-import Lean.ScopedEnvExtension
-import Lean.DocString
-
-/-!
-# "Label" attributes
-
-Allow creating attributes using `register_label_attr`,
-and retrieving the array of `Name`s of declarations which have been tagged with such an attribute.
-
-These differ slightly from the built-in "tag attributes" which can be initialized with the syntax:
-```
-initialize someName : TagAttribute ← registerTagAttribute `tagName "description"
-```
-in that a "tag attribute" can only be put on a declaration at the moment it is declared,
-and can not be modified by scoping commands.
-
-The "label attributes" constructed here support adding (or locally removing) the attribute
-either at the moment of declaration, or later.
-
--/
-
-namespace Lean
-
-/-- An environment extension that just tracks an array of names. -/
-abbrev LabelExtension := SimpleScopedEnvExtension Name (Array Name)
-
-/-- The collection of all current `LabelExtension`s, indexed by name. -/
-abbrev LabelExtensionMap := HashMap Name LabelExtension
-
-/-- Store the current `LabelExtension`s. -/
-builtin_initialize labelExtensionMapRef : IO.Ref LabelExtensionMap ← IO.mkRef {}
-
-/-- Helper function for `registerLabelAttr`. -/
-def mkLabelExt (name : Name := by exact decl_name%) : IO LabelExtension :=
-  registerSimpleScopedEnvExtension {
-    name     := name
-    initial  := #[]
-    addEntry := fun d e => if d.contains e then d else d.push e
-  }
-
-/-- Helper function for `registerLabelAttr`. -/
-def mkLabelAttr (attrName : Name) (attrDescr : String) (ext : LabelExtension)
-  (ref : Name := by exact decl_name%) : IO Unit :=
-registerBuiltinAttribute {
-  ref   := ref
-  name  := attrName
-  descr := attrDescr
-  applicationTime := AttributeApplicationTime.afterCompilation
-  add   := fun declName _ _ =>
-    ext.add declName
-  erase := fun declName => do
-    let s := ext.getState (← getEnv)
-    modifyEnv fun env => ext.modifyState env fun _ => s.erase declName
-}
-
-/--
-Construct a new "label attribute",
-which does nothing except keep track of the names of the declarations with that attribute.
-
-Users will generally use the `register_label_attr` macro defined below.
--/
-def registerLabelAttr (attrName : Name) (attrDescr : String)
-    (ref : Name := by exact decl_name%) : IO LabelExtension := do
-  let ext ← mkLabelExt ref
-  mkLabelAttr attrName attrDescr ext ref
-  labelExtensionMapRef.modify fun map => map.insert attrName ext
-  return ext
-
-/--
-Initialize a new "label" attribute.
-Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
--/
-macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
-  doc:(docComment)? "register_label_attr " id:ident : command => do
-  let str := id.getId.toString
-  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
-  let descr := quote (removeLeadingSpaces
-    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
-  `($[$doc:docComment]? initialize ext : Lean.LabelExtension ←
-      registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
-
-/-- When `attrName` is an attribute created using `register_labelled_attr`,
-return the names of all declarations labelled using that attribute. -/
-def labelled (attrName : Name) : CoreM (Array Name) := do
-  match (← labelExtensionMapRef.get).find? attrName with
-  | none => throwError "No extension named {attrName}"
-  | some ext => pure <| ext.getState (← getEnv)
-
-end Lean

src/Lean/Linter.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2022 Lars König. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
--/
 prelude
 import Lean.Linter.Util
 import Lean.Linter.Builtin

src/Lean/Linter/Basic.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2022 Lars König. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
--/
 prelude
 import Lean.Data.Options
 

src/Lean/Linter/Builtin.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2022 Lars König. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
--/
 prelude
 import Lean.Linter.Util
 import Lean.Elab.Command

src/Lean/Linter/MissingDocs.lean

@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+
 Authors: Mario Carneiro
 -/
 prelude

src/Lean/Linter/UnusedVariables.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich
--/
 prelude
 import Lean.Elab.Command
 import Lean.Util.ForEachExpr

src/Lean/Linter/Util.lean

@@ -1,8 +1,3 @@
-/-
-Copyright (c) 2022 Lars König. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lars König
--/
 prelude
 import Lean.Data.Options
 import Lean.Server.InfoUtils

src/Lean/Meta.lean

@@ -44,6 +44,3 @@ import Lean.Meta.ExprLens
 import Lean.Meta.ExprTraverse
 import Lean.Meta.Eval
 import Lean.Meta.CoeAttr
-import Lean.Meta.Iterator
-import Lean.Meta.LazyDiscrTree
-import Lean.Meta.LitValues

src/Lean/Meta/Basic.lean

@@ -1067,23 +1067,6 @@ partial def withNewLocalInstances (fvars : Array Expr) (j : Nat) : n α → n α
 def forallTelescope (type : Expr) (k : Array Expr → Expr → n α) : n α :=
   map2MetaM (fun k => forallTelescopeImp type k) k
 
-/--
-Given a monadic function `f` that takes a type and a term of that type and produces a new term,
-lifts this to the monadic function that opens a `∀` telescope, applies `f` to the body,
-and then builds the lambda telescope term for the new term.
--/
-def mapForallTelescope' (f : Expr → Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
-  forallTelescope (← inferType forallTerm) fun xs ty => do
-    mkLambdaFVars xs (← f ty (mkAppN forallTerm xs))
-
-/--
-Given a monadic function `f` that takes a term and produces a new term,
-lifts this to the monadic function that opens a `∀` telescope, applies `f` to the body,
-and then builds the lambda telescope term for the new term.
--/
-def mapForallTelescope (f : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
-  mapForallTelescope' (fun _ e => f e) forallTerm
-
 private def forallTelescopeReducingImp (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α :=
   forallTelescopeReducingAux type (maxFVars? := none) k
 

src/Lean/Meta/CollectMVars.lean

@@ -46,39 +46,4 @@ def getMVarsAtDecl (d : Declaration) : MetaM (Array MVarId) := do
   let (_, s) ← (collectMVarsAtDecl d).run {}
   pure s.result
 
-/--
-Collect the metavariables which `mvarId` depends on. These are the metavariables
-which appear in the type and local context of `mvarId`, as well as the
-metavariables which *those* metavariables depend on, etc.
--/
-partial def _root_.Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed := false) :
-    MetaM (HashSet MVarId) :=
-  (·.snd) <$> (go mvarId).run {}
-where
-  /-- Auxiliary definition for `getMVarDependencies`. -/
-  addMVars (e : Expr) : StateRefT (HashSet MVarId) MetaM Unit := do
-    let mvars ← getMVars e
-    let mut s ← get
-    set ({} : HashSet MVarId) -- Ensure that `s` is not shared.
-    for mvarId in mvars do
-      if ← pure includeDelayed <||> notM (mvarId.isDelayedAssigned) then
-        s := s.insert mvarId
-    set s
-    mvars.forM go
-
-  /-- Auxiliary definition for `getMVarDependencies`. -/
-  go (mvarId : MVarId) : StateRefT (HashSet MVarId) MetaM Unit :=
-    withIncRecDepth do
-      let mdecl ← mvarId.getDecl
-      addMVars mdecl.type
-      for ldecl in mdecl.lctx do
-        addMVars ldecl.type
-        if let (some val) := ldecl.value? then
-          addMVars val
-      if let (some ass) ← getDelayedMVarAssignment? mvarId then
-        let pendingMVarId := ass.mvarIdPending
-        if ← notM pendingMVarId.isAssignedOrDelayedAssigned then
-          modify (·.insert pendingMVarId)
-        go pendingMVarId
-
 end Lean.Meta

src/Lean/Meta/CompletionName.lean

@@ -1,59 +0,0 @@
-/-
-Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Basic
-import Lean.Meta.Match.MatcherInfo
-
-/-!
-This exports a predicate for checking whether a name should be made
-visible in auto-completion and other tactics that suggest names to
-insert into Lean code.
-
-The `exact?` tactic is an example of a tactic that benefits from this
-functionality.  `exact?` finds lemmas in the environment to use to
-prove a theorem, but it needs to avoid inserting references to theorems
-with unstable names such as auxillary lemmas that could change with
-minor unintentional modifications to definitions.
-
-It uses a blacklist environment extension to enable names in an
-environment to be specifically hidden.
--/
-namespace Lean.Meta
-
-builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDeclarationExtension
-
-@[export lean_completion_add_to_black_list]
-def addToCompletionBlackList (env : Environment) (declName : Name) : Environment :=
-  completionBlackListExt.tag env declName
-
-/--
-Checks whether a given name is internal due to something other than `_private`.
-Correctly deals with names like `_private.<SomeNamespace>.0.<SomeType>._sizeOf_1` in a private type
-`SomeType`, which `n.isInternal && !isPrivateName n` does not.
--/
-private def isInternalNameModuloPrivate : Name → Bool
-  | n@(.str p s) => s.get 0 == '_' && n != privateHeader || isInternalNameModuloPrivate p
-  | .num p _ => isInternalNameModuloPrivate p
-  | _       => false
-
-/--
-Return true if name is blacklisted for completion purposes.
--/
-private def isBlacklisted (env : Environment) (declName : Name) : Bool :=
-  isInternalNameModuloPrivate declName
-  || isAuxRecursor env declName
-  || isNoConfusion env declName
-  || isRecCore env declName
-  || completionBlackListExt.isTagged env declName
-  || isMatcherCore env declName
-
-/--
-Return true if completion is allowed for name.
--/
-def allowCompletion (env : Environment) (declName : Name) : Bool :=
-  !(isBlacklisted env declName)
-
-end Lean.Meta