fix: eta-reduce expressions in sym discrimination tree lookup

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

.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,53 +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.
-
-To rebuild individual stage 2 modules without a full `make stage2`, use Lake directly:
-```
-cd build/release/stage2 && lake build Init.Prelude
-```
-
-To run tests in stage2, replace `-C build/release` from above with `-C build/release/stage2`.
-
 ## New features
 
 When asked to implement new features:

.claude/commands/release.md

@@ -157,16 +157,6 @@ Note: `gh pr checks --watch` exits as soon as ALL checks complete (pass or fail)
 fail while others are still running, `--watch` will continue until everything settles, then exit
 with a non-zero code. So a background `--watch` finishing = all checks done; check which failed.
 
-## Mathlib Bump Branches
-
-Mathlib `bump/v4.X.0` branches live on the **fork** `leanprover-community/mathlib4-nightly-testing`,
-NOT on `leanprover-community/mathlib4`.
-
-## Never Force-Update Remote Refs Without Confirmation
-
-Never force-update an existing remote branch or tag via `git push --force` or the GitHub API
-without explicit user confirmation.
-
 ## Error Handling
 
 **CRITICAL**: If something goes wrong or a command fails:

.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,13 +125,13 @@ jobs:
           else
             echo "TARGET_STAGE=stage1" >> $GITHUB_ENV
           fi
-      - name: Configure Build
+      - name: Build
         run: |
           ulimit -c unlimited  # coredumps
           [ -d build ] || mkdir build
           cd build
           # arguments passed to `cmake`
-          OPTIONS=(-DWFAIL=ON)
+          OPTIONS=(-DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true)
           if [[ -n '${{ matrix.release }}' ]]; then
             # this also enables githash embedding into stage 1 library, which prohibits reusing
             # `.olean`s across commits, so we don't do it in the fast non-release CI
@@ -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
@@ -143,7 +128,7 @@ jobs:
           CMAKE_MAJOR=$(grep -E "^set\(LEAN_VERSION_MAJOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_MINOR=$(grep -E "^set\(LEAN_VERSION_MINOR " src/CMakeLists.txt | grep -oE '[0-9]+')
           CMAKE_PATCH=$(grep -E "^set\(LEAN_VERSION_PATCH " src/CMakeLists.txt | grep -oE '[0-9]+')
-          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | grep -oE '[0-9]+' | head -1)
+          CMAKE_IS_RELEASE=$(grep -m 1 -E "^set\(LEAN_VERSION_IS_RELEASE " src/CMakeLists.txt | sed -nE 's/^set\(LEAN_VERSION_IS_RELEASE ([0-9]+)\).*/\1/p')
 
           # Expected values from tag parsing
           TAG_MAJOR="${{ steps.set-release.outputs.LEAN_VERSION_MAJOR }}"
@@ -255,7 +240,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 +261,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 +269,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",
@@ -305,13 +278,12 @@ jobs:
                 "test": true,
                 "CMAKE_PRESET": "reldebug",
                 // * `elab_bench/big_do` crashes with exit code 134
-                // * `compile_bench/channel` randomly segfaults
-                "CTEST_OPTIONS": "-E 'elab_bench/big_do|compile_bench/channel'",
+                "CTEST_OPTIONS": "-E 'elab_bench/big_do'",
               },
               {
                 "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,

.github/workflows/update-stage0.yml

@@ -77,7 +77,7 @@ jobs:
       # sync options with `Linux Lake` to ensure cache reuse
       run: |
         mkdir -p build
-        cmake --preset release -B build -DWFAIL=ON
+        cmake --preset release -B build -DLEAN_EXTRA_MAKE_OPTS=-DwarningAsError=true
       shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: |

.gitignore

@@ -34,4 +34,3 @@ wdErr.txt
 wdIn.txt
 wdOut.txt
 downstream_releases/
-.claude/worktrees/

.gitpod.yml

@@ -6,6 +6,6 @@ vscode:
     - leanprover.lean4
 
 tasks:
-  - name: Build
-    init: cmake --preset dev
+  - name: Release build
+    init: cmake --preset release
     command: make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)

.vscode/tasks.json

@@ -11,15 +11,6 @@
 				"isDefault": true
 			}
 		},
-		{
-			"label": "build stage2",
-			"type": "shell",
-			"command": "make -C build/release stage2 -j$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)",
-			"problemMatcher": [],
-			"group": {
-				"kind": "build"
-			}
-		},
 		{
 			"label": "build-old",
 			"type": "shell",

CMakeLists.txt

@@ -1,6 +1,4 @@
 cmake_minimum_required(VERSION 3.21)
-include(ExternalProject)
-include(FetchContent)
 
 if(NOT CMAKE_GENERATOR MATCHES "Makefiles")
   message(FATAL_ERROR "Only makefile generators are supported")
@@ -36,6 +34,7 @@ foreach(var ${vars})
   endif()
 endforeach()
 
+include(ExternalProject)
 project(LEAN CXX C)
 
 if(NOT (DEFINED STAGE0_CMAKE_EXECUTABLE_SUFFIX))
@@ -80,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)
@@ -115,22 +114,21 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
       )
     endif()
   endif()
-  list(APPEND STAGE0_ARGS -DLEANTAR=${LEANTAR})
   list(APPEND CL_ARGS -DCADICAL=${CADICAL} -DLEANTAR=${LEANTAR})
 endif()
 
 if(USE_MIMALLOC)
-  FetchContent_Declare(
+  ExternalProject_Add(
     mimalloc
+    PREFIX mimalloc
     GIT_REPOSITORY https://github.com/microsoft/mimalloc
     GIT_TAG v2.2.3
-    # Unnecessarily deep directory structure, but it saves us from a complicated
-    # stage0 update for now. If we ever update the other dependencies like
-    # cadical, it might be worth reorganizing the directory structure.
-    SOURCE_DIR
-    "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
+    # just download, we compile it as part of each stage as it is small
+    CONFIGURE_COMMAND ""
+    BUILD_COMMAND ""
+    INSTALL_COMMAND ""
   )
-  FetchContent_MakeAvailable(mimalloc)
+  list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
 if(NOT STAGE1_PREV_STAGE)
@@ -220,9 +218,7 @@ add_custom_target(
   DEPENDS stage2
 )
 
-add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1-configure)
-
-add_custom_target(cache-get COMMAND $(MAKE) -C stage1 cache-get DEPENDS stage1-configure)
+add_custom_target(clean-stdlib COMMAND $(MAKE) -C stage1 clean-stdlib DEPENDS stage1)
 
 install(CODE "execute_process(COMMAND make -C stage1 install)")
 

CMakePresets.json

