feat: some missing Array grind annotations

This PR makes use of `hasIndepIndices`. That function was unused since
commit 54f6517ca3, but it seems it should
be used.

.claude/CLAUDE.md

@@ -0,0 +1,14 @@
+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.
+
+To build Lean you should use `make -j$(nproc) -C build/release`.
+
+To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
+
+*Never* report success on a task unless you have verified both a clean build without errors, and that the relevant tests pass. You have to keep working until you have verified both of these.
+
+All new tests should go in `tests/lean/run/`. Note that these tests don't have expected output, and just run on a success or failure basis. So you should use `#guard_msgs` to check for specific messages.
+
+If you are not following best practices specific to this repository and the user expresses frustration, stop and ask them to help update this `.claude/CLAUDE.md` file with the missing guidance.

.claude/commands/release.md

@@ -0,0 +1,69 @@
+# 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

.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@v7
+        uses: actions/github-script@v8
         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@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const { labels, number: prNumber } = context.payload.pull_request;

.github/workflows/build-template.yml

@@ -3,9 +3,6 @@ name: build-template
 on:
   workflow_call:
     inputs:
-      check-level:
-        type: string
-        required: true
       config:
         type: string
         required: true
@@ -116,10 +113,10 @@ jobs:
             build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
-          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v4-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
-            ${{ matrix.name }}-build-v3
+            ${{ matrix.name }}-build-v4
       # open nix-shell once for initial setup
       - name: Setup
         run: |
@@ -230,7 +227,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.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
+        if: matrix.test
       - name: Test Summary
         uses: test-summary/action@v2
         with:

.github/workflows/check-stage0.yml

@@ -11,8 +11,8 @@ jobs:
     - uses: actions/checkout@v5
       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@v7
+      uses: actions/github-script@v8
       with:
         script: |
           const { owner, repo, number: issue_number  } = context.issue;

.github/workflows/ci.yml

@@ -31,10 +31,6 @@ 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
@@ -110,6 +106,9 @@ jobs:
           TAG_NAME="${GITHUB_REF##*/}"
           echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
 
+      # 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)
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -117,6 +116,7 @@ jobs:
         # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
         run: |
           check_level=0
+          fast=false
 
           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
@@ -129,19 +129,24 @@ jobs:
             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@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
-            console.log(`level: ${level}`);
+            const fast = ${{ steps.set-level.outputs.fast }};
+            console.log(`level: ${level}, fast: ${fast}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
@@ -152,7 +157,8 @@ jobs:
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "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*",
@@ -165,17 +171,19 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                "os": "ubuntu-latest",
+                // usually not a bottleneck so make exclusive to `fast-ci`
+                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests 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.
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1 || isPushToMaster,
+                "test": level >= 1,
+                "secondary": level == 0,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -186,26 +194,28 @@ jobs:
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "check-level": 0,
-                "test": true,
+                "enabled": 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,
-                // made explicit until it can be assumed to have propagated to PRs
-                "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
+                // We are not warning-free yet on all platforms, start here
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
               },
               {
                 "name": "Linux Reldebug",
                 "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "CMAKE_PRESET": "reldebug",
               },
               // TODO: suddenly started failing in CI
               /*{
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
                 // exclude seriously slow/problematic tests (laketests crash)
@@ -213,9 +223,10 @@ jobs:
               },*/
               {
                 "name": "macOS",
-                "os": "macos-13",
+                "os": "macos-15-intel",
                 "release": true,
-                "check-level": 2,
+                "test": false,  // Tier 2 platform
+                "enabled": 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*",
@@ -226,7 +237,7 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && !isPr ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
+                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -235,14 +246,16 @@ 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
-                "check-level": isPr ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1,
+                "test": level >= 1,
+                "secondary": level == 0,
               },
               {
                 "name": "Windows",
-                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "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",
@@ -254,7 +267,8 @@ jobs:
                 "os": "nscloud-ubuntu-22.04-arm64-4x16",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "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*",
@@ -267,7 +281,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,
-              //  "check-level": 2,
+              //  "enabled": level >= 2,
               //  "cross": true,
               //  "shell": "bash -euxo pipefail {0}"
               //}
@@ -279,7 +293,7 @@ jobs:
               //   "wasm": true,
               //   "cmultilib": true,
               //   "release": true,
-              //   "check-level": 2,
+              //   "enabled": level >= 2,
               //   "cross": true,
               //   "shell": "bash -euxo pipefail {0}",
               //   // Just a few selected tests because wasm is slow
@@ -293,7 +307,7 @@ jobs:
               }
             }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            matrix = matrix.filter((job) => level >= job["check-level"]);
+            matrix = matrix.filter((job) => job["enabled"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
             core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
 
@@ -303,7 +317,6 @@ 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 }}
@@ -319,7 +332,6 @@ 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 }}
@@ -350,7 +362,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@v7
+      uses: actions/github-script@v8
       with:
         script: |
             core.setFailed('Some jobs failed')
@@ -367,7 +379,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -392,6 +404,8 @@ jobs:
         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@v5
         with:
@@ -411,7 +425,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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         with:
           body_path: diff.md
           prerelease: true

.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@v7
+        uses: actions/github-script@v8
         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@v7
+      uses: actions/github-script@v8
       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@v7
+        uses: actions/github-script@v8
         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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         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@72f2c25fcb47643c292f7107632f7a47c1df5cd8
+        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
         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@v7
+        uses: actions/github-script@v8
         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@v7
+        uses: actions/github-script@v8
         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@v7
+        uses: actions/github-script@v8
         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@v7
+        uses: actions/github-script@v8
         with:
           script: |
             const description =
@@ -401,6 +401,7 @@ jobs:
           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'
@@ -425,7 +426,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 -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit --allow-empty -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 }}
@@ -434,7 +435,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 -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes
@@ -460,6 +461,7 @@ jobs:
           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: |
@@ -494,7 +496,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 -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit --allow-empty -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 }}
@@ -505,7 +507,7 @@ jobs:
             git add lean-toolchain
             lake update batteries
             git add lake-manifest.json
-            git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
           fi
 
       - name: Push changes
@@ -530,6 +532,7 @@ jobs:
           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'
@@ -555,7 +558,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 -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit --allow-empty -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 }}
@@ -565,7 +568,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 -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
+            git commit --allow-empty -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@v7
+        uses: actions/github-script@v8
         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): .*[^.]($|\n\n)/.test(msg)) {
+            if (!/^(feat|fix|doc|style|refactor|test|chore|perf): (?![A-Z][a-z]).*[^.]($|\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@v9
+      - uses: actions/stale@v10
         with:
           days-before-stale: -1
           days-before-pr-stale: 30

.github/workflows/update-stage0.yml

@@ -69,10 +69,10 @@ jobs:
           build/stage1/**/*.ir
           build/stage1/**/*.c
           build/stage1/**/*.c.o*
-        key: Linux Lake-build-v3-${{ github.sha }}
+        key: Linux Lake-build-v4-${{ github.sha }}
         # fall back to (latest) previous cache
         restore-keys: |
-          Linux Lake-build-v3
+          Linux Lake-build-v4
     - if: env.should_update_stage0 == 'yes'
       # sync options with `Linux Lake` to ensure cache reuse
       run: |

.gitignore

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

CODEOWNERS

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

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`, 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`, `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)`
 * 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.
 
@@ -141,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 *);
-lean_object * initialize_C(uint8_t builtin, lean_object *);
+lean_object * initialize_A_B(uint8_t builtin);
+lean_object * initialize_C(uint8_t builtin);
 ...
 
 argv = lean_setup_args(argc, argv); // if using process-related functionality
@@ -152,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, lean_io_mk_world());
+res = initialize_A_B(builtin);
 if (lean_io_result_is_ok(res)) {
     lean_dec_ref(res);
 } else {
@@ -160,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, lean_io_mk_world());
+res = initialize_C(builtin);
 if (lean_io_result_is_ok(res)) {
 ...
 

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.
-      --^ textDocument/completion
+      --^ 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,10 +94,8 @@ 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 =>
-    have : a = b := by simp_all
-    subst this
-    have : as.reverse = as := by simp_all
-    exact Palindrome.sandwich a (ih this)
+    obtain ⟨rfl, h, -⟩ := by simpa using h
+    exact Palindrome.sandwich b (ih h)
 
 /-!
 We now define a function that returns `true` iff `as` is a palindrome.

flake.nix

@@ -25,6 +25,7 @@
         } ({
           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,9 +8,15 @@
 		},
 		{
 			"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",

script/Modulize.lean

@@ -0,0 +1,75 @@
+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

@@ -0,0 +1,616 @@
+/-
+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.endPos 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 ++ text.extract 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 ++ text.extract pos insertion
+    for mod in add do
+      if !seen.contains mod then
+        seen := seen.insert mod
+        out := out ++ s!"{mod}\n"
+    out := out ++ text.extract 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/lakefile.toml

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

script/lean-toolchain

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

script/release_checklist.py

@@ -1,5 +1,58 @@
 #!/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
+
+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
@@ -76,6 +129,39 @@ 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
@@ -84,20 +170,17 @@ 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 as e:
-        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
+
+    except requests.exceptions.RequestException:
         return None
-    except Exception as e:
-        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
+    except Exception:
         return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
@@ -286,6 +369,68 @@ 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 {}
@@ -404,30 +549,57 @@ 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
 
-    if not release_page_exists(lean_repo_url, toolchain, github_token):
-        print(f"  ❌ Release page for {toolchain} does not exist")
+    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}")
+
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-        
-    # Check the actual release notes page title
+
+    # Check the actual release notes page title (informational only - does not block)
     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:
-        # Error already printed by get_release_notes
-        lean4_success = False
+        print(f"  ⚠️  Release notes not found at {release_notes_url} (this will be fixed while updating the reference-manual repository)")
     elif not actual_title.startswith(expected_title_prefix):
-        # 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
+        print(f"  ⚠️  Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {release_notes_url}")
     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...")
 
@@ -471,6 +643,19 @@ 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")

script/release_steps.py

@@ -1,30 +1,53 @@
 #!/usr/bin/env python3
 
 """
-Execute release steps for Lean4 repositories.
+Execute Release Steps for Lean4 Downstream Repositories
 
-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.
+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)
 
 Usage:
-    python3 release_steps.py <version> <repo>
+    ./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
 
-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
+The script reads repository configurations from release_repos.yml.
+Each repository has specific handling for merging, dependencies, and testing.
 
-Example:
-    python3 release_steps.py v4.6.0 mathlib4
-    python3 release_steps.py v4.6.0 batteries
+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.
 
-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
+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
 """
 
 import argparse
@@ -566,8 +589,19 @@ def execute_release_steps(repo, version, config):
         
         # Clean lake cache for a fresh build
         print(blue("Cleaning lake cache..."))
-        run_command("rm -rf .lake", cwd=repo_path)
-        
+        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}"))
+
         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 25)
+set(LEAN_VERSION_MINOR 26)
 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,7 +34,14 @@ if (NOT LEAN_PLATFORM_TARGET)
     OUTPUT_VARIABLE LEAN_PLATFORM_TARGET OUTPUT_STRIP_TRAILING_WHITESPACE)
 endif()
 
-set(LEAN_EXTRA_LINKER_FLAGS "" CACHE STRING "Additional flags used by the linker")
+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")
 set(LEAN_TEST_VARS "LEAN_CC=${CMAKE_C_COMPILER}" CACHE STRING "Additional environment variables used when running tests")
 
@@ -82,6 +89,7 @@ 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`")
@@ -797,6 +805,9 @@ 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()
@@ -823,10 +834,13 @@ if(LEAN_INSTALL_PREFIX)
   set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
 endif()
 
-if (STAGE GREATER 1)
+
+if (USE_LAKE_CACHE AND STAGE EQUAL 1)
+  set(LAKE_ARTIFACT_CACHE_TOML "true")
+else()
   # 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
-  string(APPEND LEAN_EXTRA_LAKEFILE_TOML "\n\nenableArtifactCache = false")
+  set(LAKE_ARTIFACT_CACHE_TOML "false")
 endif()
 
 # Escape for `make`. Yes, twice.
@@ -844,15 +858,13 @@ 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_SYSTEM_NAME} MATCHES "Windows")
-  set(LAKE_LIB_PREFIX "lib")
+if(${CMAKE_BUILD_TYPE} MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
+  set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")
+else()
+  set(CMAKE_BUILD_TYPE_TOML "Release")
 endif()
 
 if(USE_LAKE)

src/Init.lean

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

src/Init/BinderNameHint.lean

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

src/Init/ByCases.lean

@@ -44,3 +44,10 @@ 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
 
-public section
+@[expose] public section
 
 universe u v
 
@@ -181,9 +181,6 @@ 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

src/Init/Control.lean

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

@@ -45,9 +45,6 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
     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`.
 -/

src/Init/Control/EState.lean

@@ -6,8 +6,6 @@ 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,7 +10,6 @@ module
 prelude
 public import Init.Control.Basic
 public import Init.Control.Id
-public import Init.Coe
 
 @[expose] public section
 

src/Init/Control/Lawful.lean

@@ -10,5 +10,3 @@ 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,8 +7,6 @@ module
 
 prelude
 public import Init.Ext
-public import Init.SimpLemmas
-public import Init.Meta
 
 public section
 
@@ -172,6 +170,7 @@ 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]
 
@@ -252,24 +251,9 @@ 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,12 +7,11 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Control.Except
 import all Init.Control.Except
-public import Init.Control.State
+public import Init.Control.Option
+import all Init.Control.Option
 import all Init.Control.State
 public import Init.Control.StateRef
-public import Init.Ext
 
 public section
 
@@ -110,6 +109,121 @@ 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,7 +7,6 @@ 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,5 +9,3 @@ 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,17 +6,13 @@ 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
@@ -64,10 +60,6 @@ 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, monadLift_map, monadLift_bind]
+  simp only [seq_eq_bind_map, 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,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Option.Basic
-public import Init.Control.Basic
 public import Init.Control.Except
 
 public section
@@ -28,7 +27,7 @@ failure occurred.
 /--
 Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
   x
 
@@ -39,13 +38,14 @@ 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]
+@[always_inline, inline, expose]
 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]
+@[always_inline, inline, expose]
 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] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] 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] protected def fail : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] 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] protected def lift (x : m α) : OptionT m α := OptionT.mk do
+@[always_inline, inline, expose] 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] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
-  let some a ← x | handle ()
+@[always_inline, inline, expose] protected def tryCatch (x : OptionT m α) (handle : PUnit → OptionT m α) : OptionT m α := OptionT.mk do
+  let some a ← x | handle ⟨⟩
   pure <| some a
 
-instance : MonadExceptOf Unit (OptionT m) where
+instance : MonadExceptOf PUnit (OptionT m) where
   throw    := fun _ => OptionT.fail
   tryCatch := OptionT.tryCatch
 

src/Init/Control/Reader.lean

@@ -8,8 +8,6 @@ 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,8 +8,6 @@ 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,7 +8,6 @@ notation, basic datatypes and type classes
 module
 
 prelude
-public meta import Init.Prelude
 public import Init.SizeOf
 
 public section
@@ -144,8 +143,9 @@ 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.
-@[inline] private def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
-@[csimp] private theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
+/-- Implementation detail. -/
+@[inline] def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
+@[csimp] 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
@@ -600,17 +600,6 @@ 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 }`. -/
@@ -1095,14 +1084,6 @@ 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
 
@@ -1165,6 +1146,7 @@ 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
@@ -1206,17 +1188,13 @@ theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c
   | isTrue hc   => absurd hc hnc
   | isFalse _   => rfl
 
--- 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
-
+@[macro_inline]
 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
@@ -1367,12 +1345,12 @@ namespace Subtype
 theorem exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
   | ⟨a, h⟩ => ⟨a, h⟩
 
-set_option linter.missingDocs false in
-@[deprecated exists_of_subtype (since := "2025-04-04")]
-abbrev existsOfSubtype := @exists_of_subtype
+variable {α : Sort u} {p : α → Prop}
 
-variable {α : Type u} {p : α → Prop}
+protected theorem ext : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
+@[deprecated Subtype.ext (since := "2025-10-26")]
 protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
@@ -1387,9 +1365,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.eq (eq_of_beq h)
+  eq_of_beq h := Subtype.ext (eq_of_beq h)
 
-instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
+instance {α : Sort 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))
@@ -1490,6 +1468,8 @@ 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
 
