feat: make computed_fields respect inline

This PR provides the necessary hooks for the new do elaborator to call
into the let and match elaborator.

The `do match` elaborator needs access to a couple of functions from the
term `match` elaborator to implement its own `elabMatchAlt`. In
particular, `withEqs`, `withPatternVars` and `checkNumPatterns` need to
be exposed. Furthermore, I think it makes sense to share
`instantiateAltLHSs`.

.claude/CLAUDE.md

@@ -1,6 +1,29 @@
 To build Lean you should use `make -j -C build/release`.
 
-To run a test you should use `cd tests/lean/run && ./test_single.sh example_test.lean`.
+## Running Tests
+
+See `doc/dev/testing.md` for full documentation. Quick reference:
+
+```bash
+# Full test suite (use after builds to verify correctness)
+make -j -C build/release test ARGS="-j$(nproc)"
+
+# Specific test by name (supports regex via ctest -R)
+make -j -C build/release test ARGS='-R grind_ematch --output-on-failure'
+
+# Rerun only previously failed tests
+make -j -C build/release test ARGS='--rerun-failed --output-on-failure'
+
+# Single test from tests/lean/run/ (quick check during development)
+cd tests/lean/run && ./test_single.sh example_test.lean
+
+# ctest directly (from stage1 build dir)
+cd build/release/stage1 && ctest -j$(nproc) --output-on-failure --timeout 300
+```
+
+The full test suite includes `tests/lean/`, `tests/lean/run/`, `tests/lean/interactive/`,
+`tests/compiler/`, `tests/pkg/`, Lake tests, and more. Using `make test` or `ctest` runs
+all of them; `test_single.sh` in `tests/lean/run/` only covers that one directory.
 
 ## New features
 
@@ -46,6 +69,42 @@ 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.
+
+## Module System for `src/` Files
+
+Files in `src/Lean/`, `src/Std/`, and `src/lake/Lake/` must have both `module` and `prelude` (CI enforces `^prelude$` on its own line). With `prelude`, nothing is auto-imported — you must explicitly import `Init.*` modules for standard library features. Check existing files in the same directory for the pattern, e.g.:
+
+```lean
+module
+
+prelude
+import Init.While  -- needed for while/repeat
+import Init.Data.String.TakeDrop  -- needed for String.startsWith
+public import Lean.Compiler.NameMangling  -- public if types are used in public signatures
+```
+
+Files outside these directories (e.g. `tests/`, `script/`) use just `module`.
+
 ## 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.
+
+## Copyright Headers
+
+New files require a copyright header. To get the year right, always run `date +%Y` rather than relying on memory. The copyright holder should be the author or their current employer — check other recent files by the same author in the repository to determine the correct entity (e.g., "Lean FRO, LLC", "Amazon.com, Inc. or its affiliates").
+
+Test files (in `tests/`) do not need copyright headers.

.claude/commands/release.md

@@ -103,6 +103,15 @@ Every time you run `release_checklist.py`, you MUST:
 This summary should be provided EVERY time you run the checklist, not just after creating new PRs.
 The user needs to see the complete picture of what's waiting for review.
 
+## Checking PR Status When Asked
+
+When the user asks for "status" or you need to report on PRs between checklist runs:
+- **ALWAYS check actual PR state** using `gh pr view <number> --repo <repo> --json state,mergedAt`
+- Do NOT rely on cached CI results or previous checklist output
+- The user may have merged PRs since your last check
+- Report which PRs are MERGED, which are OPEN with CI status, and which are still pending
+- After discovering merged PRs, rerun `release_checklist.py` to advance the release process
+
 ## Nightly Infrastructure
 
 The nightly build system uses branches and tags across two repositories:

.github/workflows/build-template.yml

@@ -102,7 +102,7 @@ jobs:
         if: matrix.cmultilib
       - name: Restore Cache
         id: restore-cache
-        uses: actions/cache/restore@v4
+        uses: actions/cache/restore@v5
         with:
           # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
           path: |
@@ -175,7 +175,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@v4
+        uses: actions/cache/save@v5
         with:
           # NOTE: must be in sync with `restore` above
           path: |

.github/workflows/ci.yml

@@ -60,10 +60,23 @@ jobs:
           if [[ -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             git fetch nightly --tags
-            LEAN_VERSION_STRING="nightly-$(date -u +%F)"
-            # do nothing if commit already has a different tag
-            if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
+            if [[ '${{ github.event_name }}' == 'workflow_dispatch' ]]; then
+              # Manual re-release: create a revision of the most recent nightly
+              BASE_NIGHTLY=$(git tag -l 'nightly-*' | sort -rV | head -1)
+              # Strip any existing -revK suffix to get the base date tag
+              BASE_NIGHTLY="${BASE_NIGHTLY%%-rev*}"
+              REV=1
+              while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
+                REV=$((REV + 1))
+              done
+              LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
+            else
+              # Scheduled: do nothing if commit already has a different tag
+              LEAN_VERSION_STRING="nightly-$(date -u +%F)"
+              if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
+                echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
+              fi
             fi
           fi
 
@@ -260,7 +273,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,
@@ -277,7 +290,7 @@ jobs:
                 // * `grind_guide` always times out.
                 // * `pkg/|lake/` tests sometimes time out (likely even hang), related to Lake CI
                 //   failures?
-                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|pkg/|lake/'"
+                "CTEST_OPTIONS": "-E 'StackOverflow|reverse-ffi|interactive|async_select_channel|9366|run/bv_|grind_guide|grind_bitvec2|grind_constProp|grind_indexmap|grind_list|grind_lint|grind_array_attach|grind_ite_trace|pkg/|lake/'"
               },
               {
                 "name": "macOS",
@@ -433,7 +446,7 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     steps:
-      - uses: actions/download-artifact@v6
+      - uses: actions/download-artifact@v7
         with:
           path: artifacts
       - name: Release
@@ -465,7 +478,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@v6
+      - uses: actions/download-artifact@v7
         with:
           path: artifacts
       - name: Prepare Nightly Release
@@ -475,7 +488,7 @@ jobs:
           git tag "${{ needs.configure.outputs.nightly }}"
           git push nightly "${{ needs.configure.outputs.nightly }}"
           git push -f origin refs/tags/${{ needs.configure.outputs.nightly }}:refs/heads/nightly
-          last_tag="$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[-0-9]*" | head -n 1)"
+          last_tag="$(git log HEAD^ --simplify-by-decoration --pretty="format:%d" | grep -o "nightly-[^ ,)]*" | head -n 1)"
           echo -e "*Changes since ${last_tag}:*\n\n" > diff.md
           git show "$last_tag":RELEASES.md > old.md
           #./script/diff_changelogs.py old.md doc/changes.md >> diff.md
@@ -498,8 +511,18 @@ jobs:
           gh workflow -R leanprover/release-index run update-index.yml
         env:
           GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
+      - name: Generate mathlib nightly-testing app token
+        id: mathlib-app-token
+        uses: actions/create-github-app-token@29824e69f54612133e76f7eaac726eef6c875baf # v2.2.1
+        continue-on-error: true
+        with:
+          app-id: ${{ secrets.MATHLIB_NIGHTLY_TESTING_APP_ID }}
+          private-key: ${{ secrets.MATHLIB_NIGHTLY_TESTING_PRIVATE_KEY }}
+          owner: leanprover-community
+          repositories: mathlib4-nightly-testing
       - name: Update toolchain on mathlib4's nightly-testing branch
+        if: steps.mathlib-app-token.outcome == 'success'
         run: |
-          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
+          gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_and_merge.yml
         env:
-          GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}
+          GITHUB_TOKEN: ${{ steps.mathlib-app-token.outputs.token }}

.github/workflows/pr-release.yml

@@ -20,7 +20,9 @@ on:
 jobs:
   on-success:
     runs-on: ubuntu-latest
-    if: github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.event == 'pull_request' && github.repository == 'leanprover/lean4'
+    # 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'
     steps:
       - name: Retrieve information about the original workflow
         uses: potiuk/get-workflow-origin@v1_1 # https://github.com/marketplace/actions/get-workflow-origin
@@ -41,6 +43,19 @@ 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: |
@@ -72,18 +87,6 @@ jobs:
           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 }}
-      # Verify artifacts were downloaded (equivalent to fail_on_unmatched_files in the old action).
-      - 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[@]}"
       # 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).
@@ -167,6 +170,18 @@ 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 != '' }}
@@ -201,8 +216,9 @@ 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.MATHLIB4_COMMENT_BOT }}" \
+                          -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
                           -H "Accept: application/vnd.github.v3+json" \
                           "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
                           | jq -r '.[].name')"
@@ -223,10 +239,10 @@ jobs:
 
             # Use GitHub API to check if a comment already exists
             existing_comment="$(curl --retry 3 --location --silent \
-                                    -H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                                    -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
                                     -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 == "leanprover-community-bot"))')"
+                                    | jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "mathlib-lean-pr-testing[bot]"))')"
             existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
             existing_comment_body="$(echo "$existing_comment" | jq -r .body)"
 
@@ -236,14 +252,14 @@ jobs:
               echo "Posting message to the comments: $MESSAGE"
 
               # Append new result to the existing comment or post a new comment
-              # It's essential we use the MATHLIB4_COMMENT_BOT token here, so that Mathlib CI can subsequently edit the comment.
+              # Use the mathlib-lean-pr-testing app token so 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 ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
                   -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"
@@ -252,7 +268,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 ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
+                  -H "Authorization: token ${{ steps.mathlib-comment-token.outputs.token }}" \
                   -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"
@@ -393,6 +409,18 @@ 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: |
@@ -404,7 +432,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: leanprover-community/batteries
-          token: ${{ secrets.MATHLIB4_BOT }}
+          token: ${{ steps.mathlib-app-token.outputs.token }}
           ref: nightly-testing
           fetch-depth: 0 # This ensures we check out all tags and branches.
           filter: tree:0
@@ -464,7 +492,7 @@ jobs:
         uses: actions/checkout@v6
         with:
           repository: leanprover-community/mathlib4-nightly-testing
-          token: ${{ secrets.MATHLIB4_BOT }}
+          token: ${{ steps.mathlib-app-token.outputs.token }}
           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@v4
+      uses: actions/cache/restore@v5
       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,42 +54,51 @@ 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
