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,46 +11,18 @@ See `tests/README.md` for full documentation. Quick reference:
 CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test
 
-# Specific test by name (supports regex via ctest -R; double-quote special chars like |)
+# Specific test by name (supports regex via ctest -R)
 CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS="-R 'grind_ematch'"
-
-# Multiple tests matching a pattern
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS="-R 'treemap|phashmap'"
+make -C build/release -j "$(nproc)" test ARGS='-R grind_ematch'
 
 # Rerun only previously failed tests
 CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
 
-# Run a test manually without ctest (test pile: pass filename relative to the pile dir)
-tests/with_stage1_test_env.sh tests/elab_bench/run_bench.sh cbv_decide.lean
-tests/with_stage1_test_env.sh tests/elab/run_test.sh grind_indexmap.lean
+# Single test from tests/foo/bar/ (quick check during development)
+cd tests/foo/bar && ./run_test example_test.lean
 ```
 
-## Benchmark vs Test Problem Sizes
-
-Benchmarks are also run as tests. Use the `TEST_BENCH` environment variable (unset in tests, set to `1` in benchmarks) to scale problem sizes:
-
-- In `compile_bench` `.init.sh` files: check `$TEST_BENCH` and set `TEST_ARGS` accordingly
-- In `elab_bench` Lean files: use `(← IO.getEnv "TEST_BENCH") == some "1"` to switch between small (test) and large (bench) inputs
-
-See `tests/README.md` for the full benchmark writing guide.
-
-## Testing stage 2
-
-When requested to test stage 2, build it as follows:
-```
-make -C build/release stage2 -j$(nproc)
-```
-Stage 2 is *not* automatically invalidated by changes to `src/` which allows for faster iteration
-when fixing a specific file in the stage 2 build but for invalidating any files that already passed
-the stage 2 build as well as for final validation,
-```
-make -C build/release/stage2 clean-stdlib
-```
-must be run manually before building.
-
 ## New features
 
 When asked to implement new features:

.github/workflows/build-template.yml

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

.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,19 +61,15 @@ 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
@@ -244,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)
@@ -265,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,
@@ -273,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",
@@ -299,7 +283,7 @@ jobs:
               {
                 "name": "Linux fsanitize",
                 // Always run on large if available, more reliable regarding timeouts
-                "os": large ? "nscloud-ubuntu-24.04-amd64-16x32-with-cache" : "ubuntu-latest",
+                "os": large ? "nscloud-ubuntu-22.04-amd64-16x32-with-cache" : "ubuntu-latest",
                 "enabled": level >= 2,
                 // do not fail nightlies on this for now
                 "secondary": level <= 2,

CMakeLists.txt

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

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

flake.nix

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

script/release_checklist.py

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

script/release_steps.py

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

src/CMakeLists.txt

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

src/Init/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

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

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

src/Init/Data/BEq.lean

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

src/Init/Data/Bool.lean

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

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

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

src/Init/Data/Int/Pow.lean

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

src/Init/Data/Int/Repr.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-module
-
-prelude
-public import Init.Data.Repr
-public import Init.Data.String.Defs
-
-namespace Int
-
-/--
-Returns the decimal string representation of an integer.
--/
-public protected def repr : Int → String
-  | ofNat m   => Nat.repr m
-  | negSucc m => "-" ++ Nat.repr (Nat.succ m)
-
-public instance : Repr Int where
-  reprPrec i prec := if i < 0 then Repr.addAppParen i.repr prec else i.repr
-
-end Int

src/Init/Data/Int/ToString.lean

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -32,7 +32,7 @@ Traverses the given iterator and stores the emitted values in an array.
 If the iterator is not finite, this function might run forever. The variant
 `it.ensureTermination.toArray` always terminates after finitely many steps.
 -/
-@[cbv_opaque, always_inline, inline]
+@[always_inline, inline]
 def Iter.toArray {α : Type w} {β : Type w}
     [Iterator α Id β] (it : Iter (α := α) β) : Array β :=
   it.toIterM.toArray.run
@@ -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/Lemmas/Combinators/Append.lean

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

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

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

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

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

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

@@ -232,6 +232,7 @@ public theorem Iter.toArray_flatMapM {α α₂ β γ : Type w} {m : Type w → T
     (it₁.flatMapM f).toArray = Array.flatten <$> (it₁.mapM fun b => do (← f b).toArray).toArray := by
   simp [flatMapM, toArray_flatMapAfterM]
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -240,9 +241,9 @@ public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α I
       | some it₂ => it₂.toList ++
           (it₁.map fun b => (f b).toList).toList.flatten := by
   simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
-  unfold Iter.toList
-  cases it₂ <;> simp [map]
+  cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
 
+set_option backward.isDefEq.respectTransparency false in
 public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     {f : β → Iter (α := α₂) γ} {it₁ : Iter (α := α) β} {it₂ : Option (Iter (α := α₂) γ)} :
@@ -251,10 +252,8 @@ public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α
       | some it₂ => it₂.toArray ++
           (it₁.map fun b => (f b).toArray).toArray.flatten := by
   simp only [flatMapAfter, Iter.toArray, toIterM_toIter, IterM.toArray_flatMapAfter]
-  unfold Iter.toArray
   cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM, - IterM.toArray_map]
 
-@[cbv_eval]
 public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id]
@@ -262,7 +261,6 @@ public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β]
     (it₁.flatMap f).toList = (it₁.map fun b => (f b).toList).toList.flatten := by
   simp [flatMap, toList_flatMapAfter]
 
-@[cbv_eval]
 public theorem Iter.toArray_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
     [Iterator α Id β] [Iterator α₂ Id γ] [Finite α Id] [Finite α₂ Id]

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

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

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

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

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

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

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

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

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 (α := α) β} :

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

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

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

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

src/Init/Data/Iterators/PostconditionMonad.lean

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

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

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

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

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

src/Init/Data/List/Basic.lean

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

src/Init/Data/List/Find.lean

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

src/Init/Data/List/Lemmas.lean

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

src/Init/Data/List/MinMaxIdx.lean

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

src/Init/Data/List/MinMaxOn.lean

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

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

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

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

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

src/Init/Data/List/Sublist.lean

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

src/Init/Data/List/TakeDrop.lean

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

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

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

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

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

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

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

src/Init/Data/Nat/ToString.lean

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

src/Init/Data/Order/Factories.lean

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

src/Init/Data/Order/MinMaxOn.lean

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

src/Init/Data/Order/Opposite.lean

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

src/Init/Data/Order/PackageFactories.lean

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

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

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

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

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

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

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

src/Init/Data/Repr.lean

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

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

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

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

@@ -28,6 +28,7 @@ open Std Std.Iterators Std.PRange Std.Slice
 
 namespace SubarrayIterator
 
+set_option backward.isDefEq.respectTransparency false in
 theorem step_eq {it : Iter (α := SubarrayIterator α) α} :
     it.step = if h : it.1.xs.start < it.1.xs.stop then
         haveI := it.1.xs.start_le_stop
@@ -126,7 +127,7 @@ public theorem forIn_toList {α : Type u} {s : Subarray α}
     ForIn.forIn s.toList init f = ForIn.forIn s init f :=
   Slice.forIn_toList
 
-@[cbv_eval, grind =]
+@[grind =]
 public theorem forIn_eq_forIn_toList {α : Type u} {s : Subarray α}
     {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
     {f : α → γ → m (ForInStep γ)} :
@@ -214,6 +215,7 @@ public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).stop = min hi xs.size := by
   simp [toSubarray_eq_min, Subarray.stop]
 
+set_option backward.whnf.reducibleClassField false in
 public theorem Subarray.toList_eq {xs : Subarray α} :
     xs.toList = (xs.array.extract xs.start xs.stop).toList := by
   let aslice := xs
@@ -243,7 +245,6 @@ private theorem Std.Internal.List.extract_eq_drop_take' {l : List α} {start sto
       List.length_take, ge_iff_le, h₁]
     omega
 
-@[cbv_eval]
 public theorem Subarray.toList_eq_drop_take {xs : Subarray α} :
     xs.toList = (xs.array.toList.take xs.stop).drop xs.start := by
   rw [Subarray.toList_eq, Array.toList_extract, Std.Internal.List.extract_eq_drop_take']

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

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

src/Init/Data/String/Basic.lean

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

src/Init/Data/String/Bootstrap.lean

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

src/Init/Data/String/Decode.lean

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

src/Init/Data/String/Defs.lean

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

src/Init/Data/String/Iter.lean

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

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

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

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

@@ -1,36 +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.Iterators.Combinators.Monadic.FilterMap
-public import Init.Data.String.Basic
-import Init.Data.String.Slice
-
-set_option doc.verso true
-
-namespace Std
-
-/--
-Appends all the elements in the iterator, in order.
--/
-public def Iter.joinString {α β : Type} [Iterator α Id β] [ToString β]
-    (it : Std.Iter (α := α) β) : String :=
-  (it.map toString).fold (init := "") (· ++ ·)
-
-/--
-Appends the elements of the iterator into a string, placing the separator {name}`s` between them.
--/
-@[inline]
-public def Iter.intercalateString {α β : Type} [Iterator α Id β] [ToString β]
-    (s : String.Slice) (it : Std.Iter (α := α) β) : String :=
-  it.map toString
-    |>.fold (init := none) (fun
-      | none, sl => some sl
-      | some str, sl => some (str ++ s ++ sl))
-    |>.getD ""
-
-end Std

src/Init/Data/String/Iterate.lean

@@ -27,7 +27,6 @@ deriving Inhabited
 /--
 Creates an iterator over the valid positions within {name}`s`, starting at {name}`p`.
 -/
-@[cbv_opaque]
 def positionsFrom {s : Slice} (p : s.Pos) :
     Std.Iter (α := PosIterator s) { p : s.Pos // p ≠ s.endPos } :=
   { internalState := { currPos := p } }
@@ -100,7 +99,7 @@ Examples:
  * {lean}`"abc".toSlice.chars.toList = ['a', 'b', 'c']`
  * {lean}`"ab∀c".toSlice.chars.toList = ['a', 'b', '∀', 'c']`
 -/
-@[cbv_opaque, expose, inline]
+@[expose, inline]
 def chars (s : Slice) :=
   Std.Iter.map (fun ⟨pos, h⟩ => pos.get h) (positions s)
 
@@ -189,7 +188,7 @@ Example:
  * {lean}`"abc".toSlice.revChars.toList = ['c', 'b', 'a']`
  * {lean}`"ab∀c".toSlice.revChars.toList = ['c', '∀', 'b', 'a']`
 -/
-@[cbv_opaque, expose, inline]
+@[expose, inline]
 def revChars (s : Slice) :=
   Std.Iter.map (fun ⟨pos, h⟩ => pos.get h) (revPositions s)
 
@@ -348,7 +347,7 @@ Examples:
  * {lean}`"coffee tea and water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3`
  * {lean}`"coffee tea water".toSlice.foldl (·.push ·) "" = "coffee tea water"`
 -/