@@ -1506,20 +1486,24 @@ 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.subsingleton a ⟨⟩
+  PUnit.ext a ⟨⟩
 
 instance : Subsingleton PUnit :=
-  Subsingleton.intro PUnit.subsingleton
+  Subsingleton.intro PUnit.ext
 
 instance : Inhabited PUnit where
   default := ⟨⟩
 
 instance : DecidableEq PUnit :=
-  fun a b => isTrue (PUnit.subsingleton a b)
+  fun a b => isTrue (PUnit.ext a b)
 
 /-! # Setoid -/
 
@@ -1605,7 +1589,7 @@ gen_injective_theorems% PSigma
 gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
-gen_injective_theorems% String.Pos
+gen_injective_theorems% String.Pos.Raw
 gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum

src/Init/Data.lean

@@ -6,7 +6,6 @@ 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
@@ -30,6 +29,7 @@ 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,5 +52,3 @@ 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,7 +7,6 @@ Authors: Dany Fabian
 module
 
 prelude
-public import Init.Classical
 public import Init.ByCases
 
 @[expose] public section

src/Init/Data/Array.lean

@@ -30,5 +30,3 @@ 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,10 +6,7 @@ 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
@@ -84,10 +81,10 @@ well-founded recursion mechanism to prove that the function terminates.
   simp [pmap]
 
 /-- Implementation of `pmap` using the zero-copy version of `attach`. -/
-@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
+@[inline] 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] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] 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]
@@ -752,9 +749,6 @@ 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,10 +6,6 @@ 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
@@ -213,20 +209,6 @@ 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.
@@ -244,7 +226,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] theorem size_swap {xs : Array α} {i j : Nat} {hi hj} : (xs.swap i j hi hj).size = xs.size := by
+@[simp, grind =] 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]
@@ -466,7 +448,7 @@ Examples:
 -/
 abbrev take (xs : Array α) (i : Nat) : Array α := extract xs 0 i
 
-@[simp] theorem take_eq_extract {xs : Array α} {i : Nat} : xs.take i = xs.extract 0 i := rfl
+@[simp, grind =] 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.
@@ -480,7 +462,7 @@ Examples:
 -/
 abbrev drop (xs : Array α) (i : Nat) : Array α := extract xs i xs.size
 
-@[simp] theorem drop_eq_extract {xs : Array α} {i : Nat} : xs.drop i = xs.extract i xs.size := rfl
+@[simp, grind =] 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
@@ -752,8 +734,7 @@ 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 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    map (i : Nat) (bs : Array β) : m (Array β) := do
+  let rec map (i : Nat) (bs : Array β) : m (Array β) := do
       if hlt : i < as.size then
         map (i+1) (bs.push (← f as[i]))
       else
@@ -913,8 +894,7 @@ 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 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-    loop (j : Nat) : m Bool := do
+    let rec 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
@@ -1252,8 +1232,7 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -1270,8 +1249,7 @@ Examples:
 -/
 @[inline]
 def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some ⟨j, h⟩ else loop (j + 1)
     else none
@@ -1307,7 +1285,6 @@ 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⟩
@@ -1717,7 +1694,6 @@ 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
@@ -1728,7 +1704,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
     as
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-@[simp] theorem popWhile_empty {p : α → Bool} :
+@[simp, grind =] theorem popWhile_empty {p : α → Bool} :
     popWhile p #[] = #[] := by
   simp [popWhile]
 