@@ -8,26 +8,16 @@
   "configurePresets": [
     {
       "name": "release",
-      "displayName": "Release build config",
+      "displayName": "Default development optimized build config",
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/release"
     },
-    {
-      "name": "dev",
-      "displayName": "Default development optimized build config",
-      "cacheVariables": {
-        "STRIP_BINARIES": "OFF"
-      },
-      "generator": "Unix Makefiles",
-      "binaryDir": "${sourceDir}/build/dev"
-    },
     {
       "name": "debug",
       "displayName": "Debug build config",
       "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "Debug",
         "LEAN_EXTRA_CXX_FLAGS": "-DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
-        "STRIP_BINARIES": "OFF"
+        "CMAKE_BUILD_TYPE": "Debug"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/debug"
@@ -36,8 +26,7 @@
       "name": "reldebug",
       "displayName": "Release with assertions enabled",
       "cacheVariables": {
-        "CMAKE_BUILD_TYPE": "RelWithAssert",
-        "STRIP_BINARIES": "OFF"
+        "CMAKE_BUILD_TYPE": "RelWithAssert"
       },
       "generator": "Unix Makefiles",
       "binaryDir": "${sourceDir}/build/reldebug"
@@ -49,7 +38,6 @@
         "LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined -DLEAN_DEFAULT_THREAD_STACK_SIZE=16*1024*1024",
         "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined",
         "LEAN_EXTRA_LINKER_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
-        "STRIP_BINARIES": "OFF",
         "SMALL_ALLOCATOR": "OFF",
         "USE_MIMALLOC": "OFF",
         "BSYMBOLIC": "OFF",
@@ -70,10 +58,6 @@
       "name": "release",
       "configurePreset": "release"
     },
-    {
-      "name": "dev",
-      "configurePreset": "dev"
-    },
     {
       "name": "debug",
       "configurePreset": "debug"
@@ -97,11 +81,6 @@
       "configurePreset": "release",
       "output": {"outputOnFailure": true, "shortProgress": true}
     },
-    {
-      "name": "dev",
-      "configurePreset": "dev",
-      "output": {"outputOnFailure": true, "shortProgress": true}
-    },
     {
       "name": "debug",
       "configurePreset": "debug",

doc/examples/compiler/run_test

@@ -1,3 +1,6 @@
+#!/usr/bin/env bash
+source ../../../tests/env_test.sh
+
 leanmake --always-make bin
 
 capture ./build/bin/test 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

@@ -1,4 +1,7 @@
+#!/usr/bin/env bash
+source ../../tests/env_test.sh
+
 capture_only "$1" \
   lean -Dlinter.all=false "$1"
-check_out_file
 check_exit_is_success
+check_out_file

doc/make/index.md

@@ -30,9 +30,6 @@ cd lean4
 cmake --preset release
 make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
 ```
-
-For development, `cmake --preset dev` is recommended instead.
-
 You can replace `$(nproc || sysctl -n hw.logicalcpu)` with the desired parallelism amount.
 
 The above commands will compile the Lean library and binaries into the

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)
 
@@ -311,16 +311,16 @@ def check_cmake_version(repo_url, branch, version_major, version_minor, github_t
         print(f"  ❌ Could not retrieve {cmake_file_path} from {branch}")
         return False
 
-    expected_patterns = [
-        (f"LEAN_VERSION_MAJOR", rf"^set\(LEAN_VERSION_MAJOR\s+{version_major}[\s)]", f"set(LEAN_VERSION_MAJOR {version_major} ...)"),
-        (f"LEAN_VERSION_MINOR", rf"^set\(LEAN_VERSION_MINOR\s+{version_minor}[\s)]", f"set(LEAN_VERSION_MINOR {version_minor} ...)"),
-        (f"LEAN_VERSION_PATCH", rf"^set\(LEAN_VERSION_PATCH\s+0[\s)]", f"set(LEAN_VERSION_PATCH 0 ...)"),
-        (f"LEAN_VERSION_IS_RELEASE", rf"^set\(LEAN_VERSION_IS_RELEASE\s+1[\s)]", f"set(LEAN_VERSION_IS_RELEASE 1 ...)"),
+    expected_lines = [
+        f"set(LEAN_VERSION_MAJOR {version_major})",
+        f"set(LEAN_VERSION_MINOR {version_minor})",
+        f"set(LEAN_VERSION_PATCH 0)",
+        f"set(LEAN_VERSION_IS_RELEASE 1)"
     ]
 
-    for name, pattern, display in expected_patterns:
-        if not any(re.match(pattern, l.strip()) for l in content.splitlines()):
-            print(f"  ❌ Missing or incorrect line in {cmake_file_path}: {display}")
+    for line in expected_lines:
+        if not any(l.strip().startswith(line) for l in content.splitlines()):
+            print(f"  ❌ Missing or incorrect line in {cmake_file_path}: {line}")
             return False
 
     print(f"  ✅ CMake version settings are correct in {cmake_file_path}")
@@ -343,11 +343,11 @@ def check_stage0_version(repo_url, branch, version_major, version_minor, github_
     for line in content.splitlines():
         stripped = line.strip()
         if stripped.startswith("set(LEAN_VERSION_MAJOR "):
-            actual = stripped.split()[1].rstrip(")")
+            actual = stripped.split()[-1].rstrip(")")
             if actual != str(version_major):
                 errors.append(f"LEAN_VERSION_MAJOR: expected {version_major}, found {actual}")
         elif stripped.startswith("set(LEAN_VERSION_MINOR "):
-            actual = stripped.split()[1].rstrip(")")
+            actual = stripped.split()[-1].rstrip(")")
             if actual != str(version_minor):
                 errors.append(f"LEAN_VERSION_MINOR: expected {version_minor}, found {actual}")
 

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
@@ -28,14 +35,6 @@ repositories:
     branch: main
     dependencies: []
 
-  - name: leansqlite
-    url: https://github.com/leanprover/leansqlite
-    toolchain-tag: true
-    stable-branch: false
-    branch: main
-    dependencies:
-      - plausible
-
   - name: verso
     url: https://github.com/leanprover/verso
     toolchain-tag: true
@@ -108,7 +107,7 @@ repositories:
     toolchain-tag: true
     stable-branch: false
     branch: main
-    dependencies: [lean4-cli, BibtexQuery, mathlib4, leansqlite]
+    dependencies: [lean4-cli, BibtexQuery, mathlib4]
 
   - name: cslib
     url: https://github.com/leanprover/cslib

script/release_steps.py

@@ -481,30 +481,22 @@ def execute_release_steps(repo, version, config):
         run_command("lake update", cwd=repo_path, stream_output=True)
     elif repo_name == "verso":
         # verso has nested Lake projects in test-projects/ that each have their own
-        # lake-manifest.json with a subverso pin and their own lean-toolchain.
-        # After updating the root manifest via `lake update`, sync the de-modulized
-        # subverso rev into all sub-manifests, and update their lean-toolchain files.
+        # lake-manifest.json with a subverso pin. After updating the root manifest via
+        # `lake update`, sync the de-modulized subverso rev into all sub-manifests.
+        # The sub-projects use an old toolchain (v4.21.0) that doesn't support module/prelude
+        # syntax, so they need the de-modulized version (tagged no-modules/<root-rev>).
+        # The "SubVerso version consistency" CI check accepts either the root or de-modulized rev.
         run_command("lake update", cwd=repo_path, stream_output=True)
         print(blue("Syncing de-modulized subverso rev to test-project sub-manifests..."))
         sync_script = (
             '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"))
-        # Update all lean-toolchain files in test-projects/ to match the root
-        print(blue("Updating lean-toolchain files in test-projects/..."))
-        find_result = run_command("find test-projects -name lean-toolchain", cwd=repo_path)
-        for tc_path in find_result.stdout.strip().splitlines():
-            if tc_path:
-                tc_file = repo_path / tc_path
-                with open(tc_file, "w") as f:
-                    f.write(f"leanprover/lean4:{version}\n")
-                print(green(f"  Updated {tc_path}"))
     elif dependencies:
         run_command(f'perl -pi -e \'s/"v4\\.[0-9]+(\\.[0-9]+)?(-rc[0-9]+)?"/"' + version + '"/g\' lakefile.*', cwd=repo_path)
         run_command("lake update", cwd=repo_path, stream_output=True)
@@ -666,61 +658,56 @@ def execute_release_steps(repo, version, config):
         # Fetch latest changes to ensure we have the most up-to-date nightly-testing branch
         print(blue("Fetching latest changes from origin..."))
         run_command("git fetch origin", cwd=repo_path)
-
-        # Check if nightly-testing branch exists on origin (use local ref after fetch for exact match)
-        nightly_check = run_command("git show-ref --verify --quiet refs/remotes/origin/nightly-testing", cwd=repo_path, check=False)
-        if nightly_check.returncode != 0:
-            print(yellow("No nightly-testing branch found on origin, skipping merge"))
-        else:
-            try:
-                print(blue("Merging origin/nightly-testing..."))
-                run_command("git merge origin/nightly-testing", cwd=repo_path)
-                print(green("Merge completed successfully"))
-            except subprocess.CalledProcessError:
-                # Merge failed due to conflicts - check which files are conflicted
-                print(blue("Merge conflicts detected, checking which files are affected..."))
-
-                # Get conflicted files using git status
-                status_result = run_command("git status --porcelain", cwd=repo_path)
-                conflicted_files = []
-
-                for line in status_result.stdout.splitlines():
-                    if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
-                        # Extract filename (skip the first 3 characters which are status codes)
-                        conflicted_files.append(line[3:])
-
-                # Filter out allowed files
-                allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
-                problematic_files = []
-
+        
+        try:
+            print(blue("Merging origin/nightly-testing..."))
+            run_command("git merge origin/nightly-testing", cwd=repo_path)
+            print(green("Merge completed successfully"))
+        except subprocess.CalledProcessError:
+            # Merge failed due to conflicts - check which files are conflicted
+            print(blue("Merge conflicts detected, checking which files are affected..."))
+            
+            # Get conflicted files using git status
+            status_result = run_command("git status --porcelain", cwd=repo_path)
+            conflicted_files = []
+            
+            for line in status_result.stdout.splitlines():
+                if len(line) >= 2 and line[:2] in ['UU', 'AA', 'DD', 'AU', 'UA', 'DU', 'UD']:
+                    # Extract filename (skip the first 3 characters which are status codes)
+                    conflicted_files.append(line[3:])
+            
+            # Filter out allowed files
+            allowed_patterns = ['lean-toolchain', 'lake-manifest.json']
+            problematic_files = []
+            
+            for file in conflicted_files:
+                is_allowed = any(pattern in file for pattern in allowed_patterns)
+                if not is_allowed:
+                    problematic_files.append(file)
+            
+            if problematic_files:
+                # There are conflicts in non-allowed files - fail
+                print(red("❌ Merge failed!"))
+                print(red(f"Merging nightly-testing resulted in conflicts in:"))
+                for file in problematic_files:
+                    print(red(f"  - {file}"))
+                print(red("Please resolve these conflicts manually."))
+                return
+            else:
+                # Only allowed files are conflicted - resolve them automatically
+                print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
+                print(blue("Resolving conflicts automatically..."))
+                
+                # For lean-toolchain and lake-manifest.json, keep our versions
                 for file in conflicted_files:
-                    is_allowed = any(pattern in file for pattern in allowed_patterns)
-                    if not is_allowed:
-                        problematic_files.append(file)
-
-                if problematic_files:
-                    # There are conflicts in non-allowed files - fail
-                    print(red("❌ Merge failed!"))
-                    print(red(f"Merging nightly-testing resulted in conflicts in:"))
-                    for file in problematic_files:
-                        print(red(f"  - {file}"))
-                    print(red("Please resolve these conflicts manually."))
-                    return
-                else:
-                    # Only allowed files are conflicted - resolve them automatically
-                    print(green(f"✅ Only allowed files conflicted: {', '.join(conflicted_files)}"))
-                    print(blue("Resolving conflicts automatically..."))
-
-                    # For lean-toolchain and lake-manifest.json, keep our versions
-                    for file in conflicted_files:
-                        print(blue(f"Keeping our version of {file}"))
-                        run_command(f"git checkout --ours {file}", cwd=repo_path)
-
-                    # Complete the merge
-                    run_command("git add .", cwd=repo_path)
-                    run_command("git commit --no-edit", cwd=repo_path)
-
-                    print(green("✅ Merge completed successfully with automatic conflict resolution"))
+                    print(blue(f"Keeping our version of {file}"))
+                    run_command(f"git checkout --ours {file}", cwd=repo_path)
+                
+                # Complete the merge
+                run_command("git add .", cwd=repo_path)
+                run_command("git commit --no-edit", cwd=repo_path)
+                
+                print(green("✅ Merge completed successfully with automatic conflict resolution"))
 
     # Build and test (skip for Mathlib)
     if repo_name not in ["mathlib4"]:

src/CMakeLists.txt

@@ -8,7 +8,7 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4 CACHE STRING "")
-set(LEAN_VERSION_MINOR 31 CACHE STRING "")
+set(LEAN_VERSION_MINOR 30 CACHE STRING "")
 set(LEAN_VERSION_PATCH 0 CACHE STRING "")
 set(LEAN_VERSION_IS_RELEASE 0 CACHE STRING "") # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
@@ -80,7 +80,6 @@ option(CCACHE "use ccache" ON)
 option(SPLIT_STACK "SPLIT_STACK" OFF)
 # When OFF we disable LLVM support
 option(LLVM "LLVM" OFF)
-option(STRIP_BINARIES "Strip produced binaries" ON)
 
 # When ON we include githash in the version string
 option(USE_GITHASH "GIT_HASH" ON)
@@ -110,27 +109,15 @@ option(RUNTIME_STATS "RUNTIME_STATS" OFF)
 option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
 option(USE_GMP "USE_GMP" ON)
 option(USE_MIMALLOC "use mimalloc" ON)
-set(LEAN_MI_SECURE 0 CACHE STRING "Configure mimalloc memory safety mitigations (https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60)")
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
 option(USE_LAKE "Use Lake instead of lean.mk for building core libs from language server" ON)
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
-set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
-set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
+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_OPTS " -Dbackward.do.legacy=false")
-
-# option used by the CI to fail on warnings
-option(WFAIL "Fail build if warnings are emitted by Lean" ON)
-if(WFAIL MATCHES "ON")
-  string(APPEND LAKE_EXTRA_ARGS " --wfail")
-  string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
-endif()
-
 if(LAZY_RC MATCHES "ON")
   set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
 endif()
@@ -207,7 +194,7 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/lib/lean")
 
 # OSX default thread stack size is very small. Moreover, in Debug mode, each new stack frame consumes a lot of extra memory.
 if((MULTI_THREAD MATCHES "ON") AND (CMAKE_SYSTEM_NAME MATCHES "Darwin"))
-  string(APPEND LEAN_EXTRA_OPTS " -s40000")
+  string(APPEND LEAN_EXTRA_MAKE_OPTS " -s40000")
 endif()
 
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
@@ -624,38 +611,6 @@ else()
       OUTPUT_VARIABLE GIT_SHA1
       OUTPUT_STRIP_TRAILING_WHITESPACE
     )
-    # Fallback for jj workspaces where git cannot find .git directly.
-    # Use `jj git root` to find the backing git repo, then `jj log` to
-    # resolve the current workspace's commit (git HEAD points to the root
-    # workspace, not the current one).
-    if("${GIT_SHA1}" STREQUAL "")
-      find_program(JJ_EXECUTABLE jj)
-      if(JJ_EXECUTABLE)
-        execute_process(
-          COMMAND "${JJ_EXECUTABLE}" git root
-          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-          OUTPUT_VARIABLE _jj_git_dir
-          OUTPUT_STRIP_TRAILING_WHITESPACE
-          ERROR_QUIET
-          RESULT_VARIABLE _jj_git_root_result
-        )
-        execute_process(
-          COMMAND "${JJ_EXECUTABLE}" log -r @ --no-graph -T "commit_id"
-          WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
-          OUTPUT_VARIABLE _jj_commit
-          OUTPUT_STRIP_TRAILING_WHITESPACE
-          ERROR_QUIET
-          RESULT_VARIABLE _jj_rev_result
-        )
-        if(_jj_git_root_result EQUAL 0 AND _jj_rev_result EQUAL 0)
-          execute_process(
-            COMMAND git --git-dir "${_jj_git_dir}" ls-tree "${_jj_commit}" stage0 --object-only
-            OUTPUT_VARIABLE GIT_SHA1
-            OUTPUT_STRIP_TRAILING_WHITESPACE
-          )
-        endif()
-      endif()
-    endif()
     message(STATUS "stage0 sha1: ${GIT_SHA1}")
     # Now that we've prepared the information for the next stage, we can forget that we will use
     # Lake in the future as we won't use it in this stage
@@ -679,9 +634,6 @@ else()
   set(LEAN_PATH_SEPARATOR ":")
 endif()
 
-# inherit genral options for lean.mk.in and stdlib.make.in
-string(APPEND LEAN_EXTRA_MAKE_OPTS " ${LEAN_EXTRA_OPTS}")
-
 # Version
 configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
 if(STAGE EQUAL 0)
@@ -807,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}"
@@ -842,14 +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()
@@ -956,13 +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
@@ -982,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()
 
@@ -993,13 +934,6 @@ add_custom_target(
 
 add_custom_target(clean-olean DEPENDS clean-stdlib)
 
-if(USE_LAKE_CACHE)
-  add_custom_target(
-    cache-get
-    COMMAND ${PREV_STAGE}/bin/lake${CMAKE_EXECUTABLE_SUFFIX} cache get --repo=leanprover/lean4
-  )
-endif()
-
 install(
   DIRECTORY "${CMAKE_BINARY_DIR}/lib/"
   DESTINATION lib
@@ -1008,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
@@ -1073,7 +1006,7 @@ string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_CC "${LEANC_CC}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_FLAGS "${LEANC_INTERNAL_FLAGS}")
 string(REPLACE "ROOT" "${CMAKE_BINARY_DIR}" LEANC_INTERNAL_LINKER_FLAGS "${LEANC_INTERNAL_LINKER_FLAGS}")
 
-toml_escape("${LEAN_EXTRA_OPTS}" LEAN_EXTRA_OPTS_TOML)
+toml_escape("${LEAN_EXTRA_MAKE_OPTS}" LEAN_EXTRA_OPTS_TOML)
 
 if(CMAKE_BUILD_TYPE MATCHES "Debug|Release|RelWithDebInfo|MinSizeRel")
   set(CMAKE_BUILD_TYPE_TOML "${CMAKE_BUILD_TYPE}")

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
@@ -802,7 +802,6 @@ Examples:
 def firstM {α : Type u} {m : Type v → Type w} [Alternative m] (f : α → m β) (as : Array α) : m β :=
   go 0
 where
-  @[specialize]
   go (i : Nat) : m β :=
     if hlt : i < as.size then
       f as[i] <|> go (i+1)
@@ -1086,17 +1085,6 @@ Examples:
 def sum {α} [Add α] [Zero α] : Array α → α :=
   foldr (· + ·) 0
 
-/--
-Computes the product of the elements of an array.
-
-Examples:
- * `#[a, b, c].prod = a * (b * (c * 1))`
- * `#[1, 2, 5].prod = 10`
--/
-@[inline, expose]
-def prod {α} [Mul α] [One α] : Array α → α :=
-  foldr (· * ·) 1
-
 /--
 Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`.
 
@@ -1265,7 +1253,7 @@ Examples:
 -/
 @[inline, expose]
 def findIdx? {α : Type u} (p : α → Bool) (as : Array α) : Option Nat :=
-  let rec @[specialize] loop (j : Nat) :=
+  let rec loop (j : Nat) :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none

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/Int.lean

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
-public import Init.Data.List.Int.Prod
 public import Init.Data.Array.MinMax
 import Init.Data.Int.Lemmas
 
@@ -75,17 +74,4 @@ theorem sum_div_length_le_max_of_max?_eq_some_int {xs : Array Int} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_int (by simpa using h)
 
-@[simp] theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
-  rw [← List.toArray_replicate, List.prod_toArray]
-  simp
-
-theorem prod_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_int (xs : Array Int) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_int {xs : Array Int} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Int.mul_comm, ← prod_eq_foldr, prod_reverse_int]
-
 end Array

src/Init/Data/Array/Lemmas.lean

@@ -3096,13 +3096,13 @@ theorem foldl_eq_foldlM {f : β → α → β} {b} {xs : Array α} {start stop :
 theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Array α} {start stop : Nat} :
     xs.foldr f b start stop = (xs.foldrM (m := Id) (pure <| f · ·) b start stop).run := rfl
 
-theorem foldl_eq_foldl_extract {xs : Array α} {f : β → α → β} {init : β} :
+public theorem foldl_eq_foldl_extract {xs : Array α} {f : β → α → β} {init : β} :
     xs.foldl (init := init) (start := start) (stop := stop) f =
       (xs.extract start stop).foldl (init := init) f := by
   simp only [foldl_eq_foldlM]
   rw [foldlM_start_stop]
 
-theorem foldr_eq_foldr_extract {xs : Array α} {f : α → β → β} {init : β} :
+public theorem foldr_eq_foldr_extract {xs : Array α} {f : α → β → β} {init : β} :
     xs.foldr (init := init) (start := start) (stop := stop) f =
       (xs.extract stop start).foldr (init := init) f := by
   simp only [foldr_eq_foldrM]
@@ -4380,47 +4380,6 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [← sum_toList, List.sum_eq_foldl]
 
-/-! ### prod -/
-
-@[simp, grind =] theorem prod_empty [Mul α] [One α] : (#[] : Array α).prod = 1 := rfl
-theorem prod_eq_foldr [Mul α] [One α] {xs : Array α} :
-    xs.prod = xs.foldr (init := 1) (· * ·) :=
-  rfl
-
-@[simp, grind =]
-theorem prod_toList [Mul α] [One α] {as : Array α} : as.toList.prod = as.prod := by
-  cases as
-  simp [Array.prod, List.prod]
-
-@[simp, grind =]
-theorem prod_append [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    {as₁ as₂ : Array α} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [← prod_toList, List.prod_append]
-
-@[simp, grind =]
-theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
-    #[x].prod = x := by
-  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
-
-@[simp, grind =]
-theorem prod_push [Mul α] [One α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} {x : α} :
-    (xs.push x).prod = xs.prod * x := by
-  simp [Array.prod_eq_foldr, Std.LawfulRightIdentity.right_id, Std.LawfulLeftIdentity.left_id,
-    ← Array.foldr_assoc]
-
-@[simp, grind =]
-theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.Commutative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : Array α) : xs.reverse.prod = xs.prod := by
-  simp [← prod_toList, List.prod_reverse]
-
-theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : Array α} :
-    xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp [← prod_toList, List.prod_eq_foldl]
-
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}
     (H : ∀ acc a, (F acc a).toList = acc.toList ++ G a) :

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/Nat.lean

@@ -8,7 +8,6 @@ module
 prelude
 public import Init.Data.Array.MinMax
 import Init.Data.List.Nat.Sum
-import Init.Data.List.Nat.Prod
 import Init.Data.Array.Lemmas
 
 public section
@@ -82,24 +81,4 @@ theorem sum_div_length_le_max_of_max?_eq_some_nat {xs : Array Nat} (h : xs.max?
   simpa [List.max?_toArray, List.sum_toArray] using
     List.sum_div_length_le_max_of_max?_eq_some_nat (by simpa using h)
 
-protected theorem prod_pos_iff_forall_pos_nat {xs : Array Nat} : 0 < xs.prod ↔ ∀ x ∈ xs, 0 < x := by
-  simp [← prod_toList, List.prod_pos_iff_forall_pos_nat]
-
-protected theorem prod_eq_zero_iff_exists_zero_nat {xs : Array Nat} :
-    xs.prod = 0 ↔ ∃ x ∈ xs, x = 0 := by
-  simp [← prod_toList, List.prod_eq_zero_iff_exists_zero_nat]
-
-@[simp] theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
-  rw [← List.toArray_replicate, List.prod_toArray]
-  simp
-
-theorem prod_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).prod = as₁.prod * as₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_nat (xs : Array Nat) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_nat {xs : Array Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
-
 end Array

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/Array/Subarray.lean

@@ -80,7 +80,7 @@ instance : SliceSize (Internal.SubarrayData α) where
   size s := s.internalRepresentation.stop - s.internalRepresentation.start
 
 @[grind =, suggest_for Subarray.size]
-theorem size_eq {xs : Subarray α} :
+public theorem size_eq {xs : Subarray α} :
     xs.size = xs.stop - xs.start := by
   simp [Std.Slice.size, SliceSize.size, start, stop]
 

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

@@ -20,20 +20,12 @@ universe u
 
 namespace ByteArray
 
-@[extern "lean_sarray_dec_eq"]
-def beq (lhs rhs : @& ByteArray) : Bool :=
-  lhs.data == rhs.data
-
-instance : BEq ByteArray where
-  beq := beq
+deriving instance BEq for ByteArray
 
 attribute [ext] ByteArray
 
-@[extern "lean_sarray_dec_eq"]
-def decEq (lhs rhs : @& ByteArray) : Decidable (lhs = rhs) :=
-  decidable_of_decidable_of_iff ByteArray.ext_iff.symm
-
-instance : DecidableEq ByteArray := decEq
+instance : DecidableEq ByteArray :=
+  fun _ _ => decidable_of_decidable_of_iff ByteArray.ext_iff.symm
 
 instance : Inhabited ByteArray where
   default := empty

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/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/Compare.lean

@@ -74,7 +74,7 @@ protected theorem isGE_compare {a b : Int} :
   rw [← Int.compare_swap, Ordering.isGE_swap]
   exact Int.isLE_compare
 
-instance : Std.LawfulOrderOrd Int where
+public instance : Std.LawfulOrderOrd Int where
   isLE_compare _ _ := Int.isLE_compare
   isGE_compare _ _ := Int.isGE_compare
 

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/Basic.lean

@@ -42,29 +42,29 @@ The conversion functions {name (scope := "Init.Data.Iterators.Basic")}`Shrink.de
 {name (scope := "Init.Data.Iterators.Basic")}`Shrink.inflate` form an equivalence between
 {name}`α` and {lean}`Shrink α`, but this equivalence is intentionally not definitional.
 -/
-def Shrink (α : Type u) : Type u := Internal.idOpaque.1 α
+public def Shrink (α : Type u) : Type u := Internal.idOpaque.1 α
 
 /-- Converts elements of {name}`α` into elements of {lean}`Shrink α`. -/
 @[always_inline]
-def Shrink.deflate {α} (x : α) : Shrink α :=
+public def Shrink.deflate {α} (x : α) : Shrink α :=
   cast (by simp [Shrink, Internal.idOpaque.property]) x
 
 /-- Converts elements of {lean}`Shrink α` into elements of {name}`α`. -/
 @[always_inline]
-def Shrink.inflate {α} (x : Shrink α) : α :=
+public def Shrink.inflate {α} (x : Shrink α) : α :=
   cast (by simp [Shrink, Internal.idOpaque.property]) x
 
 @[simp, grind =]
-theorem Shrink.deflate_inflate {α} {x : Shrink α} :
+public theorem Shrink.deflate_inflate {α} {x : Shrink α} :
     Shrink.deflate x.inflate = x := by
   simp [deflate, inflate]
 
 @[simp, grind =]
-theorem Shrink.inflate_deflate {α} {x : α} :
+public theorem Shrink.inflate_deflate {α} {x : α} :
     (Shrink.deflate x).inflate = x := by
   simp [deflate, inflate]
 
-theorem Shrink.inflate_inj {α} {x y : Shrink α} :
+public theorem Shrink.inflate_inj {α} {x y : Shrink α} :
     x.inflate = y.inflate ↔ x = y := by
   apply Iff.intro
   · intro h
@@ -72,7 +72,7 @@ theorem Shrink.inflate_inj {α} {x y : Shrink α} :
   · rintro rfl
     rfl
 
-theorem Shrink.deflate_inj {α} {x y : α} :
+public theorem Shrink.deflate_inj {α} {x y : α} :
     Shrink.deflate x = Shrink.deflate y ↔ x = y := by
   apply Iff.intro
   · intro h

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/Append.lean

@@ -190,7 +190,7 @@ def Append.instFinitenessRelation [Monad m] [Iterator α₁ m β] [Iterator α
       exact IterM.TerminationMeasures.Finite.rel_of_skip ‹_›
 
 @[no_expose]
-instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
+public instance Append.instFinite [Monad m] [Iterator α₁ m β] [Iterator α₂ m β]
     [Finite α₁ m] [Finite α₂ m] : Finite (Append α₁ α₂ m β) m :=
   .of_finitenessRelation instFinitenessRelation
 

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

@@ -271,7 +271,7 @@ private def optionPelim' {α : Type u_1} (t : Option α) {β :  Sort u_2}
 
 /--
 Inserts an `Option` case distinction after the first computation of a call to `MonadAttach.pbind`.
-This lemma is useful for simplifying the second computation, which often involves `match` expressions
+This lemma is useful for simplifying the second computation, which often involes `match` expressions
 that use `pbind`'s proof term.
 -/
 private theorem pbind_eq_pbind_if_isSome [Monad m] [MonadAttach m] (x : m (Option α)) (f : (_ : _) → _ → m β) :
@@ -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

@@ -282,7 +282,6 @@ The lexicographic order with respect to `lt` is:
 * `as.lex [] = false` is `false`
 * `(a :: as).lex (b :: bs)` is true if `lt a b` or `a == b` and `lex lt as bs` is true.
 -/
-@[specialize]
 def lex [BEq α] (l₁ l₂ : List α) (lt : α → α → Bool := by exact (· < ·)) : Bool :=
   match l₁, l₂ with
   | [],      _ :: _  => true
@@ -1005,7 +1004,6 @@ Examples:
  * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 4) = [8, 3, 2, 4, 2, 7, 4]`
  * `[8, 3, 2, 4, 2, 7, 4].dropWhile (· < 100) = []`
 -/
-@[specialize]
 def dropWhile (p : α → Bool) : List α → List α
   | []   => []
   | a::l => match p a with
@@ -1248,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 -/
 
 /--
@@ -1462,11 +1442,9 @@ Examples:
 ["circle", "square", "triangle"]
 ```
 -/
-@[inline]
 def modifyTailIdx (l : List α) (i : Nat) (f : List α → List α) : List α :=
   go i l
 where
-  @[specialize]
   go : Nat → List α → List α
   | 0, l => f l
   | _+1, [] => []
@@ -1502,7 +1480,6 @@ Examples:
  * `[1, 2, 3].modify 2 (· * 10) = [1, 2, 30]`
  * `[1, 2, 3].modify 3 (· * 10) = [1, 2, 3]`
 -/
-@[inline]
 def modify (l : List α) (i : Nat) (f : α → α) : List α :=
   l.modifyTailIdx i (modifyHead f)
 
@@ -1609,7 +1586,6 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1`
 * `[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none`
 -/
-@[specialize]
 def find? (p : α → Bool) : List α → Option α
   | []    => none
   | a::as => match p a with
@@ -1632,7 +1608,6 @@ Examples:
  * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10`
  * `[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
-@[specialize]
 def findSome? (f : α → Option β) : List α → Option β
   | []    => none
   | a::as => match f a with
@@ -1656,7 +1631,6 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 5) = some 2`
 * `[7, 6, 5, 8, 1, 2, 6].findRev? (· < 1) = none`
 -/
-@[specialize]
 def findRev? (p : α → Bool) : List α → Option α
   | []    => none
   | a::as => match findRev? p as with
@@ -1675,7 +1649,6 @@ Examples:
  * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 5 then some (10 * x) else none) = some 20`
  * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
-@[specialize]
 def findSomeRev? (f : α → Option β) : List α → Option β
   | []    => none
   | a::as => match findSomeRev? f as with
@@ -1726,11 +1699,9 @@ Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4`
 * `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none`
 -/
-@[inline]
 def findIdx? (p : α → Bool) (l : List α) : Option Nat :=
   go l 0
 where
-  @[specialize]
   go : List α → Nat → Option Nat
   | [], _ => none
   | a :: l, i => if p a then some i else go l (i + 1)
@@ -1761,7 +1732,6 @@ Examples:
 @[inline] def findFinIdx? (p : α → Bool) (l : List α) : Option (Fin l.length) :=
   go l 0 (by simp)
 where
-  @[specialize]
   go : (l' : List α) → (i : Nat) → (h : l'.length + i = l.length) → Option (Fin l.length)
   | [], _, _ => none
   | a :: l, i, h =>
@@ -1898,7 +1868,7 @@ Examples:
 * `[2, 4, 5, 6].any (· % 2 = 0) = true`
 * `[2, 4, 5, 6].any (· % 2 = 1) = true`
 -/
-@[suggest_for List.some, specialize]
+@[suggest_for List.some]
 def any : (l : List α) → (p : α → Bool) → Bool
   | [], _ => false
   | h :: t, p => p h || any t p
@@ -1918,7 +1888,7 @@ Examples:
 * `[2, 4, 6].all (· % 2 = 0) = true`
 * `[2, 4, 5, 6].all (· % 2 = 0) = false`
 -/
-@[suggest_for List.every, specialize]
+@[suggest_for List.every]
 def all : List α → (α → Bool) → Bool
   | [], _ => true
   | h :: t, p => p h && all t p
@@ -2019,7 +1989,6 @@ Examples:
 * `[1, 2, 3].zipWithAll Prod.mk [5, 6] = [(some 1, some 5), (some 2, some 6), (some 3, none)]`
 * `[x₁, x₂].zipWithAll f [y] = [f (some x₁) (some y), f (some x₂) none]`
 -/
-@[specialize]
 def zipWithAll (f : Option α → Option β → γ) : List α → List β → List γ
   | [], bs => bs.map fun b => f none (some b)
   | a :: as, [] => (a :: as).map fun a => f (some a) none
@@ -2069,20 +2038,6 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl
 
-/--
-Computes the product of the elements of a list.
-
-Examples:
- * `[a, b, c].prod = a * (b * (c * 1))`
- * `[1, 2, 5].prod = 10`
--/
-def prod {α} [Mul α] [One α] : List α → α :=
-  foldr (· * ·) 1
-
-@[simp, grind =] theorem prod_nil [Mul α] [One α] : ([] : List α).prod = 1 := rfl
-@[simp, grind =] theorem prod_cons [Mul α] [One α] {a : α} {l : List α} : (a::l).prod = a * l.prod := rfl
-theorem prod_eq_foldr [Mul α] [One α] {l : List α} : l.prod = l.foldr (· * ·) 1 := rfl
-
 /-! ### range -/
 
 /--

src/Init/Data/List/Control.lean

@@ -444,8 +444,8 @@ theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
     intro b
     cases b <;> simp
 
-@[inline, expose] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : @& List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop : (as' : @& List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
+@[inline, expose] protected def forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop : (as' : List α) → (b : β) → Exists (fun bs => bs ++ as' = as) → m β
     | [], b, _    => pure b
     | a::as', b, h => do
       have : a ∈ as := by

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/Int.lean

@@ -7,4 +7,3 @@ module
 
 prelude
 public import Init.Data.List.Int.Sum
-public import Init.Data.List.Int.Prod

src/Init/Data/List/Int/Prod.lean

@@ -1,31 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-import Init.Data.List.Lemmas
-import Init.Data.Int.Lemmas
-public import Init.Data.Int.Pow
-public import Init.Data.List.Basic
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace List
-
-@[simp]
-theorem prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n := by
-  induction n <;> simp_all [replicate_succ, Int.pow_succ, Int.mul_comm]
-
-theorem prod_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_int (xs : List Int) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-end List

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
@@ -1878,24 +1856,6 @@ theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
       Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
 
-@[simp, grind =]
-theorem prod_append [Mul α] [One α] [Std.LawfulLeftIdentity (α := α) (· * ·) 1]
-    [Std.Associative (α := α) (· * ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
-
-@[simp, grind =]
-theorem prod_singleton [Mul α] [One α] [Std.LawfulRightIdentity (· * ·) (1 : α)] {x : α} :
-    [x].prod = x := by
-  simp [List.prod_eq_foldr, Std.LawfulRightIdentity.right_id x]
-
-@[simp, grind =]
-theorem prod_reverse [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.Commutative (α := α) (· * ·)]
-    [Std.LawfulLeftIdentity (α := α) (· * ·) 1] (xs : List α) : xs.reverse.prod = xs.prod := by
-  induction xs <;>
-    simp_all [prod_append, Std.Commutative.comm (α := α) _ 1,
-      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
-
 /-! ### concat
 
 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
@@ -2802,11 +2762,6 @@ theorem sum_eq_foldl [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
     xs.sum = xs.foldl (init := 0) (· + ·) := by
   simp [sum_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
 
-theorem prod_eq_foldl [One α] [Mul α] [Std.Associative (α := α) (· * ·)]
-    [Std.LawfulIdentity (· * ·) (1 : α)] {xs : List α} :
-    xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp [prod_eq_foldr, foldl_eq_apply_foldr, Std.LawfulLeftIdentity.left_id]
-
 -- The argument `f : α₁ → α₂` is intentionally explicit, as it is sometimes not found by unification.
 theorem foldl_hom (f : α₁ → α₂) {g₁ : α₁ → β → α₁} {g₂ : α₂ → β → α₂} {l : List β} {init : α₁}
     (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init) := by

src/Init/Data/List/MinMax.lean

@@ -37,7 +37,7 @@ open Nat
 @[simp, grind =] theorem min?_nil [Min α] : ([] : List α).min? = none := rfl
 
 @[simp, grind =]
-theorem min?_singleton [Min α] {x : α} : [x].min? = some x :=
+public theorem min?_singleton [Min α] {x : α} : [x].min? = some x :=
   (rfl)
 
 -- We don't put `@[simp]` on `min?_cons'`,
@@ -52,7 +52,7 @@ theorem min?_cons' [Min α] {xs : List α} : (x :: xs).min? = some (foldl min x
   cases xs <;> simp [min?]
 
 @[simp, grind =]
-theorem isSome_min?_iff [Min α] {xs : List α} : xs.min?.isSome ↔ xs ≠ [] := by
+public theorem isSome_min?_iff [Min α] {xs : List α} : xs.min?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [min?]
 
 @[grind .]
@@ -247,7 +247,7 @@ theorem foldl_min_eq_min [Min α] [Std.IdempotentOp (min : α → α → α)] [S
 @[simp, grind =] theorem max?_nil [Max α] : ([] : List α).max? = none := rfl
 
 @[simp, grind =]
-theorem max?_singleton [Max α] {x : α} : [x].max? = some x :=
+public theorem max?_singleton [Max α] {x : α} : [x].max? = some x :=
   (rfl)
 
 -- We don't put `@[simp]` on `max?_cons'`,
@@ -262,7 +262,7 @@ theorem max?_cons' [Max α] {xs : List α} : (x :: xs).max? = some (foldl max x
   cases xs <;> simp [max?]
 
 @[simp, grind =]
-theorem isSome_max?_iff [Max α] {xs : List α} : xs.max?.isSome ↔ xs ≠ [] := by
+public theorem isSome_max?_iff [Max α] {xs : List α} : xs.max?.isSome ↔ xs ≠ [] := by
   cases xs <;> simp [max?]
 
 @[grind .]

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.lean

@@ -13,7 +13,6 @@ public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
 public import Init.Data.List.Nat.Sum
-public import Init.Data.List.Nat.Prod
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq

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

@@ -1,50 +0,0 @@
-/-
-Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-import Init.Data.List.Lemmas
-public import Init.BinderPredicates
-public import Init.NotationExtra
-import Init.Data.Nat.Lemmas
-
-public section
-
-set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
-set_option linter.indexVariables true -- Enforce naming conventions for index variables.
-
-namespace List
-
-protected theorem prod_eq_zero_iff_exists_zero_nat {l : List Nat} : l.prod = 0 ↔ ∃ x ∈ l, x = 0 := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp [Nat.mul_eq_zero, ih, eq_comm (a := (0 : Nat))]
-
-protected theorem prod_pos_iff_forall_pos_nat {l : List Nat} : 0 < l.prod ↔ ∀ x ∈ l, 0 < x := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [prod_cons, mem_cons, forall_eq_or_imp, ← ih]
-    constructor
-    · intro h
-      exact ⟨Nat.pos_of_mul_pos_right h, Nat.pos_of_mul_pos_left h⟩
-    · exact fun ⟨hx, hxs⟩ => Nat.mul_pos hx hxs
-
-@[simp]
-theorem prod_replicate_nat {n : Nat} {a : Nat} : (replicate n a).prod = a ^ n := by
-  induction n <;> simp_all [replicate_succ, Nat.pow_succ, Nat.mul_comm]
-
-theorem prod_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod := by
-  simp [prod_append]
-
-theorem prod_reverse_nat (xs : List Nat) : xs.reverse.prod = xs.prod := by
-  simp [prod_reverse]
-
-theorem prod_eq_foldl_nat {xs : List Nat} : xs.prod = xs.foldl (init := 1) (· * ·) := by
-  simp only [foldl_eq_foldr_reverse, Nat.mul_comm, ← prod_eq_foldr, prod_reverse_nat]
-
-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/Perm.lean

@@ -606,13 +606,6 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum :
   | swap => simpa [List.sum_cons] using Nat.add_left_comm ..
   | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
 
-theorem prod_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.prod = l₂.prod := by
-  induction h with
-  | nil => simp
-  | cons _ _ ih => simp [ih]
-  | swap => simpa [List.prod_cons] using Nat.mul_left_comm ..
-  | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
-
 theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by
   rw [Bool.eq_iff_iff]; simp [hp.mem_iff]
 
@@ -622,9 +615,6 @@ theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum
 grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum
 
-grind_pattern Perm.prod_nat => l₁ ~ l₂, l₁.prod
-grind_pattern Perm.prod_nat => l₁ ~ l₂, l₂.prod
-
 end Perm
 
 end List

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/List/ToArray.lean

@@ -213,9 +213,6 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
 @[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
   simp [Array.sum, List.sum]
 
-@[simp, grind =] theorem prod_toArray [Mul α] [One α] (l : List α) : l.toArray.prod = l.prod := by
-  simp [Array.prod, List.prod]
-
 @[simp, grind =] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
   apply ext'

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/Compare.lean

@@ -70,7 +70,7 @@ protected theorem isGE_compare {a b : Nat} :
   rw [← Nat.compare_swap, Ordering.isGE_swap]
   exact Nat.isLE_compare
 
-instance : Std.LawfulOrderOrd Nat where
+public instance : Std.LawfulOrderOrd Nat where
   isLE_compare _ _ := Nat.isLE_compare
   isGE_compare _ _ := Nat.isGE_compare
 

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/Gcd.lean

@@ -60,7 +60,7 @@ theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by
   cases n with
   | zero => simp
   | succ n =>
-    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `(rfl)` instead
+    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
     rw [gcd_succ]
     exact gcd_zero_left _
 instance : Std.LawfulIdentity gcd 0 where

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/Option/Attach.lean

@@ -444,7 +444,7 @@ instance : MonadAttach Option where
   CanReturn x a := x = some a
   attach x := x.attach
 
-instance : LawfulMonadAttach Option where
+public instance : LawfulMonadAttach Option where
   map_attach {α} x := by simp [MonadAttach.attach]
   canReturn_map_imp {α P x a} := by
     cases x
@@ -455,7 +455,7 @@ end Option
 
 namespace OptionT
 
-instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
+public instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     WeaklyLawfulMonadAttach (OptionT m) where
   map_attach {α} x := by
     apply OptionT.ext
@@ -466,7 +466,7 @@ instance [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] :
     | ⟨some a, _⟩ => simp [OptionT.pure, OptionT.mk]
     | ⟨none, _⟩ => simp
 
-instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
+public instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
     LawfulMonadAttach (OptionT m) where
   canReturn_map_imp {α P x a} h := by
     simp only [MonadAttach.CanReturn, OptionT.run_map] at h

src/Init/Data/Ord/String.lean

@@ -9,7 +9,7 @@ prelude
 public import Init.Data.Order.Ord
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas
-import Init.Data.String.Lemmas.StringOrder
+import Init.Data.String.Lemmas
 
 public section
 

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/Lemmas.lean

@@ -243,10 +243,6 @@ public theorem lt_iff_le_and_ne [LE α] [LT α] [LawfulOrderLT α] [IsPartialOrd
     a < b ↔ a ≤ b ∧ a ≠ b := by
   simpa [le_iff_lt_or_eq, or_and_right] using Std.ne_of_lt
 
-public theorem lt_trichotomy [LT α] [Std.Trichotomous (α := α) (· < ·)] (a b : α) :
-    a < b ∨ a = b ∨ b < a :=
-  Trichotomous.rel_or_eq_or_rel_swap
-
 end LT
 end Std
 

src/Init/Data/Order/LemmasExtra.lean

@@ -152,7 +152,7 @@ public theorem max_eq_if_isGE_compare {α : Type u} [Ord α] [LE α] {_ : Max α
     {a b : α} : max a b = if (compare a b).isGE then a else b := by
   open Classical in simp [max_eq_if, isGE_compare]
 
-theorem min_le_min [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] (a b : α) : min a b ≤ min b a := by
+private theorem min_le_min [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] (a b : α) : min a b ≤ min b a := by
   apply (LawfulOrderInf.le_min_iff (min a b) b a).2
   rw [And.comm]
   by_cases h : a ≤ b

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 β]