chore: bump patch version to 1

The namespace cache volumes were running out of space and preventing CI
from running.

.claude/CLAUDE.md

@@ -46,21 +46,6 @@ This PR adds a `num?` parameter to `mkPatternFromTheorem` to control how many
 leading quantifiers are stripped when creating a pattern.
 ```
 
-**Changelog labels:** Add one `changelog-*` label to categorize the PR for release notes:
-- `changelog-language` - Language features and metaprograms
-- `changelog-tactics` - User facing tactics
-- `changelog-server` - Language server, widgets, and IDE extensions
-- `changelog-pp` - Pretty printing
-- `changelog-library` - Library
-- `changelog-compiler` - Compiler, runtime, and FFI
-- `changelog-lake` - Lake
-- `changelog-doc` - Documentation
-- `changelog-ffi` - FFI changes
-- `changelog-other` - Other changes
-- `changelog-no` - Do not include this PR in the release changelog
-
-If you're unsure which label applies, it's fine to omit the label and let reviewers add it.
-
 ## CI Log Retrieval
 
 When CI jobs fail, investigate immediately - don't wait for other jobs to complete. Individual job logs are often available even while other jobs are still running. Try `gh run view <run-id> --log` or `gh run view <run-id> --log-failed`, or use `gh run view <run-id> --job=<job-id>` to target the specific failed job. Sleeping is fine when asked to monitor CI and no failures exist yet, but once any job fails, investigate that failure immediately.

.github/workflows/build-template.yml

@@ -66,16 +66,10 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
-        if: (!endsWith(matrix.os, '-with-cache'))
         uses: actions/checkout@v6
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
-      - name: Namespace Checkout
-        if: endsWith(matrix.os, '-with-cache')
-        uses: namespacelabs/nscloud-checkout-action@v8
-        with:
-          ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once
         run: true
         if: runner.os == 'Linux'
@@ -102,7 +96,7 @@ jobs:
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache
-        uses: actions/cache/restore@v5
+        uses: actions/cache/restore@v4
         with:
           # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
           path: |
@@ -175,7 +169,7 @@ jobs:
         # Caching on cancellation created some mysterious issues perhaps related to improper build
         # shutdown
         if: steps.restore-cache.outputs.cache-hit != 'true' && !cancelled()
-        uses: actions/cache/save@v5
+        uses: actions/cache/save@v4
         with:
           # NOTE: must be in sync with `restore` above
           path: |

.github/workflows/ci.yml

@@ -433,7 +433,7 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v7
+      - uses: actions/download-artifact@v6
         with:
           path: artifacts
       - name: Release
@@ -465,7 +465,7 @@ jobs:
           # Doesn't seem to be working when additionally fetching from lean4-nightly
           #filter: tree:0
           token: ${{ secrets.PUSH_NIGHTLY_TOKEN }}
-      - uses: actions/download-artifact@v7
+      - uses: actions/download-artifact@v6
         with:
           path: artifacts
       - name: Prepare Nightly Release

.github/workflows/pr-release.yml

@@ -20,9 +20,7 @@ on:
 jobs:
   on-success:
     runs-on: ubuntu-latest
-    # Run even if CI fails, as long as build artifacts are available
-    # The "Verify release artifacts exist" step will fail if necessary artifacts are missing
-    if: github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
+    if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
     steps:
       - name: Retrieve information about the original workflow
         uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
@@ -43,19 +41,6 @@ jobs:
           name: build-.*
           name_is_regexp: true
 
-      # Verify artifacts were downloaded before any side effects (tag creation, release deletion).
-      - name: Verify release artifacts exist
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          shopt -s nullglob
-          files=(artifacts/*/*)
-          if [ ${#files[@]} -eq 0 ]; then
-            echo "::error::No artifacts found matching artifacts/*/*"
-            exit 1
-          fi
-          echo "Found ${#files[@]} artifacts to upload:"
-          printf '%s\n' "${files[@]}"
-
       - name: Push tag
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
@@ -77,44 +62,42 @@ jobs:
           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}"
-      - name: Delete existing releases if present
+      - name: Delete existing release if present
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         run: |
-          # Delete any existing releases for this PR.
-          # The short format release is always recreated with the latest commit.
-          # The SHA-suffixed release should be unique per commit, but delete just in case.
+          # Try to delete any existing release for the current PR (just the version without the SHA suffix).
           gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} -y || true
-          gh release delete --repo ${{ github.repository_owner }}/lean4-pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} -y || true
         env:
           GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
-      # We use `gh release create` instead of `softprops/action-gh-release` because
-      # the latter enumerates all releases to check for existing ones, which fails
-      # when the repository has more than 10000 releases (GitHub API pagination limit).
-      # Upstream fix: https://github.com/softprops/action-gh-release/pull/725
       - name: Release (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          # There are coredump files in deeper subdirectories; artifacts/*/* gets the release archives.
-          gh release create \
-            --repo ${{ github.repository_owner }}/lean4-pr-releases \
-            --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}" \
-            --notes "" \
-            pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} \
-            artifacts/*/*
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        with:
+          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }}
+          # There are coredumps files here as well, but all in deeper subdirectories.
+          files: artifacts/*/*
+          fail_on_unmatched_files: true
+          draft: false
+          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
+          repository: ${{ github.repository_owner }}/lean4-pr-releases
         env:
-          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+          # The token used here must have `workflow` privileges.
+          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
       - name: Release (SHA-suffixed format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        run: |
-          gh release create \
-            --repo ${{ github.repository_owner }}/lean4-pr-releases \
-            --title "Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})" \
-            --notes "" \
-            pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }} \
-            artifacts/*/*
+        uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b
+        with:
+          name: Release for PR ${{ steps.workflow-info.outputs.pullRequestNumber }} (${{ steps.workflow-info.outputs.sourceHeadSha }})
+          # There are coredumps files here as well, but all in deeper subdirectories.
+          files: artifacts/*/*
+          fail_on_unmatched_files: true
+          draft: false
+          tag_name: pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}
+          repository: ${{ github.repository_owner }}/lean4-pr-releases
         env:
-          GH_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
+          # The token used here must have `workflow` privileges.
+          GITHUB_TOKEN: ${{ secrets.PR_RELEASES_TOKEN }}
 
       - name: Report release status (short format)
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
@@ -170,18 +153,6 @@ jobs:
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         uses: dcarbone/install-jq-action@v3.2.0
 
-      # Generate a token for posting comments to Lean PRs about mathlib compatibility.
-      # This app is in the leanprover org and installed on leanprover/lean4.
-      - name: Generate GitHub App token for Lean PR comments
-        if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        id: mathlib-comment-token
-        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
-        with:
-          app-id: ${{ secrets.MATHLIB_LEAN_PR_TESTING_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_LEAN_PR_TESTING_PRIVATE_KEY }}
-          owner: leanprover
-          repositories: lean4
-
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD for Mathlib/Batteries
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
@@ -216,9 +187,8 @@ jobs:
 
           if [[ -n "$MESSAGE" ]]; then
             # Check if force-mathlib-ci label is present
-            # Use GITHUB_TOKEN for read-only label fetch (MATHLIB4_COMMENT_BOT is only for posting comments)
             LABELS="$(curl --retry 3 --location --silent \
-                          -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
+                          -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
@@ -239,10 +209,10 @@ jobs:
 
             # Use GitHub API to check if a comment already exists
             existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                                    -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                                     -H "Accept: application/vnd.github.v3+json" \
                                     "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
-                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "mathlib-lean-pr-testing[bot]"))')"
+                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-bot"))')"
             existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
             existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
 
@@ -252,14 +222,14 @@ jobs:
               echo "Posting message to the comments: $MESSAGE"
 
               # Append new result to the existing comment or post a new comment
-              # Use the mathlib-lean-pr-testing app token so Mathlib CI can subsequently edit the comment.
+              # It's essential we use the MATHLIB4_COMMENT_BOT token here, so that Mathlib CI can subsequently edit the comment.
               if [ -z "$existing_comment_id" ]; then
                 INTRO="Mathlib CI status ([docs](https://leanprover-community.github.io/contribute/tags_and_branches.html)):"
                 # Post new comment with a bullet point
                 echo "Posting as new comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X POST \
-                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg intro "$INTRO" --arg val "$MESSAGE" '{"body":($intro + "\n" + $val)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
@@ -268,7 +238,7 @@ jobs:
                 echo "Appending to existing comment at leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments"
                 curl -L -s \
                   -X PATCH \
-                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
+                  -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
                   -H "Accept: application/vnd.github.v3+json" \
                   -d "$(jq --null-input --arg existing "$existing_comment_body" --arg message "$MESSAGE" '{"body":($existing + "\n" + $message)}')" \
                   "https://api.github.com/repos/leanprover/lean4/issues/comments/$existing_comment_id"
@@ -409,18 +379,6 @@ jobs:
       # We next automatically create a Batteries branch using this toolchain.
       # Batteries doesn't itself have a mechanism to report results of CI from this branch back to Lean
       # Instead this is taken care of by Mathlib CI, which will fail if Batteries fails.
-
-      # Generate a token from the mathlib-nightly-testing GitHub App for cross-org access
-      - name: Generate GitHub App token for leanprover-community repos
-        if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
-        id: mathlib-app-token
-        uses: actions/create-github-app-token@3ff1caaa28b64c9cc276ce0a02e2ff584f3900c5 # v2.0.2
-        with:
-          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
-          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
-          owner: leanprover-community
-          repositories: batteries,mathlib4-nightly-testing
-
       - name: Cleanup workspace
         if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
         run: |
@@ -432,7 +390,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: leanprover-community/batteries
-          token: ${{ steps.mathlib-app-token.outputs.token }}
+          token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
           filter: tree:0
@@ -492,7 +450,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: leanprover-community/mathlib4-nightly-testing
-          token: ${{ steps.mathlib-app-token.outputs.token }}
+          token: ${{ secrets.MATHLIB4_BOT }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
           filter: tree:0

.github/workflows/update-stage0.yml

@@ -58,7 +58,7 @@ jobs:
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - name: Restore Cache
       if: env.should_update_stage0 == 'yes'
-      uses: actions/cache/restore@v5
+      uses: actions/cache/restore@v4
       with:
         # NOTE: must be in sync with `restore-cache` in `build-template.yml`
         path: |

CMakeLists.txt

@@ -10,22 +10,22 @@ option(USE_MIMALLOC "use mimalloc" ON)
 get_cmake_property(vars CACHE_VARIABLES)
 foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
-  if(var MATCHES "STAGE0_(.*)")
+  if("${var}" MATCHES "STAGE0_(.*)")
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif(var MATCHES "STAGE1_(.*)")
+  elseif("${var}" MATCHES "STAGE1_(.*)")
     list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
-  elseif(currentHelpString MATCHES "No help, variable specified on the command line." OR currentHelpString STREQUAL "")
+  elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
-    if(var MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
+    if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION|LEAN_VERSION_.*|LEAN_SPECIAL_VERSION_DESC")
       # must forward options that generate incompatible .olean format
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-    elseif(var MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
+    elseif("${var}" MATCHES "LLVM*|PKG_CONFIG|USE_LAKE|USE_MIMALLOC")
       list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
     endif()
-  elseif(var MATCHES "USE_MIMALLOC")
+  elseif("${var}" MATCHES "USE_MIMALLOC")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
     list(APPEND STAGE0_ARGS "-D${var}=${${var}}")
-  elseif((var MATCHES "CMAKE_.*") AND NOT (var MATCHES "CMAKE_BUILD_TYPE") AND NOT (var MATCHES "CMAKE_HOME_DIRECTORY"))
+  elseif(("${var}" MATCHES "CMAKE_.*") AND NOT ("${var}" MATCHES "CMAKE_BUILD_TYPE") AND NOT ("${var}" MATCHES "CMAKE_HOME_DIRECTORY"))
     list(APPEND PLATFORM_ARGS "-D${var}=${${var}}")
   endif()
 endforeach()
@@ -34,15 +34,15 @@ include(ExternalProject)
 project(LEAN CXX C)
 
 if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
-  set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
+    set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
 endif()
 
 # Don't do anything with cadical on wasm
-if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   find_program(CADICAL cadical)
   if(NOT CADICAL)
     set(CADICAL_CXX c++)
-    if(CADICAL_USE_CUSTOM_CXX)
+    if (CADICAL_USE_CUSTOM_CXX)
       set(CADICAL_CXX ${CMAKE_CXX_COMPILER})
       # Use same platform flags as for Lean executables, in particular from `prepare-llvm-linux.sh`,
       # but not Lean-specific `LEAN_EXTRA_CXX_FLAGS` such as fsanitize.
@@ -54,51 +54,42 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
       set(CADICAL_CXX "${CCACHE} ${CADICAL_CXX}")
     endif()
     # missing stdio locking API on Windows
-    if(CMAKE_SYSTEM_NAME MATCHES "Windows")
+    if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
       string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
     endif()
     string(APPEND CADICAL_CXXFLAGS " -DNCLOSEFROM")
-    ExternalProject_Add(
-      cadical
+    ExternalProject_add(cadical
       PREFIX cadical
       GIT_REPOSITORY https://github.com/arminbiere/cadical
       GIT_TAG rel-2.1.2
       CONFIGURE_COMMAND ""
-      BUILD_COMMAND
-        $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
-        CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS} LDFLAGS=${CADICAL_LDFLAGS}
+      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk
+        CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
+        CXX=${CADICAL_CXX}
+        CXXFLAGS=${CADICAL_CXXFLAGS}
+        LDFLAGS=${CADICAL_LDFLAGS}
       BUILD_IN_SOURCE ON
-      INSTALL_COMMAND ""
-    )
-    set(
-      CADICAL
-      ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX}
-      CACHE FILEPATH
-      "path to cadical binary"
-      FORCE
-    )
+      INSTALL_COMMAND "")
+    set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX} CACHE FILEPATH "path to cadical binary" FORCE)
     list(APPEND EXTRA_DEPENDS cadical)
   endif()
   list(APPEND CL_ARGS -DCADICAL=${CADICAL})
 endif()
 
-if(USE_MIMALLOC)
-  ExternalProject_Add(
-    mimalloc
+if (USE_MIMALLOC)
+  ExternalProject_add(mimalloc
     PREFIX mimalloc
     GIT_REPOSITORY https://github.com/microsoft/mimalloc
     GIT_TAG v2.2.3
     # just download, we compile it as part of each stage as it is small
     CONFIGURE_COMMAND ""
     BUILD_COMMAND ""
-    INSTALL_COMMAND ""
-  )
+    INSTALL_COMMAND "")
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-if(NOT STAGE1_PREV_STAGE)
-  ExternalProject_Add(
-    stage0
+if (NOT STAGE1_PREV_STAGE)
+  ExternalProject_add(stage0
     SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
     SOURCE_SUBDIR src
     BINARY_DIR stage0
@@ -106,49 +97,38 @@ if(NOT STAGE1_PREV_STAGE)
     # (however, CI will override this as we need to embed the githash into the stage 1 library built
     # by stage 0)
     CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
-    BUILD_ALWAYS
-      ON # cmake doesn't auto-detect changes without a download method
-    INSTALL_COMMAND
-      "" # skip install
+    BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
+    INSTALL_COMMAND ""  # skip install
     DEPENDS ${EXTRA_DEPENDS}
   )
   list(APPEND EXTRA_DEPENDS stage0)
 endif()
-ExternalProject_Add(
-  stage1
+ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS
-    -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0
-    -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS ${EXTRA_DEPENDS}
   STEP_TARGETS configure
 )
-ExternalProject_Add(
-  stage2
+ExternalProject_add(stage2
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage2
-  CMAKE_ARGS
-    -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
-    ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=2 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage1 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage1
   EXCLUDE_FROM_ALL ON
   STEP_TARGETS configure
 )
-ExternalProject_Add(
-  stage3
+ExternalProject_add(stage3
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage3
-  CMAKE_ARGS
-    -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX}
-    ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=3 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage2 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
   DEPENDS stage2
@@ -157,14 +137,24 @@ ExternalProject_Add(
 
 # targets forwarded to appropriate stages
 
-add_custom_target(update-stage0 COMMAND $(MAKE) -C stage1 update-stage0 DEPENDS stage1)
+add_custom_target(update-stage0
+  COMMAND $(MAKE) -C stage1 update-stage0
+  DEPENDS stage1)
 
-add_custom_target(update-stage0-commit COMMAND $(MAKE) -C stage1 update-stage0-commit DEPENDS stage1)
+add_custom_target(update-stage0-commit
+  COMMAND $(MAKE) -C stage1 update-stage0-commit
+  DEPENDS stage1)
 
-add_custom_target(test COMMAND $(MAKE) -C stage1 test DEPENDS stage1)
+add_custom_target(test
+  COMMAND $(MAKE) -C stage1 test
+  DEPENDS stage1)
 
-add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
+add_custom_target(clean-stdlib
+  COMMAND $(MAKE) -C stage1 clean-stdlib
+  DEPENDS stage1)
 
 install(CODE "execute_process(COMMAND make -C stage1 install)")
 
-add_custom_target(check-stage3 COMMAND diff "stage2/bin/lean" "stage3/bin/lean" DEPENDS stage3)
+add_custom_target(check-stage3
+  COMMAND diff "stage2/bin/lean" "stage3/bin/lean"
+  DEPENDS stage3)

doc/dev/release_checklist.md

@@ -218,18 +218,8 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 
 # Writing the release notes
 
-Release notes content is only written for the first release candidate (`-rc1`). For subsequent RCs and stable releases,
-just update the title in the existing release notes file (see "Release notes title format" below).
-
-## Release notes title format
-
-The title in the `#doc (Manual)` line must follow these formats:
-
-- **For -rc1**: `"Lean 4.7.0-rc1 (2024-03-15)"` — Include the RC suffix and the release date
-- **For -rc2, -rc3, etc.**: `"Lean 4.7.0-rc2 (2024-03-20)"` — Update the RC number and date
-- **For stable release**: `"Lean 4.7.0 (2024-04-01)"` — Remove the RC suffix but keep the date
-
-The date should be the actual date when the tag was pushed (or when CI completed and created the release page).
+Release notes are only needed for the first release candidate (`-rc1`). For subsequent RCs and stable releases,
+just update the version number in the title of the existing release notes file.
 
 ## Generating the release notes
 