@@ -1742,8 +1718,7 @@ Examples:
  * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]`
 -/
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  go (i : Nat) (acc : Array α) : Array α :=
+  let rec go (i : Nat) (acc : Array α) : Array α :=
     if h : i < as.size then
       let a := as[i]
       if p a then
@@ -1766,7 +1741,6 @@ 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
@@ -1777,7 +1751,8 @@ termination_by xs.size - i
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
 
 -- This is required in `Lean.Data.PersistentHashMap`.
-@[simp] theorem size_eraseIdx {xs : Array α} (i : Nat) (h) : (xs.eraseIdx i h).size = xs.size - 1 := by
+@[simp, grind =]
+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
@@ -1799,7 +1774,6 @@ 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
 
@@ -1862,8 +1836,7 @@ 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 @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
-  loop (as : Array α) (j : Fin as.size) :=
+  let rec 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
@@ -1917,7 +1890,6 @@ 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]
@@ -1946,7 +1918,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
+@[specialize]
 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]
@@ -2109,7 +2081,6 @@ 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)
@@ -2163,5 +2134,3 @@ 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,10 +6,8 @@ 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,9 +6,7 @@ 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,7 +8,6 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 
 public section
@@ -32,7 +31,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_succ_eq_drop ‹_›]
+    rw (occs := [2]) [← List.getElem_cons_drop ‹_›]
     simp
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; simp
 

src/Init/Data/Array/Count.lean

@@ -6,7 +6,6 @@ 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
@@ -63,7 +62,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]
@@ -100,9 +99,6 @@ 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⟩
@@ -263,15 +259,9 @@ 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]
@@ -285,9 +275,6 @@ 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,11 +6,9 @@ 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
 

src/Init/Data/Array/Erase.lean

@@ -6,11 +6,8 @@ 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
 
@@ -142,25 +139,16 @@ 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) ∨
@@ -281,9 +269,6 @@ 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 =]
@@ -311,19 +296,20 @@ 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) :
@@ -425,9 +411,6 @@ 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,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.TakeDrop
 
 public section
 
@@ -290,9 +289,6 @@ 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⟩
@@ -430,32 +426,20 @@ 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,7 +6,6 @@ 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,10 +7,7 @@ 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
@@ -132,31 +129,19 @@ 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
@@ -321,16 +306,10 @@ theorem find?_replicate :
     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]
 
@@ -586,9 +565,6 @@ 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_succ_eq_drop, *]
+    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop, *]
 
 end Array

src/Init/Data/Array/InsertIdx.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -6,17 +6,10 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-public import Init.Data.Nat.Lemmas
-public import Init.Data.List.Range
-public import Init.Data.List.Nat.TakeDrop
-public import Init.Data.List.Nat.Modify
 public import Init.Data.List.Nat.Basic
-public import Init.Data.List.Monadic
-public import Init.Data.List.OfFn
 public import Init.Data.Array.Mem
 public import Init.Data.Array.DecidableEq
 public import Init.Data.Range.Lemmas
-public import Init.TacticsExtra
 public import Init.Data.List.ToArray
 import all Init.Data.List.Control
 import all Init.Data.Array.Basic
@@ -252,12 +245,13 @@ theorem back_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.pus
   replace h := List.append_inj_right' h (by simp)
   simpa using h
 
-theorem pop_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys := by
+theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys := by
   cases xs
   cases ys
-  simp at h
-  replace h := List.append_inj_left' h (by simp)
-  simp [h]
+  simp [And.comm]
+
+theorem pop_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys :=
+  (push_eq_push.1 h).2
 
 theorem push_inj_left {a : α} {xs ys : Array α} : xs.push a = ys.push a ↔ xs = ys :=
   ⟨pop_eq_of_push_eq, fun h => by simp [h]⟩
@@ -265,15 +259,6 @@ theorem push_inj_left {a : α} {xs ys : Array α} : xs.push a = ys.push a ↔ xs
 theorem push_inj_right {a b : α} {xs : Array α} : xs.push a = xs.push b ↔ a = b :=
   ⟨back_eq_of_push_eq, fun h => by simp [h]⟩
 
-theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys := by
-  constructor
-  · intro h
-    exact ⟨back_eq_of_push_eq h, pop_eq_of_push_eq h⟩
-  · rintro ⟨rfl, rfl⟩
-    rfl
-
-theorem push_eq_append_singleton {as : Array α} {x : α} : as.push x = as ++ #[x] := rfl
-
 theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) :
     ∃ (ys : Array α) (a : α), xs = ys.push a := by
   rcases xs with ⟨xs⟩
@@ -324,41 +309,23 @@ theorem singleton_inj : #[a] = #[b] ↔ a = b := by
 @[simp, grind =] theorem size_replicate {n : Nat} {v : α} : (replicate n v).size = n :=
   List.length_replicate ..
 
-@[deprecated size_replicate (since := "2025-03-18")]
-abbrev size_mkArray := @size_replicate
-
 @[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := by
   simp only [replicate]
 
-@[deprecated toList_replicate (since := "2025-03-18")]
-abbrev toList_mkArray := @toList_replicate
-
 @[simp, grind =] theorem replicate_zero : replicate 0 a = #[] := rfl
 
-@[deprecated replicate_zero (since := "2025-03-18")]
-abbrev mkArray_zero := @replicate_zero
-
 @[grind =]
 theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
   apply toList_inj.1
   simp [List.replicate_succ']
 
-@[deprecated replicate_succ (since := "2025-03-18")]
-abbrev mkArray_succ := @replicate_succ
-
 @[simp, grind =] theorem getElem_replicate {n : Nat} {v : α} {i : Nat} (h : i < (replicate n v).size) :
     (replicate n v)[i] = v := by simp [← getElem_toList]
 
-@[deprecated getElem_replicate (since := "2025-03-18")]
-abbrev getElem_mkArray := @getElem_replicate
-
 @[grind =] theorem getElem?_replicate {n : Nat} {v : α} {i : Nat} :
     (replicate n v)[i]? = if i < n then some v else none := by
   simp [getElem?_def]
 
-@[deprecated getElem?_replicate (since := "2025-03-18")]
-abbrev getElem?_mkArray := @getElem?_replicate
-
 /-! ### mem -/
 
 @[grind ←]
@@ -842,6 +809,11 @@ theorem contains_eq_true_of_mem [BEq α] [ReflBEq α] {a : α} {as : Array α} (
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     elem a xs = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
 
+@[grind =]
+theorem contains_iff_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
+    xs.contains a = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
+
+@[deprecated contains_iff_mem (since := "2025-10-26")]
 theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     xs.contains a = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
 
@@ -1081,12 +1053,6 @@ theorem mem_or_eq_of_mem_setIfInBounds
   cases xs
   simp
 
-@[deprecated beq_empty_eq (since := "2025-04-04")]
-abbrev beq_empty_iff := @beq_empty_eq
-
-@[deprecated empty_beq_eq (since := "2025-04-04")]
-abbrev empty_beq_iff := @empty_beq_eq
-
 @[simp, grind =] theorem push_beq_push [BEq α] {a b : α} {xs ys : Array α} :
     (xs.push a == ys.push b) = (xs == ys && a == b) := by
   cases xs
@@ -1107,9 +1073,6 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
     rw [Bool.eq_iff_iff]
     simp +contextual
 
-@[deprecated replicate_beq_replicate (since := "2025-03-18")]
-abbrev mkArray_beq_mkArray := @replicate_beq_replicate
-
 private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == b := by
   intro h
   have : isEqv #[a] #[b] BEq.beq = true := h
@@ -1173,7 +1136,7 @@ where
   aux (i bs) :
       mapM.map f xs i bs = (xs.toList.drop i).foldlM (fun bs a => bs.push <$> f a) bs := by
     unfold mapM.map; split
-    · rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
+    · rw [← List.getElem_cons_drop ‹_›]
       simp only [aux (i + 1), map_eq_pure_bind, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
@@ -1725,9 +1688,6 @@ theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : ∀ x ∈
   cases xs
   simp
 
-@[deprecated filterMap_eq_empty_iff (since := "2025-04-04")]
-abbrev filterMap_eq_nil_iff := @filterMap_eq_empty_iff
-
 theorem filterMap_eq_push_iff {f : α → Option β} {xs : Array α} {ys : Array β} {b : β} :
     filterMap f xs = ys.push b ↔ ∃ as a bs,
       xs = as.push a ++ bs ∧ filterMap f as = ys ∧ f a = some b ∧ (∀ x, x ∈ bs → f x = none) := by
@@ -1890,6 +1850,9 @@ theorem getElem_of_append {xs ys zs : Array α} (eq : xs = ys.push a ++ zs) (h :
 
 theorem push_eq_append {a : α} {as : Array α} : as.push a = as ++ #[a] := rfl
 
+@[deprecated push_eq_append (since := "2025-10-26")]
+theorem push_eq_append_singleton {as : Array α} {x : α} : as.push x = as ++ #[x] := rfl
+
 theorem append_inj {xs₁ xs₂ ys₁ ys₂ : Array α} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) :
     xs₁ = xs₂ ∧ ys₁ = ys₂ := by
   rcases xs₁ with ⟨s₁⟩
@@ -2090,11 +2053,22 @@ theorem append_eq_map_iff {f : α → β} :
   | nil => simp
   | cons as => induction as.toList <;> simp [*]
 
-@[simp] theorem flatten_toArray_map {L : List (List α)} :
+@[simp] theorem flatten_toArray_map_toArray {L : List (List α)} :
     (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
   apply ext'
   simp [Function.comp_def]
 
+@[deprecated flatten_toArray_map_toArray (since := "2025-10-26")]
+theorem flatten_toArray_map {L : List (List α)} :
+    (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
+  simp
+
+@[grind =]
+theorem flatten_map_toArray_toArray {L : List (List α)} :
+    (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
+  simp
+
+@[deprecated flatten_map_toArray_toArray (since := "2025-10-26")]
 theorem flatten_map_toArray {L : List (List α)} :
     (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   simp
@@ -2141,32 +2115,33 @@ theorem forall_mem_flatten {p : α → Prop} {xss : Array (Array α)} :
 
 theorem flatten_eq_flatMap {xss : Array (Array α)} : flatten xss = xss.flatMap id := by
   induction xss using array₂_induction
-  rw [flatten_toArray_map, List.flatten_eq_flatMap]
+  rw [flatten_toArray_map_toArray, List.flatten_eq_flatMap]
   simp [List.flatMap_map]
 
 @[simp, grind _=_] theorem map_flatten {f : α → β} {xss : Array (Array α)} :
     (flatten xss).map f = (map (map f) xss).flatten := by
   induction xss using array₂_induction with
   | of xss =>
-    simp only [flatten_toArray_map, List.map_toArray, List.map_flatten, List.map_map,
+    simp only [flatten_toArray_map_toArray, List.map_toArray, List.map_flatten, List.map_map,
       Function.comp_def]
-    rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+    rw [← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
 
 @[simp, grind =] theorem filterMap_flatten {f : α → Option β} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) :
     filterMap f (flatten xss) 0 stop = flatten (map (filterMap f) xss) := by
   subst w
   induction xss using array₂_induction
-  simp only [flatten_toArray_map, List.size_toArray, List.length_flatten, List.filterMap_toArray',
-    List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def]
-  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+  simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
+    List.filterMap_toArray', List.filterMap_flatten, List.map_toArray, List.map_map,
+    Function.comp_def]
+  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
 
 @[simp, grind =] theorem filter_flatten {p : α → Bool} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) :
     filter p (flatten xss) 0 stop = flatten (map (filter p) xss) := by
   subst w
   induction xss using array₂_induction
-  simp only [flatten_toArray_map, List.size_toArray, List.length_flatten, List.filter_toArray',
-    List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]
-  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+  simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
+    List.filter_toArray', List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]
+  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
 
 theorem flatten_filter_not_isEmpty {xss : Array (Array α)} :
     flatten (xss.filter fun xs => !xs.isEmpty) = xss.flatten := by
@@ -2189,23 +2164,23 @@ theorem flatten_filter_ne_empty [DecidablePred fun xs : Array α => xs ≠ #[]]
   induction xss using array₂_induction
   rcases xs with ⟨l⟩
   have this : [l.toArray] = [l].map List.toArray := by simp
-  simp only [List.push_toArray, flatten_toArray_map, List.append_toArray]
-  rw [this, ← List.map_append, flatten_toArray_map]
+  simp only [List.push_toArray, flatten_toArray_map_toArray, List.append_toArray]
+  rw [this, ← List.map_append, flatten_toArray_map_toArray]
   simp
 
 theorem flatten_flatten {xss : Array (Array (Array α))} : flatten (flatten xss) = flatten (map flatten xss) := by
   induction xss using array₃_induction with
   | of xss =>
-    rw [flatten_toArray_map]
+    rw [flatten_toArray_map_toArray]
     have : (xss.map (fun xs => xs.map List.toArray)).flatten = xss.flatten.map List.toArray := by
       induction xss with
       | nil => simp
       | cons xs xss ih =>
         simp only [List.map_cons, List.flatten_cons, ih, List.map_append]
-    rw [this, flatten_toArray_map, List.flatten_flatten, ← List.map_toArray, Array.map_map,
+    rw [this, flatten_toArray_map_toArray, List.flatten_flatten, ← List.map_toArray, Array.map_map,
       ← List.map_toArray, map_map, Function.comp_def]
-    simp only [Function.comp_apply, flatten_toArray_map]
-    rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map]
+    simp only [Function.comp_apply, flatten_toArray_map_toArray]
+    rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
 
 theorem flatten_eq_push_iff {xss : Array (Array α)} {ys : Array α} {y : α} :
     xss.flatten = ys.push y ↔
@@ -2214,13 +2189,13 @@ theorem flatten_eq_push_iff {xss : Array (Array α)} {ys : Array α} {y : α} :
   induction xss using array₂_induction with
   | of xs =>
     rcases ys with ⟨ys⟩
-    rw [flatten_toArray_map, List.push_toArray, mk.injEq, List.flatten_eq_append_iff]
+    rw [flatten_toArray_map_toArray, List.push_toArray, mk.injEq, List.flatten_eq_append_iff]
     constructor
     · rintro (⟨as, bs, rfl, rfl, h⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, h⟩)
       · rw [List.singleton_eq_flatten_iff] at h
         obtain ⟨xs, ys, rfl, h₁, h₂⟩ := h
         exact ⟨((as ++ xs).map List.toArray).toArray, #[], (ys.map List.toArray).toArray, by simp,
-          by simpa using h₂, by rw [flatten_toArray_map]; simpa⟩
+          by simpa using h₂, by rw [flatten_toArray_map_toArray]; simpa⟩
       · rw [List.singleton_eq_append_iff] at h
         obtain (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) := h
         · simp at h₁
@@ -2265,18 +2240,12 @@ theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} :
       rw [List.map_inj_right]
       simp +contextual
 
-theorem flatten_toArray_map_toArray {xss : List (List α)} :
-    (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
-  simp
-
 /-! ### flatMap -/
 
 theorem flatMap_def {xs : Array α} {f : α → Array β} : xs.flatMap f = flatten (map f xs) := by
   rcases xs with ⟨l⟩
   simp [flatten_toArray, Function.comp_def, List.flatMap_def]
 
-@[simp, grind =] theorem flatMap_empty {β} {f : α → Array β} : (#[] : Array α).flatMap f = #[] := rfl
-
 theorem flatMap_toList {xs : Array α} {f : α → List β} :
     xs.toList.flatMap f = (xs.flatMap (fun a => (f a).toArray)).toList := by
   rcases xs with ⟨l⟩
@@ -2287,6 +2256,7 @@ theorem flatMap_toList {xs : Array α} {f : α → List β} :
   rcases xs with ⟨l⟩
   simp
 
+@[deprecated List.flatMap_toArray_cons (since := "2025-10-29")]
 theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α} :
     (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
   simp [flatMap]
@@ -2297,6 +2267,7 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α}
   intro cs
   induction as generalizing cs <;> simp_all
 
+@[deprecated List.flatMap_toArray (since := "2025-10-29")]
 theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
     as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
   simp
@@ -2397,77 +2368,44 @@ theorem flatMap_eq_foldl {f : α → Array β} {xs : Array α} :
 
 @[simp] theorem replicate_one : replicate 1 a = #[a] := rfl
 
-@[deprecated replicate_one (since := "2025-03-18")]
-abbrev mkArray_one := @replicate_one
-
 /-- Variant of `replicate_succ` that prepends `a` at the beginning of the array. -/
 theorem replicate_succ' : replicate (n + 1) a = #[a] ++ replicate n a := by
   apply Array.ext'
   simp [List.replicate_succ]
 
-@[deprecated replicate_succ' (since := "2025-03-18")]
-abbrev mkArray_succ' := @replicate_succ'
-
 @[simp, grind =] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
   unfold replicate
   simp only [List.mem_toArray, List.mem_replicate]
 
-@[deprecated mem_replicate (since := "2025-03-18")]
-abbrev mem_mkArray := @mem_replicate
-
 @[grind →] theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
-@[deprecated eq_of_mem_mkArray (since := "2025-03-18")]
-abbrev eq_of_mem_mkArray := @eq_of_mem_replicate
-
 theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
     (∀ b, b ∈ replicate n a → p b) ↔ n = 0 ∨ p a := by
   cases n <;> simp [mem_replicate]
 
-@[deprecated forall_mem_replicate (since := "2025-03-18")]
-abbrev forall_mem_mkArray := @forall_mem_replicate
-
 @[simp] theorem replicate_succ_ne_empty {n : Nat} {a : α} : replicate (n+1) a ≠ #[] := by
   simp [replicate_succ]
 
-@[deprecated replicate_succ_ne_empty (since := "2025-03-18")]
-abbrev mkArray_succ_ne_empty := @replicate_succ_ne_empty
-
 @[simp] theorem replicate_eq_empty_iff {n : Nat} {a : α} : replicate n a = #[] ↔ n = 0 := by
   cases n <;> simp
 
-@[deprecated replicate_eq_empty_iff (since := "2025-03-18")]
-abbrev mkArray_eq_empty_iff := @replicate_eq_empty_iff
-
 @[simp] theorem replicate_inj : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
   rw [← toList_inj]
   simp
 
-@[deprecated replicate_inj (since := "2025-03-18")]
-abbrev mkArray_inj := @replicate_inj
-
 theorem eq_replicate_of_mem {a : α} {xs : Array α} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = replicate xs.size a := by
   rw [← toList_inj]
   simpa using List.eq_replicate_of_mem (by simpa using h)
 
-@[deprecated eq_replicate_of_mem (since := "2025-03-18")]
-abbrev eq_mkArray_of_mem := @eq_replicate_of_mem
-
 theorem eq_replicate_iff {a : α} {n} {xs : Array α} :
     xs = replicate n a ↔ xs.size = n ∧ ∀ (b) (_ : b ∈ xs), b = a := by
   rw [← toList_inj]
   simpa using List.eq_replicate_iff (l := xs.toList)
 
-@[deprecated eq_replicate_iff (since := "2025-03-18")]
-abbrev eq_mkArray_iff := @eq_replicate_iff
-
 theorem map_eq_replicate_iff {xs : Array α} {f : α → β} {b : β} :
     xs.map f = replicate xs.size b ↔ ∀ x ∈ xs, f x = b := by
   simp [eq_replicate_iff]
 
-@[deprecated map_eq_replicate_iff (since := "2025-03-18")]
-abbrev map_eq_mkArray_iff := @map_eq_replicate_iff
-
 @[simp] theorem map_const {xs : Array α} {b : β} : map (Function.const α b) xs = replicate xs.size b :=
   map_eq_replicate_iff.mpr fun _ _ => rfl
 
@@ -2484,143 +2422,86 @@ theorem map_const' {xs : Array α} {b : β} : map (fun _ => b) xs = replicate xs
   apply Array.ext'
   simp
 
-@[deprecated set_replicate_self (since := "2025-03-18")]
-abbrev set_mkArray_self := @set_replicate_self
-
 @[simp] theorem setIfInBounds_replicate_self : (replicate n a).setIfInBounds i a = replicate n a := by
   apply Array.ext'
   simp
 
-@[deprecated setIfInBounds_replicate_self (since := "2025-03-18")]
-abbrev setIfInBounds_mkArray_self := @setIfInBounds_replicate_self
-
 @[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   apply Array.ext'
   simp
 
-@[deprecated replicate_append_replicate (since := "2025-03-18")]
-abbrev mkArray_append_mkArray := @replicate_append_replicate
-
 theorem append_eq_replicate_iff {xs ys : Array α} {a : α} :
     xs ++ ys = replicate n a ↔
       xs.size + ys.size = n ∧ xs = replicate xs.size a ∧ ys = replicate ys.size a := by
   simp [← toList_inj, List.append_eq_replicate_iff]
 
-@[deprecated append_eq_replicate_iff (since := "2025-03-18")]
-abbrev append_eq_mkArray_iff := @append_eq_replicate_iff
-
 theorem replicate_eq_append_iff {xs ys : Array α} {a : α} :
     replicate n a = xs ++ ys ↔
       xs.size + ys.size = n ∧ xs = replicate xs.size a ∧ ys = replicate ys.size a := by
   rw [eq_comm, append_eq_replicate_iff]
 
-@[deprecated replicate_eq_append_iff (since := "2025-03-18")]
-abbrev replicate_eq_mkArray_iff := @replicate_eq_append_iff
-
 @[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
   apply Array.ext'
   simp
 
-@[deprecated map_replicate (since := "2025-03-18")]
-abbrev map_mkArray := @map_replicate
-
 @[grind =] theorem filter_replicate (w : stop = n) :
     (replicate n a).filter p 0 stop = if p a then replicate n a else #[] := by
   apply Array.ext'
   simp only [w]
   split <;> simp_all
 
-@[deprecated filter_replicate (since := "2025-03-18")]
-abbrev filter_mkArray := @filter_replicate
-
 @[simp] theorem filter_replicate_of_pos (w : stop = n) (h : p a) :
     (replicate n a).filter p 0 stop = replicate n a := by
   simp [filter_replicate, h, w]
 
-@[deprecated filter_replicate_of_pos (since := "2025-03-18")]
-abbrev filter_mkArray_of_pos := @filter_replicate_of_pos
-
 @[simp] theorem filter_replicate_of_neg (w : stop = n) (h : ¬ p a) :
     (replicate n a).filter p 0 stop = #[] := by
   simp [filter_replicate, h, w]
 
-@[deprecated filter_replicate_of_neg (since := "2025-03-18")]
-abbrev filter_mkArray_of_neg := @filter_replicate_of_neg
-
 theorem filterMap_replicate {f : α → Option β} (w : stop = n := by simp) :
     (replicate n a).filterMap f 0 stop = match f a with | none => #[] | .some b => replicate n b := by
   apply Array.ext'
   simp only [w, size_replicate, toList_filterMap', toList_replicate, List.filterMap_replicate]
   split <;> simp_all
 
-@[deprecated filterMap_replicate (since := "2025-03-18")]
-abbrev filterMap_mkArray := @filterMap_replicate
-
 -- This is not a useful `simp` lemma because `b` is unknown.
 theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
     (replicate n a).filterMap f = replicate n b := by
   simp [filterMap_replicate, h]
 
-@[deprecated filterMap_replicate_of_some (since := "2025-03-18")]
-abbrev filterMap_mkArray_of_some := @filterMap_replicate_of_some
-
 @[simp] theorem filterMap_replicate_of_isSome {f : α → Option β} (h : (f a).isSome) :
     (replicate n a).filterMap f = replicate n (Option.get _ h) := by
   match w : f a, h with
   | some b, _ => simp [filterMap_replicate, w]
 
-@[deprecated filterMap_replicate_of_isSome (since := "2025-03-18")]
-abbrev filterMap_mkArray_of_isSome := @filterMap_replicate_of_isSome
-
 @[simp] theorem filterMap_replicate_of_none {f : α → Option β} (h : f a = none) :
     (replicate n a).filterMap f = #[] := by
   simp [filterMap_replicate, h]
 
-@[deprecated filterMap_replicate_of_none (since := "2025-03-18")]
-abbrev filterMap_mkArray_of_none := @filterMap_replicate_of_none
-
 @[simp] theorem flatten_replicate_empty : (replicate n (#[] : Array α)).flatten = #[] := by
   rw [← toList_inj]
   simp
 
-@[deprecated flatten_replicate_empty (since := "2025-03-18")]
-abbrev flatten_mkArray_empty := @flatten_replicate_empty
-
 @[simp] theorem flatten_replicate_singleton : (replicate n #[a]).flatten = replicate n a := by
   rw [← toList_inj]
   simp
 
-@[deprecated flatten_replicate_singleton (since := "2025-03-18")]
-abbrev flatten_mkArray_singleton := @flatten_replicate_singleton
-
 @[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
   rw [← toList_inj]
   simp
 
-@[deprecated flatten_replicate_replicate (since := "2025-03-18")]
-abbrev flatten_mkArray_replicate := @flatten_replicate_replicate
-
 theorem flatMap_replicate {f : α → Array β} : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
   rw [← toList_inj]
   simp [List.flatMap_replicate]
 
-@[deprecated flatMap_replicate (since := "2025-03-18")]
-abbrev flatMap_mkArray := @flatMap_replicate
-
 @[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
-@[deprecated isEmpty_replicate (since := "2025-03-18")]
-abbrev isEmpty_mkArray := @isEmpty_replicate
-
 @[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
   rw [← List.toArray_replicate, List.sum_toArray]
   simp
 
-@[deprecated sum_replicate_nat (since := "2025-03-18")]
-abbrev sum_mkArray_nat := @sum_replicate_nat
-
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
 @[grind =]
@@ -2662,8 +2543,8 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i
         split <;> rename_i h₃
         · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
           exact (List.getElem?_reverse' (Eq.trans (by simp +arith) h)).symm
-        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
-          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
+        simp only [Nat.succ_le_iff, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
+          Nat.lt_succ_iff.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
     · rw [H]; split <;> rename_i h₂
       · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
         cases Nat.le_antisymm h₂.1 h₂.2
@@ -2678,7 +2559,7 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i
     split
     · rfl
     · rename_i h
-      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := xs.size - 1), this, Nat.zero_le,
+      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ_iff (n := xs.size - 1), this, Nat.zero_le,
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (xs.toList.length_reverse ▸ ‹_›)]
 
@@ -2807,9 +2688,6 @@ theorem flatten_reverse {xss : Array (Array α)} :
   rw [← toList_inj]
   simp
 
-@[deprecated reverse_replicate (since := "2025-03-18")]
-abbrev reverse_mkArray := @reverse_replicate
-
 /-! ### extract -/
 
 theorem extract_loop_zero {xs ys : Array α} {start : Nat} : extract.loop xs 0 start ys = ys := by
@@ -2829,8 +2707,8 @@ theorem extract_loop_eq_aux {xs ys : Array α} {size start : Nat} :
   | zero => rw [extract_loop_zero, extract_loop_zero, append_empty]
   | succ size ih =>
     if h : start < xs.size then
-      rw [extract_loop_succ (h := h), ih, push_eq_append_singleton]
-      rw [extract_loop_succ (h := h), ih (ys := #[].push _), push_eq_append_singleton, empty_append]
+      rw [extract_loop_succ (h := h), ih, push_eq_append]
+      rw [extract_loop_succ (h := h), ih (ys := #[].push _), push_eq_append, empty_append]
       rw [append_assoc]
     else
       rw [extract_loop_of_ge (h := Nat.le_of_not_lt h)]
@@ -3719,15 +3597,9 @@ theorem back?_replicate {a : α} {n : Nat} :
   rw [replicate_eq_toArray_replicate]
   simp only [List.back?_toArray, List.getLast?_replicate]
 
-@[deprecated back?_replicate (since := "2025-03-18")]
-abbrev back?_mkArray := @back?_replicate
-
 @[simp] theorem back_replicate {xs : Array α} (w : 0 < n) : (replicate n xs).back (by simpa using w) = xs := by
   simp [back_eq_getElem]
 
-@[deprecated back_replicate (since := "2025-03-18")]
-abbrev back_mkArray := @back_replicate
-
 /-! ## Additional operations -/
 
 /-! ### leftpad -/
@@ -3745,9 +3617,6 @@ theorem size_rightpad {n : Nat} {a : α} {xs : Array α} :
 
 theorem elem_push_self [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.push a).elem a = true := by simp
 
-@[deprecated elem_push_self (since := "2025-04-04")]
-abbrev elem_cons_self := @elem_push_self
-
 theorem contains_eq_any_beq [BEq α] {xs : Array α} {a : α} : xs.contains a = xs.any (a == ·) := by
   rcases xs with ⟨xs⟩
   simp [List.contains_eq_any_beq]
@@ -3761,11 +3630,6 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
 -- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
 grind_pattern contains_iff_exists_mem_beq => xs.contains a
 
-@[grind _=_]
-theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
-    xs.contains a ↔ a ∈ xs := by
-  simp
-
 @[simp, grind =]
 theorem contains_toList [BEq α] {xs : Array α} {x : α} :
     xs.toList.contains x = xs.contains x := by
@@ -3825,9 +3689,6 @@ theorem pop_append {xs ys : Array α} :
 @[simp, grind =] theorem pop_replicate {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a := by
   ext <;> simp
 
-@[deprecated pop_replicate (since := "2025-03-18")]
-abbrev pop_mkArray := @pop_replicate
-
 /-! ## Logic -/
 
 /-! ### any / all -/
@@ -4057,16 +3918,10 @@ theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
     (replicate n a).any f = if n = 0 then false else f a := by
   induction n <;> simp_all [replicate_succ']
 
-@[deprecated any_replicate (since := "2025-03-18")]
-abbrev any_mkArray := @any_replicate
-
 @[simp] theorem all_replicate {n : Nat} {a : α} :
     (replicate n a).all f = if n = 0 then true else f a := by
   induction n <;> simp_all +contextual [replicate_succ']
 
-@[deprecated all_replicate (since := "2025-03-18")]
-abbrev all_mkArray := @all_replicate
-
 /-! ### modify -/
 
 @[simp, grind =] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
@@ -4241,17 +4096,11 @@ theorem replace_extract {xs : Array α} {i : Nat} :
     (replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
   cases n <;> simp_all [replicate_succ', replace_append]
 
-@[deprecated replace_replicate_self (since := "2025-03-18")]
-abbrev replace_mkArray_self := @replace_replicate_self
-
 @[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
     (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all
 
-@[deprecated replace_replicate_ne (since := "2025-03-18")]
-abbrev replace_mkArray_ne := @replace_replicate_ne
-
 end replace
 
 /-! ### toListRev -/
@@ -4419,9 +4268,6 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i
 @[deprecated mem_toList_iff (since := "2025-05-26")]
 theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
 
-@[deprecated not_mem_empty (since := "2025-03-25")]
-theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
-
 /-! # get lemmas -/
 
 theorem lt_of_getElem {x : α} {xs : Array α} {i : Nat} {hidx : i < xs.size} (_ : xs[i] = x) :
@@ -4433,6 +4279,7 @@ theorem getElem_fin_eq_getElem_toList {xs : Array α} {i : Fin xs.size} : xs[i]
 @[simp] theorem ugetElem_eq_getElem {xs : Array α} {i : USize} (h : i.toNat < xs.size) :
   xs[i] = xs[i.toNat] := rfl
 
+@[deprecated getElem?_eq_none (since := "2025-10-26")]
 theorem getElem?_size_le {xs : Array α} {i : Nat} (h : xs.size ≤ i) : xs[i]? = none := by
   simp [getElem?_neg, h]
 
@@ -4452,6 +4299,7 @@ theorem getElem?_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
     (xs.push x)[i]? = some xs[i] := by
   rw [getElem?_pos (xs.push x) i (size_push _ ▸ Nat.lt_succ_of_lt h), getElem_push_lt]
 
+@[deprecated getElem?_push_size (since := "2025-10-26")]
 theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some x := by
   rw [getElem?_pos (xs.push x) xs.size (size_push _ ▸ Nat.lt_succ_self xs.size), getElem_push_eq]
 
@@ -4470,12 +4318,6 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
   cases xs
   simp
 
-/-! ### contains -/
-
-@[deprecated contains_iff (since := "2025-04-07")]
-abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a ↔ a ∈ xs :=
-  contains_iff
-
 /-! ### isPrefixOf -/
 
 @[simp, grind =] theorem isPrefixOf_toList [BEq α] {xs ys : Array α} :
@@ -4589,7 +4431,8 @@ theorem uset_toArray {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray
   apply ext'
   simp
 
-@[simp, grind =] theorem flatten_toArray {L : List (List α)} :
+@[deprecated Array.flatten_map_toArray_toArray (since := "2025-10-26")]
+theorem flatten_toArray {L : List (List α)} :
     (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   apply ext'
   simp

src/Init/Data/Array/Lex.lean

@@ -8,5 +8,3 @@ 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,11 +6,8 @@ Author: Kim Morrison
 module
 
 prelude
-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
+public import Init.Data.Range.Polymorphic.Iterators
+public import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Iterators.Consumers
 
 public section
@@ -31,7 +28,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.PRange.lt_upper_of_mem h
+    have : i < min as.size bs.size := Std.Rco.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,9 +10,7 @@ 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
 
@@ -36,14 +34,24 @@ 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
-  rw [lex, Std.PRange.forIn'_eq_match]
-  simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+  simp [lex, Std.Rco.forIn'_eq_if]
 
 private theorem cons_lex_cons.forIn'_congr_aux [Monad m] {as bs : ρ} {_ : Membership α ρ}
     [ForIn' m ρ α inferInstance] (w : as = bs)
@@ -64,13 +72,13 @@ 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.PRange.forIn'_eq_forIn'_toList]
+    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
   conv =>
     lhs; congr; congr
-    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 Std.Rco.toList_eq_if rfl (fun _ _ _ => rfl)]
+    simp only [bind_pure_comp, map_pure]
     rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.PRange.toList_Rox_eq_toList_Rcx_of_isSome_succ? (lo := 0) (h := 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,
     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]
@@ -83,16 +91,10 @@ 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₂
-    · rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
-    · rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+    cases l₂ <;> simp [lex, Std.Rco.forIn'_eq_if]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil =>
-      rw [lex, Std.PRange.forIn'_eq_match]
-      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+    | nil => simp [lex, Std.Rco.forIn'_eq_if]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 
@@ -187,12 +189,6 @@ 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 :=

src/Init/Data/Array/MapIdx.lean

@@ -6,10 +6,7 @@ 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
@@ -299,9 +296,6 @@ 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⟩
@@ -441,9 +435,6 @@ 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,8 +6,6 @@ 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,13 +6,9 @@ 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
 

src/Init/Data/Array/OfFn.lean

@@ -6,11 +6,8 @@ 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,7 +7,6 @@ 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
 
@@ -85,9 +84,6 @@ 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⟩
@@ -108,7 +104,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_singleton]
+  rw [push_eq_append]
   exact p.append .rfl
 
 grind_pattern Perm.push => xs ~ ys, xs.push x

src/Init/Data/Array/QSort.lean

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

src/Init/Data/Array/Range.lean

@@ -6,14 +6,10 @@ 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
 

src/Init/Data/Array/Subarray.lean

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

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

@@ -7,7 +7,6 @@ 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,10 +6,8 @@ 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,10 +6,8 @@ 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
 
@@ -168,9 +166,6 @@ 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
@@ -296,9 +291,6 @@ 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
@@ -350,9 +342,6 @@ 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 =]
@@ -410,7 +399,4 @@ 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

@@ -1,20 +0,0 @@
-/-
-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,5 +13,3 @@ 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,11 +6,8 @@ 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
 
@@ -206,8 +203,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 := (Nat.toDigits 16 x.toNat).asString
-  let t := (List.replicate ((n+3) / 4 - String.Internal.length s) '0').asString
+  let s := String.ofList (Nat.toDigits 16 x.toNat)
+  let t := String.ofList (List.replicate ((n+3) / 4 - String.Internal.length s) '0')
   String.Internal.append t s
 
 /-- `BitVec` representation. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -6,17 +6,13 @@ 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
 
@@ -639,12 +635,11 @@ 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_eq_ofBool_getLsb_zero,
-        ofBool_true, ofNat_eq_ofNat]
+      simp only [hy, ↓reduceIte, setWidth_one, ofBool_true, ofNat_eq_ofNat]
       rw [setWidth_ofNat_one_eq_ofNat_one_of_lt (by omega)]
       simp
     case neg hy =>
-      simp [hy, setWidth_one_eq_ofBool_getLsb_zero]
+      simp [hy, setWidth_one]
   case succ s' hs =>
     rw [mulRec_succ_eq, hs]
     have heq :
@@ -1029,7 +1024,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_iff_le.mp rltd
+        BitVec.not_lt.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']
@@ -1037,7 +1032,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_iff_le.mp rltd)
+      have rltd' := (BitVec.not_lt.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]
@@ -1411,7 +1406,7 @@ theorem eq_iff_eq_of_inv (f : α → BitVec w) (g : BitVec w → α) (h : ∀ x,
     have := congrArg g h'
     simpa [h] using this
 
-@[simp]
+@[deprecated BitVec.ne_intMin_of_msb_eq_false (since := "2025-10-26")]
 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
@@ -1516,7 +1511,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_lt_of_msb_false (by omega)
+  <;> apply ne_intMin_of_msb_eq_false (by omega)
   <;> rw [msb_udiv]
   <;> try simp only [hx, Bool.false_and]
   · simp [h, ne_zero_of_msb_true, hx]
@@ -1628,7 +1623,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_lt_of_msb_false w ((-a) / b) wpos (by simp [ha, ha0, ha_intMin])
+            · have := @BitVec.ne_intMin_of_msb_eq_false w wpos ((-a) / b) (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]
@@ -1639,7 +1634,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_lt_of_msb_false (by omega) ha
+        apply ne_intMin_of_msb_eq_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]
@@ -1931,7 +1926,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_cast]
+      simp only [hdvd, ↓reduceIte, Int.natAbs_natCast]
 
 theorem srem_zero_of_dvd {x y : BitVec w} (h : y.toInt ∣ x.toInt) :
     x.srem y = 0#w := by

src/Init/Data/BitVec/Bootstrap.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 import Init.Data.Int.Bitwise.Lemmas
+import Init.Ext
 
 public section
 

src/Init/Data/BitVec/Decidable.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Init.Data.BitVec.Bootstrap
+import Init.Ext
 
 public section
 
@@ -49,11 +50,11 @@ instance instDecidableForallBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePre
 
 instance instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] :
     Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+  decidable_of_iff (¬ ∀ v, ¬ P v) (by exact Classical.not_forall_not)
 
 instance instDecidableExistsBitVecSucc (P : BitVec (n+1) → Prop) [DecidablePred P]
     [Decidable (∀ (x : Bool) (v : BitVec n), ¬ P (v.cons x))] : Decidable (∃ v, P v) :=
-  decidable_of_iff (¬ ∀ v, ¬ P v) Classical.not_forall_not
+  decidable_of_iff (¬ ∀ v, ¬ P v) (by exact Classical.not_forall_not)
 
 /--
 For small numerals this isn't necessary (as typeclass search can use the above two instances),

src/Init/Data/BitVec/Folds.lean

@@ -6,10 +6,8 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
-public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Lemmas
-public import Init.Data.Nat.Lemmas
 public import Init.Data.Fin.Iterate
 
 public section
@@ -84,7 +82,7 @@ theorem iunfoldr_getLsbD' {f : Fin w → α → α × Bool} (state : Nat → α)
       intro i
       simp only [getLsbD_cons]
       have hj2 : j.val ≤ w := by simp
-      cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
+      cases (Nat.lt_or_eq_of_le (Nat.lt_succ_iff.mp i.isLt)) with
       | inl h3 => simp [(Nat.ne_of_lt h3)]
                   exact (ih hj2).1 ⟨i.val, h3⟩
       | inr h3 => simp [h3]

src/Init/Data/BitVec/Lemmas.lean

@@ -6,22 +6,14 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B
 module
 
 prelude
-public import Init.Data.Bool
-public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
-public import Init.Data.BitVec.BasicAux
 import all Init.Data.BitVec.BasicAux
 public import Init.Data.Fin.Lemmas
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Nat.Div.Lemmas
-public import Init.Data.Nat.Mod
-public import Init.Data.Nat.Div.Lemmas
 public import Init.Data.Int.Bitwise.Lemmas
 public import Init.Data.Int.LemmasAux
-public import Init.Data.Int.Pow
-public import Init.Data.Int.LemmasAux
 public import Init.Data.BitVec.Bootstrap
-public import Init.Data.Order.Factories
+public import Init.Data.List.BasicAux
+import Init.Data.List.Lemmas
 
 public section
 
@@ -42,14 +34,6 @@ namespace BitVec
   simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
   omega
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_of_ge (since := "2025-04-04")]
-abbrev getLsbD_ge := @getLsbD_of_ge
-
-set_option linter.missingDocs false in
-@[deprecated getMsbD_of_ge (since := "2025-04-04")]
-abbrev getMsbD_ge := @getMsbD_of_ge
-
 theorem lt_of_getLsbD {x : BitVec w} {i : Nat} : getLsbD x i = true → i < w := by
   if h : i < w then
     simp [h]
@@ -80,6 +64,7 @@ theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
 theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by
   simp
 
+@[simp]
 theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
 theorem getElem?_eq (l : BitVec w) (i : Nat) :
@@ -148,9 +133,6 @@ theorem two_pow_le_toNat_of_getElem_eq_true {i : Nat} {x : BitVec w}
   rw [← getElem_eq_testBit_toNat x i hi]
   exact hx
 
-@[grind =] theorem msb_eq_getMsbD (x : BitVec w) : x.msb = x.getMsbD 0 := by
-  simp [BitVec.msb]
-
 @[grind =] theorem getMsb_eq_getLsb (x : BitVec w) (i : Fin w) :
     x.getMsb i = x.getLsb ⟨w - 1 - i, by omega⟩ := by
   simp only [getMsb, getLsb]
@@ -177,18 +159,13 @@ theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i <
     apply getLsbD_of_ge
     omega
 
-@[simp] theorem getElem?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by
+@[deprecated getElem?_eq_none (since := "2025-10-29")]
+theorem getElem?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none := by
   simp [ge]
 
 @[simp] theorem getMsb?_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getMsb? x i = none := by
   simp [getMsb?_eq_getLsb?]; omega
 
-set_option linter.missingDocs false in
-@[deprecated getElem?_of_ge (since := "2025-04-04")] abbrev getLsb?_ge := @getElem?_of_ge
-
-set_option linter.missingDocs false in
-@[deprecated getMsb?_of_ge (since := "2025-04-04")] abbrev getMsb?_ge := @getMsb?_of_ge
-
 theorem lt_of_getElem?_eq_some (x : BitVec w) (i : Nat) : x[i]? = some b → i < w := by
   cases h : x[i]? with
   | none => simp
@@ -211,18 +188,6 @@ theorem lt_of_isSome_getMsb? (x : BitVec w) (i : Nat) : (getMsb? x i).isSome →
   else
     simp [Nat.ge_of_not_lt h]
 
-set_option linter.missingDocs false in
-@[deprecated lt_of_getElem?_eq_some (since := "2025-04-04")]
-abbrev lt_of_getLsb?_eq_some := @lt_of_getElem?_eq_some
-
-set_option linter.missingDocs false in
-@[deprecated lt_of_isSome_getElem? (since := "2025-04-04")]
-abbrev lt_of_getLsb?_isSome := @lt_of_isSome_getElem?
-
-set_option linter.missingDocs false in
-@[deprecated lt_of_isSome_getMsb? (since := "2025-04-04")]
-abbrev lt_of_getMsb?_isSome := @lt_of_isSome_getMsb?
-
 theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
     x.getMsbD i = (x.getMsb? i).getD false := by
   rw [getMsbD_eq_getLsbD]
@@ -452,12 +417,18 @@ theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
 
 -- This does not need to be a `@[simp]` theorem as it is already handled by `getElem?_eq_getElem`.
 theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
-  simp only [ofBool, ofNat_eq_ofNat, cond_eq_if]
+  simp only [ofBool, ofNat_eq_ofNat, cond_eq_ite]
   split <;> simp_all
 
-@[simp, grind =] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
+@[simp, grind =]
+theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by
   rw [getElem_eq_iff, getElem?_zero_ofBool]
 
+
+@[deprecated getElem_ofBool_zero (since := "2025-10-29")]
+theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
+  simp
+
 theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none := by
   simp
 
@@ -468,8 +439,6 @@ theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) &&
   · simp only [ofBool, ofNat_eq_ofNat, cond_true, getLsbD_ofNat, Bool.and_true]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
-theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by simp
-
 @[simp]
 theorem getElem_ofBool {b : Bool} {h : i < 1}: (ofBool b)[i] = b := by
   simp [← getLsbD_eq_getElem]
@@ -552,6 +521,10 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
 @[grind _=_] theorem msb_eq_getMsbD_zero (x : BitVec w) : x.msb = x.getMsbD 0 := by
   cases w <;> simp [getMsbD_eq_getLsbD, msb_eq_getLsbD_last]
 
+@[deprecated msb_eq_getMsbD_zero (since := "2025-10-26")]
+theorem msb_eq_getMsbD (x : BitVec w) : x.msb = x.getMsbD 0 := by
+  simp [BitVec.msb]
+
 /-! ### cast -/
 
 @[simp, grind =] theorem toFin_cast (h : w = v) (x : BitVec w) :
@@ -613,7 +586,7 @@ theorem toInt_eq_toNat_bmod (x : BitVec n) : x.toInt = Int.bmod x.toNat (2^n) :=
   simp only [toInt_eq_toNat_cond]
   split
   next g =>
-    rw [Int.bmod_pos] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_eq_emod_of_lt] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
     omega
   next g =>
     rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
@@ -1021,7 +994,14 @@ theorem msb_setWidth' (x : BitVec w) (h : w ≤ v) : (x.setWidth' h).msb = (deci
 theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k := by
   simp [BitVec.msb, getMsbD]
 
+/-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
+theorem setWidth_one {x : BitVec w} :
+    x.setWidth 1 = ofBool (x.getLsbD 0) := by
+  ext i
+  simp [show i = 0 by omega]
+
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
+@[deprecated setWidth_one (since := "2025-10-29")]
 theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
     x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by
   ext i h
@@ -1037,12 +1017,6 @@ theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
   have hv := (@Nat.testBit_one_eq_true_iff_self_eq_zero i)
   by_cases h : Nat.testBit 1 i = true <;> simp_all
 
-/-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
-theorem setWidth_one {x : BitVec w} :
-    x.setWidth 1 = ofBool (x.getLsbD 0) := by
-  ext i
-  simp [show i = 0 by omega]
-
 @[simp, grind =] theorem setWidth_ofNat_of_le (h : v ≤ w) (x : Nat) : setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_setWidth, toNat_ofNat]
@@ -1216,7 +1190,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
 
 @[simp] theorem getLsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
-  simp [getLsbD, Nat.lt_succ]
+  simp [getLsbD, Nat.lt_succ_iff]
 
 @[simp] theorem getLsbD_extractLsb {hi lo : Nat} {x : BitVec n} {i : Nat} :
     (extractLsb hi lo x).getLsbD i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i)) := by
@@ -1672,11 +1646,11 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
 
 @[simp] theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} :
     BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by
-  simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLT, toNat_not,
+  simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_natCast, toNat_eq, toNat_ofNatLT, toNat_not,
     toNat_ofNat]
   cases h : Int.negSucc n % ((2 ^ w : Nat) : Int)
   case ofNat =>
-    rw [Int.ofNat_eq_coe, Int.negSucc_emod] at h
+    rw [Int.ofNat_eq_natCast, Int.negSucc_emod] at h
     · dsimp only
       omega
     · omega
@@ -1758,9 +1732,6 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
     rw [h]
     simp
 
-set_option linter.missingDocs false in
-@[deprecated getMsbD_not (since := "2025-04-04")] abbrev getMsb_not := @getMsbD_not
-
 @[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by
   simp [BitVec.msb]
 
@@ -2580,10 +2551,6 @@ theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
   ext i h
   simp [getElem_signExtend, show i < w by omega]
 
-@[deprecated signExtend_eq_setWidth_of_le (since := "2025-03-07")]
-theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w) :
-  x.signExtend v = x.setWidth v := signExtend_eq_setWidth_of_le x hv
-
 /-- Sign extending to the same bitwidth is a no op. -/
 @[simp] theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
   rw [signExtend_eq_setWidth_of_le _ (Nat.le_refl _), setWidth_eq]
@@ -3643,9 +3610,6 @@ theorem sub_eq_add_neg {n} (x y : BitVec n) : x - y = x + - y := by
   simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod]
   rw [Nat.add_comm]
 
-set_option linter.missingDocs false in
-@[deprecated sub_eq_add_neg (since := "2025-04-04")] abbrev sub_toAdd := @sub_eq_add_neg
-
 theorem add_left_neg (x : BitVec w) : -x + x = 0#w := by
   apply toInt_inj.mp
   simp [toInt_neg, Int.add_left_neg]
@@ -3685,10 +3649,6 @@ theorem neg_one_eq_allOnes : -1#w = allOnes w := by
     have r : (2^w - 1) < 2^w := by omega
     simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
 
-set_option linter.missingDocs false in
-@[deprecated neg_one_eq_allOnes (since := "2025-04-04")]
-abbrev negOne_eq_allOnes := @neg_one_eq_allOnes
-
 theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1#w := by
   apply eq_of_toNat_eq
   simp only [toNat_neg, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
@@ -3750,6 +3710,9 @@ theorem neg_add {x y : BitVec w} : - (x + y) = - x - y := by
   apply eq_of_toInt_eq
   simp [toInt_neg, toInt_add, Int.neg_add, Int.add_neg_eq_sub]
 
+theorem sub_sub (a b c : BitVec n) : a - b - c = a - (b + c) := by
+  simp [BitVec.sub_eq_add_neg, BitVec.add_assoc, BitVec.neg_add]
+
 theorem add_neg_eq_sub {x y : BitVec w} : x + - y = (x - y) := by
   apply eq_of_toInt_eq
   simp [toInt_neg, Int.sub_eq_add_neg]
@@ -4102,6 +4065,7 @@ protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y :=
   simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod]
   apply Nat.mod_lt
 
+@[deprecated BitVec.not_lt (since := "2025-10-26")]
 theorem not_lt_iff_le {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by
   constructor <;>
     (intro h; simp only [lt_def, Nat.not_lt, le_def] at h ⊢; omega)
@@ -4118,7 +4082,7 @@ theorem not_lt_zero {x : BitVec w} : ¬x < 0#w := of_decide_eq_false rfl
 theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w := by
   constructor
   · intro h
-    have : x ≥ 0 := not_lt_iff_le.mp not_lt_zero
+    have : x ≥ 0 := BitVec.not_lt.mp not_lt_zero
     exact Eq.symm (BitVec.le_antisymm this h)
   · simp_all
 
@@ -4141,7 +4105,7 @@ theorem not_allOnes_lt {x : BitVec w} : ¬allOnes w < x := by
 theorem allOnes_le_iff {x : BitVec w} : allOnes w ≤ x ↔ x = allOnes w := by
   constructor
   · intro h
-    have : x ≤ allOnes w := not_lt_iff_le.mp not_allOnes_lt
+    have : x ≤ allOnes w := BitVec.not_lt.mp not_allOnes_lt
     exact Eq.symm (BitVec.le_antisymm h this)
   · simp_all
 
@@ -4687,9 +4651,6 @@ theorem zero_smod {x : BitVec w} : (0#w).smod x = 0#w := by
 @[simp, grind =] theorem getLsbD_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false := by
   induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_ofBoolListLE (since := "2025-04-04")] abbrev getLsb_ofBoolListLE := @getLsbD_ofBoolListLE
-
 @[simp, grind =] theorem getMsbD_ofBoolListLE :
     (ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
   simp [getMsbD_eq_getLsbD]
@@ -4760,14 +4721,6 @@ theorem getLsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i
   apply getLsbD_of_ge
   omega
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_rotateLeftAux_of_lt (since := "2025-04-04")]
-abbrev getLsbD_rotateLeftAux_of_le := @getLsbD_rotateLeftAux_of_lt
-
-set_option linter.missingDocs false in
-@[deprecated getLsbD_rotateLeftAux_of_ge (since := "2025-04-04")]
-abbrev getLsbD_rotateLeftAux_of_geq := @getLsbD_rotateLeftAux_of_ge
-
 /-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
 theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateLeft r).getLsbD i =
@@ -4924,14 +4877,6 @@ theorem getLsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i
   apply getLsbD_of_ge
   omega
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_rotateRightAux_of_lt (since := "2025-04-04")]
-abbrev getLsbD_rotateRightAux_of_le := @getLsbD_rotateRightAux_of_lt
-
-set_option linter.missingDocs false in
-@[deprecated getLsbD_rotateRightAux_of_ge (since := "2025-04-04")]
-abbrev getLsbD_rotateRightAux_of_geq := @getLsbD_rotateRightAux_of_ge
-
 /-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
 smaller than the bitwidth. -/
 theorem rotateRight_eq_rotateRightAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :

src/Init/Data/Bool.lean

@@ -111,35 +111,11 @@ Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` v
 @[simp] theorem eq_self_and : ∀ {a b : Bool}, (a = (a && b)) ↔ (a → b) := by decide
 @[simp] theorem eq_and_self : ∀ {a b : Bool}, (b = (a && b)) ↔ (b → a) := by decide
 