@@ -97,38 +106,49 @@ 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
@@ -137,24 +157,14 @@ ExternalProject_add(stage3
 
 # 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/bootstrap.md

@@ -6,7 +6,7 @@ building Lean itself - which is needed to again build those parts. This cycle is
 broken by using pre-built C files checked into the repository (which ultimately
 go back to a point where the Lean compiler was not written in Lean) in place of
 these Lean inputs and then compiling everything in multiple stages up to a fixed
-point. The build directory is organized in these stages:
+point. The build directory is organized into these stages:
 
 ```bash
 stage0/
@@ -79,7 +79,7 @@ with the contents of `src/stdlib_flags.h`, bringing them back in sync.
 NOTE: A full rebuild of stage 1 will only be triggered when the *committed* contents of `stage0/` are changed.
 Thus if you change files in it manually instead of through `update-stage0-commit` (see below) or fetching updates from git, you either need to commit those changes first or run `make -C build/release clean-stdlib`.
 The same is true for further stages except that a rebuild of them is retriggered on any committed change, not just to a specific directory.
-Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
+Thus when debugging e.g. stage 2 failures, you can resume the build from these failures on but you may want to explicitly call `clean-stdlib` to either observe changes from `.olean` files of modules that built successfully or to check that you did not break modules that built successfully at some prior point.
 
 If you have write access to the lean4 repository, you can also manually
 trigger that process, for example to be able to use new features in the compiler itself.
@@ -101,7 +101,7 @@ The script `script/rebase-stage0.sh` can be used for that.
 
 The CI should prevent PRs with changes to stage0 (besides `stdlib_flags.h`)
 from entering `master` through the (squashing!) merge queue, and label such PRs
-with the `changes-stage0` label. Such PRs should have a cleaned up history,
+with the `changes-stage0` label. Such PRs should have a cleaned-up history,
 with separate stage0 update commits; then coordinate with the admins to merge
 your PR using rebase merge, bypassing the merge queue.
 

doc/dev/release_checklist.md

@@ -30,7 +30,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     run `script/release_notes.py --since v4.5.0` on the `releases/v4.6.0` branch,
     and see the section "Writing the release notes" below for more information.
   - Release notes live in https://github.com/leanprover/reference-manual, in e.g. `Manual/Releases/v4.6.0.lean`.
-    It's best if you update these at the same time as a you update the `lean-toolchain` for the `reference-manual` repository, see below.
+    It's best if you update these at the same time as you update the `lean-toolchain` for the `reference-manual` repository, see below.
 - Go to https://github.com/leanprover/lean4/releases and verify that the `v4.6.0` release appears.
   - Verify on Github that "Set as the latest release" is checked.
 - Next, we will move a curated list of downstream repos to the latest stable release.
@@ -54,7 +54,7 @@ We'll use `v4.6.0` as the intended release version as a running example.
     - `verso`:
       - The `subverso` dependency is unusual in that it needs to be compatible with _every_ Lean release simultaneously.
         Usually you don't need to do anything.
-        If you think something is wrong here please contact David Thrane Christiansen (@david-christiansen)
+        If you think something is wrong here, please contact David Thrane Christiansen (@david-christiansen)
       - Warnings during `lake update` and `lake build` are expected.
     - `reference-manual`: the release notes generated by `script/release_notes.py` as described above must be included in
       `Manual/Releases/v4.6.0.lean`, and `import` and `include` statements adding in `Manual/Releases.lean`. 
@@ -65,7 +65,14 @@ We'll use `v4.6.0` as the intended release version as a running example.
       - The `lakefile.toml` should always refer to dependencies via their `main` or `master` branch,
         not a toolchain tag
         (with the exception of `ProofWidgets4`, which *must* use a sequential version tag).
+      - **Important:** After creating and pushing the ProofWidgets4 tag (see above),
+        the mathlib4 lakefile must be updated to reference the new tag (e.g. `v0.0.87`).
+        The `release_steps.py` script handles this automatically by looking up the latest
+        ProofWidgets4 tag compatible with the target toolchain.
       - Push the PR branch to the main Mathlib repository rather than a fork, or CI may not work reliably
+      - The "Verify Transient and Automated Commits" CI check on toolchain bump PRs can be ignored —
+        it often fails on automated commits (`x:` prefixed) from the nightly-testing history that can't be
+        reproduced in CI. This does not block merging.
     - `repl`:
       There are two copies of `lean-toolchain`/`lakefile.lean`:
       in the root, and in `test/Mathlib/`. Edit both, and run `lake update` in both directories.
@@ -146,6 +153,9 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
     * The repository does not need any changes to move to the new version.
     * Note that sometimes there are *unreviewed* but necessary changes on the `nightly-testing` branch of the repository.
       If so, you will need to merge these into the `bump_to_v4.7.0-rc1` branch manually.
+    * The `nightly-testing` branch may also contain temporary fix scripts (e.g. `fix_backward_defeq.py`,
+      `fix_deprecations.py`) that were used to adapt to breaking changes during the nightly cycle.
+      These should be reviewed and removed if no longer needed, as they can interfere with CI checks.
   - For each of the repositories listed in `script/release_repos.yml`,
     - Run `script/release_steps.py v4.7.0-rc1 <repo>` (e.g. replacing `<repo>` with `batteries`), which will walk you through the following steps:
       - Create a new branch off `master`/`main` (as specified in the `branch` field), called `bump_to_v4.7.0-rc1`.
@@ -218,8 +228,18 @@ Please read https://leanprover-community.github.io/contribute/tags_and_branches.
 
 # Writing the release notes
 
-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.
+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).
 
 ## Generating the release notes
 
@@ -273,7 +293,7 @@ open Verso.Genre
 open Verso.Genre.Manual
 open Verso.Genre.Manual.InlineLean
 
-#doc (Manual) "Lean 4.7.0-rc1 (YYYY-MM-DD)" =>
+#doc (Manual) "Lean 4.7.0-rc1 (2024-03-15)" =>
 %%%
 tag := "release-v4.7.0"
 file := "v4.7.0"

doc/examples/IJCAR2026/README.md

@@ -0,0 +1,6 @@
+# IJCAR 2026: `grind`, An SMT-Inspired Tactic for Lean 4
+
+Ancillary materials for the paper.
+
+- `examples.lean`: interactive examples from the paper
+- `analyze_grind_loc.py`: script used for the evaluation section, analyzing `grind` adoption and lines-of-code changes in Mathlib

doc/examples/IJCAR2026/analyze_grind_loc.py

@@ -0,0 +1,401 @@
+#!/usr/bin/env python3
+"""
+Analyze grind adoption LoC changes in mathlib.
+
+For each theorem/lemma in master that uses grind, find the most recent
+commit where it didn't use grind, and measure the LoC change.
+
+This script was used in preparing the "Evaluation" section of the grind paper.
+"""
+
+import subprocess
+import re
+import csv
+import sys
+from pathlib import Path
+from dataclasses import dataclass
+from concurrent.futures import ThreadPoolExecutor, as_completed
+from typing import Iterator
+from functools import lru_cache
+
+
+@dataclass
+class GrindUsage:
+    file: str
+    line_no: int
+    decl_name: str
+    decl_type: str  # theorem, lemma, def, example, etc.
+
+
+@dataclass
+class LocChange:
+    file: str
+    decl_name: str
+    decl_type: str
+    old_loc: int
+    new_loc: int
+    loc_saved: int
+    commit_sha: str
+    commit_date: str
+
+
+def run_git(args: list[str], repo: str = ".") -> str:
+    """Run a git command and return stdout."""
+    result = subprocess.run(
+        ["git", "-C", repo] + args,
+        capture_output=True, text=True, check=True
+    )
+    return result.stdout
+
+
+def run_git_safe(args: list[str], repo: str = ".") -> str | None:
+    """Run a git command, return None on failure."""
+    result = subprocess.run(
+        ["git", "-C", repo] + args,
+        capture_output=True, text=True
+    )
+    if result.returncode != 0:
+        return None
+    return result.stdout
+
+
+@lru_cache(maxsize=4096)
+def get_file_at_commit(repo: str, commit: str, file_path: str) -> str | None:
+    """Get file contents at a specific commit (cached)."""
+    return run_git_safe(["show", f"{commit}:{file_path}"], repo)
+
+
+def find_grind_usages(repo: str = ".") -> tuple[list[GrindUsage], int, int]:
+    """Find all declarations using grind in current master.
+    Returns (usages, total_grind_calls, grind_in_decls) where:
+    - total_grind_calls is the count of grind tactic calls (after filtering comments/attrs)
+    - grind_in_decls is the count of those that are inside named declarations
+    """
+    # Use git grep to find lines containing 'grind' (excludes lake packages)
+    result = run_git(["grep", "-n", "grind", "master", "--", "Mathlib/"], repo)
+
+    usages = []
+    seen = set()  # (file, decl_name) to dedupe
+    total_grind_calls = 0
+    grind_in_decls = 0
+
+    for line in result.strip().split('\n'):
+        if not line:
+            continue
+        # Format: master:path/to/file.lean:123:line content
+        match = re.match(r'^master:(.+\.lean):(\d+):(.*)$', line)
+        if not match:
+            continue
+
+        file_path, line_no_str, content = match.groups()
+        line_no = int(line_no_str)
+
+        # Skip comments and attributes (not tactic calls)
+        content_stripped = content.strip()
+        if content_stripped.startswith('--') or content_stripped.startswith('/-'):
+            continue
+        if content_stripped.startswith('attribute'):
+            continue
+        if '@[' in content and 'grind' in content:
+            # Could be an attribute like @[grind =], skip
+            if 'by' not in content and ':=' not in content:
+                continue
+
+        total_grind_calls += 1
+
+        # Find the declaration this grind belongs to
+        decl_name, decl_type = find_decl_at_line(repo, file_path, line_no)
+        if decl_name is None:
+            continue
+
+        grind_in_decls += 1
+
+        key = (file_path, decl_name)
+        if key in seen:
+            continue
+        seen.add(key)
+
+        usages.append(GrindUsage(
+            file=file_path,
+            line_no=line_no,
+            decl_name=decl_name,
+            decl_type=decl_type
+        ))
+
+    return usages, total_grind_calls, grind_in_decls
+
+
+def find_decl_at_line(repo: str, file_path: str, grind_line: int) -> tuple[str | None, str | None]:
+    """
+    Find the declaration name and type that contains the grind at the given line.
+    Search backwards from grind_line to find the most recent declaration.
+    """
+    # Get file content at master
+    content = get_file_at_commit(repo, "master", file_path)
+    if content is None:
+        return None, None
+
+    lines = content.split('\n')
+
+    # Search backwards from grind_line for a declaration
+    # Match declarations with optional leading modifiers and attributes
+    decl_pattern = re.compile(r'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+(\w+)')
+
+    for i in range(grind_line - 1, -1, -1):
+        if i >= len(lines):
+            continue
+        line = lines[i]
+        match = decl_pattern.match(line)
+        if match:
+            return match.group(2), match.group(1)
+
+    return None, None
+
+
+def find_grind_introduction_commit(repo: str, file_path: str, decl_name: str) -> str | None:
+    """
+    Find the commit that introduced grind to this declaration.
+    Returns None if the declaration was born with grind.
+    """
+    # First, find the line range of the declaration in master
+    content = get_file_at_commit(repo, "master", file_path)
+    if content is None:
+        return None
+
+    lines = content.split('\n')
+    decl_start = None
+    decl_end = None
+
+    # Find declaration start
+    decl_pattern = re.compile(rf'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+{re.escape(decl_name)}\b')
+    for i, line in enumerate(lines):
+        if decl_pattern.match(line):
+            decl_start = i
+            break
+
+    if decl_start is None:
+        return None
+
+    # Find declaration end (next top-level declaration or EOF)
+    end_patterns = re.compile(r'^(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class|namespace|section|end\s|@\[|#|/-)')
+    for i in range(decl_start + 1, len(lines)):
+        line = lines[i]
+        if line and not line[0].isspace() and end_patterns.match(line):
+            decl_end = i
+            break
+    if decl_end is None:
+        decl_end = len(lines)
+
+    # Find grind line within declaration
+    grind_line = None
+    for i in range(decl_start, decl_end):
+        if 'grind' in lines[i]:
+            grind_line = i + 1  # 1-indexed
+            break
+
+    if grind_line is None:
+        return None
+
+    # Use git blame to find when that grind line was added
+    blame_result = run_git_safe(["blame", "-L", f"{grind_line},{grind_line}", "--porcelain", "master", "--", file_path], repo)
+    if blame_result is None:
+        return None
+
+    # First line of porcelain output is the commit SHA
+    first_line = blame_result.split('\n')[0]
+    commit_sha = first_line.split()[0]
+
+    # Check if this declaration existed before this commit (without grind)
+    parent_sha = run_git_safe(["rev-parse", f"{commit_sha}^"], repo)
+    if parent_sha is None:
+        return None  # Initial commit, born with grind
+    parent_sha = parent_sha.strip()
+
+    # Check if declaration existed in parent
+    parent_content = get_file_at_commit(repo, parent_sha, file_path)
+    if parent_content is None:
+        # File didn't exist in parent - might be new file or renamed
+        return None
+
+    # Check if declaration existed and didn't have grind
+    if decl_name not in parent_content:
+        return None  # Declaration didn't exist - born with grind
+
+    # Check if it already had grind in parent
+    parent_lines = parent_content.split('\n')
+    in_decl = False
+    for line in parent_lines:
+        if decl_pattern.match(line):
+            in_decl = True
+        elif in_decl:
+            if line and not line[0].isspace() and end_patterns.match(line):
+                break
+            if 'grind' in line:
+                # Already had grind in parent — not the introduction commit
+                return None
+
+    return commit_sha
+
+
+def extract_proof_loc(repo: str, file_path: str, decl_name: str, commit: str) -> int | None:
+    """
+    Extract the number of lines in a declaration's proof at a given commit.
+    Returns None if the declaration doesn't exist at that commit.
+    """
+    content = get_file_at_commit(repo, commit, file_path)
+    if content is None:
+        return None
+
+    lines = content.split('\n')
+
+    # Find declaration start
+    decl_pattern = re.compile(rf'^(?:@\[.*?\]\s*)*(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class)\s+{re.escape(decl_name)}\b')
+    decl_start = None
+    for i, line in enumerate(lines):
+        if decl_pattern.match(line):
+            decl_start = i
+            break
+
+    if decl_start is None:
+        return None
+
+    # Find declaration end
+    end_patterns = re.compile(r'^(?:private\s+|protected\s+|noncomputable\s+|scoped\s+)*(theorem|lemma|def|example|instance|abbrev|structure|class|namespace|section|end\s|@\[|#|/-)')
+    decl_end = None
+    for i in range(decl_start + 1, len(lines)):
+        line = lines[i]
+        if line and not line[0].isspace() and end_patterns.match(line):
+            decl_end = i
+            break
+    if decl_end is None:
+        decl_end = len(lines)
+
+    # Count non-empty lines in declaration
+    loc = sum(1 for i in range(decl_start, decl_end) if lines[i].strip())
+    return loc
+
+
+def get_commit_date(repo: str, sha: str) -> str:
+    """Get the date of a commit."""
+    result = run_git(["log", "-1", "--format=%ci", sha], repo)
+    return result.strip().split()[0]  # Just the date part
+
+
+def analyze_usage_detailed(repo: str, usage: GrindUsage) -> tuple[LocChange | None, str]:
+    """Analyze a single grind usage, returning (result, skip_reason)."""
+    commit = find_grind_introduction_commit(repo, usage.file, usage.decl_name)
+    if commit is None:
+        return None, "born_with_grind"
+
+    parent = run_git_safe(["rev-parse", f"{commit}^"], repo)
+    if parent is None:
+        return None, "no_parent"
+    parent = parent.strip()
+
+    old_loc = extract_proof_loc(repo, usage.file, usage.decl_name, parent)
+    new_loc = extract_proof_loc(repo, usage.file, usage.decl_name, "master")
+
+    if old_loc is None:
+        return None, "old_loc_failed"
+    if new_loc is None:
+        return None, "new_loc_failed"
+
+    commit_date = get_commit_date(repo, commit)
+
+    return LocChange(
+        file=usage.file,
+        decl_name=usage.decl_name,
+        decl_type=usage.decl_type,
+        old_loc=old_loc,
+        new_loc=new_loc,
+        loc_saved=old_loc - new_loc,
+        commit_sha=commit[:12],
+        commit_date=commit_date
+    ), "success"
+
+
+def main(repo: str = "."):
+    print("Finding grind usages in master...", file=sys.stderr)
+    usages, total_grind_calls, grind_in_decls = find_grind_usages(repo)
+    print(f"Found {len(usages)} declarations using grind ({grind_in_decls}/{total_grind_calls} grind calls)", file=sys.stderr)
+
+    print("Analyzing git history (this may take a while)...", file=sys.stderr)
+    results: list[LocChange] = []
+    skip_reasons: dict[str, int] = {}
+
+    with ThreadPoolExecutor(max_workers=64) as executor:
+        futures = {executor.submit(analyze_usage_detailed, repo, usage): usage for usage in usages}
+
+        for i, future in enumerate(as_completed(futures)):
+            if (i + 1) % 50 == 0:
+                print(f"  Progress: {i + 1}/{len(usages)}", file=sys.stderr, flush=True)
+
+            result, reason = future.result()
+            if result:
+                results.append(result)
+            else:
+                skip_reasons[reason] = skip_reasons.get(reason, 0) + 1
+
+    total_skipped = sum(skip_reasons.values())
+    print(f"\nAnalyzed {len(results)} declarations, skipped {total_skipped}:", file=sys.stderr)
+    for reason, count in sorted(skip_reasons.items(), key=lambda x: -x[1]):
+        print(f"  - {reason}: {count}", file=sys.stderr)
+
+    # Sort by LoC saved (descending)
+    results.sort(key=lambda r: r.loc_saved, reverse=True)
+
+    # Output CSV
+    writer = csv.writer(sys.stdout)
+    writer.writerow(["file", "declaration", "type", "old_loc", "new_loc", "loc_saved", "commit", "date"])
+    for r in results:
+        writer.writerow([r.file, r.decl_name, r.decl_type, r.old_loc, r.new_loc, r.loc_saved, r.commit_sha, r.commit_date])
+
+    # Summary stats to stderr
+    total_old = sum(r.old_loc for r in results) if results else 0
+    total_new = sum(r.new_loc for r in results) if results else 0
+    total_saved = sum(r.loc_saved for r in results) if results else 0
+    avg_saved = total_saved / len(results) if results else 0
+
+    print("\n" + "=" * 60, file=sys.stderr)
+    print("GRIND ADOPTION LOC ANALYSIS", file=sys.stderr)
+    print("=" * 60, file=sys.stderr)
+
+    print("\n## Declaration Counts\n", file=sys.stderr)
+    print(f"  Total grind tactic calls:         {total_grind_calls}", file=sys.stderr)
+    print(f"  In named declarations:            {grind_in_decls} ({total_grind_calls - grind_in_decls} in anonymous/other)", file=sys.stderr)
+    print(f"  Unique declarations:              {len(usages)}", file=sys.stderr)
+    print(f"  Converted to grind:               {len(results)}", file=sys.stderr)
+    print(f"  Born with grind:                  {skip_reasons.get('born_with_grind', 0)}", file=sys.stderr)
+    if skip_reasons.get('old_loc_failed', 0) > 0:
+        print(f"  Could not trace history:          {skip_reasons.get('old_loc_failed', 0)}", file=sys.stderr)
+
+    print("\n## Lines of Code Impact\n", file=sys.stderr)
+    print(f"  Total LoC before grind:           {total_old}", file=sys.stderr)
+    print(f"  Total LoC after grind:            {total_new}", file=sys.stderr)
+    print(f"  Total LoC saved:                  {total_saved}", file=sys.stderr)
+    print(f"  Average LoC saved per theorem:    {avg_saved:.1f}", file=sys.stderr)
+    big_savings = sum(1 for r in results if r.loc_saved >= 10)
+    print(f"  Declarations shrunk by 10+ lines: {big_savings}", file=sys.stderr)
+
+    if results:
+        print("\n## Top 10 Biggest LoC Savings\n", file=sys.stderr)
+        for r in results[:10]:
+            print(f"  {r.loc_saved:+4d} lines: {r.decl_name} ({r.file})", file=sys.stderr)
+
+        # Show any that got bigger (negative savings)
+        got_bigger = [r for r in results if r.loc_saved < 0]
+        if got_bigger:
+            print(f"\n## Declarations That Got Bigger ({len(got_bigger)} total)\n", file=sys.stderr)
+            print("  (showing 5 worst):", file=sys.stderr)
+            for r in got_bigger[-5:]:  # Show worst 5
+                print(f"  {r.loc_saved:+4d} lines: {r.decl_name} ({r.file})", file=sys.stderr)
+
+    print("\n" + "=" * 60, file=sys.stderr)
+
+
+if __name__ == "__main__":
+    import argparse
+    parser = argparse.ArgumentParser(description="Analyze grind LoC savings")
+    parser.add_argument("--repo", "-r", default=".", help="Repository path")
+    args = parser.parse_args()
+    main(args.repo)

doc/examples/IJCAR2026/examples.lean

@@ -0,0 +1,127 @@
+/- Examples from the paper "grind: An SMT-Inspired Tactic for Lean 4" -/
+open Lean Grind
+
+/- Congruence closure. -/
+
+example (f : Nat → Nat) (h : a = b) : f (f b) = f (f a) := by grind
+
+/-
+E-matching.
+
+Any `f` that is the left inverse of `g` would work on this example.
+-/
+def f (x : Nat) := x - 1
+def g (x : Nat) := x + 1
+
+@[grind =] theorem fg : f (g x) = x := by simp [f, g]
+example : f a = b → a = g c → b = c := by grind
+
+/-
+Any `R` that is transitive and symmetric would work on this example.
+-/
+def R : Nat → Nat → Prop := (· % 7 = · % 7)
+@[grind →] theorem Rtrans : R x y → R y z → R x z := by grind [R]
+@[grind →] theorem Rsymm  : R x y → R y x := by grind [R]
+example : R a b → R c b → R d c → R a d := by grind
+
+/- Big step operational semantics example. -/
+
+abbrev Variable := String
+def State := Variable → Nat
+inductive Stmt : Type where
+  | skip : Stmt
+  | assign : Variable → (State → Nat) → Stmt
+  | seq : Stmt → Stmt → Stmt
+  | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt
+  | whileDo : (State → Prop) → Stmt → Stmt
+infix:60 ";; " => Stmt.seq
+export Stmt (skip assign seq ifThenElse whileDo)
+set_option quotPrecheck false in
+notation s:70 "[" x:70 "↦" n:70 "]" => (fun v ↦ if v = x then n else s v)
+inductive BigStep : Stmt → State → State → Prop where
+  | skip (s : State) : BigStep skip s s
+  | assign (x : Variable) (a : State → Nat) (s : State) : BigStep (assign x a) s (s[x ↦ a s])
+  | seq {S T : Stmt} {s t u : State} (hS : BigStep S s t) (hT : BigStep T t u) :
+    BigStep (S;; T) s u
+  | if_true {B : State → Prop} {s t : State} (hcond : B s) (S T : Stmt) (hbody : BigStep S s t) :
+    BigStep (ifThenElse B S T) s t
+  | if_false {B : State → Prop} {s t : State} (hcond : ¬ B s) (S T : Stmt) (hbody : BigStep T s t) :
+    BigStep (ifThenElse B S T) s t
+  | while_true {B S s t u} (hcond : B s) (hbody : BigStep S s t) (hrest : BigStep (whileDo B S) t u) :
+    BigStep (whileDo B S) s u
+  | while_false {B S s} (hcond : ¬ B s) : BigStep (whileDo B S) s s
+notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t
+
+example {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
+  grind [cases BigStep]
+
+theorem cases_if_of_true {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
+  grind [cases BigStep]
+
+theorem cases_if_of_false {B S T s t} (hcond : ¬ B s) : (ifThenElse B S T, s) ==> t → (T, s) ==> t := by
+  grind [cases BigStep]
+
+example {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
+  grind [BigStep] -- shortcut for `cases BigStep` and `intro BigStep`
+
+attribute [grind] BigStep
+theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==>
+    t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by grind
+
+/- Dependent pattern matching. -/
+
+inductive Vec (α : Type u) : Nat → Type u
+  | nil : Vec α 0
+  | cons : α → Vec α n → Vec α (n+1)
+@[grind =] def Vec.head : Vec α (n+1) → α
+  | .cons a _ => a
+example (as bs : Vec Int (n+1)) : as.head = bs.head
+    → (match as, bs with
+       | .cons a _, .cons b _ => a + b) = 2 * as.head := by grind
+
+/- Theory solvers. -/
+
+example [CommRing α] (a b c : α) :
+    a + b + c = 3 →
+    a^2 + b^2 + c^2 = 5 →
+    a^3 + b^3 + c^3 = 7 →
+    a^4 + b^4 + c^4 = 9 := by grind
+
+example (x : BitVec 8) : (x - 16) * (x + 16) = x^2 := by grind
+
+example [CommSemiring α] [AddRightCancel α] (x y : α) :
+    x^2*y = 1 → x*y^2 = y → y*x = 1 := by grind
+
+example (a b : UInt32) : a ≤ 2 → b ≤ 3 → a + b ≤ 5 := by grind
+
+example [LE α] [Std.IsLinearPreorder α] (a b c d : α) :
+    a ≤ b → ¬ (c ≤ b) → ¬ (d ≤ c) → a ≤ d := by grind
+
+/- Theory combination. -/
+
+example [CommRing α] [NoNatZeroDivisors α]
+    (a b c : α) (f : α → Nat) :
+    a + b + c = 3 → a^2 + b^2 + c^2 = 5 → a^3 + b^3 + c^3 = 7 →
+    f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by grind
+
+/- Interactive mode. -/
+
+-- Remark: Mathlib contains the definition of `Real`, `sin`, and `cos`.
+axiom Real : Type
+instance : Lean.Grind.CommRing Real := sorry
+
+axiom cos : Real → Real
+axiom sin : Real → Real
+axiom trig_identity : ∀ x, (cos x)^2 + (sin x)^2 = 1
+
+-- Manually specify the patterns for `trig_identity`
+grind_pattern trig_identity => cos x
+grind_pattern trig_identity => sin x
+
+example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := by
+  grind? -- Provides code action
+
+example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := by
+  grind =>
+    instantiate only [trig_identity]
+    ring

flake.lock

@@ -2,11 +2,11 @@
   "nodes": {
     "nixpkgs": {
       "locked": {
-        "lastModified": 1745636243,
-        "narHash": "sha256-kbNvlQZf8wwok3d2X1kM/TlXH/MZ+03ZNv+IPPBx+DM=",
-        "rev": "f771eb401a46846c1aebd20552521b233dd7e18b",
+        "lastModified": 1769018530,
+        "narHash": "sha256-S/5RU76BdQ32bbE99a+G9gMuatpVWEvIfeSjEqyoFS4=",
+        "rev": "88d3861acdd3d2f0e361767018218e51810df8a1",
         "type": "tarball",
-        "url": "https://releases.nixos.org/nixos/unstable/nixos-25.05pre789333.f771eb401a46/nixexprs.tar.xz"
+        "url": "https://releases.nixos.org/nixos/unstable/nixos-26.05pre931542.88d3861acdd3/nixexprs.tar.xz"
       },
       "original": {
         "type": "tarball",

flake.nix

@@ -18,7 +18,7 @@
       # An old nixpkgs for creating releases with an old glibc
       pkgsDist-old-aarch = import inputs.nixpkgs-old { localSystem.config = "aarch64-unknown-linux-gnu"; };
 
-      llvmPackages = pkgs.llvmPackages_15;
+      llvmPackages = pkgs.llvmPackages_19;
 
       devShellWithDist = pkgsDist: pkgs.mkShell.override {
           stdenv = pkgs.overrideCC pkgs.stdenv llvmPackages.clang;

releases_drafts/environment.md

@@ -1,6 +0,0 @@
-**Breaking Changes**
-
-* The functions `Lean.Environment.importModules` and `Lean.Environment.finalizeImport` have been extended with a new parameter `loadExts : Bool := false` that enables environment extension state loading.
-  Their previous behavior corresponds to setting the flag to `true` but is only safe to do in combination with `enableInitializersExecution`; see also the `importModules` docstring.
-  The new default value `false` ensures the functions can be used correctly multiple times within the same process when environment extension access is not needed.
-  The wrapper function `Lean.Environment.withImportModules` now always calls `importModules` with `loadExts := false` as it is incompatible with extension loading.

releases_drafts/module-system.md

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

script/PROFILER_README.md

@@ -0,0 +1,178 @@
+# Lean Profiler
+
+Profile Lean programs with demangled names using
+[samply](https://github.com/mstange/samply) and
+[Firefox Profiler](https://profiler.firefox.com).
+
+Python 3, no external dependencies.
+
+## Quick start
+
+```bash
+# One command: record, symbolicate, demangle, and open in Firefox Profiler
+script/lean_profile.sh ./my_lean_binary [args...]
+
+# See all options
+script/lean_profile.sh --help
+```
+
+Requirements: `samply` (`cargo install samply`), `python3`.
+
+## Reading demangled names
+
+The demangler transforms low-level C symbol names into readable Lean names
+and annotates them with compact modifiers.
+
+### Basic names
+
+| Raw symbol | Demangled |
+|---|---|
+| `l_Lean_Meta_Sym_main` | `Lean.Meta.Sym.main` |
+| `lp_std_List_map` | `List.map (std)` |
+| `_init_l_Foo_bar` | `[init] Foo.bar` |
+| `initialize_Init_Data` | `[module_init] Init.Data` |
+| `_lean_main` | `[lean] main` |
+
+### Modifier flags `[...]`
+
+Compiler-generated suffixes are folded into a bracket annotation after the
+name. These indicate *how* the function was derived from the original source
+definition.
+
+| Flag | Meaning | Compiler suffix |
+|---|---|---|
+| `arity`↓ | Reduced-arity specialization | `_redArg` |
+| `boxed` | Boxed calling-convention wrapper | `_boxed` |
+| `impl` | Implementation detail | `_impl` |
+| λ | Lambda-lifted closure | `_lam_N`, `_lambda_N`, `_elam_N` |
+| `jp` | Join point | `_jp_N` |
+| `closed` | Extracted closed subterm | `_closed_N` |
+| `private` | Private (module-scoped) definition | `_private.Module.0.` prefix |
+
+Examples:
+
+```
+Lean.Meta.Simp.simpLambda [boxed, λ]     -- boxed wrapper of a lambda-lifted closure
+Lean.Meta.foo [arity↓, private]           -- reduced-arity version of a private def
+```
+
+Multiple flags are comma-separated. Order reflects how they were collected
+(innermost suffix first).
+
+### Specializations `spec at ...`
+
+When the compiler specializes a function at a particular call site, the
+demangled name shows `spec at <context>` after the base name and its flags.
+The context names the function whose body triggered the specialization, and
+may carry its own modifier flags:
+
+```
+<base-name> [<base-flags>] spec at <context>[<context-flags>]
+```
+
+Examples:
+
+```
+-- foo specialized at call site in bar
+Lean.Meta.foo spec at Lean.Meta.bar
+
+-- foo (with a lambda closure) specialized at bar (with reduced arity and a lambda)
+Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]
+
+-- chained specialization: foo specialized at bar, then at baz
+Lean.Meta.foo spec at Lean.Meta.bar spec at Lean.Meta.baz[arity↓]
+```
+
+Context flags use the same symbols as base flags. When a context has no
+flags, the brackets are omitted.
+
+### Other annotations
+
+| Pattern | Meaning |
+|---|---|
+| `<apply/N>` | Lean runtime apply function (N arguments) |
+| `.cold.N` suffix | LLVM cold-path clone (infrequently executed) |
+| `(pkg)` suffix | Function from package `pkg` |
+
+## Tools
+
+### `script/lean_profile.sh` -- Full profiling pipeline
+
+Records a profile, symbolicates it via samply's API, demangles Lean names,
+and opens the result in Firefox Profiler. This is the recommended workflow.
+
+```bash
+script/lean_profile.sh ./build/release/stage1/bin/lean src/Lean/Elab/Term.lean
+```
+
+Environment variables:
+
+| Variable | Default | Description |
+|---|---|---|
+| `SAMPLY_RATE` | 1000 | Sampling rate in Hz |
+| `SAMPLY_PORT` | 3756 | Port for samply symbolication server |
+| `SERVE_PORT` | 3757 | Port for serving the demangled profile |
+| `PROFILE_KEEP` | 0 | Set to 1 to keep the temp directory |
+
+### `script/profiler/lean_demangle.py` -- Name demangler
+
+Demangles individual symbol names. Works as a stdin filter (like `c++filt`)
+or with arguments.
+
+```bash
+echo "l_Lean_Meta_Sym_main" | python3 script/profiler/lean_demangle.py
+# Lean.Meta.Sym.main
+
+python3 script/profiler/lean_demangle.py --raw l_foo___redArg
+# foo._redArg  (exact name, no postprocessing)
+```
+
+As a Python module:
+
+```python
+from lean_demangle import demangle_lean_name, demangle_lean_name_raw
+
+demangle_lean_name("l_foo___redArg")       # "foo [arity↓]"
+demangle_lean_name_raw("l_foo___redArg")   # "foo._redArg"
+```
+
+### `script/profiler/symbolicate_profile.py` -- Profile symbolicator
+
+Calls samply's symbolication API to resolve raw addresses into symbol names,
+then demangles them. Used internally by `lean_profile.sh`.
+
+### `script/profiler/serve_profile.py` -- Profile server
+
+Serves a profile JSON file to Firefox Profiler without re-symbolication
+(which would overwrite demangled names). Used internally by `lean_profile.sh`.
+
+### `script/profiler/lean_demangle_profile.py` -- Standalone profile rewriter
+
+Demangles names in an already-symbolicated profile file (if you have one
+from another source).
+
+```bash
+python3 script/profiler/lean_demangle_profile.py profile.json.gz -o demangled.json.gz
+```
+
+## Tests
+
+```bash
+cd script/profiler && python3 -m unittest test_demangle -v
+```
+
+## How it works
+
+The demangler is a faithful port of Lean 4's `Name.demangleAux` from
+`src/Lean/Compiler/NameMangling.lean`. It reverses the encoding used by
+`Name.mangle` / `Name.mangleAux` which turns hierarchical Lean names into
+valid C identifiers:
+
+- `_` separates name components (`Lean.Meta` -> `Lean_Meta`)
+- `__` encodes a literal underscore in a component name
+- `_xHH`, `_uHHHH`, `_UHHHHHHHH` encode special characters
+- `_N_` encodes numeric name components
+- `_00` is a disambiguation prefix for ambiguous patterns
+
+After demangling, a postprocessing pass folds compiler-generated suffixes
+into human-readable annotations (see [Reading demangled names](#reading-demangled-names)).

script/fmt

@@ -0,0 +1,13 @@
+#!/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 \
+    -- {} +

script/lean-bisect

@@ -36,7 +36,7 @@ sys.path.insert(0, str(Path(__file__).parent))
 import build_artifact
 
 # Constants
-NIGHTLY_PATTERN = re.compile(r'^nightly-(\d{4})-(\d{2})-(\d{2})$')
+NIGHTLY_PATTERN = re.compile(r'^nightly-(\d{4})-(\d{2})-(\d{2})(-rev(\d+))?$')
 VERSION_PATTERN = re.compile(r'^v4\.(\d+)\.(\d+)(-rc\d+)?$')
 # Accept short SHAs (7+ chars) - we'll resolve to full SHA later
 SHA_PATTERN = re.compile(r'^[0-9a-f]{7,40}$')
@@ -158,7 +158,7 @@ def parse_identifier(s: str) -> Tuple[str, str]:
         return ('sha', full_sha)
     error(f"Invalid identifier format: '{s}'\n"
           f"Expected one of:\n"
-          f"  - nightly-YYYY-MM-DD (e.g., nightly-2024-06-15)\n"
+          f"  - nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK (e.g., nightly-2024-06-15, nightly-2024-06-15-rev1)\n"
           f"  - v4.X.Y or v4.X.Y-rcK (e.g., v4.8.0, v4.9.0-rc1)\n"
           f"  - commit SHA (short or full)")
 
@@ -244,8 +244,13 @@ def fetch_nightly_tags() -> List[str]:
         if len(data) < 100:
             break
 
-    # Sort by date (nightly-YYYY-MM-DD format sorts lexicographically)
-    tags.sort()
+    # Sort by date and revision (nightly-YYYY-MM-DD-revK needs numeric comparison on rev)
+    def nightly_sort_key(tag):
+        m = NIGHTLY_PATTERN.match(tag)
+        if m:
+            return (int(m.group(1)), int(m.group(2)), int(m.group(3)), int(m.group(5) or 0))
+        return (0, 0, 0, 0)
+    tags.sort(key=nightly_sort_key)
     return tags
 
 def get_commit_for_nightly(nightly: str) -> str:
@@ -1024,6 +1029,7 @@ Range Syntax:
 Identifier Formats:
 
   nightly-YYYY-MM-DD    Nightly build date (e.g., nightly-2024-06-15)
+  nightly-YYYY-MM-DD-revK  Revised nightly (e.g., nightly-2024-06-15-rev1)
                         Uses pre-built toolchains from leanprover/lean4-nightly.
                         Fast: downloads via elan (~30s each).
 
@@ -1151,9 +1157,9 @@ Examples:
     # Validate --nightly-only
     if args.nightly_only:
         if from_val is not None and from_type != 'nightly':
-            error("--nightly-only requires FROM to be a nightly identifier (nightly-YYYY-MM-DD)")
+            error("--nightly-only requires FROM to be a nightly identifier (nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK)")
         if to_type != 'nightly':
-            error("--nightly-only requires TO to be a nightly identifier (nightly-YYYY-MM-DD)")
+            error("--nightly-only requires TO to be a nightly identifier (nightly-YYYY-MM-DD or nightly-YYYY-MM-DD-revK)")
 
     if from_val:
         info(f"From: {from_val} ({from_type})")

script/lean_profile.sh

@@ -0,0 +1,133 @@
+#!/bin/bash
+# Profile a Lean binary with demangled names.
+#
+# Usage:
+#   script/lean_profile.sh ./my_lean_binary [args...]
+#
+# Records a profile with samply, symbolicates via samply's API,
+# demangles Lean symbol names, and opens the result in Firefox Profiler.
+#
+# Requirements: samply (cargo install samply), python3
+#
+# Options (via environment variables):
+#   SAMPLY_RATE    — sampling rate in Hz (default: 1000)
+#   SAMPLY_PORT    — port for samply symbolication server (default: 3756)
+#   SERVE_PORT     — port for serving the demangled profile (default: 3757)
+#   PROFILE_KEEP   — set to 1 to keep the raw profile after demangling
+
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+PROFILER_DIR="$SCRIPT_DIR/profiler"
+SYMBOLICATE="$PROFILER_DIR/symbolicate_profile.py"
+SERVE_PROFILE="$PROFILER_DIR/serve_profile.py"
+
+usage() {
+    cat >&2 <<EOF
+Usage: $0 [options] <lean-binary> [args...]
+
+Profile a Lean binary and view the results in Firefox Profiler
+with demangled Lean names.
+
+Requirements:
+  samply    cargo install samply
+  python3   (included with macOS / most Linux distros)
+
+Environment variables:
+  SAMPLY_RATE    sampling rate in Hz (default: 1000)
+  SAMPLY_PORT    port for samply symbolication server (default: 3756)
+  SERVE_PORT     port for serving the demangled profile (default: 3757)
+  PROFILE_KEEP   set to 1 to keep the temp directory after profiling
+
+Reading demangled names:
+  Compiler suffixes are shown as modifier flags after the name:
+    [arity↓]   reduced-arity specialization     (_redArg)
+    [boxed]    boxed calling-convention wrapper  (_boxed)
+    [λ]        lambda-lifted closure             (_lam_N, _lambda_N, _elam_N)
+    [jp]       join point                        (_jp_N)
+    [closed]   extracted closed subterm          (_closed_N)
+    [private]  private (module-scoped) def       (_private.Module.0. prefix)
+    [impl]     implementation detail             (_impl)
+
+  Specializations appear after the flags:
+    Lean.Meta.foo [λ] spec at Lean.Meta.bar[λ, arity↓]
+      = foo (with lambda closure), specialized at bar (lambda, reduced arity)
+
+  Multiple "spec at" entries indicate chained specializations.
+  See script/PROFILER_README.md for full documentation.
+EOF
+    exit "${1:-0}"
+}
+
+if [ $# -eq 0 ]; then
+    usage 1
+fi
+
+case "${1:-}" in
+    -h|--help) usage 0 ;;
+esac
+
+if ! command -v samply &>/dev/null; then
+    echo "error: samply not found. Install with: cargo install samply" >&2
+    exit 1
+fi
+
+RATE="${SAMPLY_RATE:-1000}"
+PORT="${SAMPLY_PORT:-3756}"
+SERVE="${SERVE_PORT:-3757}"
+TMPDIR=$(mktemp -d /tmp/lean-profile-XXXXXX)
+TMPFILE="$TMPDIR/profile.json.gz"
+DEMANGLED="$TMPDIR/profile-demangled.json.gz"
+SAMPLY_LOG="$TMPDIR/samply.log"
+SAMPLY_PID=""
+
+cleanup() {
+    if [ -n "$SAMPLY_PID" ]; then
+        kill "$SAMPLY_PID" 2>/dev/null || true
+        wait "$SAMPLY_PID" 2>/dev/null || true
+    fi
+    # Safety net: kill anything still on the symbolication port
+    lsof -ti :"$PORT" 2>/dev/null | xargs kill 2>/dev/null || true
+    [ "${PROFILE_KEEP:-0}" = "1" ] || rm -rf "$TMPDIR"
+}
+trap cleanup EXIT
+
+# Step 1: Record
+echo "Recording profile (rate=${RATE} Hz)..." >&2
+samply record --save-only -o "$TMPFILE" -r "$RATE" "$@"
+
+# Step 2: Start samply server for symbolication
+echo "Starting symbolication server..." >&2
+samply load --no-open -P "$PORT" "$TMPFILE" > "$SAMPLY_LOG" 2>&1 &
+SAMPLY_PID=$!
+
+# Wait for server to be ready
+for i in $(seq 1 30); do
+    if grep -q "Local server listening" "$SAMPLY_LOG" 2>/dev/null; then
+        break
+    fi
+    sleep 0.2
+done
+
+# Extract the token from samply's output
+TOKEN=$(grep -oE '[a-z0-9]{30,}' "$SAMPLY_LOG" | head -1)
+
+if [ -z "$TOKEN" ]; then
+    echo "error: could not get samply server token" >&2
+    exit 1
+fi
+
+SERVER_URL="http://127.0.0.1:${PORT}/${TOKEN}"
+
+# Step 3: Symbolicate + demangle
+echo "Symbolicating and demangling..." >&2
+python3 "$SYMBOLICATE" --server "$SERVER_URL" "$TMPFILE" -o "$DEMANGLED"
+
+# Step 4: Kill symbolication server
+kill "$SAMPLY_PID" 2>/dev/null || true
+wait "$SAMPLY_PID" 2>/dev/null || true
+SAMPLY_PID=""
+
+# Step 5: Serve the demangled profile directly (without samply's re-symbolication)
+echo "Opening in Firefox Profiler..." >&2
+python3 "$SERVE_PROFILE" "$DEMANGLED" -P "$SERVE"

script/profiler/lean_demangle.py

@@ -0,0 +1,779 @@
+#!/usr/bin/env python3
+"""
+Lean name demangler.
+
+Demangles C symbol names produced by the Lean 4 compiler back into
+readable Lean hierarchical names.
+
+Usage as a filter (like c++filt):
+    echo "l_Lean_Meta_Sym_main" | python lean_demangle.py
+
+Usage as a module:
+    from lean_demangle import demangle_lean_name
+    print(demangle_lean_name("l_Lean_Meta_Sym_main"))
+"""
+
+import sys
+
+
+# ---------------------------------------------------------------------------
+# String.mangle / unmangle
+# ---------------------------------------------------------------------------
+
+def _is_ascii_alnum(ch):
+    """Check if ch is an ASCII letter or digit (matching Lean's isAlpha/isDigit)."""
+    return ('a' <= ch <= 'z') or ('A' <= ch <= 'Z') or ('0' <= ch <= '9')
+
+
+def mangle_string(s):
+    """Port of Lean's String.mangle: escape a single string for C identifiers."""
+    result = []
+    for ch in s:
+        if _is_ascii_alnum(ch):
+            result.append(ch)
+        elif ch == '_':
+            result.append('__')
+        else:
+            code = ord(ch)
+            if code < 0x100:
+                result.append('_x' + format(code, '02x'))
+            elif code < 0x10000:
+                result.append('_u' + format(code, '04x'))
+            else:
+                result.append('_U' + format(code, '08x'))
+    return ''.join(result)
+
+
+def _parse_hex(s, pos, n):
+    """Parse n lowercase hex digits at pos. Returns (new_pos, value) or None."""
+    if pos + n > len(s):
+        return None
+    val = 0
+    for i in range(n):
+        c = s[pos + i]
+        if '0' <= c <= '9':
+            val = (val << 4) | (ord(c) - ord('0'))
+        elif 'a' <= c <= 'f':
+            val = (val << 4) | (ord(c) - ord('a') + 10)
+        else:
+            return None
+    return (pos + n, val)
+
+
+# ---------------------------------------------------------------------------
+# Name mangling (for round-trip verification)
+# ---------------------------------------------------------------------------
+
+def _check_disambiguation(m):
+    """Port of Lean's checkDisambiguation: does mangled string m need a '00' prefix?"""
+    pos = 0
+    while pos < len(m):
+        ch = m[pos]
+        if ch == '_':
+            pos += 1
+            continue
+        if ch == 'x':
+            return _parse_hex(m, pos + 1, 2) is not None
+        if ch == 'u':
+            return _parse_hex(m, pos + 1, 4) is not None
+        if ch == 'U':
+            return _parse_hex(m, pos + 1, 8) is not None
+        if '0' <= ch <= '9':
+            return True
+        return False
+    # all underscores or empty
+    return True
+
+
+def _need_disambiguation(prev_component, mangled_next):
+    """Port of Lean's needDisambiguation."""
+    # Check if previous component (as a string) ends with '_'
+    prev_ends_underscore = (isinstance(prev_component, str) and
+                            len(prev_component) > 0 and
+                            prev_component[-1] == '_')
+    return prev_ends_underscore or _check_disambiguation(mangled_next)
+
+
+def mangle_name(components, prefix="l_"):
+    """
+    Mangle a list of name components (str or int) into a C symbol.
+    Port of Lean's Name.mangle.
+    """
+    if not components:
+        return prefix
+
+    parts = []
+    prev = None
+    for i, comp in enumerate(components):
+        if isinstance(comp, int):
+            if i == 0:
+                parts.append(str(comp) + '_')
+            else:
+                parts.append('_' + str(comp) + '_')
+        else:
+            m = mangle_string(comp)
+            if i == 0:
+                if _check_disambiguation(m):
+                    parts.append('00' + m)
+                else:
+                    parts.append(m)
+            else:
+                if _need_disambiguation(prev, m):
+                    parts.append('_00' + m)
+                else:
+                    parts.append('_' + m)
+        prev = comp
+
+    return prefix + ''.join(parts)
+
+
+# ---------------------------------------------------------------------------
+# Name demangling
+# ---------------------------------------------------------------------------
+
+def demangle_body(s):
+    """
+    Demangle a string produced by Name.mangleAux (without prefix).
+    Returns a list of components (str or int).
+
+    This is a faithful port of Lean's Name.demangleAux from NameMangling.lean.
+    """
+    components = []
+    length = len(s)
+
+    def emit(comp):
+        components.append(comp)
+
+    def decode_num(pos, n):
+        """Parse remaining digits, emit numeric component, continue."""
+        while pos < length:
+            ch = s[pos]
+            if '0' <= ch <= '9':
+                n = n * 10 + (ord(ch) - ord('0'))
+                pos += 1
+            else:
+                # Expect '_' (trailing underscore of numeric encoding)
+                pos += 1  # skip '_'
+                emit(n)
+                if pos >= length:
+                    return pos
+                # Skip separator '_' and go to name_start
+                pos += 1
+                return name_start(pos)
+        # End of string
+        emit(n)
+        return pos
+
+    def name_start(pos):
+        """Start parsing a new name component."""
+        if pos >= length:
+            return pos
+        ch = s[pos]
+        pos += 1
+        if '0' <= ch <= '9':
+            # Check for '00' disambiguation
+            if ch == '0' and pos < length and s[pos] == '0':
+                pos += 1
+                return demangle_main(pos, "", 0)
+            else:
+                return decode_num(pos, ord(ch) - ord('0'))
+        elif ch == '_':
+            return demangle_main(pos, "", 1)
+        else:
+            return demangle_main(pos, ch, 0)
+
+    def demangle_main(pos, acc, ucount):
+        """Main demangling loop."""
+        while pos < length:
+            ch = s[pos]
+            pos += 1
+
+            if ch == '_':
+                ucount += 1
+                continue
+
+            if ucount % 2 == 0:
+                # Even underscores: literal underscores in component name
+                acc += '_' * (ucount // 2) + ch
+                ucount = 0
+                continue
+
+            # Odd ucount: separator or escape
+            if '0' <= ch <= '9':
+                # End current str component, start number
+                emit(acc + '_' * (ucount // 2))
+                if ch == '0' and pos < length and s[pos] == '0':
+                    pos += 1
+                    return demangle_main(pos, "", 0)
+                else:
+                    return decode_num(pos, ord(ch) - ord('0'))
+
+            # Try hex escapes
+            if ch == 'x':
+                result = _parse_hex(s, pos, 2)
+                if result is not None:
+                    new_pos, val = result
+                    acc += '_' * (ucount // 2) + chr(val)
+                    pos = new_pos
+                    ucount = 0
+                    continue
+
+            if ch == 'u':
+                result = _parse_hex(s, pos, 4)
+                if result is not None:
+                    new_pos, val = result
+                    acc += '_' * (ucount // 2) + chr(val)
+                    pos = new_pos
+                    ucount = 0
+                    continue
+
+            if ch == 'U':
+                result = _parse_hex(s, pos, 8)
+                if result is not None:
+                    new_pos, val = result
+                    acc += '_' * (ucount // 2) + chr(val)
+                    pos = new_pos
+                    ucount = 0
+                    continue
+
+            # Name separator
+            emit(acc)
+            acc = '_' * (ucount // 2) + ch
+            ucount = 0
+
+        # End of string
+        acc += '_' * (ucount // 2)
+        if acc:
+            emit(acc)
+        return pos
+
+    name_start(0)
+    return components
+
+
+# ---------------------------------------------------------------------------
+# Prefix handling for lp_ (package prefix)
+# ---------------------------------------------------------------------------
+
+def _is_valid_string_mangle(s):
+    """Check if s is a valid output of String.mangle (no trailing bare _)."""
+    pos = 0
+    length = len(s)
+    while pos < length:
+        ch = s[pos]
+        if _is_ascii_alnum(ch):
+            pos += 1
+        elif ch == '_':
+            if pos + 1 >= length:
+                return False  # trailing bare _
+            nch = s[pos + 1]
+            if nch == '_':
+                pos += 2
+            elif nch == 'x' and _parse_hex(s, pos + 2, 2) is not None:
+                pos = _parse_hex(s, pos + 2, 2)[0]
+            elif nch == 'u' and _parse_hex(s, pos + 2, 4) is not None:
+                pos = _parse_hex(s, pos + 2, 4)[0]
+            elif nch == 'U' and _parse_hex(s, pos + 2, 8) is not None:
+                pos = _parse_hex(s, pos + 2, 8)[0]
+            else:
+                return False
+        else:
+            return False
+    return True
+
+
+def _skip_string_mangle(s, pos):
+    """
+    Skip past a String.mangle output in s starting at pos.
+    Returns the position after the mangled string (where we expect the separator '_').
+    This is a greedy scan.
+    """
+    length = len(s)
+    while pos < length:
+        ch = s[pos]
+        if _is_ascii_alnum(ch):
+            pos += 1
+        elif ch == '_':
+            if pos + 1 < length:
+                nch = s[pos + 1]
+                if nch == '_':
+                    pos += 2
+                elif nch == 'x' and _parse_hex(s, pos + 2, 2) is not None:
+                    pos = _parse_hex(s, pos + 2, 2)[0]
+                elif nch == 'u' and _parse_hex(s, pos + 2, 4) is not None:
+                    pos = _parse_hex(s, pos + 2, 4)[0]
+                elif nch == 'U' and _parse_hex(s, pos + 2, 8) is not None:
+                    pos = _parse_hex(s, pos + 2, 8)[0]
+                else:
+                    return pos  # bare '_': separator
+            else:
+                return pos
+        else:
+            return pos
+    return pos
+
+
+def _find_lp_body(s):
+    """
+    Given s = everything after 'lp_' in a symbol, find where the declaration
+    body (Name.mangleAux output) starts.
+    Returns the start index of the body within s, or None.
+
+    Strategy: try all candidate split points where the package part is a valid
+    String.mangle output and the body round-trips. Prefer the longest valid
+    package name (most specific match).
+    """
+    length = len(s)
+
+    # Collect candidate split positions: every '_' that could be the separator
+    candidates = []
+    pos = 0
+    while pos < length:
+        if s[pos] == '_':
+            candidates.append(pos)
+        pos += 1
+
+    # Try each candidate; collect all valid splits
+    valid_splits = []
+    for split_pos in candidates:
+        pkg_part = s[:split_pos]
+        if not pkg_part:
+            continue
+        if not _is_valid_string_mangle(pkg_part):
+            continue
+        body = s[split_pos + 1:]
+        if not body:
+            continue
+        components = demangle_body(body)
+        if not components:
+            continue
+        remangled = mangle_name(components, prefix="")
+        if remangled == body:
+            first = components[0]
+            # Score: prefer first component starting with uppercase
+            has_upper = isinstance(first, str) and first and first[0].isupper()
+            valid_splits.append((split_pos, has_upper))
+
+    if valid_splits:
+        # Among splits where first decl component starts uppercase, pick longest pkg.
+        # Otherwise pick shortest pkg.
+        upper_splits = [s for s in valid_splits if s[1]]
+        if upper_splits:
+            best = max(upper_splits, key=lambda x: x[0])
+        else:
+            best = min(valid_splits, key=lambda x: x[0])
+        return best[0] + 1
+
+    # Fallback: greedy String.mangle scan
+    greedy_pos = _skip_string_mangle(s, 0)
+    if greedy_pos < length and s[greedy_pos] == '_':
+        return greedy_pos + 1
+
+    return None
+
+
+# ---------------------------------------------------------------------------
+# Format name components for display
+# ---------------------------------------------------------------------------
+
+def format_name(components):
+    """Format a list of name components as a dot-separated string."""
+    return '.'.join(str(c) for c in components)
+
+
+# ---------------------------------------------------------------------------
+# Human-friendly postprocessing
+# ---------------------------------------------------------------------------
+
+# Compiler-generated suffix components — exact match
+_SUFFIX_FLAGS_EXACT = {
+    '_redArg':  'arity\u2193',
+    '_boxed':   'boxed',
+    '_impl':    'impl',
+}
+
+# Compiler-generated suffix prefixes — match with optional _N index
+# e.g., _lam, _lam_0, _lam_3, _lambda_0, _closed_2
+_SUFFIX_FLAGS_PREFIX = {
+    '_lam':     '\u03bb',
+    '_lambda':  '\u03bb',
+    '_elam':    '\u03bb',
+    '_jp':      'jp',
+    '_closed':  'closed',
+}
+
+
+def _match_suffix(component):
+    """
+    Check if a string component is a compiler-generated suffix.
+    Returns the flag label or None.
+
+    Handles both exact matches (_redArg, _boxed) and indexed suffixes
+    (_lam_0, _lambda_2, _closed_0) produced by appendIndexAfter.
+    """
+    if not isinstance(component, str):
+        return None
+    if component in _SUFFIX_FLAGS_EXACT:
+        return _SUFFIX_FLAGS_EXACT[component]
+    if component in _SUFFIX_FLAGS_PREFIX:
+        return _SUFFIX_FLAGS_PREFIX[component]
+    # Check for indexed suffix: prefix + _N
+    for prefix, label in _SUFFIX_FLAGS_PREFIX.items():
+        if component.startswith(prefix + '_'):
+            rest = component[len(prefix) + 1:]
+            if rest.isdigit():
+                return label
+    return None
+
+
+def _strip_private(components):
+    """Strip _private.Module.0. prefix. Returns (stripped_parts, is_private)."""
+    if (len(components) >= 3 and isinstance(components[0], str) and
+            components[0] == '_private'):
+        for i in range(1, len(components)):
+            if components[i] == 0:
+                if i + 1 < len(components):
+                    return components[i + 1:], True
+                break
+    return components, False
+
+
+def _strip_spec_suffixes(components):
+    """Strip trailing spec_N components (from appendIndexAfter)."""
+    parts = list(components)
+    while parts and isinstance(parts[-1], str) and parts[-1].startswith('spec_'):
+        rest = parts[-1][5:]
+        if rest.isdigit():
+            parts.pop()
+        else:
+            break
+    return parts
+
+
+def _is_spec_index(component):
+    """Check if a component is a spec_N index (from appendIndexAfter)."""
+    return (isinstance(component, str) and
+            component.startswith('spec_') and component[5:].isdigit())
+
+
+def _parse_spec_entries(rest):
+    """Parse _at_..._spec pairs into separate spec context entries.
+
+    Given components starting from the first _at_, returns:
+    - entries: list of component lists, one per _at_..._spec block
+    - remaining: components after the last _spec N (trailing suffixes)
+    """
+    entries = []
+    current_ctx = None
+    remaining = []
+    skip_next = False
+
+    for p in rest:
+        if skip_next:
+            skip_next = False
+            continue
+        if isinstance(p, str) and p == '_at_':
+            if current_ctx is not None:
+                entries.append(current_ctx)
+            current_ctx = []
+            continue
+        if isinstance(p, str) and p == '_spec':
+            if current_ctx is not None:
+                entries.append(current_ctx)
+                current_ctx = None
+            skip_next = True
+            continue
+        if isinstance(p, str) and p.startswith('_spec'):
+            if current_ctx is not None:
+                entries.append(current_ctx)
+                current_ctx = None
+            continue
+        if current_ctx is not None:
+            current_ctx.append(p)
+        else:
+            remaining.append(p)
+
+    if current_ctx is not None:
+        entries.append(current_ctx)
+
+    return entries, remaining
+
+
+def _process_spec_context(components):
+    """Process a spec context into a clean name and its flags.
+
+    Returns (name_parts, flags) where name_parts are the cleaned components
+    and flags is a deduplicated list of flag labels from compiler suffixes.
+    """
+    parts = list(components)
+    parts, _ = _strip_private(parts)
+
+    name_parts = []
+    ctx_flags = []
+    seen = set()
+
+    for p in parts:
+        flag = _match_suffix(p)
+        if flag is not None:
+            if flag not in seen:
+                ctx_flags.append(flag)
+                seen.add(flag)
+        elif _is_spec_index(p):
+            pass
+        else:
+            name_parts.append(p)
+
+    return name_parts, ctx_flags
+
+
+def postprocess_name(components):
+    """
+    Transform raw demangled components into a human-friendly display string.
+
+    Applies:
+    - Private name cleanup: _private.Module.0.Name.foo -> Name.foo [private]
+    - Hygienic name cleanup: strips _@.module._hygCtx._hyg.N
+    - Suffix folding: _redArg, _boxed, _lam_0, etc. -> [flags]
+    - Specialization: f._at_.g._spec.N -> f spec at g
+      Shown after base [flags], with context flags: spec at g[ctx_flags]
+    """
+    if not components:
+        return ""
+
+    parts = list(components)
+    flags = []
+    spec_entries = []
+
+    # --- Strip _private prefix ---
+    parts, is_private = _strip_private(parts)
+
+    # --- Strip hygienic suffixes: everything from _@ onward ---
+    at_idx = None
+    for i, p in enumerate(parts):
+        if isinstance(p, str) and p.startswith('_@'):
+            at_idx = i
+            break
+    if at_idx is not None:
+        parts = parts[:at_idx]
+
+    # --- Handle specialization: _at_ ... _spec N ---
+    at_positions = [i for i, p in enumerate(parts)
+                    if isinstance(p, str) and p == '_at_']
+    if at_positions:
+        first_at = at_positions[0]
+        base = parts[:first_at]
+        rest = parts[first_at:]
+
+        entries, remaining = _parse_spec_entries(rest)
+        for ctx_components in entries:
+            ctx_name, ctx_flags = _process_spec_context(ctx_components)
+            if ctx_name or ctx_flags:
+                spec_entries.append((ctx_name, ctx_flags))
+
+        parts = base + remaining
+
+    # --- Collect suffix flags from the end ---
+    while parts:
+        last = parts[-1]
+        flag = _match_suffix(last)
+        if flag is not None:
+            flags.append(flag)
+            parts.pop()
+        elif isinstance(last, int) and len(parts) >= 2:
+            prev_flag = _match_suffix(parts[-2])
+            if prev_flag is not None:
+                flags.append(prev_flag)
+                parts.pop()  # remove the number
+                parts.pop()  # remove the suffix
+            else:
+                break
+        else:
+            break
+
+    if is_private:
+        flags.append('private')
+
+    # --- Format result ---
+    name = '.'.join(str(c) for c in parts) if parts else '?'
+    result = name
+    if flags:
+        flag_str = ', '.join(flags)
+        result += f' [{flag_str}]'
+
+    for ctx_name, ctx_flags in spec_entries:
+        ctx_str = '.'.join(str(c) for c in ctx_name) if ctx_name else '?'
+        if ctx_flags:
+            ctx_flag_str = ', '.join(ctx_flags)
+            result += f' spec at {ctx_str}[{ctx_flag_str}]'
+        else:
+            result += f' spec at {ctx_str}'
+
+    return result
+
+
+# ---------------------------------------------------------------------------
+# Main demangling entry point
+# ---------------------------------------------------------------------------
+
+def demangle_lean_name_raw(mangled):
+    """
+    Demangle a Lean C symbol, preserving all internal name components.
+
+    Returns the exact demangled name with all compiler-generated suffixes
+    intact. Use demangle_lean_name() for human-friendly output.
+    """
+    try:
+        return _demangle_lean_name_inner(mangled, human_friendly=False)
+    except Exception:
+        return mangled
+
+
+def demangle_lean_name(mangled):
+    """
+    Demangle a C symbol name produced by the Lean 4 compiler.
+
+    Returns a human-friendly demangled name with compiler suffixes folded
+    into readable flags. Use demangle_lean_name_raw() to preserve all
+    internal components.
+    """
+    try:
+        return _demangle_lean_name_inner(mangled, human_friendly=True)
+    except Exception:
+        return mangled
+
+
+def _demangle_lean_name_inner(mangled, human_friendly=True):
+    """Inner demangle that may raise on malformed input."""
+
+    if mangled == "_lean_main":
+        return "[lean] main"
+
+    # Handle lean_ runtime functions
+    if human_friendly and mangled.startswith("lean_apply_"):
+        rest = mangled[11:]
+        if rest.isdigit():
+            return f"<apply/{rest}>"
+
+    # Strip .cold.N suffix (LLVM linker cold function clones)
+    cold_suffix = ""
+    core = mangled
+    dot_pos = core.find('.cold.')
+    if dot_pos >= 0:
+        cold_suffix = " " + core[dot_pos:]
+        core = core[:dot_pos]
+    elif core.endswith('.cold'):
+        cold_suffix = " .cold"
+        core = core[:-5]
+
+    result = _demangle_core(core, human_friendly)
+    if result is None:
+        return mangled
+    return result + cold_suffix
+
+
+def _demangle_core(mangled, human_friendly=True):
+    """Demangle a symbol without .cold suffix. Returns None if not a Lean name."""
+
+    fmt = postprocess_name if human_friendly else format_name
+
+    # _init_ prefix
+    if mangled.startswith("_init_"):
+        rest = mangled[6:]
+        body, pkg_display = _strip_lean_prefix(rest)
+        if body is None:
+            return None
+        components = demangle_body(body)
+        if not components:
+            return None
+        name = fmt(components)
+        if pkg_display:
+            return f"[init] {name} ({pkg_display})"
+        return f"[init] {name}"
+
+    # initialize_ prefix (module init functions)
+    if mangled.startswith("initialize_"):
+        rest = mangled[11:]
+        # With package: initialize_lp_{pkg}_{body} or initialize_l_{body}
+        body, pkg_display = _strip_lean_prefix(rest)
+        if body is not None:
+            components = demangle_body(body)
+            if components:
+                name = fmt(components)
+                if pkg_display:
+                    return f"[module_init] {name} ({pkg_display})"
+                return f"[module_init] {name}"
+        # Without package: initialize_{Name.mangleAux(moduleName)}
+        if rest:
+            components = demangle_body(rest)
+            if components:
+                return f"[module_init] {fmt(components)}"
+        return None
+
+    # l_ or lp_ prefix
+    body, pkg_display = _strip_lean_prefix(mangled)
+    if body is None:
+        return None
+    components = demangle_body(body)
+    if not components:
+        return None
+    name = fmt(components)
+    if pkg_display:
+        return f"{name} ({pkg_display})"
+    return name
+
+
+def _strip_lean_prefix(s):
+    """
+    Strip the l_ or lp_ prefix from a mangled symbol.
+    Returns (body, pkg_display) where body is the Name.mangleAux output
+    and pkg_display is None or a string describing the package.
+    Returns (None, None) if the string doesn't have a recognized prefix.
+    """
+    if s.startswith("l_"):
+        return (s[2:], None)
+
+    if s.startswith("lp_"):
+        after_lp = s[3:]
+        body_start = _find_lp_body(after_lp)
+        if body_start is not None:
+            pkg_mangled = after_lp[:body_start - 1]
+            # Unmangle the package name
+            pkg_components = demangle_body(pkg_mangled)
+            if pkg_components and len(pkg_components) == 1 and isinstance(pkg_components[0], str):
+                pkg_display = pkg_components[0]
+            else:
+                pkg_display = pkg_mangled
+            return (after_lp[body_start:], pkg_display)
+        # Fallback: treat everything after lp_ as body
+        return (after_lp, "?")
+
+    return (None, None)
+
+
+# ---------------------------------------------------------------------------
+# CLI
+# ---------------------------------------------------------------------------
+
+def main():
+    """Filter stdin or arguments, demangling Lean names."""
+    import argparse
+    parser = argparse.ArgumentParser(
+        description="Demangle Lean 4 C symbol names (like c++filt for Lean)")
+    parser.add_argument('names', nargs='*',
+                        help='Names to demangle (reads stdin if none given)')
+    parser.add_argument('--raw', action='store_true',
+                        help='Output exact demangled names without postprocessing')
+    args = parser.parse_args()
+
+    demangle = demangle_lean_name_raw if args.raw else demangle_lean_name
+
+    if args.names:
+        for name in args.names:
+            print(demangle(name))
+    else:
+        for line in sys.stdin:
+            print(demangle(line.rstrip('\n')))
+
+
+if __name__ == '__main__':
+    main()

script/profiler/lean_demangle_profile.py

@@ -0,0 +1,117 @@
+#!/usr/bin/env python3
+"""
+Lean name demangler for samply / Firefox Profiler profiles.
+
+Reads a profile JSON (plain or gzipped), demangles Lean function names
+in the string table, and writes the result back.
+
+Usage:
+    python lean_demangle_profile.py profile.json -o profile-demangled.json
+    python lean_demangle_profile.py profile.json.gz -o profile-demangled.json.gz
+"""
+
+import argparse
+import gzip
+import json
+import sys
+
+from lean_demangle import demangle_lean_name
+
+
+def _demangle_string_array(string_array):
+    """Demangle Lean names in a string array in-place. Returns count."""
+    count = 0
+    for i, s in enumerate(string_array):
+        if not isinstance(s, str):
+            continue
+        demangled = demangle_lean_name(s)
+        if demangled != s:
+            string_array[i] = demangled
+            count += 1
+    return count
+
+
+def rewrite_profile(profile):
+    """
+    Demangle Lean names in a Firefox Profiler profile dict (in-place).
+
+    Handles two profile formats:
+    - Newer: shared.stringArray (single shared string table)
+    - Older/samply: per-thread stringArray (each thread has its own)
+    """
+    count = 0
+
+    # Shared string table (newer Firefox Profiler format)
+    shared = profile.get("shared")
+    if shared is not None:
+        sa = shared.get("stringArray")
+        if sa is not None:
+            count += _demangle_string_array(sa)
+
+    # Per-thread string tables (samply format)
+    for thread in profile.get("threads", []):
+        sa = thread.get("stringArray")
+        if sa is not None:
+            count += _demangle_string_array(sa)
+
+    return count
+
+
+def process_profile_file(input_path, output_path):
+    """Read a profile, demangle names, write it back."""
+    is_gzip = input_path.endswith('.gz')
+
+    if is_gzip:
+        with gzip.open(input_path, 'rt', encoding='utf-8') as f:
+            profile = json.load(f)
+    else:
+        with open(input_path, 'r', encoding='utf-8') as f:
+            profile = json.load(f)
+
+    count = rewrite_profile(profile)
+
+    out_gzip = output_path.endswith('.gz') if output_path else is_gzip
+
+    if output_path:
+        if out_gzip:
+            with gzip.open(output_path, 'wt', encoding='utf-8') as f:
+                json.dump(profile, f, ensure_ascii=False)
+        else:
+            with open(output_path, 'w', encoding='utf-8') as f:
+                json.dump(profile, f, ensure_ascii=False)
+    else:
+        json.dump(profile, sys.stdout, ensure_ascii=False)
+        sys.stdout.write('\n')
+
+    return count
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Demangle Lean names in samply/Firefox Profiler profiles")
+    parser.add_argument('input', help='Input profile (JSON or .json.gz)')
+    parser.add_argument('-o', '--output',
+                        help='Output path (default: stdout for JSON, '
+                             'or input with -demangled suffix)')
+    args = parser.parse_args()
+
+    output = args.output
+    if output is None and not sys.stdout.isatty():
+        output = None  # write to stdout
+    elif output is None:
+        # Generate output filename
+        inp = args.input
+        if inp.endswith('.json.gz'):
+            output = inp[:-8] + '-demangled.json.gz'
+        elif inp.endswith('.json'):
+            output = inp[:-5] + '-demangled.json'
+        else:
+            output = inp + '-demangled'
+
+    count = process_profile_file(args.input, output)
+    if output:
+        print(f"Demangled {count} names, wrote {output}", file=sys.stderr)
+
+
+if __name__ == '__main__':
+    main()

script/profiler/serve_profile.py

@@ -0,0 +1,94 @@
+#!/usr/bin/env python3
+"""
+Serve a Firefox Profiler JSON file and open it in the browser.
+
+Unlike `samply load`, this does NOT provide a symbolication API,
+so Firefox Profiler will use the names already in the profile as-is.
+"""
+
+import argparse
+import gzip
+import http.server
+import io
+import sys
+import threading
+import webbrowser
+import urllib.parse
+
+
+class ProfileHandler(http.server.BaseHTTPRequestHandler):
+    """Serve the profile JSON and handle CORS for Firefox Profiler."""
+
+    profile_data = None  # set by main()
+
+    def do_GET(self):
+        if self.path == "/profile.json":
+            self.send_response(200)
+            self.send_header("Content-Type", "application/json")
+            self.send_header("Content-Encoding", "gzip")
+            self.send_header("Access-Control-Allow-Origin", "*")
+            self.end_headers()
+            self.wfile.write(self.profile_data)
+        else:
+            self.send_response(404)
+            self.end_headers()
+
+    def do_OPTIONS(self):
+        # CORS preflight
+        self.send_response(200)
+        self.send_header("Access-Control-Allow-Origin", "*")
+        self.send_header("Access-Control-Allow-Methods", "GET")
+        self.send_header("Access-Control-Allow-Headers", "Content-Type")
+        self.end_headers()
+
+    def log_message(self, format, *args):
+        pass  # suppress request logs
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Serve a profile JSON for Firefox Profiler")
+    parser.add_argument("profile", help="Profile file (.json or .json.gz)")
+    parser.add_argument("-P", "--port", type=int, default=3457,
+                        help="Port to serve on (default: 3457)")
+    parser.add_argument("-n", "--no-open", action="store_true",
+                        help="Do not open the browser")
+    args = parser.parse_args()
+
+    # Read the profile data (keep it gzipped for efficient serving)
+    if args.profile.endswith(".gz"):
+        with open(args.profile, "rb") as f:
+            ProfileHandler.profile_data = f.read()
+    else:
+        with open(args.profile, "rb") as f:
+            raw = f.read()
+        buf = io.BytesIO()
+        with gzip.GzipFile(fileobj=buf, mode="wb") as gz:
+            gz.write(raw)
+        ProfileHandler.profile_data = buf.getvalue()
+
+    http.server.HTTPServer.allow_reuse_address = True
+    server = http.server.HTTPServer(("127.0.0.1", args.port), ProfileHandler)
+    profile_url = f"http://127.0.0.1:{args.port}/profile.json"
+    encoded = urllib.parse.quote(profile_url, safe="")
+    viewer_url = f"https://profiler.firefox.com/from-url/{encoded}"
+
+    if not args.no_open:
+        # Open browser after a short delay to let server start
+        def open_browser():
+            webbrowser.open(viewer_url)
+        threading.Timer(0.5, open_browser).start()
+
+    print(f"Serving profile at {profile_url}", file=sys.stderr)
+    print(f"Firefox Profiler: {viewer_url}", file=sys.stderr)
+    print("Press Ctrl+C to stop.", file=sys.stderr)
+
+    try:
+        server.serve_forever()
+    except KeyboardInterrupt:
+        print("\nStopped.", file=sys.stderr)
+        server.server_close()
+
+
+if __name__ == "__main__":
+    main()

script/profiler/symbolicate_profile.py

@@ -0,0 +1,198 @@
+#!/usr/bin/env python3
+"""
+Symbolicate a raw samply profile using samply's symbolication API,
+then demangle Lean names.
+
+Usage:
+    python symbolicate_profile.py --server http://127.0.0.1:3000/TOKEN \
+        raw-profile.json.gz -o symbolicated-demangled.json.gz
+"""
+
+import argparse
+import gzip
+import json
+import sys
+import urllib.request
+
+from lean_demangle import demangle_lean_name
+
+
+def symbolicate_and_demangle(profile, server_url):
+    """
+    Symbolicate a raw samply profile via the symbolication API,
+    then demangle Lean names. Modifies the profile in-place.
+    Returns the number of names resolved.
+    """
+    libs = profile.get("libs", [])
+    memory_map = [[lib["debugName"], lib["breakpadId"]] for lib in libs]
+
+    count = 0
+    for thread in profile.get("threads", []):
+        count += _process_thread(thread, libs, memory_map, server_url)
+
+    return count
+
+
+def _process_thread(thread, libs, memory_map, server_url):
+    """Symbolicate and demangle one thread. Returns count of resolved names."""
+    sa = thread.get("stringArray")
+    ft = thread.get("frameTable")
+    func_t = thread.get("funcTable")
+    rt = thread.get("resourceTable")
+
+    if not all([sa, ft, func_t, rt]):
+        return 0
+
+    # Build mapping: func_index -> (lib_index, address)
+    # A function may be referenced by multiple frames; pick any address.
+    func_info = {}  # func_idx -> (lib_idx, address)
+    for i in range(ft.get("length", 0)):
+        addr = ft["address"][i]
+        func_idx = ft["func"][i]
+        if func_idx in func_info:
+            continue
+        res_idx = func_t["resource"][func_idx]
+        if res_idx < 0 or res_idx >= rt.get("length", 0):
+            continue
+        lib_idx = rt["lib"][res_idx]
+        if lib_idx < 0 or lib_idx >= len(libs):
+            continue
+        func_info[func_idx] = (lib_idx, addr)
+
+    if not func_info:
+        return 0
+
+    # Batch symbolication: group by lib, send all addresses at once
+    frames_to_symbolicate = []
+    func_order = []  # track which func each frame corresponds to
+    for func_idx, (lib_idx, addr) in func_info.items():
+        frames_to_symbolicate.append([lib_idx, addr])
+        func_order.append(func_idx)
+
+    # Call the symbolication API
+    symbols = _call_symbolication_api(
+        server_url, memory_map, frames_to_symbolicate)
+
+    if not symbols:
+        return 0
+
+    # Update stringArray with demangled names
+    count = 0
+    for func_idx, symbol_name in zip(func_order, symbols):
+        if symbol_name is None:
+            continue
+        demangled = demangle_lean_name(symbol_name)
+        name_idx = func_t["name"][func_idx]
+        if name_idx < len(sa):
+            sa[name_idx] = demangled
+            count += 1
+
+    return count
+
+
+def _call_symbolication_api(server_url, memory_map, frames):
+    """
+    Call the Firefox Profiler symbolication API v5.
+    frames: list of [lib_index, address]
+    Returns: list of symbol names (or None for unresolved frames).
+    """
+    url = server_url.rstrip("/") + "/symbolicate/v5"
+
+    # Send all frames as one "stack" in one job
+    req_body = json.dumps({
+        "memoryMap": memory_map,
+        "stacks": [frames],
+    }).encode()
+
+    req = urllib.request.Request(
+        url,
+        data=req_body,
+        headers={"Content-Type": "application/json"},
+    )
+
+    try:
+        with urllib.request.urlopen(req, timeout=60) as resp:
+            result = json.loads(resp.read())
+    except Exception as e:
+        print(f"Symbolication API error: {e}", file=sys.stderr)
+        return None
+
+    if "error" in result:
+        print(f"Symbolication API error: {result['error']}", file=sys.stderr)
+        return None
+
+    # Extract symbol names from result
+    results = result.get("results", [])
+    if not results:
+        return None
+
+    stacks = results[0].get("stacks", [[]])
+    if not stacks:
+        return None
+
+    symbols = []
+    for frame_result in stacks[0]:
+        if isinstance(frame_result, dict):
+            symbols.append(frame_result.get("function"))
+        elif isinstance(frame_result, str):
+            symbols.append(frame_result)
+        else:
+            symbols.append(None)
+
+    return symbols
+
+
+def process_file(input_path, output_path, server_url):
+    """Read a raw profile, symbolicate + demangle, write it back."""
+    is_gzip = input_path.endswith('.gz')
+
+    if is_gzip:
+        with gzip.open(input_path, 'rt', encoding='utf-8') as f:
+            profile = json.load(f)
+    else:
+        with open(input_path, 'r', encoding='utf-8') as f:
+            profile = json.load(f)
+
+    count = symbolicate_and_demangle(profile, server_url)
+
+    out_gzip = output_path.endswith('.gz') if output_path else is_gzip
+    if output_path:
+        if out_gzip:
+            with gzip.open(output_path, 'wt', encoding='utf-8') as f:
+                json.dump(profile, f, ensure_ascii=False)
+        else:
+            with open(output_path, 'w', encoding='utf-8') as f:
+                json.dump(profile, f, ensure_ascii=False)
+    else:
+        json.dump(profile, sys.stdout, ensure_ascii=False)
+        sys.stdout.write('\n')
+
+    return count
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Symbolicate a raw samply profile and demangle Lean names")
+    parser.add_argument('input', help='Raw profile (JSON or .json.gz)')
+    parser.add_argument('-o', '--output', help='Output path')
+    parser.add_argument('--server', required=True,
+                        help='Samply server URL (e.g., http://127.0.0.1:3000/TOKEN)')
+    args = parser.parse_args()
+
+    output = args.output
+    if output is None:
+        inp = args.input
+        if inp.endswith('.json.gz'):
+            output = inp[:-8] + '-demangled.json.gz'
+        elif inp.endswith('.json'):
+            output = inp[:-5] + '-demangled.json'
+        else:
+            output = inp + '-demangled'
+
+    count = process_file(args.input, output, args.server)
+    print(f"Symbolicated and demangled {count} names, wrote {output}",
+          file=sys.stderr)
+
+
+if __name__ == '__main__':
+    main()

script/profiler/test_demangle.py

@@ -0,0 +1,670 @@
+#!/usr/bin/env python3
+"""Tests for the Lean name demangler."""
+
+import unittest
+import json
+import gzip
+import tempfile
+import os
+
+from lean_demangle import (
+    mangle_string, mangle_name, demangle_body, format_name,
+    demangle_lean_name, demangle_lean_name_raw, postprocess_name,
+    _parse_hex, _check_disambiguation,
+)
+
+
+class TestStringMangle(unittest.TestCase):
+    """Test String.mangle (character-level escaping)."""
+
+    def test_alphanumeric(self):
+        self.assertEqual(mangle_string("hello"), "hello")
+        self.assertEqual(mangle_string("abc123"), "abc123")
+
+    def test_underscore(self):
+        self.assertEqual(mangle_string("a_b"), "a__b")
+        self.assertEqual(mangle_string("_"), "__")
+        self.assertEqual(mangle_string("__"), "____")
+
+    def test_special_chars(self):
+        self.assertEqual(mangle_string("."), "_x2e")
+        self.assertEqual(mangle_string("a.b"), "a_x2eb")
+
+    def test_unicode(self):
+        self.assertEqual(mangle_string("\u03bb"), "_u03bb")
+        self.assertEqual(mangle_string("\U0001d55c"), "_U0001d55c")
+
+    def test_empty(self):
+        self.assertEqual(mangle_string(""), "")
+
+
+class TestNameMangle(unittest.TestCase):
+    """Test Name.mangle (hierarchical name mangling)."""
+
+    def test_simple(self):
+        self.assertEqual(mangle_name(["Lean", "Meta", "Sym", "main"]),
+                         "l_Lean_Meta_Sym_main")
+
+    def test_single_component(self):
+        self.assertEqual(mangle_name(["main"]), "l_main")
+
+    def test_numeric_component(self):
+        self.assertEqual(
+            mangle_name(["_private", "Lean", "Meta", "Basic", 0,
+                         "Lean", "Meta", "withMVarContextImp"]),
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp")
+
+    def test_component_with_underscore(self):
+        self.assertEqual(mangle_name(["a_b"]), "l_a__b")
+        self.assertEqual(mangle_name(["a_b", "c"]), "l_a__b_c")
+
+    def test_disambiguation_digit_start(self):
+        self.assertEqual(mangle_name(["0foo"]), "l_000foo")
+
+    def test_disambiguation_escape_start(self):
+        self.assertEqual(mangle_name(["a", "x27"]), "l_a_00x27")
+
+    def test_numeric_root(self):
+        self.assertEqual(mangle_name([42]), "l_42_")
+        self.assertEqual(mangle_name([42, "foo"]), "l_42__foo")
+
+    def test_component_ending_with_underscore(self):
+        self.assertEqual(mangle_name(["a_", "b"]), "l_a___00b")
+
+    def test_custom_prefix(self):
+        self.assertEqual(mangle_name(["foo"], prefix="lp_pkg_"),
+                         "lp_pkg_foo")
+
+
+class TestDemangleBody(unittest.TestCase):
+    """Test demangle_body (the core Name.demangleAux algorithm)."""
+
+    def test_simple(self):
+        self.assertEqual(demangle_body("Lean_Meta_Sym_main"),
+                         ["Lean", "Meta", "Sym", "main"])
+
+    def test_single(self):
+        self.assertEqual(demangle_body("main"), ["main"])
+
+    def test_empty(self):
+        self.assertEqual(demangle_body(""), [])
+
+    def test_underscore_in_component(self):
+        self.assertEqual(demangle_body("a__b"), ["a_b"])
+        self.assertEqual(demangle_body("a__b_c"), ["a_b", "c"])
+
+    def test_numeric_component(self):
+        self.assertEqual(demangle_body("foo_42__bar"), ["foo", 42, "bar"])
+
+    def test_numeric_root(self):
+        self.assertEqual(demangle_body("42_"), [42])
+
+    def test_numeric_at_end(self):
+        self.assertEqual(demangle_body("foo_42_"), ["foo", 42])
+
+    def test_disambiguation_00(self):
+        self.assertEqual(demangle_body("a_00x27"), ["a", "x27"])
+
+    def test_disambiguation_00_at_root(self):
+        self.assertEqual(demangle_body("000foo"), ["0foo"])
+
+    def test_hex_escape_x(self):
+        self.assertEqual(demangle_body("a_x2eb"), ["a.b"])
+
+    def test_hex_escape_u(self):
+        self.assertEqual(demangle_body("_u03bb"), ["\u03bb"])
+
+    def test_hex_escape_U(self):
+        self.assertEqual(demangle_body("_U0001d55c"), ["\U0001d55c"])
+
+    def test_private_name(self):
+        body = "__private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp"
+        self.assertEqual(demangle_body(body),
+                         ["_private", "Lean", "Meta", "Basic", 0,
+                          "Lean", "Meta", "withMVarContextImp"])
+
+    def test_boxed_suffix(self):
+        body = "foo___boxed"
+        self.assertEqual(demangle_body(body), ["foo", "_boxed"])
+
+    def test_redArg_suffix(self):
+        body = "foo_bar___redArg"
+        self.assertEqual(demangle_body(body), ["foo", "bar", "_redArg"])
+
+    def test_component_ending_underscore_disambiguation(self):
+        self.assertEqual(demangle_body("a___00b"), ["a_", "b"])
+
+
+class TestRoundTrip(unittest.TestCase):
+    """Test that mangle(demangle(x)) == x for various names."""
+
+    def _check_roundtrip(self, components):
+        mangled = mangle_name(components, prefix="")
+        demangled = demangle_body(mangled)
+        self.assertEqual(demangled, components,
+                         f"Round-trip failed: {components} -> '{mangled}' -> {demangled}")
+        mangled_with_prefix = mangle_name(components, prefix="l_")
+        self.assertTrue(mangled_with_prefix.startswith("l_"))
+        body = mangled_with_prefix[2:]
+        demangled2 = demangle_body(body)
+        self.assertEqual(demangled2, components)
+
+    def test_simple_names(self):
+        self._check_roundtrip(["Lean", "Meta", "main"])
+        self._check_roundtrip(["a"])
+        self._check_roundtrip(["Foo", "Bar", "baz"])
+
+    def test_numeric(self):
+        self._check_roundtrip(["foo", 0, "bar"])
+        self._check_roundtrip([42])
+        self._check_roundtrip(["a", 1, "b", 2, "c"])
+
+    def test_underscores(self):
+        self._check_roundtrip(["_private"])
+        self._check_roundtrip(["a_b", "c_d"])
+        self._check_roundtrip(["_at_", "_spec"])
+
+    def test_private_name(self):
+        self._check_roundtrip(["_private", "Lean", "Meta", "Basic", 0,
+                                "Lean", "Meta", "withMVarContextImp"])
+
+    def test_boxed(self):
+        self._check_roundtrip(["Lean", "Meta", "foo", "_boxed"])
+
+    def test_redArg(self):
+        self._check_roundtrip(["Lean", "Meta", "foo", "_redArg"])
+
+    def test_specialization(self):
+        self._check_roundtrip(["List", "map", "_at_", "Foo", "bar", "_spec", 3])
+
+    def test_lambda(self):
+        self._check_roundtrip(["Foo", "bar", "_lambda", 0])
+        self._check_roundtrip(["Foo", "bar", "_lambda", 2])
+
+    def test_closed(self):
+        self._check_roundtrip(["myConst", "_closed", 0])
+
+    def test_special_chars(self):
+        self._check_roundtrip(["a.b"])
+        self._check_roundtrip(["\u03bb"])
+        self._check_roundtrip(["a", "b\u2192c"])
+
+    def test_disambiguation_cases(self):
+        self._check_roundtrip(["a", "x27"])
+        self._check_roundtrip(["0foo"])
+        self._check_roundtrip(["a_", "b"])
+
+    def test_complex_real_names(self):
+        """Names modeled after real Lean compiler output."""
+        self._check_roundtrip(
+            ["Lean", "MVarId", "withContext", "_at_",
+             "_private", "Lean", "Meta", "Sym", 0,
+             "Lean", "Meta", "Sym", "BackwardRule", "apply",
+             "_spec", 2, "_redArg", "_lambda", 0, "_boxed"])
+
+
+class TestDemangleRaw(unittest.TestCase):
+    """Test demangle_lean_name_raw (exact demangling, no postprocessing)."""
+
+    def test_l_prefix(self):
+        self.assertEqual(
+            demangle_lean_name_raw("l_Lean_Meta_Sym_main"),
+            "Lean.Meta.Sym.main")
+
+    def test_l_prefix_private(self):
+        result = demangle_lean_name_raw(
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp")
+        self.assertEqual(result,
+                         "_private.Lean.Meta.Basic.0.Lean.Meta.withMVarContextImp")
+
+    def test_l_prefix_boxed(self):
+        result = demangle_lean_name_raw("l_foo___boxed")
+        self.assertEqual(result, "foo._boxed")
+
+    def test_l_prefix_redArg(self):
+        result = demangle_lean_name_raw(
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___redArg")
+        self.assertEqual(
+            result,
+            "_private.Lean.Meta.Basic.0.Lean.Meta.withMVarContextImp._redArg")
+
+    def test_lean_main(self):
+        self.assertEqual(demangle_lean_name_raw("_lean_main"), "[lean] main")
+
+    def test_non_lean_names(self):
+        self.assertEqual(demangle_lean_name_raw("printf"), "printf")
+        self.assertEqual(demangle_lean_name_raw("malloc"), "malloc")
+        self.assertEqual(demangle_lean_name_raw("lean_apply_5"), "lean_apply_5")
+        self.assertEqual(demangle_lean_name_raw(""), "")
+
+    def test_init_prefix(self):
+        result = demangle_lean_name_raw("_init_l_Lean_Meta_foo")
+        self.assertEqual(result, "[init] Lean.Meta.foo")
+
+    def test_lp_prefix_simple(self):
+        mangled = mangle_name(["Lean", "Meta", "foo"], prefix="lp_std_")
+        self.assertEqual(mangled, "lp_std_Lean_Meta_foo")
+        result = demangle_lean_name_raw(mangled)
+        self.assertEqual(result, "Lean.Meta.foo (std)")
+
+    def test_lp_prefix_underscore_pkg(self):
+        pkg_mangled = mangle_string("my_pkg")
+        self.assertEqual(pkg_mangled, "my__pkg")
+        mangled = mangle_name(["Lean", "Meta", "foo"],
+                              prefix=f"lp_{pkg_mangled}_")
+        self.assertEqual(mangled, "lp_my__pkg_Lean_Meta_foo")
+        result = demangle_lean_name_raw(mangled)
+        self.assertEqual(result, "Lean.Meta.foo (my_pkg)")
+
+    def test_lp_prefix_private_decl(self):
+        mangled = mangle_name(
+            ["_private", "X", 0, "Y", "foo"], prefix="lp_pkg_")
+        self.assertEqual(mangled, "lp_pkg___private_X_0__Y_foo")
+        result = demangle_lean_name_raw(mangled)
+        self.assertEqual(result, "_private.X.0.Y.foo (pkg)")
+
+    def test_complex_specialization(self):
+        components = [
+            "Lean", "MVarId", "withContext", "_at_",
+            "_private", "Lean", "Meta", "Sym", 0,
+            "Lean", "Meta", "Sym", "BackwardRule", "apply",
+            "_spec", 2, "_redArg", "_lambda", 0, "_boxed"
+        ]
+        mangled = mangle_name(components)
+        result = demangle_lean_name_raw(mangled)
+        expected = format_name(components)
+        self.assertEqual(result, expected)
+
+    def test_cold_suffix(self):
+        result = demangle_lean_name_raw("l_Lean_Meta_foo___redArg.cold.1")
+        self.assertEqual(result, "Lean.Meta.foo._redArg .cold.1")
+
+    def test_cold_suffix_plain(self):
+        result = demangle_lean_name_raw("l_Lean_Meta_foo.cold")
+        self.assertEqual(result, "Lean.Meta.foo .cold")
+
+    def test_initialize_no_pkg(self):
+        result = demangle_lean_name_raw("initialize_Init_Control_Basic")
+        self.assertEqual(result, "[module_init] Init.Control.Basic")
+
+    def test_initialize_with_l_prefix(self):
+        result = demangle_lean_name_raw("initialize_l_Lean_Meta_foo")
+        self.assertEqual(result, "[module_init] Lean.Meta.foo")
+
+    def test_never_crashes(self):
+        """Demangling should never raise, just return the original."""
+        weird_inputs = [
+            "", "l_", "lp_", "lp_x", "_init_", "initialize_",
+            "l_____", "lp____", "l_00", "l_0",
+            "some random string", "l_ space",
+        ]
+        for inp in weird_inputs:
+            result = demangle_lean_name_raw(inp)
+            self.assertIsInstance(result, str)
+
+
+class TestPostprocess(unittest.TestCase):
+    """Test postprocess_name (human-friendly suffix folding, etc.)."""
+
+    def test_no_change(self):
+        self.assertEqual(postprocess_name(["Lean", "Meta", "main"]),
+                         "Lean.Meta.main")
+
+    def test_boxed(self):
+        self.assertEqual(postprocess_name(["foo", "_boxed"]),
+                         "foo [boxed]")
+
+    def test_redArg(self):
+        self.assertEqual(postprocess_name(["foo", "bar", "_redArg"]),
+                         "foo.bar [arity\u2193]")
+
+    def test_lambda_separate(self):
+        # _lam as separate component + numeric index
+        self.assertEqual(postprocess_name(["foo", "_lam", 0]),
+                         "foo [\u03bb]")
+
+    def test_lambda_indexed(self):
+        # _lam_0 as single string (appendIndexAfter)
+        self.assertEqual(postprocess_name(["foo", "_lam_0"]),
+                         "foo [\u03bb]")
+        self.assertEqual(postprocess_name(["foo", "_lambda_2"]),
+                         "foo [\u03bb]")
+
+    def test_lambda_boxed(self):
+        # _lam_0 followed by _boxed
+        self.assertEqual(
+            postprocess_name(["Lean", "Meta", "Simp", "simpLambda",
+                              "_lam_0", "_boxed"]),
+            "Lean.Meta.Simp.simpLambda [boxed, \u03bb]")
+
+    def test_closed(self):
+        self.assertEqual(postprocess_name(["myConst", "_closed", 3]),
+                         "myConst [closed]")
+
+    def test_closed_indexed(self):
+        self.assertEqual(postprocess_name(["myConst", "_closed_0"]),
+                         "myConst [closed]")
+
+    def test_multiple_suffixes(self):
+        self.assertEqual(postprocess_name(["foo", "_redArg", "_boxed"]),
+                         "foo [boxed, arity\u2193]")
+
+    def test_redArg_lam(self):
+        # _redArg followed by _lam_0 (issue #4)
+        self.assertEqual(
+            postprocess_name(["Lean", "profileitIOUnsafe",
+                              "_redArg", "_lam_0"]),
+            "Lean.profileitIOUnsafe [\u03bb, arity\u2193]")
+
+    def test_private_name(self):
+        self.assertEqual(
+            postprocess_name(["_private", "Lean", "Meta", "Basic", 0,
+                              "Lean", "Meta", "withMVarContextImp"]),
+            "Lean.Meta.withMVarContextImp [private]")
+
+    def test_private_with_suffix(self):
+        self.assertEqual(
+            postprocess_name(["_private", "Lean", "Meta", "Basic", 0,
+                              "Lean", "Meta", "foo", "_redArg"]),
+            "Lean.Meta.foo [arity\u2193, private]")
+
+    def test_hygienic_strip(self):
+        self.assertEqual(
+            postprocess_name(["Lean", "Meta", "foo", "_@", "Lean", "Meta",
+                              "_hyg", 42]),
+            "Lean.Meta.foo")
+
+    def test_specialization(self):
+        self.assertEqual(
+            postprocess_name(["List", "map", "_at_", "Foo", "bar",
+                              "_spec", 3]),
+            "List.map spec at Foo.bar")
+
+    def test_specialization_with_suffix(self):
+        # Base suffix _boxed appears in [flags] before spec at
+        self.assertEqual(
+            postprocess_name(["Lean", "MVarId", "withContext", "_at_",
+                              "Foo", "bar", "_spec", 2, "_boxed"]),
+            "Lean.MVarId.withContext [boxed] spec at Foo.bar")
+
+    def test_spec_context_with_flags(self):
+        # Compiler suffixes in spec context become context flags
+        self.assertEqual(
+            postprocess_name(["Lean", "Meta", "foo", "_at_",
+                              "Lean", "Meta", "bar", "_elam_1", "_redArg",
+                              "_spec", 2]),
+            "Lean.Meta.foo spec at Lean.Meta.bar[\u03bb, arity\u2193]")
+
+    def test_spec_context_flags_dedup(self):
+        # Duplicate flag labels are deduplicated
+        self.assertEqual(
+            postprocess_name(["f", "_at_",
+                              "g", "_lam_0", "_elam_1", "_redArg",
+                              "_spec", 1]),
+            "f spec at g[\u03bb, arity\u2193]")
+
+    def test_multiple_at(self):
+        # Multiple _at_ entries become separate spec at clauses
+        self.assertEqual(
+            postprocess_name(["f", "_at_", "g", "_spec", 1,
+                              "_at_", "h", "_spec", 2]),
+            "f spec at g spec at h")
+
+    def test_multiple_at_with_flags(self):
+        # Multiple spec at with flags on base and contexts
+        self.assertEqual(
+            postprocess_name(["f", "_at_", "g", "_redArg", "_spec", 1,
+                              "_at_", "h", "_lam_0", "_spec", 2,
+                              "_boxed"]),
+            "f [boxed] spec at g[arity\u2193] spec at h[\u03bb]")
+
+    def test_base_flags_before_spec(self):
+        # Base trailing suffixes appear in [flags] before spec at
+        self.assertEqual(
+            postprocess_name(["f", "_at_", "g", "_spec", 1, "_lam_0"]),
+            "f [\u03bb] spec at g")
+
+    def test_spec_context_strip_spec_suffixes(self):
+        # spec_0 in context should be stripped
+        self.assertEqual(
+            postprocess_name(["Lean", "Meta", "transformWithCache", "visit",
+                              "_at_",
+                              "_private", "Lean", "Meta", "Transform", 0,
+                              "Lean", "Meta", "transform",
+                              "Lean", "Meta", "Sym", "unfoldReducible",
+                              "spec_0", "spec_0",
+                              "_spec", 1]),
+            "Lean.Meta.transformWithCache.visit "
+            "spec at Lean.Meta.transform.Lean.Meta.Sym.unfoldReducible")
+
+    def test_spec_context_strip_private(self):
+        # _private in spec context should be stripped
+        self.assertEqual(
+            postprocess_name(["Array", "mapMUnsafe", "map", "_at_",
+                              "_private", "Lean", "Meta", "Transform", 0,
+                              "Lean", "Meta", "transformWithCache", "visit",
+                              "_spec", 1]),
+            "Array.mapMUnsafe.map "
+            "spec at Lean.Meta.transformWithCache.visit")
+
+    def test_empty(self):
+        self.assertEqual(postprocess_name([]), "")
+
+
+class TestDemangleHumanFriendly(unittest.TestCase):
+    """Test demangle_lean_name (human-friendly output)."""
+
+    def test_simple(self):
+        self.assertEqual(demangle_lean_name("l_Lean_Meta_main"),
+                         "Lean.Meta.main")
+
+    def test_boxed(self):
+        self.assertEqual(demangle_lean_name("l_foo___boxed"),
+                         "foo [boxed]")
+
+    def test_redArg(self):
+        self.assertEqual(demangle_lean_name("l_foo___redArg"),
+                         "foo [arity\u2193]")
+
+    def test_private(self):
+        self.assertEqual(
+            demangle_lean_name(
+                "l___private_Lean_Meta_Basic_0__Lean_Meta_foo"),
+            "Lean.Meta.foo [private]")
+
+    def test_private_with_redArg(self):
+        self.assertEqual(
+            demangle_lean_name(
+                "l___private_Lean_Meta_Basic_0__Lean_Meta_foo___redArg"),
+            "Lean.Meta.foo [arity\u2193, private]")
+
+    def test_cold_with_suffix(self):
+        self.assertEqual(
+            demangle_lean_name("l_Lean_Meta_foo___redArg.cold.1"),
+            "Lean.Meta.foo [arity\u2193] .cold.1")
+
+    def test_lean_apply(self):
+        self.assertEqual(demangle_lean_name("lean_apply_5"), "<apply/5>")
+        self.assertEqual(demangle_lean_name("lean_apply_12"), "<apply/12>")
+
+    def test_lean_apply_raw_unchanged(self):
+        self.assertEqual(demangle_lean_name_raw("lean_apply_5"),
+                         "lean_apply_5")
+
+    def test_init_private(self):
+        self.assertEqual(
+            demangle_lean_name(
+                "_init_l___private_X_0__Y_foo"),
+            "[init] Y.foo [private]")
+
+    def test_complex_specialization(self):
+        components = [
+            "Lean", "MVarId", "withContext", "_at_",
+            "_private", "Lean", "Meta", "Sym", 0,
+            "Lean", "Meta", "Sym", "BackwardRule", "apply",
+            "_spec", 2, "_redArg", "_lambda", 0, "_boxed"
+        ]
+        mangled = mangle_name(components)
+        result = demangle_lean_name(mangled)
+        # Base: Lean.MVarId.withContext with trailing _redArg, _lambda 0, _boxed
+        # Spec context: Lean.Meta.Sym.BackwardRule.apply (private stripped)
+        self.assertEqual(
+            result,
+            "Lean.MVarId.withContext [boxed, \u03bb, arity\u2193] "
+            "spec at Lean.Meta.Sym.BackwardRule.apply")
+
+    def test_non_lean_unchanged(self):
+        self.assertEqual(demangle_lean_name("printf"), "printf")
+        self.assertEqual(demangle_lean_name("malloc"), "malloc")
+        self.assertEqual(demangle_lean_name(""), "")
+
+
+class TestDemangleProfile(unittest.TestCase):
+    """Test the profile rewriter."""
+
+    def _make_profile_shared(self, strings):
+        """Create a profile with shared.stringArray (newer format)."""
+        return {
+            "meta": {"version": 28},
+            "libs": [],
+            "shared": {
+                "stringArray": list(strings),
+            },
+            "threads": [{
+                "name": "main",
+                "pid": "1",
+                "tid": 1,
+                "funcTable": {
+                    "name": list(range(len(strings))),
+                    "isJS": [False] * len(strings),
+                    "relevantForJS": [False] * len(strings),
+                    "resource": [-1] * len(strings),
+                    "fileName": [None] * len(strings),
+                    "lineNumber": [None] * len(strings),
+                    "columnNumber": [None] * len(strings),
+                    "length": len(strings),
+                },
+                "frameTable": {"length": 0},
+                "stackTable": {"length": 0},
+                "samples": {"length": 0},
+                "markers": {"length": 0},
+                "resourceTable": {"length": 0},
+                "nativeSymbols": {"length": 0},
+            }],
+            "pages": [],
+            "counters": [],
+        }
+
+    def _make_profile_per_thread(self, strings):
+        """Create a profile with per-thread stringArray (samply format)."""
+        return {
+            "meta": {"version": 28},
+            "libs": [],
+            "threads": [{
+                "name": "main",
+                "pid": "1",
+                "tid": 1,
+                "stringArray": list(strings),
+                "funcTable": {
+                    "name": list(range(len(strings))),
+                    "isJS": [False] * len(strings),
+                    "relevantForJS": [False] * len(strings),
+                    "resource": [-1] * len(strings),
+                    "fileName": [None] * len(strings),
+                    "lineNumber": [None] * len(strings),
+                    "columnNumber": [None] * len(strings),
+                    "length": len(strings),
+                },
+                "frameTable": {"length": 0},
+                "stackTable": {"length": 0},
+                "samples": {"length": 0},
+                "markers": {"length": 0},
+                "resourceTable": {"length": 0},
+                "nativeSymbols": {"length": 0},
+            }],
+            "pages": [],
+            "counters": [],
+        }
+
+    def test_profile_rewrite_shared(self):
+        from lean_demangle_profile import rewrite_profile
+        strings = [
+            "l_Lean_Meta_Sym_main",
+            "printf",
+            "lean_apply_5",
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_foo",
+        ]
+        profile = self._make_profile_shared(strings)
+        rewrite_profile(profile)
+        sa = profile["shared"]["stringArray"]
+        self.assertEqual(sa[0], "Lean.Meta.Sym.main")
+        self.assertEqual(sa[1], "printf")
+        self.assertEqual(sa[2], "<apply/5>")
+        self.assertEqual(sa[3], "Lean.Meta.foo [private]")
+
+    def test_profile_rewrite_per_thread(self):
+        from lean_demangle_profile import rewrite_profile
+        strings = [
+            "l_Lean_Meta_Sym_main",
+            "printf",
+            "lean_apply_5",
+            "l___private_Lean_Meta_Basic_0__Lean_Meta_foo",
+        ]
+        profile = self._make_profile_per_thread(strings)
+        count = rewrite_profile(profile)
+        sa = profile["threads"][0]["stringArray"]
+        self.assertEqual(sa[0], "Lean.Meta.Sym.main")
+        self.assertEqual(sa[1], "printf")
+        self.assertEqual(sa[2], "<apply/5>")
+        self.assertEqual(sa[3], "Lean.Meta.foo [private]")
+        self.assertEqual(count, 3)
+
+    def test_profile_json_roundtrip(self):
+        from lean_demangle_profile import process_profile_file
+        strings = ["l_Lean_Meta_main", "malloc"]
+        profile = self._make_profile_shared(strings)
+
+        with tempfile.NamedTemporaryFile(mode='w', suffix='.json',
+                                         delete=False) as f:
+            json.dump(profile, f)
+            inpath = f.name
+
+        outpath = inpath.replace('.json', '-demangled.json')
+        try:
+            process_profile_file(inpath, outpath)
+            with open(outpath) as f:
+                result = json.load(f)
+            self.assertEqual(result["shared"]["stringArray"][0],
+                             "Lean.Meta.main")
+            self.assertEqual(result["shared"]["stringArray"][1], "malloc")
+        finally:
+            os.unlink(inpath)
+            if os.path.exists(outpath):
+                os.unlink(outpath)
+
+    def test_profile_gzip_roundtrip(self):
+        from lean_demangle_profile import process_profile_file
+        strings = ["l_Lean_Meta_main", "malloc"]
+        profile = self._make_profile_shared(strings)
+
+        with tempfile.NamedTemporaryFile(suffix='.json.gz',
+                                         delete=False) as f:
+            with gzip.open(f, 'wt') as gz:
+                json.dump(profile, gz)
+            inpath = f.name
+
+        outpath = inpath.replace('.json.gz', '-demangled.json.gz')
+        try:
+            process_profile_file(inpath, outpath)
+            with gzip.open(outpath, 'rt') as f:
+                result = json.load(f)
+            self.assertEqual(result["shared"]["stringArray"][0],
+                             "Lean.Meta.main")
+        finally:
+            os.unlink(inpath)
+            if os.path.exists(outpath):
+                os.unlink(outpath)
+
+
+if __name__ == '__main__':
+    unittest.main()

script/release_checklist.py

@@ -836,6 +836,14 @@ def main():
             continue
         print(f"  ✅ On compatible toolchain (>= {toolchain})")
 
+        # For reference-manual, check that the release notes title is correct BEFORE tagging.
+        # This catches the case where the toolchain bump PR was merged without updating
+        # the release notes title (e.g., still showing "-rc1" for a stable release).
+        if name == "reference-manual":
+            if not check_reference_manual_release_title(url, toolchain, branch, github_token):
+                repo_status[name] = False
+                continue
+
         # Special handling for ProofWidgets4
         if name == "ProofWidgets4":
             if not check_proofwidgets4_release(url, toolchain, github_token):

script/release_repos.yml

@@ -65,13 +65,6 @@ repositories:
     branch: master
     dependencies: [lean4-unicode-basic]
 
-  - name: doc-gen4
-    url: https://github.com/leanprover/doc-gen4
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies: [lean4-cli, BibtexQuery]
-
   - name: reference-manual
     url: https://github.com/leanprover/reference-manual
     toolchain-tag: true
@@ -84,8 +77,7 @@ repositories:
     toolchain-tag: false
     stable-branch: false
     branch: main
-    dependencies:
-      - batteries
+    dependencies: []
 
   - name: aesop
     url: https://github.com/leanprover-community/aesop
@@ -107,10 +99,16 @@ repositories:
       - lean4checker
       - batteries
       - lean4-cli
-      - doc-gen4
       - import-graph
       - plausible
 
+  - name: doc-gen4
+    url: https://github.com/leanprover/doc-gen4
+    toolchain-tag: true
+    stable-branch: false
+    branch: main
+    dependencies: [lean4-cli, BibtexQuery, mathlib4]
+
   - name: cslib
     url: https://github.com/leanprover/cslib
     toolchain-tag: true

script/release_steps.py

@@ -24,6 +24,7 @@ What this script does:
    - Safety checks for repositories using bump branches
    - Custom build and test procedures
    - lean-fro.org: runs scripts/update.sh to regenerate site content
+   - mathlib4: updates ProofWidgets4 pin (v0.0.X sequential tags, not v4.X.Y)
 
 6. Commits the changes with message "chore: bump toolchain to {version}"
 
@@ -59,6 +60,8 @@ import re
 import subprocess
 import shutil
 import json
+import requests
+import base64
 from pathlib import Path
 
 # Color functions for terminal output
@@ -115,6 +118,60 @@ def find_repo(repo_name, config):
         sys.exit(1)
     return matching_repos[0]
 
+def get_github_token():
+    try:
+        result = subprocess.run(['gh', 'auth', 'token'], capture_output=True, text=True)
+        if result.returncode == 0:
+            return result.stdout.strip()
+    except FileNotFoundError:
+        pass
+    return None
+
+def find_proofwidgets_tag(version):
+    """Find the latest ProofWidgets4 tag that uses the given toolchain version.
+
+    ProofWidgets4 uses sequential version tags (v0.0.X) rather than toolchain-based tags.
+    This function finds the most recent tag whose lean-toolchain matches the target version
+    exactly, checking the 20 most recent tags.
+    """
+    github_token = get_github_token()
+    api_base = "https://api.github.com/repos/leanprover-community/ProofWidgets4"
+    headers = {'Authorization': f'token {github_token}'} if github_token else {}
+
+    response = requests.get(f"{api_base}/git/matching-refs/tags/v0.0.", headers=headers, timeout=30)
+    if response.status_code != 200:
+        return None
+
+    tags = response.json()
+    tag_names = []
+    for tag in tags:
+        ref = tag['ref']
+        if ref.startswith('refs/tags/v0.0.'):
+            tag_name = ref.replace('refs/tags/', '')
+            try:
+                version_num = int(tag_name.split('.')[-1])
+                tag_names.append((version_num, tag_name))
+            except (ValueError, IndexError):
+                continue
+
+    if not tag_names:
+        return None
+
+    # Sort by version number (descending) and check recent tags
+    tag_names.sort(reverse=True)
+    target = f"leanprover/lean4:{version}"
+    for _, tag_name in tag_names[:20]:
+        # Fetch lean-toolchain for this tag
+        api_url = f"{api_base}/contents/lean-toolchain?ref={tag_name}"
+        resp = requests.get(api_url, headers=headers, timeout=30)
+        if resp.status_code != 200:
+            continue
+        content = base64.b64decode(resp.json().get("content", "").replace("\n", "")).decode('utf-8').strip()
+        if content == target:
+            return tag_name
+
+    return None
+
 def setup_downstream_releases_dir():
     """Create the downstream_releases directory if it doesn't exist."""
     downstream_dir = Path("downstream_releases")
@@ -426,6 +483,62 @@ def execute_release_steps(repo, version, config):
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
 
+    # For reference-manual, update the release notes title to match the target version.
+    # e.g., for a stable release, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0 (date)"
+    # e.g., for rc2, change "Lean 4.28.0-rc1 (date)" to "Lean 4.28.0-rc2 (date)"
+    if repo_name == "reference-manual":
+        base_version = version.lstrip('v').split('-')[0]  # "4.28.0"
+        file_name = f"v{base_version.replace('.', '_')}.lean"
+        release_notes_file = repo_path / "Manual" / "Releases" / file_name
+
+        if release_notes_file.exists():
+            is_rc = "-rc" in version
+            if is_rc:
+                # For RC releases, update to the exact RC version
+                display_version = version.lstrip('v')  # "4.28.0-rc2"
+            else:
+                # For stable releases, strip any RC suffix
+                display_version = base_version  # "4.28.0"
+
+            print(blue(f"Updating release notes title in {file_name}..."))
+            content = release_notes_file.read_text()
+            # Match the #doc line title: "Lean X.Y.Z-rcN (date)" or "Lean X.Y.Z (date)"
+            new_content = re.sub(
+                r'(#doc\s+\(Manual\)\s+"Lean\s+)\d+\.\d+\.\d+(-rc\d+)?(\s+\([^)]*\)"\s*=>)',
+                rf'\g<1>{display_version}\3',
+                content
+            )
+            if new_content != content:
+                release_notes_file.write_text(new_content)
+                print(green(f"Updated release notes title to Lean {display_version}"))
+            else:
+                print(green("Release notes title already correct"))
+        else:
+            print(yellow(f"Release notes file {file_name} not found, skipping title update"))
+
+    # For mathlib4, update ProofWidgets4 pin (it uses sequential v0.0.X tags, not v4.X.Y)
+    if repo_name == "mathlib4":
+        print(blue("Checking ProofWidgets4 version pin..."))
+        pw_tag = find_proofwidgets_tag(version)
+        if pw_tag:
+            print(blue(f"Updating ProofWidgets4 pin to {pw_tag}..."))
+            for lakefile in repo_path.glob("lakefile.*"):
+                content = lakefile.read_text()
+                # Only update the ProofWidgets4 dependency line, not other v0.0.X pins
+                new_content = re.sub(
+                    r'(require\s+"leanprover-community"\s*/\s*"proofwidgets"\s*@\s*git\s+"v)0\.0\.\d+(")',
+                    rf'\g<1>{pw_tag.removeprefix("v")}\2',
+                    content
+                )
+                if new_content != content:
+                    lakefile.write_text(new_content)
+                    print(green(f"Updated ProofWidgets4 pin in {lakefile.name}"))
+            run_command("lake update proofwidgets", cwd=repo_path, stream_output=True)
+            print(green(f"Updated ProofWidgets4 to {pw_tag}"))
+        else:
+            print(yellow(f"Could not find a ProofWidgets4 tag for toolchain {version}"))
+            print(yellow("You may need to update the ProofWidgets4 pin manually"))
+
     # Commit changes (only if there are changes)
     print(blue("Checking for changes to commit..."))
     try:

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  -- make sure `Try.Config` can be evaluated anywhere
+public meta import Init.Try  -- shake: keep (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,7 +7,8 @@ Authors: Joachim Breitner
 module
 
 prelude
-public import Init.Tactics
+public import Init.Prelude
+import Init.Tactics
 
 public section
 

src/Init/BinderPredicates.lean

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

src/Init/ByCases.lean

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

src/Init/Classical.lean

@@ -142,6 +142,7 @@ 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,3 +17,4 @@ 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 [instForInOfForIn']
+  simp [forIn]
   congr
   apply funext
   intro a
@@ -322,6 +322,8 @@ 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
@@ -349,6 +351,8 @@ 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,6 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString.Basic
+public import Init.Control.State
 
 public section
 universe u v

src/Init/Control/ExceptCps.lean

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

src/Init/Control/Id.lean

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

src/Init/Control/Lawful/Basic.lean

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

src/Init/Control/Lawful/Instances.lean

@@ -12,6 +12,8 @@ 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
 
@@ -28,6 +30,8 @@ namespace ExceptT
   simp [run] at h
   assumption
 
+@[simp] theorem stM_eq [Monad m] : stM m (ExceptT ε m) α = Except ε α := rfl
+
 @[simp, grind =] theorem run_mk (x : m (Except ε α)) : run (mk x : ExceptT ε m α) = x := rfl
 
 @[simp, grind =] theorem run_pure [Monad m] (x : α) : run (pure x : ExceptT ε m α) = pure (Except.ok x) := rfl
@@ -102,7 +106,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 [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
+  simp only [Functor.map, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
     pure_bind]
 
 /-! Note that the `MonadControl` instance for `ExceptT` is not monad-generic. -/
@@ -116,11 +120,16 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ExceptT ε m β → m (stM m (ExceptT ε m) β)) → m (stM m (ExceptT ε m) α)) :
     ExceptT.run (controlAt m f) = f fun x => x.run := by
-  simp [controlAt, run_bind, bind_map_left]
+  simp [controlAt, run_bind]
 
 @[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 -/
@@ -249,6 +258,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where
   rw [← bind_pure_comp]
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → OptionT m β → m (stM m (OptionT m) β)) → m (stM m (OptionT m) α)) :
     OptionT.run (controlAt m f) = f fun x => x.run := by
   simp [controlAt, Option.elimM, Option.elim]
@@ -336,6 +346,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where
     ReaderT.run (liftWith f) ctx = (f fun x => x.run ctx) :=
   rfl
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → ReaderT ρ m β → m (stM m (ReaderT ρ m) β)) → m (stM m (ReaderT ρ m) α)) (ctx : ρ) :
     ReaderT.run (controlAt m f) ctx = f fun x => x.run ctx := by
   simp [controlAt]
@@ -436,6 +447,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
     StateT.run (liftWith f) s = ((·, s) <$> f fun x => x.run s) := by
   simp [liftWith, MonadControl.liftWith, Function.comp_def]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem run_controlAt [Monad m] [LawfulMonad m] (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m (stM m (StateT σ m) α)) (s : σ) :
     StateT.run (controlAt m f) s = f fun x => x.run s := by
   simp [controlAt]
@@ -467,15 +479,33 @@ 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
-    dsimp only [EStateM.instMonad, EStateM.map]
+    simp only [Functor.map, EStateM.map]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
   (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
-    dsimp only [EStateM.instMonad, EStateM.bind]
+    simp only [bind, EStateM.bind]
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)

src/Init/Control/Lawful/Lemmas.lean

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

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

@@ -6,14 +6,17 @@ 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
   map_attach := by
-    simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach]
+    simp only [Functor.map, MonadAttach.attach, Functor.map_map, WeaklyLawfulMonadAttach.map_attach,
+      MonadAttach.CanReturn]
     intros; rfl
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
@@ -28,7 +31,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAtta
   map_attach := by
     intro α x
     simp only [Functor.map, StateT, funext_iff, StateT.map, bind_pure_comp, MonadAttach.attach,
-      Functor.map_map]
+      Functor.map_map, MonadAttach.CanReturn]
     exact fun s => WeaklyLawfulMonadAttach.map_attach
 
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] :
@@ -43,7 +46,7 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m]
 public instance [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (ExceptT ε m) where
   map_attach {α} x := by
-    simp only [Functor.map, MonadAttach.attach, ExceptT.map]
+    simp only [Functor.map, MonadAttach.attach, ExceptT.map, MonadAttach.CanReturn]
     simp
     conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (m := m) (x := x)]
     simp only [map_eq_pure_bind]
@@ -81,6 +84,6 @@ attribute [local instance] MonadAttach.trivial
 
 public instance [Monad m] [LawfulMonad m] :
     WeaklyLawfulMonadAttach m where
-  map_attach := by simp [MonadAttach.attach]
+  map_attach := by simp [MonadAttach.attach, MonadAttach.CanReturn]
 
 end

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

@@ -6,10 +6,12 @@ Authors: Paul Reichert
 module
 
 prelude
-public import Init.Control.MonadAttach
 import all Init.Control.MonadAttach
-public import Init.Control.Lawful.Lemmas
-public import Init.Control.Lawful.MonadLift.Lemmas
+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 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.Control.Basic
+public import Init.Notation
 
 public section
 

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

@@ -14,8 +14,12 @@ 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.Lemmas
-public import Init.Control.Lawful.Instances
+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 section
 
@@ -63,7 +67,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 [instMonad, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
+  simp only [bind, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
     map_bind]
 
 instance : LawfulMonadLift m (OptionT m) where
@@ -79,7 +83,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 [instMonad, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
+  simp only [bind, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
 
 instance : LawfulMonadLift m (ExceptT ε m) where
   monadLift_pure := lift_pure
@@ -89,8 +93,7 @@ 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 [instMonad, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont,
-      Except.instMonad, Except.bind]
+    simp only [bind, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont, 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_all
+    cases a; cases b; simp [monadLift] at h; simp [h]
   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.Control.Basic
+public import Init.Core
 
 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]
+@[expose, instance_reducible]
 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.Except
+public import Init.Control.MonadAttach
 
 public section
 

src/Init/Control/StateCps.lean

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

src/Init/Control/StateRef.lean

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

src/Init/Conv.lean

@@ -51,6 +51,21 @@ scoped syntax (name := withAnnotateState)
 /-- `skip` does nothing. -/
 syntax (name := skip) "skip" : conv
 
+/--
+`cbv` performs simplification that closely mimics call-by-value evaluation.
+It reduces the target term by unfolding definitions using their defining equations and
+applying matcher equations. The unfolding is propositional, so `cbv` also works
+with functions defined via well-founded recursion or partial fixpoints.
+
+The proofs produced by `cbv` only use the three standard axioms.
+In particular, they do not require trust in the correctness of the code
+generator.
+
+This tactic is experimental and its behavior is likely to change in upcoming
+releases of Lean.
+-/
+syntax (name := cbv) "cbv" : conv
+
 /--
 Traverses into the left subterm of a binary operator.
 

src/Init/Core.lean

@@ -9,6 +9,7 @@ module
 
 prelude
 public import Init.SizeOf
+public import Init.Tactics
 
 public section
 set_option linter.missingDocs true -- keep it documented
@@ -488,6 +489,8 @@ 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_≈_»]
@@ -932,6 +935,14 @@ 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₂
@@ -1478,6 +1489,29 @@ 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⟩
 
@@ -2279,6 +2313,13 @@ instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingl
 
 /-! # Squash -/
 
+theorem equivalence_true (α : Sort u) : Equivalence fun _ _ : α => True :=
+  ⟨fun _ => trivial, fun _ => trivial, fun _ _ => trivial⟩
+
+/-- Always-true relation as a `Setoid`. -/
+protected def Setoid.trivial (α : Sort u) : Setoid α :=
+  ⟨_, equivalence_true α⟩
+
 /--
 The quotient of `α` by the universal relation. The elements of `Squash α` are those of `α`, but all
 of them are equal and cannot be distinguished.
@@ -2292,8 +2333,11 @@ and its representation in compiled code is identical to that of `α`.
 
 Consequently, `Squash.lift` may extract an `α` value into any subsingleton type `β`, while
 `Nonempty.rec` can only do the same when `β` is a proposition.
+
+`Squash` is defined in terms of `Quotient`, so `Squash` can be used when a `Quotient` argument is
+expected.
 -/
-def Squash (α : Sort u) := Quot (fun (_ _ : α) => True)
+def Squash (α : Sort u) := Quotient (Setoid.trivial α)
 
 /--
 Places a value into its squash type, in which it cannot be distinguished from any other.
@@ -2329,8 +2373,10 @@ 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.
@@ -2350,11 +2396,13 @@ 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.
 
@@ -2362,12 +2410,14 @@ 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`.
 