-@[cbv_opaque, inline]
+@[inline]
 def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Slice) : α :=
   Std.Iter.fold f init (chars s)
 
@@ -399,7 +398,7 @@ Examples:
  * {lean}`"abc".chars.toList = ['a', 'b', 'c']`
  * {lean}`"ab∀c".chars.toList = ['a', 'b', '∀', 'c']`
 -/
-@[cbv_opaque, inline]
+@[inline]
 def chars (s : String) :=
   (s.toSlice.chars : Std.Iter Char)
 
@@ -433,7 +432,7 @@ Example:
  * {lean}`"abc".revChars.toList = ['c', 'b', 'a']`
  * {lean}`"ab∀c".revChars.toList = ['c', '∀', 'b', 'a']`
 -/
-@[cbv_opaque, inline]
+@[inline]
 def revChars (s : String) :=
   (s.toSlice.revChars : Std.Iter Char)
 
@@ -463,32 +462,4 @@ def revBytes (s : String) :=
 instance {m : Type u → Type v} [Monad m] : ForIn m String Char where
   forIn s b f := ForIn.forIn s.toSlice b f
 
-/--
-Folds a function over a string from the start, accumulating a value starting with {name}`init`. The
-accumulated value is combined with each character in order, using {name}`f`.
-
-Examples:
- * {lean}`"coffee tea water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2`
- * {lean}`"coffee tea and water".foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3`
- * {lean}`"coffee tea water".foldl (·.push ·) "" = "coffee tea water"`
--/
-@[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α :=
-  s.toSlice.foldl f init
-
-@[export lean_string_foldl]
-def Internal.foldlImpl (f : String → Char → String) (init : String) (s : String) : String :=
-  String.foldl f init s
-
-/--
-Folds a function over a string from the right, accumulating a value starting with {lean}`init`. The
-accumulated value is combined with each character in reverse order, using {lean}`f`.
-
-Examples:
- * {lean}`"coffee tea water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 2`
- * {lean}`"coffee tea and water".foldr (fun c n => if c.isWhitespace then n + 1 else n) 0 = 3`
- * {lean}`"coffee tea water".foldr (fun c s => s.push c) "" = "retaw aet eeffoc"`
--/
-@[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α :=
-  s.toSlice.foldr f init
-
 end String

src/Init/Data/String/Lemmas.lean

@@ -17,9 +17,6 @@ public import Init.Data.String.Lemmas.Pattern
 public import Init.Data.String.Lemmas.Slice
 public import Init.Data.String.Lemmas.Iterate
 public import Init.Data.String.Lemmas.Intercalate
-public import Init.Data.String.Lemmas.Iter
-public import Init.Data.String.Lemmas.Hashable
-public import Init.Data.String.Lemmas.TakeDrop
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas

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

@@ -7,7 +7,6 @@ module
 
 prelude
 public import Init.Data.String.Basic
-import all Init.Data.String.Basic
 import Init.Data.ByteArray.Lemmas
 import Init.Data.Nat.MinMax
 
@@ -57,11 +56,6 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
 theorem empty_ne_singleton {c : Char} : "" ≠ singleton c := by
   simp
 
-@[simp]
-theorem ofList_cons {c : Char} {l : List Char} :
-    String.ofList (c :: l) = String.singleton c ++ String.ofList l := by
-  simp [← toList_inj]
-
 @[simp]
 theorem Slice.Pos.copy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.copy = p₂.copy ↔ p₁ = p₂ := by
   simp [String.Pos.ext_iff, Pos.ext_iff]
@@ -84,7 +78,7 @@ theorem getUTF8Byte_toSlice {s : String} {p : String.Pos.Raw} {h} :
 
 @[simp]
 theorem Pos.byte_toSlice {s : String} {p : s.Pos} {h} :
-    p.toSlice.byte h = p.byte (ne_of_apply_ne Pos.toSlice (by simpa using h)) := by
+    p.toSlice.byte h = p.byte (ne_of_apply_ne Pos.toSlice (by simpa)) := by
   simp [byte]
 
 theorem Pos.byte_eq_byte_toSlice {s : String} {p : s.Pos} {h} :
@@ -187,22 +181,6 @@ theorem sliceTo_slice {s : String} {p₁ p₂ h p} :
     (s.slice p₁ p₂ h).sliceTo p = s.slice p₁ (Pos.ofSlice p) Pos.le_ofSlice := by
   ext <;> simp
 
-@[simp]
-theorem Slice.sliceFrom_startPos {s : Slice} : s.sliceFrom s.startPos = s := by
-  ext <;> simp
-
-@[simp]
-theorem Slice.sliceTo_endPos {s : Slice} : s.sliceTo s.endPos = s := by
-  ext <;> simp
-
-@[simp]
-theorem sliceFrom_startPos {s : String} : s.sliceFrom s.startPos = s := by
-  ext <;> simp
-
-@[simp]
-theorem sliceTo_endPos {s : String} : s.sliceTo s.endPos = s := by
-  ext <;> simp
-
 end Iterate
 
 theorem Slice.copy_eq_copy_slice {s : Slice} {pos₁ pos₂ : s.Pos} {h} :
@@ -250,46 +228,4 @@ theorem Pos.get_ofToSlice {s : String} {p : (s.toSlice).Pos} {h} :
 @[simp]
 theorem push_empty {c : Char} : "".push c = singleton c := rfl
 
-namespace Slice.Pos
-
-@[simp]
-theorem nextn_zero {s : Slice} {p : s.Pos} : p.nextn 0 = p := by
-  simp [nextn]
-
-theorem nextn_add_one {s : Slice} {p : s.Pos} :
-    p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n := by
-  simp [nextn]
-
-@[simp]
-theorem nextn_endPos {s : Slice} : s.endPos.nextn n = s.endPos := by
-  cases n <;> simp [nextn_add_one]
-
-end Slice.Pos
-
-namespace Pos
-
-theorem nextn_eq_nextn_toSlice {s : String} {p : s.Pos} : p.nextn n = Pos.ofToSlice (p.toSlice.nextn n) :=
-  (rfl)
-
-@[simp]
-theorem nextn_zero {s : String} {p : s.Pos} : p.nextn 0 = p := by
-  simp [nextn_eq_nextn_toSlice]
-
-theorem nextn_add_one {s : String} {p : s.Pos} :
-    p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n := by
-  simp only [nextn_eq_nextn_toSlice, Slice.Pos.nextn_add_one, endPos_toSlice, toSlice_inj]
-  split <;> simp [Pos.next_toSlice]
-
-theorem nextn_toSlice {s : String} {p : s.Pos} : p.toSlice.nextn n = (p.nextn n).toSlice := by
-  induction n generalizing p with simp_all [nextn_add_one, Slice.Pos.nextn_add_one, apply_dite Pos.toSlice, next_toSlice]
-
-theorem toSlice_nextn {s : String} {p : s.Pos} : (p.nextn n).toSlice = p.toSlice.nextn n :=
-  nextn_toSlice.symm
-
-@[simp]
-theorem nextn_endPos {s : String} : s.endPos.nextn n = s.endPos := by
-  cases n <;> simp [nextn_add_one]
-
-end Pos
-
 end String

src/Init/Data/String/Lemmas/FindPos.lean

@@ -11,8 +11,6 @@ import all Init.Data.String.FindPos
 import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Order
 import Init.Data.Order.Lemmas
-import Init.Data.Option.Lemmas
-import Init.ByCases
 
 public section
 
@@ -219,23 +217,6 @@ theorem Pos.prev_next {s : Slice} {p : s.Pos} {h} : (p.next h).prev (by simp) =
 theorem Pos.next_prev {s : Slice} {p : s.Pos} {h} : (p.prev h).next (by simp) = p :=
   next_eq_iff.2 (by simp)
 
-theorem Pos.prev?_eq_dif {s : Slice} {p : s.Pos} : p.prev? = if h : p = s.startPos then none else some (p.prev h) :=
-  (rfl)
-
-theorem Pos.prev?_eq_some_prev {s : Slice} {p : s.Pos} (h : p ≠ s.startPos) : p.prev? = some (p.prev h) := by
-  simp [Pos.prev?, h]
-
-@[simp]
-theorem Pos.prev?_eq_none_iff {s : Slice} {p : s.Pos} : p.prev? = none ↔ p = s.startPos := by
-  simp [Pos.prev?]
-
-theorem Pos.prev?_eq_none {s : Slice} {p : s.Pos} (h : p = s.startPos) : p.prev? = none :=
-  prev?_eq_none_iff.2 h
-
-@[simp]
-theorem Pos.prev?_startPos {s : Slice} : s.startPos.prev? = none := by
-  simp
-
 end Slice
 
 @[simp]
@@ -447,18 +428,10 @@ theorem Pos.toSlice_prev {s : String} {p : s.Pos} {h} :
     (p.prev h).toSlice = p.toSlice.prev (by simpa [toSlice_inj]) := by
   simp [prev]
 
-theorem Pos.ofToSlice_prev {s : String} {p : s.toSlice.Pos} {h} :
-    Pos.ofToSlice (p.prev h) = (Pos.ofToSlice p).prev (by simpa [← toSlice_inj]) := by
-  simp [prev]
-
 theorem Pos.prev_toSlice {s : String} {p : s.Pos} {h} :
     p.toSlice.prev h = (p.prev (by simpa [← toSlice_inj])).toSlice := by
   simp [prev]
 
-theorem Pos.prev_ofToSlice {s : String} {p : s.toSlice.Pos} {h} :
-    (Pos.ofToSlice p).prev h = Pos.ofToSlice (p.prev (by simpa [← ofToSlice_inj])) := by
-  simp [prev]
-
 theorem Pos.prevn_le {s : String} {p : s.Pos} {n : Nat} :
     p.prevn n ≤ p := by
   simpa [Pos.le_iff, ← offset_toSlice] using Slice.Pos.prevn_le
@@ -471,71 +444,4 @@ theorem Pos.prev_next {s : String} {p : s.Pos} {h} : (p.next h).prev (by simp) =
 theorem Pos.next_prev {s : String} {p : s.Pos} {h} : (p.prev h).next (by simp) = p :=
   next_eq_iff.2 (by simp)
 
-theorem Pos.prev?_eq_prev?_toSlice {s : String} {p : s.Pos} : p.prev? = p.toSlice.prev?.map Pos.ofToSlice :=
-  (rfl)
-
-theorem Pos.prev?_toSlice {s : String} {p : s.Pos} : p.toSlice.prev? = p.prev?.map Pos.toSlice := by
-  simp [prev?_eq_prev?_toSlice]
-
-theorem Pos.prev?_eq_dif {s : String} {p : s.Pos} : p.prev? = if h : p = s.startPos then none else some (p.prev h) := by
-  simp [prev?_eq_prev?_toSlice, Slice.Pos.prev?_eq_dif, apply_dite (Option.map Pos.ofToSlice),
-    ofToSlice_prev]
-
-theorem Pos.prev?_eq_some_prev {s : String} {p : s.Pos} (h : p ≠ s.startPos) : p.prev? = some (p.prev h) := by
-  simp [prev?_eq_prev?_toSlice, Slice.Pos.prev?_eq_some_prev (by simpa : p.toSlice ≠ s.toSlice.startPos),
-    ofToSlice_prev]
-
-@[simp]
-theorem Pos.prev?_eq_none_iff {s : String} {p : s.Pos} : p.prev? = none ↔ p = s.startPos := by
-  simp [prev?_eq_prev?_toSlice]
-
-theorem Pos.prev?_eq_none {s : String} {p : s.Pos} (h : p = s.startPos) : p.prev? = none :=
-  prev?_eq_none_iff.2 h
-
-@[simp]
-theorem Pos.prev?_startPos {s : String} : s.startPos.prev? = none := by
-  simp
-
-namespace Slice.Pos
-
-@[simp]
-theorem prevn_zero {s : Slice} {p : s.Pos} : p.prevn 0 = p := by
-  simp [prevn]
-
-theorem prevn_add_one {s : Slice} {p : s.Pos} :
-    p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n := by
-  simp [prevn]
-
-@[simp]
-theorem prevn_startPos {s : Slice} : s.startPos.prevn n = s.startPos := by
-  cases n <;> simp [prevn_add_one]
-
-end Slice.Pos
-
-namespace Pos
-
-theorem prevn_eq_prevn_toSlice {s : String} {p : s.Pos} : p.prevn n = Pos.ofToSlice (p.toSlice.prevn n) :=
-  (rfl)
-
-@[simp]
-theorem prevn_zero {s : String} {p : s.Pos} : p.prevn 0 = p := by
-  simp [prevn_eq_prevn_toSlice]
-
-theorem prevn_add_one {s : String} {p : s.Pos} :
-    p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n := by
-  simp only [prevn_eq_prevn_toSlice, Slice.Pos.prevn_add_one, startPos_toSlice, toSlice_inj]
-  split <;> simp [Pos.prev_toSlice]
-
-theorem prevn_toSlice {s : String} {p : s.Pos} : p.toSlice.prevn n = (p.prevn n).toSlice := by
-  induction n generalizing p with simp_all [prevn_add_one, Slice.Pos.prevn_add_one, apply_dite Pos.toSlice, prev_toSlice]
-
-theorem toSlice_prevn {s : String} {p : s.Pos} : (p.prevn n).toSlice = p.toSlice.prevn n :=
-  prevn_toSlice.symm
-
-@[simp]
-theorem prevn_startPos {s : String} : s.startPos.prevn n = s.startPos := by
-  cases n <;> simp [prevn_add_one]
-
-end Pos
-
 end String

src/Init/Data/String/Lemmas/Hashable.lean

@@ -1,25 +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.String.Slice
-public import Init.Data.LawfulHashable
-import all Init.Data.String.Slice
-import Init.Data.String.Lemmas.Slice
-
-namespace String
-
-public theorem hash_eq {s : String} : hash s = String.hash s := rfl
-
-namespace Slice
-
-public theorem hash_eq {s : String.Slice} : hash s = String.hash s.copy := (rfl)
-
-public instance : LawfulHashable String.Slice where
-  hash_eq a b hab := by simp [hash_eq, beq_eq_true_iff.1 hab]
-
-end String.Slice

src/Init/Data/String/Lemmas/Intercalate.lean

@@ -10,7 +10,6 @@ public import Init.Data.String.Defs
 import all Init.Data.String.Defs
 public import Init.Data.String.Slice
 import all Init.Data.String.Slice
-import Init.ByCases
 
 public section
 
@@ -43,16 +42,6 @@ theorem intercalate_cons_of_ne_nil {s t : String} {l : List String} (h : l ≠ [
   match l, h with
   | u::l, _ => by simp
 
-theorem intercalate_append_of_ne_nil {l m : List String} {s : String} (hl : l ≠ []) (hm : m ≠ []) :
-    s.intercalate (l ++ m) = s.intercalate l ++ s ++ s.intercalate m := by
-  induction l with
-  | nil => simp_all
-  | cons hd tl ih =>
-    rw [List.cons_append, intercalate_cons_of_ne_nil (by simp_all)]
-    by_cases ht : tl = []
-    · simp_all
-    · simp [ih ht, intercalate_cons_of_ne_nil ht, String.append_assoc]
-
 @[simp]
 theorem toList_intercalate {s : String} {l : List String} :
     (s.intercalate l).toList = s.toList.intercalate (l.map String.toList) := by
@@ -60,23 +49,6 @@ theorem toList_intercalate {s : String} {l : List String} :
   | nil => simp
   | cons hd tl ih => cases tl <;> simp_all
 
-theorem join_eq_foldl : join l = l.foldl (fun r s => r ++ s) "" :=
-  (rfl)
-
-@[simp]
-theorem join_nil : join [] = "" := by
-  simp [join]
-
-@[simp]
-theorem join_cons : join (s :: l) = s ++ join l := by
-  simp only [join, List.foldl_cons, empty_append]
-  conv => lhs; rw [← String.append_empty (s := s)]
-  rw [List.foldl_assoc]
-
-@[simp]
-theorem toList_join {l : List String} : (String.join l).toList = l.flatMap String.toList := by
-  induction l <;> simp_all
-
 namespace Slice
 
 @[simp]
@@ -93,10 +65,6 @@ theorem intercalate_eq {s : Slice} {l : List Slice} :
   | nil => simp [intercalate]
   | cons hd tl ih => cases tl <;> simp_all [intercalate, intercalate.go, intercalateGo_append]
 
-@[simp]
-theorem join_eq {l : List Slice} : join l = String.join (l.map copy) := by
-  simp [join, String.join, List.foldl_map]
-
 end Slice
 
 end String

src/Init/Data/String/Lemmas/Iter.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: Julia Markus Himmel
--/
-module
-
-prelude
-public import Init.Data.String.Iter.Intercalate
-public import Init.Data.String.Slice
-import all Init.Data.String.Iter.Intercalate
-import all Init.Data.String.Defs
-import Init.Data.String.Lemmas.Intercalate
-import Init.Data.Iterators.Lemmas.Consumers.Loop
-import Init.Data.Iterators.Lemmas.Combinators.FilterMap
-
-namespace Std.Iter
-
-@[simp]
-public theorem joinString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [ToString β] {it : Std.Iter (α := α) β} :
-    it.joinString = String.join (it.toList.map toString) := by
-  rw [joinString, String.join, ← foldl_toList, toList_map]
-
-@[simp]
-public theorem intercalateString_eq {α β : Type} [Std.Iterator α Id β] [Std.Iterators.Finite α Id]
-    [ToString β] {s : String.Slice} {it : Std.Iter (α := α) β} :
-    it.intercalateString s = s.copy.intercalate (it.toList.map toString) := by
-  simp only [intercalateString, String.appendSlice_eq, ← foldl_toList, toList_map]
-  generalize s.copy = s
-  suffices ∀ (l m : List String),
-      (l.foldl (init := if m = [] then none else some (s.intercalate m))
-        (fun | none, sl => some sl | some str, sl => some (str ++ s ++ sl))).getD ""
-        = s.intercalate (m ++ l) by
-    simpa [-foldl_toList] using this (it.toList.map toString) []
-  intro l m
-  induction l generalizing m with
-  | nil => cases m <;> simp
-  | cons hd tl ih =>
-    rw [List.append_cons, ← ih, List.foldl_cons]
-    congr
-    simp only [List.append_eq_nil_iff, List.cons_ne_self, and_false, ↓reduceIte]
-    match m with
-    | [] => simp
-    | x::xs =>
-      simp only [reduceCtorEq, ↓reduceIte, List.cons_append, Option.some.injEq]
-      rw [← List.cons_append, String.intercalate_append_of_ne_nil (by simp) (by simp),
-        String.intercalate_singleton]
-
-end Std.Iter

src/Init/Data/String/Lemmas/Iterate.lean

@@ -76,7 +76,7 @@ theorem Model.map_get_positionsFrom_startPos {s : Slice} :
     (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.copy.toList :=
   Model.map_get_positionsFrom_of_splits (splits_startPos s)
 
-@[cbv_eval, simp]
+@[simp]
 theorem toList_positionsFrom {s : Slice} {p : s.Pos} :
     (s.positionsFrom p).toList = Model.positionsFrom p := by
   rw [positionsFrom]
@@ -91,7 +91,7 @@ theorem toList_positionsFrom {s : Slice} {p : s.Pos} :
 theorem toList_positions {s : Slice} : s.positions.toList = Model.positionsFrom s.startPos := by
   simp [positions]
 
-@[cbv_eval, simp]
+@[simp]
 theorem toList_chars {s : Slice} : s.chars.toList = s.copy.toList := by
   simp [chars, Model.map_get_positionsFrom_startPos]
 
@@ -177,30 +177,19 @@ theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} :
 theorem toList_revPositions {s : Slice} : s.revPositions.toList = Model.revPositionsFrom s.endPos := by
   simp [revPositions]
 
-@[cbv_eval, simp]
+@[simp]
 theorem toList_revChars {s : Slice} : s.revChars.toList = s.copy.toList.reverse := by
   simp [revChars, Model.map_get_revPositionsFrom_endPos]
 
 theorem forIn_eq_forIn_chars {m : Type u → Type v} [Monad m] {s : Slice} {b} {f : Char → β → m (ForInStep β)} :
     ForIn.forIn s b f = ForIn.forIn s.chars b f := rfl
 
-@[cbv_eval, simp]
+@[simp]
 theorem forIn_eq_forIn_toList {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : Slice} {b}
     {f : Char → β → m (ForInStep β)} :
     ForIn.forIn s b f = ForIn.forIn s.copy.toList b f := by
   rw [forIn_eq_forIn_chars, ← Std.Iter.forIn_toList, toList_chars]
 
-@[cbv_eval, simp]
-theorem foldl_eq_foldl_toList {α : Type u} {f : α → Char → α} {init : α} {s : Slice} :
-    s.foldl f init = s.copy.toList.foldl f init := by
-  rw [foldl, ← Std.Iter.foldl_toList, toList_chars]
-
-@[simp]
-theorem foldr_eq_foldr_toList {α : Type u} {f : Char → α → α} {init : α} {s : Slice} :
-    s.foldr f init = s.copy.toList.foldr f init := by
-  rw [foldr, ← Std.Iter.foldl_toList, toList_revChars, List.foldl_reverse]
-  congr
-
 end Slice
 
 /--
@@ -262,11 +251,10 @@ theorem toList_positionsFrom {s : String} {p : s.Pos} :
     (s.positionsFrom p).toList = Model.positionsFrom p := by
   simp [positionsFrom, Internal.ofToSliceWithProof, Model.positionsFrom_eq_map]
 
-@[cbv_eval]
 theorem toList_positions {s : String} : s.positions.toList = Model.positionsFrom s.startPos := by
   simp [positions]
 
-@[cbv_eval, simp]
+@[simp]
 theorem toList_chars {s : String} : s.chars.toList = s.toList := by
   simp [chars]
 
@@ -354,7 +342,7 @@ theorem toList_revPositions {s : String} :
     s.revPositions.toList = Model.revPositionsFrom s.endPos := by
   simp [revPositions]
 
-@[cbv_eval, simp]
+@[simp]
 theorem toList_revChars {s : String} : s.revChars.toList = s.toList.reverse := by
   simp [revChars]
 
@@ -367,14 +355,4 @@ theorem forIn_eq_forIn_toList {m : Type u → Type v} [Monad m] [LawfulMonad m]
     ForIn.forIn s b f = ForIn.forIn s.toList b f := by
   rw [forIn_eq_forIn_chars, ← Std.Iter.forIn_toList, toList_chars]
 
-@[simp]
-theorem foldl_eq_foldl_toList {α : Type u} {f : α → Char → α} {init : α} {s : String} :
-    s.foldl f init = s.toList.foldl f init := by
-  simp [foldl]
-
-@[simp]
-theorem foldr_eq_foldr_toList {α : Type u} {f : Char → α → α} {init : α} {s : String} :
-    s.foldr f init = s.toList.foldr f init := by
-  simp [foldr]
-
 end String

src/Init/Data/String/Lemmas/Modify.lean

@@ -49,14 +49,6 @@ theorem toList_mapAux {f : Char → Char} {s : String} {p : s.Pos}
 theorem toList_map {f : Char → Char} {s : String} : (s.map f).toList = s.toList.map f := by
   simp [map, toList_mapAux s.splits_startPos]
 
-/-
-  Used internally by the `cbv` tactic.
--/
-@[cbv_eval]
-theorem map_eq_internal {f : Char → Char} {s : String} : s.map f = .ofList (s.toList.map f) := by
-  apply String.toList_injective
-  simp only [toList_map, toList_ofList]
-
 @[simp]
 theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.length := by
   simp [← length_toList]
@@ -65,14 +57,4 @@ theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.lengt
 theorem map_eq_empty {f : Char → Char} {s : String} : s.map f = "" ↔ s = "" := by
   simp [← toList_eq_nil_iff]
 
-@[simp]
-theorem map_map {f g : Char → Char} {s : String} : String.map g (String.map f s) = String.map (g ∘ f) s  := by
-  apply String.ext
-  simp [List.map_map]
-
-@[simp]
-theorem map_id {s : String} : String.map id s = s := by
-  apply String.ext
-  simp [List.map_id]
-
 end String

src/Init/Data/String/Lemmas/Pattern.lean

@@ -13,4 +13,3 @@ public import Init.Data.String.Lemmas.Pattern.Char
 public import Init.Data.String.Lemmas.Pattern.String
 public import Init.Data.String.Lemmas.Pattern.Split
 public import Init.Data.String.Lemmas.Pattern.Find
-public import Init.Data.String.Lemmas.Pattern.TakeDrop

src/Init/Data/String/Lemmas/Pattern/Basic.lean

@@ -193,13 +193,6 @@ theorem IsLongestMatch.isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternMo
   le := Slice.Pos.le_ofSliceFrom
   isLongestMatch_sliceFrom := by simpa
 
-@[simp]
-theorem isLongestMatchAt_startPos_iff {pat : ρ} [ForwardPatternModel pat] {s : Slice} {endPos : s.Pos} :
-    IsLongestMatchAt pat s.startPos endPos ↔ IsLongestMatch pat endPos := by
-  simpa [isLongestMatchAt_iff] using
-    ⟨fun h => isLongestMatch_of_eq (by simp) (by simp) h,
-     fun h => isLongestMatch_of_eq (by simp) (by simp) h⟩
-
 /--
 Predicate stating that there is a (longest) match starting at the given position.
 -/
@@ -279,24 +272,18 @@ supplied by the {name}`ForwardPatternModel` instance.
 -/
 class LawfulForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPattern pat]
     [ForwardPatternModel pat] : Prop extends LawfulForwardPattern pat where
-  skipPrefix?_eq_some_iff (pos) : ForwardPattern.skipPrefix? pat s = some pos ↔ IsLongestMatch pat pos
+  dropPrefix?_eq_some_iff (pos) : ForwardPattern.dropPrefix? pat s = some pos ↔ IsLongestMatch pat pos
 
 open Classical in
-theorem LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat]
+theorem LawfulForwardPatternModel.dropPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat]
     [LawfulForwardPatternModel pat] {s : Slice} {p₀ : s.Pos} :
-    ForwardPattern.skipPrefix? pat (s.sliceFrom p₀) = none ↔ ¬ MatchesAt pat p₀ := by
+    ForwardPattern.dropPrefix? pat (s.sliceFrom p₀) = none ↔ ¬ MatchesAt pat p₀ := by
   rw [← Decidable.not_iff_not]
-  simp [Option.ne_none_iff_exists', LawfulForwardPatternModel.skipPrefix?_eq_some_iff]
+  simp [Option.ne_none_iff_exists', LawfulForwardPatternModel.dropPrefix?_eq_some_iff]
   refine ⟨fun ⟨p, hp⟩ => ?_, fun ⟨p, hp⟩ => ?_⟩
   · exact ⟨Slice.Pos.ofSliceFrom p, hp.isLongestMatchAt_ofSliceFrom⟩
   · exact ⟨p₀.sliceFrom p hp.le, hp.isLongestMatch_sliceFrom⟩
 
-theorem LawfulForwardPatternModel.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat]
-    [LawfulForwardPatternModel pat] {s : Slice} :
-    ForwardPattern.skipPrefix? pat s = none ↔ ¬ MatchesAt pat s.startPos := by
-  conv => lhs; rw [← sliceFrom_startPos (s := s)]
-  simp [skipPrefix?_sliceFrom_eq_none_iff]
-
 /--
 Inductive predicate stating that a list of search steps represents a valid search from a given
 position in a slice.
@@ -371,8 +358,8 @@ theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPa
           Std.PlausibleIterStep.yield, Std.IterStep.yield.injEq] at heq
         rw [← heq.1, ← heq.2]
         apply IsValidSearchFrom.matched
-        · rw [LawfulForwardPattern.skipPrefixOfNonempty?_eq,
-            LawfulForwardPatternModel.skipPrefix?_eq_some_iff] at heq'
+        · rw [LawfulForwardPattern.dropPrefixOfNonempty?_eq,
+            LawfulForwardPatternModel.dropPrefix?_eq_some_iff] at heq'
           exact heq'.isLongestMatchAt_ofSliceFrom
         · simp only [Std.IterM.toIter]
           apply ih
@@ -385,8 +372,8 @@ theorem LawfulToForwardSearcherModel.defaultImplementation {pat : ρ} [ForwardPa
         apply IsValidSearchFrom.mismatched (by simp) _ (ih _ (by simp))
         intro p' hp' hp''
         obtain rfl : pos = p' := Std.le_antisymm hp' (by simpa using hp'')
-        rwa [LawfulForwardPattern.skipPrefixOfNonempty?_eq,
-          LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff] at heq'
+        rwa [LawfulForwardPattern.dropPrefixOfNonempty?_eq,
+          LawfulForwardPatternModel.dropPrefix?_eq_none_iff] at heq'
     · split at heq <;> simp at heq
     · split at heq <;> simp at heq
 

src/Init/Data/String/Lemmas/Pattern/Char.lean

@@ -57,8 +57,8 @@ theorem isLongestMatchAt_of_get_eq {c : Char} {s : Slice} {pos : s.Pos} {h : pos
   isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩
 
 instance {c : Char} : LawfulForwardPatternModel c where
-  skipPrefix?_eq_some_iff {s} pos := by
-    simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, and_comm, eq_comm (b := pos)]
+  dropPrefix?_eq_some_iff {s} pos := by
+    simp [isLongestMatch_iff, ForwardPattern.dropPrefix?, and_comm, eq_comm (b := pos)]
 
 theorem toSearcher_eq {c : Char} {s : Slice} :
   ToForwardSearcher.toSearcher c s = ToForwardSearcher.toSearcher (· == c) s := (rfl)
@@ -136,36 +136,42 @@ theorem dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} :
 theorem dropPrefix_char_eq_dropPrefix_beq {c : Char} {s : Slice} :
     s.dropPrefix c = s.dropPrefix (· == c) := (rfl)
 
-theorem skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} :
-    s.skipPrefix? c = s.skipPrefix? (· == c) := (rfl)
+theorem Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} :
+    dropPrefix? c s = dropPrefix? (· == c) s := (rfl)
 