-@[deprecated and_eq_left_iff_imp (since := "2025-04-04")]
-abbrev and_iff_left_iff_imp := @and_eq_left_iff_imp
-
-@[deprecated and_eq_right_iff_imp (since := "2025-04-04")]
-abbrev and_iff_right_iff_imp := @and_eq_right_iff_imp
-
-@[deprecated eq_self_and (since := "2025-04-04")]
-abbrev iff_self_and := @eq_self_and
-
-@[deprecated eq_and_self (since := "2025-04-04")]
-abbrev iff_and_self := @eq_and_self
-
 @[simp] theorem not_and_eq_left_iff_and  : ∀ {a b : Bool}, ((!a && b) = a) ↔ !a ∧ !b := by decide
 @[simp] theorem and_not_eq_right_iff_and : ∀ {a b : Bool}, ((a && !b) = b) ↔ !a ∧ !b := by decide
 @[simp] theorem eq_not_self_and : ∀ {a b : Bool}, (a = (!a && b)) ↔ !a ∧ !b := by decide
 @[simp] theorem eq_and_not_self : ∀ {a b : Bool}, (b = (a && !b)) ↔ !a ∧ !b := by decide
 
-@[deprecated not_and_eq_left_iff_and (since := "2025-04-04")]
-abbrev not_and_iff_left_iff_imp := @not_and_eq_left_iff_and
-
-@[deprecated and_not_eq_right_iff_and (since := "2025-04-04")]
-abbrev and_not_iff_right_iff_imp := @and_not_eq_right_iff_and
-
-@[deprecated eq_not_self_and (since := "2025-04-04")]
-abbrev iff_not_self_and := @eq_not_self_and
-
-@[deprecated eq_and_not_self (since := "2025-04-04")]
-abbrev iff_and_not_self := @eq_and_not_self
-
 /-! ### or -/
 
 @[simp] theorem or_self_left  : ∀ (a b : Bool), (a || (a || b)) = (a || b) := by decide
