fix: incorrect borrow annotation on demangleBtLinCStr leading to segfault on panic (#12939)

This PR fixes `Id.run_seqLeft` and `Id.run_seqRight` to apply when the
two monad results are different.

.claude/CLAUDE.md

@@ -20,9 +20,24 @@ CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
 
 # Single test from tests/foo/bar/ (quick check during development)
-cd tests/foo/bar && ./run_test example_test.lean
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release -j "$(nproc)" test ARGS=-R testname'
 ```
 
+## Testing stage 2
+
+When requested to test stage 2, build it as follows:
+```
+make -C build/release stage2 -j$(nproc)
+```
+Stage 2 is *not* automatically invalidated by changes to `src/` which allows for faster iteration
+when fixing a specific file in the stage 2 build but for invalidating any files that already passed
+the stage 2 build as well as for final validation,
+```
+make -C build/release/stage2 clean-stdlib
+```
+must be run manually before building.
+
 ## New features
 
 When asked to implement new features:

.github/workflows/ci.yml

@@ -166,7 +166,7 @@ jobs:
       # 0: PRs without special label
       # 1: PRs with `merge-ci` label, merge queue checks, master commits
       # 2: nightlies
-      # 3: PRs with `release-ci` label, full releases
+      # 3: PRs with `release-ci` or `lake-ci` label, full releases
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -175,6 +175,7 @@ jobs:
         run: |
           check_level=0
           fast=false
+          lake_ci=false
 
           if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=3
@@ -189,13 +190,19 @@ jobs:
             elif echo "$labels" | grep -q "merge-ci"; then
               check_level=1
             fi
+            if echo "$labels" | grep -q "lake-ci"; then
+              lake_ci=true
+            fi
             if echo "$labels" | grep -q "fast-ci"; then
               fast=true
             fi
           fi
 
-          echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
-          echo "fast=$fast" >> "$GITHUB_OUTPUT"
+          {
+            echo "check-level=$check_level"
+            echo "fast=$fast"
+            echo "lake-ci=$lake_ci"
+          } >> "$GITHUB_OUTPUT"
         env:
           GH_TOKEN: ${{ github.token }}
 
@@ -206,6 +213,7 @@ jobs:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
             const fast = ${{ steps.set-level.outputs.fast }};
+            const lakeCi = "${{ steps.set-level.outputs.lake-ci }}" == "true";
             console.log(`level: ${level}, fast: ${fast}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
@@ -379,6 +387,11 @@ jobs:
                 job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DUSE_LAKE=OFF";
               }
             }
+            if (lakeCi) {
+              for (const job of matrix) {
+                job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DLAKE_CI=ON";
+              }
+            }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
             matrix = matrix.filter((job) => job["enabled"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));

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

@@ -1,5 +1,5 @@
 # This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
-# `release-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
+# `release-ci`, `lake-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
 # If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
 # from that set are removed automatically at the same time.
 # Similarly, if any `changelog-XXX` label is added, other `changelog-YYY` labels are removed.
@@ -12,7 +12,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'changelog-'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'lake-ci') || contains(github.event.comment.body, 'changelog-'))
     runs-on: ubuntu-latest
 
     steps:
@@ -28,6 +28,7 @@ jobs:
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
           const releaseCI = commentLines.includes('release-ci');
+          const lakeCI = commentLines.includes('lake-ci');
           const changelogMatch = commentLines.find(line => line.startsWith('changelog-'));
 
           if (awaitingReview || awaitingAuthor || wip) {
@@ -49,6 +50,9 @@ jobs:
           if (releaseCI) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
           }
