fix: unnecessary NatModules in grind linarith

This PR fixes a performance issue in `grind linarith`. It was creating
unnecessary `NatModule`/`IntModule` structures for commutative rings
without an order. This kind of type should be handled by `grind ring` only.

.claude/CLAUDE.md

@@ -1,34 +0,0 @@
-To build Lean you should use `make -j -C build/release`.
-
-To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
-
-## New features
-
-When asked to implement new features:
-* begin by reviewing existing relevant code and tests
-* write comprehensive tests first (expecting that these will initially fail)
-* and then iterate on the implementation until the tests pass.
-
-All new tests should go in `tests/lean/run/`. These tests don't have expected output; we just check there are no errors. You should use `#guard_msgs` to check for specific messages.
-
-## Success Criteria
-
-*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass.
-
-## Build System Safety
-
-**NEVER manually delete build directories** (build/, stage0/, stage1/, etc.) even when builds fail.
-- ONLY use the project's documented build command: `make -j -C build/release`
-- If a build is broken, ask the user before attempting any manual cleanup
-
-## LSP and IDE Diagnostics
-
-After rebuilding, LSP diagnostics may be stale until the user interacts with files. Trust command-line test results over IDE diagnostics.
-
-## Update prompting when the user is frustrated
-
-If the user expresses frustration with you, stop and ask them to help update this `.claude/CLAUDE.md` file with missing guidance.
-
-## Creating pull requests.
-
-All PRs must have a first paragraph starting with "This PR". This paragraph is automatically incorporated into release notes. Read `lean4/doc/dev/commit_convention.md` when making PRs.

.claude/commands/release.md

@@ -1,69 +0,0 @@
-# Release Management Command
-
-Execute the release process for a given version by running the release checklist and following its instructions.
-
-## Before Starting
-
-**IMPORTANT**: Before beginning the release process, read the in-file documentation:
-- Read `script/release_checklist.py` for what the checklist script does
-- Read `script/release_steps.py` for what the release steps script does
-
-These comments explain the scripts' behavior, which repositories get special handling, and how errors are handled.
-
-## Arguments
-- `version`: The version to release (e.g., v4.24.0)
-
-## Process
-
-1. Run `script/release_checklist.py {version}` to check the current status
-2. **CRITICAL: If preliminary lean4 checks fail, STOP immediately and alert the user**
-   - Check for: release branch exists, CMake version correct, tag exists, release page exists, release notes exist
-   - **IMPORTANT**: The release page is created AUTOMATICALLY by CI after pushing the tag - DO NOT create it manually
-   - Do NOT create any PRs or proceed with repository updates if these checks fail
-3. Create a todo list tracking all repositories that need updates
-4. **CRITICAL RULE: You can ONLY run `release_steps.py` for a repository if `release_checklist.py` explicitly says to do so**
-   - The checklist output will say "Run `script/release_steps.py {version} {repo_name}` to create it"
-   - If a repository shows "🟡 Dependencies not ready", you CANNOT create a PR for it yet
-   - You MUST rerun `release_checklist.py` before attempting to create PRs for any new repositories
-5. For each repository that the checklist says needs updating:
-   - Run `script/release_steps.py {version} {repo_name}` to create the PR
-   - Mark it complete when the PR is created
-6. After creating PRs, notify the user which PRs need review and merging
-7. **MANDATORY: Rerun `release_checklist.py` to check current status**
-   - Do this after creating each batch of PRs
-   - Do this after the user reports PRs have been merged
-   - NEVER assume a repository is ready without checking the checklist output
-8. As PRs are merged and tagged, dependent repositories will become ready
-9. Continue the cycle: run checklist → create PRs for ready repos → wait for merges → repeat
-10. Continue until all repositories are updated and the release is complete
-
-## Important Notes
-
-- The `release_steps.py` script is idempotent - it's safe to rerun
-- The `release_checklist.py` script is idempotent - it's safe to rerun
-- Some repositories depend on others (e.g., mathlib4 depends on batteries, aesop, etc.)
-- Wait for user to merge PRs before dependent repos can be updated
-- Alert user if anything unusual or scary happens
-- Use appropriate timeouts for long-running builds (verso can take 10+ minutes)
-- ProofWidgets4 uses semantic versioning (v0.0.X) - it's okay to create and push the next sequential tag yourself when needed for a release
-
-## PR Status Reporting
-
-Every time you run `release_checklist.py`, you MUST:
-1. Parse the output to identify ALL open PRs mentioned (lines with "✅ PR with title ... exists")
-2. Provide a summary to the user listing ALL open PRs that need review
-3. Group them by status:
-   - PRs for repositories that are blocked by dependencies (show these but note they're blocked)
-   - PRs for repositories that are ready to merge (highlight these)
-4. Format the summary clearly with PR numbers and URLs
-
-This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
-The user needs to see the complete picture of what's waiting for review.
-
-## Error Handling
-
-**CRITICAL**: If something goes wrong or a command fails:
-- **DO NOT** try to manually reproduce the failing steps yourself
-- **DO NOT** try to fix things by running git commands or other manual operations
-- Both scripts are idempotent and designed to handle partial completion gracefully
-- If a script continues to fail after retrying, report the error to the user and wait for instructions

.gitattributes

@@ -4,9 +4,3 @@ RELEASES.md merge=union
 stage0/** binary linguist-generated
 # The following file is often manually edited, so do show it in diffs
 stage0/src/stdlib_flags.h -binary -linguist-generated
-# These files should not have line endings translated on Windows, because
-# it throws off parser tests. Later lines override earlier ones, so the
-# runner code is still treated as ordinary text.
-tests/lean/docparse/* eol=lf
-tests/lean/docparse/*.lean eol=auto
-tests/lean/docparse/*.sh eol=auto

.github/workflows/actionlint.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout
-      uses: actions/checkout@v5
+      uses: actions/checkout@v4
     - name: actionlint
       uses: raven-actions/actionlint@v2
       with:

.github/workflows/awaiting-manual.yml

@@ -12,7 +12,7 @@ jobs:
       - name: Check awaiting-manual label
         id: check-awaiting-manual-label
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const { labels, number: prNumber } = context.payload.pull_request;

.github/workflows/awaiting-mathlib.yml

@@ -12,7 +12,7 @@ jobs:
       - name: Check awaiting-mathlib label
         id: check-awaiting-mathlib-label
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const { labels, number: prNumber } = context.payload.pull_request;

.github/workflows/build-template.yml

@@ -3,6 +3,9 @@ name: build-template
 on:
   workflow_call:
     inputs:
+      check-level:
+        type: string
+        required: true
       config:
         type: string
         required: true
@@ -67,7 +70,7 @@ jobs:
         if: runner.os == 'macOS'
       - name: Checkout
         if: (!endsWith(matrix.os, '-with-cache'))
-        uses: actions/checkout@v5
+        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 }}
@@ -113,10 +116,10 @@ jobs:
             build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
-          key: ${{ matrix.name }}-build-v4-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
-            ${{ matrix.name }}-build-v4
+            ${{ matrix.name }}-build-v3
       # open nix-shell once for initial setup
       - name: Setup
         run: |
@@ -213,7 +216,7 @@ jobs:
           else
             ${{ matrix.tar || 'tar' }} cf - $dir | zstd -T0 --no-progress -o pack/$dir.tar.zst
           fi
-      - uses: actions/upload-artifact@v5
+      - uses: actions/upload-artifact@v4
         if: matrix.release
         with:
           name: build-${{ matrix.name }}
@@ -227,7 +230,7 @@ jobs:
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: matrix.test
+        if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
       - name: Test Summary
         uses: test-summary/action@v2
         with:

.github/workflows/check-prelude.yml

@@ -7,7 +7,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v5
+        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 }}

.github/workflows/check-stage0.yml

@@ -8,11 +8,11 @@ jobs:
   check-stage0-on-queue:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v4
       with:
         ref: ${{ github.event.pull_request.head.sha }}
+        filter: blob:none
         fetch-depth: 0
-        filter: tree:0
 
     - name: Find base commit
       if: github.event_name == 'pull_request'
@@ -31,7 +31,7 @@ jobs:
 
     - if: github.event_name == 'pull_request'
       name: Set label
-      uses: actions/github-script@v8
+      uses: actions/github-script@v7
       with:
         script: |
           const { owner, repo, number: issue_number  } = context.issue;

.github/workflows/ci.yml

@@ -31,6 +31,10 @@ jobs:
   configure:
     runs-on: ubuntu-latest
     outputs:
+      # 0: PRs without special label
+      # 1: PRs with `merge-ci` label, merge queue checks, master commits
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
+      check-level: ${{ steps.set-level.outputs.check-level }}
       # The build matrix, dynamically generated here
       matrix: ${{ steps.set-matrix.outputs.matrix }}
       # secondary build jobs that should not block the CI success/merge queue
@@ -50,7 +54,7 @@ jobs:
 
     steps:
       - name: Checkout
-        uses: actions/checkout@v5
+        uses: actions/checkout@v4
         # don't schedule nightlies on forks
         if: github.event_name == 'schedule' && github.repository == 'leanprover/lean4' || inputs.action == 'release nightly'
       - name: Set Nightly
@@ -106,54 +110,6 @@ jobs:
           TAG_NAME="${GITHUB_REF##*/}"
           echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
 
-      - name: Validate CMakeLists.txt version matches tag
-        if: steps.set-release.outputs.RELEASE_TAG != ''
-        run: |
-          echo "Validating CMakeLists.txt version matches tag ${{ steps.set-release.outputs.RELEASE_TAG }}"
-
-          # Extract version values from CMakeLists.txt
-          CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_IS_RELEASE=$(grep -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+')
-
-          # Expected values from tag parsing
-          TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"
-          TAG_MINOR="${{ steps.set-release.outputs.LEAN_VERSION_MINOR }}"
-          TAG_PATCH="${{ steps.set-release.outputs.LEAN_VERSION_PATCH }}"
-
-          ERRORS=""
-
-          if [[ "$CMAKE_MAJOR" != "$TAG_MAJOR" ]]; then
-            ERRORS+="LEAN_VERSION_MAJOR: expected $TAG_MAJOR, found $CMAKE_MAJOR\n"
-          fi
-          if [[ "$CMAKE_MINOR" != "$TAG_MINOR" ]]; then
-            ERRORS+="LEAN_VERSION_MINOR: expected $TAG_MINOR, found $CMAKE_MINOR\n"
-          fi
-          if [[ "$CMAKE_PATCH" != "$TAG_PATCH" ]]; then
-            ERRORS+="LEAN_VERSION_PATCH: expected $TAG_PATCH, found $CMAKE_PATCH\n"
-          fi
-          if [[ "$CMAKE_IS_RELEASE" != "1" ]]; then
-            ERRORS+="LEAN_VERSION_IS_RELEASE: expected 1, found $CMAKE_IS_RELEASE\n"
-          fi
-
-          if [[ -n "$ERRORS" ]]; then
-            echo "::error::Version mismatch between tag and src/CMakeLists.txt"
-            echo ""
-            echo "Tag ${{ steps.set-release.outputs.RELEASE_TAG }} expects version $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
-            echo "But src/CMakeLists.txt has mismatched values:"
-            echo -e "$ERRORS"
-            echo ""
-            echo "Fix src/CMakeLists.txt, delete the tag, and re-tag."
-            exit 1
-          fi
-
-          echo "Version validation passed: $TAG_MAJOR.$TAG_MINOR.$TAG_PATCH"
-
-      # 0: PRs without special label
-      # 1: PRs with `merge-ci` label, merge queue checks, master commits
-      # 2: nightlies
-      # 3: PRs with `release-ci` label, full releases
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -161,39 +117,31 @@ jobs:
         # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
         run: |
           check_level=0
-          fast=false
 
-          if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
-            check_level=3
-          elif [[ -n "${{ steps.set-nightly.outputs.nightly }}" ]]; then
+          if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=2
           elif [[ "${{ github.event_name }}" != "pull_request" ]]; then
             check_level=1
           else
             labels="$(gh api repos/${{ github.repository_owner }}/${{ github.event.repository.name }}/pulls/${{ github.event.pull_request.number }} --jq '.labels')"
             if echo "$labels" | grep -q "release-ci"; then
-              check_level=3
+              check_level=2
             elif echo "$labels" | grep -q "merge-ci"; then
               check_level=1
             fi
-            if echo "$labels" | grep -q "fast-ci"; then
-              fast=true
-            fi
           fi
 
           echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
-          echo "fast=$fast" >> "$GITHUB_OUTPUT"
         env:
           GH_TOKEN: ${{ github.token }}
 
       - name: Configure build matrix
         id: set-matrix
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
-            const fast = ${{ steps.set-level.outputs.fast }};
-            console.log(`level: ${level}, fast: ${fast}`);
+            console.log(`level: ${level}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
@@ -204,8 +152,7 @@ jobs:
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -218,19 +165,17 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the
                 //    Linux lake build and adds little value in the merge queue
                 // 3. To run it in release (obviously)
                 // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
                 //    available as an artifact for Grove to use.
-                "enabled": isPr || level != 1 || isPushToMaster,
-                "test": level >= 1,
-                "secondary": level == 0,
+                "check-level": (isPr || isPushToMaster) ? 0 : 2,
+                "secondary": isPr,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -241,44 +186,36 @@ jobs:
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
+                "check-level": 0,
+                "test": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
-                "test": true,
                 // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
                 "test-speedcenter": large && level >= 2,
-                // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
+                // made explicit until it can be assumed to have propagated to PRs
+                "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
               },
               {
                 "name": "Linux Reldebug",
                 "os": "ubuntu-latest",
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "CMAKE_PRESET": "reldebug",
               },
-              {
+              // TODO: suddenly started failing in CI
+              /*{
                 "name": "Linux fsanitize",
-                // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": level >= 2,
-                // do not fail nightlies on this for now
-                "secondary": level <= 2,
-                "test": true,
+                "os": "ubuntu-latest",
+                "check-level": 2,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
-                // `StackOverflow*` correctly triggers ubsan
-                // `reverse-ffi` fails to link in sanitizers
-                // `interactive` and `async_select_channel` fail nondeterministically, would need to
-                // be investigated.
-                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel'"
-              },
+                // exclude seriously slow/problematic tests (laketests crash)
+                "CTEST_OPTIONS": "-E 'interactivetest|leanpkgtest|laketest|benchtest'"
+              },*/
               {
                 "name": "macOS",
-                "os": "macos-15-intel",
+                "os": "macos-13",
                 "release": true,
-                "test": false,  // Tier 2 platform
-                "enabled": level >= 2,
+                "check-level": 2,
                 "shell": "bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@@ -289,7 +226,7 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
+                "os": large && !isPr ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -298,16 +235,14 @@ jobs:
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
                 // See "Linux release" for release job levels; Grove is not a concern here
-                "enabled": isPr || level != 1,
-                "test": level >= 1,
-                "secondary": level == 0,
+                "check-level": isPr ? 0 : 2,
+                "secondary": isPr,
               },
               {
                 "name": "Windows",
-                "os": large && (fast || level >= 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -319,8 +254,7 @@ jobs:
                 "os": "nscloud-ubuntu-22.04-arm64-4x16",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -333,7 +267,7 @@ jobs:
               //  "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
               //  "cmultilib": true,
               //  "release": true,
-              //  "enabled": level >= 2,
+              //  "check-level": 2,
               //  "cross": true,
               //  "shell": "bash -euxo pipefail {0}"
               //}
@@ -345,7 +279,7 @@ jobs:
               //   "wasm": true,
               //   "cmultilib": true,
               //   "release": true,
-              //   "enabled": level >= 2,
+              //   "check-level": 2,
               //   "cross": true,
               //   "shell": "bash -euxo pipefail {0}",
               //   // Just a few selected tests because wasm is slow
@@ -359,7 +293,7 @@ jobs:
               }
             }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            matrix = matrix.filter((job) => job["enabled"]);
+            matrix = matrix.filter((job) => level >= job["check-level"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
             core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
 
@@ -369,6 +303,7 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix}}
+      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -384,6 +319,7 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix-secondary}}
+      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -414,7 +350,7 @@ jobs:
         content: |
           A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
     - if: contains(needs.*.result, 'failure')
-      uses: actions/github-script@v8
+      uses: actions/github-script@v7
       with:
         script: |
             core.setFailed('Some jobs failed')
@@ -427,11 +363,11 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v6
+      - uses: actions/download-artifact@v4
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -452,14 +388,12 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v5
+        uses: actions/checkout@v4
         with:
           # needed for tagging
           fetch-depth: 0
-          # Doesn't seem to be working when additionally fetching from lean4-nightly
-          #filter: tree:0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v6
+      - uses: actions/download-artifact@v4
         with:
           path: artifacts
       - name: Prepare Nightly Release
@@ -477,7 +411,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           body_path: diff.md
           prerelease: true

.github/workflows/copyright-header.yml

@@ -6,7 +6,7 @@ jobs:
   check-lean-files:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v4
 
     - name: Verify .lean files start with a copyright header.
       run: |

.github/workflows/grove.yml

@@ -110,7 +110,7 @@ jobs:
       # material.
       - id: deploy-alias
         if: ${{ steps.should-run.outputs.should-run == 'true' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         name: Compute Alias
         with:
           result-encoding: string

.github/workflows/labels-from-comments.yml

@@ -17,7 +17,7 @@ jobs:
 
     steps:
     - name: Add label based on comment
-      uses: actions/github-script@v8
+      uses: actions/github-script@v7
       with:
         github-token: ${{ secrets.GITHUB_TOKEN }}
         script: |

.github/workflows/pr-body.yml

@@ -11,7 +11,7 @@ jobs:
     steps:
       - name: Check PR body
         if: github.event_name == 'pull_request'
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const { title, body, labels, draft } = context.payload.pull_request;

.github/workflows/pr-release.yml

@@ -48,17 +48,17 @@ jobs:
           git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
           git -C lean4.git fetch -n origin master
           git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-
+          
           # Create both the original tag and the SHA-suffixed tag
           SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
           SHORT_SHA="${SHORT_SHA:0:7}"
-
+          
           # Export the short SHA for use in subsequent steps
           echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"
 
           git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
           git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
-
+          
           git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
           git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
@@ -71,7 +71,7 @@ jobs:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -86,7 +86,7 @@ jobs:
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: softprops/action-gh-release@6da8fa9354ddfdc4aeace5fc48d7f679b5214090
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
           # There are coredumps files here as well, but all in deeper subdirectories.
@@ -101,7 +101,7 @@ jobs:
 
       - name: Report release status (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             await github.rest.repos.createCommitStatus({
@@ -115,7 +115,7 @@ jobs:
 
       - name: Report release status (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             await github.rest.repos.createCommitStatus({
@@ -129,7 +129,7 @@ jobs:
 
       - name: Add label
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             await github.rest.issues.addLabels({
@@ -200,7 +200,7 @@ jobs:
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
-
+            
             if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
               echo "force-mathlib-ci label detected, forcing CI despite issues"
               MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
@@ -301,7 +301,7 @@ jobs:
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
-
+            
             if echo "$LABELS" | grep -q "^force-manual-ci$"; then
               echo "force-manual-ci label detected, forcing CI despite issues"
               MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
@@ -368,7 +368,7 @@ jobs:
 
       - name: Report mathlib base
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' }}
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const description =
@@ -395,13 +395,12 @@ jobs:
       # Checkout the Batteries repository with all branches
       - name: Checkout Batteries repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v5
+        uses: actions/checkout@v4
         with:
           repository: leanprover-community/batteries
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
 
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
@@ -426,7 +425,7 @@ jobs:
             git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
             git add lean-toolchain
-            git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
             echo "Branch already exists, updating lean-toolchain."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
@@ -435,7 +434,7 @@ jobs:
             git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
             git add lean-toolchain
-            git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes
@@ -455,13 +454,12 @@ jobs:
       # Checkout the mathlib4 repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        uses: actions/checkout@v5
+        uses: actions/checkout@v4
         with:
           repository: leanprover-community/mathlib4-nightly-testing
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
 
       - name: install elan
         run: |
@@ -496,7 +494,7 @@ jobs:
             sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean
             lake update batteries
             git add lakefile.lean lake-manifest.json
-            git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
             echo "Branch already exists, updating lean-toolchain and bumping Batteries."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
@@ -507,7 +505,7 @@ jobs:
             git add lean-toolchain
             lake update batteries
             git add lake-manifest.json
-            git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes
@@ -526,13 +524,12 @@ jobs:
       # Checkout the reference manual repository with all branches
       - name: Checkout mathlib4 repository
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
-        uses: actions/checkout@v5
+        uses: actions/checkout@v4
         with:
           repository: leanprover/reference-manual
           token: ${{ secrets.MANUAL_PR_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
-          filter: tree:0
 
       - name: Check if tag in reference manual exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
@@ -558,7 +555,7 @@ jobs:
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
             git add lean-toolchain
             git add lakefile.lean lake-manifest.json
-            git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           else
             echo "Branch already exists, updating lean-toolchain."
             git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
@@ -568,7 +565,7 @@ jobs:
             echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
             git add lean-toolchain
             git add lake-manifest.json
-            git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes

.github/workflows/pr-title.yml

@@ -10,11 +10,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Check PR title
-        uses: actions/github-script@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
             console.log(`Message: ${msg}`)
-            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): (?![A-Z][a-z]).*[^.]($|\n\n)/.test(msg)) {
+            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(msg)) {
               core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
             }

.github/workflows/stale.yml

@@ -11,7 +11,7 @@ jobs:
   stale:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/stale@v10
+      - uses: actions/stale@v9
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

.github/workflows/update-stage0.yml

@@ -21,13 +21,11 @@ jobs:
     runs-on: nscloud-ubuntu-22.04-amd64-8x16
     env:
       CCACHE_DIR: ${{ github.workspace }}/.ccache
-      CCACHE_COMPRESS: true
-      CCACHE_MAXSIZE: 400M
     steps:
     # This action should push to an otherwise protected branch, so it
     # uses a deploy key with write permissions, as suggested at
     # https://stackoverflow.com/a/76135647/946226
-    - uses: actions/checkout@v5
+    - uses: actions/checkout@v4
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
     - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
@@ -69,19 +67,15 @@ jobs:
           build/stage1/**/*.ir
           build/stage1/**/*.c
           build/stage1/**/*.c.o*
-        key: Linux Lake-build-v4-${{ github.sha }}
+        key: Linux Lake-build-v3-${{ github.sha }}
         # fall back to (latest) previous cache
         restore-keys: |
-          Linux Lake-build-v4
+          Linux Lake-build-v3
     - if: env.should_update_stage0 == 'yes'
-      # sync options with `Linux Lake` to ensure cache reuse
-      run: |
-        mkdir -p build
-        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
+      run: cmake --preset release
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
-      run: |
-        make -j$NPROC -C build update-stage0-commit
+      run: make -j$NPROC -C build/release  update-stage0-commit
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: git show --stat

.gitignore

@@ -20,6 +20,7 @@ tasks.json
 settings.json
 .gdb_history
 .vscode/*
+!.vscode/settings.json
 script/__pycache__
 *.produced.out
 CMakeSettings.json

CMakePresets.json

@@ -41,7 +41,7 @@
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
-        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000 LSAN_OPTIONS=max_leaks=10"
+        "LEAN_TEST_VARS": "MAIN_STACK_SIZE=16000"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/sanitize"

CODEOWNERS

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

README.md

@@ -2,19 +2,19 @@ This is the repository for **Lean 4**.
 
 # About
 
-- [Quickstart](https://lean-lang.org/install/)
+- [Quickstart](https://lean-lang.org/documentation/setup/)
 - [Homepage](https://lean-lang.org)
 - [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
 - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
-- [Documentation Overview](https://lean-lang.org/learn/)
+- [Documentation Overview](https://lean-lang.org/documentation/)
 - [Language Reference](https://lean-lang.org/doc/reference/latest/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://lean-lang.org/examples/)
+- [Examples](https://lean-lang.org/lean4/doc/examples.html)
 - [External Contribution Guidelines](CONTRIBUTING.md)
 
 # Installation
 
-See [Install Lean](https://lean-lang.org/install/).
+See [Setting Up Lean](https://lean-lang.org/documentation/setup/).
 
 # Contributing
 

doc/dev/bootstrap.md

@@ -72,9 +72,6 @@ update the archived C source code of the stage 0 compiler in `stage0/src`.
 
 The github repository will automatically update stage0 on `master` once
 `src/stdlib_flags.h` and `stage0/src/stdlib_flags.h` are out of sync.
-To trigger this, modify `stage0/src/stdlib_flags.h` (e.g., by adding or changing
-a comment). When `update-stage0` runs, it will overwrite `stage0/src/stdlib_flags.h`
-with the contents of `src/stdlib_flags.h`, bringing them back in sync.
 
 NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
 Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.

doc/dev/ffi.md

@@ -52,7 +52,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
 * `Nat` and `Int` are represented by `lean_object *`.
   Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
-* A universe `Sort u`, type constructor `... → Sort u`, `Void α` or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
+* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
   Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
@@ -129,7 +129,8 @@ For all other modules imported by `lean`, the initializer is run without `builti
 Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtin_init]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
 `lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping).
 
-The initializer for module `A.B` in a package `foo` is called `initialize_foo_A_B`. For modules in the Lean core (e.g., `Init.Prelude`), the initializer is called `initialize_Init_Prelude`. Module initializers will automatically initialize any imported modules. They are also idempotent (when run with the same `builtin` flag), but not thread-safe.
+The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
+Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
 
 **Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
 
@@ -140,8 +141,8 @@ void lean_initialize_runtime_module();
 void lean_initialize();
 char ** lean_setup_args(int argc, char ** argv);
 
-lean_object * initialize_A_B(uint8_t builtin);
-lean_object * initialize_C(uint8_t builtin);
+lean_object * initialize_A_B(uint8_t builtin, lean_object *);
+lean_object * initialize_C(uint8_t builtin, lean_object *);
 ...
 
 argv = lean_setup_args(argc, argv); // if using process-related functionality
@@ -151,7 +152,7 @@ lean_initialize_runtime_module();
 lean_object * res;
 // use same default as for Lean executables
 uint8_t builtin = 1;
-res = initialize_A_B(builtin);
+res = initialize_A_B(builtin, lean_io_mk_world());
 if (lean_io_result_is_ok(res)) {
     lean_dec_ref(res);
 } else {
@@ -159,7 +160,7 @@ if (lean_io_result_is_ok(res)) {
     lean_dec(res);
     return ...;  // do not access Lean declarations if initialization failed
 }
-res = initialize_C(builtin);
+res = initialize_C(builtin, lean_io_mk_world());
 if (lean_io_result_is_ok(res)) {
 ...
 

doc/dev/index.md

@@ -99,19 +99,3 @@ on to `nightly-with-manual` branch. (It is fine to force push after rebasing.)
 CI will generate a branch of the reference manual called `lean-pr-testing-NNNN`
 in `leanprover/reference-manual`. This branch uses the toolchain for your PR,
 and will report back to the Lean PR with results from Mathlib CI.
-
-### Avoiding rebuilds for downstream projects
-
-If you want to test changes to Lean on downstream projects and would like to avoid rebuilding modules you have already built/fetched using the project's configured Lean toolchain, you can often do so as long as your build of Lean is close enough to that Lean toolchain (compatible .olean format including structure of all relevant environment extensions).
-
-To override the toolchain without rebuilding for a single command, for example `lake build` or `lake lean`, you can use the prefix
-```
-LEAN_GITHASH=$(lean --githash) lake +lean4 ...
-```
-Alternatively, use
-```
-export LEAN_GITHASH=$(lean --githash)
-export ELAN_TOOLCHAIN=lean4
-```
-to persist these changes for the lifetime of the current shell, which will affect any processes spawned from it such as VS Code started via `code .`.
-If you use a setup where you cannot directly start your editor from the command line, such as VS Code Remote, you might want to consider using [direnv](https://direnv.net/) together with an editor extension for it instead so that you can put the lines above into `.envrc`.

doc/dev/testing.md

@@ -59,7 +59,7 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     open Foo in
     theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
     Bla.
-      --^ completion
+      --^ textDocument/completion
     ```
     In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
     auto-completion request at `Bla.`. The expected output is stored in

doc/examples/palindromes.lean

@@ -94,8 +94,10 @@ theorem List.palindrome_of_eq_reverse (h : as.reverse = as) : Palindrome as := b
   next   => exact Palindrome.nil
   next a => exact Palindrome.single a
   next a b as ih =>
-    obtain ⟨rfl, h, -⟩ := by simpa using h
-    exact Palindrome.sandwich b (ih h)
+    have : a = b := by simp_all
+    subst this
+    have : as.reverse = as := by simp_all
+    exact Palindrome.sandwich a (ih this)
 
 /-!
 We now define a function that returns `true` iff `as` is a palindrome.

flake.nix

@@ -25,7 +25,6 @@
         } ({
           buildInputs = with pkgs; [
             cmake gmp libuv ccache pkg-config
-            llvmPackages.bintools  # wrapped lld
             llvmPackages.llvm  # llvm-symbolizer for asan/lsan
             gdb
             tree  # for CI

lean.code-workspace

@@ -8,15 +8,9 @@
 		},
 		{
 			"path": "tests"
-		},
-		{
-			"path": "script"
 		}
 	],
 	"settings": {
-		// Open terminal at root, not current workspace folder
-		// (there is not way to directly refer to the root folder included as `.` above)
-		"terminal.integrated.cwd": "${workspaceFolder:src}/..",
 		"files.insertFinalNewline": true,
 		"files.trimTrailingWhitespace": true,
 		"cmake.buildDirectory": "${workspaceFolder}/build/release",
@@ -43,15 +37,6 @@
 					"isDefault": true
 				}
 			},