-theorem Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} :
-    skipPrefix? c s = skipPrefix? (· == c) s := (rfl)
-
-theorem Pos.skipWhile_char_eq_skipWhile_beq {c : Char} {s : Slice} (curr : s.Pos) :
-    Pos.skipWhile curr c = Pos.skipWhile curr (· == c) := by
-  fun_induction Pos.skipWhile curr c with
+private theorem dropWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) :
+    dropWhile.go s c curr = dropWhile.go s (· == c) curr := by
+  fun_induction dropWhile.go s c curr with
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [Pos.skipWhile]
-    simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h₁, h₂, ih]
+    conv => rhs; rw [dropWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [Pos.skipWhile]
-    simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h, ih]
+    conv => rhs; rw [dropWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [Pos.skipWhile]
-    simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq]
-
-theorem skipPrefixWhile_char_eq_skipPrefixWhile_beq {c : Char} {s : Slice} :
-    s.skipPrefixWhile c = s.skipPrefixWhile (· == c) :=
-  Pos.skipWhile_char_eq_skipWhile_beq s.startPos
+    conv => rhs; rw [dropWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq]
 
 theorem dropWhile_char_eq_dropWhile_beq {c : Char} {s : Slice} :
     s.dropWhile c = s.dropWhile (· == c) := by