@@ -169,35 +145,11 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
 @[simp] theorem eq_self_or : ∀ {a b : Bool}, (a = (a || b)) ↔ (b → a) := by decide
 @[simp] theorem eq_or_self : ∀ {a b : Bool}, (b = (a || b)) ↔ (a → b) := by decide
 
-@[deprecated or_eq_left_iff_imp (since := "2025-04-04")]
-abbrev or_iff_left_iff_imp := @or_eq_left_iff_imp
-
-@[deprecated or_eq_right_iff_imp (since := "2025-04-04")]
-abbrev or_iff_right_iff_imp := @or_eq_right_iff_imp
-
-@[deprecated eq_self_or (since := "2025-04-04")]
-abbrev iff_self_or := @eq_self_or
-
-@[deprecated eq_or_self (since := "2025-04-04")]
-abbrev iff_or_self := @eq_or_self
-
 @[simp] theorem not_or_eq_left_iff_and  : ∀ {a b : Bool}, ((!a || b) = a) ↔ a ∧ b := by decide
 @[simp] theorem or_not_eq_right_iff_and : ∀ {a b : Bool}, ((a || !b) = b) ↔ a ∧ b := by decide
 @[simp] theorem eq_not_self_or : ∀ {a b : Bool}, (a = (!a || b)) ↔ a ∧ b := by decide
 @[simp] theorem eq_or_not_self : ∀ {a b : Bool}, (b = (a || !b)) ↔ a ∧ b := by decide
 