@@ -283,7 +273,7 @@ open Verso.Genre
 open Verso.Genre.Manual
 open Verso.Genre.Manual.InlineLean
 
-#doc (Manual) "Lean 4.7.0-rc1 (2024-03-15)" =>
+#doc (Manual) "Lean 4.7.0-rc1 (YYYY-MM-DD)" =>
 %%%
 tag := "release-v4.7.0"
 file := "v4.7.0"
@@ -326,27 +316,7 @@ Common errors and fixes:
 
 ## Creating the PR
 
-**Important: Timing with the reference-manual tag**
-
-The reference-manual repository deploys documentation when a version tag is pushed. If you merge
-release notes AFTER the tag is created, the deployed documentation won't include them.
-
-You have two options:
-
-1. **Preferred**: Include the release notes in the same PR as the toolchain bump (or merge the
-   release notes PR before creating the tag). This ensures the tag includes the release notes.
-
-2. **If release notes are merged after the tag**: You must regenerate the tag to trigger a new deployment:
-   ```bash
-   cd /path/to/reference-manual
-   git fetch origin
-   git tag -d v4.7.0-rc1  # Delete local tag
-   git tag v4.7.0-rc1 origin/main  # Create tag at current main (which has release notes)
-   git push origin :refs/tags/v4.7.0-rc1  # Delete remote tag
-   git push origin v4.7.0-rc1  # Push new tag (triggers Deploy workflow)
-   ```
-
-If creating a separate PR for release notes:
+Create a separate PR for the release notes (don't bundle with the toolchain bump PR):
 ```bash
 git checkout -b v4.7.0-release-notes
 git add Manual/Releases/v4_7_0.lean Manual/Releases.lean

script/fmt

@@ -1,13 +0,0 @@
-#!/usr/bin/env bash
-set -euo pipefail
-
-# This script expects to be run from the repo root.
-
-# Format cmake files
-find -regex '.*/CMakeLists\.txt\(\.in\)?\|.*\.cmake\(\.in\)?' \
-  ! -path './build/*' \
-  ! -path "./stage0/*" \
-  -exec \
-    uvx gersemi --in-place --line-length 120 --indent 2 \
-    --definitions src/cmake/Modules/ src/CMakeLists.txt \
-    -- {} +

src/Init.lean

@@ -42,7 +42,7 @@ public import Init.While
 public import Init.Syntax
 public import Init.Internal
 public import Init.Try
-public meta import Init.Try  -- shake: keep (make sure `Try.Config` can be evaluated anywhere)
+public meta import Init.Try  -- make sure `Try.Config` can be evaluated anywhere
 public import Init.BinderNameHint
 public import Init.Task
 public import Init.MethodSpecsSimp

src/Init/BinderNameHint.lean

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

src/Init/BinderPredicates.lean

@@ -6,10 +6,7 @@ Authors: Gabriel Ebner
 module
 
 prelude
-public meta import Init.Grind.Tactics
-public import Init.Notation
-import Init.Meta.Defs
-import Init.NotationExtra
+public import Init.NotationExtra
 
 public section
 

src/Init/ByCases.lean

@@ -6,9 +6,7 @@ Authors: Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public meta import Init.Grind.Tactics
-public import Init.Grind.Tactics
-import Init.SimpLemmas
+public import Init.Classical
 
 public section
 

src/Init/Classical.lean

@@ -142,7 +142,6 @@ is classically true but not constructively. -/
 
 /-- Transfer decidability of `¬ p` to decidability of `p`. -/
 -- This can not be an instance as it would be tried everywhere.
-@[instance_reducible]
 def decidable_of_decidable_not (p : Prop) [h : Decidable (¬ p)] : Decidable p :=
   match h with
   | isFalse h => isTrue (Classical.not_not.mp h)

src/Init/Control.lean

@@ -17,4 +17,3 @@ public import Init.Control.Lawful
 public import Init.Control.StateCps
 public import Init.Control.ExceptCps
 public import Init.Control.MonadAttach
-public import Init.Control.EState

src/Init/Control/Basic.lean

@@ -29,7 +29,7 @@ instance (priority := 500) instForInOfForIn' [ForIn' m ρ α d] : ForIn m ρ α
     (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
     (h : ∀ a m b, f a m b = g a b) :
     forIn' x b f = forIn x b g := by
-  simp [forIn]
+  simp [instForInOfForIn']
   congr
   apply funext
   intro a
@@ -322,8 +322,6 @@ class MonadControl (m : semiOutParam (Type u → Type v)) (n : Type u → Type w
   -/
   restoreM : {α : Type u} → m (stM α) → n α
 
-attribute [reducible] MonadControl.stM
-
 /--
 A way to lift a computation from one monad to another while providing the lifted computation with a
 means of interpreting computations from the outer monad. This provides a means of lifting
@@ -351,8 +349,6 @@ class MonadControlT (m : Type u → Type v) (n : Type u → Type w) where
   -/
   restoreM {α : Type u} : stM α → n α
 
-attribute [reducible] MonadControlT.stM
-
 export MonadControlT (stM liftWith restoreM)
 
 @[always_inline]

src/Init/Control/EState.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.ToString.Basic
-public import Init.Control.State
 
 public section
 universe u v

src/Init/Control/ExceptCps.lean

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

src/Init/Control/Id.lean

@@ -8,6 +8,7 @@ The identity Monad.
 module
 
 prelude
+public import Init.Core
 public import Init.Control.MonadAttach
 
 public section

src/Init/Control/Lawful/Basic.lean

@@ -6,9 +6,7 @@ Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 module
 
 prelude
-public import Init.Control.Id
-public import Init.Grind.Tactics
-import Init.Ext
+public import Init.Ext
 
 public section
 

src/Init/Control/Lawful/Instances.lean

@@ -12,8 +12,6 @@ public import Init.Control.Option
 import all Init.Control.Option
 import all Init.Control.State
 public import Init.Control.StateRef
-public import Init.Control.State
-public import Init.Ext
 
 public section
 
@@ -104,7 +102,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 @[simp] theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) (e : ε) :
     f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β) := by
-  simp only [Functor.map, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
+  simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
     pure_bind]
 
 /-! Note that the `MonadControl` instance for `ExceptT` is not monad-generic. -/
@@ -123,11 +121,6 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 @[simp] theorem run_control [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) :
     ExceptT.run (control f) = f fun x => x.run := run_controlAt f
 
-@[simp, grind =]
-theorem run_adapt [Monad m] (f : ε → ε') (x : ExceptT ε m α)
-    : run (ExceptT.adapt f x : ExceptT ε' m α) = Except.mapError f <$> run x :=
-  rfl
-
 end ExceptT
 
 /-! # Except -/
@@ -474,33 +467,15 @@ namespace EStateM
 @[simp, grind =] theorem run_throw (e : ε) (s : σ):
     EStateM.run (throw e : EStateM ε σ PUnit) s = .error e s := rfl
 
-@[simp, grind =] theorem run_bind (x : EStateM ε σ α) (f : α → EStateM ε σ β)
-    : EStateM.run (x >>= f : EStateM ε σ β) s
-      =
-      match EStateM.run x s with
-      | .ok x s => EStateM.run (f x) s
-      | .error e s => .error e s :=
-  rfl
-
-@[simp, grind =]
-theorem run_adaptExcept (f : ε → ε') (x : EStateM ε σ α) (s : σ)
-    : EStateM.run (EStateM.adaptExcept f x : EStateM ε' σ α) s
-     =
-     match EStateM.run x s with
-     | .ok x s => .ok x s
-     | .error e s => .error (f e) s := by
-  simp only [EStateM.run, EStateM.adaptExcept]
-  cases (x s) <;> rfl
-
 instance : LawfulMonad (EStateM ε σ) := .mk'
   (id_map := fun x => funext <| fun s => by
-    simp only [Functor.map, EStateM.map]
+    dsimp only [EStateM.instMonad, EStateM.map]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
   (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
-    simp only [bind, EStateM.bind]
+    dsimp only [EStateM.instMonad, EStateM.bind]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)

src/Init/Control/Lawful/Lemmas.lean

@@ -7,9 +7,7 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Classical
-public import Init.Ext
-import Init.ByCases
+public import Init.ByCases
 
 public section
 

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

@@ -6,11 +6,9 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Control.Reader
+public import Init.Control.Lawful.Instances
 import Init.Control.Lawful.MonadAttach.Lemmas
-public import Init.Control.Lawful.Basic
-public import Init.Control.State
-public import Init.Control.StateRef
-public import Init.Ext
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ReaderT ρ m) where

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

@@ -6,12 +6,10 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Control.MonadAttach
 import all Init.Control.MonadAttach
-public import Init.Classical
-public import Init.Control.Lawful.Basic
-public import Init.Control.Lawful.MonadLift.Basic
-import Init.Control.Lawful.MonadLift.Lemmas
-import Init.RCases
+public import Init.Control.Lawful.Lemmas
+public import Init.Control.Lawful.MonadLift.Lemmas
 
 public theorem LawfulMonadAttach.canReturn_bind_imp' [Monad m] [LawfulMonad m]
     [MonadAttach m] [LawfulMonadAttach m]

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

@@ -6,7 +6,7 @@ Authors: Quang Dao
 module
 
 prelude
-public import Init.Notation
+public import Init.Control.Basic
 
 public section
 

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

@@ -14,12 +14,8 @@ import all Init.Control.StateRef
 public import Init.Control.StateCps
 import all Init.Control.StateCps
 import all Init.Control.Id
-public import Init.Control.Lawful.MonadLift.Basic
-public import Init.Control.Option
-public import Init.Control.State
-public import Init.Control.StateRef
-import Init.Control.Lawful.Instances
-import Init.Control.Lawful.MonadLift.Lemmas
+public import Init.Control.Lawful.MonadLift.Lemmas
+public import Init.Control.Lawful.Instances
 
 public section
 
@@ -67,7 +63,7 @@ variable [Monad m] [LawfulMonad m]
 @[simp]
 theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
     OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by
-  simp only [bind, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
+  simp only [instMonad, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
     map_bind]
 
 instance : LawfulMonadLift m (OptionT m) where
@@ -83,7 +79,7 @@ variable [Monad m] [LawfulMonad m]
 @[simp]
 theorem lift_bind {α β ε : Type u} (ma : m α) (f : α → m β) :
     ExceptT.lift (ε := ε) (ma >>= f) = ExceptT.lift ma >>= (fun a => ExceptT.lift (f a)) := by
-  simp only [bind, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
+  simp only [instMonad, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
 
 instance : LawfulMonadLift m (ExceptT ε m) where
   monadLift_pure := lift_pure
@@ -93,7 +89,8 @@ instance : LawfulMonadLift (Except ε) (ExceptT ε m) where
   monadLift_pure _ := by
     simp only [MonadLift.monadLift, mk, pure, Except.pure, ExceptT.pure]
   monadLift_bind ma _ := by
-    simp only [bind, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont, Except.bind]
+    simp only [instMonad, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont,
+      Except.instMonad, Except.bind]
     rcases ma with _ | _ <;> simp
 
 end ExceptT

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

@@ -6,9 +6,9 @@ Authors: Quang Dao
 module
 
 prelude
+public import Init.Control.Id
 public import Init.Control.Lawful.Basic
 public import Init.Control.Lawful.MonadLift.Basic
-import Init.Ext
 
 public section
 
@@ -17,7 +17,7 @@ universe u v w
 theorem instMonadLiftTOfMonadLift_instMonadLiftTOfPure [Monad m] [Monad n] {_ : MonadLift m n}
     [LawfulMonadLift m n] : instMonadLiftTOfMonadLift Id m n = Id.instMonadLiftTOfPure := by
   have hext {a b : MonadLiftT Id n} (h : @a.monadLift = @b.monadLift) : a = b := by
-    cases a; cases b; simp [monadLift] at h; simp [h]
+    cases a <;> cases b <;> simp_all
   apply hext
   ext α x
   simp [monadLift, LawfulMonadLift.monadLift_pure]

src/Init/Control/MonadAttach.lean

@@ -6,7 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Core
+public import Init.Control.Basic
 
 set_option linter.all true
 
@@ -70,7 +70,7 @@ information to the return value, except a trivial proof of {name}`True`.
 This instance is used whenever no more useful {name}`MonadAttach` instance can be implemented.
 It always has a {name}`WeaklyLawfulMonadAttach`, but usually no {name}`LawfulMonadAttach` instance.
 -/
-@[expose, instance_reducible]
+@[expose]
 public protected def MonadAttach.trivial {m : Type u → Type v} [Monad m] : MonadAttach m where
   CanReturn _ _ := True
   attach x := (⟨·, .intro⟩) <$> x

src/Init/Control/Option.lean

@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Option.Basic
-public import Init.Control.MonadAttach
+public import Init.Control.Except
 
 public section
 

src/Init/Control/StateCps.lean

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

src/Init/Control/StateRef.lean

@@ -9,7 +9,6 @@ module
 
 prelude
 public import Init.System.ST
-public import Init.Control.Reader
 
 public section
 

src/Init/Conv.lean

@@ -51,10 +51,6 @@ scoped syntax (name := withAnnotateState)
 /-- `skip` does nothing. -/
 syntax (name := skip) "skip" : conv
 
-/-- `cbv` performs simplification that closely mimics call-by-value evaluation,
-using equations associated with definitions and the matchers. -/
-syntax (name := cbv) "cbv" : conv
-
 /--
 Traverses into the left subterm of a binary operator.
 

src/Init/Core.lean

@@ -9,7 +9,6 @@ module
 
 prelude
 public import Init.SizeOf
-public import Init.Tactics
 
 public section
 set_option linter.missingDocs true -- keep it documented
@@ -489,8 +488,6 @@ class HasEquiv (α : Sort u) where
   the notion of equivalence is type-dependent. -/
   Equiv : α → α → Sort v
 
-attribute [reducible] HasEquiv.Equiv
-
 @[inherit_doc] infix:50 " ≈ "  => HasEquiv.Equiv
 
 recommended_spelling "equiv" for "≈" in [HasEquiv.Equiv, «term_≈_»]
@@ -935,14 +932,6 @@ noncomputable def HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sor
 noncomputable def HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} {β : Sort u2} {b : β} (h : a ≍ b) (m : motive a) : motive b :=
   h.rec m
 
-/-- `HEq.ndrec` specialized to homogeneous heterogeneous equality -/
-noncomputable def HEq.homo_ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : a ≍ b) : motive b :=
-  (eq_of_heq h).ndrec m
-
-/-- `HEq.ndrec` specialized to homogeneous heterogeneous equality, symmetric variant -/
-noncomputable def HEq.homo_ndrec_symm.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : b ≍ a) : motive b :=
-  (eq_of_heq h).ndrec_symm m
-
 /-- `HEq.ndrec` variant -/
 noncomputable def HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≍ b) (h₂ : p a) : p b :=
   eq_of_heq h₁ ▸ h₂
@@ -1489,29 +1478,6 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂
 
 /-! # Dependent products -/
 
-instance {α : Type u} {β : α → Type v} [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)] :
-    DecidableEq (Sigma β)
-  | ⟨a₁, b₁⟩, ⟨a₂, b₂⟩ =>
-    match a₁, b₁, a₂, b₂, h₁ a₁ a₂ with
-    | _, b₁, _, b₂, isTrue (Eq.refl _) =>
-      match b₁, b₂, h₂ _ b₁ b₂ with
-      | _, _, isTrue (Eq.refl _) => isTrue rfl
-      | _, _, isFalse n => isFalse fun h ↦
-        Sigma.noConfusion rfl .rfl (heq_of_eq h) fun _ e₂ ↦ n (eq_of_heq e₂)
-    | _, _, _, _, isFalse n => isFalse fun h ↦
-      Sigma.noConfusion rfl .rfl (heq_of_eq h) fun e₁ _ ↦ n (eq_of_heq e₁)
-
-instance {α : Sort u} {β : α → Sort v} [h₁ : DecidableEq α] [h₂ : ∀ a, DecidableEq (β a)] : DecidableEq (PSigma β)
-  | ⟨a₁, b₁⟩, ⟨a₂, b₂⟩ =>
-    match a₁, b₁, a₂, b₂, h₁ a₁ a₂ with
-    | _, b₁, _, b₂, isTrue (Eq.refl _) =>
-      match b₁, b₂, h₂ _ b₁ b₂ with
-      | _, _, isTrue (Eq.refl _) => isTrue rfl
-      | _, _, isFalse n => isFalse fun h ↦
-        PSigma.noConfusion rfl .rfl (heq_of_eq h) fun _ e₂ ↦ n (eq_of_heq e₂)
-    | _, _, _, _, isFalse n => isFalse fun h ↦
-      PSigma.noConfusion rfl .rfl (heq_of_eq h) fun e₁ _ ↦ n (eq_of_heq e₁)
-
 theorem Exists.of_psigma_prop {α : Sort u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x)
   | ⟨x, hx⟩ => ⟨x, hx⟩
 
@@ -2363,10 +2329,8 @@ namespace Lean
 /--
 Depends on the correctness of the Lean compiler, interpreter, and all `[implemented_by ...]` and `[extern ...]` annotations.
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom trustCompiler : True
 
-set_option linter.deprecated false in
 /--
 When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
 The kernel will not use the interpreter if `c` is not a constant.
@@ -2386,13 +2350,11 @@ Recall that the compiler trusts the correctness of all `[implemented_by ...]` an
 If an extern function is executed, then the trusted code base will also include the implementation of the associated
 foreign function.
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 opaque reduceBool (b : Bool) : Bool :=
   -- This ensures that `#print axioms` will track use of `reduceBool`.
   have := trustCompiler
   b
 
-set_option linter.deprecated false in
 /--
 Similar to `Lean.reduceBool` for closed `Nat` terms.
 
@@ -2400,14 +2362,12 @@ Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α)
 The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
 We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection).
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 opaque reduceNat (n : Nat) : Nat :=
   -- This ensures that `#print axioms` will track use of `reduceNat`.
   have := trustCompiler
   n
 
 
