fix: squeeze simp and paren

.claude/CLAUDE.md

@@ -1,12 +1,7 @@
 (In the following, use `sysctl -n hw.logicalcpu` instead of `nproc` on macOS)
 
-## Building
-
 To build Lean you should use `make -j$(nproc) -C build/release`.
 
-The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
-Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
-
 ## Running Tests
 
 See `tests/README.md` for full documentation. Quick reference:
@@ -16,46 +11,18 @@ See `tests/README.md` for full documentation. Quick reference:
 CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test
 
-# Specific test by name (supports regex via ctest -R; double-quote special chars like |)
+# Specific test by name (supports regex via ctest -R)
 CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS="-R 'grind_ematch'"
-
-# Multiple tests matching a pattern
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS="-R 'treemap|phashmap'"
+make -C build/release -j "$(nproc)" test ARGS='-R grind_ematch'
 
 # Rerun only previously failed tests
 CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
 
-# Run a test manually without ctest (test pile: pass filename relative to the pile dir)
-tests/with_stage1_test_env.sh tests/elab_bench/run_bench.sh cbv_decide.lean
-tests/with_stage1_test_env.sh tests/elab/run_test.sh grind_indexmap.lean
+# Single test from tests/foo/bar/ (quick check during development)
+cd tests/foo/bar && ./run_test example_test.lean
 ```
 
-## Benchmark vs Test Problem Sizes
-
-Benchmarks are also run as tests. Use the `TEST_BENCH` environment variable (unset in tests, set to `1` in benchmarks) to scale problem sizes:
-
-- In `compile_bench` `.init.sh` files: check `$TEST_BENCH` and set `TEST_ARGS` accordingly
-- In `elab_bench` Lean files: use `(← IO.getEnv "TEST_BENCH") == some "1"` to switch between small (test) and large (bench) inputs
-
-See `tests/README.md` for the full benchmark writing guide.
-
-## 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/build-template.yml

@@ -33,7 +33,7 @@ jobs:
         include: ${{fromJson(inputs.config)}}
       # complete all jobs
       fail-fast: false
-    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-5gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-1gb"]', matrix.os)) || matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}
@@ -78,7 +78,7 @@ jobs:
       # (needs to be after "Install *" to use the right shell)
       - name: CI Merge Checkout
         run: |
-          git fetch --depth=${{ matrix.name == 'Linux Lake (Cached)' && '10' || '1' }} origin ${{ github.sha }}
+          git fetch --depth=1 origin ${{ github.sha }}
           git checkout FETCH_HEAD flake.nix flake.lock script/prepare-* tests/elab/importStructure.lean
         if: github.event_name == 'pull_request'
       # (needs to be after "Checkout" so files don't get overridden)
@@ -125,7 +125,7 @@ jobs:
           else
             echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
           fi
-      - name: Configure Build
+      - name: Build
         run: |
           ulimit -c unlimited  # coredumps
           [ -d build ] || mkdir build
@@ -162,21 +162,7 @@ jobs:
           fi
           # contortion to support empty OPTIONS with old macOS bash
           cmake .. --preset ${{ matrix.CMAKE_PRESET || 'release' }} -B . ${{ matrix.CMAKE_OPTIONS }} ${OPTIONS[@]+"${OPTIONS[@]}"} -DLEAN_INSTALL_PREFIX=$PWD/..
-      - name: Build Stage 0 & Configure Stage 1
-        run: |
-          ulimit -c unlimited  # coredumps
-          time make -C build stage1-configure -j$NPROC
-      - name: Download Lake Cache
-        if: matrix.name == 'Linux Lake (Cached)'
-        run: |
-          cd src
-          ../build/stage0/bin/lake cache get --repo=${{ github.repository }}
-        timeout-minutes: 20 # prevent excessive hanging from network issues
-        continue-on-error: true
-      - name: Build Target Stage
-        run: |
-          ulimit -c unlimited  # coredumps
-          time make -C build $TARGET_STAGE -j$NPROC
+          time make $TARGET_STAGE -j$NPROC
       # Should be done as early as possible and in particular *before* "Check rebootstrap" which
       # changes the state of stage1/
       - name: Save Cache
@@ -195,21 +181,6 @@ jobs:
             build/stage1/**/*.c
             build/stage1/**/*.c.o*' || '' }}
           key: ${{ steps.restore-cache.outputs.cache-primary-key }}
-      - name: Upload Lake Cache
-        # Caching on cancellation created some mysterious issues perhaps related to improper build
-        # shutdown. Also, since this needs access to secrets, it cannot be run on forks.
-        if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
-        run: |
-          curl --version
-          cd src
-          time ../build/stage0/bin/lake build -o ../build/lake-mappings.jsonl
-          time ../build/stage0/bin/lake cache put ../build/lake-mappings.jsonl --repo=${{ github.repository }}
-        env:
-          LAKE_CACHE_KEY: ${{ secrets.LAKE_CACHE_KEY }}
-          LAKE_CACHE_ARTIFACT_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/a1
-          LAKE_CACHE_REVISION_ENDPOINT: ${{ vars.LAKE_CACHE_ENDPOINT }}/r1
-        timeout-minutes: 20 # prevent excessive hanging from network issues
-        continue-on-error: true
       - name: Install
         run: |
           make -C build/$TARGET_STAGE install
@@ -276,10 +247,10 @@ jobs:
       - name: Check rebootstrap
         run: |
           set -e
-          git config user.email "stage0@lean-fro.org"
-          git config user.name "update-stage0"
+          # clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
+          # changes yet
           make -C build update-stage0
-          git commit --allow-empty -m "chore: update-stage0"
+          make -C build/stage1 clean-stdlib
           time make -C build -j$NPROC
           time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
         if: matrix.check-rebootstrap

.github/workflows/check-empty-pr.yml

@@ -1,29 +0,0 @@
-name: Check for empty PR
-
-on:
-  merge_group:
-  pull_request:
-
-jobs:
-  check-empty-pr:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v6
-      with:
-        ref: ${{ github.event_name == 'pull_request' && github.event.pull_request.head.sha || github.sha }}
-        fetch-depth: 0
-        filter: tree:0
-
-    - name: Check for empty diff
-      run: |
-        if [[ "${{ github.event_name }}" == "pull_request" ]]; then
-          base=$(git merge-base "origin/${{ github.base_ref }}" HEAD)
-        else
-          base=$(git rev-parse HEAD^1)
-        fi
-        if git diff --quiet "$base" HEAD --; then
-          echo "This PR introduces no changes compared to its base branch." | tee "$GITHUB_STEP_SUMMARY"
-          echo "It may be a duplicate of an already-merged PR." | tee -a "$GITHUB_STEP_SUMMARY"
-          exit 1
-        fi
-      shell: bash

.github/workflows/ci.yml

@@ -61,35 +61,20 @@ jobs:
             git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git
             git fetch nightly --tags
             if [[ '${{ github.event_name }}' == 'workflow_dispatch' ]]; then
-              # Manual re-release: retry today's nightly, or create a revision if it already exists
-              TODAY_NIGHTLY="nightly-$(date -u +%F)"
-              if git rev-parse "refs/tags/${TODAY_NIGHTLY}" >/dev/null 2>&1; then
-                # Today's nightly already exists, create a revision
-                REV=1
-                while git rev-parse "refs/tags/${TODAY_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
-                  REV=$((REV + 1))
-                done
-                LEAN_VERSION_STRING="${TODAY_NIGHTLY}-rev${REV}"
-              else
-                # Today's nightly doesn't exist yet (e.g. scheduled run failed), create it
-                LEAN_VERSION_STRING="${TODAY_NIGHTLY}"
-              fi
+              # Manual re-release: create a revision of the most recent nightly
+              BASE_NIGHTLY=$(git tag -l 'nightly-*' | sort -rV | head -1)
+              # Strip any existing -revK suffix to get the base date tag
+              BASE_NIGHTLY="${BASE_NIGHTLY%%-rev*}"
+              REV=1
+              while git rev-parse "refs/tags/${BASE_NIGHTLY}-rev${REV}" >/dev/null 2>&1; do
+                REV=$((REV + 1))
+              done
+              LEAN_VERSION_STRING="${BASE_NIGHTLY}-rev${REV}"
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
             else
-              # Scheduled: do nothing if commit already has a different tag (e.g. a release tag)
+              # Scheduled: do nothing if commit already has a different tag
               LEAN_VERSION_STRING="nightly-$(date -u +%F)"
-              HEAD_TAG="$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || true)"
-              if [[ -n "$HEAD_TAG" && "$HEAD_TAG" != "$LEAN_VERSION_STRING" ]]; then
-                echo "HEAD already tagged as ${HEAD_TAG}, skipping nightly"
-              elif git rev-parse "refs/tags/${LEAN_VERSION_STRING}" >/dev/null 2>&1; then
-                # Today's nightly already exists (e.g. from a manual release), create a revision
-                REV=1
-                while git rev-parse "refs/tags/${LEAN_VERSION_STRING}-rev${REV}" >/dev/null 2>&1; do
-                  REV=$((REV + 1))
-                done
-                LEAN_VERSION_STRING="${LEAN_VERSION_STRING}-rev${REV}"
-                echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
-              else
+              if [[ "$(git name-rev --name-only --tags --no-undefined HEAD 2> /dev/null || echo "$LEAN_VERSION_STRING")" == "$LEAN_VERSION_STRING" ]]; then
                 echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
               fi
             fi
@@ -181,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` or `lake-ci` label, full releases
+      # 3: PRs with `release-ci` label, full releases
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -190,7 +175,6 @@ 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
@@ -205,19 +189,13 @@ 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"
-            echo "fast=$fast"
-            echo "lake-ci=$lake_ci"
-          } >> "$GITHUB_OUTPUT"
+          echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
+          echo "fast=$fast" >> "$GITHUB_OUTPUT"
         env:
           GH_TOKEN: ${{ github.token }}
 
@@ -228,7 +206,6 @@ 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' }};
@@ -255,7 +232,7 @@ jobs:
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
                 // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large && fast ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "release": true,
                 // Special handling for release jobs. We want:
                 // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
@@ -276,7 +253,7 @@ jobs:
               },
               {
                 "name": "Linux Lake",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
                 "check-stage3": level >= 2,
@@ -284,19 +261,7 @@ jobs:
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
                 // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
-              },
-              {
-                "name": "Linux Lake (Cached)",
-                "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
-                "enabled": true,
-                "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
-                "test": true,
-                "secondary": true,
-                // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
-                "test-bench": large && level >= 2,
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror",
               },
               {
                 "name": "Linux Reldebug",
@@ -310,7 +275,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-24.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,
@@ -414,11 +379,6 @@ 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`, `lake-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
+# `release-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, 'lake-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, 'changelog-'))
     runs-on: ubuntu-latest
 
     steps:
@@ -28,7 +28,6 @@ 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) {
@@ -50,9 +49,6 @@ 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') || contains(github.event.label.name, 'lake-ci')
+    if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci')
     steps:
     - run: |
         # Finding latest CI workflow run on current pull request

CMakeLists.txt

@@ -79,7 +79,7 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   endif()
   find_program(LEANTAR leantar)
   if(NOT LEANTAR)
-    set(LEANTAR_VERSION v0.1.19)
+    set(LEANTAR_VERSION v0.1.18)
     if(CMAKE_SYSTEM_NAME MATCHES "Windows")
       set(LEANTAR_ARCHIVE_SUFFIX .zip)
       set(LEANTAR_TARGET x86_64-pc-windows-msvc)
@@ -114,7 +114,6 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
       )
     endif()
   endif()
-  list(APPEND STAGE0_ARGS -DLEANTAR=${LEANTAR})
   list(APPEND CL_ARGS -DCADICAL=${CADICAL} -DLEANTAR=${LEANTAR})
 endif()
 

CONTRIBUTING.md

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

doc/dev/index.md

@@ -1,9 +1,7 @@
 # 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](../../tests/README.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](testing.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

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

@@ -0,0 +1,11 @@
+#!/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

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

doc/examples/interp.lean.out.expected

@@ -1,4 +1,3 @@
 30
 interp.lean:146:4: warning: declaration uses `sorry`
-interp.lean:146:0: warning: declaration uses `sorry`
 3628800

doc/examples/run_test

@@ -0,0 +1,9 @@
+#!/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

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

flake.nix

@@ -67,5 +67,5 @@
         oldGlibc = devShellWithDist pkgsDist-old;
         oldGlibcAArch = devShellWithDist pkgsDist-old-aarch;
       };
-    }) ["x86_64-linux" "aarch64-linux" "aarch64-darwin"]);
+    }) ["x86_64-linux" "aarch64-linux"]);
 }

script/release_checklist.py

@@ -236,7 +236,7 @@ def parse_version(version_str):
 def is_version_gte(version1, version2):
     """Check if version1 >= version2, including proper handling of release candidates."""
     # Check if version1 is a nightly toolchain
-    if version1.startswith("leanprover/lean4:nightly-") or version1.startswith("leanprover/lean4-nightly:"):
+    if version1.startswith("leanprover/lean4:nightly-"):
         return False
     return parse_version(version1) >= parse_version(version2)
 

script/release_repos.yml

@@ -14,6 +14,13 @@ repositories:
     bump-branch: true
     dependencies: []
 
+  - name: lean4checker
+    url: https://github.com/leanprover/lean4checker
+    toolchain-tag: true
+    stable-branch: true
+    branch: master
+    dependencies: []
+
   - name: quote4
     url: https://github.com/leanprover-community/quote4
     toolchain-tag: true

script/release_steps.py

@@ -492,9 +492,8 @@ 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 | 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'
+            '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 "{}"\''
         )
         run_command(sync_script, cwd=repo_path)
         print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))

src/CMakeLists.txt

@@ -118,9 +118,6 @@ option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires
 set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
-# Temporary, core-only flags. Must be synced with stdlib_flags.h.
-string(APPEND LEAN_EXTRA_MAKE_OPTS " -Dbackward.do.legacy=false")
-
 if(LAZY_RC MATCHES "ON")
   set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
 endif()
@@ -762,7 +759,7 @@ if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
   add_dependencies(leancpp copy-cadical)
 endif()
 
-if(LEANTAR AND INSTALL_LEANTAR)
+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}"
@@ -797,7 +794,7 @@ if(LLVM AND STAGE GREATER 0)
   set(EXTRA_LEANMAKE_OPTS "LLVM=1")
 endif()
 
-set(STDLIBS Init Std Lean Leanc LeanIR)
+set(STDLIBS Init Std Lean Leanc)
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   list(APPEND STDLIBS Lake LeanChecker)
 endif()
@@ -904,16 +901,9 @@ if(PREV_STAGE)
   add_custom_target(update-stage0-commit COMMAND git commit -m "chore: update stage0" DEPENDS update-stage0)
 endif()
 
-if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
-  add_custom_target(leanir ALL
-    DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanir
-    VERBATIM)
-endif()
-
 # use Bash version for building, use Lean version in bin/ for tests & distribution
 configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/leanc.sh" @ONLY)