-  simp only [dropWhile]; exact congrArg _ skipPrefixWhile_char_eq_skipPrefixWhile_beq
+  simpa only [dropWhile] using dropWhileGo_eq s.startPos
+
+private theorem takeWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) :
+    takeWhile.go s c curr = takeWhile.go s (· == c) curr := by
+  fun_induction takeWhile.go s c curr with
+  | case1 pos nextCurr h₁ h₂ ih =>
+    conv => rhs; rw [takeWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h₁, h₂, ih]
+  | case2 pos nextCurr h ih =>
+    conv => rhs; rw [takeWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih]
+  | case3 pos h =>
+    conv => rhs; rw [takeWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq]
 
 theorem takeWhile_char_eq_takeWhile_beq {c : Char} {s : Slice} :
     s.takeWhile c = s.takeWhile (· == c) := by
-  simp only [takeWhile]; exact congrArg _ skipPrefixWhile_char_eq_skipPrefixWhile_beq
+  simp only [takeWhile]; exact takeWhileGo_eq s.startPos
 
 theorem all_char_eq_all_beq {c : Char} {s : Slice} :
     s.all c = s.all (· == c) := by
@@ -186,41 +192,47 @@ theorem contains_char_eq_contains_beq {c : Char} {s : Slice} :
 theorem endsWith_char_eq_endsWith_beq {c : Char} {s : Slice} :
     s.endsWith c = s.endsWith (· == c) := (rfl)
 
