feat: add @[grind ext] attributes for extensional maps

This PR ensures that `grind +premises` silently drops warnings and
errors about bad suggestions.

.claude/commands/release.md

@@ -16,14 +16,26 @@ These comments explain the scripts' behavior, which repositories get special han
 ## Process
 
 1. Run `script/release_checklist.py {version}` to check the current status
-2. Create a todo list tracking all repositories that need updates
-3. For each repository that needs updating:
+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
-4. After creating PRs, notify the user which PRs need review and merging
-5. Continuously rerun `script/release_checklist.py {version}` to check progress
-6. As PRs are merged, dependent repositories will become ready - create PRs for those as well
-7. Continue until all repositories are updated and the release is complete
+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
 

.github/workflows/build-template.yml

@@ -3,9 +3,6 @@ name: build-template
 on:
   workflow_call:
     inputs:
-      check-level:
-        type: string
-        required: true
       config:
         type: string
         required: true
@@ -230,7 +227,7 @@ jobs:
         run: |
           ulimit -c unlimited  # coredumps
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTEST_OPTIONS }}
-        if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
+        if: matrix.test
       - name: Test Summary
         uses: test-summary/action@v2
         with:

.github/workflows/check-stage0.yml

@@ -11,8 +11,8 @@ jobs:
     - uses: actions/checkout@v5
       with:
         ref: ${{ github.event.pull_request.head.sha }}
-        filter: blob:none
         fetch-depth: 0
+        filter: tree:0
 
     - name: Find base commit
       if: github.event_name == 'pull_request'

.github/workflows/ci.yml

@@ -31,10 +31,6 @@ jobs:
   configure:
     runs-on: ubuntu-latest
     outputs:
-      # 0: PRs without special label
-      # 1: PRs with `merge-ci` label, merge queue checks, master commits
-      # 2: PRs with `release-ci` label, releases (incl. nightlies)
-      check-level: ${{ steps.set-level.outputs.check-level }}
       # The build matrix, dynamically generated here
       matrix: ${{ steps.set-matrix.outputs.matrix }}
       # secondary build jobs that should not block the CI success/merge queue
@@ -110,6 +106,9 @@ jobs:
           TAG_NAME="${GITHUB_REF##*/}"
           echo "RELEASE_TAG=$TAG_NAME" >> "$GITHUB_OUTPUT"
 
+      # 0: PRs without special label
+      # 1: PRs with `merge-ci` label, merge queue checks, master commits
+      # 2: PRs with `release-ci` label, releases (incl. nightlies)
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -117,6 +116,7 @@ jobs:
         # rerun the workflow run after setting the `release-ci`/`merge-ci` labels.
         run: |
           check_level=0
+          fast=false
 
           if [[ -n "${{ steps.set-nightly.outputs.nightly }}" || -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=2
@@ -129,9 +129,13 @@ 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 }}
 
@@ -141,7 +145,8 @@ jobs:
         with:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
-            console.log(`level: ${level}`);
+            const fast = ${{ steps.set-level.outputs.fast }};
+            console.log(`level: ${level}, fast: ${fast}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
             const isPr = "${{ github.event_name }}" == "pull_request";
@@ -152,7 +157,8 @@ jobs:
                 "name": "Linux LLVM",
                 "os": "ubuntu-latest",
                 "release": false,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -165,17 +171,19 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                "os": "ubuntu-latest",
+                // usually not a bottleneck so make exclusive to `fast-ci`
+                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary is sufficient)
+                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
                 // 2. To skip it in merge queues as it takes longer than the
                 //    Linux lake build and adds little value in the merge queue
                 // 3. To run it in release (obviously)
                 // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
                 //    available as an artifact for Grove to use.
-                "check-level": (isPr || isPushToMaster) ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1 || isPushToMaster,
+                "test": level >= 1,
+                "secondary": level == 0,
                 "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -186,27 +194,28 @@ jobs:
               {
                 "name": "Linux Lake",
                 "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "check-level": 0,
+                "enabled": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
-                // only check-level >= 1 opts into tests implicitly. TODO: Clean up this logic.
                 "test": true,
                 // NOTE: `test-speedcenter` currently seems to be broken on `ubuntu-latest`
                 "test-speedcenter": large && level >= 2,
-                // made explicit until it can be assumed to have propagated to PRs
-                "CMAKE_OPTIONS": "-DUSE_LAKE=ON",
+                // We are not warning-free yet on all platforms, start here
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
               },
               {
                 "name": "Linux Reldebug",
                 "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "CMAKE_PRESET": "reldebug",
               },
               // TODO: suddenly started failing in CI
               /*{
                 "name": "Linux fsanitize",
                 "os": "ubuntu-latest",
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 // turn off custom allocator & symbolic functions to make LSAN do its magic
                 "CMAKE_PRESET": "sanitize",
                 // exclude seriously slow/problematic tests (laketests crash)
@@ -217,7 +226,7 @@ jobs:
                 "os": "macos-15-intel",
                 "release": true,
                 "test": false,  // Tier 2 platform
-                "check-level": 2,
+                "enabled": level >= 2,
                 "shell": "bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-apple-darwin.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
@@ -228,7 +237,7 @@ jobs:
               {
                 "name": "macOS aarch64",
                 // standard GH runner only comes with 7GB so use large runner if possible when running tests
-                "os": large && !isPr ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
+                "os": large && (fast || level >= 1) ? "nscloud-macos-sequoia-arm64-6x14" : "macos-15",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-darwin_aarch64",
                 "release": true,
                 "shell": "bash -euxo pipefail {0}",
@@ -237,14 +246,16 @@ jobs:
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
                 // See "Linux release" for release job levels; Grove is not a concern here
-                "check-level": isPr ? 0 : 2,
-                "secondary": isPr,
+                "enabled": isPr || level != 1,
+                "test": level >= 1,
+                "secondary": level == 0,
               },
               {
                 "name": "Windows",
-                "os": large && level == 2 ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
+                "os": large && (fast || level == 2) ? "namespace-profile-windows-amd64-4x16" : "windows-2022",
                 "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\"",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
@@ -256,7 +267,8 @@ jobs:
                 "os": "nscloud-ubuntu-22.04-arm64-4x16",
                 "CMAKE_OPTIONS": "-DLEAN_INSTALL_SUFFIX=-linux_aarch64",
                 "release": true,
-                "check-level": 2,
+                "enabled": level >= 2,
+                "test": true,
                 "shell": "nix develop .#oldGlibcAArch -c bash -euxo pipefail {0}",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/19.1.2/lean-llvm-aarch64-linux-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
@@ -269,7 +281,7 @@ jobs:
               //  "CMAKE_OPTIONS": "-DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_MMAP=OFF -DUSE_GMP=OFF -DLEAN_EXTRA_CXX_FLAGS='-m32' -DLEANC_OPTS='-m32' -DMMAP=OFF -DLEAN_INSTALL_SUFFIX=-linux_x86 -DCMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/ -DPKG_CONFIG_EXECUTABLE=/usr/bin/i386-linux-gnu-pkg-config",
               //  "cmultilib": true,
               //  "release": true,
-              //  "check-level": 2,
+              //  "enabled": level >= 2,
               //  "cross": true,
               //  "shell": "bash -euxo pipefail {0}"
               //}
@@ -281,7 +293,7 @@ jobs:
               //   "wasm": true,
               //   "cmultilib": true,
               //   "release": true,
-              //   "check-level": 2,
+              //   "enabled": level >= 2,
               //   "cross": true,
               //   "shell": "bash -euxo pipefail {0}",
               //   // Just a few selected tests because wasm is slow
@@ -295,7 +307,7 @@ jobs:
               }
             }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
-            matrix = matrix.filter((job) => level >= job["check-level"]);
+            matrix = matrix.filter((job) => job["enabled"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));
             core.setOutput('matrix-secondary', matrix.filter((job) => job["secondary"]));
 
@@ -305,7 +317,6 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix}}
-      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -321,7 +332,6 @@ jobs:
     uses: ./.github/workflows/build-template.yml
     with:
       config: ${{needs.configure.outputs.matrix-secondary}}
-      check-level: ${{ needs.configure.outputs.check-level }}
       nightly: ${{ needs.configure.outputs.nightly }}
       LEAN_VERSION_MAJOR: ${{ needs.configure.outputs.LEAN_VERSION_MAJOR }}
       LEAN_VERSION_MINOR: ${{ needs.configure.outputs.LEAN_VERSION_MINOR }}
@@ -394,6 +404,8 @@ jobs:
         with:
           # needed for tagging
           fetch-depth: 0
+          # Doesn't seem to be working when additionally fetching from lean4-nightly
+          #filter: tree:0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
       - uses: actions/download-artifact@v5
         with:

.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}"
@@ -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"
@@ -401,6 +401,7 @@ jobs:
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0
 
       - name: Check if tag exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
@@ -460,6 +461,7 @@ jobs:
           token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0
 
       - name: install elan
         run: |
@@ -530,6 +532,7 @@ jobs:
           token: ${{ secrets.MANUAL_PR_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
+          filter: tree:0
 
       - name: Check if tag in reference manual exists
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'

.gitignore

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

doc/dev/ffi.md

@@ -52,7 +52,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
   Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
 * `Nat` and `Int` are represented by `lean_object *`.
   Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
-* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
+* A universe `Sort u`, type constructor `... → Sort u`, `Void α` or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
 * Any other type is represented by `lean_object *`.
   Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
 
@@ -141,8 +141,8 @@ void lean_initialize_runtime_module();
 void lean_initialize();
 char ** lean_setup_args(int argc, char ** argv);
 
-lean_object * initialize_A_B(uint8_t builtin, lean_object *);
-lean_object * initialize_C(uint8_t builtin, lean_object *);
+lean_object * initialize_A_B(uint8_t builtin);
+lean_object * initialize_C(uint8_t builtin);
 ...
 
 argv = lean_setup_args(argc, argv); // if using process-related functionality
@@ -152,7 +152,7 @@ lean_initialize_runtime_module();
 lean_object * res;
 // use same default as for Lean executables
 uint8_t builtin = 1;
-res = initialize_A_B(builtin, lean_io_mk_world());
+res = initialize_A_B(builtin);
 if (lean_io_result_is_ok(res)) {
     lean_dec_ref(res);
 } else {
@@ -160,7 +160,7 @@ if (lean_io_result_is_ok(res)) {
     lean_dec(res);
     return ...;  // do not access Lean declarations if initialization failed
 }
-res = initialize_C(builtin, lean_io_mk_world());
+res = initialize_C(builtin);
 if (lean_io_result_is_ok(res)) {
 ...
 

lean.code-workspace

@@ -15,7 +15,8 @@
 	],
 	"settings": {
 		// Open terminal at root, not current workspace folder
-		"terminal.integrated.cwd": "${workspaceFolder:.}",
+		// (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

@@ -57,19 +57,19 @@ def main (args : List String) : IO Unit := do
         sec := "\n\n" ++ sec
       if insertPos?.isNone then
         sec := sec ++ "\n\n"
-      text := text.extract 0 insertPos ++ sec ++ text.extract insertPos text.endPos
+      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.endPos
+      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.endPos
+    text := initText ++ "module\n\n" ++ text.extract startPos text.rawEndPos
 
     IO.FS.writeFile path text

script/Shake.lean

@@ -131,10 +131,11 @@ structure State where
   `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)->+ -(public import ...)-> _ -(public import)->* j`
-  * `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 all)->+ -(public meta import ...)-> _ -(public (meta)? 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 := #[]
   /--
@@ -162,10 +163,10 @@ def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps
     -- `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)->+ -(public import ...)-> _ -(public import)->* j`
-      transImps := transImps.union .priv (impTransImps.get .pub)
+      -- `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`
+  -- `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
@@ -173,10 +174,13 @@ def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps
 
   if !imp.isExported then
     if imp.isMeta then
-      -- `j ∈ transDeps[i].metaPriv` if `i -(meta import ...)-> _ -(public (meta)? import ...)->* j`
+      -- `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)->+ -(public meta import ...)-> _ -(public (meta)? import ...)->* j`
+      -- `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
@@ -185,7 +189,8 @@ def addTransitiveImps (transImps : Needs) (imp : Import) (j : Nat) (impTransImps
 def calcNeeds (env : Environment) (i : ModuleIdx) : Needs := Id.run do
   let mut needs := default
   for ci in env.header.moduleData[i]!.constants do
-    let pubCI? := env.setExporting true |>.find? ci.name
+    -- 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
@@ -216,7 +221,8 @@ 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
-    let pubCI? := env.setExporting true |>.find? ci.name
+    -- 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
@@ -286,7 +292,7 @@ and `endPos` is the position of the end of the header.
 -/
 def parseHeaderFromString (text path : String) :
     IO (System.FilePath × Parser.InputContext ×
-      TSyntaxArray ``Parser.Module.import × String.Pos) := do
+      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
@@ -294,8 +300,8 @@ def parseHeaderFromString (text path : String) :
     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 + ⟨1⟩
-  pure (path, inputCtx, .mk header.raw[2].getArgs, insertion)
+  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.
 
@@ -304,13 +310,18 @@ and `endPos` is the position of the end of the header.
 -/
 def parseHeader (srcSearchPath : SearchPath) (mod : Name) :
     IO (System.FilePath × Parser.InputContext ×
-      TSyntaxArray ``Parser.Module.import × String.Pos) := do
+      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 }
@@ -326,11 +337,20 @@ def decodeImport : TSyntax ``Parser.Module.import → Import
 * `addOnly`: if true, only add missing imports, do not remove unused ones
 -/
 def visitModule (srcSearchPath : SearchPath)
-    (i : Nat) (needs : Needs) (preserve : Needs) (edits : Edits)
+    (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
@@ -354,7 +374,8 @@ def visitModule (srcSearchPath : SearchPath)
       newDeps := addTransitiveImps newDeps imp j s.transDeps[j]!
     else
       let k := NeedsKind.ofImport imp
-      if !addOnly && !deps.has k j && !deps.has { k with isExported := false } j then
+      -- 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]!
@@ -385,7 +406,8 @@ def visitModule (srcSearchPath : SearchPath)
 
   if githubStyle then
     try