+          if (lakeCI) {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['lake-ci'] });
+          }
 
           if (changelogMatch) {
             const changelogLabel = changelogMatch.trim();

.github/workflows/restart-on-label.yml

@@ -7,7 +7,7 @@ on:
 jobs:
   restart-on-label:
     runs-on: ubuntu-latest
-    if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci')
+    if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci') || contains(github.event.label.name, 'lake-ci')
     steps:
     - run: |
         # Finding latest CI workflow run on current pull request

CMakeLists.txt

@@ -41,7 +41,7 @@ if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
   set(STAGE0_CMAKE_EXECUTABLE_SUFFIX "${CMAKE_EXECUTABLE_SUFFIX}")
 endif()
 
-# Don't do anything with cadical on wasm
+# Don't do anything with cadical/leantar on wasm
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   find_program(CADICAL cadical)
   if(NOT CADICAL)
@@ -77,7 +77,44 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
     set(CADICAL ${CMAKE_BINARY_DIR}/cadical/cadical${CMAKE_EXECUTABLE_SUFFIX})
     list(APPEND EXTRA_DEPENDS cadical)
   endif()
-  list(APPEND CL_ARGS -DCADICAL=${CADICAL})
+  find_program(LEANTAR leantar)
+  if(NOT LEANTAR)
+    set(LEANTAR_VERSION v0.1.19)
+    if(CMAKE_SYSTEM_NAME MATCHES "Windows")
+      set(LEANTAR_ARCHIVE_SUFFIX .zip)
+      set(LEANTAR_TARGET x86_64-pc-windows-msvc)
+    else()
+      set(LEANTAR_ARCHIVE_SUFFIX .tar.gz)
+      if(CMAKE_SYSTEM_PROCESSOR MATCHES "arm64")
+        set(LEANTAR_TARGET_ARCH aarch64)
+      else()
+        set(LEANTAR_TARGET_ARCH x86_64)
+      endif()
+      if(CMAKE_SYSTEM_NAME MATCHES "Darwin")
+        set(LEANTAR_TARGET_OS apple-darwin)
+      else()
+        set(LEANTAR_TARGET_OS unknown-linux-musl)
+      endif()
+      set(LEANTAR_TARGET ${LEANTAR_TARGET_ARCH}-${LEANTAR_TARGET_OS})
+    endif()
+    set(
+      LEANTAR
+      ${CMAKE_BINARY_DIR}/leantar/leantar-${LEANTAR_VERSION}-${LEANTAR_TARGET}/leantar${CMAKE_EXECUTABLE_SUFFIX}
+    )
+    if(NOT EXISTS "${LEANTAR}")
+      file(
+        DOWNLOAD
+          https://github.com/digama0/leangz/releases/download/${LEANTAR_VERSION}/leantar-${LEANTAR_VERSION}-${LEANTAR_TARGET}${LEANTAR_ARCHIVE_SUFFIX}
+        ${CMAKE_BINARY_DIR}/leantar${LEANTAR_ARCHIVE_SUFFIX}
+      )
+      file(
+        ARCHIVE_EXTRACT
+        INPUT ${CMAKE_BINARY_DIR}/leantar${LEANTAR_ARCHIVE_SUFFIX}
+        DESTINATION ${CMAKE_BINARY_DIR}/leantar
+      )
+    endif()
+  endif()
+  list(APPEND CL_ARGS -DCADICAL=${CADICAL} -DLEANTAR=${LEANTAR})
 endif()
 
 if(USE_MIMALLOC)

CONTRIBUTING.md

@@ -7,7 +7,7 @@ Helpful links
 -------
 
 * [Development Setup](./doc/dev/index.md)
-* [Testing](./doc/dev/testing.md)
+* [Testing](./tests/README.md)
 * [Commit convention](./doc/dev/commit_convention.md)
 
 Before You Submit a Pull Request (PR):

LICENSES

@@ -1370,4 +1370,208 @@ FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-SOFTWARE.
+SOFTWARE.
+==============================================================================
+leantar is by Mario Carneiro and distributed under the Apache 2.0 License:
+==============================================================================
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.

doc/dev/index.md

@@ -1,7 +1,9 @@
 # Development Workflow
 
 If you want to make changes to Lean itself, start by [building Lean](../make/index.md) from a clean checkout to make sure that everything is set up correctly.
-After that, read on below to find out how to set up your editor for changing the Lean source code, followed by further sections of the development manual where applicable such as on the [test suite](testing.md) and [commit convention](commit_convention.md).
+After that, read on below to find out how to set up your editor for changing the Lean source code,
+followed by further sections of the development manual where applicable
+such as on the [test suite](../../tests/README.md) and [commit convention](commit_convention.md).
 
 If you are planning to make any changes that may affect the compilation of Lean itself, e.g. changes to the parser, elaborator, or compiler, you should first read about the [bootstrapping pipeline](bootstrap.md).
 You should not edit the `stage0` directory except using the commands described in that section when necessary.

doc/dev/testing.md

@@ -1,142 +0,0 @@
-# Test Suite
-
-**Warning:** This document is partially outdated.
-It describes the old test suite, which is currently in the process of being replaced.
-The new test suite's documentation can be found at [`tests/README.md`](../../tests/README.md).
-
-After [building Lean](../make/index.md) you can run all the tests using
-```
-cd build/release
-make test ARGS=-j4
-```
-Change the 4 to the maximum number of parallel tests you want to
-allow. The best choice is the number of CPU cores on your machine as
-the tests are mostly CPU bound.  You can find the number of processors
-on linux using `nproc` and on Windows it is the `NUMBER_OF_PROCESSORS`
-environment variable.
-
-You can run tests after [building a specific stage](bootstrap.md) by
-adding the `-C stageN` argument. The default when run as above is stage 1.  The
-Lean tests will automatically use that stage's corresponding Lean
-executables
-
-Running `make test` will not pick up new test files; run
-```bash
-cmake build/release/stage1
-```
-to update the list of tests.
-
-You can also use `ctest` directly if you are in the right folder.  So
-to run stage1 tests with a 300 second timeout run this:
-
-```bash
-cd build/release/stage1
-ctest -j 4 --output-on-failure --timeout 300
-```
-Useful `ctest` flags are `-R <name of test>` to run a single test, and
-`--rerun-failed` to run all tests that failed during the last run.
-You can also pass `ctest` flags via `make test ARGS="--rerun-failed"`.
-
-To get verbose output from ctest pass the `--verbose` command line
-option. Test output is normally suppressed and only summary
-information is displayed. This option will show all test output.
-
-## Test Suite Organization
-
-All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
-
-- [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/): contains tests that come equipped with a
-  .lean.expected.out file. The driver script [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/test_single.sh) runs
-  each test and checks the actual output (*.produced.out) with the
-  checked in expected output.
-
-- [`tests/lean/run`](https://github.com/leanprover/lean4/tree/master/tests/lean/run/): contains tests that are run through the lean
-  command line one file at a time. These tests only look for error
-  codes and do not check the expected output even though output is
-  produced, it is ignored.
-
-  **Note:** Tests in this directory run with `-Dlinter.all=false` to reduce noise.
-  If your test needs to verify linter behavior (e.g., deprecation warnings),
-  explicitly enable the relevant linter with `set_option linter.<name> true`.
-
-- [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a
-  given position in the input file. Each .lean file contains comments
-  that indicate how to simulate a client request at that position.
-  using a `--^` point to the line position. Example:
-    ```lean,ignore
-    open Foo in
-    theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
-    Bla.
-      --^ completion
-    ```
-    In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
-    auto-completion request at `Bla.`. The expected output is stored in
-    a .lean.expected.out in the json format that is part of the
-    [Language Server
-    Protocol](https://microsoft.github.io/language-server-protocol/).
-
-    This can also be used to test the following additional requests:
-    ```
-    --^ textDocument/hover
-    --^ textDocument/typeDefinition
-    --^ textDocument/definition
-    --^ $/lean/plainGoal
-    --^ $/lean/plainTermGoal
-    --^ insert: ...
-    --^ collectDiagnostics
-    ```
-
-- [`tests/lean/server`](https://github.com/leanprover/lean4/tree/master/tests/lean/server/): Tests more of the Lean `--server` protocol.
-  There are just a few of them, and it uses .log files containing
-  JSON.
-
-- [`tests/compiler`](https://github.com/leanprover/lean4/tree/master/tests/compiler/): contains tests that will run the Lean compiler and
-  build an executable that is executed and the output is compared to
-  the .lean.expected.out file. This test also contains a subfolder
-  [`foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) which shows how to extend Lean using C++.
-
-- [`tests/lean/trust0`](https://github.com/leanprover/lean4/tree/master/tests/lean/trust0): tests that run Lean in a mode that Lean doesn't
-  even trust the .olean files (i.e., trust 0).
-
-- [`tests/bench`](https://github.com/leanprover/lean4/tree/master/tests/bench/): contains performance tests.
-
-- [`tests/plugin`](https://github.com/leanprover/lean4/tree/master/tests/plugin/): tests that compiled Lean code can be loaded into
-  `lean` via the `--plugin` command line option.
-
-## Writing Good Tests
-
-Every test file should contain:
-* an initial `/-! -/` module docstring summarizing the test's purpose
-* a module docstring for each test section that describes what is tested
-  and, if not 100% clear, why that is the desirable behavior
-
-At the time of writing, most tests do not follow these new guidelines yet.
-For an example of a conforming test, see [`tests/lean/1971.lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/1971.lean).
-
-## Fixing Tests
-
-When the Lean source code or the standard library are modified, some of the
-tests break because the produced output is slightly different, and we have
-to reflect the changes in the `.lean.expected.out` files.
-We should not blindly copy the new produced output since we may accidentally
-miss a bug introduced by recent changes.
-The test suite contains commands that allow us to see what changed in a convenient way.
-First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
-
-```
-sudo apt-get install meld
-```
-
-Now, suppose `bad_class.lean` test is broken. We can see the problem by going to [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean) directory and
-executing
-
-```
-./test_single.sh -i bad_class.lean
-```
-
-When the `-i` option is provided, `meld` is automatically invoked
-whenever there is discrepancy between the produced and expected
-outputs. `meld` can also be used to repair the problems.
-
-In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
-To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.

doc/examples/compiler/run_test

@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-source ../../../tests/env_test.sh
-source "$TEST_DIR/util.sh"
-
-leanmake --always-make bin
-
-exec_capture test.lean \
-  ./build/bin/test hello world
-
-check_exit test.lean
-check_out test.lean

doc/examples/compiler/run_test.sh

@@ -0,0 +1,4 @@
+leanmake --always-make bin
+
+capture ./build/bin/test hello world
+check_out_contains "[hello, world]"

doc/examples/run_test

@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-source ../../tests/env_test.sh
-source "$TEST_DIR/util.sh"
-
-exec_capture "$1" \
-  lean -Dlinter.all=false "$1"
-
-check_exit "$1"
-check_out "$1"

doc/examples/run_test.sh

@@ -0,0 +1,4 @@
+capture_only "$1" \
+  lean -Dlinter.all=false "$1"
+check_exit_is_success
+check_out_file

script/release_steps.py

@@ -492,8 +492,9 @@ def execute_release_steps(repo, version, config):
             'ROOT_REV=$(jq -r \'.packages[] | select(.name == "subverso") | .rev\' lake-manifest.json); '
             'SUBVERSO_URL=$(jq -r \'.packages[] | select(.name == "subverso") | .url\' lake-manifest.json); '
             'DEMOD_REV=$(git ls-remote "$SUBVERSO_URL" "refs/tags/no-modules/$ROOT_REV" | awk \'{print $1}\'); '
-            'find test-projects -name lake-manifest.json -print0 | '
-            'xargs -0 -I{} sh -c \'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "{}" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "{}"\''
+            'find test-projects -name lake-manifest.json -print0 | while IFS= read -r -d \'\' f; do '
+            'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "$f" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "$f"; '
+            'done'
         )
         run_command(sync_script, cwd=repo_path)
         print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))

src/CMakeLists.txt

@@ -87,6 +87,8 @@ option(USE_GITHASH "GIT_HASH" ON)
 option(INSTALL_LICENSE "INSTALL_LICENSE" ON)
 # When ON we install a copy of cadical
 option(INSTALL_CADICAL "Install a copy of cadical" ON)
+# When ON we install a copy of leantar
+option(INSTALL_LEANTAR "Install a copy of leantar" ON)
 
 # FLAGS for disabling optimizations and debugging
 option(FREE_VAR_RANGE_OPT "FREE_VAR_RANGE_OPT" ON)
@@ -757,6 +759,14 @@ if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
   add_dependencies(leancpp copy-cadical)
 endif()
 
+if(STAGE GREATER 0 AND LEANTAR AND INSTALL_LEANTAR)
+  add_custom_target(
+    copy-leantar
+    COMMAND cmake -E copy_if_different "${LEANTAR}" "${CMAKE_BINARY_DIR}/bin/leantar${CMAKE_EXECUTABLE_SUFFIX}"
+  )
+  add_dependencies(leancpp copy-leantar)
+endif()
+
 # MSYS2 bash usually handles Windows paths relatively well, but not when putting them in the PATH
 string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")
 
@@ -913,6 +923,10 @@ if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
   install(PROGRAMS "${CADICAL}" DESTINATION bin)
 endif()
 
+if(STAGE GREATER 0 AND LEANTAR AND INSTALL_LEANTAR)
+  install(PROGRAMS "${LEANTAR}" DESTINATION bin)
+endif()
+
 add_custom_target(
   clean-stdlib
   COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" || true

src/Init.lean

@@ -30,6 +30,7 @@ public import Init.Hints
 public import Init.Conv
 public import Init.Guard
 public import Init.Simproc
+public import Init.CbvSimproc
 public import Init.SizeOfLemmas
 public import Init.BinderPredicates
 public import Init.Ext

src/Init/CbvSimproc.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public meta import Init.Data.ToString.Name  -- shake: keep (transitive public meta dep, fix)
+public import Init.Tactics
+import Init.Meta.Defs
+
+public section
+
+namespace Lean.Parser
+
+syntax cbvSimprocEval := "cbv_eval"
+
+/--
+A user-defined simplification procedure used by the `cbv` tactic.
+The body must have type `Lean.Meta.Sym.Simp.Simproc` (`Expr → SimpM Result`).
+Procedures are indexed by a discrimination tree pattern and fire at one of three phases:
+`↓` (pre), `cbv_eval` (eval), or `↑` (post, default).
+-/
+syntax (docComment)? attrKind "cbv_simproc " (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? ident " (" term ")" " := " term : command
+
+/--
+A `cbv_simproc` declaration without automatically adding it to the cbv simproc set.
+To activate, use `attribute [cbv_simproc]`.
+-/
+syntax (docComment)? "cbv_simproc_decl " ident " (" term ")" " := " term : command
+
+syntax (docComment)? attrKind "builtin_cbv_simproc " (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? ident " (" term ")" " := " term : command
+
+syntax (docComment)? "builtin_cbv_simproc_decl " ident " (" term ")" " := " term : command
+
+syntax (name := cbvSimprocPattern) "cbv_simproc_pattern% " term " => " ident : command
+
+syntax (name := cbvSimprocPatternBuiltin) "builtin_cbv_simproc_pattern% " term " => " ident : command
+
+namespace Attr
+
+syntax (name := cbvSimprocAttr) "cbv_simproc" (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? : attr
+
+syntax (name := cbvSimprocBuiltinAttr) "builtin_cbv_simproc" (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? : attr
+
+end Attr
+
+macro_rules
+  | `($[$doc?:docComment]? cbv_simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Sym.Simp.Simproc
+    `($[$doc?:docComment]? meta def $n:ident : $(mkIdent simprocType) := $body
+      cbv_simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? builtin_cbv_simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Sym.Simp.Simproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      builtin_cbv_simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind cbv_simproc $[$phase?]? $n:ident ($pattern:term) := $body) => do
+    `($[$doc?:docComment]? cbv_simproc_decl $n ($pattern) := $body
+      attribute [$kind cbv_simproc $[$phase?]?] $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind builtin_cbv_simproc $[$phase?]? $n:ident ($pattern:term) := $body) => do
+    `($[$doc?:docComment]? builtin_cbv_simproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_cbv_simproc $[$phase?]?] $n)
+
+end Lean.Parser

src/Init/Control.lean

@@ -18,3 +18,4 @@ public import Init.Control.StateCps
 public import Init.Control.ExceptCps
 public import Init.Control.MonadAttach
 public import Init.Control.EState
+public import Init.Control.Do

src/Init/Control/Lawful/Basic.lean

@@ -254,8 +254,8 @@ instance : LawfulMonad Id := by
 @[simp, grind =] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
 @[simp, grind =] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
 @[simp, grind =] theorem pure_run (a : Id α) : pure a.run = a := rfl
-@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
-@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
+@[simp] theorem run_seqRight (x : Id α) (y : Id β) : (x *> y).run = y.run := rfl
+@[simp] theorem run_seqLeft (x : Id α) (y : Id β) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
 
 end Id

src/Init/Conv.lean

@@ -280,7 +280,7 @@ resulting in `t'`, which becomes the new target subgoal. -/
 syntax (name := convConvSeq) "conv" " => " convSeq : conv
 
 /-- `· conv` focuses on the main conv goal and tries to solve it using `s`. -/
-macro dot:patternIgnore("· " <|> ". ") s:convSeq : conv => `(conv| {%$dot ($s) })
+macro dot:unicode("· ", ". ") s:convSeq : conv => `(conv| {%$dot ($s) })
 
 
 /-- `fail_if_success t` fails if the tactic `t` succeeds. -/

src/Init/Data/Array/Basic.lean

@@ -148,6 +148,9 @@ end List
 
 namespace Array
 
+@[simp, grind =] theorem getElem!_toList [Inhabited α] {xs : Array α} {i : Nat} : xs.toList[i]! = xs[i]! := by
+  rw [List.getElem!_toArray]
+
 theorem size_eq_length_toList {xs : Array α} : xs.size = xs.toList.length := rfl
 
 /-! ### Externs -/
@@ -2148,7 +2151,4 @@ protected def repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
 instance {α : Type u} [Repr α] : Repr (Array α) where
   reprPrec xs _ := Array.repr xs
 
-instance [ToString α] : ToString (Array α) where
-  toString xs := String.Internal.append "#" (toString xs.toList)
-
 end Array

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

@@ -78,7 +78,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
   simp only [lex, size_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add,
     Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.Rco.forIn'_eq_forIn'_toList]
   rw [cons_lex_cons.forIn'_congr_aux (Nat.toList_rco_eq_cons (by omega)) rfl (fun _ _ _ => rfl)]
-  simp only [bind_pure_comp, map_pure, Nat.toList_rco_succ_succ, Nat.add_comm 1]
+  simp only [Nat.toList_rco_succ_succ, Nat.add_comm 1]
   cases h : lt a b
   · cases h' : a == b <;> simp [bne, *]
   · simp [*]

src/Init/Data/ByteArray/Basic.lean

@@ -469,5 +469,3 @@ def prevn : Iterator → Nat → Iterator
 
 end Iterator
 end ByteArray
-
-instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩

src/Init/Data/FloatArray/Basic.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Float
 import Init.Ext
 public import Init.GetElem
+public import Init.Data.ToString.Extra
 
 public section
 universe u

src/Init/Data/Int/Pow.lean

@@ -118,16 +118,19 @@ theorem toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) : (x ^ k).toNat =
   | succ k ih =>
     rw [Int.pow_succ, Int.toNat_mul (Int.pow_nonneg h) h, ih, Nat.pow_succ]
 
-protected theorem sq_nonnneg (m : Int) : 0 ≤ m ^ 2 := by
+protected theorem sq_nonneg (m : Int) : 0 ≤ m ^ 2 := by
   rw [Int.pow_succ, Int.pow_one]
   cases m
   · apply Int.mul_nonneg <;> simp
   · apply Int.mul_nonneg_of_nonpos_of_nonpos <;> exact negSucc_le_zero _
 
+@[deprecated Int.sq_nonneg (since := "2026-03-13")]
+protected theorem sq_nonnneg (m : Int) : 0 ≤ m ^ 2 := Int.sq_nonneg m
+
 protected theorem pow_nonneg_of_even {m : Int} {n : Nat} (h : n % 2 = 0) : 0 ≤ m ^ n := by
   rw [← Nat.mod_add_div n 2, h, Nat.zero_add, Int.pow_mul]
   apply Int.pow_nonneg
-  exact Int.sq_nonnneg m
+  exact Int.sq_nonneg m
 
 protected theorem neg_pow {m : Int} {n : Nat} : (-m)^n = (-1)^(n % 2) * m^n := by
   rw [Int.neg_eq_neg_one_mul, Int.mul_pow]

src/Init/Data/Iterators/Combinators.lean

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Combinators.Append
 public import Init.Data.Iterators.Combinators.Monadic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.Iterators.Combinators.FlatMap

src/Init/Data/Iterators/Combinators/Append.lean

@@ -0,0 +1,79 @@
+/-
+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.Iterators.Combinators.Monadic.Append
+
+public section
+
+namespace Std
+open Std.Iterators Std.Iterators.Types
+
+/--
+Given two iterators `it₁` and `it₂`, `it₁.append it₂` is an iterator that first outputs all values
+of `it₁` in order and then all values of `it₂` in order.
+
+**Marble diagram:**
+
+```text
+it₁                 ---a----b---c--⊥
+it₂                                 --d--e--⊥
+it₁.append it₂      ---a----b---c-----d--e--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₁` and `it₂` are finite
+* `Productive` instance: only if `it₁` and `it₂` are productive
+
+Note: If `it₁` is not finite, then `it₁.append it₂` can be productive while `it₂` is not.
+The standard library does not provide a `Productive` instance for this case.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`.
+-/
+@[inline, expose]
+def Iter.append {α₁ : Type w} {α₂ : Type w} {β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    (it₁ : Iter (α := α₁) β) (it₂ : Iter (α := α₂) β) :
+    Iter (α := Append α₁ α₂ Id β) β :=
+  (it₁.toIterM.append it₂.toIterM).toIter
+
+/--
+This combinator is only useful for advanced use cases.
+
+Given an iterator `it₂`, returns an iterator that behaves exactly like `it₂` but is of the same
+type as `it₁.append it₂` (after `it₁` has been exhausted).
+This is useful for constructing intermediate states of the append iterator.
+
+**Marble diagram:**
+
+```text
+it₂                        --a--b--⊥
+Iter.appendSnd α₁ it₂      --a--b--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₂` and iterators of type `α₁` are finite
+* `Productive` instance: only if `it₂` and iterators of type `α₁` are productive
+
+Note: If iterators of type `α₁` are not finite, then `append α₁ it₂` can be productive while `it₂` is not.
+The standard library does not provide a `Productive` instance for this case.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₂`.
+-/
+@[inline, expose]
+def Iter.Intermediate.appendSnd {α₂ : Type w} {β : Type w}
+    [Iterator α₂ Id β] (α₁ : Type w) (it₂ : Iter (α := α₂) β) :
+    Iter (α := Append α₁ α₂ Id β) β :=
+  (IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter
+
+end Std

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

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Combinators.Monadic.Append
 public import Init.Data.Iterators.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Combinators.Monadic.FlatMap
 public import Init.Data.Iterators.Combinators.Monadic.Take

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

@@ -0,0 +1,261 @@
+/-
+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.Iterators.Consumers.Monadic.Loop
+public import Init.Classical
+import Init.Data.Option.Lemmas
+import Init.ByCases
+import Init.Omega
+
+public section
+
+/-!
+This module provides the iterator combinator `IterM.append`.
+-/
+
+namespace Std
+
+variable {α : Type w} {m : Type w → Type w'} {β : Type w}
+
+/--
+The internal state of the `IterM.append` iterator combinator.
+-/
+inductive Iterators.Types.Append (α₁ α₂ : Type w) (m : Type w → Type w') (β : Type w) where
+  | fst : IterM (α := α₁) m β → IterM (α := α₂) m β → Append α₁ α₂ m β
+  | snd : IterM (α := α₂) m β → Append α₁ α₂ m β
+
+open Std.Iterators Std.Iterators.Types
+
+/--
+Given two iterators `it₁` and `it₂`, `it₁.append it₂` is an iterator that first outputs all values
+of `it₁` in order and then all values of `it₂` in order.
+
+**Marble diagram:**
+
+```text
+it₁                 ---a----b---c--⊥
+it₂                                 --d--e--⊥
+it₁.append it₂      ---a----b---c-----d--e--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₁` and `it₂` are finite
+* `Productive` instance: only if `it₁` and `it₂` are productive
+
+Note: If `it₁` is not finite, then `it₁.append it₂` can be productive while `it₂` is not.
+The standard library does not provide a `Productive` instance for this case.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`.
+-/
+@[inline, expose]
+def IterM.append [Iterator α₁ m β] [Iterator α₂ m β]
+    (it₁ : IterM (α := α₁) m β) (it₂ : IterM (α := α₂) m β) :=
+  (⟨Iterators.Types.Append.fst it₁ it₂⟩ : IterM m β)
+
+/--
+This combinator is only useful for advanced use cases.
+
+Given an iterator `it₂`, `IterM.Intermediate.appendSnd α₁ it₂` returns an iterator that behaves
+exactly like `it₂` but has the same type as `it₁.append it₂` (after `it₁` has been exhausted).
+This is useful for constructing intermediate states of the append iterator.
+
+**Marble diagram:**
+
+```text
+it₂                                  --a--b--⊥
+IterM.Intermediate.appendSnd α₁ it₂  --a--b--⊥
+```
+
+**Termination properties:**
+
+* `Finite` instance: only if `it₂` and iterators of type `α₁` are finite
+* `Productive` instance: only if `it₂` and iterators of type `α₁` are productive
+
+Note: If iterators of type `α₁` are not finite, then `appendSnd α₁ it₂` can be productive
+while `it₂` is not. The standard library does not provide a `Productive` instance for this case.
+
+**Performance:**
+
+This combinator incurs an additional O(1) cost with each output of `it₂`.
+-/
+@[inline, expose]
+def IterM.Intermediate.appendSnd [Iterator α₂ m β] (α₁ : Type w) (it₂ : IterM (α := α₂) m β) :=
+  (⟨Iterators.Types.Append.snd (α₁ := α₁) it₂⟩ : IterM m β)
+
+namespace Iterators.Types
+
+inductive Append.PlausibleStep [Iterator α₁ m β] [Iterator α₂ m β] :
+    IterM (α := Append α₁ α₂ m β) m β → IterStep (IterM (α := Append α₁ α₂ m β) m β) β → Prop where
+  | fstYield {it₁ : IterM (α := α₁) m β}  {it₂ : IterM (α := α₂) m β} :
+    it₁.IsPlausibleStep (.yield it₁' out) → PlausibleStep (it₁.append it₂) (.yield (it₁'.append it₂) out)
+  | fstSkip {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    it₁.IsPlausibleStep (.skip it₁') → PlausibleStep (it₁.append it₂) (.skip (it₁'.append it₂))
+  | fstDone {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    it₁.IsPlausibleStep .done → PlausibleStep (it₁.append it₂) (.skip (IterM.Intermediate.appendSnd α₁ it₂))
+  | sndYield {it₂ : IterM (α := α₂) m β} :
+    it₂.IsPlausibleStep (.yield it₂' out) →
+      PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) (.yield (IterM.Intermediate.appendSnd α₁ it₂') out)
+  | sndSkip {it₂ : IterM (α := α₂) m β} :
+    it₂.IsPlausibleStep (.skip it₂') →
+      PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) (.skip (IterM.Intermediate.appendSnd α₁ it₂'))
+  | sndDone {it₂ : IterM (α := α₂) m β} :
+    it₂.IsPlausibleStep .done → PlausibleStep (IterM.Intermediate.appendSnd α₁ it₂) .done
+
+@[inline]
+instance Append.instIterator [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] :
+    Iterator (Append α₁ α₂ m β) m β where
+  IsPlausibleStep := Append.PlausibleStep
+  step
+    | ⟨.fst it₁ it₂⟩ => do
+      match (← it₁.step).inflate with
+      | .yield it₁' out h => return .deflate <| .yield (it₁'.append it₂) out (.fstYield h)
+      | .skip it₁' h => return .deflate <| .skip (it₁'.append it₂) (.fstSkip h)
+      | .done h => return .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂) (.fstDone h)
+    | ⟨.snd it₂⟩ => do
+      match (← it₂.step).inflate with
+      | .yield it₂' out h => return .deflate <| .yield (IterM.Intermediate.appendSnd α₁ it₂') out (.sndYield h)
+      | .skip it₂' h => return .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂') (.sndSkip h)
+      | .done h => return .deflate <| .done (.sndDone h)
+
+instance Append.instIteratorLoop {n : Type x → Type x'} [Monad m] [Monad n]
+    [Iterator α₁ m β] [Iterator α₂ m β] :
+    IteratorLoop (Append α₁ α₂ m β) m n :=
+  .defaultImplementation
+
+section Finite
+
+variable {α₁ : Type w} {α₂ : Type w} {m : Type w → Type w'} {β : Type w}
+
+variable (α₁ α₂ m β) in
+def Append.Rel [Monad m] [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m] :
+    IterM (α := Append α₁ α₂ m β) m β → IterM (α := Append α₁ α₂ m β) m β → Prop :=
+  InvImage
+    (Prod.Lex
+      (Option.lt (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps))
+      (InvImage IterM.TerminationMeasures.Finite.Rel IterM.finitelyManySteps))
+    (fun it => match it.internalState with
+      | .fst it₁ it₂ => (some it₁, it₂)
+      | .snd it₂ => (none, it₂))
+
+theorem Append.rel_of_fst [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] {it₁ it₁' : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β}
+    (h : it₁'.finitelyManySteps.Rel it₁.finitelyManySteps) :
+    Append.Rel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂) := by
+  exact Prod.Lex.left _ _ h
+
+theorem Append.rel_fstDone [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    Append.Rel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂) := by
+  exact Prod.Lex.left _ _ trivial
+
+theorem Append.rel_of_snd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] {it₂ it₂' : IterM (α := α₂) m β}
+    (h : it₂'.finitelyManySteps.Rel it₂.finitelyManySteps) :
+    Append.Rel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂') (IterM.Intermediate.appendSnd α₁ it₂) := by
+  exact Prod.Lex.right _ h
+
+def Append.instFinitenessRelation [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] :
+    FinitenessRelation (Append α₁ α₂ m β) m where
+  Rel := Append.Rel α₁ α₂ m β
+  wf := by
+    apply InvImage.wf
+    refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
+    · exact Option.wellFounded_lt <| InvImage.wf _ WellFoundedRelation.wf
+    · exact InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    cases h' <;> cases h
+    case fstYield =>
+      apply Append.rel_of_fst
+      exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case fstSkip =>
+      apply Append.rel_of_fst
+      exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
+    case fstDone =>
+      exact Append.rel_fstDone
+    case sndYield =>
+      apply Append.rel_of_snd
+      exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
+    case sndSkip =>
+      apply Append.rel_of_snd
+      exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
+
+@[no_expose]
+public instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Finite α₁ m] [Finite α₂ m] : Finite (Append α₁ α₂ m β) m :=
+  .of_finitenessRelation instFinitenessRelation
+
+end Finite
+
+section Productive
+
+variable {α₁ : Type w} {α₂ : Type w} {m : Type w → Type w'} {β : Type w}
+
+variable (α₁ α₂ m β) in
+def Append.ProductiveRel [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] :
+    IterM (α := Append α₁ α₂ m β) m β → IterM (α := Append α₁ α₂ m β) m β → Prop :=
+  InvImage
+    (Prod.Lex
+      (Option.lt (InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips))
+      (InvImage IterM.TerminationMeasures.Productive.Rel IterM.finitelyManySkips))
+    (fun it => match it.internalState with
+      | .fst it₁ it₂ => (some it₁, it₂)
+      | .snd it₂ => (none, it₂))
+
+theorem Append.productiveRel_of_fst [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] {it₁ it₁' : IterM (α := α₁) m β}
+    {it₂ : IterM (α := α₂) m β}
+    (h : it₁'.finitelyManySkips.Rel it₁.finitelyManySkips) :
+    Append.ProductiveRel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂) := by
+  exact Prod.Lex.left _ _ h
+
+theorem Append.productiveRel_fstDone [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] {it₁ : IterM (α := α₁) m β}
+    {it₂ : IterM (α := α₂) m β} :
+    Append.ProductiveRel α₁ α₂ m β (IterM.Intermediate.appendSnd α₁ it₂) (it₁.append it₂) := by
+  exact Prod.Lex.left _ _ trivial
+
+theorem Append.productiveRel_of_snd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] {it₂ it₂' : IterM (α := α₂) m β}
+    (h : it₂'.finitelyManySkips.Rel it₂.finitelyManySkips) :
+    Append.ProductiveRel α₁ α₂ m β
+      (IterM.Intermediate.appendSnd α₁ it₂') (IterM.Intermediate.appendSnd α₁ it₂) := by
+  exact Prod.Lex.right _ h
+
+private def Append.instProductivenessRelation [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] :
+    ProductivenessRelation (Append α₁ α₂ m β) m where
+  Rel := Append.ProductiveRel α₁ α₂ m β
+  wf := by
+    apply InvImage.wf
+    refine ⟨fun (a, b) => Prod.lexAccessible (WellFounded.apply ?_ a) (WellFounded.apply ?_) b⟩
+    · exact Option.wellFounded_lt <| InvImage.wf _ WellFoundedRelation.wf
+    · exact InvImage.wf _ WellFoundedRelation.wf
+  subrelation {it it'} h := by
+    cases h
+    case fstSkip =>
+      apply Append.productiveRel_of_fst
+      exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
+    case fstDone =>
+      exact Append.productiveRel_fstDone
+    case sndSkip =>
+      apply Append.productiveRel_of_snd
+      exact IterM.TerminationMeasures.Productive.rel_of_skip ‹_›
+
+instance Append.instProductive [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    [Productive α₁ m] [Productive α₂ m] : Productive (Append α₁ α₂ m β) m :=
+  .of_productivenessRelation instProductivenessRelation
+
+end Productive
+
+end Std.Iterators.Types

src/Init/Data/Iterators/Lemmas/Combinators.lean

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Lemmas.Combinators.Append
 public import Init.Data.Iterators.Lemmas.Combinators.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic
 public import Init.Data.Iterators.Lemmas.Combinators.FilterMap

src/Init/Data/Iterators/Lemmas/Combinators/Append.lean

@@ -0,0 +1,193 @@
+/-
+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.Iterators.Combinators.Append
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
+public import Init.Data.Iterators.Consumers.Collect
+public import Init.Data.Iterators.Consumers.Access
+import Init.Data.Iterators.Lemmas.Consumers.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Access
+import Init.Data.Iterators.Lemmas.Basic
+import Init.Omega
+
+public section
+
+namespace Std
+open Std.Iterators Std.Iterators.Types
+
+theorem Iter.append_eq_toIter_append_toIterM {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    it₁.append it₂ = (it₁.toIterM.append it₂.toIterM).toIter :=
+  rfl
+
+theorem Iter.Intermediate.appendSnd_eq_toIter_appendSnd_toIterM {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    {it₂ : Iter (α := α₂) β} :
+    Iter.Intermediate.appendSnd α₁ it₂ = (IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter :=
+  rfl
+
+theorem Iter.step_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    (it₁.append it₂).step =
+      match it₁.step with
+      | .yield it₁' out h => .yield (it₁'.append it₂) out (.fstYield h)
+      | .skip it₁' h => .skip (it₁'.append it₂) (.fstSkip h)
+      | .done h => .skip (Iter.Intermediate.appendSnd α₁ it₂) (.fstDone h) := by
+  simp only [Iter.step, append_eq_toIter_append_toIterM, toIterM_toIter, IterM.step_append,
+    Id.run_bind]
+  cases it₁.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;>
+    simp [Intermediate.appendSnd_eq_toIter_appendSnd_toIterM]
+
+theorem Iter.Intermediate.step_appendSnd {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β]
+    {it₂ : Iter (α := α₂) β} :
+    (Iter.Intermediate.appendSnd α₁ it₂).step =
+      match it₂.step with
+      | .yield it₂' out h => .yield (Iter.Intermediate.appendSnd α₁ it₂') out (.sndYield h)
+      | .skip it₂' h => .skip (Iter.Intermediate.appendSnd α₁ it₂') (.sndSkip h)
+      | .done h => .done (.sndDone h) := by
+  simp only [Iter.step, appendSnd, toIterM_toIter, IterM.Intermediate.step_appendSnd, Id.run_bind]
+  cases it₂.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
+
+@[simp]
+theorem Iter.toList_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    (it₁.append it₂).toList = it₁.toList ++ it₂.toList := by
+  simp [append_eq_toIter_append_toIterM, toList_eq_toList_toIterM]
+
+@[simp]
+theorem Iter.toListRev_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    (it₁.append it₂).toListRev = it₂.toListRev ++ it₁.toListRev := by
+  simp [append_eq_toIter_append_toIterM, toListRev_eq_toListRev_toIterM]
+
+@[simp]
+theorem Iter.toArray_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
+    (it₁.append it₂).toArray = it₁.toArray ++ it₂.toArray := by
+  simp [append_eq_toIter_append_toIterM, toArray_eq_toArray_toIterM]
+
+@[simp]
+theorem Iter.atIdxSlow?_appendSnd {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id]
+    {it₂ : Iter (α := α₂) β} {n : Nat} :
+    (Iter.Intermediate.appendSnd α₁ it₂).atIdxSlow? n = it₂.atIdxSlow? n := by
+  induction n, it₂ using Iter.atIdxSlow?.induct_unfolding with
+  | yield_zero it it' out h h' =>
+    simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it),
+      Intermediate.step_appendSnd, h']
+  | yield_succ it it' out h h' n ih =>
+    simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it),
+      Intermediate.step_appendSnd, h', ih]
+  | skip_case n it it' h h' ih =>
+    simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it),
+      Intermediate.step_appendSnd, h', ih]
+  | done_case n it h h' =>
+    simp only [atIdxSlow?_eq_match (it := Iter.Intermediate.appendSnd α₁ it),
+      Intermediate.step_appendSnd, h']
+
+theorem Iter.atIdxSlow?_append_of_eq_some {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n : Nat} {b : β}
+    (h : it₁.atIdxSlow? n = some b) :
+    (it₁.append it₂).atIdxSlow? n = some b := by
+  induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing it₂ with
+  | yield_zero it it' out hp h' =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    cases h
+    simp [step_append, h']
+  | yield_succ it it' out hp h' n ih =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp [step_append, h', ih h]
+  | skip_case n it it' hp h' ih =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp [step_append, h', ih h]
+  | done_case n it hp h' =>
+    cases h
+
+theorem Iter.atIdxSlow?_append {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Productive α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n : Nat} :
+    (it₁.append it₂).atIdxSlow? n =
+      if n < it₁.toList.length then it₁.atIdxSlow? n
+      else it₂.atIdxSlow? (n - it₁.toList.length) := by
+  induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing it₂ with
+  | yield_zero it it' out h h' =>
+    simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h']
+    rw [toList_eq_match_step (it := it)]
+    simp [h']
+  | yield_succ it it' out h h' n ih =>
+    simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h', ih]
+    rw [toList_eq_match_step (it := it)]
+    simp [h', Nat.succ_lt_succ_iff, Nat.succ_sub_succ]
+  | skip_case n it it' h h' ih =>
+    simp only [atIdxSlow?_eq_match (it := it.append it₂), step_append, h', ih]
+    rw [toList_eq_match_step (it := it)]
+    simp [h']
+  | done_case n it h h' =>
+    simp [atIdxSlow?_eq_match (it := it.append it₂), step_append, h',
+      atIdxSlow?_appendSnd, toList_eq_match_step]
+
+theorem Iter.atIdxSlow?_append_of_productive {α₁ α₂ β : Type w}
+    [Iterator α₁ Id β] [Iterator α₂ Id β] [Productive α₁ Id] [Productive α₂ Id]
+    {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} {n k : Nat}
+    (hk : it₁.atIdxSlow? k = none)
+    (hmin : ∀ j, j < k → (it₁.atIdxSlow? j).isSome)
+    (hle : k ≤ n) :
+    (it₁.append it₂).atIdxSlow? n = it₂.atIdxSlow? (n - k) := by
+  induction n, it₁ using Iter.atIdxSlow?.induct_unfolding generalizing k it₂ with
+  | yield_zero it it' out hp h' =>
+    exfalso
+    have : k = 0 := by omega
+    subst this
+    rw [atIdxSlow?_eq_match (it := it)] at hk
+    simp [h'] at hk
+  | yield_succ it it' out hp h' n ih =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp only [step_append, h']
+    match k with
+    | 0 =>
+      rw [atIdxSlow?_eq_match (it := it)] at hk
+      simp [h'] at hk
+    | k + 1 =>
+      rw [atIdxSlow?_eq_match (it := it)] at hk
+      simp [h'] at hk
+      have hmin' : ∀ j, j < k → (it'.atIdxSlow? j).isSome := by
+        intro j hj
+        have h := hmin (j + 1) (by omega)
+        rw [atIdxSlow?_eq_match (it := it)] at h
+        simpa [h'] using h
+      rw [ih hk hmin' (by omega)]
+      congr 1
+      omega
+  | skip_case n it it' hp h' ih =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp only [step_append, h']
+    rw [atIdxSlow?_eq_match (it := it)] at hk; simp [h'] at hk
+    have hmin' : ∀ j, j < k → (it'.atIdxSlow? j).isSome := by
+      intro j hj
+      have h := hmin j hj
+      rw [atIdxSlow?_eq_match (it := it)] at h
+      simpa [h'] using h
+    exact ih hk hmin' hle
+  | done_case n it hp h' =>
+    rw [atIdxSlow?_eq_match (it := it.append it₂)]
+    simp only [step_append, h', atIdxSlow?_appendSnd]
+    have hk0 : k = 0 := by
+      false_or_by_contra
+      have h := hmin 0 (by omega)
+      rw [atIdxSlow?_eq_match (it := it)] at h
+      simp [h'] at h
+    simp [hk0]
+
+end Std

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

@@ -435,8 +435,9 @@ theorem Iter.forIn_filterMapWithPostcondition
         match ← (f out).run with
         | some c => g c acc
         | none => return .yield acc) := by
-  simp +instances [Iter.forIn_eq_forIn_toIterM, filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+  simp only [filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition, forIn_eq_forIn_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  rfl -- expressions are equal up to different matchers
 
 theorem Iter.forIn_filterMapM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -448,8 +449,9 @@ theorem Iter.forIn_filterMapM
         match ← f out with
         | some c => g c acc
         | none => return .yield acc) := by
-  simp +instances [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+  simp [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  rfl
 
 theorem Iter.forIn_filterMap
     [Monad n] [LawfulMonad n] [Finite α Id]
@@ -469,8 +471,8 @@ theorem Iter.forIn_mapWithPostcondition
     {g : β₂ → γ → o (ForInStep γ)} :
     forIn (it.mapWithPostcondition f) init g =
       forIn it init (fun out acc => do g (← (f out).run) acc) := by
-  simp +instances [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_mapM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -498,8 +500,8 @@ theorem Iter.forIn_filterWithPostcondition
     haveI : MonadLift n o := ⟨monadLift⟩
     forIn (it.filterWithPostcondition f) init g =
       forIn it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc) := by
-  simp +instances [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_filterM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -508,8 +510,8 @@ theorem Iter.forIn_filterM
     [IteratorLoop α Id o] [LawfulIteratorLoop α Id o]
     {it : Iter (α := α) β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} :
     forIn (it.filterM f) init g = forIn it init (fun out acc => do if (← f out).down then g out acc else return .yield acc) := by
-  simp +instances [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_filter
     [Monad n] [LawfulMonad n]
@@ -550,8 +552,9 @@ theorem Iter.foldM_filterMapM {α β γ δ : Type w}
       it.foldM (init := init) (fun d b => do
           let some c ← f b | pure d
           g d c) := by
-  simp +instances [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
+  simp only [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  rfl
 
 theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -563,8 +566,8 @@ theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
     {f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : Iter (α := α) β} :
     (it.mapWithPostcondition f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do let c ← (f b).run; g d c) := by
-  simp +instances [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_mapM {α β γ δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -578,8 +581,8 @@ theorem Iter.foldM_mapM {α β γ δ : Type w}
     haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
     (it.mapM f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
-  simp +instances [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -591,8 +594,8 @@ theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
     {f : β → PostconditionT n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
     (it.filterWithPostcondition f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do if (← (f b).run).down then g d b else pure d) := by
-  simp +instances [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_filterM {α β δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -605,8 +608,8 @@ theorem Iter.foldM_filterM {α β δ : Type w}
     {f : β → n (ULift Bool)} {g : δ → β → o δ} {init : δ} {it : Iter (α := α) β} :
     (it.filterM f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do if (← f b).down then g d b else pure d) := by
-  simp +instances [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM,
-    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp only [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM]
+  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_filterMap {α β γ δ : Type w} {n : Type w → Type w''}
     [Iterator α Id β] [Finite α Id] [Monad n] [LawfulMonad n]

src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean

@@ -121,22 +121,22 @@ public theorem Iter.step_flatMapAfterM {α : Type w} {β : Type w} {α₂ : Type
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Iterator α Id β] [Iterator α₂ m γ]
     {f : β → m (IterM (α := α₂) m γ)} {it₁ : Iter (α := α) β} {it₂ : Option (IterM (α := α₂) m γ)} :
   (it₁.flatMapAfterM f it₂).step = (do
-    match it₂ with
+    match hit : it₂ with
     | none =>
       match it₁.step with
       | .yield it₁' b h =>
         let fx ← MonadAttach.attach (f b)
-        return .deflate (.skip (it₁'.flatMapAfterM f (some fx.val)) (.outerYield_flatMapM_pure h fx.property))
-      | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f none) (.outerSkip_flatMapM_pure h))
-      | .done h => return .deflate (.done (.outerDone_flatMapM_pure h))
+        return .deflate (.skip (it₁'.flatMapAfterM f (some fx.val)) (hit ▸ .outerYield_flatMapM_pure h fx.property))
+      | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f it₂) (hit ▸ .outerSkip_flatMapM_pure h))
+      | .done h => return .deflate (.done (hit ▸ .outerDone_flatMapM_pure h))
     | some it₂ =>
       match (← it₂.step).inflate with
       | .yield it₂' out h =>
-        return .deflate (.yield (it₁.flatMapAfterM f (some it₂')) out (.innerYield_flatMapM_pure h))
+        return .deflate (.yield (it₁.flatMapAfterM f (some it₂')) out (hit ▸ .innerYield_flatMapM_pure h))
       | .skip it₂' h =>
-        return .deflate (.skip (it₁.flatMapAfterM f (some it₂')) (.innerSkip_flatMapM_pure h))
+        return .deflate (.skip (it₁.flatMapAfterM f (some it₂')) (hit ▸ .innerSkip_flatMapM_pure h))
       | .done h =>
-        return .deflate (.skip (it₁.flatMapAfterM f none) (.innerDone_flatMapM_pure h))) := by
+        return .deflate (.skip (it₁.flatMapAfterM f none) (hit ▸ .innerDone_flatMapM_pure h))) := by
   simp only [flatMapAfterM, IterM.step_flatMapAfterM, Iter.step_mapWithPostcondition,
     PostconditionT.operation_pure]
   split
@@ -232,7 +232,6 @@ public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → T
     (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
   simp [flatMapM, toArray_flatMapAfterM]
 
-set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -241,9 +240,9 @@ public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α I
       | some it₂ => it₂.toList ++
           (it₁.map fun b => (f b).toList).toList.flatten := by
   simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
-  cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
+  unfold Iter.toList
+  cases it₂ <;> simp [map]
 
-set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -252,6 +251,7 @@ public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α
       | some it₂ => it₂.toArray ++
           (it₁.map fun b => (f b).toArray).toArray.flatten := by
   simp only [flatMapAfter, Iter.toArray, toIterM_toIter, IterM.toArray_flatMapAfter]
+  unfold Iter.toArray
   cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM, - IterM.toArray_map]
 
 public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]

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

@@ -6,6 +6,7 @@ Authors: Paul Reichert
 module
 
 prelude
+public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
 public import Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/Append.lean

@@ -0,0 +1,107 @@
+/-
+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.Iterators.Combinators.Monadic.Append
+public import Init.Data.Iterators.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
+import Init.Data.Iterators.Lemmas.Monadic.Basic
+import Init.Data.List.Lemmas
+import Init.Data.List.ToArray
+
+public section
+
+namespace Std
+open Std.Iterators Std.Iterators.Types
+
+variable {α₁ α₂ β : Type w} {m : Type w → Type w'}
+
+theorem IterM.step_append [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    (it₁.append it₂).step = (do
+      match (← it₁.step).inflate with
+      | .yield it₁' out h =>
+        pure <| .deflate <| .yield (it₁'.append it₂) out (.fstYield h)
+      | .skip it₁' h =>
+        pure <| .deflate <| .skip (it₁'.append it₂) (.fstSkip h)
+      | .done h =>
+        pure <| .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂) (.fstDone h)) := by
+  simp only [append, Intermediate.appendSnd, step, Iterator.step]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
+
+theorem IterM.Intermediate.step_appendSnd [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+    {it₂ : IterM (α := α₂) m β} :
+    (IterM.Intermediate.appendSnd α₁ it₂).step = (do
+      match (← it₂.step).inflate with
+      | .yield it₂' out h =>
+        pure <| .deflate <| .yield (IterM.Intermediate.appendSnd α₁ it₂') out (.sndYield h)
+      | .skip it₂' h =>
+        pure <| .deflate <| .skip (IterM.Intermediate.appendSnd α₁ it₂') (.sndSkip h)
+      | .done h =>
+        pure <| .deflate <| .done (.sndDone h)) := by
+  simp only [Intermediate.appendSnd, step, Iterator.step]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn <;> rfl
+
+@[simp]
+theorem IterM.toList_appendSnd [Monad m] [LawfulMonad m]
+    [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
+    {it₂ : IterM (α := α₂) m β} :
+    (IterM.Intermediate.appendSnd α₁ it₂).toList = it₂.toList := by
+  induction it₂ using IterM.inductSteps with | step it₂ ihy ihs
+  rw [toList_eq_match_step (it := IterM.Intermediate.appendSnd α₁ it₂),
+      toList_eq_match_step (it := it₂)]
+  simp only [Intermediate.step_appendSnd, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+@[simp]
+theorem IterM.toList_append [Monad m] [LawfulMonad m]
+    [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
+    {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    (it₁.append it₂).toList = (do
+      let l₁ ← it₁.toList
+      let l₂ ← it₂.toList
+      pure (l₁ ++ l₂)) := by
+  induction it₁ using IterM.inductSteps with | step it₁ ihy ihs
+  rw [toList_eq_match_step (it := it₁.append it₂), toList_eq_match_step (it := it₁)]
+  simp only [step_append, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›, - bind_pure_comp]
+  · simp [ihs ‹_›]
+  · simp [toList_appendSnd, - bind_pure_comp]
+
+@[simp]
+theorem IterM.toListRev_append [Monad m] [LawfulMonad m]
+    [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
+    {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    (it₁.append it₂).toListRev = (do
+      let l₁ ← it₁.toListRev
+      let l₂ ← it₂.toListRev
+      pure (l₂ ++ l₁)) := by
+  rw [toListRev_eq (it := it₁.append it₂), toList_append,
+      toListRev_eq (it := it₁), toListRev_eq (it := it₂)]
+  simp [map_bind, bind_pure_comp, List.reverse_append]
+
+@[simp]
+theorem IterM.toArray_append [Monad m] [LawfulMonad m]
+    [Iterator α₁ m β] [Iterator α₂ m β] [Finite α₁ m] [Finite α₂ m]
+    {it₁ : IterM (α := α₁) m β} {it₂ : IterM (α := α₂) m β} :
+    (it₁.append it₂).toArray = (do
+      let a₁ ← it₁.toArray
+      let a₂ ← it₂.toArray
+      pure (a₁ ++ a₂)) := by
+  rw [← toArray_toList (it := it₁.append it₂), toList_append,
+      ← toArray_toList (it := it₁), ← toArray_toList (it := it₂)]
+  simp [map_bind, - bind_pure_comp, ← List.toArray_appendList, - toArray_toList]
+
+end Std

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

@@ -374,7 +374,6 @@ theorem IterM.toList_map_eq_toList_filterMapM {α β γ : Type w} {m : Type w
   simp [toList_map_eq_toList_mapM, toList_mapM_eq_toList_filterMapM]
   congr <;> simp
 
-set_option backward.whnf.reducibleClassField false in
 /--
 Variant of `toList_filterMapWithPostcondition_filterMapWithPostcondition` that is intended to be
 used with the `apply` tactic. Because neither the LHS nor the RHS determine all implicit parameters,
@@ -395,7 +394,7 @@ private theorem IterM.toList_filterMapWithPostcondition_filterMapWithPostconditi
       (it.filterMapWithPostcondition (n := o) fg).toList := by
   induction it using IterM.inductSteps with | step it ihy ihs
   letI : MonadLift n o := ⟨monadLift⟩
-  haveI : LawfulMonadLift n o := ⟨by simp +instances [this], by simp +instances [this]⟩
+  haveI : LawfulMonadLift n o := ⟨LawfulMonadLiftT.monadLift_pure, LawfulMonadLiftT.monadLift_bind⟩
   rw [toList_eq_match_step, toList_eq_match_step, step_filterMapWithPostcondition,
     bind_assoc, step_filterMapWithPostcondition, step_filterMapWithPostcondition]
   simp only [bind_assoc, liftM_bind]
@@ -602,7 +601,6 @@ theorem IterM.toList_map_mapM {α β γ δ : Type w}
     toList_filterMapM_mapM]
   congr <;> simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m]
@@ -626,7 +624,6 @@ theorem IterM.toList_filterMapWithPostcondition {α β γ : Type w} {m : Type w
   · simp [ihs ‹_›, heq]
   · simp [heq]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m] [Iterator α Id β] [Finite α Id]
@@ -647,25 +644,25 @@ theorem IterM.toList_mapWithPostcondition {α β γ : Type w} {m : Type w → Ty
   · simp [ihs ‹_›, heq]
   · simp [heq]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_filterMapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
     [Iterator α Id β] [Finite α Id]
     {f : β → m (Option γ)} (it : IterM (α := α) Id β) :
     (it.filterMapM f).toList = it.toList.run.filterMapM f := by
-  simp [toList_filterMapM_eq_toList_filterMapWithPostcondition, toList_filterMapWithPostcondition,
-    PostconditionT.attachLift, PostconditionT.run_eq_map, WeaklyLawfulMonadAttach.map_attach]
+  simp only [toList_filterMapM_eq_toList_filterMapWithPostcondition,
+    toList_filterMapWithPostcondition, PostconditionT.run_eq_map]
+  simp [PostconditionT.attachLift, WeaklyLawfulMonadAttach.map_attach]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem IterM.toList_mapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
     [Iterator α Id β] [Finite α Id]
     {f : β → m γ} (it : IterM (α := α) Id β) :
     (it.mapM f).toList = it.toList.run.mapM f := by
-  simp [toList_mapM_eq_toList_mapWithPostcondition, toList_mapWithPostcondition,
-    PostconditionT.attachLift, PostconditionT.run_eq_map, WeaklyLawfulMonadAttach.map_attach]
+  simp only [toList_mapM_eq_toList_mapWithPostcondition, toList_mapWithPostcondition,
+    PostconditionT.run_eq_map]
+  simp [PostconditionT.attachLift, WeaklyLawfulMonadAttach.map_attach]
 
 @[simp]
 theorem IterM.toList_filterMap {α β γ : Type w} {m : Type w → Type w'}
@@ -1303,7 +1300,6 @@ theorem IterM.forIn_filterMap
   rw [filterMap, forIn_filterMapWithPostcondition]
   simp [PostconditionT.run_eq_map]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem IterM.forIn_mapWithPostcondition
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
     [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
@@ -1314,9 +1310,9 @@ theorem IterM.forIn_mapWithPostcondition
     haveI : MonadLift n o := ⟨monadLift⟩
     forIn (it.mapWithPostcondition f) init g =
       forIn it init (fun out acc => do g (← (f out).run) acc) := by
-  rw [mapWithPostcondition, InternalCombinators.map, ← InternalCombinators.filterMap,
-    ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
-  simp [PostconditionT.run_eq_map]
+  unfold mapWithPostcondition InternalCombinators.map Map.instIterator Map.instIteratorLoop Map
+  rw [← InternalCombinators.filterMap, ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
+  simp
 
 theorem IterM.forIn_mapM
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -1480,7 +1476,7 @@ theorem IterM.foldM_filterM {α β δ : Type w}
   simp [filterM, foldM_filterMapWithPostcondition, PostconditionT.run_attachLift]
   congr 1; ext out acc
   apply bind_congr; intro fx
-  cases fx.down <;> simp [PostconditionT.run_eq_map]
+  cases fx.down <;> simp
 
 theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]

src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.lean

@@ -21,14 +21,14 @@ open Std.Internal Std.Iterators
 theorem IterM.step_flattenAfter {α α₂ β : Type w} {m : Type w → Type w'} [Monad m]
     [Iterator α m (IterM (α := α₂) m β)] [Iterator α₂ m β]
     {it₁ : IterM (α := α) m (IterM (α := α₂) m β)} {it₂ : Option (IterM (α := α₂) m β)} :
-  (it₁.flattenAfter it₂).step = (do
+  (it₁.flattenAfter it₂).step = (
     match it₂ with
-    | none =>
+    | none => do
       match (← it₁.step).inflate with
       | .yield it₁' it₂' h => return .deflate (.skip (it₁'.flattenAfter (some it₂')) (.outerYield h))
       | .skip it₁' h => return .deflate (.skip (it₁'.flattenAfter none) (.outerSkip h))
       | .done h => return .deflate (.done (.outerDone h))
-    | some it₂ =>
+    | some it₂ => do
       match (← it₂.step).inflate with
       | .yield it₂' out h => return .deflate (.yield (it₁.flattenAfter (some it₂')) out (.innerYield h))
       | .skip it₂' h => return .deflate (.skip (it₁.flattenAfter (some it₂')) (.innerSkip h))
@@ -130,16 +130,16 @@ public theorem IterM.step_flatMapAfterM {α : Type w} {β : Type w} {α₂ : Typ
     {γ : Type w} {m : Type w → Type w'} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
     [Iterator α m β] [Iterator α₂ m γ] {f : β → m (IterM (α := α₂) m γ)} {it₁ : IterM (α := α) m β}
     {it₂ : Option (IterM (α := α₂) m γ)} :
-  (it₁.flatMapAfterM f it₂).step = (do
+  (it₁.flatMapAfterM f it₂).step = (
     match it₂ with
-    | none =>
+    | none => do
       match (← it₁.step).inflate with
       | .yield it₁' b h =>
         let fx ← MonadAttach.attach (f b)
         return .deflate (.skip (it₁'.flatMapAfterM f (some fx.val)) (.outerYield_flatMapM h fx.property))
       | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfterM f none) (.outerSkip_flatMapM h))
       | .done h => return .deflate (.done (.outerDone_flatMapM h))
-    | some it₂ =>
+    | some it₂ => do
       match (← it₂.step).inflate with
       | .yield it₂' out h => return .deflate (.yield (it₁.flatMapAfterM f (some it₂')) out (.innerYield_flatMapM h))
       | .skip it₂' h => return .deflate (.skip (it₁.flatMapAfterM f (some it₂')) (.innerSkip_flatMapM h))
@@ -171,15 +171,15 @@ public theorem IterM.step_flatMapM {α : Type w} {β : Type w} {α₂ : Type w}
 public theorem IterM.step_flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] [Iterator α m β] [Iterator α₂ m γ]
     {f : β → IterM (α := α₂) m γ} {it₁ : IterM (α := α) m β} {it₂ : Option (IterM (α := α₂) m γ)} :
-  (it₁.flatMapAfter f it₂).step = (do
+  (it₁.flatMapAfter f it₂).step = (
     match it₂ with
-    | none =>
+    | none => do
       match (← it₁.step).inflate with
       | .yield it₁' b h =>
         return .deflate (.skip (it₁'.flatMapAfter f (some (f b))) (.outerYield_flatMap h))
       | .skip it₁' h => return .deflate (.skip (it₁'.flatMapAfter f none) (.outerSkip_flatMap h))
       | .done h => return .deflate (.done (.outerDone_flatMap h))
-    | some it₂ =>
+    | some it₂ => do
       match (← it₂.step).inflate with
       | .yield it₂' out h => return .deflate (.yield (it₁.flatMapAfter f (some it₂')) out (.innerYield_flatMap h))
       | .skip it₂' h => return .deflate (.skip (it₁.flatMapAfter f (some it₂')) (.innerSkip_flatMap h))

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

@@ -32,11 +32,12 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
       IterM.DefaultConsumers.forIn' (n := m) (fun _ _ f x => f x.run) γ (fun _ _ _ => True)
         it.toIterM init _ (fun _ => id)
           (fun out h acc => return ⟨← f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc, trivial⟩) := by
-  simp +instances only [ForIn'.forIn']
+  simp only [ForIn'.forIn']
   have : ∀ a b c, f a b c = (Subtype.val <$> (⟨·, trivial⟩) <$> f a b c) := by simp
   simp +singlePass only [this]
   rw [hl.lawful (fun _ _ f x => f x.run) (wf := IteratorLoop.wellFounded_of_finite)]
-  simp +instances [IteratorLoop.defaultImplementation]
+  simp only [IteratorLoop.forIn, Functor.map_map, id_map',
+    bind_pure_comp]
 
 theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
@@ -81,7 +82,7 @@ theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β]
       letI : ForIn' m (IterM (α := α) Id β) β _ := IterM.instForIn'
       ForIn'.forIn' it.toIterM init
         (fun out h acc => f out (isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by
-  simp +instances [ForIn'.forIn', monadLift]
+  simp [ForIn'.forIn', monadLift]
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]

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

@@ -109,10 +109,10 @@ theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m
     letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn'
     ForIn'.forIn' (α := β) (m := n) it init f = IterM.DefaultConsumers.forIn' (n := n)
         (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) it init _ (fun _ => id) (return ⟨← f · · ·, trivial⟩) := by
-  simp +instances only [ForIn'.forIn']
+  simp only [ForIn'.forIn']
   have : f = (Subtype.val <$> (⟨·, trivial⟩) <$> f · · ·) := by simp
   rw [this, hl.lawful (fun _ _ f x => monadLift x >>= f) (wf := IteratorLoop.wellFounded_of_finite)]
-  simp +instances [IteratorLoop.defaultImplementation]
+  simp [IteratorLoop.forIn]
   try rfl
 
 theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]

src/Init/Data/Iterators/PostconditionMonad.lean

@@ -272,6 +272,12 @@ theorem PostconditionT.run_bind' {m : Type w → Type w'} [Monad m] [LawfulMonad
     (x >>= f).run = x.run >>= (f · |>.run) :=
   run_bind
 
+@[simp]
+protected theorem PostconditionT.run_pure {m : Type w → Type w'} [Monad m] [LawfulMonad m]
+    {α : Type w} {x : α} :
+    (pure x : PostconditionT m α).run = pure x := by
+  simp [run_eq_map]
+
 @[simp]
 theorem PostconditionT.property_lift {m : Type w → Type w'} [Functor m] {α : Type w}
     {x : m α} : (lift x : PostconditionT m α).Property = (fun _ => True) := by

src/Init/Data/List/Lemmas.lean

@@ -936,6 +936,12 @@ theorem getElem_zero_eq_head {l : List α} (h : 0 < l.length) :
   | nil => simp at h
   | cons _ _ => simp
 
+theorem head!_eq_getElem! [Inhabited α] {l : List α} : head! l = l[0]! := by
+  cases l <;> rfl
+
+theorem headD_eq_getD {l : List α} {fallback} : headD l fallback = l.getD 0 fallback := by
+  cases l <;> rfl
+
 theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
   cases xs with
   | nil => simp at h

src/Init/Data/List/ToArray.lean

@@ -225,7 +225,7 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
 @[simp, grind =] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]
-  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  simp only [forIn_toArray]
   induction l with
   | nil => simp
   | cons a l ih =>
@@ -258,7 +258,7 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
 @[simp, grind =] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
     l.toArray.findM? f = l.findM? f := by
   rw [Array.findM?]
-  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  simp only [forIn_toArray]
   induction l with
   | nil => simp
   | cons a l ih =>

src/Init/Data/Option/Instances.lean

@@ -172,10 +172,10 @@ instance [Monad m] : ForM m (Option α) α :=
   ⟨Option.forM⟩
 
 instance [Monad m] : ForIn' m (Option α) α inferInstance where
-  forIn' x init f := do
+  forIn' x init f :=
     match x with
     | none => return init
-    | some a =>
+    | some a => do
       match ← f a rfl init with
       | .done r | .yield r => return r
 

src/Init/Data/Order/Factories.lean

@@ -208,7 +208,7 @@ public instance LawfulOrderLT.of_lt {α : Type u} [LT α] [i : Asymm (α := α)
     haveI := LE.ofLT α
     LawfulOrderLT α :=
   letI := LE.ofLT α
-  { lt_iff a b := by simp +instances [LE.le]; apply Asymm.asymm }
+  { lt_iff a b := by simp [LE.le]; apply Asymm.asymm }
 
 /--
 If an `LT α` instance is asymmetric and its negation is transitive, then `LE.ofLT α` represents a
@@ -253,8 +253,7 @@ public theorem LawfulOrderInf.of_lt {α : Type u} [Min α] [LT α]
   letI := LE.ofLT α
   { le_min_iff a b c := by
       open Classical in
-      simp +instances only [LE.le]
-      simp [← not_or, Decidable.not_iff_not]
+      simp only [LE.le, ← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using min_lt_iff a b c }
 
 /--
@@ -283,8 +282,7 @@ public theorem LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α]
   letI := LE.ofLT α
   { max_le_iff a b c := by
       open Classical in
-      simp +instances only [LE.le]
-      simp [← not_or, Decidable.not_iff_not]
+      simp only [LE.le, ← not_or, Decidable.not_iff_not]
       simpa [Decidable.imp_iff_not_or] using lt_max_iff a b c }
 
 /--

src/Init/Data/Order/Opposite.lean

@@ -287,7 +287,7 @@ scoped instance (priority := low) instLawfulOrderLTOpposite {il : LE α} {it : L
   letI := il.opposite
   letI := it.opposite
   { lt_iff a b := by
-      simp +instances only [LE.opposite, LT.opposite]
+      simp only [LE.le, LT.lt]
       letI := il; letI := it
       exact LawfulOrderLT.lt_iff b a }
 
@@ -297,7 +297,7 @@ scoped instance (priority := low) instLawfulOrderBEqOpposite {il : LE α} {ib :
     LawfulOrderBEq α :=
   letI := il.opposite
   { beq_iff_le_and_ge a b := by
-      simp +instances only [LE.opposite]
+      simp only [LE.le]
       letI := il; letI := ib
       rw [LawfulOrderBEq.beq_iff_le_and_ge]
       exact and_comm }
@@ -310,7 +310,7 @@ scoped instance (priority := low) instLawfulOrderInfOpposite {il : LE α} {im :
   letI := il.opposite
   letI := im.oppositeMax
   { max_le_iff a b c := by
-      simp +instances only [LE.opposite, Min.oppositeMax]
+      simp only [LE.le, Max.max]
       letI := il; letI := im
       exact LawfulOrderInf.le_min_iff c a b }
 
@@ -322,11 +322,11 @@ scoped instance (priority := low) instLawfulOrderMinOpposite {il : LE α} {im :
   letI := il.opposite
   letI := im.oppositeMax
   { max_eq_or a b := by
-      simp +instances only [Min.oppositeMax]
+      simp only [Max.max]
       letI := il; letI := im
       exact MinEqOr.min_eq_or a b
     max_le_iff a b c := by
-      simp +instances only [LE.opposite, Min.oppositeMax]
+      simp only [LE.le, Max.max]
       letI := il; letI := im
       exact LawfulOrderInf.le_min_iff c a b }
 
@@ -338,7 +338,7 @@ scoped instance (priority := low) instLawfulOrderSupOpposite {il : LE α} {im :
   letI := il.opposite
   letI := im.oppositeMin
   { le_min_iff a b c := by
-      simp +instances only [LE.opposite, Max.oppositeMin]
+      simp only [LE.le, Min.min]
       letI := il; letI := im
       exact LawfulOrderSup.max_le_iff b c a }
 
@@ -350,11 +350,11 @@ scoped instance (priority := low) instLawfulOrderMaxOpposite {il : LE α} {im :
   letI := il.opposite
   letI := im.oppositeMin
   { min_eq_or a b := by
-      simp +instances only [Max.oppositeMin]
+      simp only [Min.min]
       letI := il; letI := im
       exact MaxEqOr.max_eq_or a b
     le_min_iff a b c := by
-      simp +instances only [LE.opposite, Max.oppositeMin]
+      simp only [LE.le, Min.min]
       letI := il; letI := im
       exact LawfulOrderSup.max_le_iff b c a }
 
@@ -366,11 +366,11 @@ scoped instance (priority := low) instLawfulOrderLeftLeaningMinOpposite {il : LE
   letI := il.opposite
   letI := im.oppositeMax
   { max_eq_left a b hab := by
-      simp +instances only [Min.oppositeMax]
+      simp only [Max.max]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMin.min_eq_left a b hab
     max_eq_right a b hab := by
-      simp +instances only [Min.oppositeMax]
+      simp only [Max.max]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMin.min_eq_right a b hab }
 
@@ -382,11 +382,11 @@ scoped instance (priority := low) instLawfulOrderLeftLeaningMaxOpposite {il : LE
   letI := il.opposite
   letI := im.oppositeMin
   { min_eq_left a b hab := by
-      simp +instances only [Max.oppositeMin]
+      simp only [Min.min]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMax.max_eq_left a b hab
     min_eq_right a b hab := by
-      simp +instances only [Max.oppositeMin]
+      simp only [Min.min]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMax.max_eq_right a b hab }
 

src/Init/Data/Order/PackageFactories.lean

@@ -796,7 +796,6 @@ automatically. If it fails, it is necessary to provide some of the fields manual
 @[inline, expose, implicit_reducible]
 public def LinearOrderPackage.ofOrd (α : Type u)
     (args : Packages.LinearOrderOfOrdArgs α := by exact {}) : LinearOrderPackage α :=
-  -- set_option backward.isDefEq.respectTransparency false in
   letI := LinearPreorderPackage.ofOrd α args.toLinearPreorderOfOrdArgs
   haveI : LawfulEqOrd α := ⟨args.eq_of_compare _ _⟩
   letI : Min α := args.min

src/Init/Data/Range/Polymorphic/RangeIterator.lean

@@ -597,7 +597,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LE α] [Decidabl
     LawfulIteratorLoop (Rxc.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp only [IterM.step_eq,
@@ -636,7 +636,7 @@ The pure function mapping a range iterator of type {name}`IterM` to the next ste
 This function is prefixed with {lit}`Monadic` in order to disambiguate it from the version for iterators
 of type {name}`Iter`.
 -/
-@[inline]
+@[inline, implicit_reducible]
 def Iterator.Monadic.step [UpwardEnumerable α] [LT α] [DecidableLT α]
     (it : IterM (α := Rxo.Iterator α) Id α) :
     IterStep (IterM (α := Rxo.Iterator α) Id α) α :=
@@ -1113,7 +1113,6 @@ private theorem Iterator.instIteratorLoop.loop_eq_wf [UpwardEnumerable α] [LT
     · rw [WellFounded.fix_eq]
       simp_all
 
-set_option backward.isDefEq.respectTransparency false in
 private theorem Iterator.instIteratorLoop.loopWf_eq [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] (γ : Type u)
@@ -1165,14 +1164,13 @@ termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf
 decreasing_by
   simp [IteratorLoop.rel, Monadic.isPlausibleStep_iff, Monadic.step, *]
 
-set_option backward.isDefEq.respectTransparency false in
 instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     {n : Type u → Type w} [Monad n] [LawfulMonad n] :
     LawfulIteratorLoop (Rxo.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp [IterM.step_eq, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure (liftBind := lift)]
@@ -1637,7 +1635,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
     LawfulIteratorLoop (Rxi.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp +instances only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
     rw [IterM.DefaultConsumers.forIn'.wf]
     split; rotate_left
     · simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure]

src/Init/Data/Range/Polymorphic/SInt.lean

@@ -248,7 +248,16 @@ instance : HasModel Int8 (BitVec 8) where
   le_iff_encode_le := by simp [LE.le, Int8.le]
   lt_iff_encode_lt := by simp [LT.lt, Int8.lt]
 
-set_option backward.whnf.reducibleClassField false in
+private theorem succ?_eq_minValueSealed {x : Int8} :
+    UpwardEnumerable.succ? x = if x + 1 = minValueSealed then none else some (x + 1) :=
+  (rfl)
+
+private theorem succMany?_eq_maxValueSealed {i : Int8} :
+    UpwardEnumerable.succMany? n i =
+      have := i.minValue_le_toInt
+      if h : i.toInt + n ≤ maxValueSealed.toInt then some (.ofIntLE _ (by omega) (maxValueSealed_def ▸ h)) else none :=
+  (rfl)
+
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -256,16 +265,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int8.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
+    simp [HasModel.succMany?_eq, succMany?_eq_maxValueSealed, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 
 instance : LawfulUpwardEnumerable Int8 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int8 := by
-  simp +instances only [instUpwardEnumerable_eq]
+  rw [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int8 where
@@ -277,7 +286,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int8 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int8 := by exact inferInstance
 
@@ -294,7 +303,7 @@ theorem instRxiHasSize_eq :
     HasModel.encode, HasModel.toNat_two_pow_sub_one_sub_toInt (show 8 > 0 by omega)]
 
 public instance instRxiLawfulHasSize : Rxi.LawfulHasSize Int8 := by
-  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int8 := by exact inferInstance
 
@@ -344,7 +353,6 @@ instance : HasModel Int16 (BitVec 16) where
   le_iff_encode_le := by simp [LE.le, Int16.le]
   lt_iff_encode_lt := by simp [LT.lt, Int16.lt]
 
-set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -440,7 +448,6 @@ instance : HasModel Int32 (BitVec 32) where
   le_iff_encode_le := by simp [LE.le, Int32.le]
   lt_iff_encode_lt := by simp [LT.lt, Int32.lt]
 
-set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -536,7 +543,6 @@ instance : HasModel Int64 (BitVec 64) where
   le_iff_encode_le := by simp [LE.le, Int64.le]
   lt_iff_encode_lt := by simp [LT.lt, Int64.lt]
 
-set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -637,7 +643,6 @@ instance : HasModel ISize (BitVec System.Platform.numBits) where
   le_iff_encode_le := by simp [LE.le, ISize.le]
   lt_iff_encode_lt := by simp [LT.lt, ISize.lt]
 
-set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext

src/Init/Data/Rat/Basic.lean

@@ -11,6 +11,7 @@ public import Init.Data.OfScientific
 public import Init.Data.Int.DivMod.Basic
 public import Init.Data.String.Defs
 public import Init.Data.ToString.Macro
+public import Init.Data.ToString.Extra
 import Init.Data.Hashable
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.DivMod.Lemmas

src/Init/Data/SInt/Basic.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.UInt.Basic
+public import Init.Data.ToString.Extra
 
 @[expose] public section
 

src/Init/Data/Slice/Array/Iterator.lean

@@ -10,6 +10,7 @@ public import Init.Data.Slice.Operations
 import all Init.Data.Range.Polymorphic.Basic
 import Init.Omega
 public import Init.Data.Array.Subarray
+public import Init.Data.ToString.Extra
 
 public section
 
@@ -25,7 +26,7 @@ variable {shape : RangeShape} {α : Type u}
 structure SubarrayIterator (α : Type u) where
   xs : Subarray α
 
-@[inline, expose]
+@[inline, expose, implicit_reducible]
 def SubarrayIterator.step :
     IterM (α := SubarrayIterator α) Id α → IterStep (IterM (α := SubarrayIterator α) m α) α
   | ⟨⟨xs⟩⟩ =>

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

@@ -28,7 +28,6 @@ open Std Std.Iterators Std.PRange Std.Slice
 
 namespace SubarrayIterator
 
-set_option backward.isDefEq.respectTransparency false in
 theorem step_eq {it : Iter (α := SubarrayIterator α) α} :
     it.step = if h : it.1.xs.start < it.1.xs.stop then
         haveI := it.1.xs.start_le_stop
@@ -215,7 +214,6 @@ public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).stop = min hi xs.size := by
   simp [toSubarray_eq_min, Subarray.stop]
 
-set_option backward.whnf.reducibleClassField false in
 public theorem Subarray.toList_eq {xs : Subarray α} :
     xs.toList = (xs.array.extract xs.start xs.stop).toList := by
   let aslice := xs

src/Init/Data/Slice/List/Iterator.lean

@@ -11,6 +11,7 @@ public import Init.Data.Iterators.Producers.List
 public import Init.Data.Iterators.Combinators.Take
 import all Init.Data.Range.Polymorphic.Basic
 public import Init.Data.Slice.Operations
+public import Init.Data.ToString.Extra
 
 public section
 

src/Init/Data/Slice/List/Lemmas.lean

@@ -70,7 +70,6 @@ end ListSlice
 
 namespace List
 
-set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.take hi).drop lo := by
@@ -78,9 +77,9 @@ public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
   simp only [Std.Rco.Sliceable.mkSlice, toSlice, ListSlice.toList_eq]
   by_cases h : lo < hi
   · have : lo ≤ hi := by omega
-    simp +instances [h, List.take_drop, Nat.add_sub_cancel' ‹_›, ← List.take_eq_take_min]
+    simp [h, List.take_drop, Nat.add_sub_cancel' ‹_›, ← List.take_eq_take_min]
   · have : min hi xs.length ≤ lo := by omega
-    simp +instances [h, Nat.min_eq_right this]
+    simp [h, Nat.min_eq_right this]
 
 @[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} :
@@ -111,12 +110,11 @@ public theorem size_mkSlice_rcc {xs : List α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.length - lo := by
   simp [← length_toList_eq_size]
 
-set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo...*].toList = xs.drop lo := by
   rw [List.drop_eq_drop_min]
-  simp +instances [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice]
+  simp [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice]
 
 @[simp, grind =]
 public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} :
@@ -290,11 +288,11 @@ section ListSubslices
 
 namespace ListSlice
 
-set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
-  simp +instances only [instSliceableListSliceNat_1, List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
+  rw [instSliceableListSliceNat_1]
+  simp only [List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
   obtain ⟨⟨xs, stop⟩⟩ := xs
   cases stop
   · simp
@@ -329,13 +327,13 @@ public theorem size_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.size - lo := by
   simp [← length_toList_eq_size]
 
-set_option backward.whnf.reducibleClassField false in
 @[simp, grind =]
 public theorem toList_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
     xs[lo...*].toList = xs.toList.drop lo := by
-  simp +instances only [instSliceableListSliceNat_2, ListSlice.toList_eq (xs := xs)]
+  rw [instSliceableListSliceNat_2]
+  simp only [ListSlice.toList_eq (xs := xs)]
   obtain ⟨⟨xs, stop⟩⟩ := xs
-  simp +instances only
+  simp only
   split <;> simp
 
 @[simp, grind =]

src/Init/Data/String/Bootstrap.lean

@@ -55,9 +55,11 @@ end String
 
 namespace String.Internal
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_posof"]
 opaque posOf (s : String) (c : Char) : Pos.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_offsetofpos"]
 opaque offsetOfPos (s : String) (pos : Pos.Raw) : Nat
 
@@ -67,6 +69,7 @@ opaque extract : (@& String) → (@& Pos.Raw) → (@& Pos.Raw) → String
 @[extern "lean_string_length"]
 opaque length : (@& String) → Nat
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_pushn"]
 opaque pushn (s : String) (c : Char) (n : Nat) : String
 
@@ -76,45 +79,57 @@ opaque append : String → (@& String) → String
 @[extern "lean_string_utf8_next"]
 opaque next (s : @& String) (p : @& Pos.Raw) : Pos.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_isempty"]
 opaque isEmpty (s : String) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_foldl"]
 opaque foldl (f : String → Char → String) (init : String) (s : String) : String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_isprefixof"]
 opaque isPrefixOf (p : String) (s : String) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_any"]
 opaque any (s : String) (p : Char → Bool) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_contains"]
 opaque contains (s : String) (c : Char) : Bool
 
 @[extern "lean_string_utf8_get"]
 opaque get (s : @& String) (p : @& Pos.Raw) : Char
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_capitalize"]
 opaque capitalize (s : String) : String
 
 @[extern "lean_string_utf8_at_end"]
 opaque atEnd : (@& String) → (@& Pos.Raw) → Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_nextwhile"]
 opaque nextWhile (s : String) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_trim"]
 opaque trim (s : String) : String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_intercalate"]
 opaque intercalate (s : String) : List String → String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_front"]
 opaque front (s : String) : Char
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_drop"]
 opaque drop (s : String) (n : Nat) : String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_dropright"]
 opaque dropRight (s : String) (n : Nat) : String
 
@@ -141,33 +156,43 @@ def List.asString (s : List Char) : String :=
 
 namespace Substring.Raw.Internal
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_tostring"]
 opaque toString : Substring.Raw → String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_drop"]
 opaque drop : Substring.Raw → Nat → Substring.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_front"]
 opaque front (s : Substring.Raw) : Char
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_takewhile"]
 opaque takeWhile : Substring.Raw → (Char → Bool) → Substring.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_extract"]
 opaque extract : Substring.Raw → String.Pos.Raw → String.Pos.Raw → Substring.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_all"]
 opaque all (s : Substring.Raw) (p : Char → Bool) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_beq"]
 opaque beq (ss1 ss2 : Substring.Raw) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_isempty"]
 opaque isEmpty (ss : Substring.Raw) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_get"]
 opaque get : Substring.Raw → String.Pos.Raw → Char
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_prev"]
 opaque prev : Substring.Raw → String.Pos.Raw → String.Pos.Raw
 
@@ -175,9 +200,11 @@ end Substring.Raw.Internal
 
 namespace String.Pos.Raw.Internal
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_pos_sub"]
 opaque sub : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_pos_min"]
 opaque min (p₁ p₂ : Pos.Raw) : Pos.Raw
 

src/Init/Data/ToString.lean

@@ -9,3 +9,4 @@ prelude
 public import Init.Data.ToString.Basic
 public import Init.Data.ToString.Macro
 public import Init.Data.ToString.Name
+public import Init.Data.ToString.Extra

src/Init/Data/ToString/Basic.lean

@@ -51,29 +51,6 @@ instance {p : Prop} : ToString (Decidable p) := ⟨fun h =>
   | Decidable.isTrue _  => "true"
   | Decidable.isFalse _ => "false"⟩
 
-/--
-Converts a list into a string, using `ToString.toString` to convert its elements.
-
-The resulting string resembles list literal syntax, with the elements separated by `", "` and
-enclosed in square brackets.
-
-The resulting string may not be valid Lean syntax, because there's no such expectation for
-`ToString` instances.
-
-Examples:
-* `[1, 2, 3].toString = "[1, 2, 3]"`
-* `["cat", "dog"].toString = "[cat, dog]"`
-* `["cat", "dog", ""].toString = "[cat, dog, ]"`
--/
-protected def List.toString [ToString α] : List α → String
-  | [] => "[]"
-  | [x] => String.Internal.append (String.Internal.append "[" (toString x)) "]"
-  | x::xs => String.push (xs.foldl (fun l r => String.Internal.append (String.Internal.append l ", ") (toString r))
-      (String.Internal.append "[" (toString x))) ']'
-
-instance {α : Type u} [ToString α] : ToString (List α) :=
-  ⟨List.toString⟩
-
 instance : ToString PUnit.{u+1} :=
   ⟨fun _ => "()"⟩
 
@@ -89,11 +66,6 @@ instance : ToString Nat :=
 instance : ToString String.Pos.Raw :=
   ⟨fun p => Nat.repr p.byteIdx⟩
 
-instance : ToString Int where
-  toString
-    | Int.ofNat m   => toString m
-    | Int.negSucc m => String.Internal.append "-" (toString (succ m))
-
 instance (n : Nat) : ToString (Fin n) :=
   ⟨fun f => toString (Fin.val f)⟩
 

src/Init/Data/ToString/Extra.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.String.Defs
+
+public section
+
+/--
+Converts a list into a string, using `ToString.toString` to convert its elements.
+
+The resulting string resembles list literal syntax, with the elements separated by `", "` and
+enclosed in square brackets.
+
+The resulting string may not be valid Lean syntax, because there's no such expectation for
+`ToString` instances.
+
+Examples:
+* `[1, 2, 3].toString = "[1, 2, 3]"`
+* `["cat", "dog"].toString = "[cat, dog]"`
+* `["cat", "dog", ""].toString = "[cat, dog, ]"`
+-/
+protected def List.toString [ToString α] : List α → String
+  | [] => "[]"
+  | [x] => "[" ++ toString x ++ "]"
+  | x::xs => String.push (xs.foldl (fun l r => l ++ ", " ++ toString r) ("[" ++ (toString x))) ']'
+
+instance {α : Type u} [ToString α] : ToString (List α) :=
+  ⟨List.toString⟩
+
+instance [ToString α] : ToString (Array α) where
+  toString xs := "#" ++ (toString xs.toList)
+
+instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
+
+instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)

src/Init/Data/Vector/Basic.lean

@@ -278,7 +278,7 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
     (xs : Vector α n) (f : (i : Nat) → α → (h : i < n) → m β) : m (Vector β n) :=
   let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = n) (ys : Vector β (n - i)) : m (Vector β n) := do
     match i, inv with
-    | 0,    _  => pure ys
+    | 0,   inv => return ys.cast (by omega)
     | i+1, inv =>
       have j_lt : j < n := by
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]

src/Init/Data/Vector/MapIdx.lean

@@ -363,7 +363,7 @@ theorem toArray_mapFinIdxM [Monad m] [LawfulMonad m] {xs : Vector α n}
       = Array.mapFinIdxM.map xs.toArray (fun i x h => f i x (size_toArray xs ▸ h))
         i j (size_toArray _ ▸ inv) bs.toArray := by
     match i with
-    | 0 => simp only [mapFinIdxM.map, map_pure, Array.mapFinIdxM.map, Nat.sub_zero]
+    | 0 => simp [mapFinIdxM.map, map_pure, Array.mapFinIdxM.map, Nat.sub_zero]
     | k + 1 =>
       simp only [mapFinIdxM.map, map_bind, Array.mapFinIdxM.map, getElem_toArray]
       conv => lhs; arg 2; intro; rw [go]

src/Init/Grind/Config.lean

@@ -15,6 +15,9 @@ Passed to `grind` using, for example, the `grind (config := { matchEqs := true }
 structure Config where
   /-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
   trace : Bool := false
+  /-- If `markInstances` is `true`, E-matching proofs are marked with instance IDs
+  for precise tracking of which theorems appear in the final proof. -/
+  markInstances : Bool := false
   /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
   or for which no patterns can be generated. -/
   lax : Bool := false

src/Init/Grind/Interactive.lean

@@ -177,7 +177,7 @@ syntax (name := next) "next " binderIdent* " => " grindSeq : grind
 `· grindSeq` focuses on the main `grind` goal and tries to solve it using the given
 sequence of `grind` tactics.
 -/
-macro dot:patternIgnore("· " <|> ". ") s:grindSeq : grind => `(grind| next%$dot =>%$dot $s:grindSeq )
+macro dot:unicode("· ", ". ") s:grindSeq : grind => `(grind| next%$dot =>%$dot $s:grindSeq )
 
 /--
 `any_goals tac` applies the tactic `tac` to every goal,

src/Init/Notation.lean

@@ -366,16 +366,19 @@ recommended_spelling "shiftLeft" for "<<<" in [HShiftLeft.hShiftLeft, «term_<<<
 recommended_spelling "shiftRight" for ">>>" in [HShiftRight.hShiftRight, «term_>>>_»]
 recommended_spelling "not" for "~~~" in [Complement.complement, «term~~~_»]
 
--- declare ASCII alternatives first so that the latter Unicode unexpander wins
-@[inherit_doc] infix:50 " <= " => LE.le
-@[inherit_doc] infix:50 " ≤ "  => LE.le
-@[inherit_doc] infix:50 " < "  => LT.lt
-@[inherit_doc] infix:50 " >= " => GE.ge
-@[inherit_doc] infix:50 " ≥ "  => GE.ge
-@[inherit_doc] infix:50 " > "  => GT.gt
-@[inherit_doc] infix:50 " = "  => Eq
-@[inherit_doc] infix:50 " == " => BEq.beq
-@[inherit_doc] infix:50 " ≍ "  => HEq
+-- TODO(kmill) remove these after stage0 update. There are builtin macros still using `«term_>=_»`
+@[inherit_doc] infix:50 (priority := low) " >= " => GE.ge
+@[inherit_doc] infix:50 (priority := low) " <= " => LE.le
+macro_rules | `($x >= $y)  => `(binrel% GE.ge $x $y)
+macro_rules | `($x <= $y)  => `(binrel% LE.le $x $y)
+
+@[inherit_doc] infix:50 unicode(" ≤ ", " <= ") => LE.le
+@[inherit_doc] infix:50 " < "                  => LT.lt
+@[inherit_doc] infix:50 unicode(" ≥ ", " >= ") => GE.ge
+@[inherit_doc] infix:50 " > "                  => GT.gt
+@[inherit_doc] infix:50 " = "                  => Eq
+@[inherit_doc] infix:50 " == "                 => BEq.beq
+@[inherit_doc] infix:50 " ≍ "                  => HEq
 
 /-!
   Remark: the infix commands above ensure a delaborator is generated for each relations.
@@ -383,39 +386,27 @@ recommended_spelling "not" for "~~~" in [Complement.complement, «term~~~_»]
   It has better support for applying coercions. For example, suppose we have `binrel% Eq n i` where `n : Nat` and
   `i : Int`. The default elaborator fails because we don't have a coercion from `Int` to `Nat`, but
   `binrel%` succeeds because it also tries a coercion from `Nat` to `Int` even when the nat occurs before the int. -/
-macro_rules | `($x <= $y) => `(binrel% LE.le $x $y)
 macro_rules | `($x ≤ $y)  => `(binrel% LE.le $x $y)
 macro_rules | `($x < $y)  => `(binrel% LT.lt $x $y)
 macro_rules | `($x > $y)  => `(binrel% GT.gt $x $y)
-macro_rules | `($x >= $y) => `(binrel% GE.ge $x $y)
 macro_rules | `($x ≥ $y)  => `(binrel% GE.ge $x $y)
 macro_rules | `($x = $y)  => `(binrel% Eq $x $y)
 macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
 
 recommended_spelling "le" for "≤" in [LE.le, «term_≤_»]
-/-- prefer `≤` over `<=` -/
-recommended_spelling "le" for "<=" in [LE.le, «term_<=_»]
 recommended_spelling "lt" for "<" in [LT.lt, «term_<_»]
 recommended_spelling "gt" for ">" in [GT.gt, «term_>_»]
 recommended_spelling "ge" for "≥" in [GE.ge, «term_≥_»]
-/-- prefer `≥` over `>=` -/
-recommended_spelling "ge" for ">=" in [GE.ge, «term_>=_»]
 recommended_spelling "eq" for "=" in [Eq, «term_=_»]
 recommended_spelling "beq" for "==" in [BEq.beq, «term_==_»]
 recommended_spelling "heq" for "≍" in [HEq, «term_≍_»]
 
-@[inherit_doc] infixr:35 " /\\ " => And
-@[inherit_doc] infixr:35 " ∧ "   => And
-@[inherit_doc] infixr:30 " \\/ " => Or
-@[inherit_doc] infixr:30 " ∨  "  => Or
+@[inherit_doc] infixr:35 unicode(" ∧ ", " /\\ ") => And
+@[inherit_doc] infixr:30 unicode(" ∨ ", " \\/ ") => Or
 @[inherit_doc] notation:max "¬" p:40 => Not p
 
 recommended_spelling "and" for "∧" in [And, «term_∧_»]
-/-- prefer `∧` over `/\` -/
-recommended_spelling "and" for "/\\" in [And, «term_/\_»]
 recommended_spelling "or" for "∨" in [Or, «term_∨_»]
-/-- prefer `∨` over `\/` -/
-recommended_spelling "or" for "\\/" in [Or, «term_\/_»]
 recommended_spelling "not" for "¬" in [Not, «term¬_»]
 
 @[inherit_doc] infixl:35 " && " => and

src/Init/NotationExtra.lean

@@ -25,9 +25,9 @@ syntax explicitBinders            := (ppSpace bracketedExplicitBinders)+ <|> unb
 open TSyntax.Compat in
 meta def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type? : Option Syntax) (body : Syntax) : MacroM Syntax :=
   let rec loop (i : Nat) (h : i ≤ idents.size) (acc : Syntax) := do
-    match i with
-    | 0   => pure acc
-    | i + 1 =>
+    match i, h with
+    | 0, _   => pure acc
+    | i + 1, h =>
       let ident := idents[i][0]
       let acc ← match ident.isIdent, type? with
         | true,  none      => `($combinator fun $ident => $acc)
@@ -39,9 +39,9 @@ meta def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax)
 
 meta def expandBracketedBindersAux (combinator : Syntax) (binders : Array Syntax) (body : Syntax) : MacroM Syntax :=
   let rec loop (i : Nat) (h : i ≤ binders.size) (acc : Syntax) := do
-    match i with
-    | 0   => pure acc
-    | i+1 =>
+    match i, h with
+    | 0, _   => pure acc
+    | i+1, h =>
       let idents := binders[i][1].getArgs
       let type   := binders[i][3]
       loop i (Nat.le_of_succ_le h) (← expandExplicitBindersAux combinator idents (some type) acc)
@@ -63,7 +63,7 @@ meta def expandBracketedBinders (combinatorDeclName : Name) (bracketedExplicitBi
   let combinator := mkCIdentFrom (← getRef) combinatorDeclName
   expandBracketedBindersAux combinator #[bracketedExplicitBinders] body
 
-syntax unifConstraint := term patternIgnore(" =?= " <|> " ≟ ") term
+syntax unifConstraint := term unicode(" ≟ ", " =?= ") term
 syntax unifConstraintElem := colGe unifConstraint ", "?
 
 syntax (docComment)? attrKind "unif_hint" (ppSpace ident)? (ppSpace bracketedBinder)*
@@ -317,7 +317,7 @@ macro_rules
       attribute [instance] $ctor)
 
 namespace Lean
-syntax cdotTk := patternIgnore("· " <|> ". ")
+syntax cdotTk := unicode("· ", ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
 

src/Init/Omega/Constraint.lean

@@ -52,6 +52,11 @@ namespace Constraint
 private local instance : Append String where
   append := String.Internal.append
 
+private local instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)
+
 instance : ToString Constraint where
   toString := private fun
   | ⟨none, none⟩ => "(-∞, ∞)"

src/Init/Omega/LinearCombo.lean

@@ -41,6 +41,14 @@ private def join (l : List String) : String :=
 private local instance : Append String where
   append := String.Internal.append
 
+private local instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)
+
+private local instance : Append String where
+  append := String.Internal.append
+
 instance : ToString LinearCombo where
   toString lc := private
     s!"{lc.const}{join <| lc.coeffs.toList.zipIdx.map fun ⟨c, i⟩ => s!" + {c} * x{i+1}"}"

src/Init/System/IO.lean

@@ -6,6 +6,7 @@ Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Ma
 module
 
 prelude
+public import Init.Control.Do
 public import Init.System.IOError
 public import Init.System.FilePath
 import Init.Data.String.TakeDrop

src/Init/Tactics.lean

@@ -577,7 +577,7 @@ If `thm` is a theorem `a = b`, then as a rewrite rule,
 * `thm` means to replace `a` with `b`, and
 * `← thm` means to replace `b` with `a`.
 -/
-syntax rwRule    := patternIgnore("← " <|> "<- ")? term
+syntax rwRule    := unicode("← ", "<- ")? term
 /-- A `rwRuleSeq` is a list of `rwRule` in brackets. -/
 syntax rwRuleSeq := " [" withoutPosition(rwRule,*,?) "]"
 
@@ -653,7 +653,7 @@ A simp lemma specification is:
 * optional `←` to use the lemma backward
 * `thm` for the theorem to rewrite with
 -/
-syntax simpLemma := ppGroup((simpPre <|> simpPost)? patternIgnore("← " <|> "<- ")? term)
+syntax simpLemma := ppGroup((simpPre <|> simpPost)? unicode("← ", "<- ")? term)
 /-- An erasure specification `-thm` says to remove `thm` from the simp set -/
 syntax simpErase := "-" term:max
 /-- The simp lemma specification `*` means to rewrite with all hypotheses -/
@@ -2262,6 +2262,42 @@ with grind
 ```
 This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`.
 
+### Witnesses
+
+When a specification has a parameter whose type is tagged with `@[mvcgen_witness_type]`, `mvcgen`
+classifies the corresponding goal as a *witness* rather than a verification condition.
+Witnesses are concrete values that the user must provide (inspired by zero-knowledge proofs),
+as opposed to invariants (predicates maintained across loop iterations) or verification conditions
+(propositions to prove).
+
+Witness goals are labelled `witness1`, `witness2`, etc. and can be provided in a `witnesses` section
+that appears before the `invariants` section:
+```
+mvcgen [...] witnesses
+· W1
+· W2
+invariants
+· I1
+with grind
+```
+Like invariants, witnesses support case label syntax:
+```
+mvcgen [...] witnesses
+| witness1 => W1
+```
+
+See the `@[mvcgen_witness_type]` attribute for how to register custom witness types.
+
+### Invariant and witness type attributes
+
+The `@[mvcgen_invariant_type]` and `@[mvcgen_witness_type]` tag attributes control how `mvcgen`
+classifies subgoals:
+* A goal whose type is an application of a type tagged with `@[mvcgen_invariant_type]` is classified
+  as an invariant (`inv<n>`).
+* A goal whose type is an application of a type tagged with `@[mvcgen_witness_type]` is classified
+  as a witness (`witness<n>`).
+* All other goals are classified as verification conditions (`vc<n>`).
+
 ### Invariant suggestions
 
 `mvcgen` will suggest invariants for you if you use the `invariants?` keyword.
@@ -2395,7 +2431,7 @@ If there are several with the same priority, it is uses the "most recent one". E
   cases d <;> rfl
 ```
 -/
-syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? unicode("← ", "<- ")? (ppSpace prio)? : attr
 
 /--
 Theorems tagged with the `wf_preprocess` attribute are used during the processing of functions defined
@@ -2409,7 +2445,7 @@ that diverges as compiled to be accepted without an explicit `partial` keyword,
 remove irrelevant subterms or change the evaluation order by hiding terms under binders. Therefore
 avoid tagging theorems with `[wf_preprocess]` unless they preserve also operational behavior.
 -/
-syntax (name := wf_preprocess) "wf_preprocess" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := wf_preprocess) "wf_preprocess" (Tactic.simpPre <|> Tactic.simpPost)? unicode("← ", "<- ")? (ppSpace prio)? : attr
 
 /--
 Theorems tagged with the `method_specs_simp` attribute are used by `@[method_specs]` to further
@@ -2421,7 +2457,7 @@ The `method_specs` theorems are created on demand (using the realizable constant
 this simp set should behave the same in all modules. Do not add theorems to it except in the module
 defining the thing you are rewriting.
 -/
-syntax (name := method_specs_simp) "method_specs_simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := method_specs_simp) "method_specs_simp" (Tactic.simpPre <|> Tactic.simpPost)? unicode("← ", "<- ")? (ppSpace prio)? : attr
 
 /--
 Register a theorem as a rewrite rule for `cbv` evaluation of a given definition.
@@ -2431,7 +2467,7 @@ You can instruct `cbv` to rewrite the lemma from right-to-left:
 @[cbv_eval ←] theorem my_thm : rhs = lhs := ...
 ```
 -/
-syntax (name := cbv_eval) "cbv_eval" patternIgnore("← " <|> "<- ")? (ppSpace ident)? : attr
+syntax (name := cbv_eval) "cbv_eval" unicode("← ", "<- ")? (ppSpace ident)? : attr
 
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"

src/Lean/AddDecl.lean

@@ -169,7 +169,7 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
 where
   doAdd := do
     profileitM Exception "type checking" (← getOptions) do
-      withTraceNode `Kernel (return m!"{exceptEmoji ·} typechecking declarations {decl.getTopLevelNames}") do
+      withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
         warnIfUsesSorry decl
         try
           let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?

src/Lean/Compiler/ExternAttr.lean

@@ -56,6 +56,7 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
   return { entries := entries.toList }
 
 -- Forward declaration
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_add_extern"]
 opaque addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit
 

src/Lean/Compiler/IR.lean

@@ -13,7 +13,6 @@ public import Lean.Compiler.IR.CompilerM
 public import Lean.Compiler.IR.NormIds
 public import Lean.Compiler.IR.Checker
 public import Lean.Compiler.IR.UnboxResult
-public import Lean.Compiler.IR.EmitC
 public import Lean.Compiler.IR.Sorry
 public import Lean.Compiler.IR.ToIR
 public import Lean.Compiler.IR.ToIRType
@@ -34,7 +33,6 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
   let mut decls := decls
   decls ← updateSorryDep decls
   logDecls `result decls
-  checkDecls decls
   addDecls decls
   inferMeta decls
   return decls

src/Lean/Compiler/IR/AddExtern.lean

@@ -15,6 +15,7 @@ import Lean.Compiler.LCNF.ExplicitBoxing
 import Lean.Compiler.LCNF.Internalize
 public import Lean.Compiler.ExternAttr
 import Lean.Compiler.LCNF.ExplicitRC
+import Lean.Compiler.Options
 
 public section
 
@@ -32,9 +33,10 @@ where
     let type ← Compiler.LCNF.getOtherDeclMonoType declName
     let mut typeIter := type
     let mut params := #[]
+    let ignoreBorrow := Compiler.compiler.ignoreBorrowAnnotation.get (← getOptions)
     repeat
       let .forallE binderName ty b _ := typeIter | break
-      let borrow := isMarkedBorrowed ty
+      let borrow := !ignoreBorrow && isMarkedBorrowed ty
       params := params.push {
         fvarId := (← mkFreshFVarId)
         type := ty,
@@ -70,6 +72,9 @@ where
       decl.saveImpure
       let decls ← Compiler.LCNF.addBoxedVersions #[decl]
       let decls ← Compiler.LCNF.runExplicitRc decls
+      for decl in decls do
+        decl.saveImpure
+        modifyEnv fun env => Compiler.LCNF.recordFinalImpureDecl env decl.name
       return decls
 
   addIr (decls : Array (Compiler.LCNF.Decl .impure)) : CoreM Unit := do

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -9,7 +9,6 @@ prelude
 public import Lean.Compiler.NameMangling
 public import Lean.Compiler.IR.EmitUtil
 public import Lean.Compiler.IR.NormIds
-public import Lean.Compiler.IR.SimpCase
 public import Lean.Compiler.IR.LLVMBindings
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.ModPkgExt

src/Lean/Compiler/IR/SimpCase.lean

@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Lean.Compiler.IR.Basic
-
-public section
-
-namespace Lean.IR
-
-def ensureHasDefault (alts : Array Alt) : Array Alt :=
-  if alts.any Alt.isDefault then alts
-  else if alts.size < 2 then alts
-  else
-    let last := alts.back!
-    let alts := alts.pop
-    alts.push (Alt.default last.body)
-
-end Lean.IR

src/Lean/Compiler/LCNF/Basic.lean

@@ -850,9 +850,11 @@ where
     | .jmp .. => inc
     | .return .. | unreach .. => return ()
 
+@[inline]
 partial def Code.forM [Monad m] (c : Code pu) (f : Code pu → m Unit) : m Unit :=
   go c
 where
+  @[specialize]
   go (c : Code pu) : m Unit := do
     f c
     match c with

src/Lean/Compiler/LCNF/Check.lean

@@ -257,7 +257,7 @@ def run (x : CheckM α) : CompilerM α :=
 end Pure
 end Check
 
-def Decl.check (decl : Decl pu) : CompilerM Unit := do
+def Decl.check (decl : Decl pu) : CompilerM Unit :=
   match pu with
   | .pure => Check.Pure.run do decl.value.forCodeM (Check.Pure.checkFunDeclCore decl.name decl.params decl.type)
   | .impure => return () -- TODO: port the IR check once it actually makes sense to

src/Lean/Compiler/LCNF/EmitUtil.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+module
+
+prelude
+public import Lean.Compiler.LCNF.CompilerM
+import Lean.Compiler.LCNF.PhaseExt
+import Lean.Compiler.InitAttr
+
+namespace Lean.Compiler.LCNF
+
+private structure CollectUsedDeclsState where
+  visited : NameSet := {}
+  localDecls : Array (Decl .impure) := #[]
+  extSigs : Array (Signature .impure) := #[]
+
+/--
+Find all declarations that the declarations in `decls` transitively depend on. They are returned
+partitioned into the declarations from the current module and declarations from other modules.
+-/
+public partial def collectUsedDecls (decls : Array Name) :
+    CoreM (Array (Decl .impure) × Array (Signature .impure)) := do
+  let (_, state) ← go decls |>.run {}
+  return (state.localDecls, state.extSigs)
+where
+  go (names : Array Name) : StateRefT CollectUsedDeclsState CoreM Unit :=
+    names.forM fun name => do
+      if (← get).visited.contains name then return
+      modify fun s => { s with visited := s.visited.insert name }
+      if let some decl ← getLocalImpureDecl? name then
+        modify fun s => { s with localDecls := s.localDecls.push decl }
+        decl.value.forCodeM (·.forM visitCode)
+        let env ← getEnv
+        if let some initializer := getBuiltinInitFnNameFor? env decl.name <|> getInitFnNameFor? env decl.name then
+          go #[initializer]
+      else if let some sig ← getImpureSignature? name then
+        modify fun s => { s with extSigs := s.extSigs.push sig }
+      else
+        panic! s!"collectUsedDecls: could not find declaration or signature for '{name}'"
+
+  visitCode (code : Code .impure) : StateRefT CollectUsedDeclsState CoreM Unit := do
+    match code with
+    | .let decl _ =>
+      match decl.value with
+      | .const declName .. | .fap declName .. | .pap declName .. =>
+        go #[declName]
+      | _ => return ()
+    | _ => return ()
+
+public def usesModuleFrom (env : Environment) (modulePrefix : Name) : Bool :=
+  env.header.modules.any fun mod => mod.irPhases != .comptime && modulePrefix.isPrefixOf mod.module
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/InferType.lean

@@ -267,13 +267,13 @@ def LetValue.inferType (e : LetValue pu) : CompilerM Expr :=
   | .pure => InferType.Pure.inferLetValueType e |>.run {}
   | .impure => panic! "Infer type for impure unimplemented" -- TODO
 
-def Code.inferType (code : Code pu) : CompilerM Expr := do
+def Code.inferType (code : Code pu) : CompilerM Expr :=
   match pu with
   | .pure =>
     match code with
     | .let _ k | .fun _ k _ | .jp _ k => k.inferType
     | .return fvarId => getType fvarId
-    | .jmp fvarId args => InferType.Pure.inferAppTypeCore (← getType fvarId) args |>.run {}
+    | .jmp fvarId args => do InferType.Pure.inferAppTypeCore (← getType fvarId) args |>.run {}
     | .unreach type => return type
     | .cases c => return c.resultType
   | .impure => panic! "Infer type for impure unimplemented" -- TODO

src/Lean/Compiler/LCNF/Internalize.lean

@@ -32,14 +32,10 @@ def InternalizeM.run' (x : InternalizeM pu α) (state : FVarSubst pu) (ctx : Con
 private def refreshBinderName (binderName : Name) : InternalizeM pu Name := do
   match binderName with
   | .num p _ =>
-    let r := .num p (← getThe CompilerM.State).nextIdx
-    modifyThe CompilerM.State fun s => { s with nextIdx := s.nextIdx + 1 }
-    return r
+    return .num p (← modifyGetThe CompilerM.State fun s => (s.nextIdx, { s with nextIdx := s.nextIdx + 1 }))
   | _ =>
     if (← read).uniqueIdents then
-      let r := .num binderName (← getThe CompilerM.State).nextIdx
-      modifyThe CompilerM.State fun s => { s with nextIdx := s.nextIdx + 1 }
-      return r
+      return .num binderName (← modifyGetThe CompilerM.State fun s => (s.nextIdx, { s with nextIdx := s.nextIdx + 1 }))
     else
       return binderName
 
@@ -59,7 +55,10 @@ private def mkNewFVarId (fvarId : FVarId) : InternalizeM pu FVarId := do
   addFVarSubst fvarId fvarId'
   return fvarId'
 
-private partial def internalizeExpr (e : Expr) : InternalizeM pu Expr :=
+private partial def internalizeExpr (e : Expr) : InternalizeM pu Expr := do
+  if pu == .impure then
+    -- impure types don't contain fvars
+    return e
   go e
 where
   goApp (e : Expr) : InternalizeM pu Expr := do

src/Lean/Compiler/LCNF/Main.lean

@@ -38,6 +38,7 @@ def shouldGenerateCode (declName : Name) : CoreM Bool := do
   if hasMacroInlineAttribute env declName then return false
   if (getImplementedBy? env declName).isSome then return false
   if (← Meta.isMatcher declName) then return false
+  if (← Meta.isMatcherLike declName) then return false
   if isCasesOnLike env declName then return false
   -- TODO: check if type class instance
   return true

src/Lean/Compiler/LCNF/Passes.lean

@@ -85,7 +85,9 @@ def saveImpure : Pass where
   phaseOut := .impure
   name := `saveImpure
   run decls := decls.mapM fun decl => do
-    (← normalizeFVarIds decl).saveImpure
+    let decl ← normalizeFVarIds decl
+    decl.saveImpure
+    modifyEnv fun env => recordFinalImpureDecl env decl.name
     return decl
   shouldAlwaysRunCheck := true
 
@@ -160,8 +162,8 @@ def builtinPassManager : PassManager := {
     pushProj (occurrence := 1),
     detectSimpleGround,
     inferVisibility (phase := .impure),
-    saveImpure, -- End of impure phase
     toposortPass,
+    saveImpure, -- End of impure phase
   ]
 }
 

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -23,15 +23,15 @@ namespace Lean.Compiler.LCNF
 /--
 Set of public declarations whose base bodies should be exported to other modules
 -/
-private builtin_initialize baseTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+private builtin_initialize baseTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 /--
 Set of public declarations whose mono bodies should be exported to other modules
 -/
-private builtin_initialize monoTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+private builtin_initialize monoTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 /--
 Set of public declarations whose impure bodies should be exported to other modules
 -/
-private builtin_initialize impureTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+private builtin_initialize impureTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 
 private def getTransparencyExt : Phase → EnvExtension (List Name × NameSet)
   | .base => baseTransparentDeclsExt
@@ -171,6 +171,9 @@ def getMonoDecl? (declName : Name) : CoreM (Option (Decl .pure)) := do
 def getLocalImpureDecl? (declName : Name) : CoreM (Option (Decl .impure)) := do
   return impureExt.getState (← getEnv) |>.find? declName
 
+def getLocalImpureDecls : CoreM (Array Name) := do
+  return impureExt.getState (← getEnv) |>.toArray |>.map (·.fst)
+
 def getImpureSignature? (declName : Name) : CoreM (Option (Signature .impure)) := do
   return getSigCore? (← getEnv) impureSigExt declName
 
@@ -213,7 +216,7 @@ def getDecl? (declName : Name) : CompilerM (Option ((pu : Purity) × Decl pu)) :
   let some decl ← getDeclAt? declName (← getPhase) | return none
   return some ⟨_, decl⟩
 
-def getLocalDeclAt? (declName : Name) (phase : Phase) : CompilerM (Option (Decl phase.toPurity)) := do
+def getLocalDeclAt? (declName : Name) (phase : Phase) : CompilerM (Option (Decl phase.toPurity)) :=
   match phase with
   | .base => return baseExt.getState (← getEnv) |>.find? declName
   | .mono => return monoExt.getState (← getEnv) |>.find? declName
@@ -224,4 +227,23 @@ def getLocalDecl? (declName : Name) : CompilerM (Option ((pu : Purity) × Decl p
   let some decl ← getLocalDeclAt? declName (← getPhase) | return none
   return some ⟨_, decl⟩
 
+builtin_initialize declOrderExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
+
+def recordFinalImpureDecl (env : Environment) (name : Name) : Environment :=
+  declOrderExt.modifyState env fun s =>
+    (name :: s.1, s.2.insert name)
+
+def getImpureDeclIndices (env : Environment) (targets : Array Name) : Std.HashMap Name Nat := Id.run do
+  let (names, set) := declOrderExt.getState env
+  let mut map := Std.HashMap.emptyWithCapacity set.size
+  let targetSet := Std.HashSet.ofArray targets
+  let mut i := set.size
+  for name in names do
+    if targetSet.contains name then
+      map := map.insert name i
+    assert! i != 0
+    i := i - 1
+  assert! map.size == targets.size
+  return map
+
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PublicDeclsExt.lean

@@ -10,15 +10,18 @@ public import Lean.Environment
 
 namespace Lean.Compiler.LCNF
 
-/-- Creates a replayable local environment extension holding a name set. -/
-public def mkDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
+/--
+Creates a replayable local environment extension holding a name set and the list of names in the
+order they were added to the set.
+-/
+public def mkOrderedDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
   registerEnvExtension
     (mkInitial := pure ([], {}))
     (asyncMode := .sync)
     (replay? := some <| fun oldState newState _ s =>
       let newEntries := newState.1.take (newState.1.length - oldState.1.length)
-      newEntries.foldl (init := s) fun s n =>
-        if s.1.contains n then
+      newEntries.reverse.foldl (init := s) fun s n =>
+        if s.2.contains n then
           s
         else
           (n :: s.1, if newState.2.contains n then s.2.insert n else s.2))
@@ -26,7 +29,7 @@ public def mkDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
 /--
 Set of declarations to be exported to other modules; visibility shared by base/mono/IR phases.
 -/
-private builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+private builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 
 public def isDeclPublic (env : Environment) (declName : Name) : Bool := Id.run do
   if !env.header.isModule then

src/Lean/Compiler/LCNF/SimpCase.lean

@@ -115,6 +115,16 @@ def Decl.simpCase (decl : Decl .impure) : CompilerM (Decl .impure) := do
   let value ← decl.value.mapCodeM (·.simpCase)
   return { decl with value }
 
+public def ensureHasDefault (alts : Array (Alt .impure)) : Array (Alt .impure) :=
+  if alts.any (· matches .default ..) then
+    alts
+  else if alts.size < 2 then
+    alts
+  else
+    let last := alts.back!
+    let alts := alts.pop
+    alts.push (.default last.getCode)
+
 public def simpCase : Pass :=
   Pass.mkPerDeclaration `simpCase .impure Decl.simpCase 0
 

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -7,10 +7,13 @@ module
 prelude
 public import Lean.Compiler.InitAttr
 public import Lean.Compiler.LCNF.ToLCNF
+import Lean.Compiler.Options
 import Lean.Meta.Transform
 import Lean.Meta.Match.MatcherInfo
 import Init.While
+
 public section
+
 namespace Lean.Compiler.LCNF
 /--
 Inline constants tagged with the `[macro_inline]` attribute occurring in `e`.
@@ -35,33 +38,45 @@ private def normalizeAlt (e : Expr) (numParams : Nat) : MetaM Expr :=
         Meta.mkLambdaFVars (xs ++ ys) (mkAppN e ys)
 
 /--
-Inline auxiliary `matcher` applications.
+Inline auxiliary `matcher` applications and matcher-like declarations (e.g. `match_on_same_ctor.het`)
 -/
 partial def inlineMatchers (e : Expr) : CoreM Expr :=
   Meta.MetaM.run' <| Meta.transform e fun e => do
     let .const declName us := e.getAppFn | return .continue
-    let some info ← Meta.getMatcherInfo? declName | return .continue
-    let numArgs := e.getAppNumArgs
-    if numArgs > info.arity then
-      return .continue
-    else if numArgs < info.arity then
-      Meta.forallBoundedTelescope (← Meta.inferType e) (info.arity - numArgs) fun xs _ =>
-        return .visit (← Meta.mkLambdaFVars xs (mkAppN e xs))
+    if let some info ← Meta.getMatcherInfo? declName then
+      let numArgs := e.getAppNumArgs
+      if numArgs > info.arity then
+        return .continue
+      else if numArgs < info.arity then
+        Meta.forallBoundedTelescope (← Meta.inferType e) (info.arity - numArgs) fun xs _ =>
+          return .visit (← Meta.mkLambdaFVars xs (mkAppN e xs))
+      else
+        let mut args := e.getAppArgs
+        let altNumParams := info.altNumParams
+        let rec inlineMatcher (i : Nat) (args : Array Expr) (letFVars : Array Expr) : MetaM Expr := do
+          if h : i < altNumParams.size then
+            let altIdx := i + info.getFirstAltPos
+            let numParams := altNumParams[i]
+            let alt ← normalizeAlt args[altIdx]! numParams
+            Meta.withLetDecl (← mkFreshUserName `_alt) (← Meta.inferType alt) alt fun altFVar =>
+              inlineMatcher (i+1) (args.set! altIdx altFVar) (letFVars.push altFVar)
+          else
+            let info ← getConstInfo declName
+            let value := (← Core.instantiateValueLevelParams info us).beta args
+            Meta.mkLetFVars letFVars value
+        return .visit (← inlineMatcher 0 args #[])
+    else if ← Meta.isMatcherLike declName then
+      let info ← getConstInfo declName
+      let value ← Core.instantiateValueLevelParams info us
+      /-
+      Currently the only declarations that are "matcher like" are `match_on_same_ctor.het`, for them
+      each alternative is used uniquely so we can just beta reduce without introducing code
+      duplication. If more "matcher like" things are introduced we might have to extend this with a
+      generalized notion of matcher information.
+      -/
+      return .visit (value.beta e.getAppArgs)
     else
-      let mut args := e.getAppArgs
-      let altNumParams := info.altNumParams
-      let rec inlineMatcher (i : Nat) (args : Array Expr) (letFVars : Array Expr) : MetaM Expr := do
-        if h : i < altNumParams.size then
-          let altIdx := i + info.getFirstAltPos
-          let numParams := altNumParams[i]
-          let alt ← normalizeAlt args[altIdx]! numParams
-          Meta.withLetDecl (← mkFreshUserName `_alt) (← Meta.inferType alt) alt fun altFVar =>
-            inlineMatcher (i+1) (args.set! altIdx altFVar) (letFVars.push altFVar)
-        else
-          let info ← getConstInfo declName
-          let value := (← Core.instantiateValueLevelParams info us).beta args
-          Meta.mkLetFVars letFVars value
-      return .visit (← inlineMatcher 0 args #[])
+      return .continue
 
 /--
 Replace nested occurrences of `unsafeRec` names with the safe ones.
@@ -115,10 +130,11 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
   let paramsFromTypeBinders (expr : Expr) : CompilerM (Array (Param .pure)) := do
     let mut params := #[]
     let mut currentExpr := expr
+    let ignoreBorrow := compiler.ignoreBorrowAnnotation.get (← getOptions)
     repeat
       match currentExpr with
       | .forallE binderName type body _ =>
-        let borrow := isMarkedBorrowed type
+        let borrow := !ignoreBorrow && isMarkedBorrowed type
         params := params.push (← mkParam binderName type borrow)
         currentExpr := body
       | _ => break
@@ -144,12 +160,15 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
       let value ← macroInline value
       return (type, value)
     let code ← toLCNF value
-    let decl ← if let .fun decl (.return _) := code then
+    let mut decl ← if let .fun decl (.return _) := code then
       eraseFunDecl decl (recursive := false)
       pure { name := declName, params := decl.params, type, value := .code decl.value, levelParams := info.levelParams, safe, inlineAttr? : Decl .pure }
     else
       pure { name := declName, params := #[], type, value := .code code, levelParams := info.levelParams, safe, inlineAttr? }
     /- `toLCNF` may eta-reduce simple declarations. -/
-    decl.etaExpand
+    decl ← decl.etaExpand
+    if compiler.ignoreBorrowAnnotation.get (← getOptions) then
+      decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
+    return decl
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -452,7 +452,7 @@ where
   visitCore (e : Expr) : M (Arg .pure) := withIncRecDepth do
     if let some arg := (← get).cache.find? e then
       return arg
-    let r : Arg ← match e with
+    let r : Arg .pure ← match e with
       | .app ..      => visitApp e
       | .const ..    => visitApp e
       | .proj s i e  => visitProj s i e

src/Lean/Compiler/LCNF/Toposort.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Compiler.LCNF.CompilerM
 public import Lean.Compiler.LCNF.PassManager
+import Lean.Compiler.InitAttr
 
 /-!
 This module "topologically sorts" an SCC of decls (an SCC of decls in the pipeline may in fact
@@ -42,8 +43,11 @@ where
     if (← get).seen.contains decl.name then
       return ()
 
+    let env ← getEnv
     modify fun s => { s with seen := s.seen.insert decl.name }
     decl.value.forCodeM (·.forM visitConsts)
+    if let some initializer := getBuiltinInitFnNameFor? env decl.name <|> getInitFnNameFor? env decl.name then
+      visitConst initializer
     modify fun s => { s with order := s.order.push decl }
 
   visitConsts (code : Code pu) : ToposortM pu Unit := do
@@ -51,15 +55,16 @@ where
     | .let decl _ =>
       match decl.value with
       | .const declName .. | .fap declName .. | .pap declName .. =>
-        if let some d := (← read).declsMap[declName]? then
-          process d
+        visitConst declName
       | _ => return ()
     | _ => return ()
 
+  visitConst (declName : Name) : ToposortM pu Unit := do
+    if let some d := (← read).declsMap[declName]? then
+      process d
+
 public def toposortDecls (decls : Array (Decl pu)) : CompilerM (Array (Decl pu)) := do
-  let (externDecls, otherDecls) := decls.partition (fun decl => decl.value matches .extern ..)
-  let otherDecls ← toposort otherDecls
-  return externDecls ++ otherDecls
+  toposort decls
 
 public def toposortPass : Pass where
   phase := .impure

src/Lean/Compiler/NameDemangling.lean

@@ -333,11 +333,7 @@ public def demangleBtLine (line : String) : Option String := do
   return pfx ++ demangled ++ sfx
 
 @[export lean_demangle_bt_line_cstr]
-def demangleBtLineCStr (line : @& String) : String :=
+def demangleBtLineCStr (line : String) : String :=
   (demangleBtLine line).getD ""
 
-@[export lean_demangle_symbol_cstr]
-def demangleSymbolCStr (symbol : @& String) : String :=
-  (demangleSymbol symbol).getD ""
-
 end Lean.Name.Demangle

src/Lean/Compiler/Options.lean

@@ -35,4 +35,10 @@ register_builtin_option compiler.relaxedMetaCheck : Bool := {
   descr := "Allow mixed `meta`/non-`meta` references in the same module. References to imports are unaffected."
 }
 
+register_builtin_option compiler.ignoreBorrowAnnotation : Bool := {
+  defValue := false
+  descr := "Ignore user defined borrow inference annotations. This is useful for export/extern \
+    forward declarations"
+}
+
 end Lean.Compiler

src/Lean/CoreM.lean

@@ -431,6 +431,10 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 @[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
   Prod.fst <$> x.run ctx s
 
+/--
+Run a `CoreM` monad in IO.
+Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.getNumHeartbeats`.
+-/
 @[inline] def CoreM.toIO (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do
   match (← (x.run { ctx with initHeartbeats := (← IO.getNumHeartbeats) } s).toIO') with
   | Except.error (Exception.error _ msg)   => throw <| IO.userError (← msg.toString)
@@ -440,7 +444,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
   (·.1) <$> x.toIO ctx s
 
--- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
+/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 

src/Lean/Data.lean

@@ -29,3 +29,4 @@ public import Lean.Data.NameTrie
 public import Lean.Data.RBTree
 public import Lean.Data.RBMap
 public import Lean.Data.RArray
+public import Lean.Data.Iterators

src/Lean/Data/EditDistance.lean

@@ -43,7 +43,7 @@ public def levenshtein (str1 str2 : String) (cutoff : Nat) : Option Nat := Id.ru
     let mut iter2 := str2.startPos
     let mut j : Fin (len2 + 1) := 0
     while h2 : ¬iter2.IsAtEnd do
-      let j' : Fin _ := j + 1
+      let j' : Fin (len2 + 1) := j + 1
       let deletionCost := v0[j'] + 1
       let insertionCost := v1[j] + 1
       let substCost :=

src/Lean/Data/Iterators.lean

@@ -0,0 +1,9 @@
+/-
+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 Lean.Data.Iterators.Producers

src/Lean/Data/Iterators/Producers.lean

@@ -0,0 +1,9 @@
+/-
+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 Lean.Data.Iterators.Producers.PersistentHashMap

src/Lean/Data/Iterators/Producers/PersistentHashMap.lean

@@ -0,0 +1,223 @@
+/-
+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.Subarray
+public import Init.Data.Array.Subarray.Split
+public import Lean.Data.PersistentHashMap
+import Init.Data.Iterators.Consumers
+import Init.Omega
+import Init.Data.Slice.Array.Lemmas
+import Init.Data.Array.Mem
+import Init.Data.List.TakeDrop
+
+/-!
+# PersistentHashMap iterator
+
+This module provides an iterator for `Lean.PersistentHashMap` that is accessible via
+`Lean.PersistentHashMap.iter`.
+-/
+
+public section
+
+namespace Lean.PersistentHashMap
+
+open Std Std.Iterators
+
+/--
+A zipper for traversing a `PersistentHashMap`. This is an inductive structure
+representing the remaining key-value pairs to yield.
+-/
+inductive Zipper (α : Type u) (β : Type v) where
+  /-- No more elements to yield. -/
+  | done
+  /-- A frame of entries from a trie node. -/
+  | consEntries : Subarray (Entry α β (Node α β)) → Zipper α β → Zipper α β
+  /-- A frame of key-value pairs from a collision node. -/
+  | consCollision : (keys : Subarray α) → (vals : Subarray β) → keys.size = vals.size →
+      Zipper α β → Zipper α β
+
+def Zipper.prependNode (node : Node α β) (z : Zipper α β) : Zipper α β :=
+  match node with
+  | .entries es => .consEntries es.toSubarray z
+  | .collision keys vals hsz => .consCollision keys[*...*] vals[*...*] (by simpa) z
+
+@[inline]
+def Zipper.step (it : IterM (α := Zipper α β) Id (α × β)) : IterStep (IterM (α := Zipper α β) Id (α × β)) (α × β) :=
+  match it.internalState with
+  | .done => .done
+  | .consEntries es z' =>
+    if h : 0 < es.size then
+      let z : Zipper α β := .consEntries (es.drop 1) z'
+      match es[0] with
+      | .null => .skip ⟨z⟩
+      | .entry k v => .yield ⟨z⟩ (k, v)
+      | .ref node => .skip ⟨z.prependNode node⟩
+    else
+      .skip ⟨z'⟩
+  | .consCollision keys vals hsz z' =>
+    if h : 0 < vals.size then
+      .yield ⟨.consCollision (keys.drop 1) (vals.drop 1) (by simp [*]) z'⟩ (keys[0], vals[0])
+    else
+      .skip ⟨z'⟩
+
+instance instIterator : Iterator (Zipper α β) Id (α × β) where
+  IsPlausibleStep it step := step = Zipper.step it
+  step it := return .deflate <| ⟨Zipper.step it, rfl⟩
+
+/-- Counts the total number of entries reachable from a node, including nested children. -/
+def Node.measure (node : Node α β) : Nat :=
+  match node with
+  | .entries es => measureEntries es 0
+  | .collision _ vals _ => vals.size
+termination_by (sizeOf node, 0)
+where
+  /-- Counts the total entries in an entries array starting at index `i`. -/
+  measureEntries (es : Array (Entry α β (Node α β))) (i : Nat) : Nat :=
+    if h : i < es.size then
+      (match h_eq : es[i] with
+       | .null => 1
+       | .entry _ _ => 1
+       | .ref node =>
+         have : sizeOf node < sizeOf es := by
+           have h1 := Array.sizeOf_get es i h
+           rw [h_eq] at h1
+           simp +arith at h1
+           omega
+         2 + Node.measure node) + measureEntries es (i + 1)
+    else 0
+  termination_by (sizeOf es, es.size - i)
+  decreasing_by all_goals simp_wf <;> omega
+
+def Entry.measure (entry : Entry α β (Node α β)) : Nat :=
+  match entry with
+  | .null => 1
+  | .entry _ _ => 1
+  | .ref node => 2 + node.measure
+
+/-- Counts entries remaining in a subarray, including nested children. -/
+def subarrayMeasure (es : Subarray (Entry α β (Node α β))) : Nat :=
+  es.toList.map (·.measure) |>.sum
+
+/-- Counts the total remaining work in a zipper, including entries nested in child nodes. -/
+def Zipper.measure : Zipper α β → Nat
+  | .done => 0
+  | .consEntries es z' => subarrayMeasure es + z'.measure + 1
+  | .consCollision _ vals _ z' => vals.size + z'.measure + 1
+
+private theorem subarrayMeasure_cons (es : Subarray (Entry α β (Node α β)))
+    (h : 0 < es.size) :
+    subarrayMeasure es = es[0].measure + subarrayMeasure (es.drop 1) := by
+  simp only [subarrayMeasure, Subarray.toList_drop]
+  have hlen : 0 < es.toList.length := by simpa [Subarray.length_toList] using h
+  conv => lhs; rw [show es.toList = List.drop 0 es.toList from List.drop_zero.symm]
+  rw [List.drop_eq_getElem_cons (by omega)]
+  simp [List.map_cons, List.sum_cons, Subarray.getElem_eq_getElem_toList]
+
+private theorem measureEntries_eq_list_sum (es : Array (Entry α β (Node α β))) (i : Nat) :
+    Node.measure.measureEntries es i =
+      ((es.toList.drop i).map Entry.measure).sum := by
+  unfold Node.measure.measureEntries
+  split
+  · rename_i h
+    rw [List.drop_eq_getElem_cons (by simpa using h)]
+    simp only [List.map_cons, List.sum_cons]
+    rw [measureEntries_eq_list_sum es (i + 1)]
+    congr 1
+    simp only [Array.getElem_toList]
+    cases es[i] <;> simp [Entry.measure]
+  · rename_i h
+    rw [List.drop_eq_nil_of_le (by simpa using h)]
+    simp
+  termination_by es.size - i
+
+private theorem subarrayMeasure_toSubarray_eq (nes : Array (Entry α β (Node α β))) :
+    subarrayMeasure nes.toSubarray = Node.measure (.entries nes) := by
+  simp only [subarrayMeasure, Node.measure]
+  have h1 : nes.toSubarray.toList = nes.toList := by
+    rw [Subarray.toList_eq_drop_take]
+    simp only [Array.size_eq_length_toList, Array.start_toSubarray, le_refl, Nat.min_eq_left,
+      Nat.zero_le, Array.stop_toSubarray, Array.array_toSubarray, List.take_length, List.drop_zero]
+  have h2 := measureEntries_eq_list_sum nes 0
+  simp only [List.drop_zero] at h2
+  rw [h1]
+  exact h2.symm
+
+private def instFinitenessRelation :
+    FinitenessRelation (Zipper α β) Id where
+  Rel t' t := t'.internalState.measure < t.internalState.measure
+  wf := InvImage.wf _ Nat.lt_wfRel.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator] at h'
+    subst h'
+    simp only [Zipper.step] at h
+    split at h
+    · -- .done: no successor
+      simp only [IterStep.successor_done] at h
+      exact nomatch h
+    · -- .consEntries es z'
+      rename_i es z' heq
+      split at h
+      · -- 0 < es.size
+        rename_i hsz
+        have h1 := subarrayMeasure_cons es hsz
+        match heq_es0 : es[0] with
+        | .null =>
+          simp only [heq_es0, IterStep.successor_skip, Option.some.injEq] at h; subst h
+          simp only [heq, Zipper.measure, heq_es0, Entry.measure] at h1 ⊢; omega
+        | .entry k v =>
+          simp only [heq_es0, IterStep.successor_yield, Option.some.injEq] at h; subst h
+          simp only [heq, Zipper.measure, heq_es0, Entry.measure] at h1 ⊢; omega
+        | .ref node =>
+          simp only [heq_es0, IterStep.successor_skip, Option.some.injEq] at h; subst h
+          simp only [heq_es0, Entry.measure] at h1
+          match heq_node : node with
+          | .entries nes =>
+            simp only [Zipper.prependNode, heq, Zipper.measure]
+            have h2 := subarrayMeasure_toSubarray_eq nes
+            omega
+          | .collision ks vs hsz' =>
+            simp only [Zipper.prependNode, heq, Zipper.measure, Array.size_mkSlice_rii]
+            simp only [Node.measure] at h1
+            omega
+      · -- ¬(0 < es.size) → skip to z'
+        simp only [IterStep.successor_skip, Option.some.injEq] at h; subst h
+        simp only [heq, Zipper.measure]; omega
+    · -- .consCollision keys vals hsz z'
+      rename_i keys vals hsz_eq z' heq
+      split at h
+      · -- 0 < vals.size → yield
+        simp only [IterStep.successor_yield, Option.some.injEq] at h; subst h
+        simp only [heq, Zipper.measure, Subarray.size_drop]; omega
+      · -- ¬(0 < vals.size) → skip
+        simp only [IterStep.successor_skip, Option.some.injEq] at h; subst h
+        simp only [heq, Zipper.measure]; omega
+
+instance instFinite : Finite (Zipper α β) Id :=
+  .of_finitenessRelation instFinitenessRelation
+
+@[always_inline, inline]
+instance instIteratorLoop {n : Type _ → Type _} [Monad n] :
+    IteratorLoop (Zipper α β) Id n :=
+  .defaultImplementation
+
+/--
+Returns a finite iterator over the key-value pairs of the given `PersistentHashMap`.
+The iteration order is unspecified.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
+@[inline]
+def iter [BEq α] [Hashable α] (map : PersistentHashMap α β) :
+    Iter (α := Zipper α β) (α × β) :=
+  ⟨Zipper.prependNode map.root .done⟩
+
+end Lean.PersistentHashMap

src/Lean/Data/Json/Parser.lean

@@ -141,7 +141,7 @@ def natMaybeZero : Parser Nat := do
 @[inline]
 def numSign : Parser Int := do
   let c ← peek!
-  let sign ← if c == '-' then
+  if c == '-' then
     skip
     return (-1 : Int)
   else

src/Lean/Data/KVMap.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Format.Syntax
 public import Init.Data.ToString.Name
+public import Init.Data.ToString.Extra
 
 public section
 

src/Lean/Data/Lsp/Capabilities.lean

@@ -69,6 +69,11 @@ structure LeanClientCapabilities where
   If `none` or `false`, silent diagnostics will not be served to the client.
   -/
   silentDiagnosticSupport? : Option Bool := none
+  /--
+  The latest RPC wire format supported by the client.
+  Defaults to `v0` when `none`.
+  -/
+  rpcWireFormat? : Option RpcWireFormat := none
   deriving ToJson, FromJson
 
 structure ClientCapabilities where
@@ -86,6 +91,13 @@ def ClientCapabilities.silentDiagnosticSupport (c : ClientCapabilities) : Bool :
     | return false
   return silentDiagnosticSupport
 
+def ClientCapabilities.rpcWireFormat (c : ClientCapabilities) : RpcWireFormat := Id.run do
+  let some lean := c.lean?
+    | return .v0
+  let some v := lean.rpcWireFormat?
+    | return .v0
+  return v
+
 structure LeanServerCapabilities where
   moduleHierarchyProvider? : Option ModuleHierarchyOptions
   rpcProvider? : Option RpcOptions