-theorem skipSuffix?_char_eq_skipSuffix?_beq {c : Char} {s : Slice} :
-    s.skipSuffix? c = s.skipSuffix? (· == c) := (rfl)
-
 theorem dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} :
     s.dropSuffix? c = s.dropSuffix? (· == c) := (rfl)
 
 theorem dropSuffix_char_eq_dropSuffix_beq {c : Char} {s : Slice} :
     s.dropSuffix c = s.dropSuffix (· == c) := (rfl)
 
-theorem Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq {c : Char} {s : Slice} :
-    skipSuffix? c s = skipSuffix? (· == c) s := (rfl)
+theorem Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} :
+    dropSuffix? c s = dropSuffix? (· == c) s := (rfl)
 
-theorem Pos.revSkipWhile_char_eq_revSkipWhile_beq {c : Char} {s : Slice} (curr : s.Pos) :
-    Pos.revSkipWhile curr c = Pos.revSkipWhile curr (· == c) := by
-  fun_induction Pos.revSkipWhile curr c with
+private theorem dropEndWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) :
+    dropEndWhile.go s c curr = dropEndWhile.go s (· == c) curr := by
+  fun_induction dropEndWhile.go s c curr with
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [Pos.revSkipWhile]
-    simp [← Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq, h₁, h₂, ih]
+    conv => rhs; rw [dropEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [Pos.revSkipWhile]
-    simp [← Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq, h, ih]
+    conv => rhs; rw [dropEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [Pos.revSkipWhile]
-    simp [← Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq]
-
-theorem skipSuffixWhile_char_eq_skipSuffixWhile_beq {c : Char} {s : Slice} :
-    s.skipSuffixWhile c = s.skipSuffixWhile (· == c) :=
-  Pos.revSkipWhile_char_eq_revSkipWhile_beq s.endPos
+    conv => rhs; rw [dropEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq]
 
 theorem dropEndWhile_char_eq_dropEndWhile_beq {c : Char} {s : Slice} :
     s.dropEndWhile c = s.dropEndWhile (· == c) := by
-  simp only [dropEndWhile]; exact congrArg _ skipSuffixWhile_char_eq_skipSuffixWhile_beq
+  simpa only [dropEndWhile] using dropEndWhileGo_eq s.endPos
+
+private theorem takeEndWhileGo_eq {c : Char} {s : Slice} (curr : s.Pos) :
+    takeEndWhile.go s c curr = takeEndWhile.go s (· == c) curr := by
+  fun_induction takeEndWhile.go s c curr with
+  | case1 pos nextCurr h₁ h₂ ih =>
+    conv => rhs; rw [takeEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih]
+  | case2 pos nextCurr h ih =>
+    conv => rhs; rw [takeEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih]
+  | case3 pos h =>
+    conv => rhs; rw [takeEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq]
 
 theorem takeEndWhile_char_eq_takeEndWhile_beq {c : Char} {s : Slice} :
     s.takeEndWhile c = s.takeEndWhile (· == c) := by
-  simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_char_eq_skipSuffixWhile_beq
+  simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos
 
 end String.Slice

src/Init/Data/String/Lemmas/Pattern/Find/Char.lean

@@ -183,7 +183,7 @@ theorem find?_char_eq_some_iff_splits {c : Char} {s : String} {pos : s.Pos} :
   · rintro ⟨t, u, hsplit, hnotin⟩
     exact ⟨pos.toSlice, ⟨t, u, Pos.splits_toSlice_iff.mpr hsplit, hnotin⟩, by simp⟩
 
-@[cbv_eval, simp]
+@[simp]
 theorem contains_char_eq {c : Char} {s : String} : s.contains c = decide (c ∈ s.toList) := by
   simp [contains_eq_contains_toSlice, Slice.contains_char_eq, copy_toSlice]
 

src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean

@@ -58,7 +58,7 @@ theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s :
   simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff_splits, decide_eq_true_eq,
     decide_eq_false_iff_not]
 
-@[cbv_eval, simp]
+@[simp]
 theorem contains_bool_eq {p : Char → Bool} {s : Slice} : s.contains p = s.copy.toList.any p := by
   rw [Bool.eq_iff_iff, Pattern.Model.contains_eq_true_iff]
   simp only [Pattern.Model.CharPred.matchesAt_iff, ne_eq, List.any_eq_true,

src/Init/Data/String/Lemmas/Pattern/Find/String.lean

@@ -90,12 +90,4 @@ theorem contains_string_eq_false_iff {t s : String} :
     s.contains t = false ↔ ¬(t.toList <:+: s.toList) :=
   Bool.eq_false_iff.trans (not_congr contains_string_iff)
 
-/-
-  Used internally by the `cbv` tactic.
--/
-@[cbv_eval]
-theorem contains_string_eq_internal {t s : String} :
-    s.contains t = t.toList.isInfixOf_internal s.toList := by
-  rw [Bool.eq_iff_iff, contains_string_iff, List.isInfixOf_internal_iff_isInfix]
-
 end String

src/Init/Data/String/Lemmas/Pattern/Pred.lean

@@ -57,8 +57,8 @@ theorem isLongestMatchAt_of_get {p : Char → Bool} {s : Slice} {pos : s.Pos} {h
   isLongestMatchAt_iff.2 ⟨h, by simp [hc]⟩
 
 instance {p : Char → Bool} : LawfulForwardPatternModel p where
-  skipPrefix?_eq_some_iff {s} pos := by
-    simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, and_comm, eq_comm (b := pos)]
+  dropPrefix?_eq_some_iff {s} pos := by
+    simp [isLongestMatch_iff, ForwardPattern.dropPrefix?, and_comm, eq_comm (b := pos)]
 
 instance {p : Char → Bool} : LawfulToForwardSearcherModel p :=
   .defaultImplementation
@@ -126,13 +126,13 @@ theorem matchAt?_eq_matchAt?_decide {p : Char → Prop} [DecidablePred p] {s : S
   ext endPos
   simp [isLongestMatchAt_iff_isLongestMatchAt_decide]
 
-theorem skipPrefix?_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] :
-    ForwardPattern.skipPrefix? p = ForwardPattern.skipPrefix? (decide <| p ·) := rfl
+theorem dropPrefix?_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePred p] :
+    ForwardPattern.dropPrefix? p = ForwardPattern.dropPrefix? (decide <| p ·) := rfl
 
 instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPatternModel p where
-  skipPrefix?_eq_some_iff {s} pos := by
-    rw [skipPrefix?_eq_skipPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide]
-    exact LawfulForwardPatternModel.skipPrefix?_eq_some_iff ..
+  dropPrefix?_eq_some_iff {s} pos := by
+    rw [dropPrefix?_eq_dropPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide]
+    exact LawfulForwardPatternModel.dropPrefix?_eq_some_iff ..
 
 theorem toSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} :
     ToForwardSearcher.toSearcher p s = ToForwardSearcher.toSearcher (decide <| p ·) s := (rfl)