-@[deprecated not_or_eq_left_iff_and (since := "2025-04-04")]
-abbrev not_or_iff_left_iff_imp := @not_or_eq_left_iff_and
-
-@[deprecated or_not_eq_right_iff_and (since := "2025-04-04")]
-abbrev or_not_iff_right_iff_imp := @or_not_eq_right_iff_and
-
-@[deprecated eq_not_self_or (since := "2025-04-04")]
-abbrev iff_not_self_or := @eq_not_self_or
-
-@[deprecated eq_or_not_self (since := "2025-04-04")]
-abbrev iff_or_not_self := @eq_or_not_self
-
 theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
 instance : Std.Commutative (· || ·) := ⟨or_comm⟩
 
@@ -562,6 +514,7 @@ theorem exists_bool {p : Bool → Prop} : (∃ b, p b) ↔ p false ∨ p true :=
 theorem cond_eq_ite {α} (b : Bool) (t e : α) : cond b t e = if b then t else e := by
   cases b <;> simp
 
+@[deprecated cond_eq_ite (since := "2025-10-29")]
 theorem cond_eq_if : (bif b then x else y) = (if b then x else y) := cond_eq_ite b x y
 
 @[simp] theorem cond_not (b : Bool) (t e : α) : cond (!b) t e = cond b e t := by
@@ -621,11 +574,6 @@ protected theorem cond_false {α : Sort u} {a b : α} : cond false a b = b := co
 @[simp] theorem cond_then_self  : ∀ (c b : Bool), cond c c b = (c || b) := by decide
 @[simp] theorem cond_else_self : ∀ (c b : Bool), cond c b c = (c && b) := by decide
 
-@[deprecated cond_then_not_self (since := "2025-04-04")] abbrev cond_true_not_same := @cond_then_not_self
-@[deprecated cond_else_not_self (since := "2025-04-04")] abbrev cond_false_not_same := @cond_else_not_self
-@[deprecated cond_then_self (since := "2025-04-04")] abbrev cond_true_same := @cond_then_self
-@[deprecated cond_else_self (since := "2025-04-04")] abbrev cond_false_same := @cond_else_self
-
 theorem cond_pos {b : Bool} {a a' : α} (h : b = true) : (bif b then a else a') = a := by
   rw [h, cond_true]
 
@@ -665,7 +613,7 @@ theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidab
 
 end Bool
 
-export Bool (cond_eq_if xor and or not)
+export Bool (cond_eq_if cond_eq_ite xor and or not)
 
 /-! ### decide -/
 

src/Init/Data/ByteArray.lean

@@ -10,5 +10,3 @@ public import Init.Data.ByteArray.Basic
 public import Init.Data.ByteArray.Bootstrap
 public import Init.Data.ByteArray.Extra
 public import Init.Data.ByteArray.Lemmas
-
-public section

src/Init/Data/ByteArray/Basic.lean

@@ -6,13 +6,12 @@ Author: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.DecidableEq
 public import Init.Data.UInt.Basic
-public import Init.Data.UInt.BasicAux
 import all Init.Data.UInt.BasicAux
-public import Init.Data.Option.Basic
 public import Init.Data.Array.Extract
 
+set_option doc.verso true
+
 @[expose] public section
 universe u
 
@@ -25,27 +24,46 @@ attribute [ext] ByteArray
 instance : DecidableEq ByteArray :=
   fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
 
-@[deprecated emptyWithCapacity (since := "2025-03-12")]
-abbrev mkEmpty := emptyWithCapacity
-
 instance : Inhabited ByteArray where
   default := empty
 
 instance : EmptyCollection ByteArray where
   emptyCollection := ByteArray.empty
 
+/--
+Retrieves the size of the array as a platform-specific fixed-width integer.
+
+Because {name}`USize` is big enough to address all memory on every platform that Lean supports,
+there are in practice no {name}`ByteArray`s that have more elements that {name}`USize` can count.
+-/
 @[extern "lean_sarray_size", simp]
 def usize (a : @& ByteArray) : USize :=
   a.size.toUSize
 
+/--
+Retrieves the byte at the indicated index. Callers must prove that the index is in bounds. The index
+is represented by a platform-specific fixed-width integer (either 32 or 64 bits).
+
+Because {name}`USize` is big enough to address all memory on every platform that Lean supports, there are
+in practice no {name}`ByteArray`s for which {name}`uget` cannot retrieve all elements.
+-/
 @[extern "lean_byte_array_uget"]
 def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, h => bs[i]
 
+/--
+Retrieves the byte at the indicated index. Panics if the index is out of bounds.
+-/
 @[extern "lean_byte_array_get"]
 def get! : (@& ByteArray) → (@& Nat) → UInt8
   | ⟨bs⟩, i => bs[i]!
 
+/--
+Retrieves the byte at the indicated index. Callers must prove that the index is in bounds.
+
+Use {name}`uget` for a more efficient alternative or {name}`get!` for a variant that panics if the
+index is out of bounds.
+-/
 @[extern "lean_byte_array_fget"]
 def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
   | ⟨bs⟩, i, _ => bs[i]
@@ -56,37 +74,65 @@ instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
 instance : GetElem ByteArray USize UInt8 fun xs i => i.toFin < xs.size where
   getElem xs i h := xs.uget i h
 
+/--
+Replaces the byte at the given index.
+
+The array is modified in-place if there are no other references to it.
+
+If the index is out of bounds, the array is returned unmodified.
+-/
 @[extern "lean_byte_array_set"]
 def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
   | ⟨bs⟩, i, b => ⟨bs.set! i b⟩
 
+/--
+Replaces the byte at the given index.
+
+No bounds check is performed, but the function requires a proof that the index is in bounds. This
+proof can usually be omitted, and will be synthesized automatically.
+
+The array is modified in-place if there are no other references to it.
+-/
 @[extern "lean_byte_array_fset"]
 def set : (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩
 
-@[extern "lean_byte_array_uset"]
+@[extern "lean_byte_array_uset", inherit_doc ByteArray.set]
 def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
   | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩
 
+/--
+Computes a hash for a {name}`ByteArray`.
+-/
 @[extern "lean_byte_array_hash"]
 protected opaque hash (a : @& ByteArray) : UInt64
 
 instance : Hashable ByteArray where
   hash := ByteArray.hash
 
+/--
+Returns {name}`true` when {name}`s` contains zero bytes.
+-/
 def isEmpty (s : ByteArray) : Bool :=
   s.size == 0
 
 /--
-  Copy the slice at `[srcOff, srcOff + len)` in `src` to `[destOff, destOff + len)` in `dest`, growing `dest` if necessary.
-  If `exact` is `false`, the capacity will be doubled when grown. -/
+Copies the slice at `[srcOff, srcOff + len)` in {name}`src` to `[destOff, destOff + len)` in
+{name}`dest`, growing {name}`dest` if necessary. If {name}`exact` is {name}`false`, the capacity
+will be doubled when grown.
+-/
 @[extern "lean_byte_array_copy_slice"]
 def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
   ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + min len (src.data.size - srcOff)) dest.data.size⟩
 
+/--
+Copies the bytes with indices {name}`b` (inclusive) to {name}`e` (exclusive) to a new
+{name}`ByteArray`.
+-/
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)
 
+@[inline]
 protected def fastAppend (a : ByteArray) (b : ByteArray) : ByteArray :=
   -- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize
   b.copySlice 0 a a.size b.size false
@@ -113,6 +159,9 @@ theorem append_eq {a b : ByteArray} : a.append b = a ++ b := rfl
 theorem fastAppend_eq {a b : ByteArray} : a.fastAppend b = a ++ b := by
   simp [← append_eq_fastAppend]
 
+/--
+Converts a packed array of bytes to a linked list.
+-/
 def toList (bs : ByteArray) : List UInt8 :=
   let rec loop (i : Nat) (r : List UInt8) :=
     if i < bs.size then
@@ -123,16 +172,12 @@ def toList (bs : ByteArray) : List UInt8 :=
     decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
-  let rec @[specialize] loop (i : Nat) :=
-    if h : i < a.size then
-      if p a[i] then some i else loop (i+1)
-    else
-      none
-    termination_by a.size - i
-    decreasing_by decreasing_trivial_pre_omega
-  loop start
+/--
+Finds the index of the first byte in {name}`a` for which {name}`p` returns {name}`true`. If no byte
+in {name}`a` satisfies {name}`p`, then the result is {name}`none`.
 
+The index is returned along with a proof that it is a valid index in the array.
+-/
 @[inline] def findFinIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option (Fin a.size) :=
   let rec @[specialize] loop (i : Nat) :=
     if h : i < a.size then
@@ -144,11 +189,29 @@ def toList (bs : ByteArray) : List UInt8 :=
   loop start
 
 /--
-  We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
-  This is similar to the `Array` version.
+Finds the index of the first byte in {name}`a` for which {name}`p` returns {name}`true`. If no byte
+in {name}`a` satisfies {name}`p`, then the result is {name}`none`.
 
-  TODO: avoid code duplication in the future after we improve the compiler.
+The variant {name}`findFinIdx?` additionally returns a proof that the found index is in bounds.
 -/
+@[inline] def findIdx? (a : ByteArray) (p : UInt8 → Bool) (start := 0) : Option Nat :=
+  let rec @[specialize] loop (i : Nat) :=
+    if h : i < a.size then
+      if p a[i] then some i else loop (i+1)
+    else
+      none
+    termination_by a.size - i
+    decreasing_by decreasing_trivial_pre_omega
+  loop start
+
+/--
+An efficient implementation of {name}`ForIn.forIn` for {name}`ByteArray` that uses {name}`USize`
+rather than {name}`Nat` for indices.
+
+We claim this unsafe implementation is correct because an array cannot have more than
+{name}`USize.size` elements in our runtime. This is similar to the {name}`Array` version.
+-/
+-- TODO: avoid code duplication in the future after we improve the compiler.
 @[inline] unsafe def forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
   let sz := as.usize
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -161,7 +224,11 @@ def toList (bs : ByteArray) : List UInt8 :=
       pure b
   loop 0 b
 
-/-- Reference implementation for `forIn` -/
+/--
+The reference implementation of {name}`ForIn.forIn` for {name}`ByteArray`.
+
+In compiled code, this is replaced by the more efficient {name}`ByteArray.forInUnsafe`.
+-/
 @[implemented_by ByteArray.forInUnsafe]
 protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
   let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
@@ -179,7 +246,13 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
 instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
-/-- See comment at `forInUnsafe` -/
+/--
+An efficient implementation of a monadic left fold on for {name}`ByteArray` that uses {name}`USize`
+rather than {name}`Nat` for indices.
+
+We claim this unsafe implementation is correct because an array cannot have more than
+{name}`USize.size` elements in our runtime. This is similar to the {name}`Array` version.
+-/
 -- TODO: avoid code duplication.
 @[inline]
 unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β :=
@@ -196,7 +269,14 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   else
     pure init
 
-/-- Reference implementation for `foldlM` -/
+/--
+A monadic left fold on {name}`ByteArray` that iterates over an array from low to high indices,
+computing a running value.
+
+Each element of the array is combined with the value from the prior elements using a monadic
+function {name}`f`. The initial value {name}`init` is the starting value before any elements have
+been processed.
+-/
 @[implemented_by foldlMUnsafe]
 def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β :=
   let fold (stop : Nat) (h : stop ≤ as.size) :=
@@ -214,11 +294,23 @@ def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 →
   else
     fold as.size (Nat.le_refl _)
 
+/--
+A left fold on {name}`ByteArray` that iterates over an array from low to high indices, computing a
+running value.
+
+Each element of the array is combined with the value from the prior elements using a function
+{name}`f`. The initial value {name}`init` is the starting value before any elements have been
+processed.
+
+{name}`ByteArray.foldlM` is a monadic variant of this function.
+-/
 @[inline]
 def foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : β :=
   Id.run <| as.foldlM (pure <| f · ·) init start stop
 
-/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
+set_option doc.verso false -- Awaiting intra-module forward reference support
+/--
+Iterator over the bytes (`UInt8`) of a `ByteArray`.
 
 Typically created by `arr.iter`, where `arr` is a `ByteArray`.
 
@@ -242,6 +334,7 @@ structure Iterator where
   current byte is `(default : UInt8)`. -/
   idx : Nat
   deriving Inhabited
+set_option doc.verso true
 
 /-- Creates an iterator at the beginning of an array. -/
 def mkIterator (arr : ByteArray) : Iterator :=
@@ -259,16 +352,25 @@ theorem Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx :=
 
 namespace Iterator
 
-/-- Number of bytes remaining in the iterator. -/
+/--
+The number of bytes remaining in the iterator.
+-/
 def remainingBytes : Iterator → Nat
   | ⟨arr, i⟩ => arr.size - i
 
 @[inherit_doc Iterator.idx]
 def pos := Iterator.idx
 
-/-- The byte at the current position.
+/-- True if the iterator is past the array's last byte. -/
+@[inline]
+def atEnd : Iterator → Bool
+  | ⟨arr, i⟩ => i ≥ arr.size
 
-On an invalid position, returns `(default : UInt8)`. -/
+/--
+The byte at the current position.
+
+On an invalid position, returns {lean}`(default : UInt8)`.
+-/
 @[inline]
 def curr : Iterator → UInt8
   | ⟨arr, i⟩ =>
@@ -277,27 +379,28 @@ def curr : Iterator → UInt8
     else
       default
 
-/-- Moves the iterator's position forward by one byte, unconditionally.
+/--
+Moves the iterator's position forward by one byte, unconditionally.
 
 It is only valid to call this function if the iterator is not at the end of the array, *i.e.*