-      let (path, inputCtx, imports, endHeader) ← parseHeader srcSearchPath s.modNames[i]!
+      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!
@@ -529,33 +551,43 @@ def main (args : List String) : IO UInt32 := do
   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 do
-    edits ← visitModule (addOnly := !pkg.isPrefixOf s.modNames[i]!) srcSearchPath i t.get revNeeds edits args.githubStyle args.explain
-    if isExtraRevModUse s.env i then
-      revNeeds := revNeeds.union .priv {i}
+  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 count ← edits.foldM (init := 0) fun count mod (remove, add) => do
+  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 (path, inputCtx, imports, insertion) ←
-      try parseHeader srcSearchPath mod
-      catch e => println! e.toString; return count
+    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 := 0
+    let mut pos : String.Pos.Raw := 0
     let mut out : String := ""
     let mut seen : Std.HashSet Import := {}
     for stx in imports do
@@ -563,17 +595,17 @@ def main (args : List String) : IO UInt32 := do
       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.endPos stx.raw.getTailPos?.get! + ⟨1⟩
+        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.endPos
+    out := out ++ text.extract insertion text.rawEndPos
 
     IO.FS.writeFile path out
-    return count + 1
+    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.

script/release_checklist.py

@@ -13,8 +13,15 @@ What this script does:
    - 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
-   - Checks the release notes page on lean-lang.org
+   - 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)
@@ -122,6 +129,39 @@ def release_page_exists(repo_url, tag_name, github_token):
     response = requests.get(api_url, headers=headers)
     return response.status_code == 200
 
+def get_tag_workflow_status(repo_url, tag_name, github_token):
+    """Get the status of CI workflows running for a specific tag."""
+    api_base = repo_url.replace("https://github.com/", "https://api.github.com/repos/")
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+
+    # Get workflow runs for the tag
+    # GitHub's workflow runs API uses the branch/tag name in the 'head_branch' field
+    api_url = f"{api_base}/actions/runs?event=push&head_branch={tag_name}"
+    response = requests.get(api_url, headers=headers)
+
+    if response.status_code != 200:
+        return None
+
+    data = response.json()
+    workflow_runs = data.get('workflow_runs', [])
+
+    if not workflow_runs:
+        return None
+
+    # Get the most recent workflow run for this tag
+    run = workflow_runs[0]
+    status = run.get('status')
+    conclusion = run.get('conclusion')
+    workflow_name = run.get('name', 'CI')
+    run_id = run.get('id')
+
+    return {
+        'status': status,
+        'conclusion': conclusion,
+        'workflow_name': workflow_name,
+        'run_id': run_id
+    }
+
 def get_release_notes(tag_name):
     """Fetch release notes page title from lean-lang.org."""
     # Strip -rcX suffix if present for the URL
@@ -130,20 +170,17 @@ def get_release_notes(tag_name):
     try:
         response = requests.get(reference_url)
         response.raise_for_status() # Raise HTTPError for bad responses (4xx or 5xx)
-        
+
         # Extract title using regex
         match = re.search(r"<title>(.*?)</title>", response.text, re.IGNORECASE | re.DOTALL)
         if match:
             return match.group(1).strip()
         else:
-            print(f"  ⚠️ Could not find <title> tag in {reference_url}")
             return None
-            
-    except requests.exceptions.RequestException as e:
-        print(f"  ❌ Error fetching release notes from {reference_url}: {e}")
+
+    except requests.exceptions.RequestException:
         return None
-    except Exception as e:
-        print(f"  ❌ An unexpected error occurred while processing release notes: {e}")
+    except Exception:
         return None
 
 def get_branch_content(repo_url, branch, file_path, github_token):
@@ -512,30 +549,57 @@ def main():
             print(f"  ❌ Short commit hash {commit_hash[:SHORT_HASH_LENGTH]} is numeric and starts with 0, causing issues for version parsing. Try regenerating the last commit to get a new hash.")
             lean4_success = False
 
-    if not release_page_exists(lean_repo_url, toolchain, github_token):
-        print(f"  ❌ Release page for {toolchain} does not exist")
+    release_page_ready = release_page_exists(lean_repo_url, toolchain, github_token)
+    if not release_page_ready:
+        print(f"  ❌ Release page for {toolchain} does not exist (This will be created by CI.)")
+
+        # Check CI workflow status
+        workflow_status = get_tag_workflow_status(lean_repo_url, toolchain, github_token)
+        if workflow_status:
+            status = workflow_status['status']
+            conclusion = workflow_status['conclusion']
+            workflow_name = workflow_status['workflow_name']
+            run_id = workflow_status['run_id']
+            workflow_url = f"{lean_repo_url}/actions/runs/{run_id}"
+
+            if status == 'in_progress' or status == 'queued':
+                print(f"     🔄 {workflow_name} workflow is {status}: {workflow_url}")
+            elif status == 'completed':
+                if conclusion == 'success':
+                    print(f"     ✅ {workflow_name} workflow completed successfully: {workflow_url}")
+                elif conclusion == 'failure':
+                    print(f"     ❌ {workflow_name} workflow failed: {workflow_url}")
+                else:
+                    print(f"     ⚠️  {workflow_name} workflow completed with status: {conclusion}: {workflow_url}")
+            else:
+                print(f"     ℹ️  {workflow_name} workflow status: {status}: {workflow_url}")
+
         lean4_success = False
     else:
         print(f"  ✅ Release page for {toolchain} exists")
-        
-    # Check the actual release notes page title
+
+    # Check the actual release notes page title (informational only - does not block)
     actual_title = get_release_notes(toolchain)
     expected_title_prefix = f"Lean {toolchain.lstrip('v')}" # e.g., "Lean 4.19.0" or "Lean 4.19.0-rc1"
+    base_tag = toolchain.split('-')[0]
+    release_notes_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
 
     if actual_title is None:
-        # Error already printed by get_release_notes
-        lean4_success = False
+        print(f"  ⚠️  Release notes not found at {release_notes_url} (this will be fixed while updating the reference-manual repository)")
     elif not actual_title.startswith(expected_title_prefix):
-        # Construct URL for the error message (using the base tag)
-        base_tag = toolchain.split('-')[0]
-        check_url = f"https://lean-lang.org/doc/reference/latest/releases/{base_tag}/"
-        print(f"  ❌ Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {check_url}")
-        lean4_success = False
+        print(f"  ⚠️  Release notes page title mismatch. Expected prefix '{expected_title_prefix}', got '{actual_title}'. Check {release_notes_url}")
     else:
         print(f"  ✅ Release notes page title looks good ('{actual_title}').")
 
     repo_status["lean4"] = lean4_success
 
+    # If the release page doesn't exist, skip repository checks and master branch checks
+    # The preliminary infrastructure must be in place first
+    if not release_page_exists(lean_repo_url, toolchain, github_token):
+        print("\n⚠️  Release process blocked: preliminary Lean4 infrastructure incomplete.")
+        print("   Complete the steps above, then rerun this script to proceed with downstream repositories.")
+        return
+
     # Load repositories and perform further checks
     print("\nChecking repositories...")
 

script/release_steps.py

@@ -589,8 +589,19 @@ def execute_release_steps(repo, version, config):
         
         # Clean lake cache for a fresh build
         print(blue("Cleaning lake cache..."))
-        run_command("rm -rf .lake", cwd=repo_path)
-        
+        run_command("lake clean", cwd=repo_path)
+
+        # Check if downstream of Mathlib and get cache if so
+        mathlib_package_dir = repo_path / ".lake" / "packages" / "mathlib"
+        if mathlib_package_dir.exists():
+            print(blue("Project is downstream of Mathlib, fetching cache..."))
+            try:
+                run_command("lake exe cache get", cwd=repo_path, stream_output=True)
+                print(green("Cache fetched successfully"))
+            except subprocess.CalledProcessError as e:
+                print(yellow("Failed to fetch cache, continuing anyway..."))
+                print(yellow(f"Cache fetch error: {e}"))
+
         try:
             run_command("lake build", cwd=repo_path, stream_output=True)
             print(green("Build completed successfully"))

src/CMakeLists.txt

@@ -10,7 +10,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 25)
+set(LEAN_VERSION_MINOR 26)
 set(LEAN_VERSION_PATCH 0)
 set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")

src/Init.lean

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

src/Init/BinderNameHint.lean

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

src/Init/Classical.lean

@@ -181,9 +181,6 @@ theorem not_imp_iff_and_not : ¬(a → b) ↔ a ∧ ¬b := Decidable.not_imp_iff
 
 theorem not_and_iff_not_or_not : ¬(a ∧ b) ↔ ¬a ∨ ¬b := Decidable.not_and_iff_not_or_not
 
-@[deprecated not_and_iff_not_or_not (since := "2025-03-18")]
-abbrev not_and_iff_or_not_not := @not_and_iff_not_or_not
-
 theorem not_iff : ¬(a ↔ b) ↔ (¬a ↔ b) := Decidable.not_iff
 
 @[simp] theorem imp_iff_left_iff  : (b ↔ a → b) ↔ a ∨ b := Decidable.imp_iff_left_iff

src/Init/Control/Basic.lean

@@ -45,9 +45,6 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
     forIn x b f = forIn' x b (fun x h => binderNameHint x f <| binderNameHint h () <| f x) := by
   rfl
 