-set_option linter.deprecated false in
 /--
 The axiom `ofReduceBool` is used to perform proofs by reflection. See `reduceBool`.
 
@@ -2421,10 +2381,8 @@ external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
 
-set_option linter.deprecated false in
 /--
 The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool`.
 
@@ -2434,7 +2392,6 @@ external type checkers that do not implement this feature.
 Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
 So, you are mainly losing the capability of type checking your development using external checkers.
 -/
-@[deprecated "in-kernel native reduction is deprecated; assert native evaluations with axioms instead" (since := "2026-02-01")]
 axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b
 
 
@@ -2485,7 +2442,7 @@ class IdempotentOp (op : α → α → α) : Prop where
   idempotent : (x : α) → op x x = x
 
 /--
-`LeftIdentity op o` indicates `o` is a left identity of `op`.
+`LeftIdentify op o` indicates `o` is a left identity of `op`.
 
 This class does not require a proof that `o` is an identity, and
 is used primarily for inferring the identity using class resolution.
@@ -2493,7 +2450,7 @@ is used primarily for inferring the identity using class resolution.
 class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 
 /--
-`LawfulLeftIdentity op o` indicates `o` is a verified left identity of
+`LawfulLeftIdentify op o` indicates `o` is a verified left identity of
 `op`.
 -/
 class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extends LeftIdentity op o where
@@ -2501,7 +2458,7 @@ class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extend
   left_id : ∀ a, op o a = a
 
 /--
-`RightIdentity op o` indicates `o` is a right identity `o` of `op`.
+`RightIdentify op o` indicates `o` is a right identity `o` of `op`.
 
 This class does not require a proof that `o` is an identity, and is used
 primarily for inferring the identity using class resolution.
@@ -2509,7 +2466,7 @@ primarily for inferring the identity using class resolution.
 class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 
 /--
-`LawfulRightIdentity op o` indicates `o` is a verified right identity of
+`LawfulRightIdentify op o` indicates `o` is a verified right identity of
 `op`.
 -/
 class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop extends RightIdentity op o where

src/Init/Data/AC.lean

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

src/Init/Data/Array.lean

@@ -30,7 +30,3 @@ public import Init.Data.Array.Erase
 public import Init.Data.Array.Zip
 public import Init.Data.Array.InsertIdx
 public import Init.Data.Array.Extract
-public import Init.Data.Array.MinMax
-public import Init.Data.Array.Nat
-public import Init.Data.Array.Int
-public import Init.Data.Array.Count

src/Init/Data/Array/Attach.lean

@@ -6,10 +6,8 @@ Authors: Joachim Breitner, Mario Carneiro
 module
 
 prelude
+public import Init.Data.Array.Count
 import all Init.Data.List.Attach
-public import Init.Data.Array.Lemmas
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Count
 
 public section
 

src/Init/Data/Array/Basic.lean

@@ -11,9 +11,6 @@ public import Init.Data.List.ToArrayImpl
 import all Init.Data.List.ToArrayImpl
 public import Init.Data.Array.Set
 import all Init.Data.Array.Set
-public import Init.WF
-meta import Init.MetaTypes
-import Init.WFTactics
 
 public section
 

src/Init/Data/Array/BasicAux.lean

@@ -7,9 +7,7 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Set
-public import Init.Util
-import Init.Data.Nat.Linear
+public import Init.Data.Nat.Linear
 
 public section
 

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

@@ -7,10 +7,8 @@ Authors: Mario Carneiro
 module
 
 prelude
+public import Init.Data.List.TakeDrop
 import all Init.Data.Array.Basic
-public import Init.Data.List.Control
-import Init.Data.List.Lemmas
-import Init.Data.List.TakeDrop
 
 public section
 

src/Init/Data/Array/Count.lean

@@ -7,14 +7,8 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-import Init.Grind.Util  -- shake: keep (`@[grind]` dependency)
-public import Init.BinderPredicates
-public import Init.Ext
-public import Init.NotationExtra
-import Init.Data.Array.Lemmas
-import Init.Data.Bool
-import Init.Data.List.Count
-import Init.Data.List.Nat.Count
+public import Init.Data.Array.Lemmas
+public import Init.Data.List.Nat.Count
 
 public section
 
@@ -98,18 +92,6 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
   rcases xs with ⟨xs⟩
   simp
 
-/-- This lemma is only relevant for `grind`. -/
-@[grind ←=]
-theorem _root_.Std.Internal.Array.countP_eq_zero_of_forall {xs : Array α} (h : ∀ x ∈ xs, ¬ p x) : xs.countP p = 0 :=
-  countP_eq_zero.mpr h
-
-/-- This lemma is only relevant for `grind`. -/
-theorem _root_.Std.Internal.Array.not_of_countP_eq_zero_of_mem {xs : Array α} (h : xs.countP p = 0) (h' : x ∈ xs) : ¬ p x :=
-   countP_eq_zero.mp h _ h'
-
-grind_pattern Std.Internal.Array.not_of_countP_eq_zero_of_mem => xs.countP p, x ∈ xs where
-  guard xs.countP p = 0
-
 @[simp] theorem countP_eq_size {p} : countP p xs = xs.size ↔ ∀ a ∈ xs, p a := by
   rcases xs with ⟨xs⟩
   simp

src/Init/Data/Array/DecidableEq.lean

@@ -7,14 +7,8 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Basic
-public import Init.Data.Nat.Lemmas
-import Init.ByCases
-import Init.Classical
-import Init.Data.BEq
-import Init.Data.Bool
-import Init.Data.List.Nat.BEq
-import Init.RCases
+public import Init.Data.BEq
+public import Init.Data.List.Nat.BEq
 
 public section
 

src/Init/Data/Array/Erase.lean

@@ -8,13 +8,6 @@ module
 prelude
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Lemmas
-import Init.Data.Array.Bootstrap
-import Init.Data.Bool
-import Init.Data.List.Erase
-import Init.Data.List.Nat.Basic
-import Init.Data.List.Nat.Erase
-import Init.Data.List.TakeDrop
-import Init.Omega
 
 public section
 

src/Init/Data/Array/Extract.lean

@@ -6,16 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.BinderPredicates
-public import Init.Ext
-public import Init.NotationExtra
-import Init.ByCases
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Lemmas
-import Init.Data.Bool
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.TakeDrop
-import Init.Omega
+public import Init.Data.Array.Lemmas
 
 public section
 

src/Init/Data/Array/FinRange.lean

@@ -6,11 +6,7 @@ Authors: François G. Dorais
 module
 
 prelude
-public import Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.Array.OfFn
-import Init.Data.Fin.Lemmas
-import Init.Omega
+public import Init.Data.Array.OfFn
 
 public section
 

src/Init/Data/Array/Find.lean

@@ -6,22 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.List.Nat.Sum
+public import Init.Data.List.Nat.Find
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Attach
-public import Init.Data.Option.BasicAux
-import Init.ByCases
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.MapIdx
-import Init.Data.Bool
-import Init.Data.Fin.Lemmas
-import Init.Data.List.Count
-import Init.Data.List.Find
-import Init.Data.List.Impl
-import Init.Data.List.Nat.Find
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.TakeDrop
-import Init.Omega
+public import Init.Data.Array.Range
 
 public section
 
@@ -127,7 +114,7 @@ theorem getElem_zero_flatten.proof {xss : Array (Array α)} (h : 0 < xss.flatten
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
     List.findSome?_isSome_iff, isSome_getElem?]
   simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
-    List.sum_pos_iff_exists_pos_nat, List.mem_map] at h
+    Nat.sum_pos_iff_exists_pos, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
   exact ⟨xs, m, by simpa using h⟩
 
@@ -687,39 +674,6 @@ theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
   simp only [Option.map_map, Function.comp_def, Fin.cast_cast]
   simp [Array.size]
 
-/-! ### find? and findFinIdx? -/
-
-theorem find?_eq_map_findFinIdx?_getElem {xs : Array α} {p : α → Bool} :
-    xs.find? p = (xs.findFinIdx? p).map (xs[·]) := by
-  cases xs
-  simp [List.find?_eq_map_findFinIdx?_getElem]
-  rfl
-
-theorem find?_eq_bind_findIdx?_getElem? {xs : Array α} {p : α → Bool} :
-    xs.find? p = (xs.findIdx? p).bind (xs[·]?) := by
-  cases xs
-  simp [List.find?_eq_bind_findIdx?_getElem?]
-
-theorem find?_eq_getElem?_findIdx {xs : Array α} {p : α → Bool} :
-    xs.find? p = xs[xs.findIdx p]? := by
-  cases xs
-  simp [List.find?_eq_getElem?_findIdx]
-
-theorem findIdx?_eq_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
-    xs.findIdx? p = (xs.find? p).bind (xs.idxOf? ·) := by
-  cases xs
-  simp [List.findIdx?_eq_bind_find?_idxOf?]
-
-theorem findFinIdx?_eq_bind_find?_finIdxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
-    xs.findFinIdx? p = (xs.find? p).bind (xs.finIdxOf? ·) := by
-  cases xs
-  simp [List.findFinIdx?_eq_bind_find?_finIdxOf?]
-
-theorem findIdx_eq_getD_bind_find?_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} :
-    xs.findIdx p = ((xs.find? p).bind (xs.idxOf? ·)).getD xs.size := by
-  cases xs
-  simp [List.findIdx_eq_getD_bind_find?_idxOf?]
-
 /-! ### idxOf
 
 The verification API for `idxOf` is still incomplete.

src/Init/Data/Array/GetLit.lean

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

src/Init/Data/Array/InsertIdx.lean

@@ -6,11 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Basic
-import Init.Data.List.Nat.InsertIdx
-import Init.Data.List.ToArray
-import Init.Data.Nat.Lemmas
-import Init.Omega
+public import Init.Data.Array.Lemmas
 
 public section
 

src/Init/Data/Array/Int.lean

@@ -1,34 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Sebastian Graf, Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.Int.Lemmas
-import Init.Data.List.Int.Sum
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace Array
-
-@[simp] theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
-  rw [← List.toArray_replicate, List.sum_toArray]
-  simp
-
-theorem sum_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [sum_append]
-
-theorem sum_reverse_int (xs : Array Int) : xs.reverse.sum = xs.sum := by
-  simp [sum_reverse]
-
-theorem sum_eq_foldl_int {xs : Array Int} : xs.sum = xs.foldl (init := 0) (· + ·) := by
-  simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
-
-end Array

src/Init/Data/Array/Lemmas.lean

@@ -6,28 +6,14 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Nat.Basic
+public import Init.Data.Array.Mem
+public import Init.Data.Array.DecidableEq
+public import Init.Data.Range.Lemmas
 public import Init.Data.List.ToArray
 import all Init.Data.List.Control
 import all Init.Data.Array.Basic
 import all Init.Data.Array.Bootstrap
-public import Init.Data.Nat.Lemmas
-public import Init.Data.Nat.MinMax
-import Init.ByCases
-import Init.Data.Array.DecidableEq
-import Init.Data.Bool
-import Init.Data.Fin.Lemmas
-import Init.Data.List.Find
-import Init.Data.List.Nat.Basic
-import Init.Data.List.Nat.Modify
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Range
-import Init.Data.List.Zip
-import Init.Data.Nat.Linear
-import Init.Data.Nat.Simproc
-import Init.Data.Option.Lemmas
-import Init.Data.Prod
-import Init.Omega
-import Init.TacticsExtra
 
 public section
 
@@ -496,18 +482,9 @@ theorem mem_iff_getElem {a} {xs : Array α} : a ∈ xs ↔ ∃ (i : Nat) (h : i
 theorem mem_iff_getElem? {a} {xs : Array α} : a ∈ xs ↔ ∃ i : Nat, xs[i]? = some a := by
   simp [getElem?_eq_some_iff, mem_iff_getElem]
 
-theorem exists_mem_iff_exists_getElem {P : α → Prop} {xs : Array α} :
-    (∃ x ∈ xs, P x) ↔ ∃ (i : Nat), ∃ (hi : i < xs.size), P (xs[i]) := by
-  cases xs; simp [List.exists_mem_iff_exists_getElem]
-
-theorem forall_mem_iff_forall_getElem {P : α → Prop} {xs : Array α} :
-    (∀ x ∈ xs, P x) ↔ ∀ (i : Nat) (hi : i < xs.size), P (xs[i]) := by
-  cases xs; simp [List.forall_mem_iff_forall_getElem]
-
-@[deprecated forall_mem_iff_forall_getElem (since := "2026-01-29")]
 theorem forall_getElem {xs : Array α} {p : α → Prop} :
     (∀ (i : Nat) h, p (xs[i]'h)) ↔ ∀ a, a ∈ xs → p a := by
-  exact forall_mem_iff_forall_getElem.symm
+  cases xs; simp [List.forall_getElem]
 
 /-! ### isEmpty -/
 
@@ -1992,14 +1969,6 @@ theorem append_eq_append_iff {ws xs ys zs : Array α} :
     · left; exact ⟨as.toList, by simp⟩
     · right; exact ⟨cs.toList, by simp⟩
 
-theorem append_eq_append_iff_of_size_eq_left {ws xs ys zs : Array α} (h : ws.size = xs.size) :
-    ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  simpa [← Array.toList_inj] using List.append_eq_append_iff_of_size_eq_left h
-
-theorem append_eq_append_iff_of_size_eq_right {ws xs ys zs : Array α} (h : ys.size = zs.size) :
-    ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  simpa [← Array.toList_inj] using List.append_eq_append_iff_of_size_eq_right h
-
 @[grind =] theorem set_append {xs ys : Array α} {i : Nat} {x : α} (h : i < (xs ++ ys).size) :
     (xs ++ ys).set i x =
       if h' : i < xs.size then
@@ -2531,6 +2500,10 @@ theorem flatMap_replicate {f : α → Array β} : (replicate n a).flatMap f = (r
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
+@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
+  rw [← List.toArray_replicate, List.sum_toArray]
+  simp
+
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
 @[grind =]
@@ -3092,18 +3065,6 @@ theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop :
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Array α} {start stop : Nat} :
     xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
-public theorem foldl_eq_foldl_extract {xs : Array α} {f : β → α → β} {init : β} :
-    xs.foldl (init := init) (start := start) (stop := stop) f =
-      (xs.extract start stop).foldl (init := init) f := by
-  simp only [foldl_eq_foldlM]
-  rw [foldlM_start_stop]
-
-public theorem foldr_eq_foldr_extract {xs : Array α} {f : α → β → β} {init : β} :
-    xs.foldr (init := init) (start := start) (stop := stop) f =
-      (xs.extract stop start).foldr (init := init) f := by
-  simp only [foldr_eq_foldrM]
-  rw [foldrM_start_stop]
-
 @[simp] theorem id_run_foldlM {f : β → α → Id β} {b} {xs : Array α} {start stop : Nat} :
     Id.run (xs.foldlM f b start stop) = xs.foldl (f · · |>.run) b start stop := rfl
 
@@ -4316,31 +4277,19 @@ theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then
 /-! ### sum -/
 
 @[simp, grind =] theorem sum_empty [Add α] [Zero α] : (#[] : Array α).sum = 0 := rfl
-theorem sum_eq_foldr [Add α] [Zero α] {xs : Array α} :
-    xs.sum = xs.foldr (init := 0) (· + ·) :=
-  rfl
 
 -- Without further algebraic hypotheses, there's no useful `sum_push` lemma.
 
 @[simp, grind =]
-theorem sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
+theorem sum_eq_sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
   cases as
   simp [Array.sum, List.sum]
 
-@[deprecated sum_toList (since := "2026-01-14")]
-def sum_eq_sum_toList := @sum_toList
-
 @[simp, grind =]
-theorem sum_append [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
-    [Std.LeftIdentity (α := α) (· + ·) 0] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
-    {as₁ as₂ : Array α} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [← sum_toList, List.sum_append]
-
-@[simp, grind =]
-theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
-    [Std.Commutative (α := α) (· + ·)]
-    [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : Array α) : xs.reverse.sum = xs.sum := by
-  simp [← sum_toList, List.sum_reverse]
+theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+  cases as₁
+  cases as₂
+  simp [List.sum_append_nat]
 
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}

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

@@ -6,10 +6,9 @@ Author: Kim Morrison
 module
 
 prelude
-public import Init.Data.Range.Polymorphic.RangeIterator
-import Init.Data.Range.Polymorphic.Iterators
-import Init.Data.Range.Polymorphic.Nat
-import Init.Omega
+public import Init.Data.Range.Polymorphic.Iterators
+public import Init.Data.Range.Polymorphic.Nat
+import Init.Data.Iterators.Consumers
 
 public section
 

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

@@ -8,13 +8,9 @@ module
 prelude
 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.NatLemmas
-public import Init.Data.BEq
-import Init.Data.Array.DecidableEq
-import Init.Data.Array.Lemmas
-import Init.Data.Bool
-import Init.Data.List.Lex
-import Init.Data.Range.Polymorphic.Lemmas
 
 public section
 

src/Init/Data/Array/MapIdx.lean

@@ -7,9 +7,9 @@ module
 
 prelude
 import all Init.Data.Array.Basic
+public import Init.Data.Array.OfFn
 public import Init.Data.List.MapIdx
 import all Init.Data.List.MapIdx
-import Init.Data.Array.OfFn
 
 public section
 

src/Init/Data/Array/Mem.lean

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

src/Init/Data/Array/MinMax.lean

@@ -1,403 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Paul Reichert
--/
-module
-
-prelude
-public import Init.Data.Array.Lemmas
-import Init.Data.List.MinMax
-public import Init.Data.Order.Classes
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.DecidableEq
-import Init.Data.List.TakeDrop
-import Init.Data.Order.Lemmas
-
-namespace Array
-
-/-! ## Minima and maxima -/
-
-/-! ### min -/
-
-/--
-Returns the smallest element of a non-empty array.
-
-Examples:
-* `#[4].min (by decide) = 4`
-* `#[1, 4, 2, 10, 6].min (by decide) = 1`
--/
-public protected def min [Min α] (arr : Array α) (h : arr ≠ #[]) : α :=
-  haveI : arr.size > 0 := by simp [Array.size_pos_iff, h]
-  arr.foldl min arr[0] (start := 1)
-
-/-! ### min? -/
-
-/--
-Returns the smallest element of the array if it is not empty, or `none` if it is empty.
-
-Examples:
-* `#[].min? = none`
-* `#[4].min? = some 4`
-* `#[1, 4, 2, 10, 6].min? = some 1`
--/
-public protected def min? [Min α] (arr : Array α) : Option α :=
-  if h : arr ≠ #[] then
-    some (arr.min h)
-  else
-    none
-
-/-! ### max -/
-
-/--
-Returns the largest element of a non-empty array.
-
-Examples:
-* `#[4].max (by decide) = 4`
-* `#[1, 4, 2, 10, 6].max (by decide) = 10`
--/
-public protected def max [Max α] (arr : Array α) (h : arr ≠ #[]) : α :=
-  haveI : arr.size > 0 := by simp [Array.size_pos_iff, h]
-  arr.foldl max arr[0] (start := 1)
-
-/-! ### max? -/
-
-/--
-Returns the largest element of the array if it is not empty, or `none` if it is empty.
-
-Examples:
-* `#[].max? = none`
-* `#[4].max? = some 4`
-* `#[1, 4, 2, 10, 6].max? = some 10`
--/
-public protected def max? [Max α] (arr : Array α) : Option α :=
-  if h : arr ≠ #[] then
-    some (arr.max h)
-  else
-    none
-
-/-! ### Compatibility with `List` -/
-
-@[simp, grind =]
-public theorem _root_.List.min_toArray [Min α] {l : List α} {h} :
-    l.toArray.min h = l.min (by simpa [List.ne_nil_iff_length_pos] using h) := by
-  let h' : l ≠ [] := by simpa [List.ne_nil_iff_length_pos] using h
-  change l.toArray.min h = l.min h'
-  rw [Array.min]
-  · induction l
-    · contradiction
-    · rename_i x xs
-      simp only [List.getElem_toArray, List.getElem_cons_zero, List.size_toArray, List.length_cons]
-      rw [List.toArray_cons, foldl_eq_foldl_extract]
-      rw [← Array.foldl_toList, Array.toList_extract, List.extract_eq_drop_take]
-      simp [List.min]
-
-public theorem _root_.List.min_eq_min_toArray [Min α] {l : List α} {h} :
-    l.min h = l.toArray.min (by simpa [List.ne_nil_iff_length_pos] using h) := by
-  simp
-
-@[simp, grind =]
-public theorem min_toList [Min α] {xs : Array α} {h} :
-    xs.toList.min h = xs.min (by simpa [List.ne_nil_iff_length_pos] using h) := by
-  cases xs; simp
-
-public theorem min_eq_min_toList [Min α] {xs : Array α} {h} :
-    xs.min h = xs.toList.min (by simpa [List.ne_nil_iff_length_pos] using h) := by
-  simp
-
-@[simp, grind =]
-public theorem _root_.List.min?_toArray [Min α] {l : List α} :
-    l.toArray.min? = l.min? := by
-  rw [Array.min?]
-  split
-  · simp [List.min_toArray, List.min_eq_get_min?, - List.get_min?]
-  · simp_all
-
-@[simp, grind =]
-public theorem min?_toList [Min α] {xs : Array α} :
-    xs.toList.min? = xs.min? := by
-  cases xs; simp
-
-@[simp, grind =]
-public theorem _root_.List.max_toArray [Max α] {l : List α} {h} :
-    l.toArray.max h = l.max (by simpa [List.ne_nil_iff_length_pos] using h) := by
-  let h' : l ≠ [] := by simpa [List.ne_nil_iff_length_pos] using h
-  change l.toArray.max h = l.max h'
-  rw [Array.max]
-  · induction l
-    · contradiction
-    · rename_i x xs
-      simp only [List.getElem_toArray, List.getElem_cons_zero, List.size_toArray, List.length_cons]
-      rw [List.toArray_cons, foldl_eq_foldl_extract]
-      rw [← Array.foldl_toList, Array.toList_extract, List.extract_eq_drop_take]
-      simp [List.max]
-
-public theorem _root_.List.max_eq_max_toArray [Max α] {l : List α} {h} :
-    l.max h = l.toArray.max (by simpa [List.ne_nil_iff_length_pos] using h) := by
-  simp
-
-@[simp, grind =]
-public theorem max_toList [Max α] {xs : Array α} {h} :
-    xs.toList.max h = xs.max (by simpa [List.ne_nil_iff_length_pos] using h) := by
-  cases xs; simp
-
-public theorem max_eq_max_toList [Max α] {xs : Array α} {h} :
-    xs.max h = xs.toList.max (by simpa [List.ne_nil_iff_length_pos] using h) := by
-  simp
-
-@[simp, grind =]
-public theorem _root_.List.max?_toArray [Max α] {l : List α} :
-    l.toArray.max? = l.max? := by
-  rw [Array.max?]
-  split
-  · simp [List.max_toArray, List.max_eq_get_max?, - List.get_max?]
-  · simp_all
-
-@[simp, grind =]
-public theorem max?_toList [Max α] {xs : Array α} :
-    xs.toList.max? = xs.max? := by
-  cases xs; simp
-
-/-! ### Lemmas about `min?` -/
-
-@[simp, grind =]
-public theorem min?_empty [Min α] : (#[] : Array α).min? = none :=
-  (rfl)
-
-@[simp, grind =]
-public theorem min?_singleton [Min α] {x : α} : #[x].min? = some x :=
-  (rfl)
-
--- We don't put `@[simp]` on `min?_singleton_append'`,
--- because the definition in terms of `foldl` is not useful for proofs.
-public theorem min?_singleton_append' [Min α] {xs : Array α} :
-    (#[x] ++ xs).min? = some (xs.foldl min x) := by
-  simp [← min?_toList, toList_append, List.min?]
-
-@[simp]
-public theorem min?_singleton_append [Min α] [Std.Associative (min : α → α → α)] {xs : Array α} :
-    (#[x] ++ xs).min? = some (xs.min?.elim x (min x)) := by
-  simp [← min?_toList, toList_append, List.min?_cons]
-
-@[simp, grind =]
-public theorem min?_eq_none_iff {xs : Array α} [Min α] : xs.min? = none ↔ xs = #[] := by
-  rcases xs with ⟨l⟩
-  simp
-
-@[simp, grind =]
-public theorem isSome_min?_iff {xs : Array α} [Min α] : xs.min?.isSome ↔ xs ≠ #[] := by
-  rcases xs with ⟨l⟩
-  simp
-
-@[grind .]
-public theorem isSome_min?_of_mem {xs : Array α} [Min α] {a : α} (h : a ∈ xs) :
-    xs.min?.isSome := by
-  rw [← min?_toList]
-  apply List.isSome_min?_of_mem (a := a)
-  simpa
-
-public theorem isSome_min?_of_ne_empty [Min α] (xs : Array α) (h : xs ≠ #[]) : xs.min?.isSome := by
-  rw [← min?_toList]
-  apply List.isSome_min?_of_ne_nil
-  simpa
-
-public theorem min?_mem [Min α] [Std.MinEqOr α] (xs : Array α) (h : xs.min? = some a) : a ∈ xs := by
-  rw [← min?_toList] at h
-  simpa using List.min?_mem h
-
-public theorem le_min?_iff [Min α] [LE α] [Std.LawfulOrderInf α] :
-    {xs : Array α} → xs.min? = some a → ∀ {x}, x ≤ a ↔ ∀ b, b ∈ xs → x ≤ b := by
-  intro xs h x
-  simp only [← min?_toList] at h
-  simpa using List.le_min?_iff h
-
-public theorem min?_eq_some_iff [Min α] [LE α] {xs : Array α} [Std.IsLinearOrder α]
-    [Std.LawfulOrderMin α] : xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
-  rcases xs with ⟨l⟩
-  simpa using List.min?_eq_some_iff
-
-public theorem min?_replicate [Min α] [Std.IdempotentOp (min : α → α → α)] {n : Nat} {a : α} :
-    (replicate n a).min? = if n = 0 then none else some a := by
-  rw [← List.toArray_replicate, List.min?_toArray, List.min?_replicate]
-
-@[simp, grind =]
-public theorem min?_replicate_of_pos [Min α] [Std.MinEqOr α] {n : Nat} {a : α} (h : 0 < n) :
-    (replicate n a).min? = some a := by
-  simp [min?_replicate, Nat.ne_of_gt h]
-
-public theorem foldl_min [Min α] [Std.IdempotentOp (min : α → α → α)]
-    [Std.Associative (min : α → α → α)] {xs : Array α} {a : α} :
-    xs.foldl (init := a) min = min a (xs.min?.getD a) := by
-  rcases xs with ⟨l⟩
-  simp [List.foldl_min]
-
-/-! ### Lemmas about `max?` -/
-
-@[simp, grind =]
-public theorem max?_empty [Max α] : (#[] : Array α).max? = none :=
-  (rfl)
-
-@[simp, grind =]
-public theorem max?_singleton [Max α] {x : α} : #[x].max? = some x :=
-  (rfl)
-
--- We don't put `@[simp]` on `max?_singleton_append'`,
--- because the definition in terms of `foldl` is not useful for proofs.
-public theorem max?_singleton_append' [Max α] {xs : Array α} : (#[x] ++ xs).max? = some (xs.foldl max x) := by
-  simp [← max?_toList, toList_append, List.max?]
-
-@[simp]
-public theorem max?_singleton_append [Max α] [Std.Associative (max : α → α → α)] {xs : Array α} :
-    (#[x] ++ xs).max? = some (xs.max?.elim x (max x)) := by
-  simp [← max?_toList, toList_append, List.max?_cons]
-
-@[simp, grind =]
-public theorem max?_eq_none_iff {xs : Array α} [Max α] : xs.max? = none ↔ xs = #[] := by
-  rcases xs with ⟨l⟩
-  simp
-
-@[simp, grind =]
-public theorem isSome_max?_iff {xs : Array α} [Max α] : xs.max?.isSome ↔ xs ≠ #[] := by
-  rcases xs with ⟨l⟩
-  simp
-
-@[grind .]
-public theorem isSome_max?_of_mem {xs : Array α} [Max α] {a : α} (h : a ∈ xs) :
-    xs.max?.isSome := by
-  rw [← max?_toList]
-  apply List.isSome_max?_of_mem (a := a)
-  simpa
-
-public theorem isSome_max?_of_ne_empty [Max α] (xs : Array α) (h : xs ≠ #[]) : xs.max?.isSome := by
-  rw [← max?_toList]
-  apply List.isSome_max?_of_ne_nil
-  simpa
-
-public theorem max?_mem [Max α] [Std.MaxEqOr α] (xs : Array α) (h : xs.max? = some a) : a ∈ xs := by
-  rw [← max?_toList] at h
-  simpa using List.max?_mem h
-
-public theorem max?_le_iff [Max α] [LE α] [Std.LawfulOrderSup α] :
-    {xs : Array α} → xs.max? = some a → ∀ {x}, a ≤ x ↔ ∀ b, b ∈ xs → b ≤ x := by
-  intro xs h x
-  simp only [← max?_toList] at h
-  simpa using List.max?_le_iff h
-
-public theorem max?_eq_some_iff [Max α] [LE α] {xs : Array α} [Std.IsLinearOrder α]
-    [Std.LawfulOrderMax α] : xs.max? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → b ≤ a := by
-  rcases xs with ⟨l⟩
-  simpa using List.max?_eq_some_iff
-
-public theorem max?_replicate [Max α] [Std.IdempotentOp (max : α → α → α)] {n : Nat} {a : α} :
-    (replicate n a).max? = if n = 0 then none else some a := by
-  rw [← List.toArray_replicate, List.max?_toArray, List.max?_replicate]
-
-@[simp, grind =]
-public theorem max?_replicate_of_pos [Max α] [Std.MaxEqOr α] {n : Nat} {a : α} (h : 0 < n) :
-    (replicate n a).max? = some a := by
-  simp [max?_replicate, Nat.ne_of_gt h]
-
-public theorem foldl_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
-    {xs : Array α} {a : α} : xs.foldl (init := a) max = max a (xs.max?.getD a) := by
-  rcases xs with ⟨l⟩
-  simp [List.foldl_max]
-
-/-! ### Lemmas about `min` -/
-
-@[simp, grind =]
-theorem min_singleton [Min α] {x : α} :
-    #[x].min (ne_empty_of_size_eq_add_one rfl) = x := by
-  (rfl)
-
-public theorem min?_eq_some_min [Min α] : {xs : Array α} → (h : xs ≠ #[]) →
-    xs.min? = some (xs.min h)
-  | ⟨a::as⟩, _ => by simp [Array.min, Array.min?]
-
-public theorem min_eq_get_min? [Min α] : (xs : Array α) → (h : xs ≠ #[]) →
-    xs.min h = xs.min?.get (xs.isSome_min?_of_ne_empty h)
-  | ⟨a::as⟩, _ => by simp [Array.min, Array.min?]
-
-@[simp, grind =]
-public theorem get_min? [Min α] {xs : Array α} {h : xs.min?.isSome} :
-    xs.min?.get h = xs.min (isSome_min?_iff.mp h) := by
-  simp [min?_eq_some_min (isSome_min?_iff.mp h)]
-
-@[grind .]
-public theorem min_mem [Min α] [Std.MinEqOr α] {xs : Array α} (h : xs ≠ #[]) : xs.min h ∈ xs :=
-  xs.min?_mem (min?_eq_some_min h)
-
-@[grind .]
-public theorem min_le_of_mem [Min α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMin α]
-    {xs : Array α} {a : α} (ha : a ∈ xs) :
-    xs.min (ne_empty_of_mem ha) ≤ a :=
-  (Array.min?_eq_some_iff.mp (min?_eq_some_min (ne_empty_of_mem ha))).right a ha
-
-public protected theorem le_min_iff [Min α] [LE α] [Std.LawfulOrderInf α]
-    {xs : Array α} (h : xs ≠ #[]) : ∀ {x}, x ≤ xs.min h ↔ ∀ b, b ∈ xs → x ≤ b :=
-  le_min?_iff (min?_eq_some_min h)
-
-public theorem min_eq_iff [Min α] [LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMin α]
-    (h : xs ≠ #[]) : xs.min h = a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
-  simpa [min?_eq_some_min h] using (min?_eq_some_iff (xs := xs))
-
-@[simp, grind =]
-public theorem min_replicate [Min α] [Std.MinEqOr α] {n : Nat} {a : α} (h : (replicate n a) ≠ #[]) :
-    (replicate n a).min h = a := by
-  have n_pos : 0 < n := by simpa [Nat.ne_zero_iff_zero_lt] using h
-  simpa [min?_eq_some_min h] using (min?_replicate_of_pos (a := a) n_pos)
-
-public theorem foldl_min_eq_min [Min α] [Std.IdempotentOp (min : α → α → α)]
-    [Std.Associative (min : α → α → α)] {xs : Array α} (h : xs ≠ #[]) {a : α} :
-    xs.foldl min a = min a (xs.min h) := by
-  simpa [min?_eq_some_min h] using foldl_min (xs := xs)
-
-/-! ### Lemmas about `max` -/
-
-@[simp, grind =]
-theorem max_singleton [Max α] {x : α} :
-    #[x].max (ne_empty_of_size_eq_add_one rfl) = x := by
-  (rfl)
-
-public theorem max?_eq_some_max [Max α] : {xs : Array α} → (h : xs ≠ #[]) →
-    xs.max? = some (xs.max h)
-  | ⟨a::as⟩, _ => by simp [Array.max, Array.max?]
-
-public theorem max_eq_get_max? [Max α] : (xs : Array α) → (h : xs ≠ #[]) →
-    xs.max h = xs.max?.get (xs.isSome_max?_of_ne_empty h)
-  | ⟨a::as⟩, _ => by simp [Array.max, Array.max?]
-
-@[simp, grind =]
-public theorem get_max? [Max α] {xs : Array α} {h : xs.max?.isSome} :
-    xs.max?.get h = xs.max (isSome_max?_iff.mp h) := by
-  simp [max?_eq_some_max (isSome_max?_iff.mp h)]
-
-@[grind .]
-public theorem max_mem [Max α] [Std.MaxEqOr α] {xs : Array α} (h : xs ≠ #[]) : xs.max h ∈ xs :=
-  xs.max?_mem (max?_eq_some_max h)
-
-public protected theorem max_le_iff [Max α] [LE α] [Std.LawfulOrderSup α]
-    {xs : Array α} (h : xs ≠ #[]) : ∀ {x}, xs.max h ≤ x ↔ ∀ b, b ∈ xs → b ≤ x :=
-  max?_le_iff (max?_eq_some_max h)
-
-public theorem max_eq_iff [Max α] [LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMax α]
-    (h : xs ≠ #[]) : xs.max h = a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → b ≤ a := by
-  simpa [max?_eq_some_max h] using (max?_eq_some_iff (xs := xs))
-
-@[grind .]
-public theorem le_max_of_mem [Max α] [LE α] [Std.IsLinearOrder α] [Std.LawfulOrderMax α]
-    {xs : Array α} {a : α} (ha : a ∈ xs) :
-    a ≤ xs.max (ne_empty_of_mem ha) :=
-  (Array.max?_eq_some_iff.mp (max?_eq_some_max (ne_empty_of_mem ha))).right a ha
-
-@[simp, grind =]
-public theorem max_replicate [Max α] [Std.MaxEqOr α] {n : Nat} {a : α} (h : (replicate n a) ≠ #[]) :
-    (replicate n a).max h = a := by
-  have n_pos : 0 < n := by simpa [Nat.ne_zero_iff_zero_lt] using h
-  simpa [max?_eq_some_max h] using (max?_replicate_of_pos (a := a) n_pos)
-
-public theorem foldl_max_eq_max [Max α] [Std.IdempotentOp (max : α → α → α)]
-    [Std.Associative (max : α → α → α)] {xs : Array α} (h : xs ≠ #[]) {a : α} :
-    xs.foldl max a = max a (xs.max h) := by
-  simpa [max?_eq_some_max h] using foldl_max (xs := xs)
-
-end Array

src/Init/Data/Array/Monadic.lean

@@ -9,7 +9,6 @@ prelude
 import all Init.Data.List.Control
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Attach
-import Init.Data.Bool
 
 public section
 

src/Init/Data/Array/Nat.lean

@@ -1,42 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Sebastian Graf, Paul Reichert
--/
-module
-
-prelude
-import Init.Data.List.Nat.Sum
-public import Init.BinderPredicates
-public import Init.Data.Array.Basic
-public import Init.NotationExtra
-import Init.Data.Array.Lemmas
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace Array
-
-protected theorem sum_pos_iff_exists_pos_nat {xs : Array Nat} : 0 < xs.sum ↔ ∃ x ∈ xs, 0 < x := by
-  simp [← sum_toList, List.sum_pos_iff_exists_pos_nat]
-
-protected theorem sum_eq_zero_iff_forall_eq_nat {xs : Array Nat} :
-    xs.sum = 0 ↔ ∀ x ∈ xs, x = 0 := by
-  simp [← sum_toList, List.sum_eq_zero_iff_forall_eq_nat]
-
-@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  rw [← List.toArray_replicate, List.sum_toArray]
-  simp
-
-theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  simp [sum_append]
-
-theorem sum_reverse_nat (xs : Array Nat) : xs.reverse.sum = xs.sum := by
-  simp [sum_reverse]
-
-theorem sum_eq_foldl_nat {xs : Array Nat} : xs.sum = xs.foldl (init := 0) (· + ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
-
-end Array

src/Init/Data/Array/OfFn.lean

@@ -7,13 +7,8 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.List.OfFn
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Monadic
-import Init.Data.Fin.Lemmas
-import Init.Data.List.FinRange
-import Init.Data.Option.Lemmas
-import Init.Omega
+public import Init.Data.Array.Monadic
+public import Init.Data.List.FinRange
 
 public section
 
@@ -58,11 +53,6 @@ theorem ofFn_succ' {f : Fin (n+1) → α} :
   apply Array.toList_inj.mp
   simp [List.ofFn_succ]
 
-@[simp]
-theorem ofFn_getElem {xs : Array α} :
-    Array.ofFn (fun i : Fin xs.size => xs[i.val]) = xs := by
-  ext <;> simp
-
 @[simp]
 theorem ofFn_eq_empty_iff {f : Fin n → α} : ofFn f = #[] ↔ n = 0 := by
   rw [← Array.toList_inj]
@@ -77,12 +67,6 @@ theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i =
   · rintro ⟨i, rfl⟩
     apply mem_of_getElem (i := i) <;> simp
 
-@[simp, grind =]
-theorem map_ofFn {f : Fin n → α} {g : α → β} :
-    (Array.ofFn f).map g = Array.ofFn (g ∘ f) := by
-  apply Array.ext_getElem?
-  simp [Array.getElem?_ofFn]
-
 /-! ### ofFnM -/
 
 /-- Construct (in a monadic context) an array by applying a monadic function to each index. -/

src/Init/Data/Array/Perm.lean

@@ -6,13 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
+public import Init.Data.List.Nat.Perm
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Basic
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.Perm
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Perm
-import Init.Omega
+public import Init.Data.Array.Lemmas
 
 public section
 

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

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Vector.Basic
 public import Init.Data.Ord.Basic
-import Init.Omega
 
 public section
 

src/Init/Data/Array/Range.lean

@@ -8,16 +8,8 @@ module
 prelude
 import all Init.Data.Array.Basic
 import all Init.Data.Array.OfFn
-public import Init.BinderPredicates
-public import Init.Data.Nat.Lemmas
-public import Init.Ext
-import Init.ByCases
-import Init.Data.Array.Count
-import Init.Data.Array.MapIdx
-import Init.Data.Array.Zip
-import Init.Data.List.Find
-import Init.Data.List.Nat.Range
-import Init.Data.List.Range
+public import Init.Data.Array.MapIdx
+public import Init.Data.Array.Zip
 
 public section
 

src/Init/Data/Array/Subarray.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Basic
+import Init.Data.Array.GetLit
 public import Init.Data.Slice.Basic
 
 public section

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

@@ -9,7 +9,7 @@ module
 prelude
 public import Init.Data.Array.Subarray
 import all Init.Data.Array.Subarray
-import Init.Omega
+public import Init.Omega
 
 public section
 

src/Init/Data/Array/TakeDrop.lean

@@ -7,11 +7,7 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Basic
-public import Init.NotationExtra
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.TakeDrop
+public import Init.Data.Array.Lemmas
 
 public section
 

src/Init/Data/Array/Zip.lean

@@ -7,14 +7,7 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Control.Lawful
-public import Init.Data.Function
-import Init.Data.Array.Lemmas
-import Init.Data.List.Nat.TakeDrop
-import Init.Data.List.Zip
-import Init.Data.Option.Lemmas
-import Init.Data.Prod
-import Init.Omega
+public import Init.Data.Array.TakeDrop
 
 public section
 

src/Init/Data/BEq.lean

@@ -6,8 +6,7 @@ Authors: Mario Carneiro, Markus Himmel
 module
 
 prelude
-public import Init.Grind.Tactics
-import Init.Data.Bool
+public import Init.Data.Bool
 
 public section
 

src/Init/Data/BitVec/Basic.lean

@@ -6,16 +6,8 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
+public import Init.Data.Nat.Bitwise.Lemmas
 public import Init.Data.Int.Bitwise.Basic
-public import Init.Data.Bool
-public import Init.Data.Int.DivMod.Basic
-public import Init.WF
-import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Linear
-import Init.Meta.Defs
-import Init.Omega
-import Init.WFTactics
 
 @[expose] public section
 
@@ -269,7 +261,7 @@ Usually accessed via the `/` operator.
 -/
 @[expose]
 def udiv (x y : BitVec n) : BitVec n :=
-  (x.toNat / y.toNat)#'(by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
+  (x.toNat / y.toNat)#'(Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
 instance : Div (BitVec n) := ⟨.udiv⟩
 
 /--
@@ -279,7 +271,7 @@ SMT-LIB name: `bvurem`.
 -/
 @[expose]
 def umod (x y : BitVec n) : BitVec n :=
-  (x.toNat % y.toNat)#'(by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
+  (x.toNat % y.toNat)#'(Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
 instance : Mod (BitVec n) := ⟨.umod⟩
 
 /--
@@ -523,7 +515,7 @@ Example:
 -/
 @[expose]
 protected def and (x y : BitVec n) : BitVec n :=
-  (x.toNat &&& y.toNat)#'(by exact Nat.and_lt_two_pow x.toNat y.isLt)
+  (x.toNat &&& y.toNat)#'(Nat.and_lt_two_pow x.toNat y.isLt)
 instance : AndOp (BitVec w) := ⟨.and⟩
 
 /--
@@ -536,7 +528,7 @@ Example:
 -/
 @[expose]
 protected def or (x y : BitVec n) : BitVec n :=
-  (x.toNat ||| y.toNat)#'(by exact Nat.or_lt_two_pow x.isLt y.isLt)
+  (x.toNat ||| y.toNat)#'(Nat.or_lt_two_pow x.isLt y.isLt)
 instance : OrOp (BitVec w) := ⟨.or⟩
 
 /--
@@ -549,7 +541,7 @@ Example:
 -/
 @[expose]
 protected def xor (x y : BitVec n) : BitVec n :=
-  (x.toNat ^^^ y.toNat)#'(by exact Nat.xor_lt_two_pow x.isLt y.isLt)
+  (x.toNat ^^^ y.toNat)#'(Nat.xor_lt_two_pow x.isLt y.isLt)
 instance : XorOp (BitVec w) := ⟨.xor⟩
 
 /--

src/Init/Data/BitVec/BasicAux.lean

@@ -6,7 +6,7 @@ Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex
 module
 
 prelude
-public import Init.Grind.Tactics
+public import Init.Data.Fin.Basic
 
 public section
 

src/Init/Data/BitVec/Bitblast.lean

@@ -7,20 +7,12 @@ module
 
 prelude
 import all Init.Data.Nat.Bitwise.Basic
+public import Init.Data.Int.DivMod
 import all Init.Data.Int.DivMod
 import all Init.Data.BitVec.Basic
+public import Init.Data.BitVec.Decidable
 public import Init.Data.BitVec.Folds
-public import Init.BinderPredicates
-public import Init.Data.BitVec.Lemmas
-public import Init.Data.Nat.Lemmas
-import Init.ByCases
-import Init.Data.BitVec.Bootstrap
-import Init.Data.BitVec.Decidable
-import Init.Data.Int.Pow
-import Init.Data.Nat.Div.Lemmas
-import Init.Data.Nat.Mod
-import Init.Data.Nat.Simproc
-import Init.TacticsExtra
+import Init.BinderPredicates
 
 @[expose] public section
 
@@ -2241,7 +2233,7 @@ def aandRec (x y : BitVec w) (s : Nat) (hs : s < w) : Bool :=
 -/
 def resRec (x y : BitVec w) (s : Nat) (hs : s < w) (hslt : 0 < s) : Bool :=
   match hs0 : s with
-  | 0 => False.elim (by omega)
+  | 0 => by omega
   | s' + 1 =>
     match hs' : s' with
     | 0 => aandRec x y 1 (by omega)

src/Init/Data/BitVec/Bootstrap.lean

@@ -8,10 +8,8 @@ module
 prelude
 public import Init.Data.BitVec.Basic
 import all Init.Data.BitVec.Basic
+import Init.Data.Int.Bitwise.Lemmas
 import Init.Ext
-import Init.ByCases
-import Init.Data.Nat.Div.Lemmas
-import Init.TacticsExtra
 
 public section
 

src/Init/Data/BitVec/Decidable.lean

@@ -7,11 +7,8 @@ Authors: Joe Hendrix, Harun Khan, Alex Keizer, Abdalrhman M Mohamed, Siddharth B
 module
 
 prelude
+public import Init.Data.BitVec.Bootstrap
 import Init.Ext
-public import Init.Data.BitVec.Basic
-public import Init.PropLemmas
-import Init.Classical
-import Init.Data.BitVec.Bootstrap
 
 public section
 

src/Init/Data/BitVec/Folds.lean

@@ -7,10 +7,8 @@ module
 
 prelude
 import all Init.Data.BitVec.Basic
-public import Init.Data.BitVec.Basic
-public import Init.Ext
-import Init.Data.BitVec.Lemmas
-import Init.Data.Fin.Iterate
+public import Init.Data.BitVec.Lemmas
+public import Init.Data.Fin.Iterate
 
 public section
 

src/Init/Data/BitVec/Lemmas.lean

@@ -9,20 +9,11 @@ prelude
 import all Init.Data.BitVec.Basic
 import all Init.Data.BitVec.BasicAux
 public import Init.Data.Fin.Lemmas
+public import Init.Data.Int.Bitwise.Lemmas
+public import Init.Data.Int.LemmasAux
+public import Init.Data.BitVec.Bootstrap
 public import Init.Data.List.BasicAux
 import Init.Data.List.Lemmas
-public import Init.Data.BitVec.Basic
-import Init.ByCases
-import Init.Data.BitVec.Bootstrap
-import Init.Data.Int.Bitwise.Lemmas
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.LemmasAux
-import Init.Data.Int.Pow
-import Init.Data.Nat.Div.Lemmas
-import Init.Data.Nat.MinMax
-import Init.Data.Nat.Mod
-import Init.Data.Nat.Simproc
-import Init.TacticsExtra
 
 public section
 

src/Init/Data/Bool.lean

@@ -636,7 +636,7 @@ def boolPredToPred : Coe (α → Bool) (α  → Prop) where
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
-@[expose, instance_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+@[expose] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/

src/Init/Data/ByteArray/Basic.lean

@@ -6,12 +6,9 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.UInt.Basic
 import all Init.Data.UInt.BasicAux
-public import Init.Data.Array.DecidableEq
-public import Init.Data.List.Attach
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Lemmas
-import Init.Omega
+public import Init.Data.Array.Extract
 
 set_option doc.verso true
 

src/Init/Data/ByteArray/Extra.lean

@@ -7,8 +7,7 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
-import Init.Data.String.Defs
-import Init.Data.UInt.Basic
+import Init.Data.String.Basic
 
 set_option doc.verso true
 

src/Init/Data/ByteArray/Lemmas.lean

@@ -7,11 +7,6 @@ module
 
 prelude
 public import Init.Data.ByteArray.Basic
-import Init.ByCases
-import Init.Data.Array.Bootstrap
-import Init.Data.Array.Extract
-import Init.Data.Array.Lemmas
-import Init.Omega
 
 public section
 
@@ -291,41 +286,4 @@ theorem extract_zero_max_size {a : ByteArray} {i : Nat} : a.extract 0 (max i a.s
   ext1
   simp [Nat.le_max_right]
 
-theorem append_eq_append_iff_of_size_eq_left {ws xs ys zs : ByteArray} (h : ws.size = xs.size) :
-    ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  simpa [ByteArray.ext_iff] using Array.append_eq_append_iff_of_size_eq_left h
-
-theorem append_eq_append_iff_of_size_eq_right {ws xs ys zs : ByteArray} (h : ys.size = zs.size) :
-    ws ++ ys = xs ++ zs ↔ ws = xs ∧ ys = zs := by
-  simpa [ByteArray.ext_iff] using Array.append_eq_append_iff_of_size_eq_right h
-
-@[simp]
-theorem size_push {bs : ByteArray} {b : UInt8} : (bs.push b).size = bs.size + 1 := by
-  rw [ByteArray.size, data_push, Array.size_push, ← ByteArray.size]
-
-theorem ext_getElem {a b : ByteArray} (h₀ : a.size = b.size) (h : ∀ (i : Nat) hi hi', a[i]'hi = b[i]'hi') : a = b := by
-  rw [ByteArray.ext_iff]
-  apply Array.ext (by simpa using h₀)
-  simpa [← ByteArray.getElem_eq_getElem_data]
-
-@[simp]
-theorem _root_.List.toByteArray_inj {l l' : List UInt8} : l.toByteArray = l'.toByteArray ↔ l = l' := by
-  simp [ByteArray.ext_iff]
-
-theorem extract_eq_extract_iff_getElem {as bs : ByteArray} {i j len : Nat}
-    (hi : i + len ≤ as.size) (hj : j + len ≤ bs.size) :
-    as.extract i (i + len) = bs.extract j (j + len) ↔ ∀ k, (hk : k < len) → as[i + k] = bs[j + k] := by
-  induction len with
-  | zero => simp
-  | succ len ih =>
-    rw [← Nat.add_assoc, ← Nat.add_assoc, ByteArray.extract_eq_extract_append_extract (i + len) (by omega) (by omega),
-      ByteArray.extract_eq_extract_append_extract (a := bs) (j + len) (by omega) (by omega),
-      ByteArray.append_eq_append_iff_of_size_eq_left (by simp; omega), ih (by omega) (by omega),
-      ByteArray.extract_add_one (by omega), ByteArray.extract_add_one (by omega)]
-    simp only [List.toByteArray_inj, List.cons.injEq, and_true]
-    refine ⟨fun ⟨h, h'⟩ k hk => ?_, fun h => ⟨fun k hk => h k (by omega), h len (by omega)⟩⟩
-    by_cases hk' : k < len
-    · exact h k hk'
-    · exact (by omega : k = len) ▸ h'
-
 end ByteArray

src/Init/Data/Char/Basic.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.UInt.BasicAux
-import Init.Data.Nat.Div.Basic
 
 @[expose] public section
 

src/Init/Data/Char/Lemmas.lean

@@ -7,9 +7,7 @@ module
 
 prelude
 import all Init.Data.Char.Basic
-public import Init.Data.Char.Basic
-public import Init.Ext
-import Init.Data.UInt.Lemmas
+public import Init.Data.UInt.Lemmas
 
 public section
 
@@ -50,7 +48,6 @@ instance ltTrans : Trans (· < · : Char → Char → Prop) (· < ·) (· < ·)
   trans := Char.lt_trans
 
 -- This instance is useful while setting up instances for `String`.
-@[instance_reducible]
 def notLTTrans : Trans (¬ · < · : Char → Char → Prop) (¬ · < ·) (¬ · < ·) where
   trans h₁ h₂ := by simpa using Char.le_trans (by simpa using h₂) (by simpa using h₁)
 

src/Init/Data/Char/Order.lean

@@ -8,9 +8,7 @@ module
 prelude
 public import Init.Data.Char.Basic
 import Init.Data.Char.Lemmas
-public import Init.Data.Order.Classes
-import Init.Data.Order.Factories
-import Init.PropLemmas
+public import Init.Data.Order.Factories
 
 open Std
 

src/Init/Data/Char/Ordinal.lean

@@ -7,18 +7,11 @@ module
 
 prelude
 public import Init.Data.Fin.OverflowAware
+public import Init.Data.UInt.Basic
 public import Init.Data.Function
 import Init.Data.Char.Lemmas
 import Init.Data.Char.Order
 import Init.Grind
-public import Init.Data.Char.Basic
-import Init.ByCases
-import Init.Data.Fin.Lemmas
-import Init.Data.Int.OfNat
-import Init.Data.Nat.Linear
-import Init.Data.Nat.Simproc
-import Init.Data.Option.Lemmas
-import Init.Data.UInt.Lemmas
 
 /-!
 # Bijection between `Char` and `Fin Char.numCodePoints`

src/Init/Data/Dyadic/Basic.lean

@@ -6,17 +6,9 @@ Authors: Kim Morrison, Robin Arnez
 module
 
 prelude
+public import Init.Data.Rat.Lemmas
 import Init.Data.Int.Bitwise.Lemmas
-public import Init.Data.Int.Bitwise.Basic
-public import Init.Data.Order.Classes
-public import Init.Data.Rat.Basic
-import Init.ByCases
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.Pow
-import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Option.Lemmas
-import Init.Data.Rat.Lemmas
-import Init.Omega
+import Init.Hints
 
 /-!
 # The dyadic rationals

src/Init/Data/Dyadic/Instances.lean

@@ -8,12 +8,9 @@ module
 prelude
 public import Init.Data.Dyadic.Basic
 public import Init.Grind.Ordered.Ring
-import Init.Data.Rat.Lemmas
 
 /-! # Internal `grind` algebra instances for `Dyadic`. -/
 
-@[expose] public section
-
 open Lean.Grind
 
 namespace Dyadic

src/Init/Data/Dyadic/Inv.lean

@@ -4,17 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 module
-
 prelude
-public import Init.Data.Dyadic.Basic
-import Init.Data.Rat.Lemmas
+import Init.Data.Dyadic.Round
+import Init.Grind.Ordered.Ring
 
 /-!
 # Inversion for dyadic numbers
 -/
 
-@[expose] public section
-
 namespace Dyadic
 
 /--

src/Init/Data/Dyadic/Round.lean

@@ -7,15 +7,9 @@ module
 
 prelude
 public import Init.Data.Dyadic.Basic
-import Init.Data.Dyadic.Instances
+import all Init.Data.Dyadic.Instances
 import Init.Grind.Ordered.Rat
 import Init.Grind.Ordered.Field
-import Init.ByCases
-import Init.Data.Int.Bitwise.Lemmas
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.Pow
-import Init.Data.Option.Lemmas
-import Init.Omega
 
 namespace Dyadic
 

src/Init/Data/Fin/Basic.lean

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

src/Init/Data/Fin/Bitwise.lean

@@ -6,9 +6,7 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.Fin.Basic
-import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Nat.Div.Basic
+public import Init.Data.Nat.Bitwise
 
 public section
 

src/Init/Data/Fin/Fold.lean

@@ -7,12 +7,7 @@ module
 
 prelude
 public import Init.Control.Lawful.Basic
-public import Init.Ext
-import Init.Data.Fin.Lemmas
-import Init.Data.Nat.Lemmas
-import Init.Omega
-import Init.TacticsExtra
-import Init.WFTactics
+public import Init.Data.Fin.Lemmas
 
 public section
 

src/Init/Data/Fin/Iterate.lean

@@ -6,9 +6,7 @@ Authors: Joe Hendrix
 module
 
 prelude
-public import Init.Data.Fin.Basic
-import Init.PropLemmas
-import Init.WFTactics
+public import Init.PropLemmas
 
 public section
 

src/Init/Data/Fin/Lemmas.lean

@@ -6,15 +6,9 @@ Authors: Mario Carneiro, Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Nat.Lemmas
 public import Init.Ext
-public import Init.Data.Nat.Div.Basic
-public import Init.Data.Order.Classes
-public import Init.NotationExtra
-import Init.ByCases
-import Init.Data.Nat.Lemmas
-import Init.Data.Nat.Linear
-import Init.Omega
-import Init.TacticsExtra
+import Init.Data.Order.Lemmas
 
 @[expose] public section
 
@@ -124,7 +118,7 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
-@[expose, instance_reducible]
+@[expose]
 def instNatCast (n : Nat) [NeZero n] : NatCast (Fin n) where
   natCast a := Fin.ofNat n a
 
@@ -146,7 +140,7 @@ This is not a global instance, but may be activated locally via `open Fin.IntCas
 
 See the doc-string for `Fin.NatCast.instNatCast` for more details.
 -/
-@[expose, instance_reducible]
+@[expose]
 def instIntCast (n : Nat) [NeZero n] : IntCast (Fin n) where
   intCast := Fin.intCast
 
@@ -992,7 +986,7 @@ For the induction:
   let rec go (j : Nat) (h) (h2 : i ≤ j) (x : motive ⟨j, h⟩) : motive i :=
     if hi : i.1 = j then _root_.cast (by simp [← hi]) x
     else match j with
-      | 0 => False.elim (by omega)
+      | 0 => by omega
       | j + 1 => go j (by omega) (by omega) (cast ⟨j, by omega⟩ x)
   go _ _ (by omega) last
 

src/Init/Data/Fin/Log2.lean

@@ -6,8 +6,7 @@ Authors: Henrik Böving
 module
 
 prelude
-public import Init.Prelude
-import Init.Data.Nat.Log2
+public import Init.Data.Nat.Log2
 
 public section
 

src/Init/Data/FloatArray/Basic.lean

@@ -8,7 +8,7 @@ module
 prelude
 public import Init.Data.Float
 import Init.Ext
-public import Init.GetElem
+public import Init.Data.Array.DecidableEq
 
 public section
 universe u

src/Init/Data/Format/Basic.lean

@@ -6,10 +6,9 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Control.State
 public import Init.Data.Int.Basic
 public import Init.Data.String.Bootstrap
-import Init.Control.State
-import Init.Data.Nat.Bitwise.Basic
 
 public section
 

src/Init/Data/Format/Instances.lean

@@ -6,9 +6,8 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Array.Basic
 import Init.Data.String.Search
-public import Init.Data.ToString.Basic
-import Init.Data.Iterators.Consumers.Collect
 
 public section
 

src/Init/Data/Format/Macro.lean

@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 module
 
 prelude
-public meta import Init.Meta
-public import Init.Notation
+public import Init.Data.Format.Basic
+public import Init.Data.ToString.Macro
 
 public section
 

src/Init/Data/Format/Syntax.lean

@@ -6,10 +6,10 @@ Author: Leonardo de Moura
 module
 
 prelude
+public import Init.Data.Format.Macro
+public import Init.Data.Format.Instances
+public import Init.Meta
 import Init.Data.ToString.Name
-public import Init.Data.ToString.Basic
-import Init.Data.Format.Instances
-import Init.Data.Format.Macro
 
 public section
 

src/Init/Data/Hashable.lean

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

src/Init/Data/Int/Basic.lean

@@ -9,7 +9,7 @@ module
 
 prelude
 public import Init.Data.Cast
-public import Init.Data.Nat.Basic
+public import Init.Data.Nat.Div.Basic
 
 public section
 

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

@@ -6,16 +6,10 @@ Authors: Siddharth Bhat, Jeremy Avigad
 module
 
 prelude
+public import Init.Data.Nat.Bitwise.Lemmas
 public import Init.Data.Int.Bitwise.Basic
 import all Init.Data.Int.Bitwise.Basic
-public import Init.Data.Int.DivMod.Basic
-import Init.ByCases
-import Init.Data.Int.DivMod.Lemmas
-import Init.Data.Int.Pow
-import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Nat.Lemmas
-import Init.Omega
-import Init.RCases
+public import Init.Data.Int.DivMod.Lemmas
 
 public section
 

src/Init/Data/Int/Compare.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Ord.Basic
 import all Init.Data.Ord.Basic
+public import Init.Data.Int.Order
 import Init.Omega
 
 public section