@@ -2381,8 +2431,10 @@ 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`.
 
@@ -2392,6 +2444,7 @@ 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
 
 
@@ -2442,7 +2495,7 @@ class IdempotentOp (op : α → α → α) : Prop where
   idempotent : (x : α) → op x x = x
 
 /--
-`LeftIdentify op o` indicates `o` is a left identity of `op`.
+`LeftIdentity 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.
@@ -2450,7 +2503,7 @@ is used primarily for inferring the identity using class resolution.
 class LeftIdentity (op : α → β → β) (o : outParam α) : Prop
 
 /--
-`LawfulLeftIdentify op o` indicates `o` is a verified left identity of
+`LawfulLeftIdentity op o` indicates `o` is a verified left identity of
 `op`.
 -/
 class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extends LeftIdentity op o where
@@ -2458,7 +2511,7 @@ class LawfulLeftIdentity (op : α → β → β) (o : outParam α) : Prop extend
   left_id : ∀ a, op o a = a
 
 /--
-`RightIdentify op o` indicates `o` is a right identity `o` of `op`.
+`RightIdentity 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.
@@ -2466,7 +2519,7 @@ primarily for inferring the identity using class resolution.
 class RightIdentity (op : α → β → α) (o : outParam β) : Prop
 
 /--
-`LawfulRightIdentify op o` indicates `o` is a verified right identity of
+`LawfulRightIdentity op o` indicates `o` is a verified right identity of
 `op`.
 -/
 class LawfulRightIdentity (op : α → β → α) (o : outParam β) : Prop extends RightIdentity op o where
@@ -2540,3 +2593,11 @@ class Trichotomous (r : α → α → Prop) : Prop where
   trichotomous (a b : α) : ¬ r a b → ¬ r b a → a = b
 
 end Std
+
+@[simp] theorem flip_flip {α : Sort u} {β : Sort v} {φ : Sort w} {f : α → β → φ} :
+    flip (flip f) = f := by
+  apply funext
+  intro a
+  apply funext
+  intro b
+  rw [flip, flip]

src/Init/Data/AC.lean

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

src/Init/Data/Array.lean

@@ -30,3 +30,7 @@ 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,8 +6,10 @@ 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,6 +11,9 @@ 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
 
@@ -90,7 +93,7 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 
 @[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
   simp only [getElem?_def, getElem_toList]
-  simp only [Array.size]
+  simp only [Array.size]; rfl
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma
@@ -2122,7 +2125,7 @@ Examples:
 
 /-! ### Repr and ToString -/
 
-protected def Array.repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
+protected def repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
   let _ : Std.ToFormat α := ⟨repr⟩
   if xs.size == 0 then
     "#[]"

src/Init/Data/Array/BasicAux.lean

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

src/Init/Data/Array/BinSearch.lean

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

src/Init/Data/Array/Bootstrap.lean

@@ -7,8 +7,10 @@ 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
 
@@ -50,7 +52,9 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
   unfold foldrM.fold
   match i with
   | 0 => simp
-  | i+1 => rw [← List.take_concat_get h]; simp [← aux]
+  | i+1 =>
+    set_option backward.isDefEq.respectTransparency false in
+    rw [← List.take_concat_get h]; simp [← aux]
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
     xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by

src/Init/Data/Array/Count.lean

@@ -7,8 +7,14 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
-public import Init.Data.List.Nat.Count
+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 section
 
@@ -92,6 +98,18 @@ 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
@@ -99,11 +117,13 @@ theorem countP_le_size : countP p xs ≤ xs.size := by
 theorem countP_replicate {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0 := by
   simp [← List.toArray_replicate, List.countP_replicate]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem boole_getElem_le_countP {xs : Array α} {i : Nat} (h : i < xs.size) :
     (if p xs[i] then 1 else 0) ≤ xs.countP p := by
   rcases xs with ⟨xs⟩
   simp [List.boole_getElem_le_countP]
 
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem countP_set {xs : Array α} {i : Nat} {a : α} (h : i < xs.size) :
     (xs.set i a).countP p = xs.countP p - (if p xs[i] then 1 else 0) + (if p a then 1 else 0) := by

src/Init/Data/Array/DecidableEq.lean

@@ -7,8 +7,14 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.BEq
-public import Init.Data.List.Nat.BEq
+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 section
 
@@ -70,7 +76,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
     simpa [isEqv_iff_rel] using h'
 
 @[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
-  simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]
+  simp [isEqv_eq_decide, List.isEqv_eq_decide, Array.size]; rfl
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
   have ⟨h, h'⟩ := rel_of_isEqv h
@@ -81,6 +87,7 @@ private theorem isEqvAux_self (r : α → α → Bool) (hr : ∀ a, r a a) (xs :
   induction i with
   | zero => simp [Array.isEqvAux]
   | succ i ih =>
+    set_option backward.isDefEq.respectTransparency false in
     simp_all only [isEqvAux, Bool.and_self]
 
 theorem isEqv_self_beq [BEq α] [ReflBEq α] (xs : Array α) : Array.isEqv xs xs (· == ·) = true := by
@@ -147,7 +154,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
   simp [BEq.beq, isEqv_eq_decide]
 
 @[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
-  simp [beq_eq_decide, List.beq_eq_decide, Array.size]
+  simp [beq_eq_decide, List.beq_eq_decide, Array.size]; rfl
 
 end Array
 

src/Init/Data/Array/Erase.lean

@@ -8,6 +8,13 @@ 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
 
@@ -322,7 +329,7 @@ theorem eraseIdx_eq_take_drop_succ {xs : Array α} {i : Nat} (h) :
   rcases xs with ⟨xs⟩
   simp only [List.size_toArray] at h
   simp only [List.eraseIdx_toArray, List.eraseIdx_eq_take_drop_succ, take_eq_extract,
-    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, drop_eq_extract,
+    List.extract_toArray, List.extract_eq_take_drop, Nat.sub_zero, List.drop_zero, drop_eq_extract,
     List.size_toArray, List.append_toArray, mk.injEq, List.append_cancel_left_eq]
   rw [List.take_of_length_le]
   simp

src/Init/Data/Array/Extract.lean

@@ -6,7 +6,16 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Lemmas
+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 section
 

src/Init/Data/Array/FinRange.lean

@@ -6,7 +6,11 @@ Authors: François G. Dorais
 module
 
 prelude
-public import Init.Data.Array.OfFn
+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 section
 

src/Init/Data/Array/Find.lean

@@ -6,9 +6,22 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.List.Nat.Find
+import Init.Data.List.Nat.Sum
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Range
+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 section
 
@@ -70,6 +83,10 @@ theorem findSome?_eq_some_iff {f : α → Option β} {xs : Array α} {b : β} :
   · rintro ⟨xs, a, ys, h₀, h₁, h₂⟩
     exact ⟨xs.toList, a, ys.toList, by simpa using congrArg toList h₀, h₁, by simpa⟩
 
+theorem isSome_findSome? {xs : Array α} {f : α → Option β} :
+    (xs.findSome? f).isSome = xs.any (f · |>.isSome) := by
+  simp [← findSome?_toList, List.isSome_findSome?]
+
 @[simp, grind =] theorem findSome?_guard {xs : Array α} : findSome? (Option.guard p) xs = find? p xs := by
   cases xs; simp
 
@@ -114,7 +131,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,
-    Nat.sum_pos_iff_exists_pos, List.mem_map] at h
+    List.sum_pos_iff_exists_pos_nat, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
   exact ⟨xs, m, by simpa using h⟩
 
@@ -184,6 +201,10 @@ theorem find?_eq_some_iff_append {xs : Array α} :
     exact ⟨as.toList, ⟨l, by simpa using congrArg Array.toList h'⟩,
       by simpa using h⟩
 
+theorem isSome_find? {xs : Array α} {f : α → Bool} :
+    (xs.find? f).isSome = xs.any (f ·) := by
+  simp [← find?_toList, List.isSome_find?]
+
 theorem find?_push {xs : Array α} : (xs.push a).find? p = (xs.find? p).or (if p a then some a else none) := by
   cases xs; simp
 
@@ -412,6 +433,7 @@ theorem lt_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < x
   simp only [Nat.not_lt] at f
   exact absurd (@findIdx_getElem _ p xs (Nat.lt_of_le_of_lt f h)) (h2 (xs.findIdx p) f)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- `xs.findIdx p = i` iff `p xs[i]` and `¬ p xs [j]` for all `j < i`. -/
 theorem findIdx_eq {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) :
     xs.findIdx p = i ↔ p xs[i] ∧ ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false := by
@@ -600,12 +622,12 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp; rfl
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp
+  simp; rfl
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -674,6 +696,40 @@ 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?]
+  rfl
+
+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.
@@ -746,7 +802,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?]
 
-@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
+@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp; rfl
 
 @[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by

src/Init/Data/Array/GetLit.lean

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

src/Init/Data/Array/InsertIdx.lean

@@ -6,7 +6,11 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.Array.Lemmas
+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 section
 

src/Init/Data/Array/Int.lean

@@ -0,0 +1,77 @@
+/-
+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.List.Int.Sum
+public import Init.Data.Array.MinMax
+import Init.Data.Int.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
+
+@[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]
+
+theorem min_mul_length_le_sum_int {xs : Array Int} (h : xs ≠ #[]) :
+    xs.min h * xs.size ≤ xs.sum := by
+  rcases xs with ⟨l⟩
+  simpa [List.min_toArray, List.sum_toArray] using List.min_mul_length_le_sum_int (by simpa using h)
+
+theorem mul_length_le_sum_of_min?_eq_some_int {xs : Array Int} (h : xs.min? = some x) :
+    x * xs.size ≤ xs.sum := by
+  rcases xs with ⟨l⟩
+  simpa [List.min?_toArray, List.sum_toArray] using
+    List.mul_length_le_sum_of_min?_eq_some_int (by simpa using h)
+
+theorem min_le_sum_div_length_int {xs : Array Int} (h : xs ≠ #[]) :
+    xs.min h ≤ xs.sum / xs.size := by
+  rcases xs with ⟨l⟩
+  simpa [List.min_toArray, List.sum_toArray] using List.min_le_sum_div_length_int (by simpa using h)
+
+theorem le_sum_div_length_of_min?_eq_some_int {xs : Array Int} (h : xs.min? = some x) :
+    x ≤ xs.sum / xs.size := by
+  rcases xs with ⟨l⟩
+  simpa [List.min?_toArray, List.sum_toArray] using
+    List.le_sum_div_length_of_min?_eq_some_int (by simpa using h)
+
+theorem sum_le_max_mul_length_int {xs : Array Int} (h : xs ≠ #[]) :
+    xs.sum ≤ xs.max h * xs.size := by
+  rcases xs with ⟨l⟩
+  simpa [List.max_toArray, List.sum_toArray] using List.sum_le_max_mul_length_int (by simpa using h)
+
+theorem sum_le_max_mul_length_of_max?_eq_some_int {xs : Array Int} (h : xs.max? = some x) :
+    xs.sum ≤ x * xs.size := by
+  rcases xs with ⟨l⟩
+  simpa [List.max?_toArray, List.sum_toArray] using
+    List.sum_le_max_mul_length_of_max?_eq_some_int (by simpa using h)
+
+theorem sum_div_length_le_max_int {xs : Array Int} (h : xs ≠ #[]) :
+    xs.sum / xs.size ≤ xs.max h := by
+  rcases xs with ⟨l⟩
+  simpa [List.max_toArray, List.sum_toArray] using List.sum_div_length_le_max_int (by simpa using h)
+
+theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max? = some x) :
+    xs.sum / xs.size ≤ x := by
+  rcases xs with ⟨l⟩
+  simpa [List.max?_toArray, List.sum_toArray] using
+    List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -6,14 +6,28 @@ 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
 
@@ -156,6 +170,7 @@ theorem getD_getElem? {xs : Array α} {i : Nat} {d : α} :
 
 @[simp] theorem getElem?_empty {i : Nat} : (#[] : Array α)[i]? = none := rfl
 
+set_option backward.isDefEq.respectTransparency false in
 theorem getElem_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
     have : i < (xs.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
     (xs.push x)[i] = xs[i] := by
@@ -482,9 +497,18 @@ 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
-  cases xs; simp [List.forall_getElem]
+  exact forall_mem_iff_forall_getElem.symm
 
 /-! ### isEmpty -/
 
@@ -872,7 +896,7 @@ theorem all_push {xs : Array α} {a : α} {p : α → Bool} :
 @[simp] theorem getElem_set_ne {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
     (pj : j < xs.size) (h : i ≠ j) :
     (xs.set i v)[j]'(by simp [*]) = xs[j] := by
-  simp only [set, ← getElem_toList, List.getElem_set_ne h]
+  simp only [set, ← getElem_toList, List.getElem_set_ne h]; rfl
 
 @[simp] theorem getElem?_set_ne {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} {j : Nat}
     (ne : i ≠ j) : (xs.set i v)[j]? = xs[j]? := by
@@ -1969,6 +1993,14 @@ 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
@@ -2500,10 +2532,6 @@ 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 =]
@@ -2827,7 +2855,7 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} :
   · simp only [length_toList, size_extract, List.length_take, List.length_drop]
     omega
   · intro n h₁ h₂
-    simp
+    simp; rfl
 
 @[simp] theorem extract_size {xs : Array α} : xs.extract 0 xs.size = xs := by
   apply ext
@@ -3065,6 +3093,18 @@ 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
 
@@ -3935,6 +3975,7 @@ theorem all_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
   · simp only [Id.run_pure]
     rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_modify {xs : Array α} {f : α → α} {i : Nat} :
     (xs.modify i f).toList = xs.toList.modify i f := by
   apply List.ext_getElem
@@ -4107,7 +4148,7 @@ variable [LawfulBEq α]
     (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
   rcases xs with ⟨xs⟩
   simp only [List.replace_toArray, List.getElem?_toArray, List.getElem?_replace, take_eq_extract,
-    List.extract_toArray, List.extract_eq_drop_take, Nat.sub_zero, List.drop_zero, List.mem_toArray]
+    List.extract_toArray, List.extract_eq_take_drop, Nat.sub_zero, List.drop_zero, List.mem_toArray]
 
 theorem getElem?_replace_of_ne {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) :
     (xs.replace a b)[i]? = xs[i]? := by
@@ -4220,6 +4261,7 @@ private theorem getElem_ofFn_go {f : Fin n → α} {acc i k} (h : i ≤ n) (w₁
     · simp
       omega
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp] theorem getElem_ofFn {f : Fin n → α} {i : Nat} (h : i < (ofFn f).size) :
     (ofFn f)[i] = f ⟨i, size_ofFn (f := f) ▸ h⟩ := by
   unfold ofFn
@@ -4277,19 +4319,31 @@ 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_eq_sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
+theorem 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_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  cases as₁
-  cases as₂
-  simp [List.sum_append_nat]
+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 foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}
@@ -4439,11 +4493,13 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
   cases xs
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} :
     xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by simp)) := by
   cases xs
   simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem findFinIdx?_toList {p : α → Bool} {xs : Array α} :
     xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by simp)) := by
   cases xs
@@ -4568,6 +4624,7 @@ namespace List
     as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip := by
   ext1 <;> simp
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem firstM_toArray [Alternative m] {as : List α} {f : α → m β} :
     as.toArray.firstM f = as.firstM f := by
   unfold Array.firstM

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

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

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

@@ -8,9 +8,13 @@ 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
 
@@ -72,6 +72,7 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz
   simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
   split <;> simp_all
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} :
     (xs.mapFinIdx f).toList = xs.toList.mapFinIdx (fun i a h => f i a (by simpa)) := by
   apply List.ext_getElem <;> simp
@@ -105,6 +106,7 @@ theorem mapIdx_spec {f : Nat → α → β} {xs : Array α}
       xs[i]?.map (f i) := by
   simp [getElem?_def, size_mapIdx, getElem_mapIdx]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =] theorem toList_mapIdx {f : Nat → α → β} {xs : Array α} :
     (xs.mapIdx f).toList = xs.toList.mapIdx (fun i a => f i a) := by
   apply List.ext_getElem <;> simp

src/Init/Data/Array/Mem.lean

@@ -6,7 +6,11 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
-public import Init.Data.List.BasicAux
+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 section
 

src/Init/Data/Array/MinMax.lean

@@ -0,0 +1,403 @@
+/-
+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_take_drop]
+      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_take_drop]
+      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,6 +9,7 @@ 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

@@ -0,0 +1,84 @@
+/-
+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.MinMax
+import Init.Data.List.Nat.Sum
+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]
+
+theorem min_mul_length_le_sum_nat {xs : Array Nat} (h : xs ≠ #[]) :
+    xs.min h * xs.size ≤ xs.sum := by
+  rcases xs with ⟨l⟩
+  simpa [List.min_toArray, List.sum_toArray] using List.min_mul_length_le_sum_nat (by simpa using h)
+
+theorem mul_length_le_sum_of_min?_eq_some_nat {xs : Array Nat} (h : xs.min? = some x) :
+    x * xs.size ≤ xs.sum := by
+  rcases xs with ⟨l⟩
+  simpa [List.min?_toArray, List.sum_toArray] using
+    List.mul_length_le_sum_of_min?_eq_some_nat (by simpa using h)
+
+theorem min_le_sum_div_length_nat {xs : Array Nat} (h : xs ≠ #[]) :
+    xs.min h ≤ xs.sum / xs.size := by
+  rcases xs with ⟨l⟩
+  simpa [List.min_toArray, List.sum_toArray] using List.min_le_sum_div_length_nat (by simpa using h)
+
+theorem le_sum_div_length_of_min?_eq_some_nat {xs : Array Nat} (h : xs.min? = some x) :
+    x ≤ xs.sum / xs.size := by
+  rcases xs with ⟨l⟩
+  simpa [List.min?_toArray, List.sum_toArray] using
+    List.le_sum_div_length_of_min?_eq_some_nat (by simpa using h)
+
+theorem sum_le_max_mul_length_nat {xs : Array Nat} (h : xs ≠ #[]) :
+    xs.sum ≤ xs.max h * xs.size := by
+  rcases xs with ⟨l⟩
+  simpa [List.max_toArray, List.sum_toArray] using List.sum_le_max_mul_length_nat (by simpa using h)
+
+theorem sum_le_max_mul_length_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max? = some x) :
+    xs.sum ≤ x * xs.size := by
+  rcases xs with ⟨l⟩
+  simpa [List.max?_toArray, List.sum_toArray] using
+    List.sum_le_max_mul_length_of_max?_eq_some_nat (by simpa using h)
+
+theorem sum_div_length_le_max_nat {xs : Array Nat} (h : xs ≠ #[]) :
+    xs.sum / xs.size ≤ xs.max h := by
+  rcases xs with ⟨l⟩
+  simpa [List.max_toArray, List.sum_toArray] using List.sum_div_length_le_max_nat (by simpa using h)
+
+theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max? = some x) :
+    xs.sum / xs.size ≤ x := by
+  rcases xs with ⟨l⟩
+  simpa [List.max?_toArray, List.sum_toArray] using
+    List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h)
+
+end Array

src/Init/Data/Array/OfFn.lean

@@ -7,8 +7,13 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Monadic
-public import Init.Data.List.FinRange
+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 section
 
@@ -36,6 +41,7 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     intro h₃
     simp only [show i = n by omega]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem ofFn_add {n m} {f : Fin (n + m) → α} :
     ofFn f = (ofFn (fun i => f (i.castLE (Nat.le_add_right n m)))) ++ (ofFn (fun i => f (i.natAdd n))) := by
   induction m with
@@ -53,6 +59,11 @@ 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]
@@ -67,6 +78,12 @@ 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. -/
@@ -91,6 +108,7 @@ theorem ofFnM_succ {n} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} :
       pure (as.push a)) := by
   simp [ofFnM, Fin.foldlM_succ_last]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem ofFnM_add {n m} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} :
     ofFnM f = (do
       let as ← ofFnM fun i : Fin n => f (i.castLE (Nat.le_add_right n k))

src/Init/Data/Array/Perm.lean

@@ -6,9 +6,13 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Init.Data.List.Nat.Perm
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
+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 section
 
@@ -131,7 +135,7 @@ theorem extract {xs ys : Array α} (h : xs ~ ys) {lo hi : Nat}
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp_all only [perm_iff_toList_perm, List.getElem?_toArray, List.extract_toArray,
-    List.extract_eq_drop_take]
+    List.extract_eq_take_drop]
   apply List.Perm.take_of_getElem? (w := fun i h => by simpa using whi (lo + i) (by omega))
   apply List.Perm.drop_of_getElem? (w := wlo)
   exact h

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

@@ -8,6 +8,7 @@ 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,8 +8,16 @@ module
 prelude
 import all Init.Data.Array.Basic
 import all Init.Data.Array.OfFn
-public import Init.Data.Array.MapIdx
-public import Init.Data.Array.Zip
+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 section
 

src/Init/Data/Array/Subarray.lean

@@ -7,7 +7,6 @@ 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
-public import Init.Omega
+import Init.Omega
 
 public section
 

src/Init/Data/Array/TakeDrop.lean

@@ -7,7 +7,11 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.Lemmas
+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 section
 

src/Init/Data/Array/Zip.lean

@@ -7,7 +7,14 @@ module
 
 prelude
 import all Init.Data.Array.Basic
-public import Init.Data.Array.TakeDrop
+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 section
 

src/Init/Data/BEq.lean

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

src/Init/Data/BitVec/Basic.lean

@@ -6,8 +6,16 @@ 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
 
@@ -202,7 +210,7 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   String.Internal.append t s
 
 /-- `BitVec` representation. -/
-protected def BitVec.repr (a : BitVec n) : Std.Format :=
+protected def repr (a : BitVec n) : Std.Format :=
   "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
 
 instance : Repr (BitVec n) where
@@ -261,7 +269,7 @@ Usually accessed via the `/` operator.
 -/
 @[expose]
 def udiv (x y : BitVec n) : BitVec n :=
-  (x.toNat / y.toNat)#'(Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
+  (x.toNat / y.toNat)#'(by exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) x.isLt)
 instance : Div (BitVec n) := ⟨.udiv⟩
 
 /--
@@ -271,7 +279,7 @@ SMT-LIB name: `bvurem`.
 -/
 @[expose]
 def umod (x y : BitVec n) : BitVec n :=
-  (x.toNat % y.toNat)#'(Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
+  (x.toNat % y.toNat)#'(by exact Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt)
 instance : Mod (BitVec n) := ⟨.umod⟩
 
 /--
@@ -515,7 +523,7 @@ Example:
 -/
 @[expose]
 protected def and (x y : BitVec n) : BitVec n :=
-  (x.toNat &&& y.toNat)#'(Nat.and_lt_two_pow x.toNat y.isLt)
+  (x.toNat &&& y.toNat)#'(by exact Nat.and_lt_two_pow x.toNat y.isLt)
 instance : AndOp (BitVec w) := ⟨.and⟩
 
 /--
@@ -528,7 +536,7 @@ Example:
 -/
 @[expose]
 protected def or (x y : BitVec n) : BitVec n :=
-  (x.toNat ||| y.toNat)#'(Nat.or_lt_two_pow x.isLt y.isLt)
+  (x.toNat ||| y.toNat)#'(by exact Nat.or_lt_two_pow x.isLt y.isLt)
 instance : OrOp (BitVec w) := ⟨.or⟩
 
 /--
@@ -541,7 +549,7 @@ Example:
 -/
 @[expose]
 protected def xor (x y : BitVec n) : BitVec n :=
-  (x.toNat ^^^ y.toNat)#'(Nat.xor_lt_two_pow x.isLt y.isLt)
+  (x.toNat ^^^ y.toNat)#'(by exact 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.Data.Fin.Basic
+public import Init.Grind.Tactics
 
 public section
 

src/Init/Data/BitVec/Bitblast.lean

@@ -7,12 +7,20 @@ 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
-import Init.BinderPredicates
+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
 
 @[expose] public section
 
@@ -2184,6 +2192,7 @@ def uppcRec {w} (x : BitVec w) (s : Nat) (hs : s < w) : Bool :=
   | 0 => x.msb
   | i + 1 =>  x[w - 1 - i] || uppcRec x i (by omega)
 
+set_option backward.isDefEq.respectTransparency false in
 /-- The unsigned parallel prefix of `x` at `s` is `true` if and only if x interpreted
   as a natural number is greater or equal than `2 ^ (w - 1 - (s - 1))`. -/
 @[simp]
@@ -2233,7 +2242,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 => by omega
+  | 0 => False.elim (by omega)
   | s' + 1 =>
     match hs' : s' with
     | 0 => aandRec x y 1 (by omega)

src/Init/Data/BitVec/Bootstrap.lean

@@ -8,8 +8,10 @@ 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,8 +7,11 @@ 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,8 +7,10 @@ module
 
 prelude
 import all Init.Data.BitVec.Basic
-public import Init.Data.BitVec.Lemmas
-public import Init.Data.Fin.Iterate
+public import Init.Data.BitVec.Basic
+public import Init.Ext
+import Init.Data.BitVec.Lemmas
+import Init.Data.Fin.Iterate
 
 public section
 

src/Init/Data/BitVec/Lemmas.lean

@@ -9,11 +9,20 @@ 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
 
@@ -1189,7 +1198,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
       (decide (0 < len) &&
       (decide (start + len ≤ w) &&
       x.getMsbD (w - (start + len)))) := by
-  simp [BitVec.msb, getMsbD_extractLsb']
+  simp [BitVec.msb, getMsbD_extractLsb']; rfl
 
 @[simp, grind =] theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
     (extractLsb hi lo x)[i] = getLsbD x (lo+i) := by
@@ -1225,7 +1234,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
 
 @[simp, grind =] theorem msb_extractLsb {hi lo : Nat} {x : BitVec w} :
     (extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo)) := by
-  simp [BitVec.msb]
+  simp [BitVec.msb]; rfl
 
 theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
     x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega) := by
@@ -2572,6 +2581,19 @@ theorem msb_signExtend {x : BitVec w} :
   · simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega]
   · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
 
+/-- Sign-extending to `w + n` bits, extracting bits `[w - 1 + n..n]`, and setting width
+back to `w` is equivalent to arithmetic right shift by `n`, since both sides discard the `n`
+least significant bits and replicate the sign bit into the upper bits. -/
+@[simp]
+theorem signExtend_extractLsb_setWidth {x : BitVec w} {n : Nat} :
+    ((x.signExtend (w + n)).extractLsb (w - 1 + n) n).setWidth w = x.sshiftRight n := by
+  ext i hi
+  simp only [getElem_sshiftRight, getElem_setWidth, getLsbD_extract,
+    Nat.add_sub_cancel, show i ≤ w - 1 by omega, decide_true, getLsbD_signExtend,
+    Bool.true_and]
+  by_cases hni : n + i < w
+  <;> (simp [hni]; omega)
+
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) :
   x.signExtend v = x.setWidth v := by
@@ -2762,8 +2784,9 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 @[simp] theorem append_zero_width (x : BitVec w) (y : BitVec 0) : x ++ y = x := by
   ext i ih
   rw [getElem_append] -- Why does this not work with `simp [getElem_append]`?
-  simp
+  simp; rfl
 
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n == 0 then y.toInt else (2 ^ m) * x.toInt + y.toNat := by
@@ -5269,6 +5292,7 @@ theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
 theorem replicate_zero {x : BitVec w} : x.replicate 0 = 0#0 := by
   simp [replicate]
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp, grind =]
 theorem replicate_one {w : Nat} {x : BitVec w} :
     (x.replicate 1) = x.cast (by rw [Nat.mul_one]) := by
@@ -5320,6 +5344,7 @@ theorem append_assoc {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w
 theorem append_assoc' {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} :
     (x₁ ++ (x₂ ++ x₃)) = ((x₁ ++ x₂) ++ x₃).cast (by omega) := by simp [append_assoc]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem replicate_append_self {x : BitVec w} :
     x ++ x.replicate n = (x.replicate n ++ x).cast (by omega) := by
   induction n with

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] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+@[expose, instance_reducible] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/

src/Init/Data/ByteArray/Basic.lean

@@ -6,9 +6,12 @@ Author: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.UInt.Basic
 import all Init.Data.UInt.BasicAux
-public import Init.Data.Array.Extract
+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
 
 set_option doc.verso true
 

src/Init/Data/ByteArray/Extra.lean

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

src/Init/Data/ByteArray/Lemmas.lean

@@ -7,6 +7,11 @@ 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
 
@@ -106,13 +111,13 @@ theorem getElem_eq_getElem_data {a : ByteArray} {i : Nat} {h : i < a.size} :
 theorem getElem_append_left {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
     (hlt : i < a.size) : (a ++ b)[i] = a[i] := by
   simp only [getElem_eq_getElem_data, data_append]
-  rw [Array.getElem_append_left (by simpa)]
+  rw [Array.getElem_append_left (by simpa)]; rfl
 
 theorem getElem_append_right {i : Nat} {a b : ByteArray} {h : i < (a ++ b).size}
     (hle : a.size ≤ i) : (a ++ b)[i] = b[i - a.size]'(by simp_all; omega) := by
   simp only [getElem_eq_getElem_data, data_append]
   rw [Array.getElem_append_right (by simpa)]
-  simp
+  simp; rfl
 
 @[simp]
 theorem _root_.List.getElem_toByteArray {l : List UInt8} {i : Nat} {h : i < l.toByteArray.size} :
@@ -218,7 +223,7 @@ theorem getElem_extract_aux {xs : ByteArray} {start stop : Nat} (h : i < (xs.ext
 
 theorem getElem_extract {i : Nat} {b : ByteArray} {start stop : Nat}
     (h) : (b.extract start stop)[i]'h = b[start + i]'(getElem_extract_aux h) := by
-  simp [getElem_eq_getElem_data]
+  simp [getElem_eq_getElem_data]; rfl
 
 theorem extract_eq_extract_left {a : ByteArray} {i i' j : Nat} :
     a.extract i j = a.extract i' j ↔ min j a.size - i = min j a.size - i' := by
@@ -231,25 +236,25 @@ theorem extract_add_one {a : ByteArray} {i : Nat} (ha : i + 1 ≤ a.size) :
     omega
   · rename_i j hj hj'
     obtain rfl : j = 0 := by simpa using hj'
-    simp [ByteArray.getElem_eq_getElem_data]
+    simp [ByteArray.getElem_eq_getElem_data]; rfl
 
 theorem extract_add_two {a : ByteArray} {i : Nat} (ha : i + 2 ≤ a.size) :
     a.extract i (i + 2) = [a[i], a[i + 1]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_one (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem extract_add_three {a : ByteArray} {i : Nat} (ha : i + 3 ≤ a.size) :
     a.extract i (i + 3) = [a[i], a[i + 1], a[i + 2]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_two (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem extract_add_four {a : ByteArray} {i : Nat} (ha : i + 4 ≤ a.size) :
     a.extract i (i + 4) = [a[i], a[i + 1], a[i + 2], a[i + 3]].toByteArray := by
   rw [extract_eq_extract_append_extract (i + 1) (by simp) (by omega),
     extract_add_one (by omega), extract_add_three (by omega)]
-  simp [← List.toByteArray_append]
+  simp [← List.toByteArray_append]; rfl
 
 theorem append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c) := by
   ext1
@@ -286,4 +291,41 @@ 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,6 +7,7 @@ module
 
 prelude
 public import Init.Data.UInt.BasicAux
+import Init.Data.Nat.Div.Basic
 
 @[expose] public section
 
@@ -162,16 +163,19 @@ The lowercase ASCII letters are the following: `abcdefghijklmnopqrstuvwxyz`.
 -/
 @[inline]
 def toUpper (c : Char) : Char :=
-  if h : c.val ≥ 'a'.val ∧ c.val ≤ 'z'.val then
+  if h : 'a'.val ≤ c.val ∧ c.val ≤ 'z'.val then
     ⟨c.val + ('A'.val - 'a'.val), ?_⟩
   else
     c
 where finally
-  have h₁ : 2^32 ≤ c.val.toNat + ('A'.val - 'a'.val).toNat :=
-    @Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by decide)
-  have h₂ : c.val.toBitVec.toNat + ('A'.val - 'a'.val).toNat < 2^32 + 0xd800 :=
-    Nat.add_lt_add_right (Nat.lt_of_le_of_lt h.2 (by decide)) _
-  have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := rfl
+  -- This expression is a ground non-value; generalize for better
+  -- control on where it is evaluated.
+  generalize hx : 'A'.val - 'a'.val = x
+  have h₁ : 2^32 ≤ c.val.toNat + x.toNat :=
+    @Nat.add_le_add 'a'.val.toNat _ (2^32 - 'a'.val.toNat) _ h.1 (by rw [← hx]; decide)
+  have h₂ : c.val.toBitVec.toNat + x.toNat < 2^32 + 0xd800 :=
+    Nat.add_lt_of_lt_sub (Nat.lt_of_le_of_lt h.2 (by rw [← hx]; decide))
+  have add_eq {x y : UInt32} : (x + y).toNat = (x.toNat + y.toNat) % 2^32 := id rfl
   replace h₂ := Nat.sub_lt_left_of_lt_add h₁ h₂
   exact .inl <| lt_of_eq_of_lt (add_eq.trans (Nat.mod_eq_sub_mod h₁) |>.trans
     (Nat.mod_eq_of_lt (Nat.lt_trans h₂ (by decide)))) h₂

src/Init/Data/Char/Lemmas.lean

@@ -7,7 +7,9 @@ module
 
 prelude
 import all Init.Data.Char.Basic
-public import Init.Data.UInt.Lemmas
+public import Init.Data.Char.Basic
+public import Init.Ext
+import Init.Data.UInt.Lemmas
 
 public section
 
@@ -48,6 +50,7 @@ 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₁)
 
@@ -80,6 +83,7 @@ def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
 @[simp]
 theorem toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8 := rfl
 
+@[simp]
 theorem toString_eq_singleton {c : Char} : c.toString = String.singleton c := rfl
 
 end Char

src/Init/Data/Char/Order.lean

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