@@ -181,39 +181,43 @@ theorem dropPrefix?_prop_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePre
 theorem dropPrefix_prop_eq_dropPrefix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.dropPrefix p = s.dropPrefix (decide <| p ·) := (rfl)
 
-theorem skipPrefix?_prop_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
-    s.skipPrefix? p = s.skipPrefix? (decide <| p ·) := (rfl)
-
-theorem Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide
+theorem Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide
     {p : Char → Prop} [DecidablePred p] {s : Slice} :
-    skipPrefix? p s = skipPrefix? (decide <| p ·) s := (rfl)
+    dropPrefix? p s = dropPrefix? (decide <| p ·) s := (rfl)
 
-theorem Pos.skipWhile_prop_eq_skipWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
-    (curr : s.Pos) :
-    Pos.skipWhile curr p = Pos.skipWhile curr (decide <| p ·) := by
-  fun_induction Pos.skipWhile curr p with
+private theorem dropWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) :
+    dropWhile.go s p curr = dropWhile.go s (decide <| p ·) curr := by
+  fun_induction dropWhile.go s p curr with
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [Pos.skipWhile]
-    simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h₁, h₂, ih]
+    conv => rhs; rw [dropWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [Pos.skipWhile]
-    simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h, ih]
+    conv => rhs; rw [dropWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [Pos.skipWhile]
-    simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide]
-
-theorem skipPrefixWhile_prop_eq_skipPrefixWhile_decide {p : Char → Prop} [DecidablePred p]
-    {s : Slice} :
-    s.skipPrefixWhile p = s.skipPrefixWhile (decide <| p ·) :=
-  Pos.skipWhile_prop_eq_skipWhile_decide s.startPos
+    conv => rhs; rw [dropWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide]
 
 theorem dropWhile_prop_eq_dropWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.dropWhile p = s.dropWhile (decide <| p ·) := by