-`Iterator.atEnd` is `false`; otherwise, the resulting iterator will be invalid. -/
+{name}`Iterator.atEnd` is {name}`false`; otherwise, the resulting iterator will be invalid.
+-/
 @[inline]
 def next : Iterator → Iterator
   | ⟨arr, i⟩ => ⟨arr, i + 1⟩
 
-/-- Decreases the iterator's position.
+/--
+Decreases the iterator's position.
 
-If the position is zero, this function is the identity. -/
+If the position is zero, this function is the identity.
+-/
 @[inline]
 def prev : Iterator → Iterator
   | ⟨arr, i⟩ => ⟨arr, i - 1⟩
 
-/-- True if the iterator is past the array's last byte. -/
-@[inline]
-def atEnd : Iterator → Bool
-  | ⟨arr, i⟩ => i ≥ arr.size
-
-/-- True if the iterator is not past the array's last byte. -/
+/--
+True if the iterator is valid; that is, it is not past the array's last byte.
+-/
 @[inline]
 def hasNext : Iterator → Bool
   | ⟨arr, i⟩ => i < arr.size
@@ -323,17 +426,21 @@ def next' (it : Iterator) (_h : it.hasNext) : Iterator :=
 def hasPrev : Iterator → Bool
   | ⟨_, i⟩ => i > 0
 
-/-- Moves the iterator's position to the end of the array.
+/--
+Moves the iterator's position to the end of the array.
 
-Note that `i.toEnd.atEnd` is always `true`. -/
+Given {given}`i : ByteArray.Iterator`, note that {lean}`i.toEnd.atEnd` is always {name}`true`.
+-/
 @[inline]
 def toEnd : Iterator → Iterator
   | ⟨arr, _⟩ => ⟨arr, arr.size⟩
 
-/-- Moves the iterator's position several bytes forward.
+/--
+Moves the iterator's position several bytes forward.
 
 The resulting iterator is only valid if the number of bytes to skip is less than or equal to
-the number of bytes left in the iterator. -/
+the number of bytes left in the iterator.
+-/
 @[inline]
 def forward : Iterator → Nat → Iterator
   | ⟨arr, i⟩, f => ⟨arr, i + f⟩
@@ -341,9 +448,11 @@ def forward : Iterator → Nat → Iterator
 @[inherit_doc forward, inline]
 def nextn : Iterator → Nat → Iterator := forward
 
-/-- Moves the iterator's position several bytes back.
+/--
+Moves the iterator's position several bytes back.
 
-If asked to go back more bytes than available, stops at the beginning of the array. -/
+If asked to go back more bytes than available, stops at the beginning of the array.
+-/
 @[inline]
 def prevn : Iterator → Nat → Iterator
   | ⟨arr, i⟩, f => ⟨arr, i - f⟩

src/Init/Data/ByteArray/Bootstrap.lean

@@ -6,16 +6,22 @@ Author: Markus Himmel
 module
 
 prelude
-public import Init.Prelude
 public import Init.Data.List.Basic
 
 public section
+set_option doc.verso true
 
 namespace ByteArray
 
 @[simp]
 theorem data_push {a : ByteArray} {b : UInt8} : (a.push b).data = a.data.push b := rfl
 
+/--
+Appends two byte arrays.
+
+In compiled code, calls to {name}`ByteArray.append` are replaced with the much more efficient
+{name (scope:="Init.Data.ByteArray.Basic")}`ByteArray.fastAppend`.
+-/
 @[expose]
 protected def append (a b : ByteArray) : ByteArray :=
   ⟨⟨a.data.toList ++ b.data.toList⟩⟩

src/Init/Data/ByteArray/Extra.lean

@@ -9,7 +9,13 @@ prelude
 public import Init.Data.ByteArray.Basic
 import Init.Data.String.Basic
 
-/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
+set_option doc.verso true
+
+/--
+Interprets a {name}`ByteArray` of size 8 as a little-endian {name}`UInt64`.
+
+Panics if the array's size is not 8.
+-/
 public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
@@ -21,7 +27,11 @@ public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
 
-/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
+/--
+Interprets a {name}`ByteArray` of size 8 as a big-endian {name}`UInt64`.
+
+Panics if the array's size is not 8.
+-/
 public def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 0).toUInt64 <<< 0x38 |||

src/Init/Data/ByteArray/Lemmas.lean

@@ -7,10 +7,11 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
-public import Init.Data.Array.Extract
 
 public section
 
+namespace ByteArray
+
 -- At present the preferred normal form for empty byte arrays is `ByteArray.empty`
 @[simp]
 theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl
@@ -19,10 +20,10 @@ theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl
 theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl
 
 @[simp]
-theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
+theorem data_empty : ByteArray.empty.data = #[] := rfl
 
 @[simp]
-theorem ByteArray.data_extract {a : ByteArray} {b e : Nat} :
+theorem data_extract {a : ByteArray} {b e : Nat} :
     (a.extract b e).data = a.data.extract b e := by
   simp [extract, copySlice]
   by_cases b ≤ e
@@ -30,39 +31,39 @@ theorem ByteArray.data_extract {a : ByteArray} {b e : Nat} :
   · rw [Array.extract_eq_empty_of_le (by omega), Array.extract_eq_empty_of_le (by omega)]
 
 @[simp]
-theorem ByteArray.extract_zero_size {b : ByteArray} : b.extract 0 b.size = b := by
+theorem extract_zero_size {b : ByteArray} : b.extract 0 b.size = b := by
   ext1
   simp
 
 @[simp]
-theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by
+theorem extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by
   ext1
   simp [Nat.min_le_left]
 
-theorem ByteArray.fastAppend_eq_copySlice {a b : ByteArray} :
+theorem fastAppend_eq_copySlice {a b : ByteArray} :
   a.fastAppend b = b.copySlice 0 a a.size b.size false := rfl
 
 @[simp]
-theorem List.toByteArray_append {l l' : List UInt8} :
+theorem _root_.List.toByteArray_append {l l' : List UInt8} :
     (l ++ l').toByteArray = l.toByteArray ++ l'.toByteArray := by
   simp [List.toByteArray_append']
 
 @[simp]
-theorem ByteArray.toList_data_append {l l' : ByteArray} :
+theorem toList_data_append {l l' : ByteArray} :
     (l ++ l').data.toList = l.data.toList ++ l'.data.toList := by
   simp [← append_eq]
 
 @[simp]
-theorem ByteArray.data_append {l l' : ByteArray} :
+theorem data_append {l l' : ByteArray} :
     (l ++ l').data = l.data ++ l'.data := by
   simp [← Array.toList_inj]
 
 @[simp]
-theorem ByteArray.size_empty : ByteArray.empty.size = 0 := by
+theorem size_empty : ByteArray.empty.size = 0 := by
   simp [← ByteArray.size_data]
 
 @[simp]
-theorem List.data_toByteArray {l : List UInt8} :
+theorem _root_.List.data_toByteArray {l : List UInt8} :
     l.toByteArray.data = l.toArray := by
   rw [List.toByteArray]
   suffices ∀ a b, (List.toByteArray.loop a b).data = b.data ++ a.toArray by
@@ -71,153 +72,159 @@ theorem List.data_toByteArray {l : List UInt8} :
   fun_induction List.toByteArray.loop a b with simp_all
 
 @[simp]
-theorem List.size_toByteArray {l : List UInt8} :
+theorem _root_.List.size_toByteArray {l : List UInt8} :
     l.toByteArray.size = l.length := by
   simp [← ByteArray.size_data]
 
 @[simp]
-theorem List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl
+theorem _root_.List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl
 
 @[simp]
-theorem ByteArray.empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by
+theorem empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by
   ext1
   simp
 
 @[simp]
-theorem ByteArray.append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
+theorem append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
   ext1
   simp
 
 @[simp, grind =]
-theorem ByteArray.size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size := by
+theorem size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size := by
   simp [← size_data]
 
 @[simp]
-theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by
+theorem size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by
   refine ⟨fun h => ?_, fun h => h ▸ ByteArray.size_empty⟩
   ext1
   simp [← Array.size_eq_zero_iff, h]
 
-theorem ByteArray.getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
+theorem getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
     a[i] = a.data[i]'(by simpa [← size_data]) := rfl
 
 @[simp]
-theorem ByteArray.getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
+theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
     (hlt : i < a.size) : (a ++ b)[i] = a[i] := by
   simp only [getElem_eq_getElem_data, data_append]
   rw [Array.getElem_append_left (by simpa)]
 
-theorem ByteArray.getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
+theorem getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
     (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by
   simp only [getElem_eq_getElem_data, data_append]
   rw [Array.getElem_append_right (by simpa)]
   simp
 
 @[simp]
-theorem List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} :
+theorem _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} :
     l.toByteArray[i]'h = l[i]'(by simp_all) := by
   simp [ByteArray.getElem_eq_getElem_data]
 
-theorem List.getElem_eq_getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.length} :
+theorem _root_.List.getElem_eq_getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.length} :
     l[i]'h = l.toByteArray[i]'(by simp_all) := by
   simp
 
 @[simp]
-theorem ByteArray.size_extract {a : ByteArray} {b e : Nat} :
+theorem size_extract {a : ByteArray} {b e : Nat} :
     (a.extract b e).size = min e a.size - b := by
   simp [← size_data]
 
 @[simp]
-theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by
+theorem extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by
   rw [← size_eq_zero_iff, size_extract]
   omega
 
 @[simp]
-theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by
+theorem extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by
   simp only [extract_eq_empty_iff]
   exact Nat.le_trans (Nat.min_le_left _ _) (by simp)
 
 @[simp]
-theorem ByteArray.append_eq_empty_iff {a b : ByteArray} :
+theorem append_eq_empty_iff {a b : ByteArray} :
     a ++ b = ByteArray.empty ↔ a = ByteArray.empty ∧ b = ByteArray.empty := by
   simp [← size_eq_zero_iff, size_append]
 
 @[simp]
-theorem List.toByteArray_eq_empty {l : List UInt8} :
+theorem toByteArray_eq_empty {l : List UInt8} :
     l.toByteArray = ByteArray.empty ↔ l = [] := by
   simp [← ByteArray.size_eq_zero_iff]
 
-theorem ByteArray.append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) :
+@[simp]
+theorem append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) :
     xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂ := by
   simp [ByteArray.ext_iff, Array.append_right_inj]
 
 @[simp]
-theorem ByteArray.extract_append_extract {a : ByteArray} {i j k : Nat} :
+theorem append_left_inj {xs₁ xs₂ : ByteArray} (ys : ByteArray) :
+    xs₁ ++ ys = xs₂ ++ ys ↔ xs₁ = xs₂ := by
+  simp [ByteArray.ext_iff, Array.append_left_inj]
+
+@[simp]
+theorem extract_append_extract {a : ByteArray} {i j k : Nat} :
     a.extract i j ++ a.extract j k = a.extract (min i j) (max j k) := by
   ext1
   simp
 
-theorem ByteArray.extract_eq_extract_append_extract {a : ByteArray} {i k : Nat} (j : Nat)
+theorem extract_eq_extract_append_extract {a : ByteArray} {i k : Nat} (j : Nat)
     (hi : i ≤ j) (hk : j ≤ k) :
     a.extract i k = a.extract i j ++ a.extract j k := by
   simp
   rw [Nat.min_eq_left hi, Nat.max_eq_right hk]
 
-theorem ByteArray.append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂ := by
+theorem append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂ := by
   simp only [ByteArray.ext_iff, ← ByteArray.size_data, ByteArray.data_append] at *
   exact Array.append_inj_left h hl
 
-theorem ByteArray.extract_append_eq_right {a b : ByteArray} {i : Nat} (hi : i = a.size) :
-    (a ++ b).extract i (a ++ b).size = b := by
-  subst hi
+theorem extract_append_eq_right {a b : ByteArray} {i j : Nat} (hi : i = a.size) (hj : j = a.size + b.size) :
+    (a ++ b).extract i j = b := by
+  subst hi hj
   ext1
   simp [← size_data]
 
-theorem ByteArray.extract_append_eq_left {a b : ByteArray} {i : Nat} (hi : i = a.size) :
+theorem extract_append_eq_left {a b : ByteArray} {i : Nat} (hi : i = a.size) :
     (a ++ b).extract 0 i = a := by
   subst hi
   ext1
   simp
 
-theorem ByteArray.extract_append_size_left {a b : ByteArray} {i : Nat} :
+theorem extract_append_size_left {a b : ByteArray} {i : Nat} :
     (a ++ b).extract i a.size = a.extract i a.size := by
   ext1
   simp
 
-theorem ByteArray.extract_append_size_add {a b : ByteArray} {i j : Nat} :
+theorem extract_append_size_add {a b : ByteArray} {i j : Nat} :
     (a ++ b).extract (a.size + i) (a.size + j) = b.extract i j := by
   ext1
   simp
 
-theorem ByteArray.extract_append  {as bs : ByteArray} {i j : Nat} :
+theorem extract_append  {as bs : ByteArray} {i j : Nat} :
     (as ++ bs).extract i j = as.extract i j ++ bs.extract (i - as.size) (j - as.size) := by
   ext1
   simp
 
-theorem ByteArray.extract_append_size_add' {a b : ByteArray} {i j k : Nat} (h : k = a.size) :
+theorem extract_append_size_add' {a b : ByteArray} {i j k : Nat} (h : k = a.size) :
     (a ++ b).extract (k + i) (k + j) = b.extract i j := by
   cases h
   rw [extract_append_size_add]
 
-theorem ByteArray.extract_extract {a : ByteArray} {i j k l : Nat} :
+theorem extract_extract {a : ByteArray} {i j k l : Nat} :
     (a.extract i j).extract k l = a.extract (i + k) (min (i + l) j) := by
   ext1
   simp
 
-theorem ByteArray.getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.extract start stop).size) :
+theorem getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.extract start stop).size) :
     start + i < xs.size := by
   rw [size_extract] at h; apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
   apply Nat.sub_le_sub_right; apply Nat.min_le_right
 
-theorem ByteArray.getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat}
+theorem getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat}
     (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by
   simp [getElem_eq_getElem_data]
 
-theorem ByteArray.extract_eq_extract_left {a : ByteArray} {i i' j : Nat} :
+theorem extract_eq_extract_left {a : ByteArray} {i i' j : Nat} :
     a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by
   simp [ByteArray.ext_iff, Array.extract_eq_extract_left]
 
-theorem ByteArray.extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
+theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
     a.extract i (i + 1) = [a[i]].toByteArray := by
   ext
   · simp
@@ -226,34 +233,57 @@ theorem ByteArray.extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.si
     obtain rfl : j = 0 := by simpa using hj'
     simp [ByteArray.getElem_eq_getElem_data]
 
-theorem ByteArray.extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) :
+theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) :
     a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_one (by omega)]
   simp [← List.toByteArray_append]
 
-theorem ByteArray.extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) :
+theorem extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) :
     a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_two (by omega)]
   simp [← List.toByteArray_append]
 
-theorem ByteArray.extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) :
+theorem extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) :
     a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_three (by omega)]
   simp [← List.toByteArray_append]
 