-			{
-				"label": "build-old",
-				"type": "shell",
-				"command": "make -C build/release -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4) LAKE_EXTRA_ARGS=--old",
-				"problemMatcher": [],
-				"group": {
-					"kind": "build"
-				}
-			},
 			{
 				"label": "test",
 				"type": "shell",

releases_drafts/module-system.md

@@ -1,54 +0,0 @@
-This release introduces the Lean module system, which allows files to
-control the visibility of their contents for other files. In previous
-releases, this feature was available as a preview when the option
-`experimental.module` was set to `true`; it is now a fully supported
-feature of Lean.
-
-# Benefits
-
-Because modules reduce the amount of information exposed to other
-code, they speed up rebuilds because irrelevant changes can be
-ignored, they make it possible to be deliberate about API evolution by
-hiding details that may change from clients, they help proofs be
-checked faster by avoiding accidentally unfolding definitions, and
-they lead to smaller executable files through improved dead code
-elimination.
-
-# Visibility
-
-A source file is a module if it begins with the `module` keyword.  By
-default, declarations in a module are private; the `public` modifier
-exports them. Proofs of theorems and bodies of definitions are private
-by default even when their signatures are public; the bodies of
-definitions can be made public by adding the `@[expose]`
-attribute. Theorems and opaque constants never expose their bodies.
-
-`public section` and `@[expose] section` change the default visibility
-of declarations in the section.
-
-# Imports
-
-Modules may only import other modules. By default, `import` adds the
-public information of the imported module to the private scope of the
-current module. Adding the `public` modifier to an import places the
-imported modules's public information in the public scope of the
-current module, exposing it in turn to the current module's clients.
-
-Within a package, `import all` can be used to import another module's
-private scope into the current module; this can be used to separate
-lemmas or tests from definition modules without exposing details to
-downstream clients.
-
-# Meta Code
-
-Code used in metaprograms must be marked `meta`. This ensures that the
-code is compiled and available for execution when it is needed during
-elaboration. Meta code may only reference other meta code. A whole
-module can be made available in the meta phase using `meta import`;
-this allows code to be shared across phases by importing the module in
-each phase. Code that is reachable from public metaprograms must be
-imported via `public meta import`, while local metaprograms can use
-plain `meta import` for their dependencies.
-
-
-The module system is described in detail in [the Lean language reference](https://lean-reference-manual-review.netlify.app/find/?domain=Verso.Genre.Manual.section&name=files).

script/AnalyzeGrindAnnotations.lean

@@ -0,0 +1,132 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean
+
+namespace Lean.Meta.Grind.Analyzer
+
+
+/-!
+A simple E-matching annotation analyzer.
+For each theorem annotated as an E-matching candidate, it creates an artificial goal, executes `grind` and shows the
+number of instances created.
+For a theorem of the form `params -> type`, the artificial goal is of the form `params -> type -> False`.
+-/
+
+/--
+`grind` configuration for the analyzer. We disable case-splits and lookahead,
+increase the number of generations, and limit the number of instances generated.
+-/
+def config : Grind.Config := {
+  splits       := 0
+  lookahead    := false
+  mbtc         := false
+  ematch       := 20
+  instances    := 100
+  gen          := 10
+}
+
+structure Config where
+  /-- Minimum number of instantiations to trigger summary report -/
+  min : Nat := 10
+  /-- Minimum number of instantiations to trigger detailed report -/
+  detailed : Nat := 50
+
+def mkParams : MetaM Params := do
+  let params ← Grind.mkParams config
+  let ematch ← getEMatchTheorems
+  let casesTypes ← Grind.getCasesTypes
+  return { params with ematch, casesTypes }
+
+/-- Returns the total number of generated instances.  -/
+private def sum (cs : PHashMap Origin Nat) : Nat := Id.run do
+  let mut r := 0
+  for (_, c) in cs do
+    r := r + c
+  return r
+
+private def thmsToMessageData (thms : PHashMap Origin Nat) : MetaM MessageData := do
+  let data := thms.toArray.filterMap fun (origin, c) =>
+    match origin with
+    | .decl declName => some (declName, c)
+    | _ => none
+  let data := data.qsort fun (d₁, c₁) (d₂, c₂) => if c₁ == c₂ then Name.lt d₁ d₂ else c₁ > c₂
+  let data ← data.mapM fun (declName, counter) =>
+    return .trace { cls := `thm } m!"{.ofConst (← mkConstWithLevelParams declName)} ↦ {counter}" #[]
+  return .trace { cls := `thm } "instances" data
+
+/--
+Analyzes theorem `declName`. That is, creates the artificial goal based on `declName` type,
+and invokes `grind` on it.
+-/
+def analyzeEMatchTheorem (declName : Name) (c : Config) : MetaM Unit := do
+  let info ← getConstInfo declName
+  let mvarId ← forallTelescope info.type fun _ type => do
+    withLocalDeclD `h type fun _ => do
+      return (← mkFreshExprMVar (mkConst ``False)).mvarId!
+  let result ← Grind.main mvarId (← mkParams) (pure ())
+  let thms := result.counters.thm
+  let s := sum thms
+  if s > c.min then
+    IO.println s!"{declName} : {s}"
+  if s > c.detailed then
+    logInfo m!"{declName}\n{← thmsToMessageData thms}"
+
+-- Not sure why this is failing: `down_pure` perhaps has an unnecessary universe parameter?
+run_meta analyzeEMatchTheorem ``Std.Do.SPred.down_pure {}
+
+/-- Analyzes all theorems in the standard library marked as E-matching theorems. -/
+def analyzeEMatchTheorems (c : Config := {}) : MetaM Unit := do
+  let origins := (← getEMatchTheorems).getOrigins
+  let decls := origins.filterMap fun | .decl declName => some declName | _ => none
+  for declName in decls.mergeSort Name.lt do
+    try
+      analyzeEMatchTheorem declName c
+    catch e =>
+      logError m!"{declName} failed with {e.toMessageData}"
+  logInfo m!"Finished analyzing {decls.length} theorems"
+
+/-- Macro for analyzing E-match theorems with unlimited heartbeats -/
+macro "#analyzeEMatchTheorems" : command => `(
+  set_option maxHeartbeats 0 in
+  run_meta analyzeEMatchTheorems
+)
+
+#analyzeEMatchTheorems
+
+-- -- We can analyze specific theorems using commands such as
+set_option trace.grind.ematch.instance true
+
+-- 1. grind immediately sees `(#[] : Array α) = ([] : List α).toArray` but probably this should be hidden.
+-- 2. `Vector.toArray_empty` keys on `Array.mk []` rather than `#v[].toArray`
+-- I guess we could add `(#[].extract _ _).extract _ _` as a stop pattern.
+run_meta analyzeEMatchTheorem ``Array.extract_empty {}
+
+-- Neither `Option.bind_some` nor `Option.bind_fun_some` fire, because the terms appear inside
+-- lambdas. So we get crazy things like:
+-- `fun x => ((some x).bind some).bind fun x => (some x).bind fun x => (some x).bind some`
+-- We could consider replacing `filterMap_some` with
+-- `filterMap g (filterMap f xs) = filterMap (f >=> g) xs`
+-- to avoid the lambda that `grind` struggles with, but this would require more API around the fish.
+run_meta analyzeEMatchTheorem ``Array.filterMap_some {}
+
+-- Not entirely certain what is wrong here, but certainly
+-- `eq_empty_of_append_eq_empty` is firing too often.
+-- Ideally we could instantiate this is we fine `xs ++ ys` in the same equivalence class,
+-- note just as soon as we see `xs ++ ys`.
+-- I've tried removing this in https://github.com/leanprover/lean4/pull/10162
+run_meta analyzeEMatchTheorem ``Array.range'_succ {}
+
+-- Perhaps the same story here.
+run_meta analyzeEMatchTheorem ``Array.range_succ {}
+
+-- `zip_map_left` and `zip_map_right` are bad grind lemmas,
+-- checking if they can be removed in https://github.com/leanprover/lean4/pull/10163
+run_meta analyzeEMatchTheorem ``Array.zip_map {}
+
+-- It seems crazy to me that as soon as we have `0 >>> n = 0`, we instantiate based on the
+-- pattern `0 >>> n >>> m` by substituting `0` into `0 >>> n` to produce the `0 >>> n >>> n`.
+-- I don't think any forbidden subterms can help us here. I don't know what to do. :-(
+run_meta analyzeEMatchTheorem ``Int.zero_shiftRight {}

script/Modulize.lean

@@ -1,75 +0,0 @@
-import Lake.CLI.Main
-
-/-!
-
-Usage: `lean --run script/Modulize.lean [--meta] file1.lean file2.lean ...`
-
-A simple script that inserts `module` and `public section` into un-modulized files and
-bumps their imports to `public`.
-
-When `--meta` is passed, `public meta section` and `public meta import` is used instead.
--/
-
-open Lean Parser.Module
-
-def main (args : List String) : IO Unit := do
-  let mut args := args
-  let mut doMeta := false
-  while !args.isEmpty && args[0]!.startsWith "-" do
-    match args[0]! with
-    | "--meta" => doMeta := true
-    | arg => throw <| .userError s!"unknown flag '{arg}'"
-    args := args.tail
-
-  for path in args do
-    -- Parse the input file
-    let mut text ← IO.FS.readFile path
-    let inputCtx := Parser.mkInputContext text path
-    let (header, parserState, msgs) ← Parser.parseHeader inputCtx
-    if !msgs.toList.isEmpty then -- skip this file if there are parse errors
-      msgs.forM fun msg => msg.toString >>= IO.println
-      throw <| .userError "parse errors in file"
-    let `(header| $[module%$moduleTk?]? $imps:import*) := header
-      | throw <| .userError s!"unexpected header syntax of {path}"
-    if moduleTk?.isSome then
-      continue
-
-    -- initial whitespace if empty header
-    let startPos := header.raw.getPos? |>.getD parserState.pos
-
-    let dummyEnv ← mkEmptyEnvironment
-    let (initCmd, parserState', _) :=
-      Parser.parseCommand inputCtx { env := dummyEnv, options := {} } parserState msgs
-
-    -- insert section if any trailing command
-    if !initCmd.isOfKind ``Parser.Command.eoi then
-      let insertPos? :=
-          -- put below initial module docstring if any
-          guard (initCmd.isOfKind ``Parser.Command.moduleDoc) *> initCmd.getTailPos? <|>
-          -- else below header
-          header.raw.getTailPos?
-      let insertPos := insertPos?.getD startPos  -- empty header
-      let mut sec := if doMeta then
-        "public meta section"
-      else
-        "@[expose] public section"
-      if !imps.isEmpty then
-        sec := "\n\n" ++ sec
-      if insertPos?.isNone then
-        sec := sec ++ "\n\n"
-      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.rawEndPos
-
-    -- prepend each import with `public `
-    for imp in imps.reverse do
-      let insertPos := imp.raw.getPos?.get!
-      let prfx := if doMeta then "public meta " else "public "
-      text := text.extract 0 insertPos ++ prfx ++ text.extract insertPos text.rawEndPos
-
-    -- insert `module` header
-    let mut initText := text.extract 0 startPos
-    if !initText.trim.isEmpty then
-      -- If there is a header comment, preserve it and put `module` in the line after
-      initText := initText.trimRight ++ "\n"
-    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
-
-    IO.FS.writeFile path text

script/Shake.lean

@@ -1,616 +0,0 @@
-/-
-Copyright (c) 2023 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Sebastian Ullrich
--/
-import Lake.CLI.Main
-import Lean.ExtraModUses
-
-/-! # `lake exe shake` command
-
-This command will check the current project (or a specified target module) and all dependencies for
-unused imports. This works by looking at generated `.olean` files to deduce required imports and
-ensuring that every import is used to contribute some constant or other elaboration dependency
-recorded by `recordExtraModUse`. Because recompilation is not needed this is quite fast (about 8
-seconds to check `Mathlib` and all dependencies).
--/
-
-/-- help string for the command line interface -/
-def help : String := "Lean project tree shaking tool
-Usage: lake exe shake [OPTIONS] <MODULE>..
-
-Arguments:
-  <MODULE>
-    A module path like `Mathlib`. All files transitively reachable from the
-    provided module(s) will be checked.
-
-Options:
-  --force
-    Skips the `lake build --no-build` sanity check
-
-  --fix
-    Apply the suggested fixes directly. Make sure you have a clean checkout
-    before running this, so you can review the changes.
-"
-
-open Lean
-
-/-- We use `Nat` as a bitset for doing efficient set operations.
-The bit indexes will usually be a module index. -/
-structure Bitset where
-  toNat : Nat
-deriving Inhabited, DecidableEq, Repr
-
-namespace Bitset
-
-instance : EmptyCollection Bitset where
-  emptyCollection := { toNat := 0 }
-
-instance : Insert Nat Bitset where
-  insert i s := { toNat := s.toNat ||| (1 <<< i) }
-
-instance : Singleton Nat Bitset where
-  singleton i := insert i ∅
-
-instance : Inter Bitset where
-  inter a b := { toNat := a.toNat &&& b.toNat }
-
-instance : Union Bitset where
-  union a b := { toNat := a.toNat ||| b.toNat }
-
-instance : XorOp Bitset where
-  xor a b := { toNat := a.toNat ^^^ b.toNat }
-
-def has (s : Bitset) (i : Nat) : Bool := s ∩ {i} ≠ ∅
-
-end Bitset
-
-/-- The kind of a module dependency, corresponding to the homonymous `ExtraModUse` fields. -/
-structure NeedsKind where
-  isExported : Bool
-  isMeta : Bool
-deriving Inhabited, BEq, Repr, Hashable
-
-namespace NeedsKind
-
-@[match_pattern]  abbrev priv : NeedsKind := { isExported := false, isMeta := false }
-@[match_pattern]  abbrev pub  : NeedsKind := { isExported := true,  isMeta := false }
-@[match_pattern]  abbrev metaPriv : NeedsKind := { isExported := false, isMeta := true }
-@[match_pattern]  abbrev metaPub  : NeedsKind := { isExported := true,  isMeta := true }
-
-def all : Array NeedsKind := #[pub, priv, metaPub, metaPriv]
-
-def ofImport : Lean.Import → NeedsKind
-  | { isExported := true, isMeta := true, .. } => .metaPub
-  | { isExported := true, isMeta := false, .. } => .pub
-  | { isExported := false, isMeta := true, .. } => .metaPriv
-  | { isExported := false, isMeta := false, .. } => .priv
-
-end NeedsKind
-
-/-- Logically, a map `NeedsKind → Bitset`. -/
-structure Needs where
-  pub : Bitset
-  priv : Bitset
-  metaPub : Bitset
-  metaPriv : Bitset
-deriving Inhabited, Repr
-
-def Needs.empty : Needs := default
-
-def Needs.get (needs : Needs) (k : NeedsKind) : Bitset :=
-  match k with
-  | .pub => needs.pub
-  | .priv => needs.priv
-  | .metaPub => needs.metaPub
-  | .metaPriv => needs.metaPriv
-
-def Needs.has (needs : Needs) (k : NeedsKind) (i : ModuleIdx) : Bool :=
-  needs.get k |>.has i
-
-def Needs.set (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
-  match k with
-  | .pub   => { needs with pub := s }
-  | .priv  => { needs with priv := s }
-  | .metaPub => { needs with metaPub := s }
-  | .metaPriv => { needs with metaPriv := s }
-
-def Needs.modify (needs : Needs) (k : NeedsKind) (f : Bitset → Bitset) : Needs :=
-  needs.set k (f (needs.get k))
-
-def Needs.union (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
-  needs.modify k (· ∪ s)
-
-def Needs.sub (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
-  needs.modify k (fun s' => s' ^^^ (s' ∩ s))
-
-/-- The main state of the checker, containing information on all loaded modules. -/
-structure State where
-  env  : Environment
-  /--
-  `transDeps[i]` is the (non-reflexive) transitive closure of `mods[i].imports`. More specifically,
-  * `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
-  * `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
-  * `j ∈ transDeps[i].priv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].pub/priv`
-  * `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import)->* j`
-  * `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import)->* j`
-  * `j ∈ transDeps[i].metaPriv` if `i -(import ...)-> i'` and `j ∈ transDeps[i'].metaPub`
-  * `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].metaPub/metaPriv`
-  -/
-  transDeps : Array Needs := #[]
-  /--
-  `transDepsOrig` is the initial value of `transDeps` before changes potentially resulting from
-  changes to upstream headers.
-  -/
-  transDepsOrig : Array Needs := #[]
-
-def State.mods (s : State) := s.env.header.moduleData
-def State.modNames (s : State) := s.env.header.moduleNames
-
-/--
-Given module `j`'s transitive dependencies, computes the union of `transImps` and the transitive
-dependencies resulting from importing the module via `imp` according to the rules of
-`State.transDeps`.
--/
-def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps : Needs) : Needs := Id.run do
-  let mut transImps := transImps
-
-  -- `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
-  if imp.isExported && !imp.isMeta then
-    transImps := transImps.union .pub {j} |>.union .pub (impTransImps.get .pub)
-
-  if !imp.isExported && !imp.isMeta then
-    -- `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
-    transImps := transImps.union .priv {j} |>.union .priv (impTransImps.get .pub)
-    if imp.importAll then
-      -- `j ∈ transDeps[i].priv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].pub/priv`
-      transImps := transImps.union .priv (impTransImps.get .pub ∪ impTransImps.get .priv)
-
-  -- `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import)->* j`
-  if imp.isExported then
-    transImps := transImps.union .metaPub (impTransImps.get .metaPub)
-    if imp.isMeta then
-      transImps := transImps.union .metaPub {j} |>.union .metaPub (impTransImps.get .pub ∪ impTransImps.get .metaPub)
-
-  if !imp.isExported then
-    if imp.isMeta then
-      -- `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import)->* j`
-      transImps := transImps.union .metaPriv {j} |>.union .metaPriv (impTransImps.get .pub ∪ impTransImps.get .metaPub)
-    if imp.importAll then
-      -- `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].metaPub/metaPriv`
-      transImps := transImps.union .metaPriv (impTransImps.get .metaPub ∪ impTransImps.get .metaPriv)
-    else
-      -- `j ∈ transDeps[i].metaPriv` if `i -(import ...)-> i'` and `j ∈ transDeps[i'].metaPub`
-      transImps := transImps.union .metaPriv (impTransImps.get .metaPub)
-
-  transImps
-
-/-- Calculates the needs for a given module `mod` from constants and recorded extra uses. -/
-def calcNeeds (env : Environment) (i : ModuleIdx) : Needs := Id.run do
-  let mut needs := default
-  for ci in env.header.moduleData[i]!.constants do
-    -- Added guard for cases like `structure` that are still exported even if private
-    let pubCI? := guard (!isPrivateName ci.name) *> (env.setExporting true).find? ci.name
-    let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
-    needs := visitExpr k ci.type needs
-    if let some e := ci.value? (allowOpaque := true) then
-      -- type and value has identical visibility under `meta`
-      let k := if k.isMeta then k else
-        if pubCI?.any (·.hasValue (allowOpaque := true)) then .pub else .priv
-      needs := visitExpr k e needs
-
-  for use in getExtraModUses env i do
-    let j := env.getModuleIdx? use.module |>.get!
-    needs := needs.union { use with } {j}
-
-  return needs
-where
-  /-- Accumulate the results from expression `e` into `deps`. -/
-  visitExpr (k : NeedsKind) e deps :=
-    Lean.Expr.foldConsts e deps fun c deps => match env.getModuleIdxFor? c with
-      | some j =>
-        let k := { k with isMeta := k.isMeta && !isMeta env c }
-        if j != i then deps.union k {j} else deps
-      | _ => deps
-
-/--
-Calculates the same as `calcNeeds` but tracing each module to a use-def declaration pair or
-`none` if merely a recorded extra use.
--/
-def getExplanations (env : Environment) (i : ModuleIdx) :
-    Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name)) := Id.run do
-  let mut deps := default
-  for ci in env.header.moduleData[i]!.constants do
-    -- Added guard for cases like `structure` that are still exported even if private
-    let pubCI? := guard (!isPrivateName ci.name) *> (env.setExporting true).find? ci.name
-    let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
-    deps := visitExpr k ci.name ci.type deps
-    if let some e := ci.value? (allowOpaque := true) then
-      let k := if k.isMeta then k else
-        if pubCI?.any (·.hasValue (allowOpaque := true)) then .pub else .priv
-      deps := visitExpr k ci.name e deps
-
-  for use in getExtraModUses env i do
-    let j := env.getModuleIdx? use.module |>.get!
-    if !deps.contains (j, { use with }) then
-      deps := deps.insert (j, { use with }) none
-
-  return deps
-where
-  /-- Accumulate the results from expression `e` into `deps`. -/
-  visitExpr (k : NeedsKind) name e deps :=
-    Lean.Expr.foldConsts e deps fun c deps => match env.getModuleIdxFor? c with
-      | some i =>
-        let k := { k with isMeta := k.isMeta && !isMeta env c }
-        if
-          if let some (some (name', _)) := deps[(i, k)]? then
-            decide (name.toString.length < name'.toString.length)
-          else true
-        then
-          deps.insert (i, k) (name, c)
-        else
-          deps
-      | _ => deps
-
-partial def initStateFromEnv (env : Environment) : State := Id.run do
-  let mut s := { env }
-  for i in 0...env.header.moduleData.size do
-    let mod := env.header.moduleData[i]!
-    let mut imps := #[]
-    let mut transImps := Needs.empty
-    for imp in mod.imports do
-      let j := env.getModuleIdx? imp.module |>.get!
-      imps := imps.push j
-      transImps := addTransitiveImps transImps imp j s.transDeps[j]!
-    s := { s with transDeps := s.transDeps.push transImps }
-  s := { s with transDepsOrig := s.transDeps }
-  return s
-
-/-- The list of edits that will be applied in `--fix`. `edits[i] = (removed, added)` where:
-
-* If `j ∈ removed` then we want to delete module named `j` from the imports of `i`
-* If `j ∈ added` then we want to add module index `j` to the imports of `i`.
--/
-abbrev Edits := Std.HashMap Name (Array Import × Array Import)
-
-/-- Register that we want to remove `tgt` from the imports of `src`. -/
-def Edits.remove (ed : Edits) (src : Name) (tgt : Import) : Edits :=
-  match ed.get? src with
-  | none => ed.insert src (#[tgt], #[])
-  | some (a, b) => ed.insert src (a.push tgt, b)
-
-/-- Register that we want to add `tgt` to the imports of `src`. -/
-def Edits.add (ed : Edits) (src : Name) (tgt : Import) : Edits :=
-  match ed.get? src with
-  | none => ed.insert src (#[], #[tgt])
-  | some (a, b) => ed.insert src (a, b.push tgt)
-
-/-- Parse a source file to extract the location of the import lines, for edits and error messages.
-
-Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
-and `endPos` is the position of the end of the header.
--/
-def parseHeaderFromString (text path : String) :
-    IO (System.FilePath × Parser.InputContext ×
-      TSyntax ``Parser.Module.header × String.Pos.Raw) := do
-  let inputCtx := Parser.mkInputContext text path
-  let (header, parserState, msgs) ← Parser.parseHeader inputCtx
-  if !msgs.toList.isEmpty then -- skip this file if there are parse errors
-    msgs.forM fun msg => msg.toString >>= IO.println
-    throw <| .userError "parse errors in file"
-  -- the insertion point for `add` is the first newline after the imports
-  let insertion := header.raw.getTailPos?.getD parserState.pos
-  let insertion := text.findAux (· == '\n') text.rawEndPos insertion + '\n'
-  pure (path, inputCtx, header, insertion)
-
-/-- Parse a source file to extract the location of the import lines, for edits and error messages.
-
-Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
-and `endPos` is the position of the end of the header.
--/
-def parseHeader (srcSearchPath : SearchPath) (mod : Name) :
-    IO (System.FilePath × Parser.InputContext ×
-      TSyntax ``Parser.Module.header × String.Pos.Raw) := do
-  -- Parse the input file
-  let some path ← srcSearchPath.findModuleWithExt "lean" mod
-    | throw <| .userError s!"error: failed to find source file for {mod}"
-  let text ← IO.FS.readFile path
-  parseHeaderFromString text path.toString
-
-def decodeHeader : TSyntax ``Parser.Module.header → Option (TSyntax `module) × Option (TSyntax `prelude) × TSyntaxArray ``Parser.Module.import
-  | `(Parser.Module.header| $[module%$moduleTk?]? $[prelude%$preludeTk?]? $imports*) =>
-    (moduleTk?.map .mk, preludeTk?.map .mk, imports)
-  | _ => unreachable!
-
-def decodeImport : TSyntax ``Parser.Module.import → Import
-  | `(Parser.Module.import| $[public%$pubTk?]? $[meta%$metaTk?]? import $[all%$allTk?]? $id) =>
-    { module := id.getId, isExported := pubTk?.isSome, isMeta := metaTk?.isSome, importAll := allTk?.isSome }
-  | stx => panic! s!"unexpected syntax {stx}"
-
-/-- Analyze and report issues from module `i`. Arguments:
-
-* `srcSearchPath`: Used to find the path for error reporting purposes
-* `i`: the module index
-* `needs`: the module's calculated needs
-* `pinned`: dependencies that should be preserved even if unused
-* `edits`: accumulates the list of edits to apply if `--fix` is true
-* `addOnly`: if true, only add missing imports, do not remove unused ones
--/
-def visitModule (srcSearchPath : SearchPath)
-    (i : Nat) (needs : Needs) (preserve : Needs) (edits : Edits) (headerStx : TSyntax ``Parser.Module.header)
-    (addOnly := false) (githubStyle := false) (explain := false) : StateT State IO Edits := do
-  let s ← get
-  -- Do transitive reduction of `needs` in `deps`.
-  let mut deps := needs
-  let (_, prelude?, imports) := decodeHeader headerStx
-  if prelude?.isNone then
-    deps := deps.union .pub {s.env.getModuleIdx? `Init |>.get!}
-  for imp in imports do
-    if addOnly || imp.raw.getTrailing?.any (·.toString.toSlice.contains "shake: keep") then
-      let imp := decodeImport imp
-      let j := s.env.getModuleIdx? imp.module |>.get!
-      let k := NeedsKind.ofImport imp
-      deps := deps.union k {j}
-  for j in [0:s.mods.size] do
-    let transDeps := s.transDeps[j]!
-    for k in NeedsKind.all do
-      if s.transDepsOrig[i]!.has k j && preserve.has k j then
-        deps := deps.union k {j}
-      if deps.has k j then
-        let transDeps := addTransitiveImps .empty { k with module := .anonymous } j transDeps
-        for k' in NeedsKind.all do
-          deps := deps.sub k' (transDeps.sub k' {j} |>.get k')
-
-  -- Any import which is not in `transDeps` was unused.
-  -- Also accumulate `newDeps` which is the transitive closure of the remaining imports
-  let mut toRemove : Array Import := #[]
-  let mut newDeps := Needs.empty
-  for imp in s.mods[i]!.imports do
-    let j := s.env.getModuleIdx? imp.module |>.get!
-    if
-        -- skip folder-nested imports
-        s.modNames[i]!.isPrefixOf imp.module ||
-        imp.importAll then
-      newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
-    else
-      let k := NeedsKind.ofImport imp
-      -- A private import should also be removed if the public version is needed
-      if !deps.has k j || !k.isExported && deps.has { k with isExported := true } j then
-        toRemove := toRemove.push imp
-      else
-        newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
-
-  -- If `newDeps` does not cover `deps`, then we have to add back some imports until it does.
-  -- To minimize new imports we pick only new imports which are not transitively implied by
-  -- another new import
-  let mut toAdd : Array Import := #[]
-  for j in [0:s.mods.size] do
-    for k in NeedsKind.all do
-      if deps.has k j && !newDeps.has k j && !newDeps.has { k with isExported := true } j then
-        let imp := { k with module := s.modNames[j]! }
-        toAdd := toAdd.push imp
-        newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
-
-  -- mark and report the removals
-  let mut edits := toRemove.foldl (init := edits) fun edits imp =>
-    edits.remove s.modNames[i]! imp
-
-  if !toAdd.isEmpty || !toRemove.isEmpty || explain then
-    if let some path ← srcSearchPath.findModuleWithExt "lean" s.modNames[i]! then
-      println! "{path}:"
-    else
-      println! "{s.modNames[i]!}:"
-
-  if !toRemove.isEmpty then
-    println! "  remove {toRemove}"
-
-  if githubStyle then
-    try
-      let (path, inputCtx, stx, endHeader) ← parseHeader srcSearchPath s.modNames[i]!
-      let (_, _, imports) := decodeHeader stx
-      for stx in imports do
-        if toRemove.any fun imp => imp == decodeImport stx then
-          let pos := inputCtx.fileMap.toPosition stx.raw.getPos?.get!
-          println! "{path}:{pos.line}:{pos.column+1}: warning: unused import \
-            (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)"
-      if !toAdd.isEmpty then
-        -- we put the insert message on the beginning of the last import line
-        let pos := inputCtx.fileMap.toPosition endHeader
-        println! "{path}:{pos.line-1}:1: warning: \
-          add {toAdd} instead"
-    catch _ => pure ()
-
-  -- mark and report the additions
-  edits := toAdd.foldl (init := edits) fun edits imp =>
-    edits.add s.modNames[i]! imp
-
-  if !toAdd.isEmpty then
-    println! "  add {toAdd}"
-
-  -- recalculate transitive dependencies of downstream modules
-  let mut newTransDepsI := Needs.empty
-  for imp in s.mods[i]!.imports do
-    if !toRemove.contains imp then
-      let j := s.env.getModuleIdx? imp.module |>.get!
-      newTransDepsI := addTransitiveImps newTransDepsI imp j s.transDeps[j]!
-  for imp in toAdd do
-    let j := s.env.getModuleIdx? imp.module |>.get!
-    newTransDepsI := addTransitiveImps newTransDepsI imp j s.transDeps[j]!
-
-  set { s with transDeps := s.transDeps.set! i newTransDepsI }
-
-  if explain then
-    let explanation := getExplanations s.env i
-    let sanitize n := if n.hasMacroScopes then (sanitizeName n).run' { options := {} } else n
-    let run (imp : Import) := do
-      let j := s.env.getModuleIdx? imp.module |>.get!
-      if let some exp? := explanation[(j, NeedsKind.ofImport imp)]? then
-        println! "  note: `{imp}` required"
-        if let some (n, c) := exp? then
-          println! "    because `{sanitize n}` refers to `{sanitize c}`"
-        else
-          println! "    because of additional compile-time dependencies"
-    for j in s.mods[i]!.imports do
-      if !toRemove.contains j then
-        run j
-    for i in toAdd do run i
-
-  return edits
-
-/-- Convert a list of module names to a bitset of module indexes -/
-def toBitset (s : State) (ns : List Name) : Bitset :=
-  ns.foldl (init := ∅) fun c name =>
-    match s.env.getModuleIdxFor? name with
-    | some i => c ∪ {i}
-    | none => c
-
-/-- The parsed CLI arguments. See `help` for more information -/
-structure Args where
-  /-- `--help`: shows the help -/
-  help : Bool := false
-  /-- `--force`: skips the `lake build --no-build` sanity check -/
-  force : Bool := false
-  /-- `--gh-style`: output messages that can be parsed by `gh-problem-matcher-wrap` -/
-  githubStyle : Bool := false
-  /-- `--explain`: give constants explaining why each module is needed -/
-  explain : Bool := false
-  /-- `--fix`: apply the fixes directly -/
-  fix : Bool := false
-  /-- `<MODULE>..`: the list of root modules to check -/
-  mods : Array Name := #[]
-
-local instance : Ord Import where
-  compare a b :=
-    if a.isExported && !b.isExported then
-      Ordering.lt
-    else if !a.isExported && b.isExported then
-      Ordering.gt
-    else
-      a.module.cmp b.module
-
-/-- The main entry point. See `help` for more information on arguments. -/
-def main (args : List String) : IO UInt32 := do
-  initSearchPath (← findSysroot)
-  -- Parse the arguments
-  let rec parseArgs (args : Args) : List String → Args
-    | [] => args
-    | "--help" :: rest => parseArgs { args with help := true } rest
-    | "--force" :: rest => parseArgs { args with force := true } rest
-    | "--fix" :: rest => parseArgs { args with fix := true } rest
-    | "--explain" :: rest => parseArgs { args with explain := true } rest
-    | "--gh-style" :: rest => parseArgs { args with githubStyle := true } rest
-    | "--" :: rest => { args with mods := args.mods ++ rest.map (·.toName) }
-    | other :: rest => parseArgs { args with mods := args.mods.push other.toName } rest
-  let args := parseArgs {} args
-
-  -- Bail if `--help` is passed
-  if args.help then
-    IO.println help
-    IO.Process.exit 0
-
-  if !args.force then
-    if (← IO.Process.output { cmd := "lake", args := #["build", "--no-build"] }).exitCode != 0 then
-      IO.println "There are out of date oleans. Run `lake build` or `lake exe cache get` first"
-      IO.Process.exit 1
-
-  -- Determine default module(s) to run shake on
-  let defaultTargetModules : Array Name ← try
-    let (elanInstall?, leanInstall?, lakeInstall?) ← Lake.findInstall?
-    let config ← Lake.MonadError.runEIO <| Lake.mkLoadConfig { elanInstall?, leanInstall?, lakeInstall? }
-    let some workspace ← Lake.loadWorkspace config |>.toBaseIO
-      | throw <| IO.userError "failed to load Lake workspace"
-    let defaultTargetModules := workspace.root.defaultTargets.flatMap fun target =>
-      if let some lib := workspace.root.findLeanLib? target then
-        lib.roots
-      else if let some exe := workspace.root.findLeanExe? target then
-        #[exe.config.root]
-      else
-        #[]
-    pure defaultTargetModules
-  catch _ =>
-    pure #[]
-
-  let srcSearchPath ← getSrcSearchPath
-  -- the list of root modules
-  let mods := if args.mods.isEmpty then defaultTargetModules else args.mods
-  -- Only submodules of `pkg` will be edited or have info reported on them
-  let pkg := mods[0]!.components.head!
-
-  -- Load all the modules
-  let imps := mods.map ({ module := · })
-  let (_, s) ← importModulesCore imps (isExported := true) |>.run
-  let s := s.markAllExported
-  let env ← finalizeImport s (isModule := true) imps {} (leakEnv := false) (loadExts := false)
-
-  StateT.run' (s := initStateFromEnv env) do
-
-  let s ← get
-  -- Parse the config file
-
-  -- Run the calculation of the `needs` array in parallel
-  let needs := s.mods.mapIdx fun i _ =>
-    Task.spawn fun _ => calcNeeds s.env i
-
-  -- Parse headers in parallel
-  let headers ← s.mods.mapIdxM fun i _ =>
-    BaseIO.asTask (parseHeader srcSearchPath s.modNames[i]! |>.toBaseIO)
-
-  if args.fix then
-    println! "The following changes will be made automatically:"
-
-  -- Check all selected modules
-  let mut edits : Edits := ∅
-  let mut revNeeds : Needs := default
-  for i in [0:s.mods.size], t in needs, header in headers do
-    match header.get with
-    | .ok (_, _, stx, _) =>
-      edits ← visitModule (addOnly := !pkg.isPrefixOf s.modNames[i]!)
-        srcSearchPath i t.get revNeeds edits stx args.githubStyle args.explain
-      if isExtraRevModUse s.env i then
-        revNeeds := revNeeds.union .priv {i}
-    | .error e =>
-      println! e.toString
-
-  if !args.fix then
-    -- return error if any issues were found
-    return if edits.isEmpty then 0 else 1
-
-  -- Apply the edits to existing files
-  let mut count := 0
-  for mod in s.modNames, header? in headers do
-    let some (remove, add) := edits[mod]? | continue
-    let add : Array Import := add.qsortOrd
-
-    -- Parse the input file
-    let .ok (path, inputCtx, stx, insertion) := header?.get | continue
-    let (_, _, imports) := decodeHeader stx
-    let text := inputCtx.fileMap.source
-
-    -- Calculate the edit result
-    let mut pos : String.Pos.Raw := 0
-    let mut out : String := ""
-    let mut seen : Std.HashSet Import := {}
-    for stx in imports do
-      let mod := decodeImport stx
-      if remove.contains mod || seen.contains mod then
-        out := out ++ String.Pos.Raw.extract text pos stx.raw.getPos?.get!
-        -- We use the end position of the syntax, but include whitespace up to the first newline
-        pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + '\n'
-      seen := seen.insert mod
-    out := out ++ String.Pos.Raw.extract text pos insertion
-    for mod in add do
-      if !seen.contains mod then
-        seen := seen.insert mod
-        out := out ++ s!"{mod}\n"
-    out := out ++ String.Pos.Raw.extract text insertion text.rawEndPos
-
-    IO.FS.writeFile path out
-    count := count + 1
-
-  -- Since we throw an error upon encountering issues, we can be sure that everything worked
-  -- if we reach this point of the script.
-  if count > 0 then
-    println! "Successfully applied {count} suggestions."
-  else
-    println! "No edits required."
-  return 0

script/apply.lean

@@ -60,7 +60,7 @@ if (arity == fixed + {n}) \{
   for j in [n:max + 1] do
     let fs := mkFsArgs (j - n)
     let sep := if j = n then "" else ", "
-    emit s!"    case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_object(f); return r; }\n"
+    emit s!"    case {j}: \{ obj* r = FN{j}(f)({fs}{sep}{args}); lean_free_small_object(f); return r; }\n"
   emit "    }
   }
   switch (arity) {\n"
@@ -162,7 +162,7 @@ static obj* fix_args(obj* f, unsigned n, obj*const* as) {
       for (unsigned i = 0; i < fixed; i++, source++, target++) {
           *target = *source;
       }
-      lean_free_object(f);
+      lean_free_small_object(f);
     }
     for (unsigned i = 0; i < n; i++, as++, target++) {
         *target = *as;

script/bench.sh

@@ -0,0 +1,96 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+cmake --preset release 1>&2
+
+# We benchmark against stage2/bin to test new optimizations.
+timeout -s KILL 1h time make -C build/release -j$(nproc) stage3 1>&2
+export PATH=$PWD/build/release/stage2/bin:$PATH
+
+# The extra opts used to be passed to the Makefile during benchmarking only but with Lake it is
+# easier to configure them statically.
+cmake -B build/release/stage3 -S src -DLEAN_EXTRA_LAKEFILE_TOML='weakLeanArgs=["-Dprofiler=true", "-Dprofiler.threshold=9999999", "--stats"]' 1>&2
+
+(
+cd tests/bench
+timeout -s KILL 1h time temci exec --config speedcenter.yaml --in speedcenter.exec.velcom.yaml 1>&2
+temci report run_output.yaml --reporter codespeed2
+)
+
+if [ -d .git ]; then
+    DIR="$(git rev-parse @)"
+    BASE_URL="https://speed.lean-lang.org/lean4-out/$DIR"
+    {
+        cat <<'EOF'
+<!DOCTYPE html>
+<html>
+<head>
+  <meta charset="UTF-8">
+  <title>Lakeprof Report</title>
+</head>
+<h1>Lakeprof Report</h1>
+<button type="button" id="btn_fetch">View build trace in Perfetto</button>
+<script type="text/javascript">
+const ORIGIN = 'https://ui.perfetto.dev';
+
+const btnFetch = document.getElementById('btn_fetch');
+
+async function fetchAndOpen(traceUrl) {
+  const resp = await fetch(traceUrl);
+  // Error checking is left as an exercise to the reader.
+  const blob = await resp.blob();
+  const arrayBuffer = await blob.arrayBuffer();
+  openTrace(arrayBuffer, traceUrl);
+}
+
+function openTrace(arrayBuffer, traceUrl) {
+  const win = window.open(ORIGIN);
+  if (!win) {
+    btnFetch.style.background = '#f3ca63';
+  	btnFetch.onclick = () => openTrace(arrayBuffer);
+    btnFetch.innerText = 'Popups blocked, click here to open the trace file';
+    return;
+  }
+
+  const timer = setInterval(() => win.postMessage('PING', ORIGIN), 50);
+
+  const onMessageHandler = (evt) => {
+    if (evt.data !== 'PONG') return;
+
+    // We got a PONG, the UI is ready.
+    window.clearInterval(timer);
+    window.removeEventListener('message', onMessageHandler);
+
+    const reopenUrl = new URL(location.href);
+    reopenUrl.hash = `#reopen=${traceUrl}`;
+    win.postMessage({
+      perfetto: {
+        buffer: arrayBuffer,
+        title: 'Lake Build Trace',
+        url: reopenUrl.toString(),
+    }}, ORIGIN);
+  };
+
+  window.addEventListener('message', onMessageHandler);
+}
+
+// This is triggered when following the link from the Perfetto UI's sidebar.
+if (location.hash.startsWith('#reopen=')) {
+ const traceUrl = location.hash.substr(8);
+ fetchAndOpen(traceUrl);
+}
+EOF
+        cat <<EOF
+btnFetch.onclick = () => fetchAndOpen("$BASE_URL/lakeprof.trace_event");
+</script>
+EOF
+        echo "<pre><code>"
+        (cd src; lakeprof report -prc)
+        echo "</code></pre>"
+        echo "</body></html>"
+    } | tee index.html
+
+    curl -T index.html $BASE_URL/index.html
+    curl -T src/lakeprof.log $BASE_URL/lakeprof.log
+    curl -T src/lakeprof.trace_event $BASE_URL/lakeprof.trace_event
+fi

script/benchReelabRss.lean

@@ -10,16 +10,6 @@ Tests language server memory use by repeatedly re-elaborate a given file.
 NOTE: only works on Linux for now.
 -/
 
-def determineRSS (pid : UInt32) : IO Nat := do
-  let status ← IO.FS.readFile s!"/proc/{pid}/smaps_rollup"
-  let some rssLine := status.splitOn "\n" |>.find? (·.startsWith "Rss:")
-    | throw <| IO.userError "No RSS in proc status"
-  let rssLine := rssLine.dropPrefix "Rss:"
-  let rssLine := rssLine.dropWhile Char.isWhitespace
-  let some rssInKB := rssLine.takeWhile Char.isDigit |>.toNat?
-    | throw <| IO.userError "Cannot parse RSS"
-  return rssInKB
-
 def main (args : List String) : IO Unit := do
   let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
   let file ← IO.FS.realPath file
@@ -44,14 +34,11 @@ def main (args : List String) : IO Unit := do
     let text ← IO.FS.readFile file
     let (_, headerEndPos, _) ← Elab.parseImports text
     let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
-    let n := iters.toNat!
-    let mut lastRSS? : Option Nat := none
-    let mut totalRSSDelta : Int := 0
     let mut requestNo : Nat := 1
     let mut versionNo : Nat := 1
     Ipc.writeNotification ⟨"textDocument/didOpen", {
       textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }⟩
-    for i in [0:n] do
+    for i in [0:iters.toNat!] do
       if i > 0 then
         versionNo := versionNo + 1
         let params : DidChangeTextDocumentParams := {
@@ -74,16 +61,9 @@ def main (args : List String) : IO Unit := do
           IO.eprintln diag.message
       requestNo := requestNo + 1
 
-      let rss ← determineRSS (← read).pid
-      -- The first `didChange` usually results in a significantly higher RSS increase than
-      -- the others, so we ignore it.
-      if i > 1 then
-        if let some lastRSS := lastRSS? then
-          totalRSSDelta := totalRSSDelta + ((rss : Int) - (lastRSS : Int))
-      lastRSS? := some rss
-
-    let avgRSSDelta := totalRSSDelta / (n - 2)
-    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
+      let status ← IO.FS.readFile s!"/proc/{(← read).pid}/status"
+      for line in status.splitOn "\n" |>.filter (·.startsWith "RssAnon") do
+        IO.eprintln line
 
     let _ ← Ipc.collectDiagnostics requestNo uri versionNo
     (← Ipc.stdin).writeLspMessage (Message.notification "exit" none)

script/benchReelabWatchdogRss.lean

@@ -1,89 +0,0 @@
-import Lean.Data.Lsp
-import Lean.Elab.Import
-open Lean
-open Lean.Lsp
-open Lean.JsonRpc
-
-/-!
-Tests watchdog memory use by repeatedly re-elaborate a given file.
-
-NOTE: only works on Linux for now.
--/
-
-def determineRSS (pid : UInt32) : IO Nat := do
-  let status ← IO.FS.readFile s!"/proc/{pid}/smaps_rollup"
-  let some rssLine := status.splitOn "\n" |>.find? (·.startsWith "Rss:")
-    | throw <| IO.userError "No RSS in proc status"
-  let rssLine := rssLine.dropPrefix "Rss:"
-  let rssLine := rssLine.dropWhile Char.isWhitespace
-  let some rssInKB := rssLine.takeWhile Char.isDigit |>.toNat?
-    | throw <| IO.userError "Cannot parse RSS"
-  return rssInKB
-
-def main (args : List String) : IO Unit := do
-  let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
-  let file ← IO.FS.realPath file
-  let uri := s!"file://{file}"
-  Ipc.runWith leanCmd (#["--server", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
-    let capabilities := {
-      textDocument? := some {
-        completion? := some {
-          completionItem? := some {
-            insertReplaceSupport? := true
-          }
-        }
-      }
-    }
-    Ipc.writeRequest ⟨0, "initialize", { capabilities : InitializeParams }⟩
-    discard <| Ipc.readResponseAs 0 InitializeResult
-    Ipc.writeNotification ⟨"initialized", InitializedParams.mk⟩
-
-    let text ← IO.FS.readFile file
-    let (_, headerEndPos, _) ← Elab.parseImports text
-    let headerEndPos := FileMap.ofString text |>.leanPosToLspPos headerEndPos
-    let n := iters.toNat!
-    let mut lastRSS? : Option Nat := none
-    let mut totalRSSDelta : Int := 0
-    let mut requestNo : Nat := 1
-    let mut versionNo : Nat := 1
-    Ipc.writeNotification ⟨"textDocument/didOpen", {
-      textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }⟩
-    for i in [0:iters.toNat!] do
-      if i > 0 then
-        versionNo := versionNo + 1
-        let params : DidChangeTextDocumentParams := {
-          textDocument := {
-            uri      := uri
-            version? := versionNo
-          }
-          contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
-            start := headerEndPos
-            «end» := headerEndPos
-          } " "]
-        }
-        let params := toJson params
-        Ipc.writeNotification ⟨"textDocument/didChange", params⟩
-        requestNo := requestNo + 1
-
-      let diags ← Ipc.collectDiagnostics requestNo uri versionNo
-      if let some diags := diags then
-        for diag in diags.param.diagnostics do
-          IO.eprintln diag.message
-      requestNo := requestNo + 1
-
-      Ipc.waitForILeans requestNo uri versionNo
-
-      let rss ← determineRSS (← read).pid
-      -- The first `didChange` usually results in a significantly higher RSS increase than
-      -- the others, so we ignore it.
-      if i > 1 then
-        if let some lastRSS := lastRSS? then
-          totalRSSDelta := totalRSSDelta + ((rss : Int) - (lastRSS : Int))
-      lastRSS? := some rss
-
-    let avgRSSDelta := totalRSSDelta / (n - 2)
-    IO.println s!"avg-reelab-rss-delta: {avgRSSDelta}"
-
-    let _ ← Ipc.collectDiagnostics requestNo uri versionNo
-    Ipc.shutdown requestNo
-    discard <| Ipc.waitForExit

script/lakefile.toml

@@ -1,9 +0,0 @@
-name = "scripts"
-
-[[lean_exe]]
-name = "modulize"
-root = "Modulize"
-
-[[lean_exe]]
-name = "shake"
-root = "Shake"

script/lean-toolchain

@@ -1 +0,0 @@
-lean4

script/merge_remote.py

@@ -5,7 +5,6 @@ Merge a tag into a branch on a GitHub repository.
 
 This script checks if a specified tag can be merged cleanly into a branch and performs
 the merge if possible. If the merge cannot be done cleanly, it prints a helpful message.
-Merge conflicts in the lean-toolchain file are automatically resolved by accepting the incoming changes.
 
 Usage:
     python3 merge_remote.py <org/repo> <branch> <tag>
@@ -59,32 +58,6 @@ def clone_repo(repo, temp_dir):
     return True
 
 
-def get_conflicted_files():
-    """Get list of files with merge conflicts."""
-    result = run_command("git diff --name-only --diff-filter=U", check=False)
-    if result.returncode == 0:
-        return result.stdout.strip().split('\n') if result.stdout.strip() else []
-    return []
-
-
-def resolve_lean_toolchain_conflict(tag):
-    """Resolve lean-toolchain conflict by accepting incoming (tag) changes."""
-    print("Resolving lean-toolchain conflict by accepting incoming changes...")
-    # Accept theirs (incoming) version for lean-toolchain
-    result = run_command(f"git checkout --theirs lean-toolchain", check=False)
-    if result.returncode != 0:
-        print("Failed to resolve lean-toolchain conflict")
-        return False
-
-    # Add the resolved file
-    add_result = run_command("git add lean-toolchain", check=False)
-    if add_result.returncode != 0:
-        print("Failed to stage resolved lean-toolchain")
-        return False
-
-    return True
-
-
 def check_and_merge(repo, branch, tag, temp_dir):
     """Check if tag can be merged into branch and perform the merge if possible."""
     # Change to the temporary directory
@@ -125,37 +98,12 @@ def check_and_merge(repo, branch, tag, temp_dir):
     # Try merging the tag directly
     print(f"Merging {tag} into {branch}...")
     merge_result = run_command(f"git merge {tag} --no-edit", check=False)
-
+    
     if merge_result.returncode != 0:
-        # Check which files have conflicts
-        conflicted_files = get_conflicted_files()
-
-        if conflicted_files == ['lean-toolchain']:
-            # Only lean-toolchain has conflicts, resolve it
-            print("Merge conflict detected only in lean-toolchain.")
-            if resolve_lean_toolchain_conflict(tag):
-                # Continue the merge with the resolved conflict
-                print("Continuing merge with resolved lean-toolchain...")
-                continue_result = run_command(f"git commit --no-edit", check=False)
-                if continue_result.returncode != 0:
-                    print("Failed to complete merge after resolving lean-toolchain")
-                    run_command("git merge --abort")
-                    return False
-            else:
-                print("Failed to resolve lean-toolchain conflict")
-                run_command("git merge --abort")
-                return False
-        else:
-            # Other files have conflicts, or unable to determine
-            if conflicted_files:
-                print(f"Cannot merge {tag} cleanly into {branch}.")
-                print(f"Merge conflicts in: {', '.join(conflicted_files)}")
-            else:
-                print(f"Cannot merge {tag} cleanly into {branch}.")
-                print("Merge conflicts would occur.")
-            print("Aborting merge.")
-            run_command("git merge --abort")
-            return False
+        print(f"Cannot merge {tag} cleanly into {branch}.")
+        print("Merge conflicts would occur. Aborting merge.")
+        run_command("git merge --abort")
+        return False
     
     print(f"Pushing changes to remote...")
     push_result = run_command(f"git push origin {branch}")

script/prepare-llvm-linux.sh

@@ -58,11 +58,7 @@ OPTIONS=()
 # We build cadical using the custom toolchain on Linux to avoid glibc versioning issues
 echo -n " -DLEAN_STANDALONE=ON -DCADICAL_USE_CUSTOM_CXX=ON"
 echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'"
-# these should also be used for cadical, so do not use `LEAN_EXTRA_CXX_FLAGS` here
-echo -n " -DCMAKE_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
-# the above does not include linker flags which will be added below based on context, so skip the
-# generic check by cmake
-echo -n " -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER_WORKS=1"
+echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'"
 # use target compiler directly when not cross-compiling
 if [[ -L llvm-host ]]; then
   echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang"

script/release_checklist.py

@@ -1,60 +1,5 @@
 #!/usr/bin/env python3
 
-"""
-Release Checklist for Lean4 and Downstream Repositories
-
-This script validates the status of a Lean4 release across all dependent repositories.
-It checks whether repositories are ready for release and identifies missing steps.
-
-IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior!
-
-What this script does:
-1. Validates preliminary Lean4 release infrastructure:
-   - Checks that the release branch (releases/vX.Y.0) exists
-   - Verifies CMake version settings are correct
-   - Confirms the release tag exists
-   - Validates the release page exists on GitHub (created automatically by CI after tag push)
-   - Checks the release notes page on lean-lang.org (updated while bumping the `reference-manual` repository)
-
-   **IMPORTANT: If the release page doesn't exist, the script will skip checking
-   downstream repositories and the master branch configuration. The preliminary
-   infrastructure must be in place before the release process can proceed.**
-
-   **NOTE: The GitHub release page is created AUTOMATICALLY by CI after the tag is pushed.
-   DO NOT create it manually. Wait for CI to complete after pushing the tag.**
-
-2. For each downstream repository (batteries, mathlib4, etc.):
-   - Checks if dependencies are ready (e.g., mathlib4 depends on batteries)
-   - Verifies the main branch is on the target toolchain (or newer)
-   - Checks if a PR exists to bump the toolchain (if not yet updated)
-   - Validates tags exist for the release version
-   - Ensures tags are merged into stable branches (for non-RC releases)
-   - Verifies bump branches exist and are configured correctly
-   - Special handling for ProofWidgets4 release tags
-   - For mathlib4: runs verify_version_tags.py to validate the release tag
-     (checks git/GitHub consistency, toolchain, elan, cache, and build)
-
-3. Optionally automates missing steps (when not in --dry-run mode):
-   - Creates missing release tags using push_repo_release_tag.py
-   - Merges tags into stable branches using merge_remote.py
-
-Usage:
-    ./release_checklist.py v4.24.0           # Check release status
-    ./release_checklist.py v4.24.0 --verbose # Show detailed debug info
-    ./release_checklist.py v4.24.0 --dry-run # Check only, don't execute fixes
-
-For automated release management with Claude Code:
-    /release v4.24.0                 # Run full release process with Claude
-
-The script reads repository configurations from release_repos.yml and reports:
-- ✅ for completed requirements
-- ❌ for missing requirements (with instructions to fix)
-- 🟡 for repositories waiting on dependencies
-- ⮕ for automated actions being taken
-
-This script is idempotent and safe to rerun multiple times.
-"""
-
 import argparse
 import yaml
 import requests
@@ -131,39 +76,6 @@ def release_page_exists(repo_url, tag_name, github_token):
     response = requests.get(api_url, headers=headers)
     return response.status_code == 200
 
-def get_tag_workflow_status(repo_url, tag_name, github_token):
-    """Get the status of CI workflows running for a specific tag."""
-    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-
-    # Get workflow runs for the tag
-    # GitHub's workflow runs API uses the branch/tag name in the 'head_branch' field
-    api_url = f"{api_base}/actions/runs?event=push&head_branch={tag_name}"
-    response = requests.get(api_url, headers=headers)
-
-    if response.status_code != 200:
-        return None
-
-    data = response.json()
-    workflow_runs = data.get('workflow_runs', [])
-
-    if not workflow_runs:
-        return None
-
-    # Get the most recent workflow run for this tag
-    run = workflow_runs[0]
-    status = run.get('status')
-    conclusion = run.get('conclusion')
-    workflow_name = run.get('name', 'CI')
-    run_id = run.get('id')
-
-    return {
-        'status': status,
-        'conclusion': conclusion,
-        'workflow_name': workflow_name,
-        'run_id': run_id
-    }
-
 def get_release_notes(tag_name):
     """Fetch release notes page title from lean-lang.org."""
     # Strip -rcX suffix if present for the URL
@@ -172,17 +84,20 @@ def get_release_notes(tag_name):
     try:
         response = requests.get(reference_url)
         response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx)
-
+        
         # Extract title using regex
         match = re.search(r"<title>(.*?)</title>", response.text, re.IGNORECASE | re.DOTALL)
         if match:
             return match.group(1).strip()
         else:
+            print(f"  ⚠️ Could not find <title> tag in {reference_url}")
             return None
-
-    except requests.exceptions.RequestException:
+            
+    except requests.exceptions.RequestException as e:
+        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
         return None
-    except Exception:
+    except Exception as e:
+        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
         return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
@@ -371,68 +286,6 @@ def check_bump_branch_toolchain(url, bump_branch, github_token):
     print(f"  ✅ Bump branch correctly uses toolchain: {content}")
     return True
 
-def get_pr_ci_status(repo_url, pr_number, github_token):
-    """Get the CI status for a pull request."""
-    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-
-    # Get PR details to find the head SHA
-    pr_response = requests.get(f"{api_base}/pulls/{pr_number}", headers=headers)
-    if pr_response.status_code != 200:
-        return "unknown", "Could not fetch PR details"
-
-    pr_data = pr_response.json()
-    head_sha = pr_data['head']['sha']
-
-    # Get check runs for the commit
-    check_runs_response = requests.get(
-        f"{api_base}/commits/{head_sha}/check-runs",
-        headers=headers
-    )
-
-    if check_runs_response.status_code != 200:
-        return "unknown", "Could not fetch check runs"
-
-    check_runs_data = check_runs_response.json()
-    check_runs = check_runs_data.get('check_runs', [])
-
-    if not check_runs:
-        # No check runs, check for status checks (legacy)
-        status_response = requests.get(
-            f"{api_base}/commits/{head_sha}/status",
-            headers=headers
-        )
-        if status_response.status_code == 200:
-            status_data = status_response.json()
-            state = status_data.get('state', 'unknown')
-            if state == 'success':
-                return "success", "All status checks passed"
-            elif state == 'failure':
-                return "failure", "Some status checks failed"
-            elif state == 'pending':
-                return "pending", "Status checks in progress"
-        return "unknown", "No CI checks found"
-
-    # Analyze check runs
-    conclusions = [run['conclusion'] for run in check_runs if run.get('status') == 'completed']
-    in_progress = [run for run in check_runs if run.get('status') in ['queued', 'in_progress']]
-
-    if in_progress:
-        return "pending", f"{len(in_progress)} check(s) in progress"
-
-    if not conclusions:
-        return "pending", "Checks queued"
-
-    if all(c == 'success' for c in conclusions):
-        return "success", f"All {len(conclusions)} checks passed"
-
-    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
-    if failed > 0:
-        return "failure", f"{failed} check(s) failed"
-
-    # Some checks are cancelled, skipped, or neutral
-    return "warning", f"Some checks did not complete normally"
-
 def pr_exists_with_title(repo_url, title, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + "/pulls"
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -501,57 +354,6 @@ def check_proofwidgets4_release(repo_url, target_toolchain, github_token):
     print(f"     You will need to create and push a tag v0.0.{next_version}")
     return False
 
-def run_mathlib_verify_version_tags(toolchain, verbose=False):
-    """Run mathlib4's verify_version_tags.py script to validate the release tag.
-
-    This clones mathlib4 to a temp directory and runs the verification script.
-    Returns True if verification passes, False otherwise.
-    """
-    import tempfile
-
-    print(f"  ... Running mathlib4 verify_version_tags.py {toolchain}")
-
-    with tempfile.TemporaryDirectory() as tmpdir:
-        # Clone mathlib4 (shallow clone is sufficient for running the script)
-        clone_result = subprocess.run(
-            ['git', 'clone', '--depth', '1', 'https://github.com/leanprover-community/mathlib4.git', tmpdir],
-            capture_output=True,
-            text=True
-        )
-        if clone_result.returncode != 0:
-            print(f"  ❌ Failed to clone mathlib4: {clone_result.stderr.strip()[:200]}")
-            return False
-
-        # Run the verification script
-        script_path = os.path.join(tmpdir, 'scripts', 'verify_version_tags.py')
-        if not os.path.exists(script_path):
-            print(f"  ❌ verify_version_tags.py not found in mathlib4 (expected at scripts/verify_version_tags.py)")
-            return False
-
-        # Run from the mathlib4 directory so git operations work
-        result = subprocess.run(
-            ['python3', script_path, toolchain],
-            cwd=tmpdir,
-            capture_output=True,
-            text=True,
-            timeout=900  # 15 minutes timeout for cache download etc.
-        )
-
-        # Print output with indentation
-        if result.stdout:
-            for line in result.stdout.strip().split('\n'):
-                print(f"     {line}")
-        if result.stderr:
-            for line in result.stderr.strip().split('\n'):
-                print(f"     {line}")
-
-        if result.returncode != 0:
-            print(f"  ❌ mathlib4 verify_version_tags.py failed")
-            return False
-
-        print(f"  ✅ mathlib4 verify_version_tags.py passed")
-        return True
-
 def main():
     parser = argparse.ArgumentParser(description="Check release status of Lean4 repositories")
     parser.add_argument("toolchain", help="The toolchain version to check (e.g., v4.6.0)")
@@ -602,57 +404,30 @@ def main():
             print(f"  ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.")
             lean4_success = False
 
-    release_page_ready = release_page_exists(lean_repo_url, toolchain, github_token)
-    if not release_page_ready:
-        print(f"  ❌ Release page for {toolchain} does not exist (This will be created by CI.)")
-
-        # Check CI workflow status
-        workflow_status = get_tag_workflow_status(lean_repo_url, toolchain, github_token)
-        if workflow_status:
-            status = workflow_status['status']
-            conclusion = workflow_status['conclusion']
-            workflow_name = workflow_status['workflow_name']
-            run_id = workflow_status['run_id']
-            workflow_url = f"{lean_repo_url}/actions/runs/{run_id}"
-
-            if status == 'in_progress' or status == 'queued':
-                print(f"     🔄 {workflow_name} workflow is {status}: {workflow_url}")
-            elif status == 'completed':
-                if conclusion == 'success':
-                    print(f"     ✅ {workflow_name} workflow completed successfully: {workflow_url}")
-                elif conclusion == 'failure':
-                    print(f"     ❌ {workflow_name} workflow failed: {workflow_url}")
-                else:
-                    print(f"     ⚠️  {workflow_name} workflow completed with status: {conclusion}: {workflow_url}")
-            else:
-                print(f"     ℹ️  {workflow_name} workflow status: {status}: {workflow_url}")
-
+    if not release_page_exists(lean_repo_url, toolchain, github_token):
+        print(f"  ❌ Release page for {toolchain} does not exist")
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-
-    # Check the actual release notes page title (informational only - does not block)
+        
+    # Check the actual release notes page title
     actual_title = get_release_notes(toolchain)
     expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1"
-    base_tag = toolchain.split('-')[0]
-    release_notes_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
 
     if actual_title is None:
-        print(f"  ⚠️  Release notes not found at {release_notes_url} (this will be fixed while updating the reference-manual repository)")
+        # Error already printed by get_release_notes
+        lean4_success = False
     elif not actual_title.startswith(expected_title_prefix):
-        print(f"  ⚠️  Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {release_notes_url}")
+        # Construct URL for the error message (using the base tag)
+        base_tag = toolchain.split('-')[0]
+        check_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
+        print(f"  ❌ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {check_url}")
+        lean4_success = False
     else:
         print(f"  ✅ Release notes page title looks good ('{actual_title}').")
 
     repo_status["lean4"] = lean4_success
 
-    # If the release page doesn't exist, skip repository checks and master branch checks
-    # The preliminary infrastructure must be in place first
-    if not release_page_exists(lean_repo_url, toolchain, github_token):
-        print("\n⚠️  Release process blocked: preliminary Lean4 infrastructure incomplete.")
-        print("   Complete the steps above, then rerun this script to proceed with downstream repositories.")
-        return
-
     # Load repositories and perform further checks
     print("\nChecking repositories...")
 
@@ -696,19 +471,6 @@ def main():
             if pr_info:
                 pr_number, pr_url = pr_info
                 print(f"  ✅ PR with title '{pr_title}' exists: #{pr_number} ({pr_url})")
-
-                # Check CI status
-                ci_status, ci_message = get_pr_ci_status(url, pr_number, github_token)
-                if ci_status == "success":
-                    print(f"     ✅ CI: {ci_message}")
-                elif ci_status == "failure":
-                    print(f"     ❌ CI: {ci_message}")
-                elif ci_status == "pending":
-                    print(f"     🔄 CI: {ci_message}")
-                elif ci_status == "warning":
-                    print(f"     ⚠️  CI: {ci_message}")
-                else:
-                    print(f"     ❓ CI: {ci_message}")
             else:
                 print(f"  ❌ PR with title '{pr_title}' does not exist")
                 print(f"     Run `script/release_steps.py {toolchain} {name}` to create it")
@@ -816,12 +578,6 @@ def main():
                 repo_status[name] = False
                 continue
 
-        # For mathlib4, run verify_version_tags.py to validate the release tag
-        if name == "mathlib4":
-            if not run_mathlib_verify_version_tags(toolchain, verbose):
-                repo_status[name] = False
-                continue
-
         repo_status[name] = success
 
     # Final check for lean4 master branch

script/release_notes.py

@@ -52,7 +52,6 @@ def sort_sections_order():
     return [
         "Language",
         "Library",
-        "Tactics",
         "Compiler",
         "Pretty Printing",
         "Documentation",

script/release_repos.yml

@@ -1,11 +1,4 @@
 repositories:
-  - name: lean4-cli
-    url: https://github.com/leanprover/lean4-cli
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
   - name: batteries
     url: https://github.com/leanprover-community/batteries
     toolchain-tag: true
@@ -14,13 +7,6 @@ repositories:
     bump-branch: true
     dependencies: []
 
-  - name: verso
-    url: https://github.com/leanprover/verso
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: []
-
   - name: lean4checker
     url: https://github.com/leanprover/lean4checker
     toolchain-tag: true
@@ -35,6 +21,20 @@ repositories:
     branch: master
     dependencies: []
 
+  - name: lean4-cli
+    url: https://github.com/leanprover/lean4-cli
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
+  - name: verso
+    url: https://github.com/leanprover/verso
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: []
+
   - name: plausible
     url: https://github.com/leanprover-community/plausible
     toolchain-tag: true
@@ -96,15 +96,6 @@ repositories:
       - import-graph
       - plausible
 
-  - name: cslib
-    url: https://github.com/leanprover/cslib
-    toolchain-tag: true
-    stable-branch: true
-    branch: main
-    bump-branch: true
-    dependencies:
-      - mathlib4
-
   - name: repl
     url: https://github.com/leanprover-community/repl
     toolchain-tag: true
@@ -112,11 +103,3 @@ repositories:
     branch: master
     dependencies:
       - mathlib4
-
-  - name: lean-fro.org
-    url: https://github.com/leanprover/lean-fro.org
-    toolchain-tag: false
-    stable-branch: false
-    branch: master
-    dependencies:
-      - verso

script/release_steps.py

@@ -1,53 +1,30 @@
 #!/usr/bin/env python3
 
 """
-Execute Release Steps for Lean4 Downstream Repositories
+Execute release steps for Lean4 repositories.
 
-This script automates the process of updating a downstream repository to a new Lean4 release.
-It handles creating branches, updating toolchains, merging changes, building, testing, and
-creating pull requests.
-
-IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior!
-
-What this script does:
-1. Sets up the downstream_releases/ directory for cloning repositories
-
-2. Clones or updates the target repository
-
-3. Creates a branch named bump_to_{version} for the changes
-
-4. Updates the lean-toolchain file to the target version
-
-5. Handles repository-specific variations:
-   - Different dependency update mechanisms
-   - Special merging strategies for repositories with nightly-testing branches
-   - Safety checks for repositories using bump branches
-   - Custom build and test procedures
-
-6. Commits the changes with message "chore: bump toolchain to {version}"
-
-7. Builds the project (with a clean .lake cache)
-
-8. Runs tests if available
-
-9. Pushes the branch to GitHub
-
-10. Creates a pull request (or reports if one already exists)
+This script helps automate the release process for Lean4 and its dependent repositories
+by actually executing the step-by-step instructions for updating toolchains, creating tags,
+and managing branches.
 
 Usage:
-    ./release_steps.py v4.24.0 batteries    # Update batteries to v4.24.0
-    ./release_steps.py v4.24.0-rc1 mathlib4 # Update mathlib4 to v4.24.0-rc1
+    python3 release_steps.py <version> <repo>
 
-The script reads repository configurations from release_repos.yml.
-Each repository has specific handling for merging, dependencies, and testing.
+Arguments:
+    version: The version to set in the lean-toolchain file (e.g., v4.6.0)
+    repo: The repository name as specified in release_repos.yml
 
-This script is idempotent - it's safe to rerun if it fails partway through.
-Existing branches, commits, and PRs will be reused rather than duplicated.
+Example:
+    python3 release_steps.py v4.6.0 mathlib4
+    python3 release_steps.py v4.6.0 batteries
 
-Error handling:
-- If build or tests fail, the script continues to create the PR anyway
-- Manual conflicts must be resolved by the user
-- Network issues during push/PR creation are reported with manual instructions
+The script reads repository configurations from release_repos.yml in the same directory.
+Each repository may have specific requirements for:
+- Branch management
+- Toolchain updates
+- Dependency updates
+- Tagging conventions
+- Stable branch handling
 """
 
 import argparse
@@ -400,33 +377,6 @@ def execute_release_steps(repo, version, config):
         except subprocess.CalledProcessError as e:
             print(red("Tests failed, but continuing with PR creation..."))
             print(red(f"Test error: {e}"))
-    elif repo_name == "lean-fro.org":
-        # Update lean-toolchain in examples/hero
-        print(blue("Updating examples/hero/lean-toolchain..."))
-        docs_toolchain = repo_path / "examples" / "hero" / "lean-toolchain"
-        with open(docs_toolchain, "w") as f:
-            f.write(f"leanprover/lean4:{version}\n")
-        print(green(f"Updated examples/hero/lean-toolchain to leanprover/lean4:{version}"))
-
-        print(blue("Running `lake update`..."))
-        run_command("lake update", cwd=repo_path, stream_output=True)
-        print(blue("Running `lake update` in examples/hero..."))
-        run_command("lake update", cwd=repo_path / "examples" / "hero", stream_output=True)
-    elif repo_name == "cslib":
-        print(blue("Updating lakefile.toml..."))
-        run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
-        
-        print(blue("Updating docs/lakefile.toml..."))
-        run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path / "docs")
-
-        # Update lean-toolchain in docs
-        print(blue("Updating docs/lean-toolchain..."))
-        docs_toolchain = repo_path / "docs" / "lean-toolchain"
-        with open(docs_toolchain, "w") as f:
-            f.write(f"leanprover/lean4:{version}\n")
-        print(green(f"Updated docs/lean-toolchain to leanprover/lean4:{version}"))
-
-        run_command("lake update", cwd=repo_path, stream_output=True)
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
@@ -589,19 +539,8 @@ def execute_release_steps(repo, version, config):
         
         # Clean lake cache for a fresh build
         print(blue("Cleaning lake cache..."))
-        run_command("lake clean", cwd=repo_path)
-
-        # Check if downstream of Mathlib and get cache if so
-        mathlib_package_dir = repo_path / ".lake" / "packages" / "mathlib"
-        if mathlib_package_dir.exists():
-            print(blue("Project is downstream of Mathlib, fetching cache..."))
-            try:
-                run_command("lake exe cache get", cwd=repo_path, stream_output=True)
-                print(green("Cache fetched successfully"))
-            except subprocess.CalledProcessError as e:
-                print(yellow("Failed to fetch cache, continuing anyway..."))
-                print(yellow(f"Cache fetch error: {e}"))
-
+        run_command("rm -rf .lake", cwd=repo_path)
+        
         try:
             run_command("lake build", cwd=repo_path, stream_output=True)
             print(green("Build completed successfully"))

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 27)
+set(LEAN_VERSION_MINOR 24)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -34,15 +34,8 @@ if (NOT LEAN_PLATFORM_TARGET)
     OUTPUT_VARIABLE LEAN_PLATFORM_TARGET OUTPUT_STRIP_TRAILING_WHITESPACE)
 endif()
 
-set(LEAN_EXTRA_LINKER_FLAGS_DEFAULT "")
-# Use lld by default, if available
-find_program(LLD_PATH lld)
-if(LLD_PATH)
-  string(APPEND LEAN_EXTRA_LINKER_FLAGS_DEFAULT " -fuse-ld=lld")
-endif()
-
-set(LEAN_EXTRA_LINKER_FLAGS ${LEAN_EXTRA_LINKER_FLAGS_DEFAULT} CACHE STRING "Additional flags used by the linker")
-set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler. Unlike `CMAKE_CXX_FLAGS`, these will not be used to build e.g. cadical.")
+set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker")
+set(LEAN_EXTRA_CXX_FLAGS "" CACHE STRING "Additional flags used by the C++ compiler")
 set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests")
 
 if (NOT CMAKE_BUILD_TYPE)
@@ -89,7 +82,6 @@ option(USE_MIMALLOC "use mimalloc" ON)
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
-option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
 set(LEAN_EXTRA_MAKE_OPTS  ""                           CACHE STRING "extra options to lean --make")
 set(LEANC_CC              ${CMAKE_C_COMPILER}          CACHE STRING "C compiler to use in `leanc`")
@@ -191,7 +183,7 @@ endif()
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules")
 
 # Initialize CXXFLAGS.
-set(CMAKE_CXX_FLAGS                "${CMAKE_CXX_FLAGS} ${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
+set(CMAKE_CXX_FLAGS                "${LEAN_EXTRA_CXX_FLAGS} -DLEAN_BUILD_TYPE=\"${CMAKE_BUILD_TYPE}\" -DLEAN_EXPORTING")
 set(CMAKE_CXX_FLAGS_DEBUG          "-DLEAN_DEBUG")
 set(CMAKE_CXX_FLAGS_MINSIZEREL     "-DNDEBUG")
 set(CMAKE_CXX_FLAGS_RELEASE        "-DNDEBUG")
@@ -805,9 +797,6 @@ install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
 
 # symlink source into expected installation location for go-to-definition, if file system allows it
 file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
-# get rid of all files in `src/lean` that may have been loaded from the cache
-# (at the time of writing this, this is the case for some lake test .c files)
-file(REMOVE_RECURSE ${CMAKE_BINARY_DIR}/src/lean)
 if(${STAGE} EQUAL 0)
   file(CREATE_LINK ${CMAKE_SOURCE_DIR}/../../src ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
 else()
@@ -834,13 +823,10 @@ if(LEAN_INSTALL_PREFIX)
   set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
 endif()
 
-
-if (USE_LAKE_CACHE AND STAGE EQUAL 1)
-  set(LAKE_ARTIFACT_CACHE_TOML "true")
-else()
+if (STAGE GREATER 1)
   # The build of stage2+ may depend on local changes made to src/ that are not reflected by the
   # commit hash in stage1/bin/lean, so we make sure to disable the global cache
-  set(LAKE_ARTIFACT_CACHE_TOML "false")
+  string(APPEND LEAN_EXTRA_LAKEFILE_TOML "\n\nenableArtifactCache = false")
 endif()
 
 # Escape for `make`. Yes, twice.
@@ -858,13 +844,15 @@ endfunction()
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
+set(LEANC_OPTS_TOML "${LEANC_OPTS} ${LEANC_EXTRA_CC_FLAGS} ${LEANC_INTERNAL_FLAGS}")
+set(LINK_OPTS_TOML "${LEANC_INTERNAL_LINKER_FLAGS} -L${CMAKE_BINARY_DIR}/lib/lean ${LEAN_EXTRA_LINKER_FLAGS}")
 
 toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
+toml_escape("${LEANC_OPTS_TOML}" LEANC_OPTS_TOML)
+toml_escape("${LINK_OPTS_TOML}" LINK_OPTS_TOML)
 
-if(${CMAKE_BUILD_TYPE} MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
-  set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")
-else()
-  set(CMAKE_BUILD_TYPE_TOML "Release")
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  set(LAKE_LIB_PREFIX "lib")
 endif()
 
 if(USE_LAKE)

src/Init.lean

@@ -14,6 +14,7 @@ public import Init.ByCases
 public import Init.RCases
 public import Init.Core
 public import Init.Control
+public import Init.Data.Basic
 public import Init.WF
 public import Init.WFTactics
 public import Init.Data
@@ -41,8 +42,5 @@ public import Init.While
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try
-public meta import Init.Try  -- make sure `Try.Config` can be evaluated anywhere
 public import Init.BinderNameHint
 public import Init.Task
-public import Init.MethodSpecsSimp
-public import Init.LawfulBEqTactics

src/Init/BinderNameHint.lean

@@ -7,6 +7,7 @@ Authors: Joachim Breitner
 module
 
 prelude
+public import Init.Prelude
 public import Init.Tactics
 
 public section

src/Init/ByCases.lean

@@ -44,10 +44,3 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
 @[simp] theorem dite_eq_ite [Decidable P] :
   (dite P (fun _ => a) (fun _ => b)) = ite P a b := rfl
-
--- Remark: dite and ite are "defally equal" when we ignore the proofs.
-@[deprecated dite_eq_ite (since := "2025-10-29")]
-theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun _ => t) (fun _ => e) = ite c t e :=
-  match h with
-  | isTrue _    => rfl
-  | isFalse _   => rfl

src/Init/Classical.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.PropLemmas
 
-@[expose] public section
+public section
 
 universe u v
 
@@ -181,6 +181,9 @@ theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff
 
 theorem not_and_iff_not_or_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_not_or_not
 
+@[deprecated not_and_iff_not_or_not (since := "2025-03-18")]
+abbrev not_and_iff_or_not_not := @not_and_iff_not_or_not
+
 theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
 
 @[simp] theorem imp_iff_left_iff  : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff
@@ -205,5 +208,3 @@ export Classical (imp_iff_right_iff imp_and_neg_imp_iff and_or_imp not_imp)
 
 /-- Show that an element extracted from `P : ∃ a, p a` using `P.choose` satisfies `p`. -/
 theorem Exists.choose_spec {p : α → Prop} (P : ∃ a, p a) : p P.choose := Classical.choose_spec P
-
-grind_pattern Exists.choose_spec => P.choose

src/Init/Control.lean

@@ -16,3 +16,5 @@ public import Init.Control.Option
 public import Init.Control.Lawful
 public import Init.Control.StateCps
 public import Init.Control.ExceptCps
+
+public section

src/Init/Control/Basic.lean

@@ -25,7 +25,7 @@ instances are provided for the same type.
 instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α where
   forIn x b f := forIn' x b fun a _ => f a
 
-@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} (x : ρ) (b : β)
+@[simp] theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
     (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
     (h : ∀ a m b, f a m b = g a b) :
     forIn' x b f = forIn x b g := by
@@ -40,11 +40,14 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
   simp [h]
   rfl
 
-@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β}
+@[wf_preprocess] theorem forIn_eq_forIn' [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m]
     (x : ρ) (b : β) (f : (a : α) → β → m (ForInStep β)) :
     forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
   rfl
 
+@[deprecated forIn_eq_forIn' (since := "2025-04-04")]
+abbrev forIn_eq_forin' := @forIn_eq_forIn'
+
 /--
 Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`.
 -/
@@ -403,7 +406,7 @@ class ForM (m : Type u → Type v) (γ : Type w₁) (α : outParam (Type w₂))
   /--
   Runs the monadic action `f` on each element of the collection `coll`.
   -/
-  forM (coll : γ) (f : α → m PUnit) : m PUnit
+  forM [Monad m] (coll : γ) (f : α → m PUnit) : m PUnit
 
 export ForM (forM)
 

src/Init/Control/EState.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Control.State
+public import Init.Control.Except
 public import Init.Data.ToString.Basic
 
 public section

src/Init/Control/Except.lean

@@ -10,6 +10,7 @@ module
 prelude
 public import Init.Control.Basic
 public import Init.Control.Id
+public import Init.Coe
 
 @[expose] public section
 
@@ -148,23 +149,6 @@ This is the inverse of `ExceptT.mk`.
 @[always_inline, inline, expose]
 def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
 
-/--
-Use a monadic action that may throw an exception by providing explicit success and failure
-continuations.
--/
-@[always_inline, inline, expose]
-def ExceptT.runK [Monad m] (x : ExceptT ε m α) (ok : α → m β) (error : ε → m β) : m β :=
-  x.run >>= (·.casesOn error ok)
-
-/--
-Returns the value of a computation, forgetting whether it was an exception or a success.
-
-This corresponds to early return.
--/
-@[always_inline, inline, expose]
-def ExceptT.runCatch [Monad m] (x : ExceptT α m α) : m α :=
-  x.runK pure pure
-
 namespace ExceptT
 
 variable {ε : Type u} {m : Type u → Type v} [Monad m]

src/Init/Control/Lawful.lean

@@ -10,3 +10,5 @@ public import Init.Control.Lawful.Basic
 public import Init.Control.Lawful.Instances
 public import Init.Control.Lawful.Lemmas
 public import Init.Control.Lawful.MonadLift
+
+public section

src/Init/Control/Lawful/Basic.lean

@@ -7,6 +7,8 @@ module
 
 prelude
 public import Init.Ext
+public import Init.SimpLemmas
+public import Init.Meta
 
 public section
 
@@ -145,7 +147,7 @@ class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplica
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
 attribute [simp] pure_bind bind_assoc bind_pure_comp
-attribute [grind <=] pure_bind
+attribute [grind] pure_bind
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
   change x >>= (fun a => pure (id a)) = x
@@ -170,7 +172,6 @@ theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ =>
 theorem map_congr [Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x := by
   simp [funext h]
 
-@[deprecated seq_eq_bind_map (since := "2025-10-26")]
 theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : mf <*> x = mf >>= fun f => f <$> x := by
   rw [bind_map]
 
@@ -251,9 +252,24 @@ instance : LawfulMonad Id := by
 @[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
 @[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
 @[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
-@[simp] theorem pure_run (a : Id α) : pure a.run = a := rfl
 @[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
 @[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
 
+-- These lemmas are bad as they abuse the defeq of `Id α` and `α`
+@[deprecated run_map (since := "2025-03-05")] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
+@[deprecated run_bind (since := "2025-03-05")] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
+@[deprecated run_pure (since := "2025-03-05")] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+
 end Id
+
+/-! # Option -/
+
+instance : LawfulMonad Option := LawfulMonad.mk'
+  (id_map := fun x => by cases x <;> rfl)
+  (pure_bind := fun _ _ => rfl)
+  (bind_assoc := fun x _ _ => by cases x <;> rfl)
+  (bind_pure_comp := fun _ x => by cases x <;> rfl)
+
+instance : LawfulApplicative Option := inferInstance
+instance : LawfulFunctor Option := inferInstance

src/Init/Control/Lawful/Instances.lean

@@ -7,11 +7,12 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
+public import Init.Control.Except
 import all Init.Control.Except
-public import Init.Control.Option
-import all Init.Control.Option
+public import Init.Control.State
 import all Init.Control.State
 public import Init.Control.StateRef
+public import Init.Ext
 
 public section
 
@@ -109,121 +110,6 @@ instance : LawfulMonad (Except ε) := LawfulMonad.mk'
 instance : LawfulApplicative (Except ε) := inferInstance
 instance : LawfulFunctor (Except ε) := inferInstance
 
-/-! # OptionT -/
-
-namespace OptionT
-
-@[ext] theorem ext {x y : OptionT m α} (h : x.run = y.run) : x = y := by
-  simp [run] at h
-  assumption
-
-@[simp, grind =] theorem run_mk {m : Type u → Type v} (x : m (Option α)) :
-    OptionT.run (OptionT.mk x) = x := by rfl
-
-@[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : OptionT m α) = pure (some x) := by
-  simp [run, pure, OptionT.pure, OptionT.mk]
-
-@[simp, grind =] theorem run_lift  [Monad.{u, v} m] (x : m α) : run (OptionT.lift x : OptionT m α) = (return some (← x) : m (Option α)) := by
-  simp [run, OptionT.lift, OptionT.mk]
-
-@[simp, grind =] theorem run_throw [Monad m] : run (throw e : OptionT m β) = pure none := by
-  simp [run, throw, throwThe, MonadExceptOf.throw, OptionT.fail, OptionT.mk]
-
-@[simp, grind =] theorem run_bind_lift [Monad m] [LawfulMonad m] (x : m α) (f : α → OptionT m β) : run (OptionT.lift x >>= f : OptionT m β) = x >>= fun a => run (f a) := by
-  simp [OptionT.run, OptionT.lift, bind, OptionT.bind, OptionT.mk]
-
-@[simp, grind =] theorem bind_throw [Monad m] [LawfulMonad m] (f : α → OptionT m β) : (throw e >>= f) = throw e := by
-  simp [throw, throwThe, MonadExceptOf.throw, bind, OptionT.bind, OptionT.mk, OptionT.fail]
-
-@[simp, grind =] theorem run_bind (f : α → OptionT m β) [Monad m] :
-    (x >>= f).run = Option.elimM x.run (pure none) (fun x => (f x).run) := by
-  change x.run >>= _ = _
-  simp [Option.elimM]
-  exact bind_congr fun |some _ => rfl | none => rfl
-
-@[simp, grind =] theorem lift_pure [Monad m] [LawfulMonad m] {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
-  simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
-
-@[simp, grind =] theorem run_map [Monad m] [LawfulMonad m] (f : α → β) (x : OptionT m α)
-    : (f <$> x).run = Option.map f <$> x.run := by
-  simp [Functor.map, Option.map, ←bind_pure_comp]
-  apply bind_congr
-  intro a; cases a <;> simp [OptionT.pure, OptionT.mk]
-
-protected theorem seq_eq {α β : Type u} [Monad m] (mf : OptionT m (α → β)) (x : OptionT m α) : mf <*> x = mf >>= fun f => f <$> x :=
-  rfl
-
-protected theorem bind_pure_comp [Monad m] (f : α → β) (x : OptionT m α) : x >>= pure ∘ f = f <$> x := by
-  intros; rfl
-
-protected theorem seqLeft_eq {α β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : x <* y = const β <$> x <*> y := by
-  change (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
-  rw [← OptionT.bind_pure_comp]
-  apply ext
-  simp [Option.elimM, Option.elim]
-  apply bind_congr
-  intro
-  | none => simp
-  | some _ =>
-    simp [←bind_pure_comp]; apply bind_congr; intro b;
-    cases b <;> simp [const]
-
-protected theorem seqRight_eq [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) : x *> y = const α id <$> x <*> y := by
-  change (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
-  rw [← OptionT.bind_pure_comp]
-  apply ext
-  simp [Option.elimM, Option.elim]
-  apply bind_congr
-  intro a; cases a <;> simp
-
-instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where
-  id_map         := by intros; apply ext; simp
-  map_const      := by intros; rfl
-  seqLeft_eq     := OptionT.seqLeft_eq
-  seqRight_eq    := OptionT.seqRight_eq
-  pure_seq       := by intros; apply ext; simp [OptionT.seq_eq, Option.elimM, Option.elim]
-  bind_pure_comp := OptionT.bind_pure_comp
-  bind_map       := by intros; rfl
-  pure_bind      := by intros; apply ext; simp [Option.elimM, Option.elim]
-  bind_assoc     := by intros; apply ext; simp [Option.elimM, Option.elim]; apply bind_congr; intro a; cases a <;> simp
-
-@[simp] theorem run_seq [Monad m] [LawfulMonad m] (f : OptionT m (α → β)) (x : OptionT m α) :
-    (f <*> x).run = Option.elimM f.run (pure none) (fun f => Option.map f <$> x.run) := by
-  simp [seq_eq_bind_map, Option.elimM, Option.elim]
-
-@[simp] theorem run_seqLeft [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
-    (x <* y).run = Option.elimM x.run (pure none)
-      (fun x => Option.map (Function.const β x) <$> y.run) := by
-  simp [seqLeft_eq, seq_eq_bind_map, Option.elimM, OptionT.run_bind]
-
-@[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
-    (x *> y).run = Option.elimM x.run (pure none) (Function.const α y.run) := by
-  simp only [seqRight_eq, run_seq, Option.elimM, run_map, Option.elim, bind_map_left]
-  refine bind_congr (fun | some _ => by simp | none => by simp)
-
-@[simp, grind =] theorem run_failure [Monad m] : (failure : OptionT m α).run = pure none := by rfl
-
-@[simp] theorem map_failure [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) :
-    f <$> (failure : OptionT m α) = (failure : OptionT m β) := by
-  simp [OptionT.mk, Functor.map, Alternative.failure, OptionT.fail, OptionT.bind]
-
-@[simp] theorem run_orElse [Monad m] (x : OptionT m α) (y : OptionT m α) :
-    (x <|> y).run = Option.elimM x.run y.run (fun x => pure (some x)) :=
-  bind_congr fun | some _ => by rfl | none => by rfl
-
-end OptionT
-
-/-! # Option -/
-
-instance : LawfulMonad Option := LawfulMonad.mk'
-  (id_map := fun x => by cases x <;> rfl)
-  (pure_bind := fun _ _ => by rfl)
-  (bind_assoc := fun a _ _ => by cases a <;> rfl)
-  (bind_pure_comp := fun _ x => by cases x <;> rfl)
-
-instance : LawfulApplicative Option := inferInstance
-instance : LawfulFunctor Option := inferInstance
-
 /-! # ReaderT -/
 
 namespace ReaderT

src/Init/Control/Lawful/Lemmas.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
+public import Init.RCases
 public import Init.ByCases
 
 public section

src/Init/Control/Lawful/MonadLift.lean

@@ -9,3 +9,5 @@ prelude
 public import Init.Control.Lawful.MonadLift.Basic
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.MonadLift.Instances
+
+public section

src/Init/Control/Lawful/MonadLift/Instances.lean

@@ -6,13 +6,17 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
+public import Init.Control.Option
 import all Init.Control.Option
+public import Init.Control.Except
 import all Init.Control.Except
 public import Init.Control.ExceptCps
 import all Init.Control.ExceptCps
+public import Init.Control.StateRef
 import all Init.Control.StateRef
 public import Init.Control.StateCps
 import all Init.Control.StateCps
+public import Init.Control.Id
 import all Init.Control.Id
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.Instances
@@ -60,6 +64,10 @@ namespace OptionT
 
 variable [Monad m] [LawfulMonad m]
 
+@[simp]
+theorem lift_pure {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
+  simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
+
 @[simp]
 theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
     OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by

src/Init/Control/Lawful/MonadLift/Lemmas.lean

@@ -23,7 +23,7 @@ theorem monadLift_map [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α
 
 theorem monadLift_seq [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) :
     monadLift (mf <*> ma) = monadLift mf <*> (monadLift ma : n α) := by
-  simp only [seq_eq_bind_map, monadLift_map, monadLift_bind]
+  simp only [seq_eq_bind, monadLift_map, monadLift_bind]
 
 theorem monadLift_seqLeft [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
     monadLift (x <* y) = (monadLift x : n α) <* (monadLift y : n β) := by

src/Init/Control/Option.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Option.Basic
+public import Init.Control.Basic
 public import Init.Control.Except
 
 public section
@@ -27,7 +28,7 @@ failure occurred.
 /--
 Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
   x
 
@@ -38,14 +39,13 @@ variable {m : Type u → Type v} [Monad m] {α β : Type u}
 Converts an action that returns an `Option` into one that might fail, with `none` indicating
 failure.
 -/
-@[always_inline, inline, expose]
 protected def mk (x : m (Option α)) : OptionT m α :=
   x
 
 /--
 Sequences two potentially-failing actions. The second action is run only if the first succeeds.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
   match (← x) with
   | some a => f a
@@ -54,7 +54,7 @@ protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β :
 /--
 Succeeds with the provided value.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 protected def pure (a : α) : OptionT m α := OptionT.mk do
   pure (some a)
 
@@ -69,7 +69,7 @@ instance {m : Type u → Type v} [Pure m] : Inhabited (OptionT m α) where
 /--
 Recovers from failures. Typically used via the `<|>` operator.
 -/
-@[always_inline, inline, expose] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   match (← x) with
   | some a => pure (some a)
   | _      => y ()
@@ -77,7 +77,7 @@ Recovers from failures. Typically used via the `<|>` operator.
 /--
 A recoverable failure.
 -/
-@[always_inline, inline, expose] protected def fail : OptionT m α := OptionT.mk do
+@[always_inline, inline] protected def fail : OptionT m α := OptionT.mk do
   pure none
 
 instance : Alternative (OptionT m) where
@@ -90,7 +90,7 @@ Converts a computation from the underlying monad into one that could fail, even
 This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
 lifting](lean-manual://section/monad-lifting).
 -/
-@[always_inline, inline, expose] protected def lift (x : m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline] protected def lift (x : m α) : OptionT m α := OptionT.mk do
   return some (← x)
 
 instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
@@ -100,11 +100,11 @@ instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
 /--
 Handles failures by treating them as exceptions of type `Unit`.
 -/
-@[always_inline, inline, expose] protected def tryCatch (x : OptionT m α) (handle : PUnit → OptionT m α) : OptionT m α := OptionT.mk do
-  let some a ← x | handle ⟨⟩
+@[always_inline, inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
+  let some a ← x | handle ()
   pure <| some a
 
-instance : MonadExceptOf PUnit (OptionT m) where
+instance : MonadExceptOf Unit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 

src/Init/Control/Reader.lean

@@ -8,6 +8,8 @@ The Reader monad transformer for passing immutable State.
 module
 
 prelude
+public import Init.Control.Basic
+public import Init.Control.Id
 public import Init.Control.Except
 
 public section

src/Init/Control/State.lean

@@ -8,6 +8,8 @@ The State monad transformer.
 module
 
 prelude
+public import Init.Control.Basic
+public import Init.Control.Id
 public import Init.Control.Except
 
 public section

src/Init/Core.lean

@@ -8,6 +8,7 @@ notation, basic datatypes and type classes
 module
 
 prelude
+public meta import Init.Prelude
 public import Init.SizeOf
 
 public section
@@ -143,9 +144,8 @@ Computed values are cached, so the value is not recomputed.
   x.fn ()
 
 -- Ensure `Thunk.fn` is still computable even if it shouldn't be accessed directly.
-/-- Implementation detail. -/
-@[inline] def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
-@[csimp] theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
+@[inline] private def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
+@[csimp] private theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
 
 /--
 Constructs a new thunk that forces `x` and then applies `x` to the result. Upon forcing, the result
@@ -377,7 +377,7 @@ class ForIn (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v))
   More information about the translation of `for` loops into `ForIn.forIn` is available in [the Lean
   reference manual](lean-manual://section/monad-iteration-syntax).
   -/
-  forIn {β} (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
+  forIn {β} [Monad m] (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β
 
 export ForIn (forIn)
 
@@ -405,7 +405,7 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)
   More information about the translation of `for` loops into `ForIn'.forIn'` is available in [the
   Lean reference manual](lean-manual://section/monad-iteration-syntax).
   -/
-  forIn' {β} (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
+  forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β
 
 export ForIn' (forIn')
 
@@ -600,6 +600,17 @@ export LawfulSingleton (insert_empty_eq)
 
 attribute [simp] insert_empty_eq
 
+@[deprecated insert_empty_eq (since := "2025-03-12")]
+theorem insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
+    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
+  insert_empty_eq _
+
+@[deprecated insert_empty_eq (since := "2025-03-12")]
+theorem LawfulSingleton.insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
+    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
+  insert_empty_eq _
+
+
 /-- Type class used to implement the notation `{ a ∈ c | p a }` -/
 class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/
@@ -1084,6 +1095,14 @@ theorem of_toBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d =
 theorem of_toBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p :=
   of_decide_eq_false h
 
+set_option linter.missingDocs false in
+@[deprecated of_toBoolUsing_eq_true (since := "2025-04-04")]
+abbrev ofBoolUsing_eq_true := @of_toBoolUsing_eq_true
+
+set_option linter.missingDocs false in
+@[deprecated of_toBoolUsing_eq_false (since := "2025-04-04")]
+abbrev ofBoolUsing_eq_false := @of_toBoolUsing_eq_false
+
 instance : Decidable True :=
   isTrue trivial
 
@@ -1146,7 +1165,6 @@ end
     else isFalse (fun h => absurd (h hp) hq)
   else isTrue (fun h => absurd h hp)
 
-@[inline]
 instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
   if hp : p then
     if hq : q then
@@ -1188,13 +1206,17 @@ theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c
   | isTrue hc   => absurd hc hnc
   | isFalse _   => rfl
 
-@[macro_inline]
+-- Remark: dite and ite are "defally equal" when we ignore the proofs.
+theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun _ => t) (fun _ => e) = ite c t e :=
+  match h with
+  | isTrue _    => rfl
+  | isFalse _   => rfl
+
 instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
   match dC with
   | isTrue _   => dT
   | isFalse _  => dE
 
-@[inline]
 instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
   match dC with
   | isTrue hc  => dT hc
@@ -1345,12 +1367,12 @@ namespace Subtype
 theorem exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
   | ⟨a, h⟩ => ⟨a, h⟩
 
-variable {α : Sort u} {p : α → Prop}
+set_option linter.missingDocs false in
+@[deprecated exists_of_subtype (since := "2025-04-04")]
+abbrev existsOfSubtype := @exists_of_subtype
 
-protected theorem ext : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
-  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+variable {α : Type u} {p : α → Prop}
 
-@[deprecated Subtype.ext (since := "2025-10-26")]
 protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
@@ -1365,9 +1387,9 @@ instance {α : Type u} {p : α → Prop} [BEq α] [ReflBEq α] : ReflBEq {x : α
   rfl {x} := BEq.refl x.1
 
 instance {α : Type u} {p : α → Prop} [BEq α] [LawfulBEq α] : LawfulBEq {x : α // p x} where
-  eq_of_beq h := Subtype.ext (eq_of_beq h)
+  eq_of_beq h := Subtype.eq (eq_of_beq h)
 
-instance {α : Sort u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
+instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)
     else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
@@ -1468,8 +1490,6 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 
 @[simp] theorem Prod.map_apply (f : α → β) (g : γ → δ) (x) (y) :
     Prod.map f g (x, y) = (f x, g y) := rfl
-
--- We add `@[grind =]` to these in `Init.Data.Prod`.
 @[simp] theorem Prod.map_fst (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).1 = f x.1 := rfl
 @[simp] theorem Prod.map_snd (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).2 = g x.2 := rfl
 
@@ -1486,24 +1506,20 @@ protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α}
 
 /-! # Universe polymorphic unit -/
 
-theorem PUnit.ext (a b : PUnit) : a = b := by
-  cases a; cases b; exact rfl
-
-@[deprecated PUnit.ext (since := "2025-10-26")]
 theorem PUnit.subsingleton (a b : PUnit) : a = b := by
   cases a; cases b; exact rfl
 
 theorem PUnit.eq_punit (a : PUnit) : a = ⟨⟩ :=
-  PUnit.ext a ⟨⟩
+  PUnit.subsingleton a ⟨⟩
 
 instance : Subsingleton PUnit :=
-  Subsingleton.intro PUnit.ext
+  Subsingleton.intro PUnit.subsingleton
 
 instance : Inhabited PUnit where
   default := ⟨⟩
 
 instance : DecidableEq PUnit :=
-  fun a b => isTrue (PUnit.ext a b)
+  fun a b => isTrue (PUnit.subsingleton a b)
 
 /-! # Setoid -/
 
@@ -1564,7 +1580,6 @@ instance {p q : Prop} [d : Decidable (p ↔ q)] : Decidable (p = q) :=
 
 gen_injective_theorems% Array
 gen_injective_theorems% BitVec
-gen_injective_theorems% ByteArray
 gen_injective_theorems% Char
 gen_injective_theorems% DoResultBC
 gen_injective_theorems% DoResultPR
@@ -1589,8 +1604,8 @@ gen_injective_theorems% PSigma
 gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
-gen_injective_theorems% String.Pos.Raw
-gen_injective_theorems% Substring.Raw
+gen_injective_theorems% String.Pos
+gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum
 gen_injective_theorems% Task
@@ -2507,7 +2522,8 @@ class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
   antisymm (a b : α) : r a b → r b a → a = b
 
-/-- `Asymm r` means that the binary relation `r` is asymmetric, that is, `r a b → ¬ r b a`. -/
+/-- `Asymm r` means that the binary relation `r` is asymmetric, that is,
+`r a b → ¬ r b a`. -/
 class Asymm (r : α → α → Prop) : Prop where
   /-- An asymmetric relation satisfies `r a b → ¬ r b a`. -/
   asymm : ∀ a b, r a b → ¬r b a
@@ -2517,19 +2533,20 @@ class Symm (r : α → α → Prop) : Prop where
   /-- A symmetric relation satisfies `r a b → r b a`. -/
   symm : ∀ a b, r a b → r b a
 
-/-- `Total X r` means that the binary relation `r` on `X` is total, that is, `r a b` or `r b a`. -/
+/-- `Total X r` means that the binary relation `r` on `X` is total, that is, that for any
+`x y : X` we have `r x y` or `r y x`. -/
 class Total (r : α → α → Prop) : Prop where
-  /-- A total relation satisfies `r a b` or `r b a`. -/
+  /-- A total relation satisfies `r a b ∨ r b a`. -/
   total : ∀ a b, r a b ∨ r b a
 
-/-- `Irrefl r` means the binary relation `r` is irreflexive, that is, `r x x` never holds. -/
+/-- `Irrefl r` means the binary relation `r` is irreflexive, that is, `r x x` never
+holds. -/
 class Irrefl (r : α → α → Prop) : Prop where
   /-- An irreflexive relation satisfies `¬ r a a`. -/
   irrefl : ∀ a, ¬r a a
 
-/-- `Trichotomous r` says that `r` is trichotomous, that is, `¬ r a b → ¬ r b a → a = b`. -/
-class Trichotomous (r : α → α → Prop) : Prop where
-  /-- An trichotomous relation `r` satisfies `¬ r a b → ¬ r b a → a = b`. -/
-  trichotomous (a b : α) : ¬ r a b → ¬ r b a → a = b
-
 end Std
+
+/-- Deprecated alias for `XorOp`. -/
+@[deprecated XorOp (since := "2025-07-30")]
+abbrev Xor := XorOp

src/Init/Data.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Basic
 public import Init.Data.Nat
 public import Init.Data.Bool
 public import Init.Data.BitVec
@@ -29,7 +30,6 @@ public import Init.Data.Random
 public import Init.Data.ToString
 public import Init.Data.Range
 public import Init.Data.Hashable
-public import Init.Data.LawfulHashable
 public import Init.Data.OfScientific
 public import Init.Data.Format
 public import Init.Data.Stream
@@ -52,3 +52,5 @@ public import Init.Data.Slice
 public import Init.Data.Order
 public import Init.Data.Rat
 public import Init.Data.Dyadic
+
+public section

src/Init/Data/AC.lean

@@ -7,6 +7,7 @@ Authors: Dany Fabian
 module
 
 prelude
+public import Init.Classical
 public import Init.ByCases
 
 @[expose] public section

src/Init/Data/Array.lean

@@ -30,3 +30,5 @@ public import Init.Data.Array.Erase
 public import Init.Data.Array.Zip
 public import Init.Data.Array.InsertIdx
 public import Init.Data.Array.Extract
+
+public section

src/Init/Data/Array/Attach.lean

@@ -6,7 +6,10 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
+public import Init.Data.Array.Mem
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Count
+public import Init.Data.List.Attach
 import all Init.Data.List.Attach
 
 public section
@@ -81,10 +84,10 @@ well-founded recursion mechanism to prove that the function terminates.
   simp [pmap]
 
 /-- Implementation of `pmap` using the zero-copy version of `attach`. -/
-@[inline] def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
     Array β := (xs.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
 
-@[csimp] theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
   funext α β p f xs H
   cases xs
   simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith_eq_pmap]
@@ -92,16 +95,16 @@ well-founded recursion mechanism to prove that the function terminates.
   intro a m h₁ h₂
   congr
 
-@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
+@[simp, grind =] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
 
-@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
+@[simp, grind =] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
     pmap f (xs.push a) h =
       (pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
   simp [pmap]
 
-@[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
+@[simp, grind =] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
 
-@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
+@[simp, grind =] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
 
 @[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
     l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
@@ -118,15 +121,17 @@ theorem pmap_eq_map {p : α → Prop} {f : α → β} {xs : Array α} (H) :
 theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (xs : Array α) {H₁ H₂}
     (h : ∀ a ∈ xs, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f xs H₁ = pmap g xs H₂ := by
   cases xs
-  simp only [List.mem_toArray] at h
+  simp only [mem_toArray] at h
   simp only [List.pmap_toArray, mk.injEq]
   rw [List.pmap_congr_left _ h]
 
+@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {xs : Array α} (H) :
     map g (pmap f xs H) = pmap (fun a h => g (f a h)) xs H := by
   cases xs
   simp [List.map_pmap]
 
+@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs : Array α} (H) :
     pmap g (map f xs) H = pmap (fun a h => g (f a) h) xs fun _ h => H _ (mem_map_of_mem h) := by
   cases xs
@@ -142,14 +147,14 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
   subst w
   simp
 
-@[simp] theorem attach_push {a : α} {xs : Array α} :
+@[simp, grind =] theorem attach_push {a : α} {xs : Array α} :
     (xs.push a).attach =
       (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   cases xs
   rw [attach_congr (List.push_toArray _ _)]
   simp [Function.comp_def]
 
-@[simp] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp, grind =] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
       (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   cases xs
@@ -171,6 +176,9 @@ theorem attach_map_val (xs : Array α) (f : α → β) :
   cases xs
   simp
 
+@[deprecated attach_map_val (since := "2025-02-17")]
+abbrev attach_map_coe := @attach_map_val
+
 -- The argument `xs : Array α` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (xs : Array α) : xs.attach.map Subtype.val = xs := by
   cases xs; simp
@@ -179,18 +187,21 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {xs : Array α} (H
     ((xs.attachWith p H).map fun (i : { i // p i}) => f i) = xs.map f := by
   cases xs; simp
 
+@[deprecated attachWith_map_val (since := "2025-02-17")]
+abbrev attachWith_map_coe := @attachWith_map_val
+
 theorem attachWith_map_subtype_val {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) :
     (xs.attachWith p H).map Subtype.val = xs := by
   cases xs; simp
 
-@[simp, grind ←]
+@[simp, grind]
 theorem mem_attach (xs : Array α) : ∀ x, x ∈ xs.attach
   | ⟨a, h⟩ => by
     have := mem_map.1 (by rw [attach_map_subtype_val] <;> exact h)
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
-@[simp, grind =]
+@[simp, grind]
 theorem mem_attachWith {xs : Array α} {q : α → Prop} (H) (x : {x // q x}) :
     x ∈ xs.attachWith q H ↔ x.1 ∈ xs := by
   cases xs
@@ -201,13 +212,12 @@ theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {xs H b} :
     b ∈ pmap f xs H ↔ ∃ (a : _) (h : a ∈ xs), f a (H a h) = b := by
   simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
 
+@[grind]
 theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {xs H} {a} (h : a ∈ xs) :
     f a (H a h) ∈ pmap f xs H := by
   rw [mem_pmap]
   exact ⟨a, h, rfl⟩
 
-grind_pattern mem_pmap_of_mem => _ ∈ pmap f xs H, a ∈ xs
-
 @[simp, grind =]
 theorem size_pmap {p : α → Prop} {f : ∀ a, p a → β} {xs H} : (pmap f xs H).size = xs.size := by
   cases xs; simp
@@ -283,23 +293,25 @@ theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp, grind =] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f xs.attach H =
       xs.pmap (P := fun a => ∃ h : a ∈ xs, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   ext <;> simp
 
-@[simp] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp, grind =] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (xs.attachWith q H₁) H₂ =
       xs.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
   ext <;> simp
 
+@[grind =]
 theorem foldl_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) :
     (xs.pmap f H).foldl g x = xs.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
+@[grind =]
 theorem foldr_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : β → γ → γ) (x : γ) :
     (xs.pmap f H).foldr g x = xs.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
@@ -333,7 +345,7 @@ theorem foldl_attach {xs : Array α} {f : β → α → β} {b : β} :
     xs.attach.foldl (fun acc t => f acc t.1) b = xs.foldl f b := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
-    List.foldl_toArray', List.mem_toArray, List.foldl_subtype]
+    List.foldl_toArray', mem_toArray, List.foldl_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
@@ -352,23 +364,25 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
     xs.attach.foldr (fun t acc => f t.1 acc) b = xs.foldr f b := by
   rcases xs with ⟨xs⟩
   simp only [List.attach_toArray, List.attachWith_mem_toArray, List.size_toArray,
-    List.foldr_toArray', List.mem_toArray, List.foldr_subtype]
+    List.foldr_toArray', mem_toArray, List.foldr_subtype]
   congr
   ext
   simpa using fun a => List.mem_of_getElem? a
 
+@[grind =]
 theorem attach_map {xs : Array α} {f : α → β} :
     (xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   cases xs
   ext <;> simp
 
+@[grind =]
 theorem attachWith_map {xs : Array α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ xs.map f → P b) :
     (xs.map f).attachWith P H = (xs.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases xs
   simp [List.attachWith_map]
 
-@[simp] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp, grind =] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
     {f : { x // P x } → β} :
     (xs.attachWith P H).map f = xs.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   cases xs <;> simp_all
@@ -386,6 +400,9 @@ theorem map_attach_eq_pmap {xs : Array α} {f : { x // x ∈ xs } → β} :
   cases xs
   ext <;> simp
 
+@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
+abbrev map_attach := @map_attach_eq_pmap
+
 @[grind =]
 theorem attach_filterMap {xs : Array α} {f : α → Option β} :
     (xs.filterMap f).attach = xs.attach.filterMap
@@ -421,6 +438,7 @@ theorem filter_attachWith {q : α → Prop} {xs : Array α} {p : {x // q x} →
   cases xs
   simp [Function.comp_def, List.filter_map]
 
+@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {xs} (H₁ H₂) :
     pmap f (pmap g xs H₁) H₂ =
       pmap (α := { x // x ∈ xs }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) xs.attach
@@ -428,7 +446,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   cases xs
   simp [List.pmap_pmap, List.pmap_map]
 
-@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
+@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
     (h : ∀ a ∈ xs ++ ys, p a) :
     (xs ++ ys).pmap f h =
       (xs.pmap f fun a ha => h a (mem_append_left ys ha)) ++
@@ -443,7 +461,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp] theorem attach_append {xs ys : Array α} :
+@[simp, grind =] theorem attach_append {xs ys : Array α} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   cases xs
@@ -451,59 +469,62 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
   rw [attach_congr (List.append_toArray _ _)]
   simp [List.attach_append, Function.comp_def]
 
-@[simp] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
+@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp [attachWith]
 
-@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
+@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
+@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
   cases xs
   simp
 
+@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
   cases xs
   simp
 
-@[simp] theorem attach_reverse {xs : Array α} :
+@[simp, grind =] theorem attach_reverse {xs : Array α} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   rw [attach_congr List.reverse_toArray]
   simp
 
+@[grind =]
 theorem reverse_attach {xs : Array α} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   simp
 
-@[simp] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp, grind =] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
   cases xs
   simp
 
-@[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
+@[simp, grind =] theorem back?_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
-@[simp]
+@[simp, grind =]
 theorem back?_attach {xs : Array α} :
     xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs
@@ -685,7 +706,7 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → Array β} {g : α → Array β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (xs.flatMap f) = xs.unattach.flatMap g := by
   cases xs
-  simp only [List.flatMap_toArray, List.unattach_toArray,
+  simp only [List.flatMap_toArray, List.unattach_toArray, 
     mk.injEq]
   rw [List.flatMap_subtype]
   simp [hf]
@@ -749,6 +770,9 @@ and simplifies these to the function directly taking the value.
     (Array.replicate n x).unattach = Array.replicate n x.1 := by
   simp [unattach]
 
+@[deprecated unattach_replicate (since := "2025-03-18")]
+abbrev unattach_mkArray := @unattach_replicate
+
 /-! ### Well-founded recursion preprocessing setup -/
 
 @[wf_preprocess] theorem map_wfParam {xs : Array α} {f : α → β} :

src/Init/Data/Array/Basic.lean

@@ -6,6 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.WFTactics
+public import Init.Data.Nat.Basic
+public import Init.Data.Fin.Basic
+public import Init.Data.UInt.BasicAux
 public import Init.GetElem
 public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
@@ -36,11 +40,11 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp, grind =] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
+@[simp, grind] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
     (set xs i v h).size = xs.size :=
   List.length_set ..
 
-@[simp, grind =] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
+@[simp, grind] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
   List.length_concat ..
 
 theorem ext {xs ys : Array α}
@@ -104,19 +108,13 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-@[simp, grind =] theorem _root_.List.mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+@[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[deprecated List.mem_toArray (since := "2025-09-04")]
-theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l :=
-  List.mem_toArray
-
-@[simp] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
+@[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
 
-grind_pattern getElem_mem => xs[i] ∈ xs
-
 @[simp, grind =] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
 
 @[simp] theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl
@@ -125,10 +123,19 @@ end Array
 
 namespace List
 
+@[deprecated Array.toArray_toList (since := "2025-02-17")]
+abbrev toArray_toList := @Array.toArray_toList
+
 -- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
 theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl
 
-@[simp, grind =] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
+@[deprecated toList_toArray (since := "2025-02-17")]
+abbrev _root_.Array.toList_toArray := @List.toList_toArray
+
+@[simp, grind] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
+
+@[deprecated size_toArray (since := "2025-02-17")]
+abbrev _root_.Array.size_toArray := @List.size_toArray
 
 @[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := rfl
@@ -190,7 +197,7 @@ Examples:
 def pop (xs : Array α) : Array α where
   toList := xs.toList.dropLast
 
-@[simp, grind =] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
+@[simp, grind] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
   match xs with
   | ⟨[]⟩ => rfl
   | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
@@ -209,6 +216,20 @@ Examples:
 def replicate {α : Type u} (n : Nat) (v : α) : Array α where
   toList := List.replicate n v
 
+/--
+Creates an array that contains `n` repetitions of `v`.
+
+The corresponding `List` function is `List.replicate`.
+
+Examples:
+ * `Array.mkArray 2 true = #[true, true]`
+ * `Array.mkArray 3 () = #[(), (), ()]`
+ * `Array.mkArray 0 "anything" = #[]`
+-/
+@[extern "lean_mk_array", deprecated replicate (since := "2025-03-18")]
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
 /--
 Swaps two elements of an array. The modification is performed in-place when the reference to the
 array is unique.
@@ -226,7 +247,7 @@ def swap (xs : Array α) (i j : @& Nat) (hi : i < xs.size := by get_elem_tactic)
   let xs'  := xs.set i v₂
   xs'.set j v₁ (Nat.lt_of_lt_of_eq hj (size_set _).symm)
 
-@[simp, grind =] theorem size_swap {xs : Array α} {i j : Nat} {hi hj} : (xs.swap i j hi hj).size = xs.size := by
+@[simp] theorem size_swap {xs : Array α} {i j : Nat} {hi hj} : (xs.swap i j hi hj).size = xs.size := by
   change ((xs.set i xs[j]).set j xs[i]
     (Nat.lt_of_lt_of_eq hj (size_set _).symm)).size = xs.size
   rw [size_set, size_set]
@@ -242,7 +263,7 @@ Examples:
 * `#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]`
 * `#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]`
 -/
-@[extern "lean_array_swap", expose]
+@[extern "lean_array_swap", grind]
 def swapIfInBounds (xs : Array α) (i j : @& Nat) : Array α :=
   if h₁ : i < xs.size then
   if h₂ : j < xs.size then swap xs i j
@@ -385,6 +406,10 @@ that requires a proof the array is non-empty.
 def back? (xs : Array α) : Option α :=
   xs[xs.size - 1]?
 
+@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), expose]
+def get? (xs : Array α) (i : Nat) : Option α :=
+  if h : i < xs.size then some xs[i] else none
+
 /--
 Swaps a new element with the element at the given index.
 
@@ -448,7 +473,7 @@ Examples:
 -/
 abbrev take (xs : Array α) (i : Nat) : Array α := extract xs 0 i
 
-@[simp, grind =] theorem take_eq_extract {xs : Array α} {i : Nat} : xs.take i = xs.extract 0 i := rfl
+@[simp] theorem take_eq_extract {xs : Array α} {i : Nat} : xs.take i = xs.extract 0 i := rfl
 
 /--
 Removes the first `i` elements of `xs`. If `xs` has fewer than `i` elements, the new array is empty.
@@ -462,7 +487,7 @@ Examples:
 -/
 abbrev drop (xs : Array α) (i : Nat) : Array α := extract xs i xs.size
 
-@[simp, grind =] theorem drop_eq_extract {xs : Array α} {i : Nat} : xs.drop i = xs.extract i xs.size := rfl
+@[simp] theorem drop_eq_extract {xs : Array α} {i : Nat} : xs.drop i = xs.extract i xs.size := rfl
 
 @[inline]
 unsafe def modifyMUnsafe [Monad m] (xs : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
@@ -570,7 +595,7 @@ protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
       | ForInStep.yield b => loop i (Nat.le_of_lt h') b
   loop as.size (Nat.le_refl _) b
 
-instance [Monad m] : ForIn' m (Array α) α inferInstance where
+instance : ForIn' m (Array α) α inferInstance where
   forIn' := Array.forIn'
 
 -- No separate `ForIn` instance is required because it can be derived from `ForIn'`.
@@ -734,7 +759,8 @@ of results.
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
   -- Note: we cannot use `foldlM` here for the reference implementation because this calls
   -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
-  let rec map (i : Nat) (bs : Array β) : m (Array β) := do
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    map (i : Nat) (bs : Array β) : m (Array β) := do
       if hlt : i < as.size then
         map (i+1) (bs.push (← f as[i]))
       else
@@ -894,7 +920,8 @@ entire array is checked.
 @[implemented_by anyMUnsafe, expose]
 def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
   let any (stop : Nat) (h : stop ≤ as.size) :=
-    let rec loop (j : Nat) : m Bool := do
+    let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    loop (j : Nat) : m Bool := do
       if hlt : j < stop then
         have : j < as.size := Nat.lt_of_lt_of_le hlt h
         if (← p as[j]) then
@@ -1001,7 +1028,7 @@ unless `start < stop`. By default, the entire array is used.
 protected def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := 0) (stop := as.size) : m PUnit :=
   as.foldlM (fun _ => f) ⟨⟩ start stop
 
-instance [Monad m] : ForM m (Array α) α where
+instance : ForM m (Array α) α where
   forM xs f := Array.forM f xs
 
 -- We simplify `Array.forM` to `forM`.
@@ -1232,7 +1259,8 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -1249,7 +1277,8 @@ Examples:
 -/
 @[inline]
 def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some ⟨j, h⟩ else loop (j + 1)
     else none
@@ -1285,6 +1314,7 @@ Examples:
 @[inline, expose]
 def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def idxOfAux [BEq α] (xs : Array α) (v : α) (i : Nat) : Option (Fin xs.size) :=
   if h : i < xs.size then
     if xs[i] == v then some ⟨i, h⟩
@@ -1295,7 +1325,7 @@ decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 
 /--
-Returns the index of the first element equal to `a`, or `none` if no element is equal
+Returns the index of the first element equal to `a`, or the size of the array if no element is equal
 to `a`. The index is returned as a `Fin`, which guarantees that it is in bounds.
 
 Examples:
@@ -1694,6 +1724,7 @@ Examples:
  * `#[3, 2, 3, 4].popWhile (· > 2) = #[3, 2]`
  * `(#[] : Array Nat).popWhile (· > 2) = #[]`
 -/
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
     if p (as[as.size - 1]'(Nat.sub_lt h (by decide))) then
@@ -1704,7 +1735,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
     as
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-@[simp, grind =] theorem popWhile_empty {p : α → Bool} :
+@[simp] theorem popWhile_empty {p : α → Bool} :
     popWhile p #[] = #[] := by
   simp [popWhile]
 
@@ -1718,7 +1749,8 @@ Examples:
  * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]`
 -/
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec go (i : Nat) (acc : Array α) : Array α :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  go (i : Nat) (acc : Array α) : Array α :=
     if h : i < as.size then
       let a := as[i]
       if p a then
@@ -1741,6 +1773,7 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]`
 -/
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def eraseIdx (xs : Array α) (i : Nat) (h : i < xs.size := by get_elem_tactic) : Array α :=
   if h' : i + 1 < xs.size then
     let xs' := xs.swap (i + 1) i
@@ -1751,8 +1784,7 @@ termination_by xs.size - i
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
 
 -- This is required in `Lean.Data.PersistentHashMap`.
-@[simp, grind =]
-theorem size_eraseIdx {xs : Array α} (i : Nat) (h) : (xs.eraseIdx i h).size = xs.size - 1 := by
+@[simp] theorem size_eraseIdx {xs : Array α} (i : Nat) (h) : (xs.eraseIdx i h).size = xs.size - 1 := by
   induction xs, i, h using Array.eraseIdx.induct with
   | @case1 xs i h h' xs' ih =>
     unfold eraseIdx
@@ -1774,6 +1806,7 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
+@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 
@@ -1836,7 +1869,8 @@ Examples:
  * `#["tues", "thur", "sat"].insertIdx 3 "wed" = #["tues", "thur", "sat", "wed"]`
 -/
 @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
-  let rec loop (as : Array α) (j : Fin as.size) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (as : Array α) (j : Fin as.size) :=
     if i < j then
       let j' : Fin as.size := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
@@ -1890,6 +1924,7 @@ def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
   else
     as
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -1918,7 +1953,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[specialize]
+@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
 def zipWithMAux {m : Type v → Type w} [Monad m] (as : Array α) (bs : Array β) (f : α → β → m γ) (i : Nat) (cs : Array γ) : m (Array γ) := do
   if h : i < as.size then
     let a := as[i]
@@ -2081,6 +2116,7 @@ private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat),
     have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
     a != as[i] && allDiffAuxAux as a i this
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   if h : i < as.size then
     allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
@@ -2134,3 +2170,5 @@ instance [ToString α] : ToString (Array α) where
   toString xs := String.Internal.append "#" (toString xs.toList)
 
 end Array
+
+export Array (mkArray)

src/Init/Data/Array/BasicAux.lean

@@ -6,8 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Nat.Linear
+public import Init.NotationExtra
 
 public section
 

src/Init/Data/Array/BinSearch.lean

@@ -6,7 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 public import Init.Data.Int.DivMod.Lemmas
+public import Init.Omega
 
 public section
 universe u v

src/Init/Data/Array/Bootstrap.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 
 public section
@@ -23,6 +24,29 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Array
 
+/--
+Use the indexing notation `a[i]` instead.
+
+Access an element from an array without needing a runtime bounds checks,
+using a `Nat` index and a proof that it is in bounds.
+
+This function does not use `get_elem_tactic` to automatically find the proof that
+the index is in bounds. This is because the tactic itself needs to look up values in
+arrays.
+-/
+@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
+def get {α : Type u} (xs : @& Array α) (i : @& Nat) (h : LT.lt i xs.size) : α :=
+  xs.toList.get ⟨i, h⟩
+
+/--
+Use the indexing notation `a[i]!` instead.
+
+Access an element from an array, or panic if the index is out of bounds.
+-/
+@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17"), expose]
+def get! {α : Type u} [Inhabited α] (xs : @& Array α) (i : @& Nat) : α :=
+  Array.getD xs i default
+
 theorem foldlM_toList.aux [Monad m]
     {f : β → α → m β} {xs : Array α} {i j} (H : xs.size ≤ i + j) {b} :
     foldlM.loop f xs xs.size (Nat.le_refl _) i j b = (xs.toList.drop j).foldlM f b := by
@@ -31,7 +55,7 @@ theorem foldlM_toList.aux [Monad m]
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_toList.aux (j := j+1) H]
-    rw (occs := [2]) [← List.getElem_cons_drop ‹_›]
+    rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     simp
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; simp
 
@@ -84,6 +108,9 @@ abbrev push_toList := @toList_push
 
 @[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
 
+@[deprecated toList_pop (since := "2025-02-17")]
+abbrev pop_toList := @Array.toList_pop
+
 @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl
 
 @[simp, grind =] theorem toList_append {xs ys : Array α} :
@@ -100,15 +127,9 @@ abbrev push_toList := @toList_push
 @[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
   apply ext'; simp only [toList_append, List.nil_append]
 
-@[simp] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
+@[simp, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
-grind_pattern append_assoc => (xs ++ ys) ++ zs where
-  xs =/= #[]; ys =/= #[]; zs =/= #[]
-
-grind_pattern append_assoc => xs ++ (ys ++ zs) where
-  xs =/= #[]; ys =/= #[]; zs =/= #[]
-
 @[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl
 
 @[simp, grind =] theorem toList_appendList {xs : Array α} {l : List α} :
@@ -116,4 +137,6 @@ grind_pattern append_assoc => xs ++ (ys ++ zs) where
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing xs <;> simp [*]
 
+
+
 end Array

src/Init/Data/Array/Count.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Nat.Count
@@ -62,7 +63,7 @@ theorem size_eq_countP_add_countP {xs : Array α} : xs.size = countP p xs + coun
   rcases xs with ⟨xs⟩
   simp [List.length_eq_countP_add_countP (p := p)]
 
-@[grind =]
+@[grind _=_]
 theorem countP_eq_size_filter {xs : Array α} : countP p xs = (filter p xs).size := by
   rcases xs with ⟨xs⟩
   simp [List.countP_eq_length_filter]
@@ -99,6 +100,9 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
 theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0 := by
   simp [← List.toArray_replicate, List.countP_replicate]
 
+@[deprecated countP_replicate (since := "2025-03-18")]
+abbrev countP_mkArray := @countP_replicate
+
 theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
   rcases xs with ⟨xs⟩
@@ -259,9 +263,15 @@ theorem count_eq_size {xs : Array α} : count a xs = xs.size ↔ ∀ b ∈ xs, a
 @[simp] theorem count_replicate_self {a : α} {n : Nat} : count a (replicate n a) = n := by
   simp [← List.toArray_replicate]
 
+@[deprecated count_replicate_self (since := "2025-03-18")]
+abbrev count_mkArray_self := @count_replicate_self
+
 theorem count_replicate {a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0 := by
   simp [← List.toArray_replicate, List.count_replicate]
 
+@[deprecated count_replicate (since := "2025-03-18")]
+abbrev count_mkArray := @count_replicate
+
 theorem filter_beq {xs : Array α} (a : α) : xs.filter (· == a) = replicate (count a xs) a := by
   rcases xs with ⟨xs⟩
   simp [List.filter_beq]
@@ -275,6 +285,9 @@ theorem replicate_count_eq_of_count_eq_size {xs : Array α} (h : count a xs = xs
   rw [← toList_inj]
   simp [List.replicate_count_eq_of_count_eq_length (by simpa using h)]
 
+@[deprecated replicate_count_eq_of_count_eq_size (since := "2025-03-18")]
+abbrev mkArray_count_eq_of_count_eq_size := @replicate_count_eq_of_count_eq_size
+
 @[simp] theorem count_filter {xs : Array α} (h : p a) : count a (filter p xs) = count a xs := by
   rcases xs with ⟨xs⟩
   simp [List.count_filter, h]

src/Init/Data/Array/DecidableEq.lean

@@ -6,9 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.BEq
 public import Init.Data.List.Nat.BEq
+public import Init.ByCases
 
 public section
 
@@ -89,41 +91,11 @@ theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs
 theorem isEqv_self [DecidableEq α] (xs : Array α) : Array.isEqv xs xs (· = ·) = true := by
   simp [isEqv, isEqvAux_self]
 
-def instDecidableEqImpl [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
-  match h:isEqv xs ys (fun a b => a = b) with
-  | true  => isTrue (eq_of_isEqv xs ys h)
-  | false => isFalse (by subst ·; rw [isEqv_self] at h; contradiction)
-
-instance instDecidableEq [DecidableEq α] : DecidableEq (Array α) := fun xs ys =>
-  match xs with
-  | ⟨[]⟩ =>
-    match ys with
-    | ⟨[]⟩ => isTrue rfl
-    | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
-  | ⟨a :: as⟩ =>
-    match ys with
-    | ⟨[]⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
-    | ⟨b :: bs⟩ => instDecidableEqImpl ⟨a :: as⟩ ⟨b :: bs⟩
-
-@[csimp]
-theorem instDecidableEq_csimp : @instDecidableEq = @instDecidableEqImpl :=
-  Subsingleton.allEq _ _
-  
-/--
-Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
--/
-instance instDecidableEqEmp (xs : Array α) : Decidable (xs = #[]) :=
-  match xs with
-  | ⟨[]⟩ => isTrue rfl
-  | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
-
-/--
-Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
--/
-instance instDecidableEmpEq (ys : Array α) : Decidable (#[] = ys) :=
-  match ys with
-  | ⟨[]⟩ => isTrue rfl
-  | ⟨_ :: _⟩ => isFalse (Array.noConfusion · (List.noConfusion ·))
+instance [DecidableEq α] : DecidableEq (Array α) :=
+  fun xs ys =>
+    match h:isEqv xs ys (fun a b => a = b) with
+    | true  => isTrue (eq_of_isEqv xs ys h)
+    | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction
 
 theorem beq_eq_decide [BEq α] (xs ys : Array α) :
     (xs == ys) = if h : xs.size = ys.size then

src/Init/Data/Array/Erase.lean

@@ -6,8 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Erase
+public import Init.Data.List.Nat.Basic
 
 public section
 
@@ -88,7 +91,7 @@ theorem mem_of_mem_eraseP {xs : Array α} : a ∈ xs.eraseP p → a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_eraseP
 
-@[simp, grind =] theorem mem_eraseP_of_neg {xs : Array α} (pa : ¬p a) : a ∈ xs.eraseP p ↔ a ∈ xs := by
+@[simp, grind] theorem mem_eraseP_of_neg {xs : Array α} (pa : ¬p a) : a ∈ xs.eraseP p ↔ a ∈ xs := by
   rcases xs with ⟨xs⟩
   simpa using List.mem_eraseP_of_neg pa
 
@@ -139,16 +142,25 @@ theorem eraseP_replicate {n : Nat} {a : α} {p : α → Bool} :
   simp only [← List.toArray_replicate, List.eraseP_toArray, List.eraseP_replicate]
   split <;> simp
 
+@[deprecated eraseP_replicate (since := "2025-03-18")]
+abbrev eraseP_mkArray := @eraseP_replicate
+
 @[simp] theorem eraseP_replicate_of_pos {n : Nat} {a : α} (h : p a) :
     (replicate n a).eraseP p = replicate (n - 1) a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray]
   simp [h]
 
+@[deprecated eraseP_replicate_of_pos (since := "2025-03-18")]
+abbrev eraseP_mkArray_of_pos := @eraseP_replicate_of_pos
+
 @[simp] theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
     (replicate n a).eraseP p = replicate n a := by
   simp only [← List.toArray_replicate, List.eraseP_toArray]
   simp [h]
 
+@[deprecated eraseP_replicate_of_neg (since := "2025-03-18")]
+abbrev eraseP_mkArray_of_neg := @eraseP_replicate_of_neg
+
 theorem eraseP_eq_iff {p} {xs : Array α} :
     xs.eraseP p = ys ↔
       ((∀ a ∈ xs, ¬ p a) ∧ xs = ys) ∨
@@ -228,7 +240,7 @@ theorem mem_of_mem_erase {a b : α} {xs : Array α} (h : a ∈ xs.erase b) : a
   rcases xs with ⟨xs⟩
   simpa using List.mem_of_mem_erase (by simpa using h)
 
-@[simp, grind =] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) :
+@[simp, grind] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {xs : Array α} (ab : a ≠ b) :
     a ∈ xs.erase b ↔ a ∈ xs :=
   erase_eq_eraseP b xs ▸ mem_eraseP_of_neg (mt eq_of_beq ab.symm)
 
@@ -259,7 +271,7 @@ theorem erase_append [LawfulBEq α] {a : α} {xs ys : Array α} :
     (xs ++ ys).erase a = if a ∈ xs then xs.erase a ++ ys else xs ++ ys.erase a := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
-  simp only [List.append_toArray, List.erase_toArray, List.erase_append, List.mem_toArray]
+  simp only [List.append_toArray, List.erase_toArray, List.erase_append, mem_toArray]
   split <;> simp
 
 @[grind =]
@@ -269,6 +281,9 @@ theorem erase_replicate [LawfulBEq α] {n : Nat} {a b : α} :
   simp only [List.erase_replicate, beq_iff_eq, List.toArray_replicate]
   split <;> simp
 
+@[deprecated erase_replicate (since := "2025-03-18")]
+abbrev erase_mkArray := @erase_replicate
+
 -- The arguments `a b` are explicit,
 -- so they can be specified to prevent `simp` repeatedly applying the lemma.
 @[grind =]
@@ -296,20 +311,19 @@ theorem erase_eq_iff [LawfulBEq α] {a : α} {xs : Array α} :
   simp only [← List.toArray_replicate, List.erase_toArray]
   simp
 
+@[deprecated erase_replicate_self (since := "2025-03-18")]
+abbrev erase_mkArray_self := @erase_replicate_self
+
 @[simp] theorem erase_replicate_ne [LawfulBEq α] {a b : α} (h : !b == a) :
     (replicate n a).erase b = replicate n a := by
   rw [erase_of_not_mem]
   simp_all
 
+@[deprecated erase_replicate_ne (since := "2025-03-18")]
+abbrev erase_mkArray_ne := @erase_replicate_ne
+
 end erase
 
-/-! ### eraseIdxIfInBounds -/
-
-@[grind =]
-theorem eraseIdxIfInBounds_eq {xs : Array α} {i : Nat} :
-    xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i else xs := by
-  simp [eraseIdxIfInBounds]
-
 /-! ### eraseIdx -/
 
 theorem eraseIdx_eq_eraseIdxIfInBounds {xs : Array α} {i : Nat} (h : i < xs.size) :
@@ -411,6 +425,9 @@ theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} {h} :
   simp only [← List.toArray_replicate, List.eraseIdx_toArray]
   simp [List.eraseIdx_replicate, h]
 
+@[deprecated eraseIdx_replicate (since := "2025-03-18")]
+abbrev eraseIdx_mkArray := @eraseIdx_replicate
+
 theorem mem_eraseIdx_iff_getElem {x : α} {xs : Array α} {k} {h} : x ∈ xs.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ xs[i]'w = x := by
   rcases xs with ⟨xs⟩
   simp [List.mem_eraseIdx_iff_getElem, *]

src/Init/Data/Array/Extract.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
 
 public section
 
@@ -200,7 +201,7 @@ theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
   simp [getElem?_extract]
   omega
 
-@[simp] theorem extract_extract {as : Array α} {i j k l : Nat} :
+@[simp, grind =] theorem extract_extract {as : Array α} {i j k l : Nat} :
     (as.extract i j).extract k l = as.extract (i + k) (min (i + l) j) := by
   ext m h₁ h₂
   · simp
@@ -208,9 +209,6 @@ theorem getElem?_extract_of_succ {as : Array α} {j : Nat} :
   · simp only [size_extract] at h₁ h₂
     simp [Nat.add_assoc]
 
-grind_pattern extract_extract => (as.extract i j).extract k l where
-  as =/= #[]
-
 theorem extract_eq_empty_of_eq_empty {as : Array α} {i j : Nat} (h : as = #[]) :
     as.extract i j = #[] := by
   simp [h]
@@ -292,6 +290,9 @@ theorem extract_append_right {as bs : Array α} :
   · simp only [size_extract, size_replicate] at h₁ h₂
     simp only [getElem_extract, getElem_replicate]
 
+@[deprecated extract_replicate (since := "2025-03-18")]
+abbrev extract_mkArray := @extract_replicate
+
 theorem extract_eq_extract_right {as : Array α} {i j j' : Nat} :
     as.extract i j = as.extract i j' ↔ min (j - i) (as.size - i) = min (j' - i) (as.size - i) := by
   rcases as with ⟨as⟩
@@ -409,6 +410,8 @@ theorem popWhile_append {xs ys : Array α} :
   rcases ys with ⟨ys⟩
   simp only [List.append_toArray, List.popWhile_toArray, List.reverse_append, List.dropWhile_append,
     List.isEmpty_iff, List.isEmpty_toArray, List.isEmpty_reverse]
+  -- Why do these not fire with `simp`?
+  rw [List.popWhile_toArray, List.isEmpty_toArray, List.isEmpty_reverse]
   split
   · rfl
   · simp
@@ -427,20 +430,32 @@ theorem popWhile_append {xs ys : Array α} :
     (replicate n a).takeWhile p = (replicate n a).filter p := by
   simp [← List.toArray_replicate]
 
+@[deprecated takeWhile_replicate_eq_filter (since := "2025-03-18")]
+abbrev takeWhile_mkArray_eq_filter := @takeWhile_replicate_eq_filter
+
 theorem takeWhile_replicate {p : α → Bool} :
     (replicate n a).takeWhile p = if p a then replicate n a else #[] := by
   simp [takeWhile_replicate_eq_filter, filter_replicate]
 
+@[deprecated takeWhile_replicate (since := "2025-03-18")]
+abbrev takeWhile_mkArray := @takeWhile_replicate
+
 @[simp] theorem popWhile_replicate_eq_filter_not {p : α → Bool} :
     (replicate n a).popWhile p = (replicate n a).filter (fun a => !p a) := by
   simp [← List.toArray_replicate, ← List.filter_reverse]
 
+@[deprecated popWhile_replicate_eq_filter_not (since := "2025-03-18")]
+abbrev popWhile_mkArray_eq_filter_not := @popWhile_replicate_eq_filter_not
+
 theorem popWhile_replicate {p : α → Bool} :
     (replicate n a).popWhile p = if p a then #[] else replicate n a := by
   simp only [popWhile_replicate_eq_filter_not, size_replicate, filter_replicate, Bool.not_eq_eq_eq_not,
     Bool.not_true]
   split <;> simp_all
 
+@[deprecated popWhile_replicate (since := "2025-03-18")]
+abbrev popWhile_mkArray := @popWhile_replicate
+
 theorem extract_takeWhile {as : Array α} {i : Nat} :
     (as.takeWhile p).extract 0 i = (as.extract 0 i).takeWhile p := by
   rcases as with ⟨as⟩

src/Init/Data/Array/FinRange.lean

@@ -6,6 +6,7 @@ Authors: François G. Dorais
 module
 
 prelude
+public import Init.Data.List.FinRange
 public import Init.Data.Array.OfFn
 
 public section

src/Init/Data/Array/Find.lean

@@ -7,7 +7,10 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Attach
 public import Init.Data.Array.Range
 
 public section
@@ -24,11 +27,11 @@ open Nat
 
 /-! ### findSome? -/
 
-@[simp, grind =] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
-@[simp, grind =] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+@[simp, grind] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
+@[simp, grind] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
   cases xs; simp [List.findSome?_append]
 
-@[grind =]
+@[grind]
 theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f = f a := by
   simp
 
@@ -129,19 +132,31 @@ theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [← List.toArray_replicate, List.findSome?_replicate]
 
+@[deprecated findSome?_replicate (since := "2025-03-18")]
+abbrev findSome?_mkArray := @findSome?_replicate
+
 @[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
   simp [findSome?_replicate, Nat.ne_of_gt h]
 
+@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_pos := @findSome?_replicate_of_pos
+
 -- Argument is unused, but used to decide whether `simp` should unfold.
 @[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
    findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [findSome?_replicate]
 
+@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_isSome := @findSome?_replicate_of_isSome
+
 @[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) :
     findSome? f (replicate n a) = none := by
   rw [Option.isNone_iff_eq_none] at h
   simp [findSome?_replicate, h]
 
+@[deprecated findSome?_replicate_of_isNone (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
+
 /-! ### find? -/
 
 @[simp, grind =] theorem find?_empty : find? p #[] = none := rfl
@@ -213,12 +228,11 @@ theorem mem_of_find?_eq_some {xs : Array α} (h : find? p xs = some a) : a ∈ x
   simp at h
   simpa using List.mem_of_find?_eq_some h
 
+@[grind]
 theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by
   cases xs
   simp [List.get_find?_mem]
 
-grind_pattern get_find?_mem => (xs.find? p).get h
-
 @[simp, grind =] theorem find?_filter {xs : Array α} (p q : α → Bool) :
     (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
   cases xs; simp
@@ -263,6 +277,9 @@ theorem find?_flatten_eq_none_iff {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.find? p = none ↔ ∀ ys ∈ xss, ∀ x ∈ ys, !p x := by
   simp
 
+@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
+
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
@@ -288,6 +305,9 @@ theorem find?_flatten_eq_some_iff {xss : Array (Array α)} {p : α → Bool} {a
       ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
         by simpa using h₁, by simpa using h₂⟩
 
+@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
+abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
+
 @[simp, grind =] theorem find?_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
@@ -297,35 +317,62 @@ theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
+@[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
+abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
+
 @[grind =]
 theorem find?_replicate :
     find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
 
+@[deprecated find?_replicate (since := "2025-03-18")]
+abbrev find?_mkArray := @find?_replicate
+
 @[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
     find? p (replicate n a) = if p a then some a else none := by
   simp [find?_replicate, Nat.ne_of_gt h]
 
+@[deprecated find?_replicate_of_size_pos (since := "2025-03-18")]
+abbrev find?_mkArray_of_length_pos := @find?_replicate_of_size_pos
+
 @[simp] theorem find?_replicate_of_pos (h : p a) :
     find? p (replicate n a) = if n = 0 then none else some a := by
   simp [find?_replicate, h]
 
+@[deprecated find?_replicate_of_pos (since := "2025-03-18")]
+abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
+
 @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
   simp [find?_replicate, h]
 
+@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
+abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
+
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
 theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [← List.toArray_replicate, Classical.or_iff_not_imp_left]
 
+@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
+abbrev find?_mkArray_eq_none_iff := @find?_replicate_eq_none_iff
+
 @[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
+@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
+abbrev find?_mkArray_eq_some_iff := @find?_replicate_eq_some_iff
+
+@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
+abbrev find?_mkArray_eq_some := @find?_replicate_eq_some_iff
+
 @[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α → Bool} (h) :
     ((replicate n a).find? p).get h = a := by
   simp [← List.toArray_replicate]
 
+@[deprecated get_find?_replicate (since := "2025-03-18")]
+abbrev get_find?_mkArray := @get_find?_replicate
+
 @[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :
@@ -348,6 +395,7 @@ theorem findIdx_singleton {a : α} {p : α → Bool} :
     #[a].findIdx p = if p a then 0 else 1 := by
   simp
 
+@[grind →]
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
   rcases xs with ⟨xs⟩
   exact List.findIdx_of_getElem?_eq_some (by simpa using w)
@@ -565,6 +613,9 @@ theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
   simp only [List.findIdx?_toArray]
   simp
 
+@[deprecated findIdx?_replicate (since := "2025-03-18")]
+abbrev findIdx?_mkArray := @findIdx?_replicate
+
 theorem findIdx?_eq_findSome?_zipIdx {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/GetLit.lean

@@ -50,6 +50,6 @@ where
   getLit_eq (xs : Array α) (i : Nat) (h₁ : xs.size = n) (h₂ : i < n) : xs.getLit i h₁ h₂ = getElem xs.toList i ((id (α := xs.toList.length = n) h₁) ▸ h₂) :=
     rfl
   go (i : Nat) (hi : i ≤ xs.size) : toListLitAux xs n hsz i hi (xs.toList.drop i) = xs.toList := by
-    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop, *]
+    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop_succ_eq_drop, *]
 
 end Array

src/Init/Data/Array/InsertIdx.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.InsertIdx
 
 public section
 

src/Init/Data/Array/Lex.lean

@@ -8,3 +8,5 @@ module
 prelude
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Lemmas
+
+public section

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

@@ -6,8 +6,11 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Data.Range.Polymorphic.Iterators
-public import Init.Data.Range.Polymorphic.Nat
+public import Init.Core
+import Init.Data.Array.Basic
+import Init.Data.Nat.Lemmas
+import Init.Data.Range.Polymorphic.Iterators
+import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Iterators.Consumers
 
 public section
@@ -28,7 +31,7 @@ Specifically, `Array.lex as bs lt` is true if
 def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
   for h : i in 0...(min as.size bs.size) do
     -- TODO: `get_elem_tactic` should be able to find this itself.
-    have : i < min as.size bs.size := Std.Rco.lt_upper_of_mem h
+    have : i < min as.size bs.size := Std.PRange.lt_upper_of_mem h
     if lt as[i] bs[i] then
       return true
     else if as[i] != bs[i] then

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

@@ -10,7 +10,9 @@ import all Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Lex
+import Init.Data.Range.Polymorphic.Lemmas
 import Init.Data.Range.Polymorphic.NatLemmas
+import Init.Data.Order.Lemmas
 
 public section
 
@@ -34,24 +36,14 @@ grind_pattern _root_.List.le_toArray => l₁.toArray ≤ l₂.toArray
 grind_pattern lt_toList => xs.toList < ys.toList
 grind_pattern le_toList => xs.toList ≤ ys.toList
 
-@[simp]
-protected theorem not_lt [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-
-@[deprecated Array.not_lt (since := "2025-10-26")]
 protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-
-@[simp]
-protected theorem not_le [LT α] {xs ys : Array α} :
-    ¬ xs ≤ ys ↔ ys < xs :=
-  Classical.not_not
-
-@[deprecated Array.not_le (since := "2025-10-26")]
 protected theorem not_le_iff_gt [LT α] {xs ys : Array α} :
     ¬ xs ≤ ys ↔ ys < xs :=
   Classical.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
-  simp [lex, Std.Rco.forIn'_eq_if]
+  rw [lex, Std.PRange.forIn'_eq_match]
+  simp [Std.PRange.SupportsUpperBound.IsSatisfied]
 
 private theorem cons_lex_cons.forIn'_congr_aux [Monad m] {as bs : ρ} {_ : Membership α ρ}
     [ForIn' m ρ α inferInstance] (w : as = bs)
@@ -72,14 +64,14 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
        (lt a b || a == b && xs.lex ys lt) := by
   simp only [lex, size_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add,
-    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
+    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.PRange.forIn'_eq_forIn'_toList]
   conv =>
     lhs; congr; congr
-    rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if_roo rfl (fun _ _ _ => rfl)]
-    simp only [bind_pure_comp, map_pure]
+    rw [cons_lex_cons.forIn'_congr_aux Std.PRange.toList_eq_match rfl (fun _ _ _ => rfl)]
+    simp only [Std.PRange.SupportsUpperBound.IsSatisfied, bind_pure_comp, map_pure]
     rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.toList_roo_eq_toList_rco_of_isSome_succ? (lo := 0) (h := rfl),
-    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_rco_succ_succ,
+  simp only [Std.PRange.toList_Rox_eq_toList_Rcx_of_isSome_succ? (lo := 0) (h := rfl),
+    Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ,
     Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
     Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
   cases lt a b
@@ -91,10 +83,16 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
   | nil =>
-    cases l₂ <;> simp [lex, Std.Rco.forIn'_eq_if]
+    cases l₂
+    · rw [lex, Std.PRange.forIn'_eq_match]
+      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+    · rw [lex, Std.PRange.forIn'_eq_match]
+      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil => simp [lex, Std.Rco.forIn'_eq_if]
+    | nil =>
+      rw [lex, Std.PRange.forIn'_eq_match]
+      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 
@@ -151,7 +149,7 @@ protected theorem lt_of_le_of_lt [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrd
 @[deprecated Array.lt_of_le_of_lt (since := "2025-08-01")]
 protected theorem lt_of_le_of_lt' [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys < zs) : xs < zs :=
   letI := LE.ofLT α
@@ -165,7 +163,7 @@ protected theorem le_trans [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α]
 @[deprecated Array.le_trans (since := "2025-08-01")]
 protected theorem le_trans' [LT α]
     [i₁ : Std.Asymm (· < · : α → α → Prop)]
-    [i₂ : Std.Trichotomous (· < · : α → α → Prop)]
+    [i₂ : Std.Antisymm (¬ · < · : α → α → Prop)]
     [i₃ : Trans (¬ · < · : α → α → Prop) (¬ · < ·) (¬ · < ·)]
     {xs ys zs : Array α} (h₁ : xs ≤ ys) (h₂ : ys ≤ zs) : xs ≤ zs :=
   letI := LE.ofLT α
@@ -189,6 +187,12 @@ protected theorem le_total [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)] (xs ys : Array α) : xs ≤ ys ∨ ys ≤ xs :=
   List.le_total xs.toList ys.toList
 
+@[simp] protected theorem not_lt [LT α]
+    {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+
+@[simp] protected theorem not_le [LT α]
+    {xs ys : Array α} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
+
 protected theorem le_of_lt [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} (h : xs < ys) : xs ≤ ys :=
@@ -196,7 +200,7 @@ protected theorem le_of_lt [LT α]
 
 protected theorem le_iff_lt_or_eq [LT α]
     [Std.Irrefl (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} : xs ≤ ys ↔ xs < ys ∨ xs = ys := by
   simpa using List.le_iff_lt_or_eq (l₁ := xs.toList) (l₂ := ys.toList)
@@ -285,7 +289,7 @@ protected theorem lt_iff_exists [LT α] {xs ys : Array α} :
 
 protected theorem le_iff_exists [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)] {xs ys : Array α} :
+    [Std.Antisymm (¬ · < · : α → α → Prop)] {xs ys : Array α} :
     xs ≤ ys ↔
       (xs = ys.take xs.size) ∨
         (∃ (i : Nat) (h₁ : i < xs.size) (h₂ : i < ys.size),
@@ -304,7 +308,7 @@ theorem append_left_lt [LT α] {xs ys zs : Array α} (h : ys < zs) :
 
 theorem append_left_le [LT α]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     {xs ys zs : Array α} (h : ys ≤ zs) :
     xs ++ ys ≤ xs ++ zs := by
   cases xs
@@ -327,9 +331,9 @@ protected theorem map_lt [LT α] [LT β]
 
 protected theorem map_le [LT α] [LT β]
     [Std.Asymm (· < · : α → α → Prop)]
-    [Std.Trichotomous (· < · : α → α → Prop)]
+    [Std.Antisymm (¬ · < · : α → α → Prop)]
     [Std.Asymm (· < · : β → β → Prop)]
-    [Std.Trichotomous (· < · : β → β → Prop)]
+    [Std.Antisymm (¬ · < · : β → β → Prop)]
     {xs ys : Array α} {f : α → β} (w : ∀ x y, x < y → f x < f y) (h : xs ≤ ys) :
     map f xs ≤ map f ys := by
   cases xs

src/Init/Data/Array/MapIdx.lean

@@ -6,7 +6,10 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Attach
 public import Init.Data.Array.OfFn
 public import Init.Data.List.MapIdx
 import all Init.Data.List.MapIdx
@@ -296,6 +299,9 @@ theorem mapFinIdx_eq_replicate_iff {xs : Array α} {f : (i : Nat) → α → (h
   rw [← toList_inj]
   simp [List.mapFinIdx_eq_replicate_iff]
 
+@[deprecated mapFinIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapFinIdx_eq_mkArray_iff := @mapFinIdx_eq_replicate_iff
+
 @[simp, grind =] theorem mapFinIdx_reverse {xs : Array α} {f : (i : Nat) → α → (h : i < xs.reverse.size) → β} :
     xs.reverse.mapFinIdx f = (xs.mapFinIdx (fun i a h => f (xs.size - 1 - i) a (by simp; omega))).reverse := by
   rcases xs with ⟨l⟩
@@ -435,6 +441,9 @@ theorem mapIdx_eq_replicate_iff {xs : Array α} {f : Nat → α → β} {b : β}
   rw [← toList_inj]
   simp [List.mapIdx_eq_replicate_iff]
 
+@[deprecated mapIdx_eq_replicate_iff (since := "2025-03-18")]
+abbrev mapIdx_eq_mkArray_iff := @mapIdx_eq_replicate_iff
+
 @[simp, grind =] theorem mapIdx_reverse {xs : Array α} {f : Nat → α → β} :
     xs.reverse.mapIdx f = (mapIdx (fun i => f (xs.size - 1 - i)) xs).reverse := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/Mem.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
+public import Init.Data.Array.Basic
+public import Init.Data.Nat.Linear
 public import Init.Data.List.BasicAux
 
 public section

src/Init/Data/Array/Monadic.lean

@@ -6,9 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Control
 import all Init.Data.List.Control
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
+public import Init.Data.List.Monadic
 
 public section
 
@@ -163,7 +167,7 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : α → β
     (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
     forIn' as b f = forIn' bs b' g := by
   cases as <;> cases bs
-  simp only [mk.injEq, List.mem_toArray, List.forIn'_toArray] at w h ⊢
+  simp only [mk.injEq, mem_toArray, List.forIn'_toArray] at w h ⊢
   exact List.forIn'_congr w hb h
 
 /--

src/Init/Data/Array/OfFn.lean

@@ -6,8 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Monadic
+public import Init.Data.List.OfFn
 public import Init.Data.List.FinRange
 
 public section

src/Init/Data/Array/Perm.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Nat.Perm
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
 
@@ -84,6 +85,9 @@ theorem Perm.size_eq {xs ys : Array α} (p : xs ~ ys) : xs.size = ys.size := by
   simp only [perm_iff_toList_perm] at p
   simpa using p.length_eq
 
+@[deprecated Perm.size_eq (since := "2025-04-17")]
+abbrev Perm.length_eq := @Perm.size_eq
+
 theorem Perm.mem_iff {a : α} {xs ys : Array α} (p : xs ~ ys) : a ∈ xs ↔ a ∈ ys := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
@@ -104,7 +108,7 @@ grind_pattern Perm.append => xs ~ ys, as ~ bs, ys ++ bs
 
 theorem Perm.push (x : α) {xs ys : Array α} (p : xs ~ ys) :
     xs.push x ~ ys.push x := by
-  rw [push_eq_append]
+  rw [push_eq_append_singleton]
   exact p.append .rfl
 
 grind_pattern Perm.push => xs ~ ys, xs.push x

src/Init/Data/Array/QSort.lean

@@ -7,3 +7,5 @@ module
 
 prelude
 public import Init.Data.Array.QSort.Basic
+
+public section

src/Init/Data/Array/Range.lean

@@ -6,10 +6,14 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.OfFn
 import all Init.Data.Array.OfFn
 public import Init.Data.Array.MapIdx
 public import Init.Data.Array.Zip
+public import Init.Data.List.Nat.Range
 
 public section
 
@@ -112,7 +116,7 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
   rw [← List.toArray_range']
-  simp only [List.find?_toArray, List.mem_toArray]
+  simp only [List.find?_toArray, mem_toArray]
   simp [List.find?_range'_eq_some]
 
 @[simp] theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :

src/Init/Data/Array/Subarray.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
+public import Init.GetElem
 import Init.Data.Array.GetLit
 public import Init.Data.Slice.Basic
 

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

@@ -7,6 +7,7 @@ Authors: David Thrane Christiansen
 module
 
 prelude
+public import Init.Data.Array.Basic
 public import Init.Data.Array.Subarray
 import all Init.Data.Array.Subarray
 public import Init.Omega

src/Init/Data/Array/TakeDrop.lean

@@ -6,8 +6,10 @@ Authors: Markus Himmel
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
 
 public section
 

src/Init/Data/Array/Zip.lean

@@ -6,8 +6,10 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.Array.TakeDrop
+public import Init.Data.List.Zip
 
 public section
 
@@ -166,6 +168,9 @@ theorem zipWith_eq_append_iff {f : α → β → γ} {as : Array α} {bs : Array
     zipWith f (replicate m a) (replicate n b) = replicate (min m n) (f a b) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zipWith_replicate (since := "2025-03-18")]
+abbrev zipWith_mkArray := @zipWith_replicate
+
 theorem map_uncurry_zip_eq_zipWith {f : α → β → γ} {as : Array α} {bs : Array β} :
     map (Function.uncurry f) (as.zip bs) = zipWith f as bs := by
   cases as
@@ -291,6 +296,9 @@ theorem zip_eq_append_iff {as : Array α} {bs : Array β} :
     zip (replicate m a) (replicate n b) = replicate (min m n) (a, b) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zip_replicate (since := "2025-03-18")]
+abbrev zip_mkArray := @zip_replicate
+
 theorem zip_eq_zip_take_min {as : Array α} {bs : Array β} :
     zip as bs = zip (as.take (min as.size bs.size)) (bs.take (min as.size bs.size)) := by
   cases as
@@ -342,6 +350,9 @@ theorem map_zipWithAll {δ : Type _} {f : α → β} {g : Option γ → Option
     zipWithAll f (replicate n a) (replicate n b) = replicate n (f (some a) (some b)) := by
   simp [← List.toArray_replicate]
 
+@[deprecated zipWithAll_replicate (since := "2025-03-18")]
+abbrev zipWithAll_mkArray := @zipWithAll_replicate
+
 /-! ### zipWithM -/
 
 @[simp, grind =]
@@ -399,4 +410,7 @@ theorem zip_of_prod {as : Array α} {bs : Array β} {xs : Array (α × β)} (hl
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by
   ext1 <;> simp
 
+@[deprecated unzip_replicate (since := "2025-03-18")]
+abbrev unzip_mkArray := @unzip_replicate
+
 end Array

src/Init/Data/Basic.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.Nat.Basic
+public import Init.Data.Fin.Basic
+public import Init.Data.List.Basic
+public import Init.Data.Char.Basic
+public import Init.Data.String.Basic
+public import Init.Data.Option.Basic
+public import Init.Data.UInt
+public import Init.Data.Repr
+public import Init.Data.ToString.Basic
+public import Init.Data.String.Extra
+
+public section

src/Init/Data/BitVec.lean

@@ -13,3 +13,5 @@ public import Init.Data.BitVec.Bitblast
 public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
+
+public section

src/Init/Data/BitVec/Basic.lean

@@ -6,8 +6,11 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
+public import Init.Data.Fin.Basic
 public import Init.Data.Nat.Bitwise.Lemmas
+public import Init.Data.Nat.Power2
 public import Init.Data.Int.Bitwise.Basic
+public import Init.Data.BitVec.BasicAux
 
 @[expose] public section
 
@@ -26,6 +29,10 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
+@[inline, deprecated BitVec.ofNatLT (since := "2025-02-13"), inherit_doc BitVec.ofNatLT]
+protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n :=
+  BitVec.ofNatLT i p
+
 section Nat
 
 /--
@@ -203,8 +210,8 @@ If `n` is `0`, then one digit is returned. Otherwise, `⌊(n + 3) / 4⌋` digits
 -- `Internal` string functions by moving this definition out to a separate file that can live
 -- downstream of `Init.Data.String.Basic`.
 protected def toHex {n : Nat} (x : BitVec n) : String :=
-  let s := String.ofList (Nat.toDigits 16 x.toNat)
-  let t := String.ofList (List.replicate ((n+3) / 4 - String.Internal.length s) '0')
+  let s := (Nat.toDigits 16 x.toNat).asString
+  let t := (List.replicate ((n+3) / 4 - String.Internal.length s) '0').asString
   String.Internal.append t s
 
 /-- `BitVec` representation. -/
@@ -867,7 +874,4 @@ def clzAuxRec {w : Nat} (x : BitVec w) (n : Nat) : BitVec w :=
 /-- Count the number of leading zeros. -/
 def clz (x : BitVec w) : BitVec w := clzAuxRec x (w - 1)
 
-/-- Count the number of trailing zeros. -/
-def ctz (x : BitVec w) : BitVec w := (x.reverse).clz
-
 end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -6,13 +6,17 @@ Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix, Siddharth Bhat
 module
 
 prelude
+public import Init.Data.Nat.Bitwise.Basic
 import all Init.Data.Nat.Bitwise.Basic
+public import Init.Data.Nat.Mod
 public import Init.Data.Int.DivMod
 import all Init.Data.Int.DivMod
+public import Init.Data.Int.LemmasAux
+public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Decidable
+public import Init.Data.BitVec.Lemmas
 public import Init.Data.BitVec.Folds
-import Init.BinderPredicates
 
 @[expose] public section
 
@@ -635,11 +639,12 @@ theorem mulRec_eq_mul_signExtend_setWidth (x y : BitVec w) (s : Nat) :
     simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
     by_cases y.getLsbD 0
     case pos hy =>
-      simp only [hy, ↓reduceIte, setWidth_one, ofBool_true, ofNat_eq_ofNat]
+      simp only [hy, ↓reduceIte, setWidth_one_eq_ofBool_getLsb_zero,
+        ofBool_true, ofNat_eq_ofNat]
       rw [setWidth_ofNat_one_eq_ofNat_one_of_lt (by omega)]
       simp
     case neg hy =>
-      simp [hy, setWidth_one]
+      simp [hy, setWidth_one_eq_ofBool_getLsb_zero]
   case succ s' hs =>
     rw [mulRec_succ_eq, hs]
     have heq :
@@ -1024,7 +1029,7 @@ theorem lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) :
     case neg.hrWidth =>
       simp only
       have hdr' : d ≤ (qr.r.shiftConcat (n.getLsbD (qr.wn - 1))) :=
-        BitVec.not_lt.mp rltd
+        BitVec.not_lt_iff_le.mp rltd
       have hr' : ((qr.r.shiftConcat (n.getLsbD (qr.wn - 1)))).toNat < 2 ^ (qr.wr + 1) := by
         apply toNat_shiftConcat_lt_of_lt <;> bv_omega
       rw [BitVec.toNat_sub_of_le hdr']
@@ -1032,7 +1037,7 @@ theorem lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) :
     case neg.hqWidth =>
       apply toNat_shiftConcat_lt_of_lt <;> omega
     case neg.hdiv =>
-      have rltd' := (BitVec.not_lt.mp rltd)
+      have rltd' := (BitVec.not_lt_iff_le.mp rltd)
       simp only [qr.toNat_shiftRight_sub_one_eq h,
         BitVec.toNat_sub_of_le rltd',
         toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hrWidth]
@@ -1406,7 +1411,7 @@ theorem eq_iff_eq_of_inv (f : α → BitVec w) (g : BitVec w → α) (h : ∀ x,
     have := congrArg g h'
     simpa [h] using this
 
-@[deprecated BitVec.ne_intMin_of_msb_eq_false (since := "2025-10-26")]
+@[simp]
 theorem ne_intMin_of_lt_of_msb_false {x : BitVec w} (hw : 0 < w) (hx : x.msb = false) :
     x ≠ intMin w := by
   have := toNat_lt_of_msb_false hx
@@ -1511,7 +1516,7 @@ theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
   by_cases hx : x.msb <;> by_cases hy : y.msb
   <;> simp only [hx, hy, neg_ne_intMin_inj]
   <;> simp only [Bool.not_eq_true] at hx hy
-  <;> apply ne_intMin_of_msb_eq_false (by omega)
+  <;> apply ne_intMin_of_lt_of_msb_false (by omega)
   <;> rw [msb_udiv]
   <;> try simp only [hx, Bool.false_and]
   · simp [h, ne_zero_of_msb_true, hx]
@@ -1623,7 +1628,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
             · have ry := (intMin_udiv_eq_intMin_iff b).mp
               simp only [hb1, imp_false] at ry
               simp [msb_udiv, ha_intMin, hb1, ry, intMin_udiv_ne_zero_of_ne_zero, hb, hb0]
-            · have := @BitVec.ne_intMin_of_msb_eq_false w wpos ((-a) / b) (by simp [ha, ha0, ha_intMin])
+            · have := @BitVec.ne_intMin_of_lt_of_msb_false w ((-a) / b) wpos (by simp [ha, ha0, ha_intMin])
               simp [msb_neg, h', this, ha, ha_intMin]
       rw [toInt_eq_toNat_of_msb hb, toInt_eq_neg_toNat_neg_of_msb_true ha, Int.neg_tdiv,
         Int.tdiv_eq_ediv_of_nonneg (by omega), sdiv_toInt_of_msb_true_of_msb_false]
@@ -1634,7 +1639,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
         rw [toInt_udiv_of_msb ha, toInt_eq_toNat_of_msb ha]
         rw [toInt_eq_neg_toNat_neg_of_msb_true hb, Int.tdiv_neg, Int.tdiv_eq_ediv_of_nonneg (by omega)]
       · apply sdiv_ne_intMin_of_ne_intMin
-        apply ne_intMin_of_msb_eq_false (by omega) ha
+        apply ne_intMin_of_lt_of_msb_false (by omega) ha
     · rw [sdiv, Int.tdiv_cases, udiv_eq, neg_eq, if_pos (toInt_nonneg_of_msb_false ha),
         if_pos (toInt_nonneg_of_msb_false hb), ha, hb, toInt_udiv_of_msb ha,
         toInt_eq_toNat_of_msb ha, toInt_eq_toNat_of_msb hb]
@@ -1926,7 +1931,7 @@ theorem toInt_sub_neg_umod {x y : BitVec w} (hxmsb : x.msb = true) (hymsb : y.ms
       rw [Int.bmod_eq_of_le (by omega) (by omega)]
       simp only [toInt_eq_toNat_of_msb hymsb, BitVec.toInt_eq_neg_toNat_neg_of_msb_true hxmsb,
         Int.dvd_neg] at hdvd
-      simp only [hdvd, ↓reduceIte, Int.natAbs_natCast]
+      simp only [hdvd, ↓reduceIte, Int.natAbs_cast]
 
 theorem srem_zero_of_dvd {x y : BitVec w} (h : y.toInt ∣ x.toInt) :
     x.srem y = 0#w := by