oops

.claude/CLAUDE.md

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

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

.github/workflows/awaiting-manual.yml

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

.github/workflows/awaiting-mathlib.yml

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

.github/workflows/build-template.yml

@@ -3,6 +3,9 @@ name: build-template
 on:
   workflow_call:
     inputs:
+      check-level:
+        type: string
+        required: true
       config:
         type: string
         required: true
@@ -113,10 +116,10 @@ jobs:
             build/stage1/**/*.ir
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
-          key: ${{ matrix.name }}-build-v4-${{ github.sha }}
+          key: ${{ matrix.name }}-build-v3-${{ github.sha }}
           # fall back to (latest) previous cache
           restore-keys: |
-            ${{ matrix.name }}-build-v4
+            ${{ matrix.name }}-build-v3
       # open nix-shell once for initial setup
       - name: Setup
         run: |
@@ -227,7 +230,7 @@ jobs:
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: matrix.test
+        if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
       - name: Test Summary
         uses: test-summary/action@v2
         with:

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

.github/workflows/ci.yml

@@ -31,6 +31,10 @@ jobs:
   configure:
     runs-on: ubuntu-latest
     outputs:
+      # 0: PRs without special label
+      # 1: PRs with `merge-ci` label, merge queue checks, master commits
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
+      check-level: ${{ steps.set-level.outputs.check-level }}
       # The build matrix, dynamically generated here
       matrix: ${{ steps.set-matrix.outputs.matrix }}
       # secondary build jobs that should not block the CI success/merge queue