-theorem ByteArray.append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by
+theorem append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by
   ext1
   simp
 
 @[simp]
-theorem ByteArray.toList_empty : ByteArray.empty.toList = [] := by
+theorem toList_empty : ByteArray.empty.toList = [] := by
   simp [ByteArray.toList, ByteArray.toList.loop]
 
-theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} :
+theorem copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} :
     ByteArray.copySlice src srcOff dest destOff len exact =
       dest.extract 0 destOff ++ src.extract srcOff (srcOff +len) ++ dest.extract (destOff + min len (src.data.size - srcOff)) dest.data.size := by
   ext1
   simp [copySlice]
+
+@[simp]
+theorem data_set {as : ByteArray} {i : Nat} {h : i < as.size} {a : UInt8} :
+    (as.set i a h).data = as.data.set i a (by simpa) := by
+  simp [set]
+
+theorem set_eq_push_extract_append_extract {as : ByteArray} {i : Nat} (h : i < as.size) {a : UInt8} :
+    as.set i a h = (as.extract 0 i).push a ++ as.extract (i + 1) as.size := by
+  ext1
+  simpa using Array.set_eq_push_extract_append_extract _
+
+@[simp]
+theorem append_toByteArray_singleton {as : ByteArray} {a : UInt8} :
+    as ++ [a].toByteArray = as.push a := by
+  ext1
+  simp
+
+@[simp]
+theorem extract_zero_max_size {a : ByteArray} {i : Nat} : a.extract 0 (max i a.size) = a := by
+  ext1
+  simp [Nat.le_max_right]
+
+end ByteArray

src/Init/Data/Char.lean

@@ -9,5 +9,3 @@ prelude
 public import Init.Data.Char.Basic
 public import Init.Data.Char.Lemmas
 public import Init.Data.Char.Order
-
-public section

src/Init/Data/Char/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Char.Basic
 import all Init.Data.Char.Basic
 public import Init.Data.UInt.Lemmas
 
@@ -14,12 +13,16 @@ public section
 
 namespace Char
 
-@[ext] protected theorem ext : {a b : Char} → a.val = b.val → a = b
+@[deprecated Char.ext (since := "2025-10-26")]
+protected theorem eq_of_val_eq : {a b : Char} → a.val = b.val → a = b
   | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
 
 theorem le_def {a b : Char} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
 theorem lt_def {a b : Char} : a < b ↔ a.1 < b.1 := .rfl
+
+@[deprecated lt_def (since := "2025-10-26")]
 theorem lt_iff_val_lt_val {a b : Char} : a < b ↔ a.val < b.val := Iff.rfl
+
 @[simp] protected theorem not_le {a b : Char} : ¬ a ≤ b ↔ b < a := UInt32.not_le
 @[simp] protected theorem not_lt {a b : Char} : ¬ a < b ↔ b ≤ a := UInt32.not_lt
 @[simp] protected theorem le_refl (a : Char) : a ≤ a := by simp [le_def]
@@ -70,4 +73,9 @@ def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
   rw [Char.ofNat, dif_pos]
   rfl
 
+@[simp]
+theorem toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8 := rfl
+
+theorem toString_eq_singleton {c : Char} : c.toString = String.singleton c := rfl
+
 end Char

src/Init/Data/Dyadic/Basic.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.Rat.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
-import Init.Data.Int.DivMod.Lemmas
+import Init.Hints
 
 /-!
 # The dyadic rationals
@@ -287,7 +287,7 @@ theorem toRat_add (x y : Dyadic) : toRat (x + y) = toRat x + toRat y := by
     · rename_i h
       cases Int.sub_eq_iff_eq_add.mp h
       rw [toRat_ofOdd_eq_mkRat, Rat.mkRat_eq_iff (NeZero.ne _) (NeZero.ne _)]
-      simp only [succ_eq_add_one, Int.ofNat_eq_coe, Int.add_shiftLeft, ← Int.shiftLeft_add,
+      simp only [succ_eq_add_one, Int.ofNat_eq_natCast, Int.add_shiftLeft, ← Int.shiftLeft_add,
         Int.natCast_mul, Int.natCast_shiftLeft, Int.shiftLeft_mul_shiftLeft, Int.add_mul]
       congr 2 <;> omega
     · rename_i h
@@ -438,7 +438,7 @@ theorem toDyadic_mkRat (a : Int) (b : Nat) (prec : Int) :
   rcases h : mkRat a b with ⟨n, d, hnz, hr⟩
   obtain ⟨m, hm, rfl, rfl⟩ := Rat.mkRat_num_den hb h
   cases prec
-  · simp only [Rat.toDyadic, Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_natCast,
+  · simp only [Rat.toDyadic, Int.ofNat_eq_natCast, Int.toNat_natCast, Int.toNat_neg_natCast,
       shiftLeft_zero, Int.natCast_mul]
     rw [Int.mul_comm d, ← Int.ediv_ediv (by simp), ← Int.shiftLeft_mul,
       Int.mul_ediv_cancel _ (by simpa using hm)]
@@ -463,7 +463,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
   rw [Rat.floor_def, Int.shiftLeft_eq, Nat.shiftLeft_eq]
   match prec with
   | .ofNat prec =>
-    simp only [Int.ofNat_eq_coe, Int.toNat_natCast, Int.toNat_neg_natCast, Nat.pow_zero,
+    simp only [Int.ofNat_eq_natCast, Int.toNat_natCast, Int.toNat_neg_natCast, Nat.pow_zero,
       Nat.mul_one]
     have : (2 ^ prec : Rat) = ((2 ^ prec : Nat) : Rat) := by simp
     rw [Rat.zpow_natCast, this, Rat.mul_def']
@@ -472,7 +472,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
       Rat.den_ofNat, Nat.one_pow, Nat.mul_one]
     split
     · simp_all
-    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
+    · rw [Int.ediv_ediv (Int.natCast_nonneg _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       rw [Int.natCast_dvd_natCast]
@@ -495,7 +495,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
     simp only [this, Int.mul_one]
     split
     · simp_all
-    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
+    · rw [Int.ediv_ediv (Int.natCast_nonneg _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       · simp
@@ -682,9 +682,11 @@ instance : LE Dyadic where
 instance : DecidableLT Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
 instance : DecidableLE Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
 
-theorem lt_iff_toRat {x y : Dyadic} : x < y ↔ x.toRat < y.toRat := blt_iff_toRat
+@[simp]
+theorem toRat_lt_toRat_iff {x y : Dyadic} : x.toRat < y.toRat ↔ x < y := blt_iff_toRat.symm
 
-theorem le_iff_toRat {x y : Dyadic} : x ≤ y ↔ x.toRat ≤ y.toRat := ble_iff_toRat
+@[simp]
+theorem toRat_le_toRat_iff {x y : Dyadic} : x.toRat ≤ y.toRat ↔ x ≤ y := ble_iff_toRat.symm
 
 @[simp]
 protected theorem not_le {x y : Dyadic} : ¬x < y ↔ y ≤ x := by
@@ -696,20 +698,20 @@ protected theorem not_lt {x y : Dyadic} : ¬x ≤ y ↔ y < x := by
 
 @[simp]
 protected theorem le_refl (x : Dyadic) : x ≤ x := by
-  rw [le_iff_toRat]
+  rw [← toRat_le_toRat_iff]
   exact Rat.le_refl
 
 protected theorem le_trans {x y z : Dyadic} (h : x ≤ y) (h' : y ≤ z) : x ≤ z := by
-  rw [le_iff_toRat] at h h' ⊢
+  rw [← toRat_le_toRat_iff] at h h' ⊢
   exact Rat.le_trans h h'
 
 protected theorem le_antisymm {x y : Dyadic} (h : x ≤ y) (h' : y ≤ x) : x = y := by
-  rw [le_iff_toRat] at h h'
+  rw [← toRat_le_toRat_iff] at h h'
   rw [← toRat_inj]
   exact Rat.le_antisymm h h'
 
 protected theorem le_total (x y : Dyadic) : x ≤ y ∨ y ≤ x := by
-  rw [le_iff_toRat, le_iff_toRat]
+  rw [← toRat_le_toRat_iff, ← toRat_le_toRat_iff]
   exact Rat.le_total
 
 instance : Std.LawfulOrderLT Dyadic where

src/Init/Data/Dyadic/Instances.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Dyadic.Basic
-public import Init.Grind.Ring.Basic
 public import Init.Grind.Ordered.Ring
 
 /-! # Internal `grind` algebra instances for `Dyadic`. -/
@@ -53,8 +52,8 @@ instance : NoNatZeroDivisors Dyadic where
 
 instance : OrderedRing Dyadic where
   zero_lt_one := by decide
-  add_le_left_iff _ := by simp [le_iff_toRat, Rat.add_le_add_right]
-  mul_lt_mul_of_pos_left {_ _ _} := by simpa [lt_iff_toRat] using Rat.mul_lt_mul_of_pos_left
-  mul_lt_mul_of_pos_right {_ _ _} := by simpa [lt_iff_toRat] using Rat.mul_lt_mul_of_pos_right
+  add_le_left_iff _ := by simp [← toRat_le_toRat_iff, Rat.add_le_add_right]
+  mul_lt_mul_of_pos_left {_ _ _} := by simpa [← toRat_lt_toRat_iff] using Rat.mul_lt_mul_of_pos_left
+  mul_lt_mul_of_pos_right {_ _ _} := by simpa [← toRat_lt_toRat_iff] using Rat.mul_lt_mul_of_pos_right
 
 end Dyadic

src/Init/Data/Dyadic/Inv.lean

@@ -5,7 +5,6 @@ Authors: Kim Morrison
 -/
 module
 prelude
-import Init.Data.Dyadic.Basic
 import Init.Data.Dyadic.Round
 import Init.Grind.Ordered.Ring
 
@@ -28,7 +27,7 @@ def invAtPrec (x : Dyadic) (prec : Int) : Dyadic :=
 /-- For a positive dyadic `x`, `invAtPrec x prec * x ≤ 1`. -/
 theorem invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) :
     invAtPrec x prec * x ≤ 1 := by
-  rw [le_iff_toRat]
+  rw [← toRat_le_toRat_iff]
   rw [toRat_mul]
   rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
   unfold invAtPrec
@@ -40,19 +39,19 @@ theorem invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) :
     simp only
     have h_le : ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat ≤ (ofOdd n k hn).toRat.inv := Rat.toRat_toDyadic_le
     have h_pos : 0 ≤ (ofOdd n k hn).toRat := by
-      rw [lt_iff_toRat, toRat_zero] at hx
+      rw [← toRat_lt_toRat_iff, toRat_zero] at hx
       exact Rat.le_of_lt hx
     calc ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat * (ofOdd n k hn).toRat
         ≤ (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := Rat.mul_le_mul_of_nonneg_right h_le h_pos
       _ = 1 := by
         apply Rat.inv_mul_cancel
-        rw [lt_iff_toRat, toRat_zero] at hx
+        rw [← toRat_lt_toRat_iff, toRat_zero] at hx
         exact Rat.ne_of_gt hx
 
 /-- For a positive dyadic `x`, `1 < (invAtPrec x prec + 2^(-prec)) * x`. -/
 theorem one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) :
     1 < (invAtPrec x prec + ofIntWithPrec 1 prec) * x := by
-  rw [lt_iff_toRat]
+  rw [← toRat_lt_toRat_iff]
   rw [toRat_mul]
   rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
   unfold invAtPrec
@@ -65,12 +64,12 @@ theorem one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) :
     have h_le : (ofOdd n k hn).toRat.inv < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat :=
       Rat.lt_toRat_toDyadic_add
     have h_pos : 0 < (ofOdd n k hn).toRat := by
-      rwa [lt_iff_toRat, toRat_zero] at hx
+      rwa [← toRat_lt_toRat_iff, toRat_zero] at hx
     calc
       1 = (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := by
         symm
         apply Rat.inv_mul_cancel
-        rw [lt_iff_toRat, toRat_zero] at hx
+        rw [← toRat_lt_toRat_iff, toRat_zero] at hx
         exact Rat.ne_of_gt hx
       _ < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat * (ofOdd n k hn).toRat :=
            Rat.mul_lt_mul_of_pos_right h_le h_pos

src/Init/Data/Dyadic/Round.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Dyadic.Basic
 import all Init.Data.Dyadic.Instances
-import Init.Data.Int.Bitwise.Lemmas
 import Init.Grind.Ordered.Rat
 import Init.Grind.Ordered.Field
 
@@ -29,7 +28,7 @@ theorem roundDown_le {x : Dyadic} {prec : Int} : roundDown x prec ≤ x :=
     match h : k - prec with
     | .ofNat l =>
       dsimp
-      rw [ofOdd_eq_ofIntWithPrec, le_iff_toRat]
+      rw [ofOdd_eq_ofIntWithPrec, ← toRat_le_toRat_iff]
       replace h : k = Int.ofNat l + prec := by omega
       subst h
       simp only [toRat_ofIntWithPrec_eq_mul_two_pow]
@@ -37,7 +36,7 @@ theorem roundDown_le {x : Dyadic} {prec : Int} : roundDown x prec ≤ x :=
       refine Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_right ?_ (Rat.zpow_nonneg (by decide))
       rw [Int.shiftRight_eq_div_pow]
       rw [← Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_right (c := 2^(Int.ofNat l)) (Rat.zpow_pos (by decide))]
-      simp only [Int.natCast_pow, Int.cast_ofNat_Int, Int.ofNat_eq_coe]
+      simp only [Int.natCast_pow, Int.cast_ofNat_Int, Int.ofNat_eq_natCast]
       rw [Rat.mul_assoc, ← Rat.zpow_add (by decide), Int.add_left_neg, Rat.zpow_zero, Rat.mul_one]
       have : (2 : Rat) ^ (l : Int) = (2 ^ l : Int) := by
         rw [Rat.zpow_natCast, Rat.intCast_pow, Rat.intCast_ofNat]

src/Init/Data/Fin.lean

@@ -11,5 +11,3 @@ public import Init.Data.Fin.Log2
 public import Init.Data.Fin.Iterate
 public import Init.Data.Fin.Fold
 public import Init.Data.Fin.Lemmas
-
-public section

src/Init/Data/Fin/Basic.lean

@@ -140,7 +140,7 @@ Modulus of bounded numbers, usually invoked via the `%` operator.
 The resulting value is that computed by the `%` operator on `Nat`.
 -/
 protected def mod : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b,  Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Division of bounded numbers, usually invoked via the `/` operator.
@@ -154,7 +154,7 @@ Examples:
  * `(5 : Fin 10) / (7 : Fin 10) = (0 : Fin 10)`
 -/
 protected def div : Fin n → Fin n → Fin n
-  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
 
 /--
 Modulus of bounded numbers with respect to a `Nat`.
@@ -162,7 +162,7 @@ Modulus of bounded numbers with respect to a `Nat`.
 The resulting value is that computed by the `%` operator on `Nat`.
 -/
 def modn : Fin n → Nat → Fin n
-  | ⟨a, h⟩, m => ⟨a % m, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, m => ⟨a % m, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Bitwise and.