-  simp only [dropWhile]; exact congrArg _ skipPrefixWhile_prop_eq_skipPrefixWhile_decide
+  simpa only [dropWhile] using dropWhileGo_eq s.startPos
+
+private theorem takeWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice} (curr : s.Pos) :
+    takeWhile.go s p curr = takeWhile.go s (decide <| p ·) curr := by
+  fun_induction takeWhile.go s p curr with
+  | case1 pos nextCurr h₁ h₂ ih =>
+    conv => rhs; rw [takeWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h₁, h₂, ih]
+  | case2 pos nextCurr h ih =>
+    conv => rhs; rw [takeWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih]
+  | case3 pos h =>
+    conv => rhs; rw [takeWhile.go]
+    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide]
 
 theorem takeWhile_prop_eq_takeWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.takeWhile p = s.takeWhile (decide <| p ·) := by
-  simp only [takeWhile]; exact congrArg _ skipPrefixWhile_prop_eq_skipPrefixWhile_decide
+  simp only [takeWhile]; exact takeWhileGo_eq s.startPos
 
 theorem all_prop_eq_all_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.all p = s.all (decide <| p ·) := by
@@ -235,46 +239,52 @@ theorem contains_prop_eq_contains_decide {p : Char → Prop} [DecidablePred p] {
 theorem endsWith_prop_eq_endsWith_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.endsWith p = s.endsWith (decide <| p ·) := (rfl)
 
-theorem skipSuffix?_prop_eq_skipSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
-    s.skipSuffix? p = s.skipSuffix? (decide <| p ·) := (rfl)
-
 theorem dropSuffix?_prop_eq_dropSuffix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.dropSuffix? p = s.dropSuffix? (decide <| p ·) := (rfl)
 
 theorem dropSuffix_prop_eq_dropSuffix_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.dropSuffix p = s.dropSuffix (decide <| p ·) := (rfl)
 
-theorem Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide
+theorem Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide
     {p : Char → Prop} [DecidablePred p] {s : Slice} :
-    skipSuffix? p s = skipSuffix? (decide <| p ·) s := (rfl)
+    dropSuffix? p s = dropSuffix? (decide <| p ·) s := (rfl)
 
-theorem Pos.revSkipWhile_prop_eq_revSkipWhile_decide {p : Char → Prop} [DecidablePred p]
-    {s : Slice} (curr : s.Pos) :
-    Pos.revSkipWhile curr p = Pos.revSkipWhile curr (decide <| p ·) := by
-  fun_induction Pos.revSkipWhile curr p with
+private theorem dropEndWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice}
+    (curr : s.Pos) :
+    dropEndWhile.go s p curr = dropEndWhile.go s (decide <| p ·) curr := by
+  fun_induction dropEndWhile.go s p curr with
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [Pos.revSkipWhile]
-    simp [← Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide, h₁, h₂, ih]
+    conv => rhs; rw [dropEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [Pos.revSkipWhile]
-    simp [← Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide, h, ih]
+    conv => rhs; rw [dropEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [Pos.revSkipWhile]
-    simp [← Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide]
-
-theorem skipSuffixWhile_prop_eq_skipSuffixWhile_decide {p : Char → Prop} [DecidablePred p]
-    {s : Slice} :
-    s.skipSuffixWhile p = s.skipSuffixWhile (decide <| p ·) :=
-  Pos.revSkipWhile_prop_eq_revSkipWhile_decide s.endPos
+    conv => rhs; rw [dropEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide]
 
 theorem dropEndWhile_prop_eq_dropEndWhile_decide {p : Char → Prop} [DecidablePred p]
     {s : Slice} :
     s.dropEndWhile p = s.dropEndWhile (decide <| p ·) := by
-  simp only [dropEndWhile]; exact congrArg _ skipSuffixWhile_prop_eq_skipSuffixWhile_decide
+  simpa only [dropEndWhile] using dropEndWhileGo_eq s.endPos
+
+private theorem takeEndWhileGo_eq {p : Char → Prop} [DecidablePred p] {s : Slice}
+    (curr : s.Pos) :
+    takeEndWhile.go s p curr = takeEndWhile.go s (decide <| p ·) curr := by
+  fun_induction takeEndWhile.go s p curr with
+  | case1 pos nextCurr h₁ h₂ ih =>
+    conv => rhs; rw [takeEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih]
+  | case2 pos nextCurr h ih =>
+    conv => rhs; rw [takeEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih]
+  | case3 pos h =>
+    conv => rhs; rw [takeEndWhile.go]
+    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide]
 
 theorem takeEndWhile_prop_eq_takeEndWhile_decide {p : Char → Prop} [DecidablePred p]
     {s : Slice} :
     s.takeEndWhile p = s.takeEndWhile (decide <| p ·) := by
-  simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_prop_eq_skipSuffixWhile_decide
+  simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos
 
 end String.Slice

src/Init/Data/String/Lemmas/Pattern/Split/Basic.lean

@@ -35,7 +35,6 @@ This gives a low-level correctness proof from which higher-level API lemmas can
 
 namespace String.Slice.Pattern.Model
 
-@[cbv_opaque]
 public protected noncomputable def split {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {s : Slice}
     (firstRejected curr : s.Pos) (hle : firstRejected ≤ curr) : List s.Subslice :=
   if h : curr = s.endPos then
@@ -154,7 +153,6 @@ end Model
 
 open Model
 
-@[cbv_eval]
 public theorem toList_splitToSubslice_eq_modelSplit {ρ : Type} (pat : ρ) [ForwardPatternModel pat]
     {σ : Slice → Type} [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
     [∀ s, Std.Iterators.Finite (σ s) Id] [LawfulToForwardSearcherModel pat] (s : Slice) :

src/Init/Data/String/Lemmas/Pattern/Split/Char.lean

@@ -23,7 +23,6 @@ import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.Order
 import Init.Data.String.Lemmas.Intercalate
 import Init.Data.List.SplitOn.Lemmas
-import Init.Data.String.Lemmas.Slice
 
 public section
 
@@ -31,7 +30,6 @@ namespace String.Slice
 
 open Pattern.Model Pattern.Model.Char
 
-@[cbv_eval]
 theorem Pattern.Model.split_char_eq_split_beq {c : Char} {s : Slice}
     (f curr : s.Pos) (hle : f ≤ curr) :
     Model.split c f curr hle = Model.split (· == c) f curr hle := by
@@ -71,11 +69,6 @@ theorem Slice.toList_split_intercalate {c : Char} {l : List Slice} (hl : ∀ s
   · simp_all
   · rw [List.splitOn_intercalate] <;> simp_all
 
-theorem Slice.toList_split_intercalate_beq {c : Char} {l : List Slice} (hl : ∀ s ∈ l, c ∉ s.copy.toList) :
-    ((Slice.intercalate (String.singleton c) l).split c).toList ==
-      if l = [] then ["".toSlice] else l := by
-  split <;> simp_all [toList_split_intercalate hl, beq_list_iff]
-
 theorem toList_split_intercalate {c : Char} {l : List String} (hl : ∀ s ∈ l, c ∉ s.toList) :
     ((String.intercalate (String.singleton c) l).split c).toList.map (·.copy) =
       if l = [] then [""] else l := by
@@ -84,9 +77,4 @@ theorem toList_split_intercalate {c : Char} {l : List String} (hl : ∀ s ∈ l,
   · simp_all
   · rw [List.splitOn_intercalate] <;> simp_all
 
-theorem toList_split_intercalate_beq {c : Char} {l : List String} (hl : ∀ s ∈ l, c ∉ s.toList) :
-    ((String.intercalate (String.singleton c) l).split c).toList ==
-      if l = [] then ["".toSlice] else l.map String.toSlice := by
-  split <;> simp_all [toList_split_intercalate hl, Slice.beq_list_iff]
-
 end String