-if(STAGE GREATER 0 AND NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+if(STAGE GREATER 0 AND EXISTS "${LEAN_SOURCE_DIR}/Leanc.lean" AND NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   configure_file("${LEAN_SOURCE_DIR}/Leanc.lean" "${CMAKE_BINARY_DIR}/leanc/Leanc.lean" @ONLY)
   add_custom_target(
     leanc
@@ -933,7 +923,7 @@ if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
   install(PROGRAMS "${CADICAL}" DESTINATION bin)
 endif()
 
-if(LEANTAR AND INSTALL_LEANTAR)
+if(STAGE GREATER 0 AND LEANTAR AND INSTALL_LEANTAR)
   install(PROGRAMS "${LEANTAR}" DESTINATION bin)
 endif()
 
@@ -952,7 +942,6 @@ install(
   PATTERN "*.hash" EXCLUDE
   PATTERN "*.trace" EXCLUDE
   PATTERN "*.rsp" EXCLUDE
-  PATTERN "*.filelist" EXCLUDE
 )
 
 # symlink source into expected installation location for go-to-definition, if file system allows it

src/Init.lean

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

@@ -1,71 +0,0 @@
-/-
-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/ExceptCps.lean

@@ -37,7 +37,7 @@ set_option linter.unusedVariables false in  -- `s` unused
 Use a monadic action that may throw an exception by providing explicit success and failure
 continuations.
 -/
-@[always_inline, inline, expose]
+@[always_inline, inline]
 def runK {ε α : Type u} (x : ExceptCpsT ε m α) (s : ε) (ok : α → m β) (error : ε → m β) : m β :=
   x _ ok error
 
@@ -83,8 +83,6 @@ of `True`.
 -/
 instance : MonadAttach (ExceptCpsT ε m) := .trivial
 
-@[simp] theorem throw_bind [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : (throw e >>= f : ExceptCpsT ε m β) = throw e := rfl
-
 @[simp] theorem run_pure [Monad m] : run (pure x : ExceptCpsT ε m α) = pure (Except.ok x) := rfl
 
 @[simp] theorem run_lift {α ε : Type u} [Monad m] (x : m α) : run (ExceptCpsT.lift x : ExceptCpsT ε m α) = (x >>= fun a => pure (Except.ok a) : m (Except ε α)) := rfl
@@ -93,20 +91,7 @@ instance : MonadAttach (ExceptCpsT ε m) := .trivial
 
 @[simp] theorem run_bind_lift [Monad m] (x : m α) (f : α → ExceptCpsT ε m β) : run (ExceptCpsT.lift x >>= f : ExceptCpsT ε m β) = x >>= fun a => run (f a) := rfl
 
-@[deprecated throw_bind (since := "2026-03-13")]
-theorem run_bind_throw [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : run (throw e >>= f : ExceptCpsT ε m β) = run (throw e) := rfl
-
-@[simp] theorem runK_pure :
-    runK (pure x : ExceptCpsT ε m α) s ok error = ok x := rfl
-
-@[simp] theorem runK_lift {α ε : Type u} [Monad m] (x : m α) (s : ε) (ok : α → m β) (error : ε → m β) :
-    runK (ExceptCpsT.lift x : ExceptCpsT ε m α) s ok error = x >>= ok := rfl
-
-@[simp] theorem runK_throw [Monad m] :
-    runK (throw e : ExceptCpsT ε m β) s ok error = error e := rfl
-
-@[simp] theorem runK_bind_lift [Monad m] (x : m α) (f : α → ExceptCpsT ε m β) :
-    runK (ExceptCpsT.lift x >>= f : ExceptCpsT ε m β) s ok error = x >>= fun a => runK (f a) s ok error := rfl
+@[simp] theorem run_bind_throw [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : run (throw e >>= f : ExceptCpsT ε m β) = run (throw e) := rfl
 
 @[simp] theorem runCatch_pure [Monad m] : runCatch (pure x : ExceptCpsT α m α) = pure x := rfl
 
@@ -117,7 +102,6 @@ theorem run_bind_throw [Monad m] (e : ε) (f : α → ExceptCpsT ε m β) : run
 
 @[simp] theorem runCatch_bind_lift [Monad m] (x : m α) (f : α → ExceptCpsT β m β) : runCatch (ExceptCpsT.lift x >>= f : ExceptCpsT β m β) = x >>= fun a => runCatch (f a) := rfl
 
-@[deprecated throw_bind (since := "2026-03-13")]
-theorem runCatch_bind_throw [Monad m] (e : β) (f : α → ExceptCpsT β m β) : runCatch (throw e >>= f : ExceptCpsT β m β) = pure e := rfl
+@[simp] theorem runCatch_bind_throw [Monad m] (e : β) (f : α → ExceptCpsT β m β) : runCatch (throw e >>= f : ExceptCpsT β m β) = pure e := rfl
 
 end ExceptCpsT

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 : 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_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
+@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
 
 end Id

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

@@ -72,11 +72,11 @@ public instance [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m]
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
+  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT _ _))
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
     LawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
+  inferInstanceAs (LawfulMonadAttach (ReaderT _ _))
 
 section
 

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

@@ -103,11 +103,11 @@ namespace StateRefT'
 instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where
   monadLift_pure _ := by
     simp only [MonadLift.monadLift, pure]
-    unfold StateRefT'.lift instMonad._aux_5 ReaderT.pure
+    unfold StateRefT'.lift ReaderT.pure
     simp only
   monadLift_bind _ _ := by
     simp only [MonadLift.monadLift, bind]
-    unfold StateRefT'.lift instMonad._aux_13 ReaderT.bind
+    unfold StateRefT'.lift ReaderT.bind
     simp only
 
 end StateRefT'

src/Init/Conv.lean

@@ -60,6 +60,9 @@ with functions defined via well-founded recursion or partial fixpoints.
 The proofs produced by `cbv` only use the three standard axioms.
 In particular, they do not require trust in the correctness of the code
 generator.
+
+This tactic is experimental and its behavior is likely to change in upcoming
+releases of Lean.
 -/
 syntax (name := cbv) "cbv" : conv
 

src/Init/Core.lean

@@ -172,8 +172,6 @@ instance thunkCoe : CoeTail α (Thunk α) where
   -- Since coercions are expanded eagerly, `a` is evaluated lazily.
   coe a := ⟨fun _ => a⟩
 
-instance [Inhabited α] : Inhabited (Thunk α) := ⟨.pure default⟩
-
 /-- A variation on `Eq.ndrec` with the equality argument first. -/
 abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
   Eq.ndrec m h

src/Init/Data/Array/Attach.lean

@@ -98,7 +98,7 @@ well-founded recursion mechanism to prove that the function terminates.
 
 @[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
     pmap f (xs.push a) h =
-      (pmap f xs (fun a m => by simp [forall_or_eq_imp] at h; exact h.1 _ m)).push (f a (h a (by simp))) := by
+      (pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
   simp [pmap]
 
 @[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
@@ -153,7 +153,7 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
 
 @[simp] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
-      (xs.attachWith P (fun x h => by simp [forall_or_eq_imp] at H; exact H.1 _ h)).push ⟨a, H a (by simp)⟩ := by
+      (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   cases xs
   simp
 

src/Init/Data/Array/Basic.lean

@@ -559,9 +559,9 @@ def modifyOp (xs : Array α) (idx : Nat) (f : α → α) : Array α :=
   xs.modify idx f
 
 /--
-  We claim this unsafe implementation is correct because an array cannot have more than `USize.size` elements in our runtime.
+  We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime.
 
-  This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < USize.size` to true. -/
+  This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/
 @[inline] unsafe def forIn'Unsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
   let sz := as.usize
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
@@ -2151,4 +2151,7 @@ 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/Find.lean

@@ -622,12 +622,12 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp; rfl
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp
+  simp; rfl
 
 -- We can't mark this as a `@[congr]` lemma since the head of the RHS is not `findFinIdx?`.
 theorem findFinIdx?_congr {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
@@ -801,7 +801,7 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?]
 
-@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
+@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp; rfl
 
 @[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by

src/Init/Data/Array/MinMax.lean

@@ -113,7 +113,7 @@ public theorem _root_.List.min?_toArray [Min α] {l : List α} :
   · simp [List.min_toArray, List.min_eq_get_min?, - List.get_min?]
   · simp_all
 
-@[simp, grind =, cbv_eval ←]
+@[simp, grind =]
 public theorem min?_toList [Min α] {xs : Array α} :
     xs.toList.min? = xs.min? := by
   cases xs; simp
@@ -153,7 +153,7 @@ public theorem _root_.List.max?_toArray [Max α] {l : List α} :
   · simp [List.max_toArray, List.max_eq_get_max?, - List.get_max?]
   · simp_all
 
-@[simp, grind =, cbv_eval ←]
+@[simp, grind =]
 public theorem max?_toList [Max α] {xs : Array α} :
     xs.toList.max? = xs.max? := by
   cases xs; simp

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

@@ -134,7 +134,6 @@ theorem Array.toList_mergeSort {xs : Array α} {le : α → α → Bool} :
     (xs.mergeSort le).toList = xs.toList.mergeSort le := by
   rw [Array.mergeSort, Subarray.toList_mergeSort, Array.toList_mkSlice_rii]
 
-@[cbv_eval]
 theorem Array.mergeSort_eq_toArray_mergeSort_toList {xs : Array α} {le : α → α → Bool} :
     xs.mergeSort le = (xs.toList.mergeSort le).toArray := by
   simp [← toList_mergeSort]

src/Init/Data/BEq.lean

@@ -36,8 +36,6 @@ theorem BEq.symm [BEq α] [Std.Symm (α := α) (· == ·)] {a b : α} : a == b
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
-theorem bne_eq [BEq α] {a b : α} : (a != b) = !(a == b) := rfl
-
 theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by
   rw [bne, BEq.comm, bne]
 
@@ -66,8 +64,3 @@ theorem BEq.neq_of_beq_of_neq [BEq α] [PartialEquivBEq α] {a b c : α} :
 instance (priority := low) [BEq α] [LawfulBEq α] : EquivBEq α where
   symm h := beq_iff_eq.2 <| Eq.symm <| beq_iff_eq.1 h
   trans hab hbc := beq_iff_eq.2 <| (beq_iff_eq.1 hab).trans <| beq_iff_eq.1 hbc
-
-theorem equivBEq_of_iff_apply_eq [BEq α] (f : α → β) (hf : ∀ a b, a == b ↔ f a = f b) : EquivBEq α where
-  rfl := by simp [hf]
-  symm := by simp [hf, eq_comm]
-  trans hab hbc := (hf _ _).2 (Eq.trans ((hf _ _).1 hab) ((hf _ _).1 hbc))

src/Init/Data/Bool.lean

@@ -664,6 +664,3 @@ but may be used locally.
 
 @[simp] theorem Bool.not'_eq_not (a : Bool) : a.not' = a.not := by
   cases a <;> simp [Bool.not']
-
-theorem Bool.rec_eq {α : Sort _} (b : Bool) {x y : α} : Bool.rec y x b = if b then x else y := by
-  cases b <;> simp

src/Init/Data/ByteArray/Basic.lean

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

src/Init/Data/Char/Lemmas.lean

@@ -86,20 +86,4 @@ theorem toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8 := rfl
 @[simp]
 theorem toString_eq_singleton {c : Char} : c.toString = String.singleton c := rfl
 
-@[simp]
-theorem toNat_val {c : Char} : c.val.toNat = c.toNat := rfl
-
-theorem val_inj {c d : Char} : c.val = d.val ↔ c = d :=
-  Char.ext_iff.symm
-
-theorem toNat_inj {c d : Char} : c.toNat = d.toNat ↔ c = d := by
-  simp [← toNat_val, ← val_inj, ← UInt32.toNat_inj]
-
-theorem isDigit_iff_toNat {c : Char} : c.isDigit ↔ '0'.toNat ≤ c.toNat ∧ c.toNat ≤ '9'.toNat := by
-  simp [isDigit, UInt32.le_iff_toNat_le]
-
-@[simp]
-theorem toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
-  simp [← toNat_val]
-
 end Char

src/Init/Data/Char/Ordinal.lean

@@ -217,7 +217,7 @@ theorem succ?_eq {c : Char} : c.succ? = (c.ordinal.addNat? 1).map Char.ofOrdinal
           Nat.reduceLeDiff, UInt32.left_eq_add]
         grind [UInt32.lt_iff_toNat_lt]
       · grind
-    · simp [coe_ordinal, -toNat_val]
+    · simp [coe_ordinal]
       grind [UInt32.lt_iff_toNat_lt]
   | case2 =>
     rw [Fin.addNat?_eq_some]

src/Init/Data/Fin/Lemmas.lean

@@ -527,14 +527,6 @@ theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.ca
 
 @[simp, grind =] theorem val_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
-/-
-**Note**
-The current pattern inference heuristic includes the implicit term `n + m` as pattern of the pattern,
-but arithmetic is problematic in patterns because it is an interpreted symbol. For example,
-we will fail to match `@val n (castNat 0 i)`. Thus, we mark the implicit subterm with `no_index`
--/
-grind_pattern val_castAdd => @val (no_index _) (castAdd m i)
-
 @[deprecated val_castAdd (since := "2025-11-21")]
 theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
@@ -645,15 +637,7 @@ theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i)
 
 theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := rfl
 
-@[simp] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
-
-/-
-**Note**
-The current pattern inference heuristic includes the implicit term `n + m` as pattern of the pattern,
-but arithmetic is problematic in patterns because it is an interpreted symbol. For example,
-we will fail to match `@val n (addNat i 0)`. Thus, we mark the implicit subterm with `no_index`
--/
-grind_pattern val_addNat => @val (no_index _) (addNat i m)
+@[simp, grind =] theorem val_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
 
 @[deprecated val_addNat (since := "2025-11-21")]
 theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl

src/Init/Data/FloatArray/Basic.lean

@@ -9,7 +9,6 @@ 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.lean

@@ -18,4 +18,3 @@ public import Init.Data.Int.Pow
 public import Init.Data.Int.Cooper
 public import Init.Data.Int.Linear
 public import Init.Data.Int.OfNat
-public import Init.Data.Int.ToString

src/Init/Data/Int/Pow.lean

@@ -118,19 +118,16 @@ 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_nonneg (m : Int) : 0 ≤ m ^ 2 := by
+protected theorem sq_nonnneg (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_nonneg m
+  exact Int.sq_nonnneg 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/Int/Repr.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2016 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.Repr
-public import Init.Data.String.Defs
-
-namespace Int
-
-/--
-Returns the decimal string representation of an integer.
--/
-public protected def repr : Int → String
-  | ofNat m   => Nat.repr m
-  | negSucc m => "-" ++ Nat.repr (Nat.succ m)
-
-public instance : Repr Int where
-  reprPrec i prec := if i < 0 then Repr.addAppParen i.repr prec else i.repr
-
-end Int

src/Init/Data/Int/ToString.lean

@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Julia Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.ToString.Extra
-import all Init.Data.Int.Repr
-import Init.Data.Int.Order
-import Init.Data.Int.LemmasAux
-
-namespace Int
-
-public theorem repr_eq_if {a : Int} :
-    a.repr = if 0 ≤ a then a.toNat.repr else "-" ++ (-a).toNat.repr := by
-  cases a <;> simp [Int.repr]
-
-@[simp]
-public theorem toString_eq_repr {a : Int} : toString a = a.repr := (rfl)
-
-end Int

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

@@ -37,7 +37,7 @@ The standard library does not provide a `Productive` instance for this case.
 
 This combinator incurs an additional O(1) cost with each output of `it₁` and `it₂`.
 -/
-@[cbv_opaque, inline, expose]
+@[inline, expose]
 def Iter.append {α₁ : Type w} {α₂ : Type w} {β : Type w}
     [Iterator α₁ Id β] [Iterator α₂ Id β]
     (it₁ : Iter (α := α₁) β) (it₂ : Iter (α := α₂) β) :

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

@@ -13,7 +13,7 @@ public section
 namespace Std
 open Std.Iterators
 
-@[cbv_opaque, always_inline, inline, expose, inherit_doc IterM.attachWith]
+@[always_inline, inline, expose, inherit_doc IterM.attachWith]
 def Iter.attachWith {α β : Type w}
     [Iterator α Id β]
     (it : Iter (α := α) β) (P : β → Prop) (h : ∀ out, it.IsPlausibleIndirectOutput out → P out) :

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

@@ -282,17 +282,17 @@ def Iter.mapM {α β γ : Type w} [Iterator α Id β] {m : Type w → Type w'}
     [Monad m] [MonadAttach m] (f : β → m γ) (it : Iter (α := α) β) :=
   (letI : MonadLift Id m := ⟨pure⟩; it.toIterM.mapM f : IterM m γ)
 
-@[cbv_opaque, always_inline, inline, inherit_doc IterM.filterMap, expose]
+@[always_inline, inline, inherit_doc IterM.filterMap, expose]
 def Iter.filterMap {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     (f : β → Option γ) (it : Iter (α := α) β) :=
   ((it.toIterM.filterMap f).toIter : Iter γ)
 
-@[cbv_opaque, always_inline, inline, inherit_doc IterM.filter, expose]
+@[always_inline, inline, inherit_doc IterM.filter, expose]
 def Iter.filter {α : Type w} {β : Type w} [Iterator α Id β]
     (f : β → Bool) (it : Iter (α := α) β) :=
   ((it.toIterM.filter f).toIter : Iter β)
 
-@[cbv_opaque, always_inline, inline, inherit_doc IterM.map, expose]
+@[always_inline, inline, inherit_doc IterM.map, expose]
 def Iter.map {α : Type w} {β : Type w} {γ : Type w} [Iterator α Id β]
     (f : β → γ) (it : Iter (α := α) β) :=
   ((it.toIterM.map f).toIter : Iter γ)

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

@@ -44,7 +44,7 @@ public def Iter.flatMapAfter {α : Type w} {β : Type w} {α₂ : Type w}
     (f : β → Iter (α := α₂) γ) (it₁ : Iter (α := α) β) (it₂ : Option (Iter (α := α₂) γ)) :=
   ((it₁.toIterM.flatMapAfter (fun b => (f b).toIterM) (Iter.toIterM <$> it₂)).toIter : Iter γ)
 
-@[cbv_opaque, always_inline, expose, inherit_doc IterM.flatMap]
+@[always_inline, expose, inherit_doc IterM.flatMap]
 public def Iter.flatMap {α : Type w} {β : Type w} {α₂ : Type w}
     {γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     (f : β → Iter (α := α₂) γ) (it : Iter (α := α) β) :=

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

@@ -168,13 +168,6 @@ instance Map.instIterator {α β γ : Type w} {m : Type w → Type w'} {n : Type
     Iterator (Map α m n lift f) n γ :=
   inferInstanceAs <| Iterator (FilterMap α m n lift _) n γ
 
-theorem Map.instIterator_eq_filterMapInstIterator {α β γ : Type w} {m : Type w → Type w'}
-    {n : Type w → Type w''} [Monad n]
-    [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} :
-    Map.instIterator (α := α) (β := β) (γ := γ) (m := m) (n := n) (lift := lift) (f := f) =
-      FilterMap.instIterator :=
-  rfl
-
 private def FilterMap.instFinitenessRelation {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] :

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

@@ -36,7 +36,7 @@ it.take 3   ---a--⊥
 
 This combinator incurs an additional O(1) cost with each output of `it`.
 -/
-@[cbv_opaque, always_inline, inline]
+@[always_inline, inline]
 def Iter.take {α : Type w} {β : Type w} [Iterator α Id β] (n : Nat) (it : Iter (α := α) β) :
     Iter (α := Take α Id) β :=
   it.toIterM.take n |>.toIter

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

@@ -44,7 +44,7 @@ it.uLift n    ---.up a----.up b---.up c--.up d---⊥
 * `Finite`: only if the original iterator is finite
 * `Productive`: only if the original iterator is productive
 -/
-@[cbv_opaque, always_inline, inline, expose]
+@[always_inline, inline, expose]
 def Iter.uLift (it : Iter (α := α) β) :
     Iter (α := Types.ULiftIterator.{v} α Id Id β (fun _ => monadLift)) (ULift β) :=
   (it.toIterM.uLift Id).toIter

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

@@ -32,7 +32,7 @@ Traverses the given iterator and stores the emitted values in an array.
 If the iterator is not finite, this function might run forever. The variant
 `it.ensureTermination.toArray` always terminates after finitely many steps.
 -/
-@[cbv_opaque, always_inline, inline]
+@[always_inline, inline]
 def Iter.toArray {α : Type w} {β : Type w}
     [Iterator α Id β] (it : Iter (α := α) β) : Array β :=
   it.toIterM.toArray.run
@@ -66,7 +66,7 @@ lists are prepend-only, this `toListRev` is usually more efficient that `toList`
 If the iterator is not finite, this function might run forever. The variant
 `it.ensureTermination.toListRev` always terminates after finitely many steps.
 -/
-@[always_inline, inline, cbv_opaque]
+@[always_inline, inline]
 def Iter.toListRev {α : Type w} {β : Type w}
     [Iterator α Id β] (it : Iter (α := α) β) : List β :=
   it.toIterM.toListRev.run
@@ -101,7 +101,7 @@ lists are prepend-only, `toListRev` is usually more efficient that `toList`.
 If the iterator is not finite, this function might run forever. The variant
 `it.ensureTermination.toList` always terminates after finitely many steps.
 -/
-@[cbv_opaque, always_inline, inline]
+@[always_inline, inline]
 def Iter.toList {α : Type w} {β : Type w}
     [Iterator α Id β] (it : Iter (α := α) β) : List β :=
   it.toIterM.toList.run

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

@@ -226,7 +226,7 @@ any element emitted by the iterator {name}`it`.
 {lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
 examined in order of iteration.
 -/
-@[inline, cbv_opaque]
+@[inline]
 def Iter.any {α β : Type w}
     [Iterator α Id β] [IteratorLoop α Id Id]
     (p : β → Bool) (it : Iter (α := α) β) : Bool :=
@@ -292,7 +292,7 @@ all element emitted by the iterator {name}`it`.
 {lit}`O(|xs|)`. Short-circuits upon encountering the first match. The elements in {name}`it` are
 examined in order of iteration.
 -/
-@[inline, cbv_opaque]
+@[inline]
 def Iter.all {α β : Type w}
     [Iterator α Id β] [IteratorLoop α Id Id]
     (p : β → Bool) (it : Iter (α := α) β) : Bool :=
@@ -644,7 +644,7 @@ Examples:
 * `[7, 6].iter.first? = some 7`
 * `[].iter.first? = none`
 -/
-@[inline, cbv_opaque]
+@[inline]
 def Iter.first? {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     (it : Iter (α := α) β) : Option β :=
   it.toIterM.first?.run

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

@@ -56,7 +56,7 @@ theorem Iter.Intermediate.step_appendSnd {α₁ α₂ β : Type w}
   simp only [Iter.step, appendSnd, toIterM_toIter, IterM.Intermediate.step_appendSnd, Id.run_bind]
   cases it₂.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toList_append {α₁ α₂ β : Type w}
     [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
     {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :
@@ -70,7 +70,7 @@ theorem Iter.toListRev_append {α₁ α₂ β : Type w}
     (it₁.append it₂).toListRev = it₂.toListRev ++ it₁.toListRev := by
   simp [append_eq_toIter_append_toIterM, toListRev_eq_toListRev_toIterM]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toArray_append {α₁ α₂ β : Type w}
     [Iterator α₁ Id β] [Iterator α₂ Id β] [Finite α₁ Id] [Finite α₂ Id]
     {it₁ : Iter (α := α₁) β} {it₂ : Iter (α := α₂) β} :

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

@@ -34,7 +34,7 @@ theorem Iter.unattach_toList_attachWith [Iterator α Id β]
     ← Id.run_map (f := List.unattach), IterM.map_unattach_toList_attachWith,
     Iter.toList_eq_toList_toIterM]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toList_attachWith [Iterator α Id β]
     {it : Iter (α := α) β} {hP}
     [Finite α Id] :
@@ -68,7 +68,7 @@ theorem Iter.unattach_toArray_attachWith [Iterator α Id β]
     (it.attachWith P hP).toListRev.unattach = it.toListRev := by
   simp [toListRev_eq]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toArray_attachWith [Iterator α Id β]
     {it : Iter (α := α) β} {hP}
     [Finite α Id] :

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

@@ -297,7 +297,7 @@ def Iter.val_step_filter {f : β → Bool} :
   · simp
   · simp
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toList_filterMap [Finite α Id]
     {f : β → Option γ} :
     (it.filterMap f).toList = it.toList.filterMap f := by
@@ -315,12 +315,12 @@ theorem Iter.toList_mapM [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawful
     (it.mapM f).toList = it.toList.mapM f := by
   simp [Iter.mapM_eq_toIter_mapM_toIterM, IterM.toList_mapM, Iter.toList_eq_toList_toIterM]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toList_map [Finite α Id] {f : β → γ} :
     (it.map f).toList = it.toList.map f := by
   simp [map_eq_toIter_map_toIterM, IterM.toList_map, Iter.toList_eq_toList_toIterM]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toList_filter [Finite α Id] {f : β → Bool} :
     (it.filter f).toList = it.toList.filter f := by
   simp [filter_eq_toIter_filter_toIterM, IterM.toList_filter, Iter.toList_eq_toList_toIterM]
@@ -369,7 +369,7 @@ theorem Iter.toListRev_filter [Finite α Id]
     (it.filter f).toListRev = it.toListRev.filter f := by
   simp [filter_eq_toIter_filter_toIterM, IterM.toListRev_filter, Iter.toListRev_eq_toListRev_toIterM]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toArray_filterMap [Finite α Id]
     {f : β → Option γ} :
     (it.filterMap f).toArray = it.toArray.filterMap f := by
@@ -387,13 +387,13 @@ theorem Iter.toArray_mapM [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfu
     (it.mapM f).toArray = it.toArray.mapM f := by
   simp [Iter.mapM_eq_toIter_mapM_toIterM, IterM.toArray_mapM, Iter.toArray_eq_toArray_toIterM]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toArray_map [Finite α Id] {f : β → γ} :
     (it.map f).toArray = it.toArray.map f := by
   simp [map_eq_toIter_map_toIterM, IterM.toArray_map, Iter.toArray_eq_toArray_toIterM]
 
-@[cbv_eval, simp]
-theorem Iter.toArray_filter [Finite α Id] {f : β → Bool} :
+@[simp]
+theorem Iter.toArray_filter[Finite α Id] {f : β → Bool} :
     (it.filter f).toArray = it.toArray.filter f := by
   simp [filter_eq_toIter_filter_toIterM, IterM.toArray_filter, Iter.toArray_eq_toArray_toIterM]
 
@@ -435,9 +435,8 @@ theorem Iter.forIn_filterMapWithPostcondition
         match ← (f out).run with
         | some c => g c acc
         | none => return .yield acc) := by
-  simp only [filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition, forIn_eq_forIn_toIterM]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
-  rfl -- expressions are equal up to different matchers
+  simp +instances [Iter.forIn_eq_forIn_toIterM, filterMapWithPostcondition, IterM.forIn_filterMapWithPostcondition,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
 
 theorem Iter.forIn_filterMapM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -449,9 +448,8 @@ theorem Iter.forIn_filterMapM
         match ← f out with
         | some c => g c acc
         | none => return .yield acc) := by
-  simp [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
-  rfl
+  simp +instances [filterMapM, forIn_eq_forIn_toIterM, IterM.forIn_filterMapM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
 
 theorem Iter.forIn_filterMap
     [Monad n] [LawfulMonad n] [Finite α Id]
@@ -471,8 +469,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 only [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp +instances [mapWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_mapWithPostcondition,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_mapM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -500,8 +498,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 only [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp +instances [filterWithPostcondition, forIn_eq_forIn_toIterM, IterM.forIn_filterWithPostcondition,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_filterM
     [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -510,8 +508,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 only [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp +instances [filterM, forIn_eq_forIn_toIterM, IterM.forIn_filterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.forIn_filter
     [Monad n] [LawfulMonad n]
@@ -552,9 +550,8 @@ 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 only [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
-  rfl
+  simp +instances [filterMapM, IterM.foldM_filterMapM, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]; rfl
 
 theorem Iter.foldM_mapWithPostcondition {α β γ δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -566,8 +563,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 only [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp +instances [mapWithPostcondition, IterM.foldM_mapWithPostcondition, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_mapM {α β γ δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -581,8 +578,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 only [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp +instances [mapM, IterM.foldM_mapM, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_filterWithPostcondition {α β δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -594,8 +591,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 only [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp +instances [filterWithPostcondition, IterM.foldM_filterWithPostcondition, foldM_eq_foldM_toIterM,
+    instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
 
 theorem Iter.foldM_filterM {α β δ : Type w}
     {n : Type w → Type w''} {o : Type w → Type w'''}
@@ -608,8 +605,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 only [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM]
-  rw [instMonadLiftTOfMonadLift_instMonadLiftTOfPure]
+  simp +instances [filterM, IterM.foldM_filterM, foldM_eq_foldM_toIterM,
+    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

@@ -232,6 +232,7 @@ 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 (α := α₂) γ)} :
@@ -240,9 +241,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]
-  unfold Iter.toList
-  cases it₂ <;> simp [map]
+  cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_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 (α := α₂) γ)} :
@@ -251,10 +252,8 @@ 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]
 
-@[cbv_eval]
 public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id]
@@ -262,7 +261,6 @@ public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β]
     (it₁.flatMap f).toList = (it₁.map fun b => (f b).toList).toList.flatten := by
   simp [flatMap, toList_flatMapAfter]
 
-@[cbv_eval]
 public theorem Iter.toArray_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id]

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

@@ -374,6 +374,7 @@ 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,
@@ -394,7 +395,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 := ⟨LawfulMonadLiftT.monadLift_pure, LawfulMonadLiftT.monadLift_bind⟩
+  haveI : LawfulMonadLift n o := ⟨by simp +instances [this], by simp +instances [this]⟩
   rw [toList_eq_match_step, toList_eq_match_step, step_filterMapWithPostcondition,
     bind_assoc, step_filterMapWithPostcondition, step_filterMapWithPostcondition]
   simp only [bind_assoc, liftM_bind]
@@ -601,6 +602,7 @@ 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]
@@ -624,6 +626,7 @@ 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]
@@ -644,25 +647,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 only [toList_filterMapM_eq_toList_filterMapWithPostcondition,
-    toList_filterMapWithPostcondition, PostconditionT.run_eq_map]
-  simp [PostconditionT.attachLift, WeaklyLawfulMonadAttach.map_attach]
+  simp [toList_filterMapM_eq_toList_filterMapWithPostcondition, toList_filterMapWithPostcondition,
+    PostconditionT.attachLift, PostconditionT.run_eq_map, 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 only [toList_mapM_eq_toList_mapWithPostcondition, toList_mapWithPostcondition,
-    PostconditionT.run_eq_map]
-  simp [PostconditionT.attachLift, WeaklyLawfulMonadAttach.map_attach]
+  simp [toList_mapM_eq_toList_mapWithPostcondition, toList_mapWithPostcondition,
+    PostconditionT.attachLift, PostconditionT.run_eq_map, WeaklyLawfulMonadAttach.map_attach]
 
 @[simp]
 theorem IterM.toList_filterMap {α β γ : Type w} {m : Type w → Type w'}
@@ -699,16 +702,18 @@ theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m]
     (it : IterM (α := α) m β) :
     (it.map f).toList = (fun x => x.map f) <$> it.toList := by
   rw [← List.filterMap_eq_map, ← toList_filterMap]
-  simp only [map, mapWithPostcondition, InternalCombinators.map, filterMap,
-    filterMapWithPostcondition, InternalCombinators.filterMap]
-  unfold Map
+  let t := type_of% (it.map f)
+  let t' := type_of% (it.filterMap (some ∘ f))
   congr
-  · simp
-  · rw [Map.instIterator_eq_filterMapInstIterator]
+  · simp [Map]
+  · simp [Map.instIterator, inferInstanceAs]
     congr
     simp
-  · simp
-  · simp
+  · simp only [map, mapWithPostcondition, InternalCombinators.map, Function.comp_apply, filterMap,
+    filterMapWithPostcondition, InternalCombinators.filterMap]
+    congr
+    · simp [Map]
+    · simp
 
 @[simp]
 theorem IterM.toList_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
@@ -1298,6 +1303,7 @@ 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]
@@ -1308,10 +1314,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
-  unfold mapWithPostcondition InternalCombinators.map Map.instIteratorLoop Map
-  rw [Map.instIterator_eq_filterMapInstIterator]
-  rw [← InternalCombinators.filterMap, ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
-  simp
+  rw [mapWithPostcondition, InternalCombinators.map, ← InternalCombinators.filterMap,
+    ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
+  simp [PostconditionT.run_eq_map]
 
 theorem IterM.forIn_mapM
     [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
@@ -1475,7 +1480,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
+  cases fx.down <;> simp [PostconditionT.run_eq_map]
 
 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/Take.lean

@@ -67,7 +67,7 @@ theorem Iter.atIdxSlow?_take {α β}
     simp only [atIdxSlow?_eq_match (it := it.take k), step_take, h']
     cases k <;> cases l <;> simp
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toList_take_of_finite {α β} [Iterator α Id β] {n : Nat}
     [Finite α Id] {it : Iter (α := α) β} :
     (it.take n).toList = it.toList.take n := by
@@ -89,7 +89,7 @@ theorem Iter.toListRev_take_of_finite {α β} [Iterator α Id β] {n : Nat}
     (it.take n).toListRev = it.toListRev.drop (it.toList.length - n) := by
   rw [toListRev_eq, toList_take_of_finite, List.reverse_take, toListRev_eq]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toArray_take_of_finite {α β} [Iterator α Id β] {n : Nat}
     [Finite α Id] {it : Iter (α := α) β} :
     (it.take n).toArray = it.toArray.take n := by

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

@@ -38,7 +38,7 @@ theorem Iter.step_uLift [Iterator α Id β] {it : Iter (α := α) β} :
     PlausibleIterStep.done, pure_bind]
   cases it.toIterM.step.run.inflate using PlausibleIterStep.casesOn <;> simp
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toList_uLift [Iterator α Id β] {it : Iter (α := α) β}
     [Finite α Id] :
     it.uLift.toList = it.toList.map ULift.up := by
@@ -52,7 +52,7 @@ theorem Iter.toListRev_uLift [Iterator α Id β] {it : Iter (α := α) β}
     it.uLift.toListRev = it.toListRev.map ULift.up := by
   rw [toListRev_eq, toListRev_eq, toList_uLift, List.map_reverse]
 
-@[cbv_eval, simp]
+@[simp]
 theorem Iter.toArray_uLift [Iterator α Id β] {it : Iter (α := α) β}
     [Finite α Id] :
     it.uLift.toArray = it.toArray.map ULift.up := by

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

@@ -88,7 +88,7 @@ theorem Iter.toList_toArray_ensureTermination {α β} [Iterator α Id β] [Finit
     it.ensureTermination.toArray.toList = it.toList := by
   simp
 
-@[cbv_eval ←, simp]
+@[simp]
 theorem Iter.toArray_toList {α β} [Iterator α Id β] [Finite α Id]
     {it : Iter (α := α) β} :
     it.toList.toArray = it.toArray := by
@@ -110,7 +110,6 @@ theorem Iter.reverse_toListRev_ensureTermination [Iterator α Id β] [Finite α
     it.ensureTermination.toListRev.reverse = it.toList := by
   simp
 
-@[cbv_eval]
 theorem Iter.toListRev_eq {α β} [Iterator α Id β] [Finite α Id]
     {it : Iter (α := α) β} :
     it.toListRev = it.toList.reverse := by

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

@@ -32,12 +32,11 @@ 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 only [ForIn'.forIn']
+  simp +instances 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 only [IteratorLoop.forIn, Functor.map_map, id_map',
-    bind_pure_comp]
+  simp +instances [IteratorLoop.defaultImplementation]
 
 theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id]
     {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
@@ -82,7 +81,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 [ForIn'.forIn', monadLift]
+  simp +instances [ForIn'.forIn', monadLift]
 
 theorem Iter.forIn_eq_forIn_toIterM {α β : Type w} [Iterator α Id β]
     [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m]
@@ -449,7 +448,7 @@ theorem Iter.toArray_eq_fold {α β : Type w} [Iterator α Id β]
   rw [← fold_hom (List.toArray)]
   simp
 
-@[cbv_eval ←, simp]
+@[simp]
 theorem Iter.foldl_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
     [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {f : γ → β → γ} {init : γ} {it : Iter (α := α) β} :
@@ -637,7 +636,6 @@ theorem Iter.any_eq_forIn {α β : Type w} [Iterator α Id β]
           return .yield false)).run := by
   simp [any_eq_anyM, anyM_eq_forIn]
 
-@[cbv_eval ←]
 theorem Iter.any_toList {α β : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} {p : β → Bool} :
@@ -728,7 +726,6 @@ theorem Iter.all_eq_forIn {α β : Type w} [Iterator α Id β]
           return .done false)).run := by
   simp [all_eq_allM, allM_eq_forIn]
 
-@[cbv_eval ←]
 theorem Iter.all_toList {α β : Type w} [Iterator α Id β]
     [Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id]
     {it : Iter (α := α) β} {p : β → Bool} :
@@ -956,7 +953,7 @@ theorem Iter.first?_eq_match_step {α β : Type w} [Iterator α Id β] [Iterator
   generalize it.toIterM.step.run.inflate = s
   rcases s with ⟨_|_|_, _⟩ <;> simp [Iter.first?_eq_first?_toIterM]
 
-@[simp, grind =, cbv_eval ←]
+@[simp, grind =]
 theorem Iter.head?_toList {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id]
     [Finite α Id] [LawfulIteratorLoop α Id Id] {it : Iter (α := α) β} :
     it.toList.head? = it.first? := by

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 only [ForIn'.forIn']
+  simp +instances 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 [IteratorLoop.forIn]
+  simp +instances [IteratorLoop.defaultImplementation]
   try rfl
 
 theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]

src/Init/Data/Iterators/Lemmas/Producers/List.lean

@@ -33,12 +33,12 @@ theorem List.step_iter_cons {x : β} {xs : List β} :
     ((x :: xs).iter).step = ⟨.yield xs.iter x, rfl⟩ := by
   simp [List.iter, List.iterM, IterM.toIter, Iter.step_eq]
 
-@[cbv_eval, simp, grind =]
+@[simp, grind =]
 theorem List.toArray_iter {l : List β} :
     l.iter.toArray = l.toArray := by
   simp [List.iter, List.toArray_iterM, Iter.toArray_eq_toArray_toIterM]
 
-@[cbv_eval, simp, grind =]
+@[simp, grind =]
 theorem List.toList_iter {l : List β} :
     l.iter.toList = l := by
   simp [List.iter, List.toList_iterM]

src/Init/Data/Iterators/PostconditionMonad.lean

@@ -272,12 +272,6 @@ 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/Iterators/Producers/List.lean

@@ -29,7 +29,7 @@ The monadic version of this iterator is `List.iterM`.
 * `Finite` instance: always
 * `Productive` instance: always
 -/
-@[cbv_opaque, always_inline, inline]
+@[always_inline, inline]
 def List.iter {α : Type w} (l : List α) :
     Iter (α := ListIterator α) α :=
   ((l.iterM Id).toIter : Iter α)

src/Init/Data/Iterators/Producers/Monadic/List.lean

@@ -46,7 +46,7 @@ The non-monadic version of this iterator is `List.iter`.
 * `Finite` instance: always
 * `Productive` instance: always
 -/
-@[cbv_opaque, always_inline, inline]
+@[always_inline, inline]
 def _root_.List.iterM {α : Type w} (l : List α) (m : Type w → Type w') [Pure m] :
     IterM (α := ListIterator α) m α :=
   ⟨{ list := l }⟩

src/Init/Data/List/Basic.lean

@@ -1246,24 +1246,6 @@ def IsInfix (l₁ : List α) (l₂ : List α) : Prop := Exists fun s => Exists f
 /-- not `isInfix` -/
 recommended_spelling "infix" for "<:+:" in [IsInfix, «term_<:+:_»]
 
-/--
-Checks whether the first list is a contiguous sub-list of the second.
-
-The relation `List.IsInfixOf` expresses this property with respect to logical equality.
-
-Examples:
- * `[2, 3].isInfixOf_internal [1, 2, 3, 4] = true`
- * `[2, 3].isInfixOf_internal [1, 3, 2, 4] = false`
- * `[2, 3].isInfixOf_internal [2, 3] = true`
- * `[2, 3].isInfixOf_internal [1] = false`
-
-  Used internally by the `cbv` tactic.
--/
-def isInfixOf_internal [BEq α] (l₁ l₂ : List α) : Bool :=
-  l₁.isPrefixOf l₂ || match l₂ with
-    | []      => false
-    | _ :: l₂ => isInfixOf_internal l₁ l₂
-
 /-! ### splitAt -/
 
 /--

src/Init/Data/List/Find.lean

@@ -1050,7 +1050,7 @@ theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} :
 
 @[simp, grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     [a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp [findFinIdx?_cons, findFinIdx?_nil]
+  simp [findFinIdx?_cons, findFinIdx?_nil]; rfl
 
 @[simp, grind =] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
     l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by

src/Init/Data/List/Lemmas.lean

@@ -877,11 +877,6 @@ theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
 theorem getLast?_cons {a : α} : (a::l).getLast? = some (l.getLast?.getD a) := by
   cases l <;> simp [getLast?, getLast]
 
-theorem getLast?_cons_of_ne_nil {x : α} {xs : List α} (h : xs ≠ []) : (x::xs).getLast? = xs.getLast? := by
-  cases xs with
-  | nil => contradiction
-  | cons => simp [getLast?_cons]
-
 @[simp] theorem getLast?_cons_cons : (a :: b :: l).getLast? = (b :: l).getLast? := by
   simp [getLast?_cons]
 
@@ -1288,13 +1283,6 @@ theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a := by
     cases h : p a <;> simp [*]
     intro h; exact Nat.lt_irrefl _ (h ▸ length_filter_le p l)
 
-theorem filter_bne_eq_self_of_not_mem [BEq α] [LawfulBEq α] {a : α} {l : List α} (h : a ∉ l) :
-    l.filter (· != a) = l := by
-  rw [List.filter_eq_self]
-  intro c hc
-  simp only [bne_iff_ne, ne_eq]
-  exact fun heq => absurd (heq ▸ hc) h
-
 @[simp]
 theorem length_filter_eq_length_iff {l} : (filter p l).length = l.length ↔ ∀ a ∈ l, p a := by
   induction l with
@@ -1348,16 +1336,6 @@ theorem foldl_filter {p : α → Bool} {f : β → α → β} {l : List α} {ini
     simp only [filter_cons, foldl_cons]
     split <;> simp [ih]
 
-theorem foldl_ite_left {P : α → Prop} [DecidablePred P] {l : List α} {f : β → α → β} {init : β} :
-    (l.foldl (init := init) fun sofar a => if P a then f sofar a else sofar) = (l.filter P).foldl (init := init) f := by
-  simp [List.foldl_filter]
-
-theorem foldl_ite_right {P : α → Prop} [DecidablePred P] {l : List α} {f : β → α → β} {init : β} :
-    (l.foldl (init := init) fun sofar a => if P a then sofar else f sofar a) =
-      (l.filter (fun a => ¬ P a)).foldl (init := init) f := by
-  simp +singlePass only [← ite_not]
-  rw [foldl_ite_left]
-
 theorem foldr_filter {p : α → Bool} {f : α → β → β} {l : List α} {init : β} :
     (l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init := by
   induction l generalizing init with

src/Init/Data/List/MinMaxIdx.lean

@@ -481,13 +481,13 @@ protected theorem maxIdxOn_nil_eq_iff_false [LE β] [DecidableLE β] {f : α →
 @[simp]
 protected theorem maxIdxOn_singleton [LE β] [DecidableLE β] {x : α} {f : α → β} :
     [x].maxIdxOn f (of_decide_eq_false rfl) = 0 :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minIdxOn_singleton
 
 @[simp]
 protected theorem maxIdxOn_lt_length [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxIdxOn f h < xs.length :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minIdxOn_lt_length h
 
 protected theorem maxIdxOn_le_of_apply_getElem_le_apply_maxOn [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -495,7 +495,7 @@ protected theorem maxIdxOn_le_of_apply_getElem_le_apply_maxOn [LE β] [Decidable
     {k : Nat} (hi : k < xs.length) (hle : f (xs.maxOn f h) ≤ f xs[k]) :
     xs.maxIdxOn f h ≤ k := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn] at hle ⊢
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minIdxOn_le_of_apply_getElem_le_apply_minOn h hi (by simpa [LE.le_opposite_iff] using hle)
 
 protected theorem apply_maxOn_lt_apply_getElem_of_lt_maxIdxOn [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β]
@@ -513,7 +513,7 @@ protected theorem getElem_maxIdxOn [LE β] [DecidableLE β] [IsLinearPreorder β
     {f : α → β} {xs : List α} (h : xs ≠ []) :
     xs[xs.maxIdxOn f h] = xs.maxOn f h := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.getElem_minIdxOn h
 
 protected theorem le_maxIdxOn_of_apply_getElem_lt_apply_getElem [LE β] [DecidableLE β] [LT β]
@@ -562,14 +562,14 @@ protected theorem maxIdxOn_cons
       else if f (xs.maxOn f h) ≤ f x then 0
       else (xs.maxIdxOn f h) + 1 := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_cons (f := f)
 
 protected theorem maxIdxOn_eq_zero_iff [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} (h : xs ≠ []) :
     xs.maxIdxOn f h = 0 ↔ ∀ x ∈ xs, f x ≤ f (xs.head h) := by
   simp only [List.maxIdxOn_eq_minIdxOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_eq_zero_iff h (f := f)
 
 protected theorem maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -580,26 +580,26 @@ protected theorem maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
       else
         xs.length + ys.maxIdxOn f hys := by
   simp only [List.maxIdxOn_eq_minIdxOn, List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minIdxOn_append hxs hys (f := f)
 
 protected theorem left_le_maxIdxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs ys : List α} {f : α → β} (h : xs ≠ []) :
     xs.maxIdxOn f h ≤ (xs ++ ys).maxIdxOn f (by simp [h]) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.left_le_minIdxOn_append h
 
 protected theorem maxIdxOn_take_le [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {i : Nat} (h : xs.take i ≠ []) :
     (xs.take i).maxIdxOn f h ≤ xs.maxIdxOn f (List.ne_nil_of_take_ne_nil h) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minIdxOn_take_le h
 
 @[simp]
 protected theorem maxIdxOn_replicate [LE β] [DecidableLE β] [Refl (α := β) (· ≤ ·)]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :
     (replicate n a).maxIdxOn f h = 0 :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minIdxOn_replicate h
 
 @[simp]

src/Init/Data/List/MinMaxOn.lean

@@ -297,13 +297,13 @@ protected theorem maxOn_cons
     (x :: xs).maxOn f (by exact of_decide_eq_false rfl) =
       if h : xs = [] then x else maxOn f x (xs.maxOn f h) := by
   simp only [maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn_cons (f := f)
 
 protected theorem maxOn_cons_cons [LE β] [DecidableLE β] {a b : α} {l : List α} {f : α → β} :
     (a :: b :: l).maxOn f (by simp) = (maxOn f a b :: l).maxOn f (by simp) := by
   simp only [List.maxOn_eq_minOn, maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn_cons_cons
 
 @[simp]
@@ -334,51 +334,51 @@ protected theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLea
     {xs : List α} (h : xs ≠ []) :
     xs.maxOn id h = xs.max h := by
   simp only [List.maxOn_eq_minOn]
-  letI : LE α := (inferInstance : LE α).opposite
-  letI : Min α := (inferInstance : Max α).oppositeMin
+  letI : LE α := (inferInstanceAs (LE α)).opposite
+  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
   simpa only [List.max_eq_min] using List.minOn_id h
 
 @[simp]
 protected theorem maxOn_mem [LE β] [DecidableLE β] {xs : List α}
     {f : α → β} {h : xs ≠ []} : xs.maxOn f h ∈ xs :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn_mem (f := f)
 
 protected theorem le_apply_maxOn_of_mem [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) :
     f y ≤ f (xs.maxOn f (List.ne_nil_of_mem hx)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_of_mem (f := f) hx
 
 protected theorem apply_maxOn_le_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) {b : β} :
     f (xs.maxOn f h) ≤ b ↔ ∀ x ∈ xs, f x ≤ b := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.le_apply_minOn_iff (f := f) h
 
 protected theorem le_apply_maxOn_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) {b : β} :
     b ≤ f (xs.maxOn f h) ↔ ∃ x ∈ xs, b ≤ f x := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_iff (f := f) h
 
 protected theorem apply_maxOn_lt_iff
      [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β] [LawfulOrderLT β]
     {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} :
     f (xs.maxOn f h) < b ↔ ∀ x ∈ xs, f x < b := by
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : LT β := (inferInstance : LT β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LT β := (inferInstanceAs (LT β)).opposite
   simpa [LT.lt_opposite_iff] using List.lt_apply_minOn_iff (f := f) h
 
 protected theorem lt_apply_maxOn_iff
      [LE β] [DecidableLE β] [LT β] [IsLinearPreorder β] [LawfulOrderLT β]
     {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} :
     b < f (xs.maxOn f h) ↔ ∃ x ∈ xs, b < f x := by
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : LT β := (inferInstance : LT β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LT β := (inferInstanceAs (LT β)).opposite
   simpa [LT.lt_opposite_iff] using List.apply_minOn_lt_iff (f := f) h
 
 protected theorem apply_maxOn_le_apply_maxOn_of_subset [LE β] [DecidableLE β]
@@ -386,14 +386,14 @@ protected theorem apply_maxOn_le_apply_maxOn_of_subset [LE β] [DecidableLE β]
     haveI : xs ≠ [] := by intro h; rw [h] at hxs; simp_all [subset_nil]
     f (ys.maxOn f hys) ≤ f (xs.maxOn f this) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_le_apply_minOn_of_subset (f := f) hxs hys
 
 protected theorem apply_maxOn_take_le [LE β] [DecidableLE β] [IsLinearPreorder β]
     {xs : List α} {f : α → β} {i : Nat} (h : xs.take i ≠ []) :
     f ((xs.take i).maxOn f h) ≤ f (xs.maxOn f (List.ne_nil_of_take_ne_nil h)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.le_apply_minOn_take (f := f) h
 
 protected theorem le_apply_maxOn_append_left [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -401,7 +401,7 @@ protected theorem le_apply_maxOn_append_left [LE β] [DecidableLE β] [IsLinearP
     f (xs.maxOn f h) ≤
       f ((xs ++ ys).maxOn f (append_ne_nil_of_left_ne_nil h ys)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_append_le_left (f := f) h
 
 protected theorem le_apply_maxOn_append_right [LE β] [DecidableLE β] [IsLinearPreorder β]
@@ -409,7 +409,7 @@ protected theorem le_apply_maxOn_append_right [LE β] [DecidableLE β] [IsLinear
     f (ys.maxOn f h) ≤
       f ((xs ++ ys).maxOn f (append_ne_nil_of_right_ne_nil xs h)) := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_minOn_append_le_right (f := f) h
 
 @[simp]
@@ -417,21 +417,21 @@ protected theorem maxOn_append [LE β] [DecidableLE β] [IsLinearPreorder β] {x
     {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) :
     (xs ++ ys).maxOn f (by simp [hxs]) = maxOn f (xs.maxOn f hxs) (ys.maxOn f hys) := by
   simp only [List.maxOn_eq_minOn, maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minOn_append (f := f) hxs hys
 
 protected theorem maxOn_eq_head [LE β] [DecidableLE β] [IsLinearPreorder β] {xs : List α}
     {f : α → β} (h : xs ≠ []) (h' : ∀ x ∈ xs, f x ≤ f (xs.head h)) :
     xs.maxOn f h = xs.head h := by
   rw [List.maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.minOn_eq_head (f := f) h (by simpa [LE.le_opposite_iff] using h')
 
 protected theorem max_map
     [LE β] [DecidableLE β] [Max β] [IsLinearPreorder β] [LawfulOrderLeftLeaningMax β] {xs : List α}
     {f : α → β} (h : xs ≠ []) : (xs.map f).max (by simpa) = f (xs.maxOn f h) := by
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : Min β := (inferInstance : Max β).oppositeMin
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
   simpa [List.max_eq_min] using List.min_map (f := f) h
 
 protected theorem maxOn_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
@@ -458,7 +458,7 @@ protected theorem max_map_eq_max [Max α] [LE α] [DecidableLE α] [LawfulOrderL
 protected theorem maxOn_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) :
     (replicate n a).maxOn f h = a :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn_replicate (f := f) h
 
 /-! # minOn? -/
@@ -579,7 +579,7 @@ protected theorem maxOn?_nil [LE β] [DecidableLE β] {f : α → β} :
 protected theorem maxOn?_cons_eq_some_maxOn
     [LE β] [DecidableLE β] {f : α → β} {x : α} {xs : List α} :
     (x :: xs).maxOn? f = some ((x :: xs).maxOn f (fun h => nomatch h)) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_cons_eq_some_minOn
 
 protected theorem maxOn?_cons
@@ -588,7 +588,7 @@ protected theorem maxOn?_cons
   have : maxOn f x = (letI : LE β := LE.opposite inferInstance; minOn f x) := by
     ext; simp only [maxOn_eq_minOn]
   simp only [List.maxOn?_eq_minOn?, this]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn?_cons
 
 @[simp]
@@ -599,8 +599,8 @@ protected theorem maxOn?_singleton [LE β] [DecidableLE β] {x : α} {f : α →
 @[simp]
 protected theorem maxOn?_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α]
     {xs : List α} : xs.maxOn? id = xs.max? := by
-  letI : LE α := (inferInstance : LE α).opposite
-  letI : Min α := (inferInstance : Max α).oppositeMin
+  letI : LE α := (inferInstanceAs (LE α)).opposite
+  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
   simpa only [List.maxOn?_eq_minOn?, List.max?_eq_min?] using List.minOn?_id (α := α)
 
 protected theorem maxOn?_eq_if
@@ -610,7 +610,7 @@ protected theorem maxOn?_eq_if
       some (xs.maxOn f h)
     else
       none :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_eq_if
 
 @[simp]
@@ -620,55 +620,55 @@ protected theorem isSome_maxOn?_iff [LE β] [DecidableLE β] {f : α → β} {xs
 
 protected theorem maxOn_eq_get_maxOn? [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxOn f h = (xs.maxOn? f).get (List.isSome_maxOn?_iff.mpr h) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn_eq_get_minOn? (f := f) h
 
 protected theorem maxOn?_eq_some_maxOn [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : xs.maxOn? f = some (xs.maxOn f h) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_eq_some_minOn (f := f) h
 
 @[simp]
 protected theorem get_maxOn? [LE β] [DecidableLE β] {f : α → β} {xs : List α}
     (h : xs ≠ []) : (xs.maxOn? f).get (List.isSome_maxOn?_iff.mpr h) = xs.maxOn f h :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.get_minOn? (f := f) h
 
 protected theorem maxOn_eq_of_maxOn?_eq_some
     [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : xs.maxOn? f = some x) :
     xs.maxOn f (List.isSome_maxOn?_iff.mp (Option.isSome_of_eq_some h)) = x :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn_eq_of_minOn?_eq_some (f := f) h
 
 protected theorem isSome_maxOn?_of_mem
     [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     (xs.maxOn? f).isSome :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.isSome_minOn?_of_mem (f := f) h
 
 protected theorem le_apply_get_maxOn?_of_mem
     [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) :
     f x ≤ f ((xs.maxOn? f).get (List.isSome_maxOn?_of_mem h)) := by
   simp only [List.maxOn?_eq_minOn?]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa [LE.le_opposite_iff] using List.apply_get_minOn?_le_of_mem (f := f) h
 
 protected theorem maxOn?_mem [LE β] [DecidableLE β] {xs : List α}
     {f : α → β} (h : xs.maxOn? f = some a) : a ∈ xs :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_mem (f := f) h
 
 protected theorem maxOn?_replicate [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} :
     (replicate n a).maxOn? f = if n = 0 then none else some a :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_replicate
 
 @[simp]
 protected theorem maxOn?_replicate_of_pos [LE β] [DecidableLE β] [IsLinearPreorder β]
     {n : Nat} {a : α} {f : α → β} (h : 0 < n) :
     (replicate n a).maxOn? f = some a :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   List.minOn?_replicate_of_pos (f := f) h
 
 @[simp]
@@ -678,7 +678,7 @@ protected theorem maxOn?_append [LE β] [DecidableLE β] [IsLinearPreorder β]
   have : maxOn f = (letI : LE β := LE.opposite inferInstance; minOn f) := by
     ext; simp only [maxOn_eq_minOn]
   simp only [List.maxOn?_eq_minOn?, this]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   exact List.minOn?_append xs ys f
 
 end List

src/Init/Data/List/Nat/TakeDrop.lean

@@ -311,7 +311,7 @@ theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
   | nil =>
     cases h rfl
   | cons y l ih =>
-    simp only [drop]
+    simp only [drop, length]
     by_cases h₁ : l = []
     · simp [h₁]
     rw [getLast_cons h₁]

src/Init/Data/List/Sort/Impl.lean

@@ -182,6 +182,7 @@ private theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α
     simp only [mergeSortTR.run, mergeSortTR.run, mergeSort]
     rw [merge_eq_mergeTR]
     rw [mergeSortTR_run_eq_mergeSort, mergeSortTR_run_eq_mergeSort]
+    rfl
 
 -- We don't make this a `@[csimp]` lemma because `mergeSort_eq_mergeSortTR₂` is faster.
 theorem mergeSort_eq_mergeSortTR : @mergeSort = @mergeSortTR := by

src/Init/Data/List/Sublist.lean

@@ -706,11 +706,6 @@ theorem infix_refl (l : List α) : l <:+: l := prefix_rfl.isInfix
 
 grind_pattern suffix_cons => _ <:+ a :: l
 
-@[simp]
-theorem suffix_cons_append {a : α} {l₁ l₂ : List α} : l₂ <:+ a :: (l₁ ++ l₂) := by
-  rw [← List.cons_append]
-  exact List.suffix_append (a :: l₁) l₂
-
 theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨l₁', l₂', h⟩ => ⟨a :: l₁', l₂', h ▸ rfl⟩
 
 theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨l₁', l₂', h⟩ =>
@@ -1297,31 +1292,6 @@ instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+: l₂) :=
 instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+ l₂) :=
   decidable_of_iff (l₁.isSuffixOf l₂) isSuffixOf_iff_suffix
 
-/-
-  Used internally by the `cbv` tactic.
--/
-theorem isInfixOf_internal_iff_isInfix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
-    l₁.isInfixOf_internal l₂ ↔ l₁ <:+: l₂ := by
-  induction l₂ with
-  | nil => simp [isInfixOf_internal, IsInfix]
-  | cons a l₂ ih =>
-    simp only [isInfixOf_internal, Bool.or_eq_true]
-    constructor
-    · rintro (h | h)
-      · exact (isPrefixOf_iff_prefix.mp h).isInfix
-      · exact infix_cons <| ih.mp h
-    · intro ⟨s, t, h⟩
-      match s with
-      | [] => left; exact isPrefixOf_iff_prefix.mpr ⟨t, h⟩
-      | a' :: s' =>
-        right; exact ih.mpr ⟨s', t, List.cons.inj h |>.2⟩
-
-/-
-  Used internally by the `cbv` tactic.
--/
-instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <:+: l₂) :=
-  decidable_of_iff (l₁.isInfixOf_internal l₂) isInfixOf_internal_iff_isInfix
-
 theorem prefix_iff_eq_append : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
   ⟨by rintro ⟨r, rfl⟩; rw [drop_left], fun e => ⟨_, e⟩⟩
 
@@ -1329,121 +1299,6 @@ theorem prefix_iff_eq_take : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ :=
   ⟨fun h => append_cancel_right <| (prefix_iff_eq_append.1 h).trans (take_append_drop _ _).symm,
     fun e => e.symm ▸ take_prefix _ _⟩
 
-theorem prefix_iff_exists_append_eq {l₁ l₂ : List α} : l₁ <+: l₂ ↔ ∃ l₃, l₁ ++ l₃ = l₂ :=
-  Iff.rfl
-
-theorem prefix_iff_exists_eq_append {l₁ l₂ : List α} : l₁ <+: l₂ ↔ ∃ l₃, l₂ = l₁ ++ l₃ := by
-  simp [prefix_iff_exists_append_eq, eq_comm]
-
 -- See `Init.Data.List.Nat.Sublist` for `suffix_iff_eq_append`, `prefix_take_iff`, and `suffix_iff_eq_drop`.
 
-theorem suffix_iff_exists_append_eq {l₁ l₂ : List α} : l₁ <:+ l₂ ↔ ∃ l₃, l₃ ++ l₁ = l₂ :=
-  Iff.rfl
-
-theorem suffix_iff_exists_eq_append {l₁ l₂ : List α} : l₁ <:+ l₂ ↔ ∃ l₃, l₂ = l₃ ++ l₁ := by
-  simp [suffix_iff_exists_append_eq, eq_comm]
-
-theorem suffix_append_self_iff {l₁ l₂ l₃ : List α} : l₁ ++ l₃ <:+ l₂ ++ l₃ ↔ l₁ <:+ l₂ := by
-  constructor
-  · rintro ⟨t, h⟩
-    exact ⟨t, List.append_cancel_right (by rwa [← List.append_assoc] at h)⟩
-  · rintro ⟨t, h⟩
-    exact ⟨t, by rw [← List.append_assoc, h]⟩
-
-theorem prefix_self_append_iff {l₁ l₂ l₃ : List α} : l₃ ++ l₁ <+: l₃ ++ l₂ ↔ l₁ <+: l₂ := by
-  constructor
-  · rintro ⟨t, h⟩
-    exact ⟨t, List.append_cancel_left (by rwa [List.append_assoc] at h)⟩
-  · rintro ⟨t, h⟩
-    exact ⟨t, by rw [List.append_assoc, h]⟩
-
-theorem suffix_append_inj_of_length_eq {l₁ l₂ s₁ s₂ : List α} (hs : s₁.length = s₂.length) :
-    l₁ ++ s₁ <:+ l₂ ++ s₂ ↔ l₁ <:+ l₂ ∧ s₁ = s₂ := by
-  simp only [suffix_iff_exists_eq_append]
-  refine ⟨?_, ?_⟩
-  · rintro ⟨l₃, h⟩
-    rw [← List.append_assoc] at h
-    obtain ⟨rfl, rfl⟩ := List.append_inj' h hs.symm
-    refine ⟨⟨l₃, by simp⟩, by simp⟩
-  · rintro ⟨⟨l₃, rfl⟩, rfl⟩
-    refine ⟨l₃, by simp⟩
-
-theorem prefix_append_inj_of_length_eq {l₁ l₂ s₁ s₂ : List α} (hs : s₁.length = s₂.length) :
-    s₁ ++ l₁ <+: s₂ ++ l₂ ↔ s₁ = s₂ ∧ l₁ <+: l₂ := by
-  constructor
-  · rintro ⟨t, h⟩
-    rw [List.append_assoc] at h
-    obtain ⟨rfl, rfl⟩ := List.append_inj h.symm hs.symm
-    exact ⟨rfl, ⟨t, rfl⟩⟩
-  · rintro ⟨rfl, t, rfl⟩
-    exact ⟨t, by simp⟩
-
-theorem singleton_suffix_iff_getLast?_eq_some {a : α} {l : List α} : [a] <:+ l ↔ l.getLast? = some a := by
-  rw [suffix_iff_exists_eq_append, getLast?_eq_some_iff]
-
-theorem singleton_prefix_iff_head?_eq_some {a : α} {l : List α} : [a] <+: l ↔ l.head? = some a := by
-  simp [prefix_iff_exists_eq_append, head?_eq_some_iff]
-
-theorem singleton_prefix_cons_iff {a b : α} {l : List α} : [a] <+: b :: l ↔ a = b := by
-  simp
-
-@[simp]
-theorem singleton_suffix_append_singleton_iff {a b : α} {l : List α} :
-    [a] <:+ l ++ [b] ↔ a = b := by
-  refine ⟨fun h => Eq.symm ?_, by rintro rfl; simp⟩
-  simpa [List.suffix_iff_exists_eq_append] using h
-
-@[simp]
-theorem singleton_suffix_cons_append_singleton_iff {a b c : α} {l : List α} :
-    [a] <:+ b :: (l ++ [c]) ↔ a = c := by
-  rw [← List.cons_append]
-  exact singleton_suffix_append_singleton_iff
-
-theorem infix_append_iff {α : Type u} {l xs ys : List α} : l <:+: xs ++ ys ↔
-    l <:+: xs ∨ l <:+: ys ∨ (∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <:+ xs ∧ l₂ <+: ys) := by
-  constructor
-  · rintro ⟨s, t, ht⟩
-    rcases List.append_eq_append_iff.mp ht with ⟨as, hxs, _⟩ | ⟨bs, hsl, hys⟩
-    · exact Or.inl ⟨s, as, hxs.symm⟩
-    · rcases List.append_eq_append_iff.mp hsl with ⟨cs, hxs', hl⟩ | ⟨ds, _, hbs⟩
-      · exact Or.inr (Or.inr ⟨cs, bs, hl,
-          List.suffix_iff_exists_eq_append.mpr ⟨s, hxs'⟩,
-          List.prefix_iff_exists_eq_append.mpr ⟨t, hys⟩⟩)
-      · exact Or.inr (Or.inl ⟨ds, t, by rw [hys, ← hbs]⟩)
-  · rintro (⟨s, t, ht⟩ | ⟨s, t, ht⟩ | ⟨l₁, l₂, rfl, hl₁, hl₂⟩)
-    · exact ⟨s, t ++ ys, by rw [← List.append_assoc, ht]⟩
-    · exact ⟨xs ++ s, t, by
-        rw [List.append_assoc] at ht
-        rw [List.append_assoc (xs ++ s), List.append_assoc xs, ht]⟩
-    · rw [List.suffix_iff_exists_eq_append] at hl₁
-      rw [List.prefix_iff_exists_eq_append] at hl₂
-      obtain ⟨s, hxs⟩ := hl₁
-      obtain ⟨t, hys⟩ := hl₂
-      exact ⟨s, t, by rw [← List.append_assoc s l₁, List.append_assoc (s ++ l₁), hxs, hys]⟩
-
-theorem infix_append_iff_ne_nil {α : Type u} {l xs ys : List α} : l <:+: xs ++ ys ↔
-    l <:+: xs ∨ l <:+: ys ∨ (∃ l₁ l₂, l₁ ≠ [] ∧ l₂ ≠ [] ∧ l = l₁ ++ l₂ ∧ l₁ <:+ xs ∧ l₂ <+: ys) := by
-  rw [List.infix_append_iff]
-  constructor
-  · rintro (h | h | ⟨l₁, l₂, hl, hl₁, hl₂⟩)
-    · exact Or.inl h
-    · exact Or.inr (Or.inl h)
-    · cases l₁ with
-      | nil =>
-        simp only [List.nil_append] at hl
-        subst hl
-        exact Or.inr (Or.inl hl₂.isInfix)
-      | cons hd tl =>
-        cases l₂ with
-        | nil =>
-          simp only [List.append_nil] at hl
-          subst hl
-          exact Or.inl hl₁.isInfix
-        | cons hd' tl' =>
-          exact Or.inr (Or.inr ⟨_, _, List.cons_ne_nil _ _, List.cons_ne_nil _ _, hl, hl₁, hl₂⟩)
-  · rintro (h | h | ⟨l₁, l₂, -, -, hl, hl₁, hl₂⟩)
-    · exact Or.inl h
-    · exact Or.inr (Or.inl h)
-    · exact Or.inr (Or.inr ⟨l₁, l₂, hl, hl₁, hl₂⟩)
-
 end List

src/Init/Data/List/TakeDrop.lean

@@ -297,14 +297,6 @@ theorem dropWhile_cons :
     (a :: l).dropWhile p = a :: l := by
   simp [dropWhile_cons, h]
 
-theorem dropWhile_beq_eq_self_of_head?_ne [BEq α] [LawfulBEq α] {a : α} {l : List α}
-    (h : l.head? ≠ some a) : l.dropWhile (· == a) = l := by
-  cases l with
-  | nil => simp
-  | cons hd tl =>
-    rw [List.dropWhile_cons_of_neg]
-    simpa [beq_iff_eq] using h
-
 theorem head?_takeWhile {p : α → Bool} {l : List α} : (l.takeWhile p).head? = l.head?.filter p := by
   cases l with
   | nil => rfl

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -102,12 +102,6 @@ instance : XorOp Nat := ⟨Nat.xor⟩
 instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩
 instance : ShiftRight Nat := ⟨Nat.shiftRight⟩
 
-@[simp] theorem land_eq {m n : Nat} : m.land n = m &&& n := rfl
-@[simp] theorem lor_eq {m n : Nat} : m.lor n = m ||| n := rfl
-@[simp] theorem xor_eq {m n : Nat} : m.xor n = m ^^^ n := rfl
-@[simp] theorem shiftLeft_eq' {m n : Nat} : m.shiftLeft n = m <<< n := rfl
-@[simp] theorem shiftRight_eq' {m n : Nat} : m.shiftRight n = m >>> n := rfl
-
 theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
   match b with
   | 0 => (Nat.mul_one _).symm

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

@@ -867,7 +867,7 @@ theorem and_le_right {n m : Nat} : n &&& m ≤ m :=
   le_of_testBit (by simp)
 
 theorem left_le_or {n m : Nat} : n ≤ n ||| m :=
-  le_of_testBit (by simp [imp_or_left_iff_true])
+  le_of_testBit (by simpa using fun i => Or.inl)
 
 theorem right_le_or {n m : Nat} : m ≤ n ||| m :=
-  le_of_testBit (by simp [imp_or_right_iff_true])
+  le_of_testBit (by simpa using fun i => Or.inr)

src/Init/Data/Nat/Div/Lemmas.lean

@@ -253,16 +253,4 @@ theorem ext_div_mod {n a b : Nat} (h0 : a / n = b / n) (h1 : a % n = b % n) : a
 theorem ext_div_mod_iff (n a b : Nat) : a = b ↔ a / n = b / n ∧ a % n = b % n :=
   ⟨fun h => ⟨h ▸ rfl, h ▸ rfl⟩, fun ⟨h0, h1⟩ => ext_div_mod h0 h1⟩
 
-/-- An induction principle mirroring the base-`b` representation of the number. -/
-theorem base_induction {P : Nat → Prop} {n : Nat} (b : Nat) (hb : 1 < b) (single : ∀ m, m < b → P m)
-    (digit : ∀ m k, k < b → 0 < m → P m → P (b * m + k)) : P n := by
-  induction n using Nat.strongRecOn with | ind n ih
-  rcases Nat.lt_or_ge n b with hn | hn
-  · exact single _ hn
-  · have := div_add_mod n b
-    rw [← this]
-    apply digit _ _ (mod_lt _ (by omega)) _ (ih _ _)
-    · exact Nat.div_pos_iff.mpr ⟨by omega, hn⟩
-    · exact div_lt_self (by omega) (by omega)
-
 end Nat

src/Init/Data/Nat/ToString.lean

@@ -19,7 +19,6 @@ import Init.Data.Nat.Bitwise
 import Init.Data.Nat.Simproc
 import Init.WFTactics
 import Init.Data.Char.Lemmas
-import Init.Data.Nat.Div.Lemmas
 
 public section
 
@@ -38,71 +37,6 @@ theorem isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) :=
     simp only [digitChar, ↓reduceIte, Nat.reduceEqDiff]
     (repeat' split) <;> simp
 
-private theorem digitChar_iff_aux :
-    ∀ n, (n.digitChar = '0' ↔ n = 0) ∧ (n.digitChar = '1' ↔ n = 1) ∧
-         (n.digitChar = '2' ↔ n = 2) ∧ (n.digitChar = '3' ↔ n = 3) ∧
-         (n.digitChar = '4' ↔ n = 4) ∧ (n.digitChar = '5' ↔ n = 5) ∧
-         (n.digitChar = '6' ↔ n = 6) ∧ (n.digitChar = '7' ↔ n = 7) ∧
-         (n.digitChar = '8' ↔ n = 8) ∧ (n.digitChar = '9' ↔ n = 9) ∧
-         (n.digitChar = 'a' ↔ n = 10) ∧ (n.digitChar = 'b' ↔ n = 11) ∧
-         (n.digitChar = 'c' ↔ n = 12) ∧ (n.digitChar = 'd' ↔ n = 13) ∧
-         (n.digitChar = 'e' ↔ n = 14) ∧ (n.digitChar = 'f' ↔ n = 15) ∧
-         (n.digitChar = '*' ↔ 16 ≤ n)
-  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | _ + 16 => by simp [digitChar]
-
-@[simp] theorem digitChar_eq_zero : n.digitChar = '0' ↔ n = 0 := (digitChar_iff_aux n).1
-@[simp] theorem digitChar_eq_one : n.digitChar = '1' ↔ n = 1 := (digitChar_iff_aux n).2.1
-@[simp] theorem digitChar_eq_two : n.digitChar = '2' ↔ n = 2 := (digitChar_iff_aux n).2.2.1
-@[simp] theorem digitChar_eq_three : n.digitChar = '3' ↔ n = 3 := (digitChar_iff_aux n).2.2.2.1
-@[simp] theorem digitChar_eq_four : n.digitChar = '4' ↔ n = 4 := (digitChar_iff_aux n).2.2.2.2.1
-@[simp] theorem digitChar_eq_five : n.digitChar = '5' ↔ n = 5 := (digitChar_iff_aux n).2.2.2.2.2.1
-@[simp] theorem digitChar_eq_six : n.digitChar = '6' ↔ n = 6 := (digitChar_iff_aux n).2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_seven : n.digitChar = '7' ↔ n = 7 := (digitChar_iff_aux n).2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_eight : n.digitChar = '8' ↔ n = 8 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_nine : n.digitChar = '9' ↔ n = 9 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_a : n.digitChar = 'a' ↔ n = 10 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_b : n.digitChar = 'b' ↔ n = 11 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_c : n.digitChar = 'c' ↔ n = 12 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_d : n.digitChar = 'd' ↔ n = 13 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_e : n.digitChar = 'e' ↔ n = 14 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_f : n.digitChar = 'f' ↔ n = 15 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
-@[simp] theorem digitChar_eq_star : n.digitChar = '*' ↔ 16 ≤ n := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2
-
-@[simp] theorem zero_eq_digitChar : '0' = n.digitChar ↔ n = 0 := digitChar_eq_zero |> eq_comm.trans
-@[simp] theorem one_eq_digitChar : '1' = n.digitChar ↔ n = 1 := digitChar_eq_one |> eq_comm.trans
-@[simp] theorem two_eq_digitChar : '2' = n.digitChar ↔ n = 2 := digitChar_eq_two |> eq_comm.trans
-@[simp] theorem three_eq_digitChar : '3' = n.digitChar ↔ n = 3 := digitChar_eq_three |> eq_comm.trans
-@[simp] theorem four_eq_digitChar : '4' = n.digitChar ↔ n = 4 := digitChar_eq_four |> eq_comm.trans
-@[simp] theorem five_eq_digitChar : '5' = n.digitChar ↔ n = 5 := digitChar_eq_five |> eq_comm.trans
-@[simp] theorem six_eq_digitChar : '6' = n.digitChar ↔ n = 6 := digitChar_eq_six |> eq_comm.trans
-@[simp] theorem seven_eq_digitChar : '7' = n.digitChar ↔ n = 7 := digitChar_eq_seven |> eq_comm.trans
-@[simp] theorem eight_eq_digitChar : '8' = n.digitChar ↔ n = 8 := digitChar_eq_eight |> eq_comm.trans
-@[simp] theorem nine_eq_digitChar : '9' = n.digitChar ↔ n = 9 := digitChar_eq_nine |> eq_comm.trans
-@[simp] theorem a_eq_digitChar : 'a' = n.digitChar ↔ n = 10 := digitChar_eq_a |> eq_comm.trans
-@[simp] theorem b_eq_digitChar : 'b' = n.digitChar ↔ n = 11 := digitChar_eq_b |> eq_comm.trans
-@[simp] theorem c_eq_digitChar : 'c' = n.digitChar ↔ n = 12 := digitChar_eq_c |> eq_comm.trans
-@[simp] theorem d_eq_digitChar : 'd' = n.digitChar ↔ n = 13 := digitChar_eq_d |> eq_comm.trans
-@[simp] theorem e_eq_digitChar : 'e' = n.digitChar ↔ n = 14 := digitChar_eq_e |> eq_comm.trans
-@[simp] theorem f_eq_digitChar : 'f' = n.digitChar ↔ n = 15 := digitChar_eq_f |> eq_comm.trans
-@[simp] theorem star_eq_digitChar : '*' = n.digitChar ↔ 16 ≤ n := digitChar_eq_star |> eq_comm.trans
-
-/-- Auxiliary theorem for `Nat.reduceDigitCharEq` simproc. -/
-protected theorem digitChar_ne {n : Nat} (c : Char)
-    (h : c != '0' && c != '1' && c != '2' && c != '3' && c != '4' && c != '5' &&
-         c != '6' && c != '7' && c != '8' && c != '9' && c != 'a' && c != 'b' &&
-         c != 'c' && c != 'd' && c != 'e' && c != 'f' && c != '*') : n.digitChar ≠ c := by
-  rintro rfl
-  match n with
-  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | _ + 16 => simp [digitChar] at h
-
-theorem toNat_digitChar_of_lt_ten {n : Nat} (hn : n < 10) : n.digitChar.toNat = 48 + n :=
-  match n with
-  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 => by simp [digitChar]
-  | _ + 10 => by omega
-
-theorem toNat_digitChar_sub_48_of_lt_ten {n : Nat} (hn : n < 10) : n.digitChar.toNat - 48 = n := by
-  simp [toNat_digitChar_of_lt_ten hn]
-
 private theorem isDigit_of_mem_toDigitsCore
     (hc : c ∈ cs → c.isDigit) (hb₁ : 0 < b) (hb₂ : b ≤ 10) (h : c ∈ toDigitsCore b fuel n cs) :
     c.isDigit := by
@@ -119,11 +53,6 @@ private theorem isDigit_of_mem_toDigitsCore
 theorem isDigit_of_mem_toDigits (hb₁ : 0 < b) (hb₂ : b ≤ 10) (hc : c ∈ toDigits b n) : c.isDigit :=
   isDigit_of_mem_toDigitsCore (fun _ => by contradiction) hb₁ hb₂ hc
 
-@[simp]
-theorem underscore_not_in_toDigits {n : Nat} : ¬'_' ∈ Nat.toDigits 10 n := by
-  intro h
-  simpa using isDigit_of_mem_toDigits (by decide) (by decide) h
-
 private theorem toDigitsCore_of_lt_base (hb : n < b) (hf : n < fuel) :
     toDigitsCore b fuel n cs = n.digitChar :: cs := by
   unfold toDigitsCore
@@ -200,11 +129,6 @@ theorem length_toDigits_pos {b n : Nat} :
   · rw [toDigitsCore_eq_toDigitsCore_nil_append]
     simp
 
-@[simp]
-theorem toDigits_ne_nil {n b : Nat} : Nat.toDigits b n ≠ [] := by
-  rw [← List.length_pos_iff]
-  exact Nat.length_toDigits_pos
-
 theorem length_toDigits_le_iff {n k : Nat} (hb : 1 < b) (h : 0 < k) :
     (Nat.toDigits b n).length ≤ k ↔ n < b ^ k := by
   match k with
@@ -230,14 +154,6 @@ theorem repr_eq_ofList_toDigits {n : Nat} :
     n.repr = .ofList (toDigits 10 n) :=
   (rfl)
 
-@[simp]
-theorem toList_repr {n : Nat} : n.repr.toList = Nat.toDigits 10 n := by
-  simp [repr_eq_ofList_toDigits]
-
-@[simp]
-theorem repr_ne_empty {n : Nat} : n.repr ≠ "" := by
-  simp [← String.toList_inj]
-
 theorem toString_eq_ofList_toDigits {n : Nat} :
     toString n = .ofList (toDigits 10 n) :=
   (rfl)
@@ -278,59 +194,4 @@ theorem length_repr_le_iff {n k : Nat} (h : 0 < k) :
     n.repr.length ≤ k ↔ n < 10 ^ k := by
   simpa [repr_eq_ofList_toDigits] using length_toDigits_le_iff (by omega) h
 
-/--
-Transforms a list of characters into a natural number, *assuming that all characters are in the
-range from `'0'` to `'9'`*.
--/
-def ofDigitChars (b : Nat) (l : List Char) (init : Nat) : Nat :=
-  l.foldl (init := init) (fun sofar c => b * sofar + (c.toNat - '0'.toNat))
-
-theorem ofDigitChars_eq_foldl {b : Nat} {l : List Char} {init : Nat} :
-    ofDigitChars b l init = l.foldl (init := init) (fun sofar c => b * sofar + (c.toNat - '0'.toNat)) :=
-  (rfl)
-
-@[simp]
-theorem ofDigitChars_nil {init : Nat} : ofDigitChars b [] init = init := by
-  simp [ofDigitChars]
-
-theorem ofDigitChars_cons {c : Char} {cs : List Char} {init : Nat} :
-    ofDigitChars b (c::cs) init = ofDigitChars b cs (b * init + (c.toNat - '0'.toNat)) := by
-  simp [ofDigitChars]
-
-theorem ofDigitChars_cons_digitChar_of_lt_ten {n : Nat} (hn : n < 10) {cs : List Char} {init : Nat} :
-    ofDigitChars b (n.digitChar :: cs) init = ofDigitChars b cs (b * init + n) := by
-  simp [ofDigitChars_cons, Nat.toNat_digitChar_sub_48_of_lt_ten hn]
-
-theorem ofDigitChars_eq_ofDigitChars_zero {l : List Char} {init : Nat} :
-    ofDigitChars 10 l init = 10 ^ l.length * init + ofDigitChars 10 l 0 := by
-  induction l generalizing init with
-  | nil => simp [ofDigitChars]
-  | cons hd tl ih =>
-    simp only [ofDigitChars, ↓Char.isValue, Char.reduceToNat, List.foldl_cons, List.length_cons,
-      Nat.mul_zero, Nat.zero_add] at ⊢ ih
-    rw [ih, ih (init := hd.toNat - 48), Nat.pow_succ, Nat.mul_add, Nat.mul_assoc, Nat.add_assoc]
-
-theorem ofDigitChars_append {l m : List Char} (init : Nat) :
-    ofDigitChars b (l ++ m) init = ofDigitChars b m (ofDigitChars b l init) := by
-  simp [ofDigitChars]
-
-@[simp]
-theorem ofDigitChars_replicate_zero {n : Nat} : ofDigitChars b (List.replicate n '0') init = b ^ n * init := by
-  induction n generalizing init with
-  | zero => simp
-  | succ n ih => simp [List.replicate_succ, ofDigitChars_cons, ih, Nat.pow_succ, Nat.mul_assoc]
-
-theorem ofDigitChars_toDigits {b n : Nat} (hb' : 1 < b) (hb : b ≤ 10) : ofDigitChars b (toDigits b n) 0 = n := by
-  induction n using base_induction b hb' with
-  | single m hm =>
-    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten (by omega : m < 10)]
-  | digit m k hk hm ih =>
-    rw [← Nat.toDigits_append_toDigits hb' hm hk,
-      ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
-      ofDigitChars_cons_digitChar_of_lt_ten (Nat.lt_of_lt_of_le hk hb), ofDigitChars_nil]
-
-@[simp]
-theorem ofDigitChars_ten_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n :=
-  ofDigitChars_toDigits (by decide) (by decide)
-
 end Nat

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

src/Init/Data/Order/MinMaxOn.lean

@@ -39,8 +39,8 @@ public theorem minOn_id [Min α] [LE α] [DecidableLE α] [LawfulOrderLeftLeanin
 
 public theorem maxOn_id [Max α] [LE α] [DecidableLE α] [LawfulOrderLeftLeaningMax α] {x y : α} :
     maxOn id x y = max x y := by
-  letI : LE α := (inferInstance : LE α).opposite
-  letI : Min α := (inferInstance : Max α).oppositeMin
+  letI : LE α := (inferInstanceAs (LE α)).opposite
+  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
   simp [maxOn, minOn_id, Max.min_oppositeMin, this]
 
 public theorem minOn_eq_or [LE β] [DecidableLE β] {f : α → β} {x y : α} :
@@ -168,32 +168,32 @@ public theorem maxOn_eq_right_of_lt
     [LE β] [DecidableLE β] [LT β] [Total (α := β) (· ≤ ·)] [LawfulOrderLT β]
     {f : α → β} {x y : α} (h : f x < f y) :
     maxOn f x y = y :=
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : LT β := (inferInstance : LT β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : LT β := (inferInstanceAs (LT β)).opposite
   minOn_eq_right_of_lt (h := by simpa [LT.lt_opposite_iff] using h) ..
 
 public theorem left_le_apply_maxOn [le : LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} : f x ≤ f (maxOn f x y) := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa only [LE.le_opposite_iff] using apply_minOn_le_left (f := f) ..
 
 public theorem right_le_apply_maxOn [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} : f y ≤ f (maxOn f x y) := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa only [LE.le_opposite_iff] using apply_minOn_le_right (f := f)
 
 public theorem apply_maxOn_le_iff [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y : α} {b : β} :
     f (maxOn f x y) ≤ b ↔ f x ≤ b ∧ f y ≤ b := by
   rw [maxOn_eq_minOn]
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   simpa only [LE.le_opposite_iff] using le_apply_minOn_iff (f := f)
 
 public theorem maxOn_assoc [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β}
     {x y z : α} : maxOn f (maxOn f x y) z = maxOn f x (maxOn f y z) :=
-  letI : LE β := (inferInstance : LE β).opposite
+  letI : LE β := (inferInstanceAs (LE β)).opposite
   minOn_assoc (f := f)
 
 public instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
@@ -203,8 +203,8 @@ public instance [LE β] [DecidableLE β] [IsLinearPreorder β] {f : α → β} :
 
 public theorem max_apply [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeaningMax β]
     {f : α → β} {x y : α} : max (f x) (f y) = f (maxOn f x y) := by
-  letI : LE β := (inferInstance : LE β).opposite
-  letI : Min β := (inferInstance : Max β).oppositeMin
+  letI : LE β := (inferInstanceAs (LE β)).opposite
+  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
   simpa [Max.min_oppositeMin] using min_apply (f := f)
 
 public theorem apply_maxOn [LE β] [DecidableLE β] [Max β] [LawfulOrderLeftLeaningMax β]

src/Init/Data/Order/Opposite.lean

@@ -44,7 +44,7 @@ def min' [LE α] [DecidableLE α] (a b : α) : α :=
 
 open scoped Std.OppositeOrderInstances in
 def max' [LE α] [DecidableLE α] (a b : α) : α :=
-  letI : LE α := (inferInstance : LE α).opposite
+  letI : LE α := (inferInstanceAs (LE α)).opposite
   -- `DecidableLE` for the opposite order is derived automatically via `OppositeOrderInstances`
   min' a b
 ```
@@ -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 only [LE.le, LT.lt]
+      simp +instances only [LE.opposite, LT.opposite]
       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 only [LE.le]
+      simp +instances only [LE.opposite]
       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 only [LE.le, Max.max]
+      simp +instances only [LE.opposite, Min.oppositeMax]
       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 only [Max.max]
+      simp +instances only [Min.oppositeMax]
       letI := il; letI := im
       exact MinEqOr.min_eq_or a b
     max_le_iff a b c := by
-      simp only [LE.le, Max.max]
+      simp +instances only [LE.opposite, Min.oppositeMax]
       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 only [LE.le, Min.min]
+      simp +instances only [LE.opposite, Max.oppositeMin]
       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 only [Min.min]
+      simp +instances only [Max.oppositeMin]
       letI := il; letI := im
       exact MaxEqOr.max_eq_or a b
     le_min_iff a b c := by
-      simp only [LE.le, Min.min]
+      simp +instances only [LE.opposite, Max.oppositeMin]
       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 only [Max.max]
+      simp +instances only [Min.oppositeMax]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMin.min_eq_left a b hab
     max_eq_right a b hab := by
-      simp only [Max.max]
+      simp +instances only [Min.oppositeMax]
       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 only [Min.min]
+      simp +instances only [Max.oppositeMin]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMax.max_eq_left a b hab
     min_eq_right a b hab := by
-      simp only [Min.min]
+      simp +instances only [Max.oppositeMin]
       letI := il; letI := im
       exact LawfulOrderLeftLeaningMax.max_eq_right a b hab }
 

src/Init/Data/Order/PackageFactories.lean

@@ -796,6 +796,7 @@ 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/Lemmas.lean

@@ -411,7 +411,6 @@ private theorem Rii.Internal.toArray_eq_toArray_iter [Least? α]
     r.toArray = (Internal.iter r).toArray := by
   rfl
 
-@[cbv_eval]
 public theorem Rxc.Iterator.toList_eq_match [LE α] [DecidableLE α]
     [UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLE α]
@@ -429,7 +428,6 @@ public theorem Rxc.Iterator.toList_eq_match [LE α] [DecidableLE α]
   · simp [*]
   · split <;> rename_i heq' <;> simp [*]
 
-@[cbv_eval]
 public theorem Rxc.Iterator.toArray_eq_match [LE α] [DecidableLE α]
     [UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLE α]
@@ -445,7 +443,6 @@ public theorem Rxc.Iterator.toArray_eq_match [LE α] [DecidableLE α]
   · rfl
   · split <;> simp
 
-@[cbv_eval]
 public theorem Rxo.Iterator.toList_eq_match [LT α] [DecidableLT α]
     [UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLT α]
@@ -462,7 +459,6 @@ public theorem Rxo.Iterator.toList_eq_match [LT α] [DecidableLT α]
   · simp [*]
   · split <;> rename_i heq' <;> simp [*]
 
-@[cbv_eval]
 public theorem Rxo.Iterator.toArray_eq_match [LT α] [DecidableLT α]
     [UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     [LawfulUpwardEnumerableLT α]
@@ -495,7 +491,6 @@ public theorem Rxc.Iterator.toList_eq_toList_rxoIterator [LE α] [DecidableLE α
       · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
     · simpa [UpwardEnumerable.lt_iff, UpwardEnumerable.le_iff, UpwardEnumerable.lt_succ_iff] using h
 
-@[cbv_eval]
 public theorem Rxi.Iterator.toList_eq_match
     [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     {it : Iter (α := Rxi.Iterator α) α} :
@@ -507,7 +502,6 @@ public theorem Rxi.Iterator.toList_eq_match
   simp only [Iter.toList_eq_match_step (it := it), Rxi.Iterator.step_eq_step, Rxi.Iterator.step]
   split <;> rename_i heq <;> simp [*]
 
-@[cbv_eval]
 public theorem Rxi.Iterator.toArray_eq_match
     [UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     {it : Iter (α := Rxi.Iterator α) α} :
@@ -614,7 +608,6 @@ namespace Rcc
 
 variable {r : Rcc α}
 
-@[cbv_eval]
 public theorem toList_eq_if_roc [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
     r.toList = if r.lower ≤ r.upper then
@@ -762,7 +755,6 @@ public theorem ClosedOpen.toList_succ_succ_eq_map [LE α] [DecidableLE α] [Upwa
       (lo...=hi).toList.map succ :=
   Rcc.toList_succ_succ_eq_map
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
     {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m]
@@ -852,7 +844,6 @@ namespace Rco
 
 variable {r : Rco α}
 
-@[cbv_eval]
 public theorem toList_eq_if_roo [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerableLT α] :
     r.toList = if r.lower < r.upper then
@@ -1020,7 +1011,6 @@ public theorem toArray_succ_succ_eq_map [LE α] [DecidableLE α] [LT α] [Decida
       (lo...hi).toArray.map succ := by
   simp [← toArray_toList, toList_succ_succ_eq_map]
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [LE α] [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
@@ -1234,7 +1224,6 @@ public theorem toArray_succ_succ_eq_map [LE α] [DecidableLE α]
     ((succ lo)...*).toArray = (lo...*).toArray.map succ := by
   simp [← toArray_toList, toList_succ_succ_eq_map]
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [LE α]
     [UpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
@@ -1341,7 +1330,6 @@ public theorem toArray_eq_match [LE α] [DecidableLE α] [UpwardEnumerable α]
   rw [Internal.toArray_eq_toArray_iter, Rxc.Iterator.toArray_eq_match (it := Internal.iter r)]
   simp [Internal.iter, Internal.toArray_eq_toArray_iter]
 
-@[cbv_eval]
 public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α] [Rxc.IsAlwaysFinite α] :
     r.toList = match UpwardEnumerable.succ? r.lower with
@@ -1485,7 +1473,6 @@ public theorem toArray_succ_succ_eq_map [LE α] [DecidableLE α] [LT α] [Decida
       (lo<...=hi).toArray.map succ := by
   simp [← toArray_toList, toList_succ_succ_eq_map]
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [LE α] [DecidableLE α] [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLT α]
     [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w}
@@ -1585,7 +1572,6 @@ public theorem toArray_eq_match [LE α] [LT α] [DecidableLT α] [UpwardEnumerab
           #[] := by
   rw [Internal.toArray_eq_toArray_iter, Rxo.Iterator.toArray_eq_match]; rfl
 
-@[cbv_eval]
 public theorem toList_eq_match_rco [UpwardEnumerable α] [LT α] [DecidableLT α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α] [Rxo.IsAlwaysFinite α] :
     r.toList = match UpwardEnumerable.succ? r.lower with
@@ -1719,7 +1705,6 @@ public theorem toArray_succ_succ_eq_map [LT α] [DecidableLT α]
       (lo<...hi).toArray.map succ := by
   simp [← toArray_toList, toList_succ_succ_eq_map]
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [LT α] [DecidableLT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
@@ -1954,7 +1939,6 @@ public theorem toArray_succ_succ_eq_map [LT α] [DecidableLT α]
     ((succ lo)<...*).toArray = (lo<...*).toArray.map succ := by
   simp [← toArray_toList, toList_succ_succ_eq_map]
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [LT α]
     [UpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α]
@@ -2055,7 +2039,6 @@ public theorem toList_toArray [Least? α] [LE α] [DecidableLE α] [UpwardEnumer
     r.toArray.toList = r.toList := by
   simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
 
-@[cbv_eval]
 public theorem toList_eq_match_rcc [LE α] [DecidableLE α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLE α]
     [Rxc.IsAlwaysFinite α] :
@@ -2248,7 +2231,6 @@ public theorem toArray_succ_eq_map [LE α] [DecidableLE α] [Least? α]
       #[UpwardEnumerable.least (hn := ⟨r.upper⟩)] ++ (*...=hi).toArray.map succ := by
   simp [← toArray_toList, toList_succ_eq_map]
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [LE α] [DecidableLE α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerableLE α] [LawfulUpwardEnumerableLeast? α]
     [Rxc.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w}
@@ -2358,7 +2340,6 @@ public theorem toList_toArray [Least? α] [LT α] [DecidableLT α] [UpwardEnumer
     r.toArray.toList = r.toList := by
   simp [Internal.toList_eq_toList_iter, Internal.toArray_eq_toArray_iter]
 
-@[cbv_eval]
 public theorem toList_eq_match_rco [LT α] [DecidableLT α] [Least? α] [UpwardEnumerable α]
     [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableLT α]
     [Rxo.IsAlwaysFinite α] :
@@ -2569,7 +2550,6 @@ public theorem toArray_succ_eq_map [LT α] [DecidableLT α] [Least? α]
       #[UpwardEnumerable.least (hn := ⟨r.upper⟩)] ++ (*...hi).toArray.map succ := by
   simp [← toArray_toList, toList_succ_eq_map]
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [LT α] [DecidableLT α] [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerableLT α] [LawfulUpwardEnumerableLeast? α]
     [Rxo.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w}
@@ -2808,7 +2788,6 @@ public theorem pairwise_toList_le [LE α] [Least? α]
     |> List.Pairwise.imp UpwardEnumerable.le_of_lt
     |> List.Pairwise.imp (fun hle => (UpwardEnumerable.le_iff ..).mpr hle)
 
-@[cbv_eval]
 public theorem forIn'_eq_forIn'_toList [Least? α]
     [UpwardEnumerable α] [LawfulUpwardEnumerableLeast? α]
     [Rxi.IsAlwaysFinite α] [LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w}

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 only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances 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, implicit_reducible]
+@[inline]
 def Iterator.Monadic.step [UpwardEnumerable α] [LT α] [DecidableLT α]
     (it : IterM (α := Rxo.Iterator α) Id α) :
     IterStep (IterM (α := Rxo.Iterator α) Id α) α :=
@@ -1113,6 +1113,7 @@ 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)
@@ -1164,13 +1165,14 @@ 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 only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances 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)]
@@ -1635,7 +1637,7 @@ instance Iterator.instLawfulIteratorLoop [UpwardEnumerable α]
     LawfulIteratorLoop (Rxi.Iterator α) Id n where
   lawful := by
     intro lift instLawfulMonadLiftFunction γ it init Pl wf f
-    simp only [IteratorLoop.forIn, IterM.DefaultConsumers.forIn'_eq_wf Pl wf]
+    simp +instances 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,16 +248,7 @@ 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]
 
-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)
-
+set_option backward.whnf.reducibleClassField false in
 theorem instUpwardEnumerable_eq :
     instUpwardEnumerable = HasModel.instUpwardEnumerable := by
   apply UpwardEnumerable.ext
@@ -265,16 +256,16 @@ theorem instUpwardEnumerable_eq :
     apply HasModel.succ?_eq_of_technicalCondition
     simp [HasModel.encode, succ?, ← Int8.toBitVec_inj, toBitVec_minValueSealed_eq_intMinSealed]
   · ext
-    simp [HasModel.succMany?_eq, succMany?_eq_maxValueSealed, HasModel.encode, HasModel.decode,
+    simp +instances [HasModel.succMany?_eq, instUpwardEnumerable, HasModel.encode, HasModel.decode,
       ← toInt_toBitVec, toBitVec_maxValueSealed_eq_intMaxSealed, ofIntLE_eq_ofInt]
 
 
 instance : LawfulUpwardEnumerable Int8 := by
-  rw [instUpwardEnumerable_eq]
+  simp +instances only [instUpwardEnumerable_eq]
   infer_instance
 
 instance : LawfulUpwardEnumerableLE Int8 := by
-  rw [instUpwardEnumerable_eq]
+  simp +instances only [instUpwardEnumerable_eq]
   infer_instance
 
 public instance instRxcHasSize : Rxc.HasSize Int8 where
@@ -286,7 +277,7 @@ theorem instRxcHasSize_eq :
     ← toInt_toBitVec, HasModel.toNat_toInt_add_one_sub_toInt (Nat.zero_lt_succ _)]
 
 public instance instRxcLawfulHasSize : Rxc.LawfulHasSize Int8 := by
-  rw [instUpwardEnumerable_eq, instRxcHasSize_eq]
+  simp +instances only [instUpwardEnumerable_eq, instRxcHasSize_eq]
   infer_instance
 public instance : Rxc.IsAlwaysFinite Int8 := by exact inferInstance
 
@@ -303,7 +294,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
-  rw [instUpwardEnumerable_eq, instRxiHasSize_eq]
+  simp +instances only [instUpwardEnumerable_eq, instRxiHasSize_eq]
   infer_instance
 public instance instRxiIsAlwaysFinite : Rxi.IsAlwaysFinite Int8 := by exact inferInstance
 
@@ -353,6 +344,7 @@ 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
@@ -448,6 +440,7 @@ 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
@@ -543,6 +536,7 @@ 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
@@ -643,6 +637,7 @@ 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,7 +11,6 @@ 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/Repr.lean

@@ -354,6 +354,16 @@ end Nat
 instance : Repr Nat where
   reprPrec n _ := Nat.repr n
 
+/--
+Returns the decimal string representation of an integer.
+-/
+protected def Int.repr : Int → String
+    | ofNat m   => Nat.repr m
+    | negSucc m => String.Internal.append "-" (Nat.repr (succ m))
+
+instance : Repr Int where
+  reprPrec i prec := if i < 0 then Repr.addAppParen i.repr prec else i.repr
+
 def hexDigitRepr (n : Nat) : String :=
   String.singleton <| Nat.digitChar n
 

src/Init/Data/SInt/Basic.lean

@@ -7,7 +7,6 @@ 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,7 +10,6 @@ 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
 
@@ -26,7 +25,7 @@ variable {shape : RangeShape} {α : Type u}
 structure SubarrayIterator (α : Type u) where
   xs : Subarray α
 
-@[inline, expose, implicit_reducible]
+@[inline, expose]
 def SubarrayIterator.step :
     IterM (α := SubarrayIterator α) Id α → IterStep (IterM (α := SubarrayIterator α) m α) α
   | ⟨⟨xs⟩⟩ =>

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

@@ -28,6 +28,7 @@ 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
@@ -126,7 +127,7 @@ public theorem forIn_toList {α : Type u} {s : Subarray α}
     ForIn.forIn s.toList init f = ForIn.forIn s init f :=
   Slice.forIn_toList
 
-@[cbv_eval, grind =]
+@[grind =]
 public theorem forIn_eq_forIn_toList {α : Type u} {s : Subarray α}
     {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
     {f : α → γ → m (ForInStep γ)} :
@@ -193,7 +194,6 @@ public theorem Array.toSubarray_eq_toSubarray_of_min_eq_min {xs : Array α}
         simp [*]; omega
       · simp
 
-@[cbv_eval]
 public theorem Array.toSubarray_eq_min {xs : Array α} {lo hi : Nat} :
     xs.toSubarray lo hi = ⟨⟨xs, min lo (min hi xs.size), min hi xs.size, Nat.min_le_right _ _,
       Nat.min_le_right _ _⟩⟩ := by
@@ -215,6 +215,7 @@ 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
@@ -244,7 +245,6 @@ private theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start sto
       List.length_take, ge_iff_le, h₁]
     omega
 
-@[cbv_eval]
 public theorem Subarray.toList_eq_drop_take {xs : Subarray α} :
     xs.toList = (xs.array.toList.take xs.stop).drop xs.start := by
   rw [Subarray.toList_eq, Array.toList_extract, Std.Internal.List.extract_eq_drop_take']

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

@@ -11,7 +11,6 @@ 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,6 +70,7 @@ 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
@@ -77,9 +78,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 [h, List.take_drop, Nat.add_sub_cancel' ‹_›, ← List.take_eq_take_min]
+    simp +instances [h, List.take_drop, Nat.add_sub_cancel' ‹_›, ← List.take_eq_take_min]
   · have : min hi xs.length ≤ lo := by omega
-    simp [h, Nat.min_eq_right this]
+    simp +instances [h, Nat.min_eq_right this]
 
 @[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} :
@@ -110,11 +111,12 @@ 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 [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice]
+  simp +instances [ListSlice.toList_eq, Std.Rci.Sliceable.mkSlice, List.toUnboundedSlice]
 
 @[simp, grind =]
 public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} :
@@ -288,11 +290,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
-  rw [instSliceableListSliceNat_1]
-  simp only [List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
+  simp +instances only [instSliceableListSliceNat_1, List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
   obtain ⟨⟨xs, stop⟩⟩ := xs
   cases stop
   · simp
@@ -327,13 +329,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
-  rw [instSliceableListSliceNat_2]
-  simp only [ListSlice.toList_eq (xs := xs)]
+  simp +instances only [instSliceableListSliceNat_2, ListSlice.toList_eq (xs := xs)]
   obtain ⟨⟨xs, stop⟩⟩ := xs
-  simp only
+  simp +instances only
   split <;> simp
 
 @[simp, grind =]

src/Init/Data/String/Basic.lean

@@ -852,10 +852,6 @@ theorem Slice.rawEndPos_copy {s : Slice} : s.copy.rawEndPos = s.rawEndPos := by
 theorem copy_toSlice {s : String} : s.toSlice.copy = s := by
   simp [← toByteArray_inj, Slice.toByteArray_copy, ← size_toByteArray]
 
-@[simp]
-theorem copy_comp_toSlice : String.Slice.copy ∘ String.toSlice = id := by
-  ext; simp
-
 theorem Slice.getUTF8Byte_eq_getUTF8Byte_copy {s : Slice} {p : Pos.Raw} {h : p < s.rawEndPos} :
     s.getUTF8Byte p h = s.copy.getUTF8Byte p (by simpa) := by
   simp [getUTF8Byte, String.getUTF8Byte, toByteArray_copy, ByteArray.getElem_extract]
@@ -1270,11 +1266,9 @@ theorem Pos.toSlice_comp_ofToSlice {s : String} :
 theorem Pos.ofToSlice_comp_toSlice {s : String} :
     Pos.ofToSlice ∘ (toSlice (s := s)) = id := by ext; simp
 
-@[simp]
 theorem Pos.toSlice_inj {s : String} {p q : s.Pos} : p.toSlice = q.toSlice ↔ p = q :=
   ⟨fun h => by simpa using congrArg Pos.ofToSlice h, (· ▸ rfl)⟩
 
-@[simp]
 theorem Pos.ofToSlice_inj {s : String} {p q : s.toSlice.Pos} : ofToSlice p = ofToSlice q ↔ p = q :=
   ⟨fun h => by simpa using congrArg Pos.toSlice h, (· ▸ rfl)⟩
 
@@ -1693,7 +1687,7 @@ def Pos.next {s : @& String} (pos : @& s.Pos) (h : pos ≠ s.endPos) : s.Pos :=
 
 @[simp]
 theorem Pos.ofToSlice_next_toSlice {s : String} {pos : s.Pos} {h} :
-    ofToSlice (Slice.Pos.next pos.toSlice h) = pos.next (ne_of_apply_ne Pos.toSlice (by simpa using h)) :=
+    ofToSlice (Slice.Pos.next pos.toSlice h) = pos.next (ne_of_apply_ne Pos.toSlice (by simpa)) :=
   rfl
 
 @[simp]
@@ -1928,7 +1922,7 @@ theorem Pos.toSlice_next {s : String} {p : s.Pos} {h} :
   simp [next, -ofToSlice_next_toSlice]
 
 theorem Pos.next_toSlice {s : String} {p : s.Pos} {h} :
-    p.toSlice.next h = (p.next (ne_of_apply_ne Pos.toSlice (by simpa using h))).toSlice := by
+    p.toSlice.next h = (p.next (ne_of_apply_ne Pos.toSlice (by simpa))).toSlice := by
   simp [Pos.toSlice_next]
 
 theorem Pos.byteIdx_lt_utf8ByteSize {s : String} (p : s.Pos) (h : p ≠ s.endPos) :

src/Init/Data/String/Bootstrap.lean

@@ -55,11 +55,9 @@ 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
 
@@ -69,7 +67,6 @@ 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
 
@@ -79,57 +76,45 @@ 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
 
@@ -156,43 +141,33 @@ 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
 
@@ -200,11 +175,9 @@ 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/String/Decode.lean

@@ -64,7 +64,7 @@ public theorem Char.utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2
   match c.utf8Size, c.utf8Size_pos, c.utf8Size_le_four with
   | 1, _, _ | 2, _, _ | 3, _, _ | 4, _, _ => simp
 
-theorem Char.toNat_le {c : Char} : c.toNat ≤ 0x10ffff := by
+theorem Char.toNat_val_le {c : Char} : c.val.toNat ≤ 0x10ffff := by
   have := c.valid
   simp [UInt32.isValidChar, Nat.isValidChar] at this
   omega
@@ -193,10 +193,10 @@ theorem helper₄ (s : Nat) (c : BitVec w₀) (v : BitVec w') (w : Nat) :
 -- TODO: possibly it makes sense to factor out this proof
 theorem String.toBitVec_getElem_utf8EncodeChar_zero_of_utf8Size_eq_one {c : Char} (h : c.utf8Size = 1) :
     ((String.utf8EncodeChar c)[0]'(by simp [h])).toBitVec = 0#1 ++ c.val.toBitVec.extractLsb' 0 7 := by
-  have h₀ : c.toNat < 128 := by
-    suffices c.toNat ≤ 127 by omega
+  have h₀ : c.val.toNat < 128 := by
+    suffices c.val.toNat ≤ 127 by omega
     simpa [Char.utf8Size_eq_one_iff, UInt32.le_iff_toNat_le] using h
-  have h₁ : c.toNat < 256 := by omega
+  have h₁ : c.val.toNat < 256 := by omega
   rw [← BitVec.toNat_inj, BitVec.toNat_append]
   simp [-Char.toUInt8_val, utf8EncodeChar_eq_singleton h, Nat.mod_eq_of_lt h₀, Nat.mod_eq_of_lt h₁]
 
@@ -977,9 +977,9 @@ theorem assemble₄_eq_some_iff_utf8EncodeChar_eq {w x y z : UInt8} {c : Char} :
         BitVec.extractLsb'_append_extractLsb'_eq_extractLsb' (by simp),
         BitVec.extractLsb'_append_extractLsb'_eq_extractLsb' (by simp),
         ← BitVec.setWidth_eq_extractLsb' (by simp), BitVec.setWidth_setWidth_eq_self]
-      have := c.toNat_le
+      have := c.toNat_val_le
       simp only [Nat.reduceAdd, BitVec.lt_def, UInt32.toNat_toBitVec, BitVec.toNat_twoPow,
-        Nat.reducePow, Nat.reduceMod, gt_iff_lt, Char.toNat_val]
+        Nat.reducePow, Nat.reduceMod, gt_iff_lt]
       omega
 
 theorem verify₄_eq_isSome_assemble₄ {w x y z : UInt8} :

src/Init/Data/String/Defs.lean

@@ -187,9 +187,6 @@ theorem append_right_inj (s : String) {t₁ t₂ : String} :
 theorem append_assoc {s₁ s₂ s₃ : String} : s₁ ++ s₂ ++ s₃ = s₁ ++ (s₂ ++ s₃) := by
   simp [← toByteArray_inj, ByteArray.append_assoc]
 
-instance : Std.Associative (α := String) (· ++ ·) where
-  assoc _ _ _ := append_assoc
-
 @[simp]
 theorem utf8ByteSize_eq_zero_iff {s : String} : s.utf8ByteSize = 0 ↔ s = "" := by
   refine ⟨fun h => ?_, fun h => h ▸ utf8ByteSize_empty⟩
@@ -233,7 +230,7 @@ Examples:
  * `"empty".isEmpty = false`
  * `" ".isEmpty = false`
 -/
-@[inline, expose] def isEmpty (s : String) : Bool :=
+@[inline] def isEmpty (s : String) : Bool :=
   s.utf8ByteSize == 0
 
 @[export lean_string_isempty]

src/Init/Data/String/Iter.lean

@@ -6,5 +6,29 @@ Authors: Markus Himmel
 module
 
 prelude
-public import Init.Data.String.Iter.Basic
-public import Init.Data.String.Iter.Intercalate
+public import Init.Data.Iterators.Combinators.FilterMap
+public import Init.Data.Iterators.Consumers.Collect
+
+set_option doc.verso true
+
+namespace Std
+
+/--
+Convenience function for turning an iterator into a list of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : List String :=
+  it.map toString |>.toList
+
+/--
+Convenience function for turning an iterator into an array of strings, provided the output of the
+iterator implements {name}`ToString`.
+-/
+@[inline]
+public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
+    (it : Iter (α := α) β) : Array String :=
+  it.map toString |>.toArray
+
+end Std

src/Init/Data/String/Iter/Basic.lean

@@ -1,34 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.Iterators.Combinators.FilterMap
-public import Init.Data.Iterators.Consumers.Collect
-
-set_option doc.verso true
-
-namespace Std
-
-/--
-Convenience function for turning an iterator into a list of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringList {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : List String :=
-  it.map toString |>.toList
-
-/--
-Convenience function for turning an iterator into an array of strings, provided the output of the
-iterator implements {name}`ToString`.
--/
-@[inline]
-public abbrev Iter.toStringArray {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Iter (α := α) β) : Array String :=
-  it.map toString |>.toArray
-
-end Std