-@[deprecated forIn_eq_forIn' (since := "2025-04-04")]
-abbrev forIn_eq_forin' := @forIn_eq_forIn'
-
 /--
 Extracts the value from a `ForInStep`, ignoring whether it is `ForInStep.done` or `ForInStep.yield`.
 -/

src/Init/Control/EState.lean

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

src/Init/Control/Except.lean

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

src/Init/Control/Lawful/Basic.lean

@@ -7,8 +7,6 @@ module
 
 prelude
 public import Init.Ext
-public import Init.SimpLemmas
-public import Init.Meta
 
 public section
 
@@ -257,11 +255,6 @@ instance : LawfulMonad Id := by
 @[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 -/

src/Init/Control/Lawful/Instances.lean

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

src/Init/Control/Lawful/Lemmas.lean

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

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

@@ -6,17 +6,13 @@ Authors: Quang Dao, Paul Reichert
 module
 
 prelude
-public import Init.Control.Option
 import all Init.Control.Option
-public import Init.Control.Except
 import all Init.Control.Except
 public import Init.Control.ExceptCps
 import all Init.Control.ExceptCps
-public import Init.Control.StateRef
 import all Init.Control.StateRef
 public import Init.Control.StateCps
 import all Init.Control.StateCps
-public import Init.Control.Id
 import all Init.Control.Id
 public import Init.Control.Lawful.MonadLift.Lemmas
 public import Init.Control.Lawful.Instances

src/Init/Control/Option.lean

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

src/Init/Control/Reader.lean

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

src/Init/Control/State.lean

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

src/Init/Core.lean

@@ -8,7 +8,6 @@ notation, basic datatypes and type classes
 module
 
 prelude
-public meta import Init.Prelude
 public import Init.SizeOf
 
 public section
@@ -601,17 +600,6 @@ export LawfulSingleton (insert_empty_eq)
 
 attribute [simp] insert_empty_eq
 
-@[deprecated insert_empty_eq (since := "2025-03-12")]
-theorem insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
-    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
-  insert_empty_eq _
-
-@[deprecated insert_empty_eq (since := "2025-03-12")]
-theorem LawfulSingleton.insert_emptyc_eq [EmptyCollection β] [Insert α β] [Singleton α β]
-    [LawfulSingleton α β] (x : α) : (insert x ∅ : β) = singleton x :=
-  insert_empty_eq _
-
-
 /-- Type class used to implement the notation `{ a ∈ c | p a }` -/
 class Sep (α : outParam <| Type u) (γ : Type v) where
   /-- Computes `{ a ∈ c | p a }`. -/
@@ -1096,14 +1084,6 @@ theorem of_toBoolUsing_eq_true {p : Prop} {d : Decidable p} (h : toBoolUsing d =
 theorem of_toBoolUsing_eq_false {p : Prop} {d : Decidable p} (h : toBoolUsing d = false) : ¬p :=
   of_decide_eq_false h
 
-set_option linter.missingDocs false in
-@[deprecated of_toBoolUsing_eq_true (since := "2025-04-04")]
-abbrev ofBoolUsing_eq_true := @of_toBoolUsing_eq_true
-
-set_option linter.missingDocs false in
-@[deprecated of_toBoolUsing_eq_false (since := "2025-04-04")]
-abbrev ofBoolUsing_eq_false := @of_toBoolUsing_eq_false
-
 instance : Decidable True :=
   isTrue trivial
 
@@ -1160,12 +1140,21 @@ variable {p q : Prop}
   decidable_of_decidable_of_iff (p := p) (h ▸ Iff.rfl)
 end
 
-@[macro_inline] instance {p q} [Decidable p] [Decidable q] : Decidable (p → q) :=
-  if hp : p then
-    if hq : q then isTrue (fun _ => hq)
-    else isFalse (fun h => absurd (h hp) hq)
-  else isTrue (fun h => absurd h hp)
+@[inline]
+instance exists_prop_decidable {p} (P : p → Prop)
+    [Decidable p] [∀ h, Decidable (P h)] : Decidable (Exists P) :=
+  if h : p then
+    decidable_of_decidable_of_iff ⟨fun h2 => ⟨h, h2⟩, fun ⟨_, h2⟩ => h2⟩
+  else isFalse fun ⟨h', _⟩ => h h'
 
+@[inline]
+instance forall_prop_decidable {p} (P : p → Prop)
+    [Decidable p] [∀ h, Decidable (P h)] : Decidable (∀ h, P h) :=
+  if h : p then
+    decidable_of_decidable_of_iff ⟨fun h2 _ => h2, fun al => al h⟩
+  else isTrue fun h2 => absurd h2 h
+
+@[inline]
 instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
   if hp : p then
     if hq : q then
@@ -1213,11 +1202,13 @@ theorem dif_eq_if (c : Prop) {h : Decidable c} {α : Sort u} (t : α) (e : α) :
   | isTrue _    => rfl
   | isFalse _   => rfl
 
+@[macro_inline]
 instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) :=
   match dC with
   | isTrue _   => dT
   | isFalse _  => dE
 
+@[inline]
 instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) :=
   match dC with
   | isTrue hc  => dT hc
@@ -1368,10 +1359,6 @@ namespace Subtype
 theorem exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
   | ⟨a, h⟩ => ⟨a, h⟩
 
-set_option linter.missingDocs false in
-@[deprecated exists_of_subtype (since := "2025-04-04")]
-abbrev existsOfSubtype := @exists_of_subtype
-
 variable {α : Type u} {p : α → Prop}
 
 protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2

src/Init/Data.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Basic
 public import Init.Data.Nat
 public import Init.Data.Bool
 public import Init.Data.BitVec

src/Init/Data/AC.lean

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

src/Init/Data/Array/Attach.lean

@@ -6,10 +6,7 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
-public import Init.Data.Array.Mem
-public import Init.Data.Array.Lemmas
 public import Init.Data.Array.Count
-public import Init.Data.List.Attach
 import all Init.Data.List.Attach
 
 public section
@@ -752,9 +749,6 @@ and simplifies these to the function directly taking the value.
     (Array.replicate n x).unattach = Array.replicate n x.1 := by
   simp [unattach]
 
-@[deprecated unattach_replicate (since := "2025-03-18")]
-abbrev unattach_mkArray := @unattach_replicate
-
 /-! ### Well-founded recursion preprocessing setup -/
 
 @[wf_preprocess] theorem map_wfParam {xs : Array α} {f : α → β} :

src/Init/Data/Array/Basic.lean

@@ -6,10 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.WFTactics
-public import Init.Data.Nat.Basic
-public import Init.Data.Fin.Basic
-public import Init.Data.UInt.BasicAux
 public import Init.GetElem
 public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
@@ -213,20 +209,6 @@ Examples:
 def replicate {α : Type u} (n : Nat) (v : α) : Array α where
   toList := List.replicate n v
 
-/--
-Creates an array that contains `n` repetitions of `v`.
-
-The corresponding `List` function is `List.replicate`.
-
-Examples:
- * `Array.mkArray 2 true = #[true, true]`
- * `Array.mkArray 3 () = #[(), (), ()]`
- * `Array.mkArray 0 "anything" = #[]`
--/
-@[extern "lean_mk_array", deprecated replicate (since := "2025-03-18")]
-def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
-  toList := List.replicate n v
-
 /--
 Swaps two elements of an array. The modification is performed in-place when the reference to the
 array is unique.
@@ -2151,5 +2133,3 @@ instance [ToString α] : ToString (Array α) where
   toString xs := String.Internal.append "#" (toString xs.toList)
 
 end Array
-
-export Array (mkArray)

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

@@ -8,7 +8,6 @@ module
 
 prelude
 public import Init.Data.List.TakeDrop
-public import Init.Data.Array.Basic
 import all Init.Data.Array.Basic
 
 public section

src/Init/Data/Array/Count.lean

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

src/Init/Data/Array/DecidableEq.lean

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

src/Init/Data/Array/Erase.lean

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

src/Init/Data/Array/Extract.lean

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

src/Init/Data/Array/FinRange.lean

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

src/Init/Data/Array/Find.lean

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

src/Init/Data/Array/InsertIdx.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -6,17 +6,10 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
-public import Init.Data.Nat.Lemmas
-public import Init.Data.List.Range
-public import Init.Data.List.Nat.TakeDrop
-public import Init.Data.List.Nat.Modify
 public import Init.Data.List.Nat.Basic
-public import Init.Data.List.Monadic
-public import Init.Data.List.OfFn
 public import Init.Data.Array.Mem
 public import Init.Data.Array.DecidableEq
 public import Init.Data.Range.Lemmas
-public import Init.TacticsExtra
 public import Init.Data.List.ToArray
 import all Init.Data.List.Control
 import all Init.Data.Array.Basic
@@ -324,41 +317,23 @@ theorem singleton_inj : #[a] = #[b] ↔ a = b := by
 @[simp, grind =] theorem size_replicate {n : Nat} {v : α} : (replicate n v).size = n :=
   List.length_replicate ..
 
-@[deprecated size_replicate (since := "2025-03-18")]
-abbrev size_mkArray := @size_replicate
-
 @[simp] theorem toList_replicate : (replicate n a).toList = List.replicate n a := by
   simp only [replicate]
 
-@[deprecated toList_replicate (since := "2025-03-18")]
-abbrev toList_mkArray := @toList_replicate
-
 @[simp, grind =] theorem replicate_zero : replicate 0 a = #[] := rfl
 
-@[deprecated replicate_zero (since := "2025-03-18")]
-abbrev mkArray_zero := @replicate_zero
-
 @[grind =]
 theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
   apply toList_inj.1
   simp [List.replicate_succ']
 
-@[deprecated replicate_succ (since := "2025-03-18")]
-abbrev mkArray_succ := @replicate_succ
-
 @[simp, grind =] theorem getElem_replicate {n : Nat} {v : α} {i : Nat} (h : i < (replicate n v).size) :
     (replicate n v)[i] = v := by simp [← getElem_toList]
 
-@[deprecated getElem_replicate (since := "2025-03-18")]
-abbrev getElem_mkArray := @getElem_replicate
-
 @[grind =] theorem getElem?_replicate {n : Nat} {v : α} {i : Nat} :
     (replicate n v)[i]? = if i < n then some v else none := by
   simp [getElem?_def]
 
-@[deprecated getElem?_replicate (since := "2025-03-18")]
-abbrev getElem?_mkArray := @getElem?_replicate
-
 /-! ### mem -/
 
 @[grind ←]
@@ -1081,12 +1056,6 @@ theorem mem_or_eq_of_mem_setIfInBounds
   cases xs
   simp
 
-@[deprecated beq_empty_eq (since := "2025-04-04")]
-abbrev beq_empty_iff := @beq_empty_eq
-
-@[deprecated empty_beq_eq (since := "2025-04-04")]
-abbrev empty_beq_iff := @empty_beq_eq
-
 @[simp, grind =] theorem push_beq_push [BEq α] {a b : α} {xs ys : Array α} :
     (xs.push a == ys.push b) = (xs == ys && a == b) := by
   cases xs
@@ -1107,9 +1076,6 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
     rw [Bool.eq_iff_iff]
     simp +contextual
 
-@[deprecated replicate_beq_replicate (since := "2025-03-18")]
-abbrev mkArray_beq_mkArray := @replicate_beq_replicate
-
 private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == b := by
   intro h
   have : isEqv #[a] #[b] BEq.beq = true := h
@@ -1725,9 +1691,6 @@ theorem forall_none_of_filterMap_eq_empty (h : filterMap f xs = #[]) : ∀ x ∈
   cases xs
   simp
 
-@[deprecated filterMap_eq_empty_iff (since := "2025-04-04")]
-abbrev filterMap_eq_nil_iff := @filterMap_eq_empty_iff
-
 theorem filterMap_eq_push_iff {f : α → Option β} {xs : Array α} {ys : Array β} {b : β} :
     filterMap f xs = ys.push b ↔ ∃ as a bs,
       xs = as.push a ++ bs ∧ filterMap f as = ys ∧ f a = some b ∧ (∀ x, x ∈ bs → f x = none) := by
@@ -2397,77 +2360,44 @@ theorem flatMap_eq_foldl {f : α → Array β} {xs : Array α} :
 
 @[simp] theorem replicate_one : replicate 1 a = #[a] := rfl
 
-@[deprecated replicate_one (since := "2025-03-18")]
-abbrev mkArray_one := @replicate_one
-
 /-- Variant of `replicate_succ` that prepends `a` at the beginning of the array. -/
 theorem replicate_succ' : replicate (n + 1) a = #[a] ++ replicate n a := by
   apply Array.ext'
   simp [List.replicate_succ]
 
-@[deprecated replicate_succ' (since := "2025-03-18")]
-abbrev mkArray_succ' := @replicate_succ'
-
 @[simp, grind =] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
   unfold replicate
   simp only [List.mem_toArray, List.mem_replicate]
 
-@[deprecated mem_replicate (since := "2025-03-18")]
-abbrev mem_mkArray := @mem_replicate
-
 @[grind →] theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
-@[deprecated eq_of_mem_mkArray (since := "2025-03-18")]
-abbrev eq_of_mem_mkArray := @eq_of_mem_replicate
-
 theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
     (∀ b, b ∈ replicate n a → p b) ↔ n = 0 ∨ p a := by
   cases n <;> simp [mem_replicate]
 
-@[deprecated forall_mem_replicate (since := "2025-03-18")]
-abbrev forall_mem_mkArray := @forall_mem_replicate
-
 @[simp] theorem replicate_succ_ne_empty {n : Nat} {a : α} : replicate (n+1) a ≠ #[] := by
   simp [replicate_succ]
 
-@[deprecated replicate_succ_ne_empty (since := "2025-03-18")]
-abbrev mkArray_succ_ne_empty := @replicate_succ_ne_empty
-
 @[simp] theorem replicate_eq_empty_iff {n : Nat} {a : α} : replicate n a = #[] ↔ n = 0 := by
   cases n <;> simp
 
-@[deprecated replicate_eq_empty_iff (since := "2025-03-18")]
-abbrev mkArray_eq_empty_iff := @replicate_eq_empty_iff
-
 @[simp] theorem replicate_inj : replicate n a = replicate m b ↔ n = m ∧ (n = 0 ∨ a = b) := by
   rw [← toList_inj]
   simp
 
-@[deprecated replicate_inj (since := "2025-03-18")]
-abbrev mkArray_inj := @replicate_inj
-
 theorem eq_replicate_of_mem {a : α} {xs : Array α} (h : ∀ (b) (_ : b ∈ xs), b = a) : xs = replicate xs.size a := by
   rw [← toList_inj]
   simpa using List.eq_replicate_of_mem (by simpa using h)
 
-@[deprecated eq_replicate_of_mem (since := "2025-03-18")]
-abbrev eq_mkArray_of_mem := @eq_replicate_of_mem
-
 theorem eq_replicate_iff {a : α} {n} {xs : Array α} :
     xs = replicate n a ↔ xs.size = n ∧ ∀ (b) (_ : b ∈ xs), b = a := by
   rw [← toList_inj]
   simpa using List.eq_replicate_iff (l := xs.toList)
 
-@[deprecated eq_replicate_iff (since := "2025-03-18")]
-abbrev eq_mkArray_iff := @eq_replicate_iff
-
 theorem map_eq_replicate_iff {xs : Array α} {f : α → β} {b : β} :
     xs.map f = replicate xs.size b ↔ ∀ x ∈ xs, f x = b := by
   simp [eq_replicate_iff]
 
-@[deprecated map_eq_replicate_iff (since := "2025-03-18")]
-abbrev map_eq_mkArray_iff := @map_eq_replicate_iff
-
 @[simp] theorem map_const {xs : Array α} {b : β} : map (Function.const α b) xs = replicate xs.size b :=
   map_eq_replicate_iff.mpr fun _ _ => rfl
 
@@ -2484,143 +2414,86 @@ theorem map_const' {xs : Array α} {b : β} : map (fun _ => b) xs = replicate xs
   apply Array.ext'
   simp
 
-@[deprecated set_replicate_self (since := "2025-03-18")]
-abbrev set_mkArray_self := @set_replicate_self
-
 @[simp] theorem setIfInBounds_replicate_self : (replicate n a).setIfInBounds i a = replicate n a := by
   apply Array.ext'
   simp
 
-@[deprecated setIfInBounds_replicate_self (since := "2025-03-18")]
-abbrev setIfInBounds_mkArray_self := @setIfInBounds_replicate_self
-
 @[simp] theorem replicate_append_replicate : replicate n a ++ replicate m a = replicate (n + m) a := by
   apply Array.ext'
   simp
 
-@[deprecated replicate_append_replicate (since := "2025-03-18")]
-abbrev mkArray_append_mkArray := @replicate_append_replicate
-
 theorem append_eq_replicate_iff {xs ys : Array α} {a : α} :
     xs ++ ys = replicate n a ↔
       xs.size + ys.size = n ∧ xs = replicate xs.size a ∧ ys = replicate ys.size a := by
   simp [← toList_inj, List.append_eq_replicate_iff]
 
-@[deprecated append_eq_replicate_iff (since := "2025-03-18")]
-abbrev append_eq_mkArray_iff := @append_eq_replicate_iff
-
 theorem replicate_eq_append_iff {xs ys : Array α} {a : α} :
     replicate n a = xs ++ ys ↔
       xs.size + ys.size = n ∧ xs = replicate xs.size a ∧ ys = replicate ys.size a := by
   rw [eq_comm, append_eq_replicate_iff]
 
-@[deprecated replicate_eq_append_iff (since := "2025-03-18")]
-abbrev replicate_eq_mkArray_iff := @replicate_eq_append_iff
-
 @[simp] theorem map_replicate : (replicate n a).map f = replicate n (f a) := by
   apply Array.ext'
   simp
 
-@[deprecated map_replicate (since := "2025-03-18")]
-abbrev map_mkArray := @map_replicate
-
 @[grind =] theorem filter_replicate (w : stop = n) :
     (replicate n a).filter p 0 stop = if p a then replicate n a else #[] := by
   apply Array.ext'
   simp only [w]
   split <;> simp_all
 
-@[deprecated filter_replicate (since := "2025-03-18")]
-abbrev filter_mkArray := @filter_replicate
-
 @[simp] theorem filter_replicate_of_pos (w : stop = n) (h : p a) :
     (replicate n a).filter p 0 stop = replicate n a := by
   simp [filter_replicate, h, w]
 
-@[deprecated filter_replicate_of_pos (since := "2025-03-18")]
-abbrev filter_mkArray_of_pos := @filter_replicate_of_pos
-
 @[simp] theorem filter_replicate_of_neg (w : stop = n) (h : ¬ p a) :
     (replicate n a).filter p 0 stop = #[] := by
   simp [filter_replicate, h, w]
 
-@[deprecated filter_replicate_of_neg (since := "2025-03-18")]
-abbrev filter_mkArray_of_neg := @filter_replicate_of_neg
-
 theorem filterMap_replicate {f : α → Option β} (w : stop = n := by simp) :
     (replicate n a).filterMap f 0 stop = match f a with | none => #[] | .some b => replicate n b := by
   apply Array.ext'
   simp only [w, size_replicate, toList_filterMap', toList_replicate, List.filterMap_replicate]
   split <;> simp_all
 
-@[deprecated filterMap_replicate (since := "2025-03-18")]
-abbrev filterMap_mkArray := @filterMap_replicate
-
 -- This is not a useful `simp` lemma because `b` is unknown.
 theorem filterMap_replicate_of_some {f : α → Option β} (h : f a = some b) :
     (replicate n a).filterMap f = replicate n b := by
   simp [filterMap_replicate, h]
 
-@[deprecated filterMap_replicate_of_some (since := "2025-03-18")]
-abbrev filterMap_mkArray_of_some := @filterMap_replicate_of_some
-
 @[simp] theorem filterMap_replicate_of_isSome {f : α → Option β} (h : (f a).isSome) :
     (replicate n a).filterMap f = replicate n (Option.get _ h) := by
   match w : f a, h with
   | some b, _ => simp [filterMap_replicate, w]
 
-@[deprecated filterMap_replicate_of_isSome (since := "2025-03-18")]
-abbrev filterMap_mkArray_of_isSome := @filterMap_replicate_of_isSome
-
 @[simp] theorem filterMap_replicate_of_none {f : α → Option β} (h : f a = none) :
     (replicate n a).filterMap f = #[] := by
   simp [filterMap_replicate, h]
 
-@[deprecated filterMap_replicate_of_none (since := "2025-03-18")]
-abbrev filterMap_mkArray_of_none := @filterMap_replicate_of_none
-
 @[simp] theorem flatten_replicate_empty : (replicate n (#[] : Array α)).flatten = #[] := by
   rw [← toList_inj]
   simp
 
-@[deprecated flatten_replicate_empty (since := "2025-03-18")]
-abbrev flatten_mkArray_empty := @flatten_replicate_empty
-
 @[simp] theorem flatten_replicate_singleton : (replicate n #[a]).flatten = replicate n a := by
   rw [← toList_inj]
   simp
 
-@[deprecated flatten_replicate_singleton (since := "2025-03-18")]
-abbrev flatten_mkArray_singleton := @flatten_replicate_singleton
-
 @[simp] theorem flatten_replicate_replicate : (replicate n (replicate m a)).flatten = replicate (n * m) a := by
   rw [← toList_inj]
   simp
 
-@[deprecated flatten_replicate_replicate (since := "2025-03-18")]
-abbrev flatten_mkArray_replicate := @flatten_replicate_replicate
-
 theorem flatMap_replicate {f : α → Array β} : (replicate n a).flatMap f = (replicate n (f a)).flatten := by
   rw [← toList_inj]
   simp [List.flatMap_replicate]
 
-@[deprecated flatMap_replicate (since := "2025-03-18")]
-abbrev flatMap_mkArray := @flatMap_replicate
-
 @[simp] theorem isEmpty_replicate : (replicate n a).isEmpty = decide (n = 0) := by
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
-@[deprecated isEmpty_replicate (since := "2025-03-18")]
-abbrev isEmpty_mkArray := @isEmpty_replicate
-
 @[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
   rw [← List.toArray_replicate, List.sum_toArray]
   simp
 
-@[deprecated sum_replicate_nat (since := "2025-03-18")]
-abbrev sum_mkArray_nat := @sum_replicate_nat
-
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
 @[grind =]
@@ -2807,9 +2680,6 @@ theorem flatten_reverse {xss : Array (Array α)} :
   rw [← toList_inj]
   simp
 
-@[deprecated reverse_replicate (since := "2025-03-18")]
-abbrev reverse_mkArray := @reverse_replicate
-
 /-! ### extract -/
 
 theorem extract_loop_zero {xs ys : Array α} {start : Nat} : extract.loop xs 0 start ys = ys := by
@@ -3719,15 +3589,9 @@ theorem back?_replicate {a : α} {n : Nat} :
   rw [replicate_eq_toArray_replicate]
   simp only [List.back?_toArray, List.getLast?_replicate]
 
-@[deprecated back?_replicate (since := "2025-03-18")]
-abbrev back?_mkArray := @back?_replicate
-
 @[simp] theorem back_replicate {xs : Array α} (w : 0 < n) : (replicate n xs).back (by simpa using w) = xs := by
   simp [back_eq_getElem]
 
-@[deprecated back_replicate (since := "2025-03-18")]
-abbrev back_mkArray := @back_replicate
-
 /-! ## Additional operations -/
 
 /-! ### leftpad -/
@@ -3745,9 +3609,6 @@ theorem size_rightpad {n : Nat} {a : α} {xs : Array α} :
 
 theorem elem_push_self [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.push a).elem a = true := by simp
 
-@[deprecated elem_push_self (since := "2025-04-04")]
-abbrev elem_cons_self := @elem_push_self
-
 theorem contains_eq_any_beq [BEq α] {xs : Array α} {a : α} : xs.contains a = xs.any (a == ·) := by
   rcases xs with ⟨xs⟩
   simp [List.contains_eq_any_beq]
@@ -3761,7 +3622,7 @@ 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 _=_]
+@[grind =]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp
@@ -3825,9 +3686,6 @@ theorem pop_append {xs ys : Array α} :
 @[simp, grind =] theorem pop_replicate {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a := by
   ext <;> simp
 
-@[deprecated pop_replicate (since := "2025-03-18")]
-abbrev pop_mkArray := @pop_replicate
-
 /-! ## Logic -/
 
 /-! ### any / all -/
@@ -4057,16 +3915,10 @@ theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
     (replicate n a).any f = if n = 0 then false else f a := by
   induction n <;> simp_all [replicate_succ']
 
-@[deprecated any_replicate (since := "2025-03-18")]
-abbrev any_mkArray := @any_replicate
-
 @[simp] theorem all_replicate {n : Nat} {a : α} :
     (replicate n a).all f = if n = 0 then true else f a := by
   induction n <;> simp_all +contextual [replicate_succ']
 
-@[deprecated all_replicate (since := "2025-03-18")]
-abbrev all_mkArray := @all_replicate
-
 /-! ### modify -/
 
 @[simp, grind =] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
@@ -4241,17 +4093,11 @@ theorem replace_extract {xs : Array α} {i : Nat} :
     (replicate n a).replace a b = #[b] ++ replicate (n - 1) a := by
   cases n <;> simp_all [replicate_succ', replace_append]
 
-@[deprecated replace_replicate_self (since := "2025-03-18")]
-abbrev replace_mkArray_self := @replace_replicate_self
-
 @[simp] theorem replace_replicate_ne {a b c : α} (h : !b == a) :
     (replicate n a).replace b c = replicate n a := by
   rw [replace_of_not_mem]
   simp_all
 
-@[deprecated replace_replicate_ne (since := "2025-03-18")]
-abbrev replace_mkArray_ne := @replace_replicate_ne
-
 end replace
 
 /-! ### toListRev -/
@@ -4419,9 +4265,6 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i
 @[deprecated mem_toList_iff (since := "2025-05-26")]
 theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
 
-@[deprecated not_mem_empty (since := "2025-03-25")]
-theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
-
 /-! # get lemmas -/
 
 theorem lt_of_getElem {x : α} {xs : Array α} {i : Nat} {hidx : i < xs.size} (_ : xs[i] = x) :
@@ -4470,12 +4313,6 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
   cases xs
   simp
 
-/-! ### contains -/
-
-@[deprecated contains_iff (since := "2025-04-07")]
-abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a ↔ a ∈ xs :=
-  contains_iff
-
 /-! ### isPrefixOf -/
 
 @[simp, grind =] theorem isPrefixOf_toList [BEq α] {xs ys : Array α} :

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

@@ -6,9 +6,6 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Core
-import Init.Data.Array.Basic
-import Init.Data.Nat.Lemmas
 public import Init.Data.Range.Polymorphic.Iterators
 public import Init.Data.Range.Polymorphic.Nat
 import Init.Data.Iterators.Consumers

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

@@ -10,9 +10,7 @@ import all Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lex.Basic
 public import Init.Data.Array.Lemmas
 public import Init.Data.List.Lex
-import Init.Data.Range.Polymorphic.Lemmas
 import Init.Data.Range.Polymorphic.NatLemmas
-import Init.Data.Order.Lemmas
 
 public section
 

src/Init/Data/Array/MapIdx.lean

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

src/Init/Data/Array/Mem.lean

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

src/Init/Data/Array/Monadic.lean

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

src/Init/Data/Array/OfFn.lean

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

src/Init/Data/Array/Perm.lean

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

src/Init/Data/Array/Range.lean

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

src/Init/Data/Array/Subarray.lean

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

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

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

src/Init/Data/Array/TakeDrop.lean

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

src/Init/Data/Array/Zip.lean

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

src/Init/Data/Basic.lean

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

src/Init/Data/BitVec/Basic.lean

@@ -6,11 +6,8 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
-public import Init.Data.Fin.Basic
 public import Init.Data.Nat.Bitwise.Lemmas
-public import Init.Data.Nat.Power2
 public import Init.Data.Int.Bitwise.Basic
-public import Init.Data.BitVec.BasicAux
 
 @[expose] public section
 

src/Init/Data/BitVec/Bitblast.lean

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

src/Init/Data/BitVec/Folds.lean

@@ -6,10 +6,8 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
-public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
 public import Init.Data.BitVec.Lemmas
-public import Init.Data.Nat.Lemmas
 public import Init.Data.Fin.Iterate
 
 public section

src/Init/Data/BitVec/Lemmas.lean

@@ -6,25 +6,14 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B
 module
 
 prelude
-public import Init.Data.Bool
-public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
-public import Init.Data.BitVec.BasicAux
 import all Init.Data.BitVec.BasicAux
 public import Init.Data.Fin.Lemmas
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Nat.Div.Lemmas
-public import Init.Data.Nat.Mod
-public import Init.Data.Nat.Div.Lemmas
 public import Init.Data.Int.Bitwise.Lemmas
 public import Init.Data.Int.LemmasAux
-public import Init.Data.Int.Pow
-public import Init.Data.Int.LemmasAux
 public import Init.Data.BitVec.Bootstrap
-public import Init.Data.Order.Factories
 public import Init.Data.List.BasicAux
 import Init.Data.List.Lemmas
-import Init.Data.BEq
 
 public section
 
@@ -45,14 +34,6 @@ namespace BitVec
   simp only [Bool.and_eq_false_imp, decide_eq_true_eq]
   omega
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_of_ge (since := "2025-04-04")]
-abbrev getLsbD_ge := @getLsbD_of_ge
-
-set_option linter.missingDocs false in
-@[deprecated getMsbD_of_ge (since := "2025-04-04")]
-abbrev getMsbD_ge := @getMsbD_of_ge
-
 theorem lt_of_getLsbD {x : BitVec w} {i : Nat} : getLsbD x i = true → i < w := by
   if h : i < w then
     simp [h]
@@ -186,12 +167,6 @@ theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i <
 @[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
@@ -214,18 +189,6 @@ theorem lt_of_isSome_getMsb? (x : BitVec w) (i : Nat) : (getMsb? x i).isSome →
   else
     simp [Nat.ge_of_not_lt h]
 
-set_option linter.missingDocs false in
-@[deprecated lt_of_getElem?_eq_some (since := "2025-04-04")]
-abbrev lt_of_getLsb?_eq_some := @lt_of_getElem?_eq_some
-
-set_option linter.missingDocs false in
-@[deprecated lt_of_isSome_getElem? (since := "2025-04-04")]
-abbrev lt_of_getLsb?_isSome := @lt_of_isSome_getElem?
-
-set_option linter.missingDocs false in
-@[deprecated lt_of_isSome_getMsb? (since := "2025-04-04")]
-abbrev lt_of_getMsb?_isSome := @lt_of_isSome_getMsb?
-
 theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
     x.getMsbD i = (x.getMsb? i).getD false := by
   rw [getMsbD_eq_getLsbD]
@@ -1761,9 +1724,6 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
     rw [h]
     simp
 
-set_option linter.missingDocs false in
-@[deprecated getMsbD_not (since := "2025-04-04")] abbrev getMsb_not := @getMsbD_not
-
 @[simp] theorem msb_not {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb) := by
   simp [BitVec.msb]
 
@@ -2583,10 +2543,6 @@ theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
   ext i h
   simp [getElem_signExtend, show i < w by omega]
 
-@[deprecated signExtend_eq_setWidth_of_le (since := "2025-03-07")]
-theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w) :
-  x.signExtend v = x.setWidth v := signExtend_eq_setWidth_of_le x hv
-
 /-- Sign extending to the same bitwidth is a no op. -/
 @[simp] theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
   rw [signExtend_eq_setWidth_of_le _ (Nat.le_refl _), setWidth_eq]
@@ -3646,9 +3602,6 @@ theorem sub_eq_add_neg {n} (x y : BitVec n) : x - y = x + - y := by
   simp only [toNat_sub, toNat_add, toNat_neg, Nat.add_mod_mod]
   rw [Nat.add_comm]
 
-set_option linter.missingDocs false in
-@[deprecated sub_eq_add_neg (since := "2025-04-04")] abbrev sub_toAdd := @sub_eq_add_neg
-
 theorem add_left_neg (x : BitVec w) : -x + x = 0#w := by
   apply toInt_inj.mp
   simp [toInt_neg, Int.add_left_neg]
@@ -3688,10 +3641,6 @@ theorem neg_one_eq_allOnes : -1#w = allOnes w := by
     have r : (2^w - 1) < 2^w := by omega
     simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
 
-set_option linter.missingDocs false in
-@[deprecated neg_one_eq_allOnes (since := "2025-04-04")]
-abbrev negOne_eq_allOnes := @neg_one_eq_allOnes
-
 theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1#w := by
   apply eq_of_toNat_eq
   simp only [toNat_neg, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
@@ -4693,9 +4642,6 @@ theorem zero_smod {x : BitVec w} : (0#w).smod x = 0#w := by
 @[simp, grind =] theorem getLsbD_ofBoolListLE : (ofBoolListLE bs).getLsbD i = bs.getD i false := by
   induction bs generalizing i <;> cases i <;> simp_all [ofBoolListLE]
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_ofBoolListLE (since := "2025-04-04")] abbrev getLsb_ofBoolListLE := @getLsbD_ofBoolListLE
-
 @[simp, grind =] theorem getMsbD_ofBoolListLE :
     (ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false) := by
   simp [getMsbD_eq_getLsbD]
@@ -4766,14 +4712,6 @@ theorem getLsbD_rotateLeftAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i
   apply getLsbD_of_ge
   omega
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_rotateLeftAux_of_lt (since := "2025-04-04")]
-abbrev getLsbD_rotateLeftAux_of_le := @getLsbD_rotateLeftAux_of_lt
-
-set_option linter.missingDocs false in
-@[deprecated getLsbD_rotateLeftAux_of_ge (since := "2025-04-04")]
-abbrev getLsbD_rotateLeftAux_of_geq := @getLsbD_rotateLeftAux_of_ge
-
 /-- When `r < w`, we give a formula for `(x.rotateLeft r).getLsbD i`. -/
 theorem getLsbD_rotateLeft_of_le {x : BitVec w} {r i : Nat} (hr: r < w) :
     (x.rotateLeft r).getLsbD i =
@@ -4930,14 +4868,6 @@ theorem getLsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i
   apply getLsbD_of_ge
   omega
 
-set_option linter.missingDocs false in
-@[deprecated getLsbD_rotateRightAux_of_lt (since := "2025-04-04")]
-abbrev getLsbD_rotateRightAux_of_le := @getLsbD_rotateRightAux_of_lt
-
-set_option linter.missingDocs false in
-@[deprecated getLsbD_rotateRightAux_of_ge (since := "2025-04-04")]
-abbrev getLsbD_rotateRightAux_of_geq := @getLsbD_rotateRightAux_of_ge
-
 /-- `rotateRight` equals the bit fiddling definition of `rotateRightAux` when the rotation amount is
 smaller than the bitwidth. -/
 theorem rotateRight_eq_rotateRightAux_of_lt {x : BitVec w} {r : Nat} (hr : r < w) :

src/Init/Data/Bool.lean

@@ -111,35 +111,11 @@ Needed for confluence of term `(a && b) ↔ a` which reduces to `(a && b) = a` v
 @[simp] theorem eq_self_and : ∀ {a b : Bool}, (a = (a && b)) ↔ (a → b) := by decide
 @[simp] theorem eq_and_self : ∀ {a b : Bool}, (b = (a && b)) ↔ (b → a) := by decide
 
-@[deprecated and_eq_left_iff_imp (since := "2025-04-04")]
-abbrev and_iff_left_iff_imp := @and_eq_left_iff_imp
-
-@[deprecated and_eq_right_iff_imp (since := "2025-04-04")]
-abbrev and_iff_right_iff_imp := @and_eq_right_iff_imp
-
-@[deprecated eq_self_and (since := "2025-04-04")]
-abbrev iff_self_and := @eq_self_and
-
-@[deprecated eq_and_self (since := "2025-04-04")]
-abbrev iff_and_self := @eq_and_self
-
 @[simp] theorem not_and_eq_left_iff_and  : ∀ {a b : Bool}, ((!a && b) = a) ↔ !a ∧ !b := by decide
 @[simp] theorem and_not_eq_right_iff_and : ∀ {a b : Bool}, ((a && !b) = b) ↔ !a ∧ !b := by decide
 @[simp] theorem eq_not_self_and : ∀ {a b : Bool}, (a = (!a && b)) ↔ !a ∧ !b := by decide
 @[simp] theorem eq_and_not_self : ∀ {a b : Bool}, (b = (a && !b)) ↔ !a ∧ !b := by decide
 
-@[deprecated not_and_eq_left_iff_and (since := "2025-04-04")]
-abbrev not_and_iff_left_iff_imp := @not_and_eq_left_iff_and
-
-@[deprecated and_not_eq_right_iff_and (since := "2025-04-04")]
-abbrev and_not_iff_right_iff_imp := @and_not_eq_right_iff_and
-
-@[deprecated eq_not_self_and (since := "2025-04-04")]
-abbrev iff_not_self_and := @eq_not_self_and
-
-@[deprecated eq_and_not_self (since := "2025-04-04")]
-abbrev iff_and_not_self := @eq_and_not_self
-
 /-! ### or -/
 
 @[simp] theorem or_self_left  : ∀ (a b : Bool), (a || (a || b)) = (a || b) := by decide
@@ -169,35 +145,11 @@ Needed for confluence of term `(a || b) ↔ a` which reduces to `(a || b) = a` v
 @[simp] theorem eq_self_or : ∀ {a b : Bool}, (a = (a || b)) ↔ (b → a) := by decide
 @[simp] theorem eq_or_self : ∀ {a b : Bool}, (b = (a || b)) ↔ (a → b) := by decide
 
-@[deprecated or_eq_left_iff_imp (since := "2025-04-04")]
-abbrev or_iff_left_iff_imp := @or_eq_left_iff_imp
-
-@[deprecated or_eq_right_iff_imp (since := "2025-04-04")]
-abbrev or_iff_right_iff_imp := @or_eq_right_iff_imp
-
-@[deprecated eq_self_or (since := "2025-04-04")]
-abbrev iff_self_or := @eq_self_or
-
-@[deprecated eq_or_self (since := "2025-04-04")]
-abbrev iff_or_self := @eq_or_self
-
 @[simp] theorem not_or_eq_left_iff_and  : ∀ {a b : Bool}, ((!a || b) = a) ↔ a ∧ b := by decide
 @[simp] theorem or_not_eq_right_iff_and : ∀ {a b : Bool}, ((a || !b) = b) ↔ a ∧ b := by decide
 @[simp] theorem eq_not_self_or : ∀ {a b : Bool}, (a = (!a || b)) ↔ a ∧ b := by decide
 @[simp] theorem eq_or_not_self : ∀ {a b : Bool}, (b = (a || !b)) ↔ a ∧ b := by decide
 
-@[deprecated not_or_eq_left_iff_and (since := "2025-04-04")]
-abbrev not_or_iff_left_iff_imp := @not_or_eq_left_iff_and
-
-@[deprecated or_not_eq_right_iff_and (since := "2025-04-04")]
-abbrev or_not_iff_right_iff_imp := @or_not_eq_right_iff_and
-
-@[deprecated eq_not_self_or (since := "2025-04-04")]
-abbrev iff_not_self_or := @eq_not_self_or
-
-@[deprecated eq_or_not_self (since := "2025-04-04")]
-abbrev iff_or_not_self := @eq_or_not_self
-
 theorem or_comm : ∀ (x y : Bool), (x || y) = (y || x) := by decide
 instance : Std.Commutative (· || ·) := ⟨or_comm⟩
 
@@ -621,11 +573,6 @@ protected theorem cond_false {α : Sort u} {a b : α} : cond false a b = b := co
 @[simp] theorem cond_then_self  : ∀ (c b : Bool), cond c c b = (c || b) := by decide
 @[simp] theorem cond_else_self : ∀ (c b : Bool), cond c b c = (c && b) := by decide
 
-@[deprecated cond_then_not_self (since := "2025-04-04")] abbrev cond_true_not_same := @cond_then_not_self
-@[deprecated cond_else_not_self (since := "2025-04-04")] abbrev cond_false_not_same := @cond_else_not_self
-@[deprecated cond_then_self (since := "2025-04-04")] abbrev cond_true_same := @cond_then_self
-@[deprecated cond_else_self (since := "2025-04-04")] abbrev cond_false_same := @cond_else_self
-
 theorem cond_pos {b : Bool} {a a' : α} (h : b = true) : (bif b then a else a') = a := by
   rw [h, cond_true]
 

src/Init/Data/ByteArray/Basic.lean

@@ -6,11 +6,8 @@ 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
@@ -27,9 +24,6 @@ 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
 

src/Init/Data/ByteArray/Bootstrap.lean

@@ -6,7 +6,6 @@ Author: Markus Himmel
 module
 
 prelude
-public import Init.Prelude
 public import Init.Data.List.Basic
 
 public section

src/Init/Data/ByteArray/Lemmas.lean

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

src/Init/Data/Char/Lemmas.lean

@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Char.Basic
 import all Init.Data.Char.Basic
 public import Init.Data.UInt.Lemmas
 
@@ -70,4 +69,9 @@ def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
   rw [Char.ofNat, dif_pos]
   rfl
 
+@[simp]
+theorem toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8 := rfl
+
+theorem toString_eq_singleton {c : Char} : c.toString = String.singleton c := rfl
+
 end Char

src/Init/Data/Dyadic/Basic.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Rat.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
-import Init.Data.Int.DivMod.Lemmas
 import Init.Hints
 
 /-!

src/Init/Data/Dyadic/Instances.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Dyadic.Basic
-public import Init.Grind.Ring.Basic
 public import Init.Grind.Ordered.Ring
 
 /-! # Internal `grind` algebra instances for `Dyadic`. -/

src/Init/Data/Dyadic/Inv.lean

@@ -5,7 +5,6 @@ Authors: Kim Morrison
 -/
 module
 prelude
-import Init.Data.Dyadic.Basic
 import Init.Data.Dyadic.Round
 import Init.Grind.Ordered.Ring
 

src/Init/Data/Dyadic/Round.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Dyadic.Basic
 import all Init.Data.Dyadic.Instances
-import Init.Data.Int.Bitwise.Lemmas
 import Init.Grind.Ordered.Rat
 import Init.Grind.Ordered.Field
 

src/Init/Data/Fin/Bitwise.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.Nat.Bitwise
-public import Init.Data.Fin.Basic
 
 public section
 

src/Init/Data/Fin/Fold.lean

@@ -6,7 +6,6 @@ Authors: François G. Dorais
 module
 
 prelude
-public import Init.Data.Nat.Linear
 public import Init.Control.Lawful.Basic
 public import Init.Data.Fin.Lemmas
 

src/Init/Data/Fin/Iterate.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.PropLemmas
-public import Init.Data.Fin.Basic
 
 public section
 

src/Init/Data/Fin/Lemmas.lean

@@ -8,10 +8,6 @@ module
 prelude
 public import Init.Data.Nat.Lemmas
 public import Init.Ext
-public import Init.ByCases
-public import Init.Conv
-public import Init.Omega
-public import Init.Data.Order.Factories
 import Init.Data.Order.Lemmas
 
 @[expose] public section

src/Init/Data/Float.lean

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

src/Init/Data/Float32.lean

@@ -6,9 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Core
-public import Init.Data.Int.Basic
-public import Init.Data.ToString.Basic
 public import Init.Data.Float
 
 public section

src/Init/Data/FloatArray/Basic.lean

@@ -6,9 +6,7 @@ Author: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Array.Basic
 public import Init.Data.Float
-public import Init.Data.Option.Basic
 import Init.Ext
 public import Init.Data.Array.DecidableEq
 
@@ -31,9 +29,6 @@ attribute [ext] FloatArray
 def emptyWithCapacity (c : @& Nat) : FloatArray :=
   { data := #[] }
 
-@[deprecated emptyWithCapacity (since := "2025-03-12")]
-abbrev mkEmpty := emptyWithCapacity
-
 def empty : FloatArray :=
   emptyWithCapacity 0
 

src/Init/Data/Format/Basic.lean

@@ -170,7 +170,7 @@ private def spaceUptoLine : Format → Bool → Int → Nat → SpaceResult
   | text s,       flatten, _, _ =>
     let p := String.Internal.posOf s '\n'
     let off := String.Internal.offsetOfPos s p
-    { foundLine := p != s.endPos, foundFlattenedHardLine := flatten && p != s.endPos, space := off }
+    { foundLine := p != s.rawEndPos, foundFlattenedHardLine := flatten && p != s.rawEndPos, space := off }
   | append f₁ f₂, flatten, m, w => merge w (spaceUptoLine f₁ flatten m w) (spaceUptoLine f₂ flatten m)
   | nest n f,     flatten, m, w => spaceUptoLine f flatten (m - n) w
   | group f _,    _,       m, w => spaceUptoLine f true m w
@@ -264,14 +264,14 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
     | nest n f => be w (gs' ({ i with f, indent := i.indent + n }::is))
     | text s =>
       let p := String.Internal.posOf s '\n'
-      if p == s.endPos then
+      if p == s.rawEndPos then
         pushOutput s
         endTags i.activeTags
         be w (gs' is)
       else
         pushOutput (String.Internal.extract s {} p)
         pushNewline i.indent.toNat
-        let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.endPos) }::is
+        let is := { i with f := text (String.Internal.extract s (String.Internal.next s p) s.rawEndPos) }::is
         -- after a hard line break, re-evaluate whether to flatten the remaining group
         -- note that we shouldn't start flattening after a hard break outside a group
         if g.fla == .disallow then
@@ -411,7 +411,6 @@ Renders a `Format` to a string.
 * `column`: begin the first line wrap `column` characters earlier than usual
   (this is useful when the output String will be printed starting at `column`)
 -/
-@[export lean_format_pretty]
 def pretty (f : Format) (width : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
   let act : StateM State Unit := prettyM f width indent
   State.out <| act (State.mk "" column) |>.snd

src/Init/Data/Format/Instances.lean

@@ -6,9 +6,7 @@ Author: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Format.Basic
 public import Init.Data.Array.Basic
-public import Init.Data.ToString.Basic
 import Init.Data.String.Basic
 
 public section

src/Init/Data/Format/Syntax.lean

@@ -9,7 +9,6 @@ prelude
 public import Init.Data.Format.Macro
 public import Init.Data.Format.Instances
 public import Init.Meta
-import Init.Data.String.Basic
 import Init.Data.ToString.Name
 
 public section

src/Init/Data/Function.lean

@@ -5,7 +5,6 @@ Authors: Kim Morrison
 -/
 module
 prelude
-public import Init.Core
 public import Init.Grind.Tactics
 public section
 namespace Function

src/Init/Data/Hashable.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.UInt.Basic
 public import Init.Data.String.Basic
-public import Init.Data.ByteArray.Basic
 
 public section
 universe u

src/Init/Data/Int/Basic.lean

@@ -313,7 +313,7 @@ the logical model.
 Examples:
  * `(7 : Int).natAbs = 7`
  * `(0 : Int).natAbs = 0`
- * `((-11 : Int).natAbs = 11`
+ * `(-11 : Int).natAbs = 11`
 -/
 @[extern "lean_nat_abs", expose]
 def natAbs (m : @& Int) : Nat :=
@@ -369,9 +369,6 @@ def toNat? : Int → Option Nat
   | (n : Nat) => some n
   | -[_+1] => none
 
-@[deprecated toNat? (since := "2025-03-11"), inherit_doc toNat?]
-abbrev toNat' := toNat?
-
 /-! ## divisibility -/
 
 /--

src/Init/Data/Int/Cooper.lean

@@ -6,7 +6,6 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Int.DivMod.Lemmas
 public import Init.Data.Int.Gcd
 
 public section

src/Init/Data/Int/DivMod/Basic.lean

@@ -118,9 +118,6 @@ instance : Mod Int where
 
 @[simp, norm_cast] theorem natCast_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
-@[deprecated natCast_ediv (since := "2025-04-17")]
-theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := natCast_ediv m n
-
 theorem ofNat_ediv_ofNat {a b : Nat} : (↑a / ↑b : Int) = (a / b : Nat) := rfl
 @[norm_cast]
 theorem negSucc_ediv_ofNat_succ {a b : Nat} : ((-[a+1]) / ↑(b+1) : Int) = -[a / succ b +1] := rfl

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -92,9 +92,6 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natA
 
 @[simp, norm_cast] theorem natCast_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
 
-@[deprecated natCast_emod (since := "2025-04-17")]
-theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := natCast_emod m n
-
 /-! ### mod definitions -/
 
 theorem emod_add_mul_ediv : ∀ a b : Int, a % b + b * (a / b) = a
@@ -233,10 +230,6 @@ theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
 @[simp] theorem mul_add_emod_self_left (a b c : Int) : (a * b + c) % a = c % a := by
   rw [Int.add_comm, add_mul_emod_self_left]
 
-@[deprecated add_mul_emod_self_right (since := "2025-04-11")]
-theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
-  add_mul_emod_self_right ..
-
 @[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
   have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
   rwa [Int.add_right_comm, emod_add_mul_ediv] at this

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -6,13 +6,7 @@ Authors: Jeremy Avigad, Mario Carneiro, Kim Morrison, Markus Himmel
 module
 
 prelude
-public import Init.Data.Int.DivMod.Bootstrap
-public import Init.Data.Nat.Lemmas
 public import Init.Data.Nat.Div.Lemmas
-public import Init.Data.Int.Order
-public import Init.Data.Int.Lemmas
-public import Init.Data.Nat.Dvd
-public import Init.RCases
 import Init.TacticsExtra
 
 public section
@@ -516,9 +510,6 @@ theorem ediv_neg_of_neg_of_pos {a b : Int} (Ha : a < 0) (Hb : 0 < b) : a / b < 0
   match a, b, eq_negSucc_of_lt_zero Ha, eq_succ_of_zero_lt Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => negSucc_lt_zero _
 
-@[deprecated ediv_neg_of_neg_of_pos (since := "2025-03-04")]
-abbrev ediv_neg' := @ediv_neg_of_neg_of_pos
-
 theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(ediv m b + 1) :=
   match b, eq_succ_of_zero_lt H with
   | _, ⟨_, rfl⟩ => rfl
@@ -551,9 +542,6 @@ theorem ediv_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a / b
 theorem ediv_nonpos_of_nonneg_of_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0 :=
   Int.nonpos_of_neg_nonneg <| Int.ediv_neg .. ▸ Int.ediv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
 
-@[deprecated ediv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
-abbrev ediv_nonpos := @ediv_nonpos_of_nonneg_of_nonpos
-
 theorem ediv_eq_zero_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a / b = 0 :=
   match a, b, eq_ofNat_of_zero_le H1, eq_succ_of_zero_lt (Int.lt_of_le_of_lt H1 H2) with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg Nat.cast <| Nat.div_eq_of_lt <| ofNat_lt.1 H2
@@ -684,25 +672,15 @@ theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl
 @[simp] theorem add_neg_mul_emod_self_right (a b c : Int) : (a + -(b * c)) % c = a % c := by
   rw [Int.neg_mul_eq_neg_mul, add_mul_emod_self_right]
 
-@[deprecated add_neg_mul_emod_self_right (since := "2025-04-11")]
-theorem add_neg_mul_emod_self {a b c : Int} : (a + -(b * c)) % c = a % c :=
-  add_neg_mul_emod_self_right ..
-
 @[simp] theorem add_neg_mul_emod_self_left (a b c : Int) : (a + -(b * c)) % b = a % b := by
   rw [Int.neg_mul_eq_mul_neg, add_mul_emod_self_left]
 
 @[simp] theorem add_emod_right (a b : Int) : (a + b) % b = a % b := by
   have := add_mul_emod_self_left a b 1; rwa [Int.mul_one] at this
 
-@[deprecated add_emod_right (since := "2025-04-11")]
-theorem add_emod_self {a b : Int} : (a + b) % b = a % b := add_emod_right ..
-
 @[simp] theorem add_emod_left (a b : Int) : (a + b) % a = b % a := by
   rw [Int.add_comm, add_emod_right]
 
-@[deprecated add_emod_left (since := "2025-04-11")]
-theorem add_emod_self_left {a b : Int} : (a + b) % a = b % a := add_emod_left ..
-
 @[simp] theorem sub_mul_emod_self_right (a b c : Int) : (a - b * c) % c = a % c := by
   simp [Int.sub_eq_add_neg]
 
@@ -943,9 +921,6 @@ where
   | -[_+1], 0 => Nat.zero_le _
   | -[_+1], succ _ => Nat.succ_le_succ (Nat.div_le_self _ _)
 
-@[deprecated natAbs_ediv_le_natAbs (since := "2025-03-05")]
-abbrev natAbs_div_le_natAbs := natAbs_ediv_le_natAbs
-
 theorem ediv_le_self {a : Int} (b : Int) (Ha : 0 ≤ a) : a / b ≤ a := by
   have := Int.le_trans le_natAbs (ofNat_le.2 <| natAbs_ediv_le_natAbs a b)
   rwa [natAbs_of_nonneg Ha] at this
@@ -978,14 +953,6 @@ theorem emod_eq_iff {a b c : Int} (hb : b ≠ 0) : a % b = c ↔ 0 ≤ c ∧ c <
   rw [← dvd_iff_emod_eq_zero, Int.dvd_neg]
   exact Int.dvd_mul_right a b
 
-@[deprecated mul_ediv_cancel (since := "2025-03-05")]
-theorem neg_mul_ediv_cancel (a b : Int) (h : b ≠ 0) : -(a * b) / b = -a := by
-  rw [neg_ediv_of_dvd (Int.dvd_mul_left a b), mul_ediv_cancel _ h]
-
-@[deprecated mul_ediv_cancel (since := "2025-03-05")]
-theorem neg_mul_ediv_cancel_left (a b : Int) (h : a ≠ 0) : -(a * b) / a = -b := by
-  rw [neg_ediv_of_dvd (Int.dvd_mul_right a b), mul_ediv_cancel_left _ h]
-
 @[simp] theorem ediv_one : ∀ a : Int, a / 1 = a
   | (_:Nat) => congrArg Nat.cast (Nat.div_one _)
   | -[_+1]  => congrArg negSucc (Nat.div_one _)
@@ -999,10 +966,6 @@ theorem ediv_minus_one (a : Int) : a / (-1) = -a := by
 theorem emod_minus_one (a : Int) : a % (-1) = 0 := by
   simp
 
-@[deprecated sub_emod_right (since := "2025-04-11")]
-theorem emod_sub_cancel (x y : Int) : (x - y) % y = x % y :=
-  sub_emod_right ..
-
 @[simp] theorem add_neg_emod_self (a b : Int) : (a + -b) % b = a % b := by
   rw [Int.add_neg_eq_sub, sub_emod_right]
 
@@ -1013,10 +976,6 @@ theorem emod_sub_cancel (x y : Int) : (x - y) % y = x % y :=
 theorem dvd_self_sub_of_emod_eq {a b : Int} : {c : Int} → a % b = c → b ∣ a - c
   | _, rfl => dvd_self_sub_emod
 
-@[deprecated dvd_self_sub_of_emod_eq (since := "2025-04-12")]
-theorem dvd_sub_of_emod_eq {a b : Int} : {c : Int} → a % b = c → b ∣ a - c :=
-  dvd_self_sub_of_emod_eq
-
 theorem dvd_sub_self_of_emod_eq {a b : Int} : {c : Int} → a % b = c → b ∣ c - a
   | _, rfl => dvd_emod_sub_self
 
@@ -1335,9 +1294,6 @@ theorem tdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0
 protected theorem tdiv_nonpos_of_nonneg_of_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a.tdiv b ≤ 0 :=
   Int.nonpos_of_neg_nonneg <| Int.tdiv_neg .. ▸ Int.tdiv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
 
-@[deprecated Int.tdiv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
-abbrev tdiv_nonpos := @Int.tdiv_nonpos_of_nonneg_of_nonpos
-
 theorem tdiv_eq_zero_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a.tdiv b = 0 :=
   match a, b, eq_ofNat_of_zero_le H1, eq_succ_of_zero_lt (Int.lt_of_le_of_lt H1 H2) with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg Nat.cast <| Nat.div_eq_of_lt <| ofNat_lt.1 H2
@@ -1896,10 +1852,6 @@ theorem le_emod_self_add_one_iff {a b : Int} (h : 0 < b) : b ≤ a % b + 1 ↔ b
         sign_eq_one_of_pos (by omega), Int.mul_add]
       omega
 
-@[deprecated le_emod_self_add_one_iff (since := "2025-04-12")]
-theorem le_mod_self_add_one_iff {a b : Int} (h : 0 < b) : b ≤ a % b + 1 ↔ b ∣ a + 1 :=
-  le_emod_self_add_one_iff h
-
 theorem add_one_tdiv_of_pos {a b : Int} (h : 0 < b) :
     (a + 1).tdiv b = a.tdiv b + if (0 < a + 1 ∧ b ∣ a + 1) ∨ (a < 0 ∧ b ∣ a) then 1 else 0 := by
   match b, h with
@@ -2035,9 +1987,6 @@ theorem fdiv_nonpos_of_nonneg_of_nonpos : ∀ {a b : Int}, 0 ≤ a → b ≤ 0
   | 0, 0, _, _ | 0, -[_+1], _, _ | succ _, 0, _, _ | succ _, -[_+1], _, _ => by
     simp [fdiv, negSucc_le_zero]
 
-@[deprecated fdiv_nonpos_of_nonneg_of_nonpos (since := "2025-03-04")]
-abbrev fdiv_nonpos := @fdiv_nonpos_of_nonneg_of_nonpos
-
 theorem fdiv_neg_of_neg_of_pos : ∀ {a b : Int}, a < 0 → 0 < b → a.fdiv b < 0
   | -[_+1], succ _, _, _ => negSucc_lt_zero _
 
@@ -2156,9 +2105,6 @@ theorem fmod_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a.fmod b :
 theorem fmod_nonneg_of_pos (a : Int) {b : Int} (hb : 0 < b) : 0 ≤ a.fmod b :=
   fmod_eq_emod_of_nonneg _ (Int.le_of_lt hb) ▸ emod_nonneg _ (Int.ne_of_lt hb).symm
 
-@[deprecated fmod_nonneg_of_pos (since := "2025-03-04")]
-abbrev fmod_nonneg' := @fmod_nonneg_of_pos
-
 theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
   fmod_eq_emod_of_nonneg _ (Int.le_of_lt H) ▸ emod_lt_of_pos a H
 
@@ -2168,10 +2114,6 @@ theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
   rw [fmod_eq_emod, add_mul_emod_self_right, fmod_eq_emod]
   simp
 
-@[deprecated add_mul_fmod_self_right (since := "2025-04-11")]
-theorem add_mul_fmod_self {a b c : Int} : (a + b * c).fmod c = a.fmod c :=
-  add_mul_fmod_self_right ..
-
 @[simp] theorem add_mul_fmod_self_left (a b c : Int) : (a + b * c).fmod b = a.fmod b := by
   rw [Int.mul_comm, Int.add_mul_fmod_self_right]
 
@@ -2470,20 +2412,12 @@ theorem dvd_sub_self_of_fmod_eq {a b c : Int} (h : a.fmod b = c) :
 @[simp] theorem fmod_one (a : Int) : a.fmod 1 = 0 := by
   simp [fmod_def, Int.one_mul, Int.sub_self]
 
-@[deprecated sub_fmod_right (since := "2025-04-12")]
-theorem fmod_sub_cancel (x y : Int) : (x - y).fmod y = x.fmod y :=
-  sub_fmod_right _ _
-
 @[simp] theorem add_neg_fmod_self (a b : Int) : (a + -b).fmod b = a.fmod b := by
   rw [Int.add_neg_eq_sub, sub_fmod_right]
 
 @[simp] theorem neg_add_fmod_self (a b : Int) : (-a + b).fmod a = b.fmod a := by
   rw [Int.add_comm, add_neg_fmod_self]
 
-@[deprecated dvd_self_sub_of_fmod_eq (since := "2025-04-12")]
-theorem dvd_sub_of_fmod_eq {a b c : Int} (h : a.fmod b = c) : b ∣ a - c :=
-  dvd_self_sub_of_fmod_eq h
-
 theorem fdiv_sign {a b : Int} : a.fdiv (sign b) = a * sign b := by
   rw [fdiv_eq_ediv]
   rcases sign_trichotomy b with h | h | h <;> simp [h]
@@ -2517,10 +2451,6 @@ theorem lt_mul_fdiv_self_add {x k : Int} (h : 0 < k) : x < k * (x.fdiv k) + k :=
 theorem emod_bmod (x : Int) (n : Nat) : Int.bmod (x%n) n = Int.bmod x n := by
   simp [bmod]
 
-@[deprecated emod_bmod (since := "2025-04-11")]
-theorem emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n) n = Int.bmod x n :=
-  emod_bmod ..
-
 theorem bdiv_add_bmod (x : Int) (m : Nat) : m * bdiv x m + bmod x m = x := by
   unfold bdiv bmod
   split
@@ -2562,9 +2492,6 @@ theorem bmod_eq_emod (x : Int) (m : Nat) : bmod x m = x % m - if x % m ≥ (m +
 theorem bmod_one (x : Int) : Int.bmod x 1 = 0 := by
   simp [Int.bmod]
 
-@[deprecated bmod_one (since := "2025-04-10")]
-abbrev bmod_one_is_zero := @bmod_one
-
 @[simp] theorem add_bmod_right (a : Int) (b : Nat) : (a + b).bmod b = a.bmod b := by
   simp [bmod_def]
 
@@ -2607,76 +2534,36 @@ abbrev bmod_one_is_zero := @bmod_one
 @[simp] theorem add_neg_mul_bmod_self_left (a : Int) (b : Nat) (c : Int) : (a + -(b * c)).bmod b = a.bmod b := by
   simp [bmod_def]
 
-@[deprecated add_bmod_right (since := "2025-04-10")]
-theorem bmod_add_cancel {x : Int} {n : Nat} : Int.bmod (x + n) n = Int.bmod x n :=
-  add_bmod_right ..
-
-@[deprecated add_mul_bmod_self_left (since := "2025-04-10")]
-theorem bmod_add_mul_cancel (x : Int) (n : Nat) (k : Int) : Int.bmod (x + n * k) n = Int.bmod x n :=
-  add_mul_bmod_self_left ..
-
-@[deprecated sub_bmod_right (since := "2025-04-10")]
-theorem bmod_sub_cancel (x : Int) (n : Nat) : Int.bmod (x - n) n = Int.bmod x n :=
-  sub_bmod_right ..
-
-@[deprecated sub_mul_bmod_self_left (since := "2025-04-10")]
-theorem Int.bmod_sub_mul_cancel (x : Int) (n : Nat) (k : Int) : (x - n * k).bmod n = x.bmod n :=
-  sub_mul_bmod_self_left ..
-
 @[simp]
 theorem emod_add_bmod (x : Int) (n : Nat) : Int.bmod (x % n + y) n = Int.bmod (x + y) n := by
   simp [Int.emod_def, Int.sub_eq_add_neg]
   rw [←Int.mul_neg, Int.add_right_comm,  Int.add_mul_bmod_self_left]
 
-@[deprecated emod_add_bmod (since := "2025-04-11")]
-theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x % n + y) n = Int.bmod (x + y) n :=
-  emod_add_bmod ..
-
 @[simp]
 theorem emod_sub_bmod (x : Int) (n : Nat) : Int.bmod (x % n - y) n = Int.bmod (x - y) n := by
   simp only [emod_def, Int.sub_eq_add_neg]
   rw [←Int.mul_neg, Int.add_right_comm,  Int.add_mul_bmod_self_left]
 
-@[deprecated emod_sub_bmod (since := "2025-04-11")]
-theorem emod_sub_bmod_congr (x : Int) (n : Nat) : Int.bmod (x % n - y) n = Int.bmod (x - y) n :=
-  emod_sub_bmod ..
-
 @[simp]
 theorem sub_emod_bmod (x : Int) (n : Nat) : Int.bmod (x - y % n) n = Int.bmod (x - y) n := by
   simp only [emod_def]
   rw [Int.sub_eq_add_neg, Int.neg_sub, Int.sub_eq_add_neg, ← Int.add_assoc, Int.add_right_comm,
     Int.add_mul_bmod_self_left, Int.sub_eq_add_neg]
 
-@[deprecated sub_emod_bmod (since := "2025-04-11")]
-theorem sub_emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x - y % n) n = Int.bmod (x - y) n :=
-  sub_emod_bmod ..
-
 @[simp]
 theorem emod_mul_bmod (x : Int) (n : Nat) : Int.bmod (x % n * y) n = Int.bmod (x * y) n := by
   simp [Int.emod_def, Int.sub_eq_add_neg]
   rw [←Int.mul_neg, Int.add_mul, Int.mul_assoc, Int.add_mul_bmod_self_left]
 
-@[deprecated emod_mul_bmod (since := "2025-04-11")]
-theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x % n * y) n = Int.bmod (x * y) n :=
-  emod_mul_bmod ..
-
 @[simp]
 theorem bmod_add_bmod : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n := by
   have := (@add_mul_bmod_self_left (Int.bmod x n + y) n (bdiv x n)).symm
   rwa [Int.add_right_comm, bmod_add_bdiv] at this
 
-@[deprecated bmod_add_bmod (since := "2025-04-11")]
-theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n :=
-  bmod_add_bmod ..
-
 @[simp]
 theorem bmod_sub_bmod : Int.bmod (Int.bmod x n - y) n = Int.bmod (x - y) n :=
   @bmod_add_bmod x n (-y)
 
-@[deprecated bmod_sub_bmod (since := "2025-04-11")]
-theorem bmod_sub_bmod_congr : Int.bmod (Int.bmod x n - y) n = Int.bmod (x - y) n :=
-  bmod_sub_bmod ..
-
 theorem add_bmod_eq_add_bmod_right (i : Int)
     (H : bmod x n = bmod y n) : bmod (x + i) n = bmod (y + i) n := by
   rw [← bmod_add_bmod, ← @bmod_add_bmod y, H]
@@ -2869,9 +2756,6 @@ theorem bmod_natAbs_add_one (x : Int) (w : x ≠ -1) : x.bmod (x.natAbs + 1) = -
   · rw [sign_eq_one_iff_pos.2 hx]
     exact ⟨by omega, by omega, ⟨-1, by omega⟩⟩
 
-@[deprecated bmod_natAbs_add_one (since := "2025-04-04")]
-abbrev bmod_natAbs_plus_one := @bmod_natAbs_add_one
-
 theorem bmod_self_add_one {x : Nat} : (x : Int).bmod (x + 1) = if x = 0 then 0 else -1 := by
   have := bmod_natAbs_add_one x (by omega)
   simp only [natAbs_natCast] at this
@@ -2992,11 +2876,6 @@ theorem bmod_eq_of_le {n : Int} {m : Nat} (hn' : -(m / 2) ≤ n) (hn : n < (m +
     n.bmod m = n :=
   (Nat.eq_zero_or_pos m).elim (by rintro rfl; simp) (fun hm => by simp_all [bmod_eq_iff])
 
-@[deprecated bmod_eq_of_le (since := "2025-04-11")]
-theorem bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(m / 2) ≤ n) (hn : n < (m + 1) / 2) :
-    n.bmod m = n :=
-  bmod_eq_of_le hn' hn
-
 theorem bmod_bmod_of_dvd {a : Int} {n m : Nat} (hnm : n ∣ m) :
     (a.bmod m).bmod n = a.bmod n := by
   rw [← Int.sub_eq_iff_eq_add.2 (bmod_add_bdiv a m).symm]
@@ -3007,11 +2886,6 @@ theorem bmod_eq_of_le_mul_two {x : Int} {y : Nat} (hle : -y ≤ x * 2) (hlt : x
     x.bmod y = x := by
   apply bmod_eq_of_le (by omega) (by omega)
 
-@[deprecated bmod_eq_of_le_mul_two (since := "2025-04-11")]
-theorem bmod_eq_self_of_le_mul_two {x : Int} {y : Nat} (hle : -y ≤ x * 2) (hlt : x * 2 < y) :
-    x.bmod y = x :=
-  bmod_eq_of_le_mul_two hle hlt
-
 /- ### ediv -/
 
 theorem ediv_lt_self_of_pos_of_ne_one {x y : Int} (hx : 0 < x) (hy : y ≠ 1) :

src/Init/Data/Int/Gcd.lean

@@ -6,8 +6,6 @@ Authors: Mario Carneiro, Markus Himmel
 module
 
 prelude
-public import Init.Data.Int.Basic
-public import Init.Data.Nat.Gcd
 public import Init.Data.Nat.Lcm
 public import Init.Data.Int.DivMod.Lemmas
 public import Init.Data.Int.Pow

src/Init/Data/Int/Lemmas.lean

@@ -6,8 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module
 
 prelude
-public import Init.Conv
-public import Init.NotationExtra
 public import Init.PropLemmas
 
 public section
@@ -76,9 +74,6 @@ theorem negSucc_inj : negSucc m = negSucc n ↔ m = n := ⟨negSucc.inj, fun H =
 
 theorem negSucc_eq (n : Nat) : -[n+1] = -((n : Int) + 1) := rfl
 
-@[deprecated negSucc_eq (since := "2025-03-11")]
-theorem negSucc_coe (n : Nat) : -[n+1] = -↑(n + 1) := rfl
-
 @[simp] theorem negSucc_ne_zero (n : Nat) : -[n+1] ≠ 0 := nofun
 
 @[simp] theorem zero_ne_negSucc (n : Nat) : 0 ≠ -[n+1] := nofun
@@ -355,10 +350,6 @@ protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
     change ofNat (n - succ m) = subNatNat n (succ m)
     rw [subNatNat, Nat.sub_eq_zero_of_le h]
 
-@[deprecated negSucc_eq (since := "2025-03-11")]
-theorem negSucc_coe' (n : Nat) : -[n+1] = -↑n - 1 := by
-  rw [Int.sub_eq_add_neg, ← Int.neg_add]; rfl
-
 protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = ↑m - ↑n := by
   apply subNatNat_elim m n fun m n i => i = m - n
   · intro i n

src/Init/Data/Int/LemmasAux.lean

@@ -6,9 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Int.Order
 public import Init.Data.Int.Pow
-public import Init.Omega
 
 public section
 
@@ -120,14 +118,8 @@ theorem pos_iff_toNat_pos {n : Int} : 0 < n ↔ 0 < n.toNat := by
 
 theorem natCast_toNat_eq_self {a : Int} : a.toNat = a ↔ 0 ≤ a := by omega
 
-@[deprecated natCast_toNat_eq_self (since := "2025-04-16")]
-theorem ofNat_toNat_eq_self {a : Int} : a.toNat = a ↔ 0 ≤ a := natCast_toNat_eq_self
-
 theorem eq_natCast_toNat {a : Int} : a = a.toNat ↔ 0 ≤ a := by omega
 
-@[deprecated eq_natCast_toNat (since := "2025-04-16")]
-theorem eq_ofNat_toNat {a : Int} : a = a.toNat ↔ 0 ≤ a := eq_natCast_toNat
-
 theorem toNat_le_toNat {n m : Int} (h : n ≤ m) : n.toNat ≤ m.toNat := by omega
 theorem toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m := by omega
 

src/Init/Data/Int/Linear.lean

@@ -6,15 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.ByCases
-public import Init.Data.Prod
-public import Init.Data.Int.Lemmas
 public import Init.Data.Int.LemmasAux
-public import Init.Data.Int.DivMod.Bootstrap
 public import Init.Data.Int.Cooper
-public import Init.Data.Int.Gcd
 import all Init.Data.Int.Gcd
-public import Init.Data.RArray
 public import Init.Data.AC
 import all Init.Data.AC
 import Init.LawfulBEqTactics

src/Init/Data/Int/OfNat.lean

@@ -6,11 +6,8 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.Int.Lemmas
-public import Init.Data.Int.DivMod
 public import Init.Data.Int.Linear
 public import Init.GrindInstances.ToInt
-public import Init.Data.RArray
 
 public section
 

src/Init/Data/Int/Order.lean

@@ -234,9 +234,6 @@ theorem eq_natAbs_of_nonneg {a : Int} (h : 0 ≤ a) : a = natAbs a := by
   let ⟨n, e⟩ := eq_ofNat_of_zero_le h
   rw [e]; rfl
 
-@[deprecated eq_natAbs_of_nonneg (since := "2025-03-11")]
-abbrev eq_natAbs_of_zero_le := @eq_natAbs_of_nonneg
-
 theorem le_natAbs {a : Int} : a ≤ natAbs a :=
   match Int.le_total 0 a with
   | .inl h => by rw [eq_natAbs_of_nonneg h]; apply Int.le_refl
@@ -554,9 +551,6 @@ protected theorem mul_le_mul_of_nonpos_left {a b c : Int}
 
 @[simp, norm_cast] theorem natAbs_natCast (n : Nat) : natAbs ↑n = n := rfl
 
-@[deprecated natAbs_natCast (since := "2025-04-16")]
-theorem natAbs_ofNat (n : Nat) : natAbs ↑n = n := natAbs_natCast n
-
 /-
 TODO: rename `natAbs_ofNat'` to `natAbs_ofNat` once the current deprecated alias
 `natAbs_ofNat := natAbs_natCast` is removed
@@ -646,17 +640,11 @@ theorem toNat_of_nonneg {a : Int} (h : 0 ≤ a) : (toNat a : Int) = a := by
 
 @[simp] theorem toNat_natCast (n : Nat) : toNat ↑n = n := rfl
 
-@[deprecated toNat_natCast (since := "2025-04-16")]
-theorem toNat_ofNat (n : Nat) : toNat ↑n = n := rfl
-
 @[simp] theorem toNat_negSucc (n : Nat) : (Int.negSucc n).toNat = 0 := by
   simp [toNat]
 
 @[simp] theorem toNat_natCast_add_one {n : Nat} : ((n : Int) + 1).toNat = n + 1 := rfl
 
-@[deprecated toNat_natCast_add_one (since := "2025-04-16")]
-theorem toNat_ofNat_add_one {n : Nat} : ((n : Int) + 1).toNat = n + 1 := toNat_natCast_add_one
-
 @[simp] theorem ofNat_toNat (a : Int) : (a.toNat : Int) = max a 0 := by
   match a with
   | (n : Nat) => simp
@@ -717,9 +705,6 @@ theorem mem_toNat? : ∀ {a : Int} {n : Nat}, toNat? a = some n ↔ a = n
   | (m : Nat), n => by simp [toNat?, Int.ofNat_inj]
   | -[m+1], n => by constructor <;> nofun
 
-@[deprecated mem_toNat? (since := "2025-03-11")]
-abbrev mem_toNat' := @mem_toNat?
-
 /-! ## Order properties of the integers -/
 
 protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_total a b).resolve_left
@@ -1259,18 +1244,10 @@ theorem natAbs_sign (z : Int) : z.sign.natAbs = if z = 0 then 0 else 1 :=
 theorem natAbs_sign_of_ne_zero {z : Int} (hz : z ≠ 0) : z.sign.natAbs = 1 := by
   rw [Int.natAbs_sign, if_neg hz]
 
-@[deprecated natAbs_sign_of_ne_zero (since := "2025-04-16")]
-theorem natAbs_sign_of_nonzero {z : Int} (hz : z ≠ 0) : z.sign.natAbs = 1 :=
-  natAbs_sign_of_ne_zero hz
-
 theorem sign_natCast_of_ne_zero {n : Nat} (hn : n ≠ 0) : Int.sign n = 1 :=
   match n, Nat.exists_eq_succ_of_ne_zero hn with
   | _, ⟨n, rfl⟩ => Int.sign_of_add_one n
 
-@[deprecated sign_natCast_of_ne_zero (since := "2025-04-16")]
-theorem sign_ofNat_of_nonzero {n : Nat} (hn : n ≠ 0) : Int.sign n = 1 :=
-  sign_natCast_of_ne_zero hn
-
 @[simp] theorem sign_neg (z : Int) : Int.sign (-z) = -Int.sign z := by
   match z with | 0 | succ _ | -[_+1] => rfl
 
@@ -1325,8 +1302,6 @@ theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
     exact Int.le_add_one (natCast_nonneg _)
   | .negSucc _ => simp +decide [sign]
 
-@[deprecated sign_nonneg_iff (since := "2025-03-11")] abbrev sign_nonneg := @sign_nonneg_iff
-
 @[simp] theorem sign_pos_iff : 0 < sign x ↔ 0 < x := by
   match x with
   | 0
@@ -1409,9 +1384,6 @@ theorem natAbs_add_of_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) :
     natAbs_add_of_nonneg (Int.neg_nonneg_of_nonpos ha) (Int.neg_nonneg_of_nonpos hb),
     natAbs_neg (-a), natAbs_neg (-b)]
 
-@[deprecated negSucc_eq (since := "2025-03-11")]
-theorem negSucc_eq' (m : Nat) : -[m+1] = -m - 1 := by simp only [negSucc_eq, Int.neg_add]; rfl
-
 theorem natAbs_lt_natAbs_of_nonneg_of_lt {a b : Int}
     (w₁ : 0 ≤ a) (w₂ : a < b) : a.natAbs < b.natAbs :=
   match a, b, eq_ofNat_of_zero_le w₁, eq_ofNat_of_zero_le (Int.le_trans w₁ (Int.le_of_lt w₂)) with
@@ -1420,9 +1392,6 @@ theorem natAbs_lt_natAbs_of_nonneg_of_lt {a b : Int}
 theorem natAbs_eq_iff_mul_eq_zero : natAbs a = n ↔ (a - n) * (a + n) = 0 := by
   rw [natAbs_eq_iff, Int.mul_eq_zero, ← Int.sub_neg, Int.sub_eq_zero, Int.sub_eq_zero]
 
-@[deprecated natAbs_eq_iff_mul_eq_zero (since := "2025-03-11")]
-abbrev eq_natAbs_iff_mul_eq_zero := @natAbs_eq_iff_mul_eq_zero
-
 instance instIsLinearOrder : IsLinearOrder Int := by
   apply IsLinearOrder.of_le
   case le_antisymm => constructor; apply Int.le_antisymm

src/Init/Data/Int/Pow.lean

@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module
 
 prelude
-public import Init.Data.Int.Lemmas
 public import Init.Data.Nat.Lemmas
 
 public section
@@ -50,10 +49,6 @@ protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := b
 
 instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := ⟨Int.pow_ne_zero (NeZero.ne _)⟩
 
--- This can't be removed until the next update-stage0
-@[deprecated Nat.pow_pos (since := "2025-02-17")]
-abbrev _root_.Nat.pos_pow_of_pos := @Nat.pow_pos
-
 @[simp, norm_cast]
 protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
   match n with

src/Init/Data/Iterators/Basic.lean

@@ -6,11 +6,8 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Core
 public import Init.Classical
 public import Init.Ext
-public import Init.NotationExtra
-public import Init.TacticsExtra
 
 set_option doc.verso true
 
@@ -244,6 +241,16 @@ def IterStep.successor : IterStep α β → Option α
   | .skip it => some it
   | .done => none
 
+@[simp]
+theorem IterStep.successor_yield {it : α} {out : β} :
+  (IterStep.yield it out).successor = some it := rfl
+
+@[simp]
+theorem IterStep.successor_skip {it : α} : (IterStep.skip (β := β) it).successor = some it := rfl
+
+@[simp]
+theorem IterStep.successor_done : (IterStep.done (α := α) (β := β)).successor = none := rfl
+
 /--
 If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
 with the result of the application of `f`.
@@ -546,6 +553,10 @@ def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
     (it' it : Iter (α := α) β) : Prop :=
   it'.toIterM.IsPlausibleSuccessorOf it.toIterM
 
+theorem Iter.isPlausibleSuccessorOf_eq_invImage {α : Type w} {β : Type w} [Iterator α Id β] :
+    IsPlausibleSuccessorOf (α := α) (β := β) =
+      InvImage (IterM.IsPlausibleSuccessorOf (α := α) (β := β) (m := Id)) Iter.toIterM := rfl
+
 theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iterator α Id β]
     {it' it : Iter (α := α) β} :
     it'.IsPlausibleSuccessorOf it ↔ ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step := by
@@ -558,6 +569,16 @@ theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iter
     exact ⟨step.mapIterator Iter.toIterM,
       by cases step <;> simp_all [IterStep.successor, Iter.IsPlausibleStep]⟩
 
+theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_yield {α : Type w} {β : Type w}
+    [Iterator α Id β] {it' it : Iter (α := α) β} {out : β}
+    (h : it.IsPlausibleStep (.yield it' out)) : it'.IsPlausibleSuccessorOf it := by
+  simpa [isPlausibleSuccessorOf_iff_exists] using ⟨.yield it' out, by simp [h]⟩
+
+theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_skip {α : Type w} {β : Type w}
+    [Iterator α Id β] {it' it : Iter (α := α) β} (h : it.IsPlausibleStep (.skip it')) :
+    it'.IsPlausibleSuccessorOf it := by
+  simpa [isPlausibleSuccessorOf_iff_exists] using ⟨.skip it', by simp [h]⟩
+
 /--
 Asserts that a certain iterator `it` could plausibly yield the value `out` after an arbitrary
 number of steps.
@@ -659,6 +680,10 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
 class Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
   wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
 
+theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
+    WellFounded (Iter.IsPlausibleSuccessorOf (α := α)) := by
+  simpa [Iter.isPlausibleSuccessorOf_eq_invImage] using InvImage.wf _ Finite.wf
+
 /--
 This type is a wrapper around `IterM` so that it becomes a useful termination measure for
 recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.finitelyManySteps`.
@@ -708,6 +733,12 @@ theorem IterM.TerminationMeasures.Finite.rel_of_skip
     Rel ⟨it'⟩ ⟨it⟩ := by
   exact .single ⟨_, rfl, h⟩
 
+theorem IterM.TerminationMeasures.Finite.rel_trans
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {it it' it'' : TerminationMeasures.Finite α m} :
+    it.Rel it' → it'.Rel it'' → it.Rel it'' :=
+  .trans
+
 macro_rules | `(tactic| decreasing_trivial) => `(tactic|
   first
   | exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›

src/Init/Data/Iterators/Combinators/Monadic/Attach.lean

@@ -6,9 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Internal.Termination
-public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 
 public section

src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean

@@ -6,8 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Basic
-public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.PostconditionMonad
 public import Init.Data.Iterators.Internal.Termination
@@ -96,7 +94,7 @@ it.filterMapWithPostcondition     ---a'-----c'-------⊥
 **Termination properties:**
 
 * `Finite` instance: only if `it` is finite
-* `Productive` instance: only if `it` is finite`
+* `Productive` instance: only if `it` is finite
 
 For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
 no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then

src/Init/Data/Iterators/Combinators/Monadic/ULift.lean

@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Internal.Termination
 public import Init.Data.Iterators.Consumers.Monadic
 

src/Init/Data/Iterators/Consumers/Access.lean

@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Consumers.Partial
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Iterators.Consumers.Monadic.Access
 

src/Init/Data/Iterators/Consumers/Collect.lean

@@ -6,7 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Consumers.Partial
 public import Init.Data.Iterators.Consumers.Monadic.Collect
 

src/Init/Data/Iterators/Consumers/Loop.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Monadic.Loop
-public import Init.Data.Iterators.Consumers.Partial
 
 public section
 
@@ -203,6 +202,59 @@ def Iter.all {α β : Type w}
     (p : β → Bool) (it : Iter (α := α) β) : Bool :=
   (it.allM (fun x => pure (f := Id) (p x))).run
 
+@[inline]
+def Iter.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m] [Iterator α Id β]
+    [IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (Option γ)) :
+    m (Option γ) :=
+  ForIn.forIn it none (fun x _ => do
+    match ← f x with
+    | none => return .yield none
+    | some fx => return .done (some fx))
+
+@[inline]
+def Iter.Partial.findSomeM? {α β : Type w} {γ : Type x} {m : Type x → Type w'} [Monad m]
+    [Iterator α Id β] [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β)
+    (f : β → m (Option γ)) :
+    m (Option γ) :=
+  ForIn.forIn it none (fun x _ => do
+    match ← f x with
+    | none => return .yield none
+    | some fx => return .done (some fx))
+
+@[inline]
+def Iter.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
+    [IteratorLoop α Id Id] [Finite α Id] (it : Iter (α := α) β) (f : β → Option γ) :
+    Option γ :=
+  Id.run (it.findSomeM? (pure <| f ·))
+
+@[inline]
+def Iter.Partial.findSome? {α β : Type w} {γ : Type x} [Iterator α Id β]
+    [IteratorLoopPartial α Id Id] (it : Iter.Partial (α := α) β) (f : β → Option γ) :
+    Option γ :=
+  Id.run (it.findSomeM? (pure <| f ·))
+
+@[inline]
+def Iter.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
+    [IteratorLoop α Id m] [Finite α Id] (it : Iter (α := α) β) (f : β → m (ULift Bool)) :
+    m (Option β) :=
+  it.findSomeM? (fun x => return if (← f x).down then some x else none)
+
+@[inline]
+def Iter.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α Id β]
+    [IteratorLoopPartial α Id m] (it : Iter.Partial (α := α) β) (f : β → m (ULift Bool)) :
+    m (Option β) :=
+  it.findSomeM? (fun x => return if (← f x).down then some x else none)
+
+@[inline]
+def Iter.find? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
+    [Finite α Id] (it : Iter (α := α) β) (f : β → Bool) : Option β :=
+  Id.run (it.findM? (pure <| .up <| f ·))
+
+@[inline]
+def Iter.Partial.find? {α β : Type w} [Iterator α Id β] [IteratorLoopPartial α Id Id]
+    (it : Iter.Partial (α := α) β) (f : β → Bool) : Option β :=
+  Id.run (it.findM? (pure <| .up <| f ·))
+
 @[always_inline, inline, expose, inherit_doc IterM.size]
 def Iter.size {α : Type w} {β : Type w} [Iterator α Id β] [IteratorSize α Id]
     (it : Iter (α := α) β) : Nat :=

src/Init/Data/Iterators/Consumers/Monadic/Loop.lean

@@ -6,8 +6,6 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.RCases
-public import Init.Data.Iterators.Basic
 public import Init.Data.Iterators.Consumers.Monadic.Partial
 public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction
 
@@ -581,6 +579,60 @@ def IterM.Partial.all {α β : Type w} {m : Type w → Type w'} [Monad m]
     (p : β → Bool) (it : IterM.Partial (α := α) m β) : m (ULift Bool) := do
   it.allM (fun x => pure (.up (p x)))
 
+@[inline]
+def IterM.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → m (Option γ)) :
+    m (Option γ) :=
+  ForIn.forIn it none (fun x _ => do
+    match ← f x with
+    | none => return .yield none
+    | some fx => return .done (some fx))
+
+@[inline]
+def IterM.Partial.findSomeM? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → m (Option γ)) :
+    m (Option γ) :=
+  ForIn.forIn it none (fun x _ => do
+    match ← f x with
+    | none => return .yield none
+    | some fx => return .done (some fx))
+
+@[inline]
+def IterM.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → Option γ) :
+    m (Option γ) :=
+  it.findSomeM? (pure <| f ·)
+
+@[inline]
+def IterM.Partial.findSome? {α β γ : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → Option γ) :
+    m (Option γ) :=
+  it.findSomeM? (pure <| f ·)
+
+@[inline]
+def IterM.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → m (ULift Bool)) :
+    m (Option β) :=
+  it.findSomeM? (fun x => return if (← f x).down then some x else none)
+
+@[inline]
+def IterM.Partial.findM? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → m (ULift Bool)) :
+    m (Option β) :=
+  it.findSomeM? (fun x => return if (← f x).down then some x else none)
+
+@[inline]
+def IterM.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoop α m m] [Finite α m] (it : IterM (α := α) m β) (f : β → Bool) :
+    m (Option β) :=
+  it.findM? (pure <| .up <| f ·)
+
+@[inline]
+def IterM.Partial.find? {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β]
+    [IteratorLoopPartial α m m] (it : IterM.Partial (α := α) m β) (f : β → Bool) :
+    m (Option β) :=
+  it.findM? (pure <| .up <| f ·)
+
 section Size
 
 /--