@@ -106,9 +110,6 @@ 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
@@ -116,7 +117,6 @@ 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,24 +129,19 @@ 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@v8
+        uses: actions/github-script@v7
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
-            const fast = ${{ steps.set-level.outputs.fast }};
-            console.log(`level: ${level}, fast: ${fast}`);
+            console.log(`level: ${level}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
@@ -157,8 +152,7 @@ jobs:
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -171,19 +165,17 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the
                 //    Linux lake build and adds little value in the merge queue
                 // 3. To run it in release (obviously)
                 // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
                 //    available as an artifact for Grove to use.
-                "enabled": isPr || level != 1 || isPushToMaster,
-                "test": level >= 1,
-                "secondary": level == 0,
+                "check-level": (isPr || isPushToMaster) ? 0 : 2,
+                "secondary": isPr,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -194,28 +186,26 @@ jobs:
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
+                "check-level": 0,
+                "test": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
-                "test": true,
                 // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
                 "test-speedcenter": large && level >= 2,
-                // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
+                // made explicit until it can be assumed to have propagated to PRs
+                "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
               },
               {
                 "name": "Linux Reldebug",
                 "os": "ubuntu-latest",
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "CMAKE_PRESET": "reldebug",
               },
               // TODO: suddenly started failing in CI
               /*{
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
                 // exclude seriously slow/problematic tests (laketests crash)
@@ -223,10 +213,9 @@ jobs:
               },*/
               {
                 "name": "macOS",
-                "os": "macos-15-intel",
+                "os": "macos-13",
                 "release": true,
-                "test": false,  // Tier 2 platform
-                "enabled": level >= 2,
+                "check-level": 2,
                 "shell": "bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@@ -237,7 +226,7 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
+                "os": large && !isPr ? "nscloud-macos-sonoma-arm64-6x14" : "macos-14",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -246,16 +235,14 @@ jobs:
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
                 // See "Linux release" for release job levels; Grove is not a concern here
-                "enabled": isPr || level != 1,
-                "test": level >= 1,
-                "secondary": level == 0,
+                "check-level": isPr ? 0 : 2,
+                "secondary": isPr,
               },
               {
                 "name": "Windows",
-                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -267,8 +254,7 @@ jobs:
                 "os": "nscloud-ubuntu-22.04-arm64-4x16",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
-                "enabled": level >= 2,
-                "test": true,
+                "check-level": 2,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -281,7 +267,7 @@ jobs:
               //  "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
               //  "cmultilib": true,
               //  "release": true,
-              //  "enabled": level >= 2,
+              //  "check-level": 2,
               //  "cross": true,
               //  "shell": "bash -euxo pipefail {0}"
               //}
@@ -293,7 +279,7 @@ jobs:
               //   "wasm": true,
               //   "cmultilib": true,
               //   "release": true,
-              //   "enabled": level >= 2,
+              //   "check-level": 2,
               //   "cross": true,
               //   "shell": "bash -euxo pipefail {0}",
               //   // Just a few selected tests because wasm is slow
@@ -307,7 +293,7 @@ jobs:
               }
             }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            matrix = matrix.filter((job) => job["enabled"]);
+            matrix = matrix.filter((job) => level >= job["check-level"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
             core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
 
@@ -317,6 +303,7 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix}}
+      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -332,6 +319,7 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix-secondary}}
+      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -362,7 +350,7 @@ jobs:
         content: |
           A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
     - if: contains(needs.*.result, 'failure')
-      uses: actions/github-script@v8
+      uses: actions/github-script@v7
       with:
         script: |
             core.setFailed('Some jobs failed')
@@ -379,7 +367,7 @@ jobs:
         with:
           path: artifacts
       - name: Release
-        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         with:
           files: artifacts/*/*
           fail_on_unmatched_files: true
@@ -404,8 +392,6 @@ 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:
@@ -425,7 +411,7 @@ jobs:
           echo -e "\n*Full commit log*\n" >> diff.md
           git log --oneline "$last_tag"..HEAD | sed 's/^/* /' >> diff.md
       - name: Release Nightly
-        uses: softprops/action-gh-release@6cbd405e2c4e67a21c47fa9e383d020e4e28b836
+        uses: softprops/action-gh-release@72f2c25fcb47643c292f7107632f7a47c1df5cd8
         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@v8
+        uses: actions/github-script@v7
         name: Compute Alias
         with:
           result-encoding: string

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

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

.github/workflows/pr-body.yml

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

.github/workflows/pr-release.yml

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

.github/workflows/pr-title.yml

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

.github/workflows/stale.yml

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

.github/workflows/update-stage0.yml

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

.gitignore

@@ -20,6 +20,7 @@ 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/ @hargoniX
+/src/library/compiler/ @zwarich
 /src/lake/ @tydeu
-/src/Lean/Compiler/ @leodemoura @hargoniX
+/src/Lean/Compiler/ @leodemoura @zwarich
 /src/Lean/Data/Lsp/ @mhuisi
 /src/Lean/Elab/Deriving/ @kim-em
 /src/Lean/Elab/Tactic/ @kim-em

doc/dev/ffi.md

@@ -52,7 +52,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
 * `Nat` and `Int` are represented by `lean_object *`.
   Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
-* A universe `Sort u`, type constructor `... → Sort u`, `Void α` or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
+* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
   Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
@@ -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 * initialize_C(uint8_t builtin);
+lean_object * initialize_A_B(uint8_t builtin, lean_object *);
+lean_object * initialize_C(uint8_t builtin, lean_object *);
 ...
 
 argv = lean_setup_args(argc, argv); // if using process-related functionality
@@ -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);
+res = initialize_A_B(builtin, lean_io_mk_world());
 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);
+res = initialize_C(builtin, lean_io_mk_world());
 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.
-      --^ completion
+      --^ textDocument/completion
     ```
     In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
     auto-completion request at `Bla.`. The expected output is stored in

doc/examples/palindromes.lean

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

flake.nix

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

lean.code-workspace

@@ -8,15 +8,9 @@
 		},
 		{
 			"path": "tests"
-		},
-		{
-			"path": "script"
 		}
 	],
 	"settings": {
-		// Open terminal at root, not current workspace folder
-		// (there is not way to directly refer to the root folder included as `.` above)
-		"terminal.integrated.cwd": "${workspaceFolder:src}/..",
 		"files.insertFinalNewline": true,
 		"files.trimTrailingWhitespace": true,
 		"cmake.buildDirectory": "${workspaceFolder}/build/release",

script/Modulize.lean

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

script/Shake.lean

@@ -1,616 +0,0 @@
-/-
-Copyright (c) 2023 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Sebastian Ullrich
--/
-import Lake.CLI.Main
-import Lean.ExtraModUses
-
-/-! # `lake exe shake` command
-
-This command will check the current project (or a specified target module) and all dependencies for
-unused imports. This works by looking at generated `.olean` files to deduce required imports and
-ensuring that every import is used to contribute some constant or other elaboration dependency
-recorded by `recordExtraModUse`. Because recompilation is not needed this is quite fast (about 8
-seconds to check `Mathlib` and all dependencies).
--/
-
-/-- help string for the command line interface -/
-def help : String := "Lean project tree shaking tool
-Usage: lake exe shake [OPTIONS] <MODULE>..
-
-Arguments:
-  <MODULE>
-    A module path like `Mathlib`. All files transitively reachable from the
-    provided module(s) will be checked.
-
-Options:
-  --force
-    Skips the `lake build --no-build` sanity check
-
-  --fix
-    Apply the suggested fixes directly. Make sure you have a clean checkout
-    before running this, so you can review the changes.
-"
-
-open Lean
-
-/-- We use `Nat` as a bitset for doing efficient set operations.
-The bit indexes will usually be a module index. -/
-structure Bitset where
-  toNat : Nat
-deriving Inhabited, DecidableEq, Repr
-
-namespace Bitset
-
-instance : EmptyCollection Bitset where
-  emptyCollection := { toNat := 0 }
-
-instance : Insert Nat Bitset where
-  insert i s := { toNat := s.toNat ||| (1 <<< i) }
-
-instance : Singleton Nat Bitset where
-  singleton i := insert i ∅
-
-instance : Inter Bitset where
-  inter a b := { toNat := a.toNat &&& b.toNat }
-
-instance : Union Bitset where
-  union a b := { toNat := a.toNat ||| b.toNat }
-
-instance : XorOp Bitset where
-  xor a b := { toNat := a.toNat ^^^ b.toNat }
-
-def has (s : Bitset) (i : Nat) : Bool := s ∩ {i} ≠ ∅
-
-end Bitset
-
-/-- The kind of a module dependency, corresponding to the homonymous `ExtraModUse` fields. -/
-structure NeedsKind where
-  isExported : Bool
-  isMeta : Bool
-deriving Inhabited, BEq, Repr, Hashable
-
-namespace NeedsKind
-
-@[match_pattern]  abbrev priv : NeedsKind := { isExported := false, isMeta := false }
-@[match_pattern]  abbrev pub  : NeedsKind := { isExported := true,  isMeta := false }
-@[match_pattern]  abbrev metaPriv : NeedsKind := { isExported := false, isMeta := true }
-@[match_pattern]  abbrev metaPub  : NeedsKind := { isExported := true,  isMeta := true }
-
-def all : Array NeedsKind := #[pub, priv, metaPub, metaPriv]
-
-def ofImport : Lean.Import → NeedsKind
-  | { isExported := true, isMeta := true, .. } => .metaPub
-  | { isExported := true, isMeta := false, .. } => .pub
-  | { isExported := false, isMeta := true, .. } => .metaPriv
-  | { isExported := false, isMeta := false, .. } => .priv
-
-end NeedsKind
-
-/-- Logically, a map `NeedsKind → Bitset`. -/
-structure Needs where
-  pub : Bitset
-  priv : Bitset
-  metaPub : Bitset
-  metaPriv : Bitset
-deriving Inhabited, Repr
-
-def Needs.empty : Needs := default
-
-def Needs.get (needs : Needs) (k : NeedsKind) : Bitset :=
-  match k with
-  | .pub => needs.pub
-  | .priv => needs.priv
-  | .metaPub => needs.metaPub
-  | .metaPriv => needs.metaPriv
-
-def Needs.has (needs : Needs) (k : NeedsKind) (i : ModuleIdx) : Bool :=
-  needs.get k |>.has i
-
-def Needs.set (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
-  match k with
-  | .pub   => { needs with pub := s }
-  | .priv  => { needs with priv := s }
-  | .metaPub => { needs with metaPub := s }
-  | .metaPriv => { needs with metaPriv := s }
-
-def Needs.modify (needs : Needs) (k : NeedsKind) (f : Bitset → Bitset) : Needs :=
-  needs.set k (f (needs.get k))
-
-def Needs.union (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
-  needs.modify k (· ∪ s)
-
-def Needs.sub (needs : Needs) (k : NeedsKind) (s : Bitset) : Needs :=
-  needs.modify k (fun s' => s' ^^^ (s' ∩ s))
-
-/-- The main state of the checker, containing information on all loaded modules. -/
-structure State where
-  env  : Environment
-  /--
-  `transDeps[i]` is the (non-reflexive) transitive closure of `mods[i].imports`. More specifically,
-  * `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
-  * `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
-  * `j ∈ transDeps[i].priv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].pub/priv`
-  * `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import)->* j`
-  * `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import)->* j`
-  * `j ∈ transDeps[i].metaPriv` if `i -(import ...)-> i'` and `j ∈ transDeps[i'].metaPub`
-  * `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].metaPub/metaPriv`
-  -/
-  transDeps : Array Needs := #[]
-  /--
-  `transDepsOrig` is the initial value of `transDeps` before changes potentially resulting from
-  changes to upstream headers.
-  -/
-  transDepsOrig : Array Needs := #[]
-
-def State.mods (s : State) := s.env.header.moduleData
-def State.modNames (s : State) := s.env.header.moduleNames
-
-/--
-Given module `j`'s transitive dependencies, computes the union of `transImps` and the transitive
-dependencies resulting from importing the module via `imp` according to the rules of
-`State.transDeps`.
--/
-def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps : Needs) : Needs := Id.run do
-  let mut transImps := transImps
-
-  -- `j ∈ transDeps[i].pub` if `i -(public import)->+ j`
-  if imp.isExported && !imp.isMeta then
-    transImps := transImps.union .pub {j} |>.union .pub (impTransImps.get .pub)
-
-  if !imp.isExported && !imp.isMeta then
-    -- `j ∈ transDeps[i].priv` if `i -(import ...)-> _ -(public import)->* j`
-    transImps := transImps.union .priv {j} |>.union .priv (impTransImps.get .pub)
-    if imp.importAll then
-      -- `j ∈ transDeps[i].priv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].pub/priv`
-      transImps := transImps.union .priv (impTransImps.get .pub ∪ impTransImps.get .priv)
-
-  -- `j ∈ transDeps[i].metaPub` if `i -(public (meta)? import)->* _ -(public meta import)-> _ -(public (meta)? import)->* j`
-  if imp.isExported then
-    transImps := transImps.union .metaPub (impTransImps.get .metaPub)
-    if imp.isMeta then
-      transImps := transImps.union .metaPub {j} |>.union .metaPub (impTransImps.get .pub ∪ impTransImps.get .metaPub)
-
-  if !imp.isExported then
-    if imp.isMeta then
-      -- `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import)->* j`
-      transImps := transImps.union .metaPriv {j} |>.union .metaPriv (impTransImps.get .pub ∪ impTransImps.get .metaPub)
-    if imp.importAll then
-      -- `j ∈ transDeps[i].metaPriv` if `i -(import all)->+ i'` and `j ∈ transDeps[i'].metaPub/metaPriv`
-      transImps := transImps.union .metaPriv (impTransImps.get .metaPub ∪ impTransImps.get .metaPriv)
-    else
-      -- `j ∈ transDeps[i].metaPriv` if `i -(import ...)-> i'` and `j ∈ transDeps[i'].metaPub`
-      transImps := transImps.union .metaPriv (impTransImps.get .metaPub)
-
-  transImps
-
-/-- Calculates the needs for a given module `mod` from constants and recorded extra uses. -/
-def calcNeeds (env : Environment) (i : ModuleIdx) : Needs := Id.run do
-  let mut needs := default
-  for ci in env.header.moduleData[i]!.constants do
-    -- Added guard for cases like `structure` that are still exported even if private
-    let pubCI? := guard (!isPrivateName ci.name) *> (env.setExporting true).find? ci.name
-    let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
-    needs := visitExpr k ci.type needs
-    if let some e := ci.value? (allowOpaque := true) then
-      -- type and value has identical visibility under `meta`
-      let k := if k.isMeta then k else
-        if pubCI?.any (·.hasValue (allowOpaque := true)) then .pub else .priv
-      needs := visitExpr k e needs
-
-  for use in getExtraModUses env i do
-    let j := env.getModuleIdx? use.module |>.get!
-    needs := needs.union { use with } {j}
-
-  return needs
-where
-  /-- Accumulate the results from expression `e` into `deps`. -/
-  visitExpr (k : NeedsKind) e deps :=
-    Lean.Expr.foldConsts e deps fun c deps => match env.getModuleIdxFor? c with
-      | some j =>
-        let k := { k with isMeta := k.isMeta && !isMeta env c }
-        if j != i then deps.union k {j} else deps
-      | _ => deps
-
-/--
-Calculates the same as `calcNeeds` but tracing each module to a use-def declaration pair or
-`none` if merely a recorded extra use.
--/
-def getExplanations (env : Environment) (i : ModuleIdx) :
-    Std.HashMap (ModuleIdx × NeedsKind) (Option (Name × Name)) := Id.run do
-  let mut deps := default
-  for ci in env.header.moduleData[i]!.constants do
-    -- Added guard for cases like `structure` that are still exported even if private
-    let pubCI? := guard (!isPrivateName ci.name) *> (env.setExporting true).find? ci.name
-    let k := { isExported := pubCI?.isSome, isMeta := isMeta env ci.name }
-    deps := visitExpr k ci.name ci.type deps
-    if let some e := ci.value? (allowOpaque := true) then
-      let k := if k.isMeta then k else
-        if pubCI?.any (·.hasValue (allowOpaque := true)) then .pub else .priv
-      deps := visitExpr k ci.name e deps
-
-  for use in getExtraModUses env i do
-    let j := env.getModuleIdx? use.module |>.get!
-    if !deps.contains (j, { use with }) then
-      deps := deps.insert (j, { use with }) none
-
-  return deps
-where
-  /-- Accumulate the results from expression `e` into `deps`. -/
-  visitExpr (k : NeedsKind) name e deps :=
-    Lean.Expr.foldConsts e deps fun c deps => match env.getModuleIdxFor? c with
-      | some i =>
-        let k := { k with isMeta := k.isMeta && !isMeta env c }
-        if
-          if let some (some (name', _)) := deps[(i, k)]? then
-            decide (name.toString.length < name'.toString.length)
-          else true
-        then
-          deps.insert (i, k) (name, c)
-        else
-          deps
-      | _ => deps
-
-partial def initStateFromEnv (env : Environment) : State := Id.run do
-  let mut s := { env }
-  for i in 0...env.header.moduleData.size do
-    let mod := env.header.moduleData[i]!
-    let mut imps := #[]
-    let mut transImps := Needs.empty
-    for imp in mod.imports do
-      let j := env.getModuleIdx? imp.module |>.get!
-      imps := imps.push j
-      transImps := addTransitiveImps transImps imp j s.transDeps[j]!
-    s := { s with transDeps := s.transDeps.push transImps }
-  s := { s with transDepsOrig := s.transDeps }
-  return s
-
-/-- The list of edits that will be applied in `--fix`. `edits[i] = (removed, added)` where:
-
-* If `j ∈ removed` then we want to delete module named `j` from the imports of `i`
-* If `j ∈ added` then we want to add module index `j` to the imports of `i`.
--/
-abbrev Edits := Std.HashMap Name (Array Import × Array Import)
-
-/-- Register that we want to remove `tgt` from the imports of `src`. -/
-def Edits.remove (ed : Edits) (src : Name) (tgt : Import) : Edits :=
-  match ed.get? src with
-  | none => ed.insert src (#[tgt], #[])
-  | some (a, b) => ed.insert src (a.push tgt, b)
-
-/-- Register that we want to add `tgt` to the imports of `src`. -/
-def Edits.add (ed : Edits) (src : Name) (tgt : Import) : Edits :=
-  match ed.get? src with
-  | none => ed.insert src (#[], #[tgt])
-  | some (a, b) => ed.insert src (a, b.push tgt)
-
-/-- Parse a source file to extract the location of the import lines, for edits and error messages.
-
-Returns `(path, inputCtx, imports, endPos)` where `imports` is the `Lean.Parser.Module.import` list
-and `endPos` is the position of the end of the header.
--/
-def parseHeaderFromString (text path : String) :
-    IO (System.FilePath × Parser.InputContext ×
-      TSyntax ``Parser.Module.header × String.Pos.Raw) := do
-  let inputCtx := Parser.mkInputContext text path
-  let (header, parserState, msgs) ← Parser.parseHeader inputCtx
-  if !msgs.toList.isEmpty then -- skip this file if there are parse errors
-    msgs.forM fun msg => msg.toString >>= IO.println
-    throw <| .userError "parse errors in file"
-  -- the insertion point for `add` is the first newline after the imports
-  let insertion := header.raw.getTailPos?.getD parserState.pos
-  let insertion := text.findAux (· == '\n') text.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

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

script/lean-toolchain

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

script/release_checklist.py

@@ -1,58 +1,5 @@
 #!/usr/bin/env python3
 
-"""
-Release Checklist for Lean4 and Downstream Repositories
-
-This script validates the status of a Lean4 release across all dependent repositories.
-It checks whether repositories are ready for release and identifies missing steps.
-
-IMPORTANT: Keep this documentation up-to-date when modifying the script's behavior!
-
-What this script does:
-1. Validates preliminary Lean4 release infrastructure:
-   - Checks that the release branch (releases/vX.Y.0) exists
-   - Verifies CMake version settings are correct
-   - Confirms the release tag exists
-   - Validates the release page exists on GitHub (created automatically by CI after tag push)
-   - Checks the release notes page on lean-lang.org (updated while bumping the `reference-manual` repository)
-
-   **IMPORTANT: If the release page doesn't exist, the script will skip checking
-   downstream repositories and the master branch configuration. The preliminary
-   infrastructure must be in place before the release process can proceed.**
-
-   **NOTE: The GitHub release page is created AUTOMATICALLY by CI after the tag is pushed.
-   DO NOT create it manually. Wait for CI to complete after pushing the tag.**
-
-2. For each downstream repository (batteries, mathlib4, etc.):
-   - Checks if dependencies are ready (e.g., mathlib4 depends on batteries)
-   - Verifies the main branch is on the target toolchain (or newer)
-   - Checks if a PR exists to bump the toolchain (if not yet updated)
-   - Validates tags exist for the release version
-   - Ensures tags are merged into stable branches (for non-RC releases)
-   - Verifies bump branches exist and are configured correctly
-   - Special handling for ProofWidgets4 release tags
-
-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
@@ -129,39 +76,6 @@ def release_page_exists(repo_url, tag_name, github_token):
     response = requests.get(api_url, headers=headers)
     return response.status_code == 200
 
-def get_tag_workflow_status(repo_url, tag_name, github_token):
-    """Get the status of CI workflows running for a specific tag."""
-    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-
-    # Get workflow runs for the tag
-    # GitHub's workflow runs API uses the branch/tag name in the 'head_branch' field
-    api_url = f"{api_base}/actions/runs?event=push&head_branch={tag_name}"
-    response = requests.get(api_url, headers=headers)
-
-    if response.status_code != 200:
-        return None
-
-    data = response.json()
-    workflow_runs = data.get('workflow_runs', [])
-
-    if not workflow_runs:
-        return None
-
-    # Get the most recent workflow run for this tag
-    run = workflow_runs[0]
-    status = run.get('status')
-    conclusion = run.get('conclusion')
-    workflow_name = run.get('name', 'CI')
-    run_id = run.get('id')
-
-    return {
-        'status': status,
-        'conclusion': conclusion,
-        'workflow_name': workflow_name,
-        'run_id': run_id
-    }
-
 def get_release_notes(tag_name):
     """Fetch release notes page title from lean-lang.org."""
     # Strip -rcX suffix if present for the URL
@@ -170,17 +84,20 @@ def get_release_notes(tag_name):
     try:
         response = requests.get(reference_url)
         response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx)
-
+        
         # Extract title using regex
         match = re.search(r"<title>(.*?)</title>", response.text, re.IGNORECASE | re.DOTALL)
         if match:
             return match.group(1).strip()
         else:
+            print(f"  ⚠️ Could not find <title> tag in {reference_url}")
             return None
-
-    except requests.exceptions.RequestException:
+            
+    except requests.exceptions.RequestException as e:
+        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
         return None
-    except Exception:
+    except Exception as e:
+        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
         return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
@@ -369,68 +286,6 @@ def check_bump_branch_toolchain(url, bump_branch, github_token):
     print(f"  ✅ Bump branch correctly uses toolchain: {content}")
     return True
 
-def get_pr_ci_status(repo_url, pr_number, github_token):
-    """Get the CI status for a pull request."""
-    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
-    headers = {'Authorization': f'token {github_token}'} if github_token else {}
-
-    # Get PR details to find the head SHA
-    pr_response = requests.get(f"{api_base}/pulls/{pr_number}", headers=headers)
-    if pr_response.status_code != 200:
-        return "unknown", "Could not fetch PR details"
-
-    pr_data = pr_response.json()
-    head_sha = pr_data['head']['sha']
-
-    # Get check runs for the commit
-    check_runs_response = requests.get(
-        f"{api_base}/commits/{head_sha}/check-runs",
-        headers=headers
-    )
-
-    if check_runs_response.status_code != 200:
-        return "unknown", "Could not fetch check runs"
-
-    check_runs_data = check_runs_response.json()
-    check_runs = check_runs_data.get('check_runs', [])
-
-    if not check_runs:
-        # No check runs, check for status checks (legacy)
-        status_response = requests.get(
-            f"{api_base}/commits/{head_sha}/status",
-            headers=headers
-        )
-        if status_response.status_code == 200:
-            status_data = status_response.json()
-            state = status_data.get('state', 'unknown')
-            if state == 'success':
-                return "success", "All status checks passed"
-            elif state == 'failure':
-                return "failure", "Some status checks failed"
-            elif state == 'pending':
-                return "pending", "Status checks in progress"
-        return "unknown", "No CI checks found"
-
-    # Analyze check runs
-    conclusions = [run['conclusion'] for run in check_runs if run.get('status') == 'completed']
-    in_progress = [run for run in check_runs if run.get('status') in ['queued', 'in_progress']]
-
-    if in_progress:
-        return "pending", f"{len(in_progress)} check(s) in progress"
-
-    if not conclusions:
-        return "pending", "Checks queued"
-
-    if all(c == 'success' for c in conclusions):
-        return "success", f"All {len(conclusions)} checks passed"
-
-    failed = sum(1 for c in conclusions if c in ['failure', 'timed_out', 'action_required'])
-    if failed > 0:
-        return "failure", f"{failed} check(s) failed"
-
-    # Some checks are cancelled, skipped, or neutral
-    return "warning", f"Some checks did not complete normally"
-
 def pr_exists_with_title(repo_url, title, github_token):
     api_url = repo_url.replace("https://github.com/", "https://api.github.com/repos/") + "/pulls"
     headers = {'Authorization': f'token {github_token}'} if github_token else {}
@@ -549,57 +404,30 @@ def main():
             print(f"  ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.")
             lean4_success = False
 
-    release_page_ready = release_page_exists(lean_repo_url, toolchain, github_token)
-    if not release_page_ready:
-        print(f"  ❌ Release page for {toolchain} does not exist (This will be created by CI.)")
-
-        # Check CI workflow status
-        workflow_status = get_tag_workflow_status(lean_repo_url, toolchain, github_token)
-        if workflow_status:
-            status = workflow_status['status']
-            conclusion = workflow_status['conclusion']
-            workflow_name = workflow_status['workflow_name']
-            run_id = workflow_status['run_id']
-            workflow_url = f"{lean_repo_url}/actions/runs/{run_id}"
-
-            if status == 'in_progress' or status == 'queued':
-                print(f"     🔄 {workflow_name} workflow is {status}: {workflow_url}")
-            elif status == 'completed':
-                if conclusion == 'success':
-                    print(f"     ✅ {workflow_name} workflow completed successfully: {workflow_url}")
-                elif conclusion == 'failure':
-                    print(f"     ❌ {workflow_name} workflow failed: {workflow_url}")
-                else:
-                    print(f"     ⚠️  {workflow_name} workflow completed with status: {conclusion}: {workflow_url}")
-            else:
-                print(f"     ℹ️  {workflow_name} workflow status: {status}: {workflow_url}")
-
+    if not release_page_exists(lean_repo_url, toolchain, github_token):
+        print(f"  ❌ Release page for {toolchain} does not exist")
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-
-    # Check the actual release notes page title (informational only - does not block)
+        
+    # Check the actual release notes page title
     actual_title = get_release_notes(toolchain)
     expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1"
-    base_tag = toolchain.split('-')[0]
-    release_notes_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
 
     if actual_title is None:
-        print(f"  ⚠️  Release notes not found at {release_notes_url} (this will be fixed while updating the reference-manual repository)")
+        # Error already printed by get_release_notes
+        lean4_success = False
     elif not actual_title.startswith(expected_title_prefix):
-        print(f"  ⚠️  Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {release_notes_url}")
+        # Construct URL for the error message (using the base tag)
+        base_tag = toolchain.split('-')[0]
+        check_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
+        print(f"  ❌ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {check_url}")
+        lean4_success = False
     else:
         print(f"  ✅ Release notes page title looks good ('{actual_title}').")
 
     repo_status["lean4"] = lean4_success
 
-    # If the release page doesn't exist, skip repository checks and master branch checks
-    # The preliminary infrastructure must be in place first
-    if not release_page_exists(lean_repo_url, toolchain, github_token):
-        print("\n⚠️  Release process blocked: preliminary Lean4 infrastructure incomplete.")
-        print("   Complete the steps above, then rerun this script to proceed with downstream repositories.")
-        return
-
     # Load repositories and perform further checks
     print("\nChecking repositories...")
 
@@ -643,19 +471,6 @@ def main():
             if pr_info:
                 pr_number, pr_url = pr_info
                 print(f"  ✅ PR with title '{pr_title}' exists: #{pr_number} ({pr_url})")
-
-                # Check CI status
-                ci_status, ci_message = get_pr_ci_status(url, pr_number, github_token)
-                if ci_status == "success":
-                    print(f"     ✅ CI: {ci_message}")
-                elif ci_status == "failure":
-                    print(f"     ❌ CI: {ci_message}")
-                elif ci_status == "pending":
-                    print(f"     🔄 CI: {ci_message}")
-                elif ci_status == "warning":
-                    print(f"     ⚠️  CI: {ci_message}")
-                else:
-                    print(f"     ❓ CI: {ci_message}")
             else:
                 print(f"  ❌ PR with title '{pr_title}' does not exist")
                 print(f"     Run `script/release_steps.py {toolchain} {name}` to create it")

script/release_steps.py

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

src/CMakeLists.txt

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

src/Init.lean

@@ -14,6 +14,7 @@ public import Init.ByCases
 public import Init.RCases
 public import Init.Core
 public import Init.Control
+public import Init.Data.Basic
 public import Init.WF
 public import Init.WFTactics
 public import Init.Data

src/Init/BinderNameHint.lean

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

src/Init/ByCases.lean

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

src/Init/Classical.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.PropLemmas
 
-@[expose] public section
+public section
 
 universe u v
 
@@ -181,6 +181,9 @@ theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff
 
 theorem not_and_iff_not_or_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_not_or_not
 
+@[deprecated not_and_iff_not_or_not (since := "2025-03-18")]
+abbrev not_and_iff_or_not_not := @not_and_iff_not_or_not
+
 theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
 
 @[simp] theorem imp_iff_left_iff  : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff

src/Init/Control.lean

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

src/Init/Control/Basic.lean

@@ -45,6 +45,9 @@ 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,6 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Control.State
+public import Init.Control.Except
 public import Init.Data.ToString.Basic
 
 public section

src/Init/Control/Except.lean

@@ -10,6 +10,7 @@ module
 prelude
 public import Init.Control.Basic
 public import Init.Control.Id
+public import Init.Coe
 
 @[expose] public section
 

src/Init/Control/Lawful.lean

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

src/Init/Control/Lawful/Basic.lean

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

src/Init/Control/Lawful/Instances.lean

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

src/Init/Control/Lawful/Lemmas.lean

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

src/Init/Control/Lawful/MonadLift.lean

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

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

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

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

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

src/Init/Control/Option.lean

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

src/Init/Control/Reader.lean

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

src/Init/Control/State.lean

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

src/Init/Core.lean

@@ -8,6 +8,7 @@ notation, basic datatypes and type classes
 module
 
 prelude
+public meta import Init.Prelude
 public import Init.SizeOf
 
 public section
@@ -143,9 +144,8 @@ Computed values are cached, so the value is not recomputed.
   x.fn ()
 
 -- Ensure `Thunk.fn` is still computable even if it shouldn't be accessed directly.
-/-- Implementation detail. -/
-@[inline] def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
-@[csimp] theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
+@[inline] private def Thunk.fnImpl (x : Thunk α) : Unit → α := fun _ => x.get
+@[csimp] private theorem Thunk.fn_eq_fnImpl : @Thunk.fn = @Thunk.fnImpl := rfl
 
 /--
 Constructs a new thunk that forces `x` and then applies `x` to the result. Upon forcing, the result
@@ -600,6 +600,17 @@ export LawfulSingleton (insert_empty_eq)
 
 attribute [simp] insert_empty_eq
 
+@[deprecated insert_empty_eq (since := "2025-03-12")]
+theorem insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
+    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
+  insert_empty_eq _
+
+@[deprecated insert_empty_eq (since := "2025-03-12")]
+theorem LawfulSingleton.insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
+    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
+  insert_empty_eq _
+
+
 /-- Type class used to implement the notation `{ a ∈ c | p a }` -/
 class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/
@@ -1084,6 +1095,14 @@ theorem of_toBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d =
 theorem of_toBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p :=
   of_decide_eq_false h
 
+set_option linter.missingDocs false in
+@[deprecated of_toBoolUsing_eq_true (since := "2025-04-04")]
+abbrev ofBoolUsing_eq_true := @of_toBoolUsing_eq_true
+
+set_option linter.missingDocs false in
+@[deprecated of_toBoolUsing_eq_false (since := "2025-04-04")]
+abbrev ofBoolUsing_eq_false := @of_toBoolUsing_eq_false
+
 instance : Decidable True :=
   isTrue trivial
 
@@ -1146,7 +1165,6 @@ end
     else isFalse (fun h => absurd (h hp) hq)
   else isTrue (fun h => absurd h hp)
 
-@[inline]
 instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
   if hp : p then
     if hq : q then
@@ -1188,13 +1206,17 @@ theorem dif_neg {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort u} {t : c
   | isTrue hc   => absurd hc hnc
   | isFalse _   => rfl
 
-@[macro_inline]
+-- Remark: dite and ite are "defally equal" when we ignore the proofs.
+theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) : dite c (fun _ => t) (fun _ => e) = ite c t e :=
+  match h with
+  | isTrue _    => rfl
+  | isFalse _   => rfl
+
 instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
   match dC with
   | isTrue _   => dT
   | isFalse _  => dE
 
-@[inline]
 instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
   match dC with
   | isTrue hc  => dT hc
@@ -1345,12 +1367,12 @@ namespace Subtype
 theorem exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
   | ⟨a, h⟩ => ⟨a, h⟩
 
-variable {α : Sort u} {p : α → Prop}
+set_option linter.missingDocs false in
+@[deprecated exists_of_subtype (since := "2025-04-04")]
+abbrev existsOfSubtype := @exists_of_subtype
 
-protected theorem ext : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
-  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+variable {α : Type u} {p : α → Prop}
 
-@[deprecated Subtype.ext (since := "2025-10-26")]
 protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
@@ -1365,9 +1387,9 @@ instance {α : Type u} {p : α → Prop} [BEq α] [ReflBEq α] : ReflBEq {x : α
   rfl {x} := BEq.refl x.1
 
 instance {α : Type u} {p : α → Prop} [BEq α] [LawfulBEq α] : LawfulBEq {x : α // p x} where
-  eq_of_beq h := Subtype.ext (eq_of_beq h)
+  eq_of_beq h := Subtype.eq (eq_of_beq h)
 
-instance {α : Sort u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
+instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)
     else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
@@ -1468,8 +1490,6 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 
 @[simp] theorem Prod.map_apply (f : α → β) (g : γ → δ) (x) (y) :
     Prod.map f g (x, y) = (f x, g y) := rfl
-
--- We add `@[grind =]` to these in `Init.Data.Prod`.
 @[simp] theorem Prod.map_fst (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).1 = f x.1 := rfl
 @[simp] theorem Prod.map_snd (f : α → β) (g : γ → δ) (x) : (Prod.map f g x).2 = g x.2 := rfl
 
@@ -1486,24 +1506,20 @@ protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α}
 
 /-! # Universe polymorphic unit -/
 
-theorem PUnit.ext (a b : PUnit) : a = b := by
-  cases a; cases b; exact rfl
-
-@[deprecated PUnit.ext (since := "2025-10-26")]
 theorem PUnit.subsingleton (a b : PUnit) : a = b := by
   cases a; cases b; exact rfl
 
 theorem PUnit.eq_punit (a : PUnit) : a = ⟨⟩ :=
-  PUnit.ext a ⟨⟩
+  PUnit.subsingleton a ⟨⟩
 
 instance : Subsingleton PUnit :=
-  Subsingleton.intro PUnit.ext
+  Subsingleton.intro PUnit.subsingleton
 
 instance : Inhabited PUnit where
   default := ⟨⟩
 
 instance : DecidableEq PUnit :=
-  fun a b => isTrue (PUnit.ext a b)
+  fun a b => isTrue (PUnit.subsingleton a b)
 
 /-! # Setoid -/
 
@@ -1589,7 +1605,7 @@ gen_injective_theorems% PSigma
 gen_injective_theorems% PSum
 gen_injective_theorems% Sigma
 gen_injective_theorems% String
-gen_injective_theorems% String.Pos.Raw
+gen_injective_theorems% String.Pos
 gen_injective_theorems% Substring
 gen_injective_theorems% Subtype
 gen_injective_theorems% Sum

src/Init/Data.lean

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

src/Init/Data/AC.lean

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

src/Init/Data/Array.lean

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

src/Init/Data/Array/Attach.lean

@@ -6,7 +6,10 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
+public import Init.Data.Array.Mem
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Count
+public import Init.Data.List.Attach
 import all Init.Data.List.Attach
 
 public section
@@ -81,10 +84,10 @@ well-founded recursion mechanism to prove that the function terminates.
   simp [pmap]
 
 /-- Implementation of `pmap` using the zero-copy version of `attach`. -/
-@[inline] def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a) :
     Array β := (xs.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
 
-@[csimp] theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
   funext α β p f xs H
   cases xs
   simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith_eq_pmap]
@@ -749,6 +752,9 @@ and simplifies these to the function directly taking the value.
     (Array.replicate n x).unattach = Array.replicate n x.1 := by
   simp [unattach]
 
+@[deprecated unattach_replicate (since := "2025-03-18")]
+abbrev unattach_mkArray := @unattach_replicate
+
 /-! ### Well-founded recursion preprocessing setup -/
 
 @[wf_preprocess] theorem map_wfParam {xs : Array α} {f : α → β} :

src/Init/Data/Array/Basic.lean

@@ -6,6 +6,10 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.WFTactics
+public import Init.Data.Nat.Basic
+public import Init.Data.Fin.Basic
+public import Init.Data.UInt.BasicAux
 public import Init.GetElem
 public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
@@ -209,6 +213,20 @@ Examples:
 def replicate {α : Type u} (n : Nat) (v : α) : Array α where
   toList := List.replicate n v
 
+/--
+Creates an array that contains `n` repetitions of `v`.
+
+The corresponding `List` function is `List.replicate`.
+
+Examples:
+ * `Array.mkArray 2 true = #[true, true]`
+ * `Array.mkArray 3 () = #[(), (), ()]`
+ * `Array.mkArray 0 "anything" = #[]`
+-/
+@[extern "lean_mk_array", deprecated replicate (since := "2025-03-18")]
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
 /--
 Swaps two elements of an array. The modification is performed in-place when the reference to the
 array is unique.
@@ -226,7 +244,7 @@ def swap (xs : Array α) (i j : @& Nat) (hi : i < xs.size := by get_elem_tactic)
   let xs'  := xs.set i v₂
   xs'.set j v₁ (Nat.lt_of_lt_of_eq hj (size_set _).symm)
 
-@[simp, grind =] theorem size_swap {xs : Array α} {i j : Nat} {hi hj} : (xs.swap i j hi hj).size = xs.size := by
+@[simp] theorem size_swap {xs : Array α} {i j : Nat} {hi hj} : (xs.swap i j hi hj).size = xs.size := by
   change ((xs.set i xs[j]).set j xs[i]
     (Nat.lt_of_lt_of_eq hj (size_set _).symm)).size = xs.size
   rw [size_set, size_set]
@@ -448,7 +466,7 @@ Examples:
 -/
 abbrev take (xs : Array α) (i : Nat) : Array α := extract xs 0 i
 
-@[simp, grind =] theorem take_eq_extract {xs : Array α} {i : Nat} : xs.take i = xs.extract 0 i := rfl
+@[simp] theorem take_eq_extract {xs : Array α} {i : Nat} : xs.take i = xs.extract 0 i := rfl
 
 /--
 Removes the first `i` elements of `xs`. If `xs` has fewer than `i` elements, the new array is empty.
@@ -462,7 +480,7 @@ Examples:
 -/
 abbrev drop (xs : Array α) (i : Nat) : Array α := extract xs i xs.size
 
-@[simp, grind =] theorem drop_eq_extract {xs : Array α} {i : Nat} : xs.drop i = xs.extract i xs.size := rfl
+@[simp] theorem drop_eq_extract {xs : Array α} {i : Nat} : xs.drop i = xs.extract i xs.size := rfl
 
 @[inline]
 unsafe def modifyMUnsafe [Monad m] (xs : Array α) (i : Nat) (f : α → m α) : m (Array α) := do
@@ -734,7 +752,8 @@ of results.
 def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) :=
   -- Note: we cannot use `foldlM` here for the reference implementation because this calls
   -- `bind` and `pure` too many times. (We are not assuming `m` is a `LawfulMonad`)
-  let rec map (i : Nat) (bs : Array β) : m (Array β) := do
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    map (i : Nat) (bs : Array β) : m (Array β) := do
       if hlt : i < as.size then
         map (i+1) (bs.push (← f as[i]))
       else
@@ -894,7 +913,8 @@ entire array is checked.
 @[implemented_by anyMUnsafe, expose]
 def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
   let any (stop : Nat) (h : stop ≤ as.size) :=
-    let rec loop (j : Nat) : m Bool := do
+    let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+    loop (j : Nat) : m Bool := do
       if hlt : j < stop then
         have : j < as.size := Nat.lt_of_lt_of_le hlt h
         if (← p as[j]) then
@@ -1232,7 +1252,8 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
@@ -1249,7 +1270,8 @@ Examples:
 -/
 @[inline]
 def findFinIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option (Fin as.size) :=
-  let rec loop (j : Nat) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some ⟨j, h⟩ else loop (j + 1)
     else none
@@ -1285,6 +1307,7 @@ Examples:
 @[inline, expose]
 def findIdx (p : α → Bool) (as : Array α) : Nat := (as.findIdx? p).getD as.size
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def idxOfAux [BEq α] (xs : Array α) (v : α) (i : Nat) : Option (Fin xs.size) :=
   if h : i < xs.size then
     if xs[i] == v then some ⟨i, h⟩
@@ -1694,6 +1717,7 @@ Examples:
  * `#[3, 2, 3, 4].popWhile (· > 2) = #[3, 2]`
  * `(#[] : Array Nat).popWhile (· > 2) = #[]`
 -/
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
     if p (as[as.size - 1]'(Nat.sub_lt h (by decide))) then
@@ -1704,7 +1728,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
     as
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-@[simp, grind =] theorem popWhile_empty {p : α → Bool} :
+@[simp] theorem popWhile_empty {p : α → Bool} :
     popWhile p #[] = #[] := by
   simp [popWhile]
 
@@ -1718,7 +1742,8 @@ Examples:
  * `#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]`
 -/
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
-  let rec go (i : Nat) (acc : Array α) : Array α :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  go (i : Nat) (acc : Array α) : Array α :=
     if h : i < as.size then
       let a := as[i]
       if p a then
@@ -1741,6 +1766,7 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]`
 -/
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def eraseIdx (xs : Array α) (i : Nat) (h : i < xs.size := by get_elem_tactic) : Array α :=
   if h' : i + 1 < xs.size then
     let xs' := xs.swap (i + 1) i
@@ -1751,8 +1777,7 @@ termination_by xs.size - i
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ h
 
 -- This is required in `Lean.Data.PersistentHashMap`.
-@[simp, grind =]
-theorem size_eraseIdx {xs : Array α} (i : Nat) (h) : (xs.eraseIdx i h).size = xs.size - 1 := by
+@[simp] theorem size_eraseIdx {xs : Array α} (i : Nat) (h) : (xs.eraseIdx i h).size = xs.size - 1 := by
   induction xs, i, h using Array.eraseIdx.induct with
   | @case1 xs i h h' xs' ih =>
     unfold eraseIdx
@@ -1774,6 +1799,7 @@ Examples:
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]`
 * `#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]`
 -/
+@[grind]
 def eraseIdxIfInBounds (xs : Array α) (i : Nat) : Array α :=
   if h : i < xs.size then xs.eraseIdx i h else xs
 
@@ -1836,7 +1862,8 @@ Examples:
  * `#["tues", "thur", "sat"].insertIdx 3 "wed" = #["tues", "thur", "sat", "wed"]`
 -/
 @[inline] def insertIdx (as : Array α) (i : Nat) (a : α) (_ : i ≤ as.size := by get_elem_tactic) : Array α :=
-  let rec loop (as : Array α) (j : Fin as.size) :=
+  let rec @[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
+  loop (as : Array α) (j : Fin as.size) :=
     if i < j then
       let j' : Fin as.size := ⟨j-1, Nat.lt_of_le_of_lt (Nat.pred_le _) j.2⟩
       let as := as.swap j' j
@@ -1890,6 +1917,7 @@ def insertIdxIfInBounds (as : Array α) (i : Nat) (a : α) : Array α :=
   else
     as
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -1918,7 +1946,7 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-@[specialize]
+@[semireducible, specialize] -- This is otherwise irreducible because it uses well-founded recursion.
 def zipWithMAux {m : Type v → Type w} [Monad m] (as : Array α) (bs : Array β) (f : α → β → m γ) (i : Nat) (cs : Array γ) : m (Array γ) := do
   if h : i < as.size then
     let a := as[i]
@@ -2081,6 +2109,7 @@ private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat),
     have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
     a != as[i] && allDiffAuxAux as a i this
 
+@[semireducible] -- This is otherwise irreducible because it uses well-founded recursion.
 private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
   if h : i < as.size then
     allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
@@ -2134,3 +2163,5 @@ instance [ToString α] : ToString (Array α) where
   toString xs := String.Internal.append "#" (toString xs.toList)
 
 end Array
+
+export Array (mkArray)

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 
 public section
@@ -31,7 +32,7 @@ theorem foldlM_toList.aux [Monad m]
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_toList.aux (j := j+1) H]
-    rw (occs := [2]) [← List.getElem_cons_drop ‹_›]
+    rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
     simp
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; simp
 

src/Init/Data/Array/Count.lean

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

src/Init/Data/Array/DecidableEq.lean

@@ -6,9 +6,11 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 public import Init.Data.BEq
 public import Init.Data.List.Nat.BEq
+public import Init.ByCases
 
 public section
 

src/Init/Data/Array/Erase.lean

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

src/Init/Data/Array/Extract.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.TakeDrop
 
 public section
 
@@ -289,6 +290,9 @@ theorem extract_append_right {as bs : Array α} :
   · simp only [size_extract, size_replicate] at h₁ h₂
     simp only [getElem_extract, getElem_replicate]
 
+@[deprecated extract_replicate (since := "2025-03-18")]
+abbrev extract_mkArray := @extract_replicate
+
 theorem extract_eq_extract_right {as : Array α} {i j j' : Nat} :
     as.extract i j = as.extract i j' ↔ min (j - i) (as.size - i) = min (j' - i) (as.size - i) := by
   rcases as with ⟨as⟩
@@ -426,20 +430,32 @@ theorem popWhile_append {xs ys : Array α} :
     (replicate n a).takeWhile p = (replicate n a).filter p := by
   simp [← List.toArray_replicate]
 
+@[deprecated takeWhile_replicate_eq_filter (since := "2025-03-18")]
+abbrev takeWhile_mkArray_eq_filter := @takeWhile_replicate_eq_filter
+
 theorem takeWhile_replicate {p : α → Bool} :
     (replicate n a).takeWhile p = if p a then replicate n a else #[] := by
   simp [takeWhile_replicate_eq_filter, filter_replicate]
 
+@[deprecated takeWhile_replicate (since := "2025-03-18")]
+abbrev takeWhile_mkArray := @takeWhile_replicate
+
 @[simp] theorem popWhile_replicate_eq_filter_not {p : α → Bool} :
     (replicate n a).popWhile p = (replicate n a).filter (fun a => !p a) := by
   simp [← List.toArray_replicate, ← List.filter_reverse]
 
+@[deprecated popWhile_replicate_eq_filter_not (since := "2025-03-18")]
+abbrev popWhile_mkArray_eq_filter_not := @popWhile_replicate_eq_filter_not
+
 theorem popWhile_replicate {p : α → Bool} :
     (replicate n a).popWhile p = if p a then #[] else replicate n a := by
   simp only [popWhile_replicate_eq_filter_not, size_replicate, filter_replicate, Bool.not_eq_eq_eq_not,
     Bool.not_true]
   split <;> simp_all
 
+@[deprecated popWhile_replicate (since := "2025-03-18")]
+abbrev popWhile_mkArray := @popWhile_replicate
+
 theorem extract_takeWhile {as : Array α} {i : Nat} :
     (as.takeWhile p).extract 0 i = (as.extract 0 i).takeWhile p := by
   rcases as with ⟨as⟩

src/Init/Data/Array/FinRange.lean

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

src/Init/Data/Array/Find.lean

@@ -7,7 +7,10 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Attach
 public import Init.Data.Array.Range
 
 public section
@@ -129,19 +132,31 @@ theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [← List.toArray_replicate, List.findSome?_replicate]
 
+@[deprecated findSome?_replicate (since := "2025-03-18")]
+abbrev findSome?_mkArray := @findSome?_replicate
+
 @[simp] theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a := by
   simp [findSome?_replicate, Nat.ne_of_gt h]
 
+@[deprecated findSome?_replicate_of_pos (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_pos := @findSome?_replicate_of_pos
+
 -- Argument is unused, but used to decide whether `simp` should unfold.
 @[simp] theorem findSome?_replicate_of_isSome (_ : (f a).isSome) :
    findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [findSome?_replicate]
 
+@[deprecated findSome?_replicate_of_isSome (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_isSome := @findSome?_replicate_of_isSome
+
 @[simp] theorem findSome?_replicate_of_isNone (h : (f a).isNone) :
     findSome? f (replicate n a) = none := by
   rw [Option.isNone_iff_eq_none] at h
   simp [findSome?_replicate, h]
 
+@[deprecated findSome?_replicate_of_isNone (since := "2025-03-18")]
+abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
+
 /-! ### find? -/
 
 @[simp, grind =] theorem find?_empty : find? p #[] = none := rfl
@@ -306,10 +321,16 @@ 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]
 
@@ -565,6 +586,9 @@ theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
   simp only [List.findIdx?_toArray]
   simp
 
+@[deprecated findIdx?_replicate (since := "2025-03-18")]
+abbrev findIdx?_mkArray := @findIdx?_replicate
+
 theorem findIdx?_eq_findSome?_zipIdx {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none := by
   rcases xs with ⟨xs⟩

src/Init/Data/Array/GetLit.lean

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

src/Init/Data/Array/InsertIdx.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -6,10 +6,17 @@ 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
@@ -245,13 +252,12 @@ 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 push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys := by
+theorem pop_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys := by
   cases xs
   cases ys
-  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
+  simp at h
+  replace h := List.append_inj_left' h (by simp)
+  simp [h]
 
 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]⟩
@@ -259,6 +265,15 @@ 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⟩
@@ -309,23 +324,41 @@ 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 ←]
@@ -809,11 +842,6 @@ 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⟩
 
@@ -1053,6 +1081,12 @@ 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
@@ -1073,6 +1107,9 @@ 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
@@ -1136,7 +1173,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 ‹_›]
+    · rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
       simp only [aux (i + 1), map_eq_pure_bind, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
@@ -1688,6 +1725,9 @@ 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
@@ -1850,9 +1890,6 @@ 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₁⟩
@@ -2053,22 +2090,11 @@ theorem append_eq_map_iff {f : α → β} :
   | nil => simp
   | cons as => induction as.toList <;> simp [*]
 
-@[simp] theorem flatten_toArray_map_toArray {L : List (List α)} :
+@[simp] theorem flatten_toArray_map {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
@@ -2115,33 +2141,32 @@ 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_toArray, List.flatten_eq_flatMap]
+  rw [flatten_toArray_map, 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_toArray, List.map_toArray, List.map_flatten, List.map_map,
+    simp only [flatten_toArray_map, List.map_toArray, List.map_flatten, List.map_map,
       Function.comp_def]
-    rw [← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
+    rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
 @[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_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 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, 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_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]
+  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]
 
 theorem flatten_filter_not_isEmpty {xss : Array (Array α)} :
     flatten (xss.filter fun xs => !xs.isEmpty) = xss.flatten := by
@@ -2164,23 +2189,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_toArray, List.append_toArray]
-  rw [this, ← List.map_append, flatten_toArray_map_toArray]
+  simp only [List.push_toArray, flatten_toArray_map, List.append_toArray]
+  rw [this, ← List.map_append, flatten_toArray_map]
   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_toArray]
+    rw [flatten_toArray_map]
     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_toArray, List.flatten_flatten, ← List.map_toArray, Array.map_map,
+    rw [this, flatten_toArray_map, 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_toArray]
-    rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
+    simp only [Function.comp_apply, flatten_toArray_map]
+    rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map]
 
 theorem flatten_eq_push_iff {xss : Array (Array α)} {ys : Array α} {y : α} :
     xss.flatten = ys.push y ↔
@@ -2189,13 +2214,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_toArray, List.push_toArray, mk.injEq, List.flatten_eq_append_iff]
+    rw [flatten_toArray_map, 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_toArray]; simpa⟩
+          by simpa using h₂, by rw [flatten_toArray_map]; simpa⟩
       · rw [List.singleton_eq_append_iff] at h
         obtain (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) := h
         · simp at h₁
@@ -2240,12 +2265,18 @@ 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⟩
@@ -2256,7 +2287,6 @@ 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]
@@ -2267,7 +2297,6 @@ 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
@@ -2368,44 +2397,77 @@ 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
 
@@ -2422,86 +2484,143 @@ 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 =]
@@ -2543,8 +2662,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_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₂)))]
+        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₂)))]
     · 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
@@ -2559,7 +2678,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_iff (n := xs.size - 1), this, Nat.zero_le,
+      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (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 ▸ ‹_›)]
 
@@ -2688,6 +2807,9 @@ 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
@@ -2707,8 +2829,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]
-      rw [extract_loop_succ (h := h), ih (ys := #[].push _), push_eq_append, empty_append]
+      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 [append_assoc]
     else
       rw [extract_loop_of_ge (h := Nat.le_of_not_lt h)]
@@ -3597,9 +3719,15 @@ 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 -/
@@ -3617,6 +3745,9 @@ 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]
@@ -3630,6 +3761,11 @@ 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
@@ -3689,6 +3825,9 @@ 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 -/
@@ -3918,10 +4057,16 @@ 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
@@ -4096,11 +4241,17 @@ 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 -/
@@ -4268,6 +4419,9 @@ 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) :
@@ -4279,7 +4433,6 @@ 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]
 
@@ -4299,7 +4452,6 @@ 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]
 
@@ -4318,6 +4470,12 @@ 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 α} :
@@ -4431,8 +4589,7 @@ theorem uset_toArray {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray
   apply ext'
   simp
 
-@[deprecated Array.flatten_map_toArray_toArray (since := "2025-10-26")]
-theorem flatten_toArray {L : List (List α)} :
+@[simp, grind =] 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,3 +8,5 @@ module
 prelude
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Lemmas
+
+public section

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

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

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

@@ -10,7 +10,9 @@ import all Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Lex
+import Init.Data.Range.Polymorphic.Lemmas
 import Init.Data.Range.Polymorphic.NatLemmas
+import Init.Data.Order.Lemmas
 
 public section
 
@@ -34,24 +36,14 @@ grind_pattern _root_.List.le_toArray => l₁.toArray ≤ l₂.toArray
 grind_pattern lt_toList => xs.toList < ys.toList
 grind_pattern le_toList => xs.toList ≤ ys.toList
 
-@[simp]
-protected theorem not_lt [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-
-@[deprecated Array.not_lt (since := "2025-10-26")]
 protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-
-@[simp]
-protected theorem not_le [LT α] {xs ys : Array α} :
-    ¬ xs ≤ ys ↔ ys < xs :=
-  Classical.not_not
-
-@[deprecated Array.not_le (since := "2025-10-26")]
 protected theorem not_le_iff_gt [LT α] {xs ys : Array α} :
     ¬ xs ≤ ys ↔ ys < xs :=
   Classical.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
-  simp [lex, Std.Rco.forIn'_eq_if]
+  rw [lex, Std.PRange.forIn'_eq_match]
+  simp [Std.PRange.SupportsUpperBound.IsSatisfied]
 
 private theorem cons_lex_cons.forIn'_congr_aux [Monad m] {as bs : ρ} {_ : Membership α ρ}
     [ForIn' m ρ α inferInstance] (w : as = bs)
@@ -72,13 +64,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.Rco.forIn'_eq_forIn'_toList]
+    Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.PRange.forIn'_eq_forIn'_toList]
   conv =>
     lhs; congr; congr
-    rw [cons_lex_cons.forIn'_congr_aux Std.Rco.toList_eq_if rfl (fun _ _ _ => rfl)]
-    simp only [bind_pure_comp, map_pure]
+    rw [cons_lex_cons.forIn'_congr_aux Std.PRange.toList_eq_match rfl (fun _ _ _ => rfl)]
+    simp only [Std.PRange.SupportsUpperBound.IsSatisfied, bind_pure_comp, map_pure]
     rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [Std.toList_Roo_eq_toList_Rco_of_isSome_succ? (lo := 0) (h := rfl),
+  simp only [Std.PRange.toList_Rox_eq_toList_Rcx_of_isSome_succ? (lo := 0) (h := rfl),
     Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.toList_Rco_succ_succ,
     Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil,
     Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero]
@@ -91,10 +83,16 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
   | nil =>
-    cases l₂ <;> simp [lex, Std.Rco.forIn'_eq_if]
+    cases l₂
+    · rw [lex, Std.PRange.forIn'_eq_match]
+      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
+    · rw [lex, Std.PRange.forIn'_eq_match]
+      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil => simp [lex, Std.Rco.forIn'_eq_if]
+    | nil =>
+      rw [lex, Std.PRange.forIn'_eq_match]
+      simp [Std.PRange.SupportsUpperBound.IsSatisfied]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 
@@ -189,6 +187,12 @@ protected theorem le_total [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)] (xs ys : Array α) : xs ≤ ys ∨ ys ≤ xs :=
   List.le_total xs.toList ys.toList
 
+@[simp] protected theorem not_lt [LT α]
+    {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+
+@[simp] protected theorem not_le [LT α]
+    {xs ys : Array α} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
+
 protected theorem le_of_lt [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} (h : xs < ys) : xs ≤ ys :=

src/Init/Data/Array/MapIdx.lean

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

src/Init/Data/Array/Mem.lean

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

src/Init/Data/Array/Monadic.lean

@@ -6,9 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Control
 import all Init.Data.List.Control
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Attach
+public import Init.Data.List.Monadic
 
 public section
 

src/Init/Data/Array/OfFn.lean

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

src/Init/Data/Array/Perm.lean

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

src/Init/Data/Array/QSort.lean

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

src/Init/Data/Array/Range.lean

@@ -6,10 +6,14 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.Array.Lemmas
+public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
+public import Init.Data.Array.OfFn
 import all Init.Data.Array.OfFn
 public import Init.Data.Array.MapIdx
 public import Init.Data.Array.Zip
+public import Init.Data.List.Nat.Range
 
 public section
 

src/Init/Data/Array/Subarray.lean

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

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

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

src/Init/Data/Array/TakeDrop.lean

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

src/Init/Data/Array/Zip.lean

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

src/Init/Data/Basic.lean

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

src/Init/Data/BitVec.lean

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

src/Init/Data/BitVec/Basic.lean

@@ -6,8 +6,11 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
+public import Init.Data.Fin.Basic
 public import Init.Data.Nat.Bitwise.Lemmas
+public import Init.Data.Nat.Power2
 public import Init.Data.Int.Bitwise.Basic
+public import Init.Data.BitVec.BasicAux
 
 @[expose] public section
 
@@ -203,8 +206,8 @@ If `n` is `0`, then one digit is returned. Otherwise, `⌊(n + 3) / 4⌋` digits
 -- `Internal` string functions by moving this definition out to a separate file that can live
 -- downstream of `Init.Data.String.Basic`.
 protected def toHex {n : Nat} (x : BitVec n) : String :=
-  let s := String.ofList (Nat.toDigits 16 x.toNat)
-  let t := String.ofList (List.replicate ((n+3) / 4 - String.Internal.length s) '0')
+  let s := (Nat.toDigits 16 x.toNat).asString
+  let t := (List.replicate ((n+3) / 4 - String.Internal.length s) '0').asString
   String.Internal.append t s
 
 /-- `BitVec` representation. -/

src/Init/Data/BitVec/Bitblast.lean

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

src/Init/Data/BitVec/Bootstrap.lean

@@ -9,7 +9,6 @@ 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,7 +8,6 @@ module
 
 prelude
 public import Init.Data.BitVec.Bootstrap
-import Init.Ext
 
 public section
 
@@ -50,11 +49,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) (by exact Classical.not_forall_not)
+  decidable_of_iff (¬ ∀ v, ¬ P v) 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) (by exact Classical.not_forall_not)
+  decidable_of_iff (¬ ∀ v, ¬ P v) 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,8 +6,10 @@ 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
@@ -82,7 +84,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_iff.mp i.isLt)) with
+      cases (Nat.lt_or_eq_of_le (Nat.lt_succ.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,14 +6,22 @@ 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.List.BasicAux
-import Init.Data.List.Lemmas
+public import Init.Data.Order.Factories
 
 public section
 
@@ -34,6 +42,14 @@ 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]
@@ -64,7 +80,6 @@ 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) :
@@ -133,6 +148,9 @@ 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]
@@ -159,13 +177,18 @@ theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i <
     apply getLsbD_of_ge
     omega
 
-@[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] 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
@@ -188,6 +211,18 @@ 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]
@@ -417,18 +452,12 @@ 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_ite]
+  simp only [ofBool, ofNat_eq_ofNat, cond_eq_if]
   split <;> simp_all
 
-@[simp, grind =]
-theorem getElem_ofBool_zero {b : Bool} : (ofBool b)[0] = b := by
+@[simp, grind =] theorem getElem_zero_ofBool (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
 
@@ -439,6 +468,8 @@ 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]
@@ -521,10 +552,6 @@ 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) :
@@ -586,7 +613,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_eq_emod_of_lt] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
+    rw [Int.bmod_pos] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
     omega
   next g =>
     rw [Int.bmod_neg] <;> simp only [←Int.natCast_emod, toNat_mod_cancel]
@@ -994,14 +1021,7 @@ 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
@@ -1017,6 +1037,12 @@ 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]
@@ -1190,7 +1216,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_iff]
+  simp [getLsbD, Nat.lt_succ]
 
 @[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
@@ -1646,11 +1672,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_natCast, toNat_eq, toNat_ofNatLT, toNat_not,
+  simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLT, toNat_not,
     toNat_ofNat]
   cases h : Int.negSucc n % ((2 ^ w : Nat) : Int)
   case ofNat =>
-    rw [Int.ofNat_eq_natCast, Int.negSucc_emod] at h
+    rw [Int.ofNat_eq_coe, Int.negSucc_emod] at h
     · dsimp only
       omega
     · omega
@@ -1732,6 +1758,9 @@ 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]
 
@@ -2551,6 +2580,10 @@ 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]
@@ -3610,6 +3643,9 @@ 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]
@@ -3649,6 +3685,10 @@ 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]
@@ -3710,9 +3750,6 @@ 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]
@@ -4065,7 +4102,6 @@ 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)
@@ -4082,7 +4118,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 := BitVec.not_lt.mp not_lt_zero
+    have : x ≥ 0 := not_lt_iff_le.mp not_lt_zero
     exact Eq.symm (BitVec.le_antisymm this h)
   · simp_all
 
@@ -4105,7 +4141,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 := BitVec.not_lt.mp not_allOnes_lt
+    have : x ≤ allOnes w := not_lt_iff_le.mp not_allOnes_lt
     exact Eq.symm (BitVec.le_antisymm h this)
   · simp_all
 
@@ -4651,6 +4687,9 @@ 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]
@@ -4721,6 +4760,14 @@ 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 =
@@ -4877,6 +4924,14 @@ 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,11 +111,35 @@ 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
@@ -145,11 +169,35 @@ 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⟩
 
@@ -514,7 +562,6 @@ 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
@@ -574,6 +621,11 @@ 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]
 
@@ -613,7 +665,7 @@ theorem decide_beq_decide (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidab
 
 end Bool
 
-export Bool (cond_eq_if cond_eq_ite xor and or not)
+export Bool (cond_eq_if xor and or not)
 
 /-! ### decide -/
 

src/Init/Data/ByteArray.lean

@@ -10,3 +10,5 @@ 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,12 +6,13 @@ 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
 
@@ -24,46 +25,27 @@ 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]
@@ -74,65 +56,37 @@ 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", inherit_doc ByteArray.set]
+@[extern "lean_byte_array_uset"]
 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
 
 /--
-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.
--/
+  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. -/
 @[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
@@ -159,9 +113,6 @@ 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
@@ -172,12 +123,16 @@ def toList (bs : ByteArray) : List UInt8 :=
     decreasing_by decreasing_trivial_pre_omega
   loop 0 []
 
-/--
-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`.
+@[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
 
-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
@@ -189,29 +144,11 @@ The index is returned along with a proof that it is a valid index in the array.
   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`.
+  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.
 
-The variant {name}`findFinIdx?` additionally returns a proof that the found index is in bounds.
+  TODO: avoid code duplication in the future after we improve the compiler.
 -/
-@[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
@@ -224,11 +161,7 @@ We claim this unsafe implementation is correct because an array cannot have more
       pure b
   loop 0 b
 
-/--
-The reference implementation of {name}`ForIn.forIn` for {name}`ByteArray`.
-
-In compiled code, this is replaced by the more efficient {name}`ByteArray.forInUnsafe`.
--/
+/-- Reference implementation for `forIn` -/
 @[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
@@ -246,13 +179,7 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr
 instance : ForIn m ByteArray UInt8 where
   forIn := ByteArray.forIn
 
-/--
-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.
--/
+/-- See comment at `forInUnsafe` -/
 -- 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 β :=
@@ -269,14 +196,7 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β
   else
     pure init
 
-/--
-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.
--/
+/-- Reference implementation for `foldlM` -/
 @[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) :=
@@ -294,23 +214,11 @@ 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
 
-set_option doc.verso false -- Awaiting intra-module forward reference support
-/--
-Iterator over the bytes (`UInt8`) of a `ByteArray`.
+/-- Iterator over the bytes (`UInt8`) of a `ByteArray`.
 
 Typically created by `arr.iter`, where `arr` is a `ByteArray`.
 
@@ -334,7 +242,6 @@ 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 :=
@@ -352,25 +259,16 @@ theorem Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx :=
 
 namespace Iterator
 
-/--
-The number of bytes remaining in the iterator.
--/
+/-- Number of bytes remaining in the iterator. -/
 def remainingBytes : Iterator → Nat
   | ⟨arr, i⟩ => arr.size - i
 
 @[inherit_doc Iterator.idx]
 def pos := Iterator.idx
 
-/-- True if the iterator is past the array's last byte. -/
-@[inline]
-def atEnd : Iterator → Bool
-  | ⟨arr, i⟩ => i ≥ arr.size
+/-- The byte at the current position.
 
-/--
-The byte at the current position.
-
-On an invalid position, returns {lean}`(default : UInt8)`.
--/
+On an invalid position, returns `(default : UInt8)`. -/
 @[inline]
 def curr : Iterator → UInt8
   | ⟨arr, i⟩ =>
@@ -379,28 +277,27 @@ 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.*
-{name}`Iterator.atEnd` is {name}`false`; otherwise, the resulting iterator will be invalid.
--/
+`Iterator.atEnd` is `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 valid; that is, it is not past the array's last byte.
--/
+/-- 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. -/
 @[inline]
 def hasNext : Iterator → Bool
   | ⟨arr, i⟩ => i < arr.size
@@ -426,21 +323,17 @@ 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.
 
-Given {given}`i : ByteArray.Iterator`, note that {lean}`i.toEnd.atEnd` is always {name}`true`.
--/
+Note that `i.toEnd.atEnd` is always `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⟩
@@ -448,11 +341,9 @@ 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,22 +6,16 @@ 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,13 +9,7 @@ prelude
 public import Init.Data.ByteArray.Basic
 import Init.Data.String.Basic
 
-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.
--/
+/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
 public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 7).toUInt64 <<< 0x38 |||
@@ -27,11 +21,7 @@ public def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
   (bs.get! 1).toUInt64 <<< 0x8  |||
   (bs.get! 0).toUInt64
 
-/--
-Interprets a {name}`ByteArray` of size 8 as a big-endian {name}`UInt64`.
-
-Panics if the array's size is not 8.
--/
+/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
 public def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
   assert! bs.size == 8
   (bs.get! 0).toUInt64 <<< 0x38 |||

src/Init/Data/ByteArray/Lemmas.lean

@@ -7,11 +7,10 @@ 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
@@ -20,10 +19,10 @@ theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl
 theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl
 
 @[simp]
-theorem data_empty : ByteArray.empty.data = #[] := rfl
+theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
 
 @[simp]
-theorem data_extract {a : ByteArray} {b e : Nat} :
+theorem ByteArray.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
@@ -31,39 +30,39 @@ theorem 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 extract_zero_size {b : ByteArray} : b.extract 0 b.size = b := by
+theorem ByteArray.extract_zero_size {b : ByteArray} : b.extract 0 b.size = b := by
   ext1
   simp
 
 @[simp]
-theorem extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by
+theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by
   ext1
   simp [Nat.min_le_left]
 
-theorem fastAppend_eq_copySlice {a b : ByteArray} :
+theorem ByteArray.fastAppend_eq_copySlice {a b : ByteArray} :
   a.fastAppend b = b.copySlice 0 a a.size b.size false := rfl
 
 @[simp]
-theorem _root_.List.toByteArray_append {l l' : List UInt8} :
+theorem List.toByteArray_append {l l' : List UInt8} :
     (l ++ l').toByteArray = l.toByteArray ++ l'.toByteArray := by
   simp [List.toByteArray_append']
 
 @[simp]
-theorem toList_data_append {l l' : ByteArray} :
+theorem ByteArray.toList_data_append {l l' : ByteArray} :
     (l ++ l').data.toList = l.data.toList ++ l'.data.toList := by
   simp [← append_eq]
 
 @[simp]
-theorem data_append {l l' : ByteArray} :
+theorem ByteArray.data_append {l l' : ByteArray} :
     (l ++ l').data = l.data ++ l'.data := by
   simp [← Array.toList_inj]
 
 @[simp]
-theorem size_empty : ByteArray.empty.size = 0 := by
+theorem ByteArray.size_empty : ByteArray.empty.size = 0 := by
   simp [← ByteArray.size_data]
 
 @[simp]
-theorem _root_.List.data_toByteArray {l : List UInt8} :
+theorem 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
@@ -72,159 +71,153 @@ theorem _root_.List.data_toByteArray {l : List UInt8} :
   fun_induction List.toByteArray.loop a b with simp_all
 
 @[simp]
-theorem _root_.List.size_toByteArray {l : List UInt8} :
+theorem List.size_toByteArray {l : List UInt8} :
     l.toByteArray.size = l.length := by
   simp [← ByteArray.size_data]
 
 @[simp]
-theorem _root_.List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl
+theorem List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl
 
 @[simp]
-theorem empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by
+theorem ByteArray.empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by
   ext1
   simp
 
 @[simp]
-theorem append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
+theorem ByteArray.append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
   ext1
   simp
 
 @[simp, grind =]
-theorem size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size := by
+theorem ByteArray.size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size := by
   simp [← size_data]
 
 @[simp]
-theorem size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by
+theorem ByteArray.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 getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
+theorem ByteArray.getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
     a[i] = a.data[i]'(by simpa [← size_data]) := rfl
 
 @[simp]
-theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
+theorem ByteArray.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 getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
+theorem ByteArray.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 _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} :
+theorem 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 _root_.List.getElem_eq_getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.length} :
+theorem 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 size_extract {a : ByteArray} {b e : Nat} :
+theorem ByteArray.size_extract {a : ByteArray} {b e : Nat} :
     (a.extract b e).size = min e a.size - b := by
   simp [← size_data]
 
 @[simp]
-theorem extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by
+theorem ByteArray.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 extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by
+theorem ByteArray.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 append_eq_empty_iff {a b : ByteArray} :
+theorem ByteArray.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 toByteArray_eq_empty {l : List UInt8} :
+theorem List.toByteArray_eq_empty {l : List UInt8} :
     l.toByteArray = ByteArray.empty ↔ l = [] := by
   simp [← ByteArray.size_eq_zero_iff]
 
-@[simp]
-theorem append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) :
+theorem ByteArray.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 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} :
+theorem ByteArray.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 extract_eq_extract_append_extract {a : ByteArray} {i k : Nat} (j : Nat)
+theorem ByteArray.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 append_inj_left {xs₁ xs₂ ys₁ ys₂ : ByteArray} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂ := by
+theorem ByteArray.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 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
+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
   ext1
   simp [← size_data]
 
-theorem extract_append_eq_left {a b : ByteArray} {i : Nat} (hi : i = a.size) :
+theorem ByteArray.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 extract_append_size_left {a b : ByteArray} {i : Nat} :
+theorem ByteArray.extract_append_size_left {a b : ByteArray} {i : Nat} :
     (a ++ b).extract i a.size = a.extract i a.size := by
   ext1
   simp
 
-theorem extract_append_size_add {a b : ByteArray} {i j : Nat} :
+theorem ByteArray.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 extract_append  {as bs : ByteArray} {i j : Nat} :
+theorem ByteArray.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 extract_append_size_add' {a b : ByteArray} {i j k : Nat} (h : k = a.size) :
+theorem ByteArray.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 extract_extract {a : ByteArray} {i j k l : Nat} :
+theorem ByteArray.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 getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.extract start stop).size) :
+theorem ByteArray.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 getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat}
+theorem ByteArray.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 extract_eq_extract_left {a : ByteArray} {i i' j : Nat} :
+theorem ByteArray.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 extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
+theorem ByteArray.extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
     a.extract i (i + 1) = [a[i]].toByteArray := by
   ext
   · simp
@@ -233,57 +226,34 @@ theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
     obtain rfl : j = 0 := by simpa using hj'
     simp [ByteArray.getElem_eq_getElem_data]
 
-theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) :
+theorem ByteArray.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 extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) :
+theorem ByteArray.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 extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) :
+theorem ByteArray.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 append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by
+theorem ByteArray.append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by
   ext1
   simp
 
 @[simp]
-theorem toList_empty : ByteArray.empty.toList = [] := by
+theorem ByteArray.toList_empty : ByteArray.empty.toList = [] := by
   simp [ByteArray.toList, ByteArray.toList.loop]
 
-theorem copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} :
+theorem ByteArray.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,3 +9,5 @@ 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,6 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Char.Basic
 import all Init.Data.Char.Basic
 public import Init.Data.UInt.Lemmas
 
@@ -13,16 +14,12 @@ public section
 
 namespace Char
 
-@[deprecated Char.ext (since := "2025-10-26")]
-protected theorem eq_of_val_eq : {a b : Char} → a.val = b.val → a = b
+@[ext] protected theorem ext : {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]
@@ -73,9 +70,4 @@ 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.Hints
+import Init.Data.Int.DivMod.Lemmas
 
 /-!
 # 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_natCast, Int.add_shiftLeft, ← Int.shiftLeft_add,
+      simp only [succ_eq_add_one, Int.ofNat_eq_coe, 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_natCast, Int.toNat_natCast, Int.toNat_neg_natCast,
+  · simp only [Rat.toDyadic, Int.ofNat_eq_coe, 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_natCast, Int.toNat_natCast, Int.toNat_neg_natCast, Nat.pow_zero,
+    simp only [Int.ofNat_eq_coe, 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.natCast_nonneg _)]
+    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
       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.natCast_nonneg _)]
+    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       · simp
@@ -682,11 +682,9 @@ instance : LE Dyadic where
 instance : DecidableLT Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
 instance : DecidableLE Dyadic := fun _ _ => inferInstanceAs (Decidable (_ = true))
 
-@[simp]
-theorem toRat_lt_toRat_iff {x y : Dyadic} : x.toRat < y.toRat ↔ x < y := blt_iff_toRat.symm
+theorem lt_iff_toRat {x y : Dyadic} : x < y ↔ x.toRat < y.toRat := blt_iff_toRat
 
-@[simp]
-theorem toRat_le_toRat_iff {x y : Dyadic} : x.toRat ≤ y.toRat ↔ x ≤ y := ble_iff_toRat.symm
+theorem le_iff_toRat {x y : Dyadic} : x ≤ y ↔ x.toRat ≤ y.toRat := ble_iff_toRat
 
 @[simp]
 protected theorem not_le {x y : Dyadic} : ¬x < y ↔ y ≤ x := by
@@ -698,20 +696,20 @@ protected theorem not_lt {x y : Dyadic} : ¬x ≤ y ↔ y < x := by
 
 @[simp]
 protected theorem le_refl (x : Dyadic) : x ≤ x := by
-  rw [← toRat_le_toRat_iff]
+  rw [le_iff_toRat]
   exact Rat.le_refl
 
 protected theorem le_trans {x y z : Dyadic} (h : x ≤ y) (h' : y ≤ z) : x ≤ z := by
-  rw [← toRat_le_toRat_iff] at h h' ⊢
+  rw [le_iff_toRat] 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 [← toRat_le_toRat_iff] at h h'
+  rw [le_iff_toRat] 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 [← toRat_le_toRat_iff, ← toRat_le_toRat_iff]
+  rw [le_iff_toRat, le_iff_toRat]
   exact Rat.le_total
 
 instance : Std.LawfulOrderLT Dyadic where

src/Init/Data/Dyadic/Instances.lean

@@ -7,6 +7,7 @@ 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`. -/
@@ -52,8 +53,8 @@ instance : NoNatZeroDivisors Dyadic where
 
 instance : OrderedRing Dyadic where
   zero_lt_one := by decide
-  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
+  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
 
 end Dyadic

src/Init/Data/Dyadic/Inv.lean

@@ -5,6 +5,7 @@ Authors: Kim Morrison
 -/
 module
 prelude
+import Init.Data.Dyadic.Basic
 import Init.Data.Dyadic.Round
 import Init.Grind.Ordered.Ring
 
@@ -27,7 +28,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 [← toRat_le_toRat_iff]
+  rw [le_iff_toRat]
   rw [toRat_mul]
   rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
   unfold invAtPrec
@@ -39,19 +40,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 [← toRat_lt_toRat_iff, toRat_zero] at hx
+      rw [lt_iff_toRat, 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 [← toRat_lt_toRat_iff, toRat_zero] at hx
+        rw [lt_iff_toRat, 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 [← toRat_lt_toRat_iff]
+  rw [lt_iff_toRat]
   rw [toRat_mul]
   rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
   unfold invAtPrec
@@ -64,12 +65,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 [← toRat_lt_toRat_iff, toRat_zero] at hx
+      rwa [lt_iff_toRat, 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 [← toRat_lt_toRat_iff, toRat_zero] at hx
+        rw [lt_iff_toRat, 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,6 +8,7 @@ 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
 
@@ -28,7 +29,7 @@ theorem roundDown_le {x : Dyadic} {prec : Int} : roundDown x prec ≤ x :=
     match h : k - prec with
     | .ofNat l =>
       dsimp
-      rw [ofOdd_eq_ofIntWithPrec, ← toRat_le_toRat_iff]
+      rw [ofOdd_eq_ofIntWithPrec, le_iff_toRat]
       replace h : k = Int.ofNat l + prec := by omega
       subst h
       simp only [toRat_ofIntWithPrec_eq_mul_two_pow]
@@ -36,7 +37,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_natCast]
+      simp only [Int.natCast_pow, Int.cast_ofNat_Int, Int.ofNat_eq_coe]
       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,3 +11,5 @@ 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, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a % b,  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, by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨a / b, 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, by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
+  | ⟨a, h⟩, m => ⟨a % m, Nat.lt_of_le_of_lt (Nat.mod_le _ _) h⟩
 
 /--
 Bitwise and.