test: add typeclass synthesis scaling benchmarks

This PR adds 9 variable-size benchmarks for typeclass synthesis in
tests/elab_bench/, covering different instance graph shapes:

- synth_chain: linear chain of explicit instances
- synth_diamond_stack: stacked diamonds (exposes synthesis failure at depth 19)
- synth_hypercube: d-dimensional hypercube with conjunctive instances
- synth_ladder_rungs_first / synth_ladder_rails_first: ladder graphs
  testing whether instance declaration order affects performance
- synth_wide_extends: wide fan-in through accumulator chain
- synth_nat_indexed: Nat-parameterized recursive class
- synth_accum_param: accumulating typeclass parameters per level
- synth_nested_param: nested V-chain with P-chain consuming it

Each benchmark programmatically generates class hierarchies at multiple
sizes using command elaborators, times synthesis via Meta.synthInstance,
and emits per-size measurement lines.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

.claude/CLAUDE.md

@@ -16,19 +16,32 @@ 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)
+# Specific test by name (supports regex via ctest -R; double-quote special chars like |)
 CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS='-R grind_ematch'
+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'"
 
 # Rerun only previously failed tests
 CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
 
-# Single test from tests/foo/bar/ (quick check during development)
-CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
-make -C build/release -j "$(nproc)" test ARGS=-R testname'
+# 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
 ```
 
+## 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:

.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-1gb"]', matrix.os)) || matrix.os }}
+    runs-on: ${{ endsWith(matrix.os, '-with-cache') && fromJSON(format('["{0}", "nscloud-git-mirror-5gb"]', matrix.os)) || matrix.os }}
     defaults:
       run:
         shell: ${{ matrix.shell || 'nix develop -c bash -euxo pipefail {0}' }}

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

@@ -0,0 +1,29 @@
+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,15 +61,19 @@ 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: 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}"
+              # 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
               echo "nightly=$LEAN_VERSION_STRING" >> "$GITHUB_OUTPUT"
             else
               # Scheduled: do nothing if commit already has a different tag

CMakeLists.txt

@@ -114,6 +114,7 @@ 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/interp.lean.out.expected

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

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-"):
+    if version1.startswith("leanprover/lean4:nightly-") or version1.startswith("leanprover/lean4-nightly:"):
         return False
     return parse_version(version1) >= parse_version(version2)
 

src/CMakeLists.txt

@@ -762,7 +762,7 @@ if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
   add_dependencies(leancpp copy-cadical)
 endif()
 
-if(STAGE GREATER 0 AND LEANTAR AND INSTALL_LEANTAR)
+if(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 +797,7 @@ if(LLVM AND STAGE GREATER 0)
   set(EXTRA_LEANMAKE_OPTS "LLVM=1")
 endif()
 
-set(STDLIBS Init Std Lean Leanc)
+set(STDLIBS Init Std Lean Leanc LeanIR)
 if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   list(APPEND STDLIBS Lake LeanChecker)
 endif()
@@ -904,9 +904,16 @@ 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 EXISTS "${LEAN_SOURCE_DIR}/Leanc.lean" AND NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
+if(STAGE GREATER 0 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
@@ -926,7 +933,7 @@ if(STAGE GREATER 0 AND CADICAL AND INSTALL_CADICAL)
   install(PROGRAMS "${CADICAL}" DESTINATION bin)
 endif()
 
-if(STAGE GREATER 0 AND LEANTAR AND INSTALL_LEANTAR)
+if(LEANTAR AND INSTALL_LEANTAR)
   install(PROGRAMS "${LEANTAR}" DESTINATION bin)
 endif()
 

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 _ _))
+  inferInstanceAs (WeaklyLawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
 
 public instance [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] :
     LawfulMonadAttach (StateRefT' ω σ m) :=
-  inferInstanceAs (LawfulMonadAttach (ReaderT _ _))
+  inferInstanceAs (LawfulMonadAttach (ReaderT (ST.Ref ω σ) m))
 
 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 ReaderT.pure
+    unfold StateRefT'.lift instMonad._aux_5 ReaderT.pure
     simp only
   monadLift_bind _ _ := by
     simp only [MonadLift.monadLift, bind]
-    unfold StateRefT'.lift ReaderT.bind
+    unfold StateRefT'.lift instMonad._aux_13 ReaderT.bind
     simp only
 
 end StateRefT'

src/Init/Conv.lean

@@ -60,9 +60,6 @@ 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,6 +172,8 @@ 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 at h; exact h.1 _ m)).push (f a (h a (by simp))) := by
+      (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
   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 at H; exact H.1 _ h)).push ⟨a, H a (by simp)⟩ := by
+      (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
   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 `usizeSz` elements in our runtime.
+  We claim this unsafe implementation is correct because an array cannot have more than `USize.size` 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 < usizeSz` 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 < USize.size` 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/Sort/Lemmas.lean

@@ -134,6 +134,7 @@ 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,6 +36,8 @@ 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]
 
@@ -64,3 +66,8 @@ 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/Char/Lemmas.lean

@@ -86,4 +86,16 @@ 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]
+
 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]
+    · simp [coe_ordinal, -toNat_val]
       grind [UInt32.lt_iff_toNat_lt]
   | case2 =>
     rw [Fin.addNat?_eq_some]

src/Init/Data/Int.lean

@@ -18,3 +18,4 @@ 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/Repr.lean

@@ -0,0 +1,24 @@
+/-
+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

@@ -0,0 +1,23 @@
+/-
+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₂`.
 -/
-@[inline, expose]
+@[cbv_opaque, 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
 
-@[always_inline, inline, expose, inherit_doc IterM.attachWith]
+@[cbv_opaque, 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 γ)
 
-@[always_inline, inline, inherit_doc IterM.filterMap, expose]
+@[cbv_opaque, 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 γ)
 
-@[always_inline, inline, inherit_doc IterM.filter, expose]
+@[cbv_opaque, 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 β)
 
-@[always_inline, inline, inherit_doc IterM.map, expose]
+@[cbv_opaque, 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 γ)
 
-@[always_inline, expose, inherit_doc IterM.flatMap]
+@[cbv_opaque, 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,6 +168,13 @@ 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`.
 -/
-@[always_inline, inline]
+@[cbv_opaque, 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
 -/
-@[always_inline, inline, expose]
+@[cbv_opaque, 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.
 -/
-@[always_inline, inline]
+@[cbv_opaque, 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.
 -/
-@[always_inline, inline]
+@[cbv_opaque, 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
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
-theorem Iter.toArray_filter[Finite α Id] {f : β → Bool} :
+@[cbv_eval, 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]
 

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

@@ -254,6 +254,7 @@ public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α
   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]
@@ -261,6 +262,7 @@ 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

@@ -699,18 +699,16 @@ 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]
-  let t := type_of% (it.map f)
-  let t' := type_of% (it.filterMap (some ∘ f))
+  simp only [map, mapWithPostcondition, InternalCombinators.map, filterMap,
+    filterMapWithPostcondition, InternalCombinators.filterMap]
+  unfold Map
   congr
-  · simp [Map]
-  · simp [Map.instIterator, inferInstanceAs]
+  · simp
+  · rw [Map.instIterator_eq_filterMapInstIterator]
     congr
     simp
-  · simp only [map, mapWithPostcondition, InternalCombinators.map, Function.comp_apply, filterMap,
-    filterMapWithPostcondition, InternalCombinators.filterMap]
-    congr
-    · simp [Map]
-    · simp
+  · simp
+  · simp
 
 @[simp]
 theorem IterM.toList_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
@@ -1310,7 +1308,8 @@ 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.instIterator Map.instIteratorLoop Map
+  unfold mapWithPostcondition InternalCombinators.map Map.instIteratorLoop Map
+  rw [Map.instIterator_eq_filterMapInstIterator]
   rw [← InternalCombinators.filterMap, ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
   simp
 

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
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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
 
-@[simp]
+@[cbv_eval ←, 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

@@ -449,7 +449,7 @@ theorem Iter.toArray_eq_fold {α β : Type w} [Iterator α Id β]
   rw [← fold_hom (List.toArray)]
   simp
 
-@[simp]
+@[cbv_eval ←, 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/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]
 
-@[simp, grind =]
+@[cbv_eval, 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]
 
-@[simp, grind =]
+@[cbv_eval, simp, grind =]
 theorem List.toList_iter {l : List β} :
     l.iter.toList = l := by
   simp [List.iter, List.toList_iterM]

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
 -/
-@[always_inline, inline]
+@[cbv_opaque, 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
 -/
-@[always_inline, inline]
+@[cbv_opaque, 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,6 +1246,24 @@ 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/Lemmas.lean

@@ -877,6 +877,11 @@ 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]
 
@@ -1283,6 +1288,13 @@ 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
@@ -1336,6 +1348,16 @@ 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
-  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : Min β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
   exact List.minOn?_append xs ys f
 
 end List

src/Init/Data/List/Sublist.lean

@@ -706,6 +706,11 @@ 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⟩ =>
@@ -1292,6 +1297,31 @@ 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⟩⟩
 
@@ -1299,6 +1329,121 @@ 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,6 +297,14 @@ 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/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)
+  le_of_testBit (by simp [imp_or_left_iff_true])
 
 theorem right_le_or {n m : Nat} : m ≤ n ||| m :=
-  le_of_testBit (by simp)
+  le_of_testBit (by simp [imp_or_right_iff_true])

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

@@ -253,4 +253,16 @@ 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,6 +19,7 @@ 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
 
@@ -94,6 +95,14 @@ protected theorem digitChar_ne {n : Nat} (c : Char)
   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
@@ -110,6 +119,11 @@ 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
@@ -186,6 +200,11 @@ 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
@@ -211,6 +230,14 @@ 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)
@@ -251,4 +278,57 @@ 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 10 (n.digitChar :: cs) init = ofDigitChars 10 cs (10 * 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]
+
+@[simp]
+theorem ofDigitChars_toDigits {n : Nat} : ofDigitChars 10 (toDigits 10 n) 0 = n := by
+  have : 1 < 10 := by decide
+  induction n using base_induction 10 this with
+  | single m hm =>
+    simp [Nat.toDigits_of_lt_base hm, ofDigitChars_cons_digitChar_of_lt_ten hm]
+  | digit m k hk hm ih =>
+    rw [← Nat.toDigits_append_toDigits this hm hk,
+      ofDigitChars_append, ih, Nat.toDigits_of_lt_base hk,
+      ofDigitChars_cons_digitChar_of_lt_ten hk, ofDigitChars_nil]
+
 end Nat

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 α := (inferInstanceAs (LE α)).opposite
-  letI : Min α := (inferInstanceAs (Max α)).oppositeMin
+  letI : LE α := (inferInstance : LE α).opposite
+  letI : Min α := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
-  letI : LT β := (inferInstanceAs (LT β)).opposite
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : LT β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
+  letI : LE β := (inferInstance : 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 β := (inferInstanceAs (LE β)).opposite
-  letI : Min β := (inferInstanceAs (Max β)).oppositeMin
+  letI : LE β := (inferInstance : LE β).opposite
+  letI : Min β := (inferInstance : 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 α := (inferInstanceAs (LE α)).opposite
+  letI : LE α := (inferInstance : LE α).opposite
   -- `DecidableLE` for the opposite order is derived automatically via `OppositeOrderInstances`
   min' a b
 ```

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

@@ -411,6 +411,7 @@ 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 α]
@@ -428,6 +429,7 @@ 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 α]
@@ -443,6 +445,7 @@ 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 α]
@@ -459,6 +462,7 @@ 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 α]
@@ -491,6 +495,7 @@ 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 α) α} :
@@ -502,6 +507,7 @@ 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 α) α} :
@@ -608,6 +614,7 @@ 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
@@ -755,6 +762,7 @@ 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]
@@ -844,6 +852,7 @@ 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
@@ -1011,6 +1020,7 @@ 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 α]
@@ -1224,6 +1234,7 @@ 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 α]
@@ -1330,6 +1341,7 @@ 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
@@ -1473,6 +1485,7 @@ 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}
@@ -1572,6 +1585,7 @@ 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
@@ -1705,6 +1719,7 @@ 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 α]
@@ -1939,6 +1954,7 @@ 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 α]
@@ -2039,6 +2055,7 @@ 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 α] :
@@ -2231,6 +2248,7 @@ 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}
@@ -2340,6 +2358,7 @@ 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 α] :
@@ -2550,6 +2569,7 @@ 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}
@@ -2788,6 +2808,7 @@ 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/Repr.lean

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

@@ -126,7 +126,7 @@ public theorem forIn_toList {α : Type u} {s : Subarray α}
     ForIn.forIn s.toList init f = ForIn.forIn s init f :=
   Slice.forIn_toList
 
-@[grind =]
+@[cbv_eval, 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 γ)} :
@@ -243,6 +243,7 @@ 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/String/Basic.lean

@@ -852,6 +852,10 @@ 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]
@@ -1266,9 +1270,11 @@ 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)⟩
 
@@ -1687,7 +1693,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)) :=
+    ofToSlice (Slice.Pos.next pos.toSlice h) = pos.next (ne_of_apply_ne Pos.toSlice (by simpa using h)) :=
   rfl
 
 @[simp]
@@ -1922,7 +1928,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))).toSlice := by
+    p.toSlice.next h = (p.next (ne_of_apply_ne Pos.toSlice (by simpa using h))).toSlice := by
   simp [Pos.toSlice_next]
 
 theorem Pos.byteIdx_lt_utf8ByteSize {s : String} (p : s.Pos) (h : p ≠ s.endPos) :

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_val_le {c : Char} : c.val.toNat ≤ 0x10ffff := by
+theorem Char.toNat_le {c : Char} : c.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.val.toNat < 128 := by
-    suffices c.val.toNat ≤ 127 by omega
+  have h₀ : c.toNat < 128 := by
+    suffices c.toNat ≤ 127 by omega
     simpa [Char.utf8Size_eq_one_iff, UInt32.le_iff_toNat_le] using h
-  have h₁ : c.val.toNat < 256 := by omega
+  have h₁ : c.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_val_le
+      have := c.toNat_le
       simp only [Nat.reduceAdd, BitVec.lt_def, UInt32.toNat_toBitVec, BitVec.toNat_twoPow,
-        Nat.reducePow, Nat.reduceMod, gt_iff_lt]
+        Nat.reducePow, Nat.reduceMod, gt_iff_lt, Char.toNat_val]
       omega
 
 theorem verify₄_eq_isSome_assemble₄ {w x y z : UInt8} :

src/Init/Data/String/Iter.lean

@@ -6,29 +6,5 @@ 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
+public import Init.Data.String.Iter.Basic
+public import Init.Data.String.Iter.Intercalate

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

@@ -0,0 +1,34 @@
+/-
+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

@@ -0,0 +1,36 @@
+/-
+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 β] [IteratorLoop α Id 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 β] [IteratorLoop α Id 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,6 +27,7 @@ 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 } }
@@ -99,7 +100,7 @@ Examples:
  * {lean}`"abc".toSlice.chars.toList = ['a', 'b', 'c']`
  * {lean}`"ab∀c".toSlice.chars.toList = ['a', 'b', '∀', 'c']`
 -/
-@[expose, inline]
+@[cbv_opaque, expose, inline]
 def chars (s : Slice) :=
   Std.Iter.map (fun ⟨pos, h⟩ => pos.get h) (positions s)
 
@@ -188,7 +189,7 @@ Example:
  * {lean}`"abc".toSlice.revChars.toList = ['c', 'b', 'a']`
  * {lean}`"ab∀c".toSlice.revChars.toList = ['c', '∀', 'b', 'a']`
 -/
-@[expose, inline]
+@[cbv_opaque, expose, inline]
 def revChars (s : Slice) :=
   Std.Iter.map (fun ⟨pos, h⟩ => pos.get h) (revPositions s)
 
@@ -347,7 +348,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"`
 -/
-@[inline]
+@[cbv_opaque, inline]
 def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Slice) : α :=
   Std.Iter.fold f init (chars s)
 
@@ -398,7 +399,7 @@ Examples:
  * {lean}`"abc".chars.toList = ['a', 'b', 'c']`
  * {lean}`"ab∀c".chars.toList = ['a', 'b', '∀', 'c']`
 -/
-@[inline]
+@[cbv_opaque, inline]
 def chars (s : String) :=
   (s.toSlice.chars : Std.Iter Char)
 
@@ -432,7 +433,7 @@ Example:
  * {lean}`"abc".revChars.toList = ['c', 'b', 'a']`
  * {lean}`"ab∀c".revChars.toList = ['c', '∀', 'b', 'a']`
 -/
-@[inline]
+@[cbv_opaque, inline]
 def revChars (s : String) :=
   (s.toSlice.revChars : Std.Iter Char)
 
@@ -462,4 +463,32 @@ 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,6 +17,8 @@ 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
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas

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

@@ -78,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)) := by
+    p.toSlice.byte h = p.byte (ne_of_apply_ne Pos.toSlice (by simpa using h)) := by
   simp [byte]
 
 theorem Pos.byte_eq_byte_toSlice {s : String} {p : s.Pos} {h} :
@@ -181,6 +181,22 @@ 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} :

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

@@ -0,0 +1,25 @@
+/-
+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,6 +10,7 @@ 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
 
@@ -42,6 +43,16 @@ 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

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

@@ -0,0 +1,51 @@
+/-
+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]
+    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id 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]
+    [Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id 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)
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, simp]
 theorem toList_chars {s : Slice} : s.chars.toList = s.copy.toList := by
   simp [chars, Model.map_get_positionsFrom_startPos]
 
@@ -177,19 +177,30 @@ theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} :
 theorem toList_revPositions {s : Slice} : s.revPositions.toList = Model.revPositionsFrom s.endPos := by
   simp [revPositions]
 
-@[simp]
+@[cbv_eval, 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
 
-@[simp]
+@[cbv_eval, 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
 
 /--
@@ -251,10 +262,11 @@ 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]
 
-@[simp]
+@[cbv_eval, simp]
 theorem toList_chars {s : String} : s.chars.toList = s.toList := by
   simp [chars]
 
@@ -342,7 +354,7 @@ theorem toList_revPositions {s : String} :
     s.revPositions.toList = Model.revPositionsFrom s.endPos := by
   simp [revPositions]
 
-@[simp]
+@[cbv_eval, simp]
 theorem toList_revChars {s : String} : s.revChars.toList = s.toList.reverse := by
   simp [revChars]
 
@@ -355,4 +367,14 @@ 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,6 +49,14 @@ 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]

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

@@ -13,3 +13,4 @@ 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,6 +193,13 @@ 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.
 -/
@@ -272,18 +279,24 @@ supplied by the {name}`ForwardPatternModel` instance.
 -/
 class LawfulForwardPatternModel {ρ : Type} (pat : ρ) [ForwardPattern pat]
     [ForwardPatternModel pat] : Prop extends LawfulForwardPattern pat where
-  dropPrefix?_eq_some_iff (pos) : ForwardPattern.dropPrefix? pat s = some pos ↔ IsLongestMatch pat pos
+  skipPrefix?_eq_some_iff (pos) : ForwardPattern.skipPrefix? pat s = some pos ↔ IsLongestMatch pat pos
 
 open Classical in
-theorem LawfulForwardPatternModel.dropPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat]
+theorem LawfulForwardPatternModel.skipPrefix?_sliceFrom_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [ForwardPatternModel pat]
     [LawfulForwardPatternModel pat] {s : Slice} {p₀ : s.Pos} :
-    ForwardPattern.dropPrefix? pat (s.sliceFrom p₀) = none ↔ ¬ MatchesAt pat p₀ := by
+    ForwardPattern.skipPrefix? pat (s.sliceFrom p₀) = none ↔ ¬ MatchesAt pat p₀ := by
   rw [← Decidable.not_iff_not]
-  simp [Option.ne_none_iff_exists', LawfulForwardPatternModel.dropPrefix?_eq_some_iff]
+  simp [Option.ne_none_iff_exists', LawfulForwardPatternModel.skipPrefix?_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.
@@ -358,8 +371,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.dropPrefixOfNonempty?_eq,
-            LawfulForwardPatternModel.dropPrefix?_eq_some_iff] at heq'
+        · rw [LawfulForwardPattern.skipPrefixOfNonempty?_eq,
+            LawfulForwardPatternModel.skipPrefix?_eq_some_iff] at heq'
           exact heq'.isLongestMatchAt_ofSliceFrom
         · simp only [Std.IterM.toIter]
           apply ih
@@ -372,8 +385,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.dropPrefixOfNonempty?_eq,
-          LawfulForwardPatternModel.dropPrefix?_eq_none_iff] at heq'
+        rwa [LawfulForwardPattern.skipPrefixOfNonempty?_eq,
+          LawfulForwardPatternModel.skipPrefix?_sliceFrom_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
-  dropPrefix?_eq_some_iff {s} pos := by
-    simp [isLongestMatch_iff, ForwardPattern.dropPrefix?, and_comm, eq_comm (b := pos)]
+  skipPrefix?_eq_some_iff {s} pos := by
+    simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, and_comm, eq_comm (b := pos)]
 
 theorem toSearcher_eq {c : Char} {s : Slice} :
   ToForwardSearcher.toSearcher c s = ToForwardSearcher.toSearcher (· == c) s := (rfl)
@@ -136,42 +136,36 @@ 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 Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq {c : Char} {s : Slice} :
-    dropPrefix? c s = dropPrefix? (· == c) s := (rfl)
+theorem skipPrefix?_char_eq_skipPrefix?_beq {c : Char} {s : Slice} :
+    s.skipPrefix? c = s.skipPrefix? (· == c) := (rfl)
 
-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
+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
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h₁, h₂, ih]
+    conv => rhs; rw [Pos.skipWhile]
+    simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq, h, ih]
+    conv => rhs; rw [Pos.skipWhile]
+    simp [← Pattern.ForwardPattern.skipPrefix?_char_eq_skipPrefix?_beq, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_char_eq_dropPrefix?_beq]
+    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
 
 theorem dropWhile_char_eq_dropWhile_beq {c : Char} {s : Slice} :
     s.dropWhile c = s.dropWhile (· == c) := by
-  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]
+  simp only [dropWhile]; exact congrArg _ skipPrefixWhile_char_eq_skipPrefixWhile_beq
 
 theorem takeWhile_char_eq_takeWhile_beq {c : Char} {s : Slice} :
     s.takeWhile c = s.takeWhile (· == c) := by
-  simp only [takeWhile]; exact takeWhileGo_eq s.startPos
+  simp only [takeWhile]; exact congrArg _ skipPrefixWhile_char_eq_skipPrefixWhile_beq
 
 theorem all_char_eq_all_beq {c : Char} {s : Slice} :
     s.all c = s.all (· == c) := by
@@ -192,47 +186,41 @@ 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.dropSuffix?_char_eq_dropSuffix?_beq {c : Char} {s : Slice} :
-    dropSuffix? c s = dropSuffix? (· == c) s := (rfl)
+theorem Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq {c : Char} {s : Slice} :
+    skipSuffix? c s = skipSuffix? (· == c) s := (rfl)
 
-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
+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
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h₁, h₂, ih]
+    conv => rhs; rw [Pos.revSkipWhile]
+    simp [← Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq, h, ih]
+    conv => rhs; rw [Pos.revSkipWhile]
+    simp [← Pattern.BackwardPattern.skipSuffix?_char_eq_skipSuffix?_beq, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_char_eq_dropSuffix?_beq]
+    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
 
 theorem dropEndWhile_char_eq_dropEndWhile_beq {c : Char} {s : Slice} :
     s.dropEndWhile c = s.dropEndWhile (· == c) := by
-  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]
+  simp only [dropEndWhile]; exact congrArg _ skipSuffixWhile_char_eq_skipSuffixWhile_beq
 
 theorem takeEndWhile_char_eq_takeEndWhile_beq {c : Char} {s : Slice} :
     s.takeEndWhile c = s.takeEndWhile (· == c) := by
-  simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos
+  simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_char_eq_skipSuffixWhile_beq
 
 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⟩
 
-@[simp]
+@[cbv_eval, 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]
 
-@[simp]
+@[cbv_eval, 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,4 +90,12 @@ 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
-  dropPrefix?_eq_some_iff {s} pos := by
-    simp [isLongestMatch_iff, ForwardPattern.dropPrefix?, and_comm, eq_comm (b := pos)]
+  skipPrefix?_eq_some_iff {s} pos := by
+    simp [isLongestMatch_iff, ForwardPattern.skipPrefix?, 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 dropPrefix?_eq_dropPrefix?_decide {p : Char → Prop} [DecidablePred p] :
-    ForwardPattern.dropPrefix? p = ForwardPattern.dropPrefix? (decide <| p ·) := rfl
+theorem skipPrefix?_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] :
+    ForwardPattern.skipPrefix? p = ForwardPattern.skipPrefix? (decide <| p ·) := rfl
 
 instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPatternModel p where
-  dropPrefix?_eq_some_iff {s} pos := by
-    rw [dropPrefix?_eq_dropPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide]
-    exact LawfulForwardPatternModel.dropPrefix?_eq_some_iff ..
+  skipPrefix?_eq_some_iff {s} pos := by
+    rw [skipPrefix?_eq_skipPrefix?_decide, isLongestMatch_iff_isLongestMatch_decide]
+    exact LawfulForwardPatternModel.skipPrefix?_eq_some_iff ..
 
 theorem toSearcher_eq {p : Char → Prop} [DecidablePred p] {s : Slice} :
     ToForwardSearcher.toSearcher p s = ToForwardSearcher.toSearcher (decide <| p ·) s := (rfl)
@@ -181,43 +181,39 @@ 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 Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide
-    {p : Char → Prop} [DecidablePred p] {s : Slice} :
-    dropPrefix? p s = dropPrefix? (decide <| p ·) s := (rfl)
+theorem skipPrefix?_prop_eq_skipPrefix?_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
+    s.skipPrefix? p = s.skipPrefix? (decide <| p ·) := (rfl)
 
-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
+theorem Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide
+    {p : Char → Prop} [DecidablePred p] {s : Slice} :
+    skipPrefix? p s = skipPrefix? (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
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h₁, h₂, ih]
+    conv => rhs; rw [Pos.skipWhile]
+    simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide, h, ih]
+    conv => rhs; rw [Pos.skipWhile]
+    simp [← Pattern.ForwardPattern.skipPrefix?_prop_eq_skipPrefix?_decide, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_prop_eq_dropPrefix?_decide]
+    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
 
 theorem dropWhile_prop_eq_dropWhile_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.dropWhile p = s.dropWhile (decide <| p ·) := by
-  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]
+  simp only [dropWhile]; exact congrArg _ skipPrefixWhile_prop_eq_skipPrefixWhile_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 takeWhileGo_eq s.startPos
+  simp only [takeWhile]; exact congrArg _ skipPrefixWhile_prop_eq_skipPrefixWhile_decide
 
 theorem all_prop_eq_all_decide {p : Char → Prop} [DecidablePred p] {s : Slice} :
     s.all p = s.all (decide <| p ·) := by
@@ -239,52 +235,46 @@ 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.dropSuffix?_prop_eq_dropSuffix?_decide
+theorem Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide
     {p : Char → Prop} [DecidablePred p] {s : Slice} :
-    dropSuffix? p s = dropSuffix? (decide <| p ·) s := (rfl)
+    skipSuffix? p s = skipSuffix? (decide <| p ·) s := (rfl)
 
-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
+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
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h₁, h₂, ih]
+    conv => rhs; rw [Pos.revSkipWhile]
+    simp [← Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide, h, ih]
+    conv => rhs; rw [Pos.revSkipWhile]
+    simp [← Pattern.BackwardPattern.skipSuffix?_prop_eq_skipSuffix?_decide, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_prop_eq_dropSuffix?_decide]
+    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
 
 theorem dropEndWhile_prop_eq_dropEndWhile_decide {p : Char → Prop} [DecidablePred p]
     {s : Slice} :
     s.dropEndWhile p = s.dropEndWhile (decide <| p ·) := by
-  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]
+  simp only [dropEndWhile]; exact congrArg _ skipSuffixWhile_prop_eq_skipSuffixWhile_decide
 
 theorem takeEndWhile_prop_eq_takeEndWhile_decide {p : Char → Prop} [DecidablePred p]
     {s : Slice} :
     s.takeEndWhile p = s.takeEndWhile (decide <| p ·) := by
-  simpa only [takeEndWhile] using takeEndWhileGo_eq s.endPos
+  simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_prop_eq_skipSuffixWhile_decide
 
 end String.Slice

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

@@ -35,6 +35,7 @@ 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
@@ -153,6 +154,7 @@ 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,6 +23,7 @@ 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
 
@@ -30,6 +31,7 @@ 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
@@ -69,6 +71,11 @@ 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
@@ -77,4 +84,9 @@ 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

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

@@ -58,12 +58,33 @@ theorem toList_split_bool {s : Slice} {p : Char → Bool} :
     (s.split p).toList.map Slice.copy = (s.copy.toList.splitOnP p).map String.ofList := by
   simp [toList_split_eq_splitToSubslice, ← toList_splitToSubslice_bool]
 
+/-
+  Used internally by the `cbv` tactic.
+-/
+@[cbv_eval]
+theorem Pattern.Model.split_bool_eq_internal {p : Char → Bool} {s : Slice} (f curr : s.Pos) (hle : f ≤ curr) :
+    Model.split p f curr hle =
+      if h : curr = s.endPos then [s.subslice _ _ hle]
+      else if p (curr.get h) then
+        s.subslice _ _ hle :: Model.split p (curr.next h) (curr.next h) (by simp [Std.le_refl])
+      else Model.split p f (curr.next h) (by simp [Std.le_trans hle _]) := by
+  by_cases h : curr = s.endPos
+  · simp only [h, split_endPos, subslice_endPos, ↓reduceDIte]
+  · simp only [h, ↓reduceDIte]
+    by_cases hp : p (curr.get h)
+    · simp only [hp, ↓reduceIte]
+      exact split_eq_of_isLongestMatchAt (isLongestMatchAt_of_get hp)
+    · rw [Bool.not_eq_true] at hp
+      simp only [hp, Bool.false_eq_true, ↓reduceIte]
+      exact split_eq_next_of_not_matchesAt h (not_matchesAt_of_get hp)
+
 end
 
 section
 
 open Pattern.Model Pattern.Model.CharPred.Decidable
 
+@[cbv_eval]
 theorem Pattern.Model.split_eq_split_decide {p : Char → Prop} [DecidablePred p] {s : Slice}
     (f curr : s.Pos) (hle : f ≤ curr) :
     Model.split p f curr hle = Model.split (decide <| p ·) f curr hle := by

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

@@ -55,6 +55,12 @@ theorem isLongestMatchAt_iff_splits {pat s : Slice} {pos₁ pos₂ : s.Pos} (h :
       pos₂.Splits (t₁ ++ pat.copy) t₂ := by
   simp only [isLongestMatchAt_iff h, copy_slice_eq_iff_splits]
 
+theorem isLongestMatch_iff_splits {pat s : Slice} {pos : s.Pos} (h : pat.isEmpty = false) :
+    IsLongestMatch pat pos ↔ ∃ t, pos.Splits pat.copy t := by
+  simp only [← isLongestMatchAt_startPos_iff, isLongestMatchAt_iff_splits h, splits_startPos_iff,
+    and_assoc, exists_and_left, exists_eq_left, empty_append]
+  exact ⟨fun ⟨h, _, h'⟩ => ⟨h, h'⟩, fun ⟨h, h'⟩ => ⟨h, h'.eq_append.symm, h'⟩⟩
+
 theorem isLongestMatchAt_iff_extract {pat s : Slice} {pos₁ pos₂ : s.Pos} (h : pat.isEmpty = false) :
     IsLongestMatchAt pat pos₁ pos₂ ↔
       s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.copy.toByteArray := by

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

@@ -39,9 +39,9 @@ theorem startsWith_iff {pat s : Slice} : startsWith pat s ↔ ∃ t, s.copy = pa
   · rintro ⟨t, rfl⟩
     simp [-size_toByteArray, ByteArray.extract_append]
 
-theorem dropPrefix?_eq_some_iff {pat s : Slice} {pos : s.Pos} :
-    dropPrefix? pat s = some pos ↔ (s.sliceTo pos).copy = pat.copy := by
-  fun_cases dropPrefix? with
+theorem skipPrefix?_eq_some_iff {pat s : Slice} {pos : s.Pos} :
+    skipPrefix? pat s = some pos ↔ (s.sliceTo pos).copy = pat.copy := by
+  fun_cases skipPrefix? with
   | case1 h =>
     simp only [offset_startPos, Pos.Raw.offsetBy_zero, Option.some.injEq]
     obtain ⟨t, ht⟩ := startsWith_iff.1 h
@@ -58,8 +58,17 @@ theorem dropPrefix?_eq_some_iff {pat s : Slice} {pos : s.Pos} :
     have := h (s.sliceFrom pos).copy
     simp [← heq, pos.splits.eq_append] at this
 
-theorem isSome_dropPrefix? {pat s : Slice} : (dropPrefix? pat s).isSome = startsWith pat s := by
-  fun_cases dropPrefix? <;> simp_all
+theorem isSome_skipPrefix? {pat s : Slice} : (skipPrefix? pat s).isSome = startsWith pat s := by
+  fun_cases skipPrefix? <;> simp_all
+
+public theorem startsWith_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    ForwardPattern.startsWith pat s = true := by
+  suffices pat.copy = "" by simp [ForwardPattern.startsWith, startsWith_iff, this]
+  simpa
+
+public theorem skipPrefix?_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    ForwardPattern.skipPrefix? pat s = some s.startPos := by
+  simpa [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff]
 
 end ForwardSliceSearcher
 
@@ -69,10 +78,10 @@ open Pattern.ForwardSliceSearcher
 
 public theorem lawfulForwardPatternModel {pat : Slice} (hpat : pat.isEmpty = false) :
     LawfulForwardPatternModel pat where
-  dropPrefixOfNonempty?_eq h := rfl
-  startsWith_eq s := isSome_dropPrefix?.symm
-  dropPrefix?_eq_some_iff pos := by
-    simp [ForwardPattern.dropPrefix?, dropPrefix?_eq_some_iff, isLongestMatch_iff hpat]
+  skipPrefixOfNonempty?_eq h := rfl
+  startsWith_eq s := isSome_skipPrefix?.symm
+  skipPrefix?_eq_some_iff pos := by
+    simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff hpat]
 
 end Model.ForwardSliceSearcher
 
@@ -82,10 +91,10 @@ open Pattern.ForwardSliceSearcher
 
 public theorem lawfulForwardPatternModel {pat : String} (hpat : pat ≠ "") :
     LawfulForwardPatternModel pat where
-  dropPrefixOfNonempty?_eq h := rfl
-  startsWith_eq s := isSome_dropPrefix?.symm
-  dropPrefix?_eq_some_iff pos := by
-    simp [ForwardPattern.dropPrefix?, dropPrefix?_eq_some_iff, isLongestMatch_iff hpat]
+  skipPrefixOfNonempty?_eq h := rfl
+  startsWith_eq s := isSome_skipPrefix?.symm
+  skipPrefix?_eq_some_iff pos := by
+    simp [ForwardPattern.skipPrefix?, skipPrefix?_eq_some_iff, isLongestMatch_iff hpat]
 
 end Model.ForwardStringSearcher
 
@@ -100,43 +109,38 @@ public theorem dropPrefix?_string_eq_dropPrefix?_toSlice {pat : String} {s : Sli
 public theorem dropPrefix_string_eq_dropPrefix_toSlice {pat : String} {s : Slice} :
     s.dropPrefix pat = s.dropPrefix pat.toSlice := (rfl)
 
-public theorem Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice
-    {pat : String} {s : Slice} :
-    dropPrefix? pat s = dropPrefix? pat.toSlice s := (rfl)
+public theorem skipPrefix?_string_eq_skipPrefix?_toSlice {pat : String} {s : Slice} :
+    s.skipPrefix? pat = s.skipPrefix? pat.toSlice := (rfl)
 
-private theorem dropWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) :
-    dropWhile.go s pat curr = dropWhile.go s pat.toSlice curr := by
-  fun_induction dropWhile.go s pat curr with
+public theorem Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice
+    {pat : String} {s : Slice} :
+    skipPrefix? pat s = skipPrefix? pat.toSlice s := (rfl)
+
+public theorem Pos.skipWhile_string_eq_skipWhile_toSlice {pat : String} {s : Slice}
+    (curr : s.Pos) :
+    Pos.skipWhile curr pat = Pos.skipWhile curr pat.toSlice := by
+  fun_induction Pos.skipWhile curr pat with
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h₁, h₂, ih]
+    conv => rhs; rw [Pos.skipWhile]
+    simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h, ih]
+    conv => rhs; rw [Pos.skipWhile]
+    simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [dropWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice]
+    conv => rhs; rw [Pos.skipWhile]
+    simp [← Pattern.ForwardPattern.skipPrefix?_string_eq_skipPrefix?_toSlice]
+
+public theorem skipPrefixWhile_string_eq_skipPrefixWhile_toSlice {pat : String} {s : Slice} :
+    s.skipPrefixWhile pat = s.skipPrefixWhile pat.toSlice :=
+  Pos.skipWhile_string_eq_skipWhile_toSlice s.startPos
 
 public theorem dropWhile_string_eq_dropWhile_toSlice {pat : String} {s : Slice} :
     s.dropWhile pat = s.dropWhile pat.toSlice := by
-  simpa only [dropWhile] using dropWhileGo_string_eq s.startPos
-
-private theorem takeWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) :
-    takeWhile.go s pat curr = takeWhile.go s pat.toSlice curr := by
-  fun_induction takeWhile.go s pat curr with
-  | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [takeWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h₁, h₂, ih]
-  | case2 pos nextCurr h ih =>
-    conv => rhs; rw [takeWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice, h, ih]
-  | case3 pos h =>
-    conv => rhs; rw [takeWhile.go]
-    simp [← Pattern.ForwardPattern.dropPrefix?_string_eq_dropPrefix?_toSlice]
+  simp only [dropWhile]; exact congrArg _ skipPrefixWhile_string_eq_skipPrefixWhile_toSlice
 
 public theorem takeWhile_string_eq_takeWhile_toSlice {pat : String} {s : Slice} :
     s.takeWhile pat = s.takeWhile pat.toSlice := by
-  simp only [takeWhile]; exact takeWhileGo_string_eq s.startPos
+  simp only [takeWhile]; exact congrArg _ skipPrefixWhile_string_eq_skipPrefixWhile_toSlice
 
 public theorem all_string_eq_all_toSlice {pat : String} {s : Slice} :
     s.all pat = s.all pat.toSlice := by
@@ -145,48 +149,43 @@ public theorem all_string_eq_all_toSlice {pat : String} {s : Slice} :
 public theorem endsWith_string_eq_endsWith_toSlice {pat : String} {s : Slice} :
     s.endsWith pat = s.endsWith pat.toSlice := (rfl)
 
+public theorem skipSuffix?_string_eq_skipSuffix?_toSlice {pat : String} {s : Slice} :
+    s.skipSuffix? pat = s.skipSuffix? pat.toSlice := (rfl)
+
 public theorem dropSuffix?_string_eq_dropSuffix?_toSlice {pat : String} {s : Slice} :
     s.dropSuffix? pat = s.dropSuffix? pat.toSlice := (rfl)
 
 public theorem dropSuffix_string_eq_dropSuffix_toSlice {pat : String} {s : Slice} :
     s.dropSuffix pat = s.dropSuffix pat.toSlice := (rfl)
 
-public theorem Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice
+public theorem Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice
     {pat : String} {s : Slice} :
-    dropSuffix? pat s = dropSuffix? pat.toSlice s := (rfl)
+    skipSuffix? pat s = skipSuffix? pat.toSlice s := (rfl)
 
-private theorem dropEndWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) :
-    dropEndWhile.go s pat curr = dropEndWhile.go s pat.toSlice curr := by
-  fun_induction dropEndWhile.go s pat curr with
+public theorem Pos.revSkipWhile_string_eq_revSkipWhile_toSlice {pat : String} {s : Slice}
+    (curr : s.Pos) :
+    Pos.revSkipWhile curr pat = Pos.revSkipWhile curr pat.toSlice := by
+  fun_induction Pos.revSkipWhile curr pat with
   | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h₁, h₂, ih]
+    conv => rhs; rw [Pos.revSkipWhile]
+    simp [← Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice, h₁, h₂, ih]
   | case2 pos nextCurr h ih =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h, ih]
+    conv => rhs; rw [Pos.revSkipWhile]
+    simp [← Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice, h, ih]
   | case3 pos h =>
-    conv => rhs; rw [dropEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice]
+    conv => rhs; rw [Pos.revSkipWhile]
+    simp [← Pattern.BackwardPattern.skipSuffix?_string_eq_skipSuffix?_toSlice]
+
+public theorem skipSuffixWhile_string_eq_skipSuffixWhile_toSlice {pat : String} {s : Slice} :
+    s.skipSuffixWhile pat = s.skipSuffixWhile pat.toSlice :=
+  Pos.revSkipWhile_string_eq_revSkipWhile_toSlice s.endPos
 
 public theorem dropEndWhile_string_eq_dropEndWhile_toSlice {pat : String} {s : Slice} :
     s.dropEndWhile pat = s.dropEndWhile pat.toSlice := by
-  simpa only [dropEndWhile] using dropEndWhileGo_string_eq s.endPos
-
-private theorem takeEndWhileGo_string_eq {pat : String} {s : Slice} (curr : s.Pos) :
-    takeEndWhile.go s pat curr = takeEndWhile.go s pat.toSlice curr := by
-  fun_induction takeEndWhile.go s pat curr with
-  | case1 pos nextCurr h₁ h₂ ih =>
-    conv => rhs; rw [takeEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h₁, h₂, ih]
-  | case2 pos nextCurr h ih =>
-    conv => rhs; rw [takeEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice, h, ih]
-  | case3 pos h =>
-    conv => rhs; rw [takeEndWhile.go]
-    simp [← Pattern.BackwardPattern.dropSuffix?_string_eq_dropSuffix?_toSlice]
+  simp only [dropEndWhile]; exact congrArg _ skipSuffixWhile_string_eq_skipSuffixWhile_toSlice
 
 public theorem takeEndWhile_string_eq_takeEndWhile_toSlice {pat : String} {s : Slice} :
     s.takeEndWhile pat = s.takeEndWhile pat.toSlice := by
-  simpa only [takeEndWhile] using takeEndWhileGo_string_eq s.endPos
+  simp only [takeEndWhile]; exact congrArg _ skipSuffixWhile_string_eq_skipSuffixWhile_toSlice
 
 end String.Slice

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

@@ -0,0 +1,12 @@
+/-
+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.String.Lemmas.Pattern.TakeDrop.Basic
+public import Init.Data.String.Lemmas.Pattern.TakeDrop.Char
+public import Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
+public import Init.Data.String.Lemmas.Pattern.TakeDrop.String

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

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Slice
+public import Init.Data.String.TakeDrop
+public import Init.Data.String.Lemmas.Pattern.Basic
+import all Init.Data.String.Slice
+import all Init.Data.String.TakeDrop
+
+public section
+
+open String.Slice Pattern Model
+
+namespace String
+
+namespace Slice
+
+theorem skipPrefix?_eq_forwardPatternSkipPrefix? {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : Slice} :
+    s.skipPrefix? pat = ForwardPattern.skipPrefix? pat s := (rfl)
+
+theorem startsWith_eq_forwardPatternStartsWith {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : Slice} :
+    s.startsWith pat = ForwardPattern.startsWith pat s := (rfl)
+
+theorem dropPrefix?_eq_map_skipPrefix? {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : Slice} :
+    s.dropPrefix? pat = (s.skipPrefix? pat).map s.sliceFrom := (rfl)
+
+theorem Pattern.Model.skipPrefix?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+    [LawfulForwardPatternModel pat] {s : Slice} {pos : s.Pos} :
+    s.skipPrefix? pat = some pos ↔ IsLongestMatch pat pos := by
+  rw [skipPrefix?_eq_forwardPatternSkipPrefix?, LawfulForwardPatternModel.skipPrefix?_eq_some_iff]
+
+theorem Pattern.Model.skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+    [LawfulForwardPatternModel pat] {s : Slice} :
+    s.skipPrefix? pat = none ↔ ¬ MatchesAt pat s.startPos := by
+  rw [skipPrefix?_eq_forwardPatternSkipPrefix?, LawfulForwardPatternModel.skipPrefix?_eq_none_iff]
+
+@[simp]
+theorem isSome_skipPrefix? {ρ : Type} {pat : ρ} [ForwardPattern pat] [LawfulForwardPattern pat] {s : Slice} :
+    (s.skipPrefix? pat).isSome = s.startsWith pat := by
+  rw [startsWith_eq_forwardPatternStartsWith, skipPrefix?, LawfulForwardPattern.startsWith_eq]
+
+theorem Pattern.Model.startsWith_eq_false_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+    [LawfulForwardPatternModel pat] {s : Slice} :
+    s.startsWith pat = false ↔ ¬ MatchesAt pat s.startPos := by
+  rw [← Pattern.Model.skipPrefix?_eq_none_iff, ← Option.isNone_iff_eq_none,
+    ← isSome_skipPrefix?, Option.isSome_eq_false_iff]
+
+theorem Pattern.Model.startsWith_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+    [LawfulForwardPatternModel pat] {s : Slice} :
+    s.startsWith pat = true ↔ MatchesAt pat s.startPos := by
+  rw [← Bool.not_eq_false, startsWith_eq_false_iff, Classical.not_not]
+
+@[simp]
+theorem skipPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [LawfulForwardPattern pat]
+    {s : Slice} : s.skipPrefix? pat = none ↔ s.startsWith pat = false := by
+  rw [← Option.isNone_iff_eq_none, ← Option.isSome_eq_false_iff, isSome_skipPrefix?]
+
+@[simp]
+theorem dropPrefix?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPattern pat] [LawfulForwardPattern pat]
+    {s : Slice} : s.dropPrefix? pat = none ↔ s.startsWith pat = false := by
+  simp [dropPrefix?_eq_map_skipPrefix?]
+
+theorem Pattern.Model.eq_append_of_dropPrefix?_eq_some {ρ : Type} {pat : ρ} [ForwardPatternModel pat] [ForwardPattern pat]
+    [LawfulForwardPatternModel pat] {s res : Slice} (h : s.dropPrefix? pat = some res) :
+    ∃ t, ForwardPatternModel.Matches pat t ∧ s.copy = t ++ res.copy := by
+  simp only [dropPrefix?_eq_map_skipPrefix?, Option.map_eq_some_iff, skipPrefix?_eq_some_iff] at h
+  obtain ⟨pos, h₁, h₂⟩ := h
+  exact ⟨(s.sliceTo pos).copy, h₁.isMatch.matches_copy, by simp [← h₂, ← copy_eq_copy_sliceTo]⟩
+
+end Slice
+
+theorem skipPrefix?_eq_skipPrefix?_toSlice {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : String} :
+    s.skipPrefix? pat = (s.toSlice.skipPrefix? pat).map Pos.ofToSlice := (rfl)
+
+theorem startsWith_eq_startsWith_toSlice {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : String} :
+    s.startsWith pat = s.toSlice.startsWith pat := (rfl)
+
+theorem dropPrefix?_eq_dropPrefix?_toSlice {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : String} :
+    s.dropPrefix? pat = s.toSlice.dropPrefix? pat := (rfl)
+
+end String

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

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Slice
+public import Init.Data.String.TakeDrop
+import Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
+import Init.Data.String.Lemmas.Pattern.Char
+import Init.Data.Option.Lemmas
+
+public section
+
+open String.Slice Pattern Model
+
+namespace String
+
+namespace Slice
+
+theorem skipPrefix?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} :
+    s.skipPrefix? c = some pos ↔ ∃ h, pos = s.startPos.next h ∧ s.startPos.get h = c := by
+  rw [Pattern.Model.skipPrefix?_eq_some_iff, Char.isLongestMatch_iff]
+
+theorem startsWith_char_iff_get {c : Char} {s : Slice} :
+    s.startsWith c ↔ ∃ h, s.startPos.get h = c := by
+  simp [Pattern.Model.startsWith_iff, Char.matchesAt_iff]
+
+theorem startsWith_char_eq_false_iff_get {c : Char} {s : Slice} :
+    s.startsWith c = false ↔ ∀ h, s.startPos.get h ≠ c := by
+  simp [Pattern.Model.startsWith_eq_false_iff, Char.matchesAt_iff]
+
+theorem startsWith_char_eq_head? {c : Char} {s : Slice} :
+    s.startsWith c = (s.copy.toList.head? == some c) := by
+  rw [Bool.eq_iff_iff, Pattern.Model.startsWith_iff, Char.matchesAt_iff_splits]
+  simp only [splits_startPos_iff, exists_and_left, exists_eq_left, beq_iff_eq]
+  refine ⟨fun ⟨t, ht⟩ => by simp [← ht], fun h => ?_⟩
+  simp only [← toList_inj, toList_append, toList_singleton, List.cons_append, List.nil_append]
+  cases h : s.copy.toList <;> simp_all [← ofList_inj]
+
+theorem startsWith_char_iff_exists_append {c : Char} {s : Slice} :
+    s.startsWith c ↔ ∃ t, s.copy = singleton c ++ t := by
+  simp only [startsWith_char_eq_head?, beq_iff_eq, List.head?_eq_some_iff, ← toList_inj,
+    toList_append, toList_singleton, List.cons_append, List.nil_append]
+  exact ⟨fun ⟨t, ht⟩ => ⟨ofList t, by simp [ht]⟩, fun ⟨t, ht⟩ => ⟨t.toList, by simp [ht]⟩⟩
+
+theorem startsWith_char_eq_false_iff_forall_append {c : Char} {s : Slice} :
+    s.startsWith c = false ↔ ∀ t, s.copy ≠ singleton c ++ t := by
+  simp [← Bool.not_eq_true, startsWith_char_iff_exists_append]
+
+theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropPrefix? c = some res) :
+    s.copy = singleton c ++ res.copy := by
+  simpa [ForwardPatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+
+end Slice
+
+theorem skipPrefix?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} :
+    s.skipPrefix? c = some pos ↔ ∃ h, pos = s.startPos.next h ∧ s.startPos.get h = c := by
+  simp [skipPrefix?_eq_skipPrefix?_toSlice, Slice.skipPrefix?_char_eq_some_iff, ← Pos.toSlice_inj,
+    Pos.toSlice_next]
+
+theorem startsWith_char_iff_get {c : Char} {s : String} :
+    s.startsWith c ↔ ∃ h, s.startPos.get h = c := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_iff_get]
+
+theorem startsWith_char_eq_false_iff_get {c : Char} {s : String} :
+    s.startsWith c = false ↔ ∀ h, s.startPos.get h ≠ c := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_eq_false_iff_get]
+
+theorem startsWith_char_eq_head? {c : Char} {s : String} :
+    s.startsWith c = (s.toList.head? == some c) := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_eq_head?]
+
+theorem startsWith_char_iff_exists_append {c : Char} {s : String} :
+    s.startsWith c ↔ ∃ t, s = singleton c ++ t := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_iff_exists_append]
+
+theorem startsWith_char_eq_false_iff_forall_append {c : Char} {s : String} :
+    s.startsWith c = false ↔ ∀ t, s ≠ singleton c ++ t := by
+  simp [← Bool.not_eq_true, startsWith_char_iff_exists_append]
+
+theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s : String} {res : Slice} (h : s.dropPrefix? c = some res) :
+    s = singleton c ++ res.copy := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix?_char_eq_some h
+
+end String

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

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Slice
+public import Init.Data.String.TakeDrop
+import Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
+import Init.Data.String.Lemmas.Pattern.Pred
+import Init.Data.Option.Lemmas
+import Init.ByCases
+
+public section
+
+open String.Slice Pattern Model
+
+namespace String
+
+namespace Slice
+
+theorem skipPrefix?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
+    s.skipPrefix? p = some pos ↔ ∃ h, pos = s.startPos.next h ∧ p (s.startPos.get h) = true := by
+  rw [Pattern.Model.skipPrefix?_eq_some_iff, CharPred.isLongestMatch_iff]
+
+theorem startsWith_bool_iff_get {p : Char → Bool} {s : Slice} :
+    s.startsWith p ↔ ∃ h, p (s.startPos.get h) = true := by
+  simp [Pattern.Model.startsWith_iff, CharPred.matchesAt_iff]
+
+theorem startsWith_bool_eq_false_iff_get {p : Char → Bool} {s : Slice} :
+    s.startsWith p = false ↔ ∀ h, p (s.startPos.get h) = false := by
+  simp [Pattern.Model.startsWith_eq_false_iff, CharPred.matchesAt_iff]
+
+theorem startsWith_bool_eq_head? {p : Char → Bool} {s : Slice} :
+    s.startsWith p = s.copy.toList.head?.any p := by
+  rw [Bool.eq_iff_iff, Pattern.Model.startsWith_iff, CharPred.matchesAt_iff]
+  by_cases h : s.startPos = s.endPos
+  · refine ⟨fun ⟨h', _⟩ => by simp_all, ?_⟩
+    have : s.copy = "" := by simp_all [Slice.startPos_eq_endPos_iff]
+    simp [this]
+  · obtain ⟨t, ht⟩ := s.splits_startPos.exists_eq_singleton_append h
+    simp [h, ht]
+
+theorem eq_append_of_dropPrefix?_bool_eq_some {p : Char → Bool} {s res : Slice} (h : s.dropPrefix? p = some res) :
+    ∃ c, s.copy = singleton c ++ res.copy ∧ p c = true := by
+  obtain ⟨_, ⟨c, ⟨rfl, h₁⟩⟩, h₂⟩ := by simpa [ForwardPatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+  exact ⟨_, h₂, h₁⟩
+
+theorem skipPrefix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : Slice} {pos : s.Pos} :
+    s.skipPrefix? P = some pos ↔ ∃ h, pos = s.startPos.next h ∧ P (s.startPos.get h) := by
+  simp [skipPrefix?_prop_eq_skipPrefix?_decide, skipPrefix?_bool_eq_some_iff]
+
+theorem startsWith_prop_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} :
+    s.startsWith P ↔ ∃ h, P (s.startPos.get h) := by
+  simp [startsWith_prop_eq_startsWith_decide, startsWith_bool_iff_get]
+
+theorem startsWith_prop_eq_false_iff_get {P : Char → Prop} [DecidablePred P] {s : Slice} :
+    s.startsWith P = false ↔ ∀ h, ¬ P (s.startPos.get h) := by
+  simp [startsWith_prop_eq_startsWith_decide, startsWith_bool_eq_false_iff_get]
+
+theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : Slice} :
+    s.startsWith P = s.copy.toList.head?.any (decide <| P ·) := by
+  simp [startsWith_prop_eq_startsWith_decide, startsWith_bool_eq_head?]
+
+theorem eq_append_of_dropPrefix_prop_eq_some {P : Char → Prop} [DecidablePred P] {s res : Slice} (h : s.dropPrefix? P = some res) :
+    ∃ c, s.copy = singleton c ++ res.copy ∧ P c := by
+  rw [dropPrefix?_prop_eq_dropPrefix?_decide] at h
+  simpa using eq_append_of_dropPrefix?_bool_eq_some h
+
+end Slice
+
+theorem skipPrefix?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
+    s.skipPrefix? p = some pos ↔ ∃ h, pos = s.startPos.next h ∧ p (s.startPos.get h) = true := by
+  simp [skipPrefix?_eq_skipPrefix?_toSlice, Slice.skipPrefix?_bool_eq_some_iff, ← Pos.toSlice_inj,
+    Pos.toSlice_next]
+
+theorem startsWith_bool_iff_get {p : Char → Bool} {s : String} :
+    s.startsWith p ↔ ∃ h, p (s.startPos.get h) = true := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_bool_iff_get]
+
+theorem startsWith_bool_eq_false_iff_get {p : Char → Bool} {s : String} :
+    s.startsWith p = false ↔ ∀ h, p (s.startPos.get h) = false := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_bool_eq_false_iff_get]
+
+theorem startsWith_bool_eq_head? {p : Char → Bool} {s : String} :
+    s.startsWith p = s.toList.head?.any p := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_bool_eq_head?]
+
+theorem eq_append_of_dropPrefix?_bool_eq_some {p : Char → Bool} {s : String} {res : Slice} (h : s.dropPrefix? p = some res) :
+    ∃ c, s = singleton c ++ res.copy ∧ p c = true := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix?_bool_eq_some h
+
+theorem skipPrefix?_prop_eq_some_iff {P : Char → Prop} [DecidablePred P] {s : String} {pos : s.Pos} :
+    s.skipPrefix? P = some pos ↔ ∃ h, pos = s.startPos.next h ∧ P (s.startPos.get h) := by
+  simp [skipPrefix?_eq_skipPrefix?_toSlice, Slice.skipPrefix?_prop_eq_some_iff, ← Pos.toSlice_inj,
+    Pos.toSlice_next]
+
+theorem startsWith_prop_iff_get {P : Char → Prop} [DecidablePred P] {s : String} :
+    s.startsWith P ↔ ∃ h, P (s.startPos.get h) := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_prop_iff_get]
+
+theorem startsWith_prop_eq_false_iff_get {P : Char → Prop} [DecidablePred P] {s : String} :
+    s.startsWith P = false ↔ ∀ h, ¬ P (s.startPos.get h) := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_prop_eq_false_iff_get]
+
+theorem startsWith_prop_eq_head? {P : Char → Prop} [DecidablePred P] {s : String} :
+    s.startsWith P = s.toList.head?.any (decide <| P ·) := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_prop_eq_head?]
+
+theorem eq_append_of_dropPrefix?_prop_eq_some {P : Char → Prop} [DecidablePred P] {s : String} {res : Slice}
+    (h : s.dropPrefix? P = some res) : ∃ c, s = singleton c ++ res.copy ∧ P c := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix_prop_eq_some h
+
+end String

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

@@ -0,0 +1,182 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Slice
+public import Init.Data.String.TakeDrop
+public import Init.Data.String.Lemmas.Splits
+import Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
+import Init.Data.String.Lemmas.Pattern.String
+import Init.Data.List.Sublist
+import Init.Data.Option.Lemmas
+import Init.Data.String.Lemmas.Basic
+
+public section
+
+open String.Slice Pattern Model
+
+namespace String
+
+namespace Slice
+
+theorem skipPrefix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.skipPrefix? pat = some s.startPos := by
+  rw [skipPrefix?_eq_forwardPatternSkipPrefix?, ForwardSliceSearcher.skipPrefix?_of_isEmpty hpat]
+
+@[simp]
+theorem skipPrefix?_slice_eq_some_iff {pat s : Slice} {pos : s.Pos} :
+    s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat.copy t := by
+  match h : pat.isEmpty with
+  | false =>
+    have := ForwardSliceSearcher.lawfulForwardPatternModel h
+    rw [Pattern.Model.skipPrefix?_eq_some_iff, ForwardSliceSearcher.isLongestMatch_iff_splits h]
+  | true => simp [skipPrefix?_slice_of_isEmpty h, (show pat.copy = "" by simpa), eq_comm]
+
+theorem startsWith_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.startsWith pat = true := by
+  rw [startsWith_eq_forwardPatternStartsWith, ForwardSliceSearcher.startsWith_of_isEmpty hpat]
+
+@[simp]
+theorem startsWith_slice_iff {pat s : Slice} :
+    s.startsWith pat ↔ pat.copy.toList <+: s.copy.toList := by
+  match h : pat.isEmpty with
+  | false =>
+    have := ForwardSliceSearcher.lawfulForwardPatternModel h
+    simp only [Model.startsWith_iff, ForwardSliceSearcher.matchesAt_iff_splits h,
+      splits_startPos_iff, exists_and_left, exists_eq_left]
+    simp only [← toList_inj, toList_append, List.prefix_iff_exists_append_eq]
+    exact ⟨fun ⟨t, ht⟩ => ⟨t.toList, by simp [ht]⟩, fun ⟨t, ht⟩ => ⟨String.ofList t, by simp [← ht]⟩⟩
+  | true => simp [startsWith_slice_of_isEmpty h, (show pat.copy = "" by simpa)]
+
+@[simp]
+theorem startsWith_slice_eq_false_iff {pat s : Slice} :
+    s.startsWith pat = false ↔ ¬ (pat.copy.toList <+: s.copy.toList) := by
+  simp [← Bool.not_eq_true, startsWith_slice_iff]
+
+theorem dropPrefix?_slice_of_isEmpty {pat s : Slice} (hpat : pat.isEmpty = true) :
+    s.dropPrefix? pat = some s := by
+  simp [dropPrefix?_eq_map_skipPrefix?, skipPrefix?_slice_of_isEmpty hpat]
+
+theorem eq_append_of_dropPrefix?_slice_eq_some {pat s res : Slice} (h : s.dropPrefix? pat = some res) :
+    s.copy = pat.copy ++ res.copy := by
+  match hpat : pat.isEmpty with
+  | false =>
+    have := ForwardSliceSearcher.lawfulForwardPatternModel hpat
+    have := Pattern.Model.eq_append_of_dropPrefix?_eq_some h
+    simp only [ForwardPatternModel.Matches] at this
+    obtain ⟨_, ⟨-, rfl⟩, h⟩ := this
+    exact h
+  | true => simp [Option.some.inj (h ▸ dropPrefix?_slice_of_isEmpty hpat), (show pat.copy = "" by simpa)]
+
+@[simp]
+theorem skipPrefix?_string_eq_some_iff {pat : String} {s : Slice} {pos : s.Pos} :
+    s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat t := by
+  simp [skipPrefix?_string_eq_skipPrefix?_toSlice]
+
+@[simp]
+theorem skipPrefix?_string_empty {s : Slice} : s.skipPrefix? "" = some s.startPos := by
+  simp
+
+@[simp]
+theorem startsWith_string_iff {pat : String} {s : Slice} :
+    s.startsWith pat ↔ pat.toList <+: s.copy.toList := by
+  simp [startsWith_string_eq_startsWith_toSlice]
+
+@[simp]
+theorem startsWith_string_empty {s : Slice} : s.startsWith "" = true := by
+  simp
+
+@[simp]
+theorem startsWith_string_eq_false_iff {pat : String} {s : Slice} :
+    s.startsWith pat = false ↔ ¬ (pat.toList <+: s.copy.toList) := by
+  simp [startsWith_string_eq_startsWith_toSlice]
+
+@[simp]
+theorem dropPrefix?_string_empty {s : Slice} : s.dropPrefix? "" = some s := by
+  simpa [dropPrefix?_string_eq_dropPrefix?_toSlice] using dropPrefix?_slice_of_isEmpty (by simp)
+
+theorem eq_append_of_dropPrefix?_string_eq_some {pat : String} {s res : Slice} (h : s.dropPrefix? pat = some res) :
+    s.copy = pat ++ res.copy := by
+  rw [dropPrefix?_string_eq_dropPrefix?_toSlice] at h
+  simpa using eq_append_of_dropPrefix?_slice_eq_some h
+
+end Slice
+
+theorem skipPrefix?_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) :
+    s.skipPrefix? pat = some s.startPos := by
+  rw [skipPrefix?_eq_skipPrefix?_toSlice, Slice.skipPrefix?_slice_of_isEmpty hpat]
+  simp
+
+@[simp]
+theorem skipPrefix?_slice_eq_some_iff {pat : Slice} {s : String} {pos : s.Pos} :
+    s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat.copy t := by
+  simp only [skipPrefix?_eq_skipPrefix?_toSlice, Option.map_eq_some_iff,
+    Slice.skipPrefix?_slice_eq_some_iff]
+  refine ⟨?_, fun h => ⟨pos.toSlice, by simpa⟩⟩
+  rintro ⟨pos, h, rfl⟩
+  simpa
+
+theorem startsWith_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) :
+    s.startsWith pat = true := by
+  rw [startsWith_eq_startsWith_toSlice, Slice.startsWith_slice_of_isEmpty hpat]
+
+@[simp]
+theorem startsWith_slice_iff {pat : Slice} {s : String} :
+    s.startsWith pat ↔ pat.copy.toList <+: s.toList := by
+  simp [startsWith_eq_startsWith_toSlice]
+
+@[simp]
+theorem startsWith_slice_eq_false_iff {pat : Slice} {s : String} :
+    s.startsWith pat = false ↔ ¬ (pat.copy.toList <+: s.toList) := by
+  simp [startsWith_eq_startsWith_toSlice]
+
+theorem dropPrefix?_slice_of_isEmpty {pat : Slice} {s : String} (hpat : pat.isEmpty = true) :
+    s.dropPrefix? pat = some s.toSlice := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice, Slice.dropPrefix?_slice_of_isEmpty hpat]
+
+theorem eq_append_of_dropPrefix?_slice_eq_some {pat res : Slice} {s : String} (h : s.dropPrefix? pat = some res) :
+    s = pat.copy ++ res.copy := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix?_slice_eq_some h
+
+@[simp]
+theorem skipPrefix?_string_empty {s : String} : s.skipPrefix? "" = some s.startPos := by
+  simp [skipPrefix?_eq_skipPrefix?_toSlice]
+
+@[simp]
+theorem skipPrefix?_string_eq_some_iff {pat s : String} {pos : s.Pos} :
+    s.skipPrefix? pat = some pos ↔ ∃ t, pos.Splits pat t := by
+  simp only [skipPrefix?_eq_skipPrefix?_toSlice, Option.map_eq_some_iff,
+    Slice.skipPrefix?_string_eq_some_iff]
+  refine ⟨?_, fun h => ⟨pos.toSlice, by simpa⟩⟩
+  rintro ⟨pos, h, rfl⟩
+  simpa
+
+@[simp]
+theorem startsWith_string_empty {s : String} : s.startsWith "" = true := by
+  simp [startsWith_eq_startsWith_toSlice]
+
+@[simp]
+theorem startsWith_string_iff {pat s : String} :
+    s.startsWith pat ↔ pat.toList <+: s.toList := by
+  simp [startsWith_eq_startsWith_toSlice]
+
+@[simp]
+theorem startsWith_string_eq_false_iff {pat s : String} :
+    s.startsWith pat = false ↔ ¬ (pat.toList <+: s.toList) := by
+  simp [startsWith_eq_startsWith_toSlice]
+
+@[simp]
+theorem dropPrefix?_string_empty {s : String} : s.dropPrefix? "" = some s.toSlice := by
+  simp [dropPrefix?_eq_dropPrefix?_toSlice]
+
+theorem eq_append_of_dropPrefix?_string_eq_some {s pat : String} {res : Slice} (h : s.dropPrefix? pat = some res) :
+    s = pat ++ res.copy := by
+  rw [dropPrefix?_eq_dropPrefix?_toSlice] at h
+  simpa using Slice.eq_append_of_dropPrefix?_string_eq_some h
+
+end String

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

@@ -33,8 +33,22 @@ theorem beq_eq_true_iff {s t : Slice} : s == t ↔ s.copy = t.copy := by
 theorem beq_eq_false_iff {s t : Slice} : (s == t) = false ↔ s.copy ≠ t.copy := by
   simp [← Bool.not_eq_true]
 
-theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) := by
-  cases h : s == t <;> simp_all
+theorem beq_eq_decide {s t : Slice} : (s == t) = decide (s.copy = t.copy) :=
+  Bool.eq_iff_iff.2 (by simp)
+
+instance : EquivBEq String.Slice :=
+  equivBEq_of_iff_apply_eq copy (by simp)
+
+theorem beq_list_iff {l l' : List String.Slice} : l == l' ↔ l.map copy = l'.map copy := by
+  induction l generalizing l' <;> cases l' <;> simp_all
+
+theorem beq_list_eq_false_iff {l l' : List String.Slice} :
+    (l == l') = false ↔ l.map copy ≠ l'.map copy := by
+  simp [← Bool.not_eq_true, beq_list_iff]
+
+theorem beq_list_eq_decide {l l' : List String.Slice} :
+    (l == l') = decide (l.map copy = l'.map copy) :=
+  Bool.eq_iff_iff.2 (by simp [beq_list_iff])
 
 end BEq
 

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

@@ -201,6 +201,26 @@ theorem Slice.Pos.Splits.eq_startPos_iff {s : Slice} {p : s.Pos} (h : p.Splits t
     p = s.startPos ↔ t₁ = "" := by
   rw [← copy_inj, ← startPos_copy, h.copy.eq_startPos_iff]
 
+@[simp]
+theorem Pos.splits_empty_left_iff {s : String} {p : s.Pos} {t : String} :
+    p.Splits "" t ↔ p = s.startPos ∧ t = s :=
+  ⟨fun h => by rw [h.eq_startPos_iff]; simp [h.eq_append], by rintro ⟨rfl, rfl⟩; simp⟩
+
+@[simp]
+theorem Pos.splits_empty_right_iff {s : String} {p : s.Pos} {t : String} :
+    p.Splits t "" ↔ p = s.endPos ∧ t = s :=
+  ⟨fun h => by rw [h.eq_endPos_iff]; simp [h.eq_append], by rintro ⟨rfl, rfl⟩; simp⟩
+
+@[simp]
+theorem Slice.Pos.splits_empty_left_iff {s : Slice} {p : s.Pos} {t : String} :
+    p.Splits "" t ↔ p = s.startPos ∧ t = s.copy :=
+  ⟨fun h => by rw [h.eq_startPos_iff]; simp [h.eq_append], by rintro ⟨rfl, rfl⟩; simp⟩
+
+@[simp]
+theorem Slice.Pos.splits_empty_right_iff {s : Slice} {p : s.Pos} {t : String} :
+    p.Splits t "" ↔ p = s.endPos ∧ t = s.copy :=
+  ⟨fun h => by rw [h.eq_endPos_iff]; simp [h.eq_append], by rintro ⟨rfl, rfl⟩; simp⟩
+
 theorem Pos.splits_next_right {s : String} (p : s.Pos) (hp : p ≠ s.endPos) :
     p.Splits (s.sliceTo p).copy (singleton (p.get hp) ++ (s.sliceFrom (p.next hp)).copy) where
   eq_append := by simpa [← append_assoc] using p.eq_copy_sliceTo_append_get hp

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

@@ -106,20 +106,24 @@ class ForwardPattern {ρ : Type} (pat : ρ) where
   Checks whether the slice starts with the pattern. If it does, the slice is returned with the
   prefix removed; otherwise the result is {name}`none`.
   -/
-  dropPrefix? : (s : Slice) →  Option s.Pos
+  skipPrefix? : (s : Slice) →  Option s.Pos
   /--
   Checks whether the slice starts with the pattern. If it does, the slice is returned with the
   prefix removed; otherwise the result is {name}`none`.
   -/
-  dropPrefixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => dropPrefix? s
+  skipPrefixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => skipPrefix? s
   /--
   Checks whether the slice starts with the pattern.
   -/
-  startsWith : (s : Slice) → Bool := fun s => (dropPrefix? s).isSome
+  startsWith : (s : Slice) → Bool := fun s => (skipPrefix? s).isSome
+
+@[deprecated ForwardPattern.dropPrefix? (since := "2026-03-19")]
+def ForwardPattern.dropPrefix? {ρ : Type} (pat : ρ) [ForwardPattern pat] (s : Slice) : Option s.Pos :=
+  ForwardPattern.skipPrefix? pat s
 
 /--
-A lawful forward pattern is one where the three functions {name}`ForwardPattern.dropPrefix?`,
-{name}`ForwardPattern.dropPrefixOfNonempty?` and {name}`ForwardPattern.startsWith` agree for any
+A lawful forward pattern is one where the three functions {name}`ForwardPattern.skipPrefix?`,
+{name}`ForwardPattern.skipPrefixOfNonempty?` and {name}`ForwardPattern.startsWith` agree for any
 given input slice.
 
 Note that this is a relatively weak condition. It is non-uniform in the sense that the functions
@@ -127,14 +131,14 @@ can still return completely different results on different slices, even if they
 string.
 
 There is a stronger lawfulness typeclass {lit}`LawfulForwardPatternModel` that asserts that the
-{name}`ForwardPattern.dropPrefix?` function behaves like a function that drops the longest prefix
+{name}`ForwardPattern.skipPrefix?` function behaves like a function that drops the longest prefix
 according to some notion of matching.
 -/
 class LawfulForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop where
-  dropPrefixOfNonempty?_eq {s : Slice} (h) :
-    ForwardPattern.dropPrefixOfNonempty? pat s h = ForwardPattern.dropPrefix? pat s
+  skipPrefixOfNonempty?_eq {s : Slice} (h) :
+    ForwardPattern.skipPrefixOfNonempty? pat s h = ForwardPattern.skipPrefix? pat s
   startsWith_eq (s : Slice) :
-    ForwardPattern.startsWith pat s = (ForwardPattern.dropPrefix? pat s).isSome
+    ForwardPattern.startsWith pat s = (ForwardPattern.skipPrefix? pat s).isSome
 
 /--
 A strict forward pattern is one which never drops an empty prefix.
@@ -144,7 +148,7 @@ iterator.
 -/
 class StrictForwardPattern {ρ : Type} (pat : ρ) [ForwardPattern pat] : Prop where
   ne_startPos {s : Slice} (h) (q) :
-    ForwardPattern.dropPrefixOfNonempty? pat s h = some q → q ≠ s.startPos
+    ForwardPattern.skipPrefixOfNonempty? pat s h = some q → q ≠ s.startPos
 
 /--
 Provides a conversion from a pattern to an iterator of {name}`SearchStep` that searches for matches
@@ -188,11 +192,11 @@ instance (s : Slice) [ForwardPattern pat] :
     Std.Iterator (DefaultForwardSearcher pat s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' (.rejected p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.endPos),
-      ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = none ∧
+      ForwardPattern.skipPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = none ∧
       p₁ = it.internalState.currPos ∧ p₂ = it.internalState.currPos.next h ∧
       it'.internalState.currPos = it.internalState.currPos.next h
     | .yield it' (.matched p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.endPos), ∃ pos,
-      ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = some pos ∧
+      ForwardPattern.skipPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) = some pos ∧
       p₁ = it.internalState.currPos ∧ p₂ = Slice.Pos.ofSliceFrom pos ∧
       it'.internalState.currPos = Slice.Pos.ofSliceFrom pos
     | .done => it.internalState.currPos = s.endPos
@@ -201,7 +205,7 @@ instance (s : Slice) [ForwardPattern pat] :
     if h : it.internalState.currPos = s.endPos then
       pure (.deflate ⟨.done, by simp [h]⟩)
     else
-      match h' : ForwardPattern.dropPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) with
+      match h' : ForwardPattern.skipPrefixOfNonempty? pat (s.sliceFrom it.internalState.currPos) (by simpa) with
       | some pos =>
         pure (.deflate ⟨.yield ⟨⟨Slice.Pos.ofSliceFrom pos⟩⟩
           (.matched it.internalState.currPos (Slice.Pos.ofSliceFrom pos)), by simp [h, h']⟩)
@@ -312,20 +316,20 @@ class BackwardPattern {ρ : Type} (pat : ρ) where
   Checks whether the slice ends with the pattern. If it does, the slice is returned with the
   suffix removed; otherwise the result is {name}`none`.
   -/
-  dropSuffix? : (s : Slice) → Option s.Pos
+  skipSuffix? : (s : Slice) → Option s.Pos
   /--
   Checks whether the slice ends with the pattern. If it does, the slice is returned with the
   suffix removed; otherwise the result is {name}`none`.
   -/
-  dropSuffixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => dropSuffix? s
+  skipSuffixOfNonempty? : (s : Slice) → (h : s.isEmpty = false) → Option s.Pos := fun s _ => skipSuffix? s
   /--
   Checks whether the slice ends with the pattern.
   -/
-  endsWith : Slice → Bool := fun s => (dropSuffix? s).isSome
+  endsWith : Slice → Bool := fun s => (skipSuffix? s).isSome
 
 /--
-A lawful backward pattern is one where the three functions {name}`BackwardPattern.dropSuffix?`,
-{name}`BackwardPattern.dropSuffixOfNonempty?` and {name}`BackwardPattern.endsWith` agree for any
+A lawful backward pattern is one where the three functions {name}`BackwardPattern.skipSuffix?`,
+{name}`BackwardPattern.skipSuffixOfNonempty?` and {name}`BackwardPattern.endsWith` agree for any
 given input slice.
 
 Note that this is a relatively weak condition. It is non-uniform in the sense that the functions
@@ -333,14 +337,14 @@ can still return completely different results on different slices, even if they
 string.
 
 There is a stronger lawfulness typeclass {lit}`LawfulBackwardPatternModel` that asserts that the
-{name}`BackwardPattern.dropSuffix?` function behaves like a function that drops the longest prefix
+{name}`BackwardPattern.skipSuffix?` function behaves like a function that skips the longest prefix
 according to some notion of matching.
 -/
 class LawfulBackwardPattern {ρ : Type} (pat : ρ) [BackwardPattern pat] : Prop where
-  dropSuffixOfNonempty?_eq {s : Slice} (h) :
-    BackwardPattern.dropSuffixOfNonempty? pat s h = BackwardPattern.dropSuffix? pat s
+  skipSuffixOfNonempty?_eq {s : Slice} (h) :
+    BackwardPattern.skipSuffixOfNonempty? pat s h = BackwardPattern.skipSuffix? pat s
   endsWith_eq (s : Slice) :
-    BackwardPattern.endsWith pat s = (BackwardPattern.dropSuffix? pat s).isSome
+    BackwardPattern.endsWith pat s = (BackwardPattern.skipSuffix? pat s).isSome
 
 /--
 A strict backward pattern is one which never drops an empty suffix.
@@ -350,7 +354,7 @@ iterator.
 -/
 class StrictBackwardPattern {ρ : Type} (pat : ρ) [BackwardPattern pat] : Prop where
   ne_endPos {s : Slice} (h) (q) :
-    BackwardPattern.dropSuffixOfNonempty? pat s h = some q → q ≠ s.endPos
+    BackwardPattern.skipSuffixOfNonempty? pat s h = some q → q ≠ s.endPos
 
 /--
 Provides a conversion from a pattern to an iterator of {name}`SearchStep` searching for matches of
@@ -394,11 +398,11 @@ instance (s : Slice) [BackwardPattern pat] :
     Std.Iterator (DefaultBackwardSearcher pat s) Id (SearchStep s) where
   IsPlausibleStep it
     | .yield it' (.rejected p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.startPos),
-      BackwardPattern.dropSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) = none ∧
+      BackwardPattern.skipSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) = none ∧
       p₁ = it.internalState.currPos.prev h ∧ p₂ = it.internalState.currPos  ∧
       it'.internalState.currPos = it.internalState.currPos.prev h
     | .yield it' (.matched p₁ p₂) => ∃ (h : it.internalState.currPos ≠ s.startPos), ∃ pos,
-      BackwardPattern.dropSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) = some pos ∧
+      BackwardPattern.skipSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) = some pos ∧
       p₁ = Slice.Pos.ofSliceTo pos ∧ p₂ = it.internalState.currPos  ∧
       it'.internalState.currPos = Slice.Pos.ofSliceTo pos
     | .done => it.internalState.currPos = s.startPos
@@ -407,7 +411,7 @@ instance (s : Slice) [BackwardPattern pat] :
     if h : it.internalState.currPos = s.startPos then
       pure (.deflate ⟨.done, by simp [h]⟩)
     else
-      match h' : BackwardPattern.dropSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) with
+      match h' : BackwardPattern.skipSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) (by simpa) with
       | some pos =>
         pure (.deflate ⟨.yield ⟨⟨Slice.Pos.ofSliceTo pos⟩⟩
           (.matched (Slice.Pos.ofSliceTo pos) it.internalState.currPos), by simp [h, h']⟩)

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

@@ -21,30 +21,30 @@ namespace String.Slice.Pattern
 namespace Char
 
 instance {c : Char} : ForwardPattern c where
-  dropPrefixOfNonempty? s h := ForwardPattern.dropPrefixOfNonempty? (· == c) s h
-  dropPrefix? s := ForwardPattern.dropPrefix? (· == c) s
+  skipPrefixOfNonempty? s h := ForwardPattern.skipPrefixOfNonempty? (· == c) s h
+  skipPrefix? s := ForwardPattern.skipPrefix? (· == c) s
   startsWith s := ForwardPattern.startsWith (· == c) s
 
 instance {c : Char} : StrictForwardPattern c where
   ne_startPos h q := StrictForwardPattern.ne_startPos (pat := (· == c)) h q
 
 instance {c : Char} : LawfulForwardPattern c where
-  dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (· == c)) h
+  skipPrefixOfNonempty?_eq h := LawfulForwardPattern.skipPrefixOfNonempty?_eq (pat := (· == c)) h
   startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (· == c)) s
 
 instance {c : Char} : ToForwardSearcher c (ToForwardSearcher.DefaultForwardSearcher (· == c)) where
   toSearcher s := ToForwardSearcher.toSearcher (· == c) s
 
 instance {c : Char} : BackwardPattern c where
-  dropSuffixOfNonempty? s h := BackwardPattern.dropSuffixOfNonempty? (· == c) s h
-  dropSuffix? s := BackwardPattern.dropSuffix? (· == c) s
+  skipSuffixOfNonempty? s h := BackwardPattern.skipSuffixOfNonempty? (· == c) s h
+  skipSuffix? s := BackwardPattern.skipSuffix? (· == c) s
   endsWith s := BackwardPattern.endsWith (· == c) s
 
 instance {c : Char} : StrictBackwardPattern c where
   ne_endPos h q := StrictBackwardPattern.ne_endPos (pat := (· == c)) h q
 
 instance {c : Char} : LawfulBackwardPattern c where
-  dropSuffixOfNonempty?_eq h := LawfulBackwardPattern.dropSuffixOfNonempty?_eq (pat := (· == c)) h
+  skipSuffixOfNonempty?_eq h := LawfulBackwardPattern.skipSuffixOfNonempty?_eq (pat := (· == c)) h
   endsWith_eq s := LawfulBackwardPattern.endsWith_eq (pat := (· == c)) s
 
 instance {c : Char} : ToBackwardSearcher c (ToBackwardSearcher.DefaultBackwardSearcher c) :=

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

@@ -30,12 +30,12 @@ namespace CharPred
 
 @[default_instance]
 instance {p : Char → Bool} : ForwardPattern p where
-  dropPrefixOfNonempty? s h :=
+  skipPrefixOfNonempty? s h :=
     if p (s.startPos.get (Slice.startPos_ne_endPos h)) then
       some (s.startPos.next (Slice.startPos_ne_endPos h))
     else
       none
-  dropPrefix? s :=
+  skipPrefix? s :=
     if h : s.startPos = s.endPos then
       none
     else if p (s.startPos.get h) then
@@ -50,17 +50,17 @@ instance {p : Char → Bool} : ForwardPattern p where
 
 instance {p : Char → Bool} : StrictForwardPattern p where
   ne_startPos {s h q} := by
-    simp only [ForwardPattern.dropPrefixOfNonempty?, Option.ite_none_right_eq_some,
+    simp only [ForwardPattern.skipPrefixOfNonempty?, Option.ite_none_right_eq_some,
       Option.some.injEq, ne_eq, and_imp]
     rintro _ rfl
     simp
 
 instance {p : Char → Bool} : LawfulForwardPattern p where
-  dropPrefixOfNonempty?_eq {s} h := by
-    simp [ForwardPattern.dropPrefixOfNonempty?, ForwardPattern.dropPrefix?,
+  skipPrefixOfNonempty?_eq {s} h := by
+    simp [ForwardPattern.skipPrefixOfNonempty?, ForwardPattern.skipPrefix?,
       Slice.startPos_eq_endPos_iff, h]
   startsWith_eq s := by
-    simp only [ForwardPattern.startsWith, ForwardPattern.dropPrefix?]
+    simp only [ForwardPattern.startsWith, ForwardPattern.skipPrefix?]
     split <;> (try split) <;> simp_all
 
 @[default_instance]
@@ -70,15 +70,15 @@ instance {p : Char → Bool} : ToForwardSearcher p (ToForwardSearcher.DefaultFor
 namespace Decidable
 
 instance {p : Char → Prop} [DecidablePred p] : ForwardPattern p where
-  dropPrefixOfNonempty? s h := ForwardPattern.dropPrefixOfNonempty? (decide <| p ·) s h
-  dropPrefix? s := ForwardPattern.dropPrefix? (decide <| p ·) s
+  skipPrefixOfNonempty? s h := ForwardPattern.skipPrefixOfNonempty? (decide <| p ·) s h
+  skipPrefix? s := ForwardPattern.skipPrefix? (decide <| p ·) s
   startsWith s := ForwardPattern.startsWith (decide <| p ·) s
 
 instance {p : Char → Prop} [DecidablePred p] : StrictForwardPattern p where
   ne_startPos h q := StrictForwardPattern.ne_startPos (pat := (decide <| p ·)) h q
 
 instance {p : Char → Prop} [DecidablePred p] : LawfulForwardPattern p where
-  dropPrefixOfNonempty?_eq h := LawfulForwardPattern.dropPrefixOfNonempty?_eq (pat := (decide <| p ·)) h
+  skipPrefixOfNonempty?_eq h := LawfulForwardPattern.skipPrefixOfNonempty?_eq (pat := (decide <| p ·)) h
   startsWith_eq s := LawfulForwardPattern.startsWith_eq (pat := (decide <| p ·)) s
 
 instance {p : Char → Prop} [DecidablePred p] : ToForwardSearcher p (ToForwardSearcher.DefaultForwardSearcher (decide <| p ·)) where
@@ -88,12 +88,12 @@ end Decidable
 
 @[default_instance]
 instance {p : Char → Bool} : BackwardPattern p where
-  dropSuffixOfNonempty? s h :=
+  skipSuffixOfNonempty? s h :=
     if p ((s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h))).get (by simp)) then
       some (s.endPos.prev (Ne.symm (by exact Slice.startPos_ne_endPos h)))
     else
       none
-  dropSuffix? s :=
+  skipSuffix? s :=
     if h : s.endPos = s.startPos then
       none
     else if p ((s.endPos.prev h).get (by simp)) then
@@ -108,17 +108,17 @@ instance {p : Char → Bool} : BackwardPattern p where
 
 instance {p : Char → Bool} : StrictBackwardPattern p where
   ne_endPos {s h q} := by
-    simp only [BackwardPattern.dropSuffixOfNonempty?, Option.ite_none_right_eq_some,
+    simp only [BackwardPattern.skipSuffixOfNonempty?, Option.ite_none_right_eq_some,
       Option.some.injEq, ne_eq, and_imp]
     rintro _ rfl
     simp
 
 instance {p : Char → Bool} : LawfulBackwardPattern p where
-  dropSuffixOfNonempty?_eq {s h} := by
-    simp [BackwardPattern.dropSuffixOfNonempty?, BackwardPattern.dropSuffix?,
+  skipSuffixOfNonempty?_eq {s h} := by
+    simp [BackwardPattern.skipSuffixOfNonempty?, BackwardPattern.skipSuffix?,
       Eq.comm (a := s.endPos), Slice.startPos_eq_endPos_iff, h]
   endsWith_eq {s} := by
-    simp only [BackwardPattern.endsWith, BackwardPattern.dropSuffix?]
+    simp only [BackwardPattern.endsWith, BackwardPattern.skipSuffix?]
     split <;> (try split) <;> simp_all
 
 @[default_instance]
@@ -128,15 +128,15 @@ instance {p : Char → Bool} : ToBackwardSearcher p (ToBackwardSearcher.DefaultB
 namespace Decidable
 
 instance {p : Char → Prop} [DecidablePred p] : BackwardPattern p where
-  dropSuffixOfNonempty? s h := BackwardPattern.dropSuffixOfNonempty? (decide <| p ·) s h
-  dropSuffix? s := BackwardPattern.dropSuffix? (decide <| p ·) s
+  skipSuffixOfNonempty? s h := BackwardPattern.skipSuffixOfNonempty? (decide <| p ·) s h
+  skipSuffix? s := BackwardPattern.skipSuffix? (decide <| p ·) s
   endsWith s := BackwardPattern.endsWith (decide <| p ·) s
 
 instance {p : Char → Prop} [DecidablePred p] : StrictBackwardPattern p where
   ne_endPos h q := StrictBackwardPattern.ne_endPos (pat := (decide <| p ·)) h q
 
 instance {p : Char → Prop} [DecidablePred p] : LawfulBackwardPattern p where
-  dropSuffixOfNonempty?_eq h := LawfulBackwardPattern.dropSuffixOfNonempty?_eq (pat := (decide <| p ·)) h
+  skipSuffixOfNonempty?_eq h := LawfulBackwardPattern.skipSuffixOfNonempty?_eq (pat := (decide <| p ·)) h
   endsWith_eq s := LawfulBackwardPattern.endsWith_eq (pat := (decide <| p ·)) s
 
 instance {p : Char → Prop} [DecidablePred p] : ToBackwardSearcher p (ToBackwardSearcher.DefaultBackwardSearcher p) :=

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

@@ -280,7 +280,7 @@ def startsWith (pat : Slice) (s : Slice) : Bool :=
     false
 
 @[inline]
-def dropPrefix? (pat : Slice) (s : Slice) : Option s.Pos :=
+def skipPrefix? (pat : Slice) (s : Slice) : Option s.Pos :=
   if startsWith pat s then
     some <| s.pos! <| pat.rawEndPos.offsetBy s.startPos.offset
   else
@@ -288,14 +288,14 @@ def dropPrefix? (pat : Slice) (s : Slice) : Option s.Pos :=
 
 instance {pat : Slice} : ForwardPattern pat where
   startsWith := startsWith pat
-  dropPrefix? := dropPrefix? pat
+  skipPrefix? := skipPrefix? pat
 
 instance {pat : String} : ToForwardSearcher pat ForwardSliceSearcher where
   toSearcher := iter pat.toSlice
 
 instance {pat : String} : ForwardPattern pat where
   startsWith := startsWith pat.toSlice
-  dropPrefix? := dropPrefix? pat.toSlice
+  skipPrefix? := skipPrefix? pat.toSlice
 
 end ForwardSliceSearcher
 
@@ -316,7 +316,7 @@ def endsWith (pat : Slice) (s : Slice) : Bool :=
     false
 
 @[inline]
-def dropSuffix? (pat : Slice) (s : Slice) : Option s.Pos :=
+def skipSuffix? (pat : Slice) (s : Slice) : Option s.Pos :=
   if endsWith pat s then
     some <| s.pos! <| s.endPos.offset.unoffsetBy pat.rawEndPos
   else
@@ -324,11 +324,11 @@ def dropSuffix? (pat : Slice) (s : Slice) : Option s.Pos :=
 
 instance {pat : Slice} : BackwardPattern pat where
   endsWith := endsWith pat
-  dropSuffix? := dropSuffix? pat
+  skipSuffix? := skipSuffix? pat
 
 instance {pat : String} : BackwardPattern pat where
   endsWith := endsWith pat.toSlice
-  dropSuffix? := dropSuffix? pat.toSlice
+  skipSuffix? := skipSuffix? pat.toSlice
 
 end BackwardSliceSearcher
 

src/Init/Data/String/Search.lean

@@ -278,43 +278,14 @@ def splitInclusive (s : String) (pat : ρ) [ToForwardSearcher pat σ] :=
 def foldlAux {α : Type u} (f : α → Char → α) (s : String) (stopPos : Pos.Raw) (i : Pos.Raw) (a : α) : α :=
   s.slice! (s.pos! i) (s.pos! stopPos) |>.foldl f a
 
-/--
-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
-
 @[deprecated String.Slice.foldr (since := "2025-11-25")]
 def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (i begPos : Pos.Raw) : α :=
   s.slice! (s.pos! begPos) (s.pos! i) |>.foldr f a
 
-/--
-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
-
 @[deprecated String.Slice.any (since := "2025-11-25")]
 def anyAux (s : String) (stopPos : Pos.Raw) (p : Char → Bool) (i : Pos.Raw) : Bool :=
   s.slice! (s.pos! i) (s.pos! stopPos) |>.any p
 
-
 /--
 Checks whether a string has a match of the pattern {name}`pat` anywhere.
 

src/Init/Data/String/Slice.lean

@@ -11,7 +11,7 @@ public import Init.Data.Ord.Basic
 public import Init.Data.Iterators.Combinators.FilterMap
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Subslice
-public import Init.Data.String.Iter
+public import Init.Data.String.Iter.Basic
 public import Init.Data.String.Iterate
 import Init.Data.Iterators.Consumers.Collect
 import Init.Data.Iterators.Consumers.Loop
@@ -84,10 +84,11 @@ instance : ToString String.Slice where
 theorem toStringToString_eq : ToString.toString = String.Slice.copy := (rfl)
 
 @[extern "lean_slice_hash"]
-opaque hash (s : @& Slice) : UInt64
+protected def hash (s : @& Slice) : UInt64 :=
+  String.hash s.copy
 
 instance : Hashable Slice where
-  hash := hash
+  hash := Slice.hash
 
 instance : LT Slice where
   lt x y := x.copy < y.copy
@@ -213,7 +214,7 @@ Examples:
  * {lean}`("ababababa".toSlice.splitToSubslice "aba").toStringList == ["coffee", "water"]`
  * {lean}`("baaab".toSlice.splitToSubslice "aa").toStringList == ["b", "ab"]`
 -/
-@[specialize pat]
+@[specialize pat, cbv_opaque]
 def splitToSubslice (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] :
     Std.Iter (α := SplitIterator pat s) s.Subslice :=
   { internalState := .operating s.startPos (ToForwardSearcher.toSearcher pat s) }
@@ -328,6 +329,26 @@ def splitInclusive (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] :
     Std.Iter (α := SplitInclusiveIterator pat s) Slice :=
   { internalState := .operating s.startPos (ToForwardSearcher.toSearcher pat s) }
 
+/--
+If {name}`pat` matches a prefix of {name}`s`, returns the position at the start of the remainder.
+Returns {name}`none` otherwise.
+
+This function is generic over all currently supported patterns.
+-/
+@[inline]
+def skipPrefix? (s : Slice) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+  ForwardPattern.skipPrefix? pat s
+
+/--
+If {name}`pat` matches a prefix at {name}`pos`, returns the position after the end of the match.
+Returns {name}`none` otherwise.
+
+This function is generic over all currently supported patterns.
+-/
+@[inline]
+def Pos.skip? {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+  ((s.sliceFrom pos).skipPrefix? pat).map Pos.ofSliceFrom
+
 /--
 If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
 
@@ -344,7 +365,7 @@ Examples:
 -/
 @[inline]
 def dropPrefix? (s : Slice) (pat : ρ) [ForwardPattern pat] : Option Slice :=
-  (ForwardPattern.dropPrefix? pat s).map s.sliceFrom
+  (s.skipPrefix? pat).map s.sliceFrom
 
 /--
 If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`s` unmodified
@@ -400,6 +421,28 @@ Examples:
 def drop (s : Slice) (n : Nat) : Slice :=
   s.sliceFrom (s.startPos.nextn n)
 
+/--
+Advances {name}`pos` as long as {name}`pat` matches.
+-/
+@[specialize pat]
+def Pos.skipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : s.Pos :=
+  if let some nextCurr := ForwardPattern.skipPrefix? pat (s.sliceFrom pos) then
+    if pos < Pos.ofSliceFrom nextCurr then
+      skipWhile (Pos.ofSliceFrom nextCurr) pat
+    else
+      pos
+  else
+    pos
+termination_by pos
+
+/--
+Returns the position after the longest prefix of {name}`s` for which {name}`pat` matches
+(potentially repeatedly).
+-/
+@[inline]
+def skipPrefixWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : s.Pos :=
+  s.startPos.skipWhile pat
+
 /--
 Creates a new slice that contains the longest prefix of {name}`s` for which {name}`pat` matched
 (potentially repeatedly).
@@ -412,18 +455,7 @@ Examples:
 -/
 @[inline]
 def dropWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : Slice :=
-  go s.startPos
-where
-  @[specialize pat]
-  go (curr : s.Pos) : Slice :=
-    if let some nextCurr := ForwardPattern.dropPrefix? pat (s.sliceFrom curr) then
-      if curr < Pos.ofSliceFrom nextCurr then
-        go (Pos.ofSliceFrom nextCurr)
-      else
-        s.sliceFrom curr
-    else
-      s.sliceFrom curr
-  termination_by curr
+  s.sliceFrom (s.skipPrefixWhile pat)
 
 /--
 Removes leading whitespace from a slice by moving its start position to the first non-whitespace
@@ -472,18 +504,7 @@ Examples:
 -/
 @[inline]
 def takeWhile (s : Slice) (pat : ρ) [ForwardPattern pat] : Slice :=
-  go s.startPos
-where
-  @[specialize pat]
-  go (curr : s.Pos) : Slice :=
-    if let some nextCurr := ForwardPattern.dropPrefix? pat (s.sliceFrom curr) then
-      if curr < Pos.ofSliceFrom nextCurr then
-        go (Pos.ofSliceFrom nextCurr)
-      else
-        s.sliceTo curr
-    else
-      s.sliceTo curr
-  termination_by curr
+  s.sliceTo (s.skipPrefixWhile pat)
 
 /--
 Finds the position of the first match of the pattern {name}`pat` in a slice {name}`s`. If there
@@ -668,6 +689,26 @@ def revSplit (s : Slice) (pat : ρ) [ToBackwardSearcher pat σ] :
     Std.Iter (α := RevSplitIterator pat s) Slice :=
   { internalState := .operating s.endPos (ToBackwardSearcher.toSearcher pat s) }
 
+/--
+If {name}`pat` matches a suffix of {name}`s`, returns the position at the beginning of the suffix.
+Returns {name}`none` otherwise.
+
+This function is generic over all currently supported patterns.
+-/
+@[inline]
+def skipSuffix? (s : Slice) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
+  BackwardPattern.skipSuffix? pat s
+
+/--
+If {name}`pat` matches a suffix at {name}`pos`, returns the position at the beginning of the match.
+Returns {name}`none` otherwise.
+
+This function is generic over all currently supported patterns.
+-/
+@[inline]
+def Pos.revSkip? {s : Slice} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+  ((s.sliceFrom pos).skipPrefix? pat).map Pos.ofSliceFrom
+
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
 
@@ -684,7 +725,7 @@ Examples:
 -/
 @[inline]
 def dropSuffix? (s : Slice) (pat : ρ) [BackwardPattern pat] : Option Slice :=
-  (BackwardPattern.dropSuffix? pat s).map s.sliceTo
+  (s.skipSuffix? pat).map s.sliceTo
 
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`s` unmodified
@@ -719,6 +760,28 @@ Examples:
 def dropEnd (s : Slice) (n : Nat) : Slice :=
   s.sliceTo (s.endPos.prevn n)
 
+/--
+Rewinds {name}`pos` as long as {name}`pat` matches.
+-/
+@[specialize pat]
+def Pos.revSkipWhile {s : Slice} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : s.Pos :=
+  if let some nextCurr := BackwardPattern.skipSuffix? pat (s.sliceTo pos) then
+    if Pos.ofSliceTo nextCurr < pos then
+      revSkipWhile (Pos.ofSliceTo nextCurr) pat
+    else
+      pos
+  else
+    pos
+termination_by pos.down
+
+/--
+Returns the position a the start of the longest suffix of {name}`s` for which {name}`pat` matches
+(potentially repeatedly).
+-/
+@[inline]
+def skipSuffixWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : s.Pos :=
+  s.endPos.revSkipWhile pat
+
 /--
 Creates a new slice that contains the longest suffix of {name}`s` for which {name}`pat` matched
 (potentially repeatedly).
@@ -730,18 +793,7 @@ Examples:
 -/
 @[inline]
 def dropEndWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : Slice :=
-  go s.endPos
-where
-  @[specialize pat]
-  go (curr : s.Pos) : Slice :=
-    if let some nextCurr := BackwardPattern.dropSuffix? pat (s.sliceTo curr) then
-      if Pos.ofSliceTo nextCurr < curr then
-        go (Pos.ofSliceTo nextCurr)
-      else
-        s.sliceTo curr
-    else
-      s.sliceTo curr
-  termination_by curr.down
+  s.sliceTo (s.skipSuffixWhile pat)
 
 /--
 Removes trailing whitespace from a slice by moving its end position to the last non-whitespace
@@ -789,18 +841,7 @@ Examples:
 -/
 @[inline]
 def takeEndWhile (s : Slice) (pat : ρ) [BackwardPattern pat] : Slice :=
-  go s.endPos
-where
-  @[specialize pat]
-  go (curr : s.Pos) : Slice :=
-    if let some nextCurr := BackwardPattern.dropSuffix? pat (s.sliceTo curr) then
-      if Pos.ofSliceTo nextCurr < curr then
-        go (Pos.ofSliceTo nextCurr)
-      else
-        s.sliceFrom curr
-    else
-      s.sliceFrom curr
-  termination_by curr.down
+  s.sliceFrom (s.skipSuffixWhile pat)
 
 /--
 Finds the position of the first match of the pattern {name}`pat` in a slice, starting
@@ -905,22 +946,20 @@ Examples:
  * {lean}`"123_".toSlice.isNat = false`
  * {lean}`"12__34".toSlice.isNat = false`
 -/
-@[inline]
-def isNat (s : Slice) : Bool :=
-  if s.isEmpty then
-    false
-  else
-    -- Track: isFirst, lastWasUnderscore, lastCharWasDigit, valid
-    let result := s.foldl (fun (isFirst, lastWasUnderscore, _lastCharWasDigit, valid) c =>
-      let isDigit := c.isDigit
-      let isUnderscore := c = '_'
-      let newValid := valid && (isDigit || isUnderscore) &&
-                      !(isFirst && isUnderscore) &&  -- Cannot start with underscore
-                      !(lastWasUnderscore && isUnderscore)  -- No consecutive underscores
-      (false, isUnderscore, isDigit, newValid))
-      (true, false, false, true)
-    -- Must be valid and last character must have been a digit (not underscore)
-    result.2.2.2 && result.2.2.1
+def isNat (s : Slice) : Bool := Id.run do
+  let mut lastWasDigit := false
+
+  for c in s do
+    if c = '_' then
+      if !lastWasDigit then
+        return false
+      lastWasDigit := false
+    else if c.isDigit then
+      lastWasDigit := true
+    else
+      return false
+
+  return lastWasDigit
 
 /--
 Interprets a slice as the decimal representation of a natural number, returning it. Returns
@@ -1015,12 +1054,13 @@ Examples:
  * {lean}`" 5".toSlice.isInt = false`
  * {lean}`"2-3".toSlice.isInt = false`
  * {lean}`"0xff".toSlice.isInt = false`
+ * {lean}`"-0_1".toSlice.isInt = true`
+ * {lean}`"-_1".toSlice.isInt = false`
 -/
 def isInt (s : Slice) : Bool :=
-  if s.front = '-' then
-    (s.drop 1).isNat
-  else
-    s.isNat
+  match s.dropPrefix? '-' with
+  | some rest => rest.isNat
+  | none => s.isNat
 
 /--
 Interprets a slice as the decimal representation of an integer, returning it. Returns {lean}`none` if
@@ -1044,12 +1084,13 @@ Examples:
  * {lean}`" 5".toSlice.toInt? = none`
  * {lean}`"2-3".toSlice.toInt? = none`
  * {lean}`"0xff".toSlice.toInt? = none`
+ * {lean}`"-0_1".toSlice.toInt? = some (-1)`
+ * {lean}`"-_1".toSlice.toInt? = none`
 -/
 def toInt? (s : Slice) : Option Int :=
-  if s.front = '-' then
-    Int.negOfNat <$> (s.drop 1).toNat?
-  else
-   Int.ofNat <$> s.toNat?
+  match s.dropPrefix? '-' with
+  | some rest => rest.toNat?.map Int.negOfNat
+  | none => s.toNat?.map Int.ofNat
 
 /--
 Interprets a string as the decimal representation of an integer, returning it. Panics if the string

src/Init/Data/String/TakeDrop.lean

@@ -208,6 +208,39 @@ def dropRightWhile (s : String) (p : Char → Bool) : String :=
 def Slice.dropRightWhile (s : Slice) (p : Char → Bool) : Slice :=
   s.dropEndWhile p
 
+/--
+If {name}`pat` matches a prefix of {name}`s`, returns the position at the start of the remainder.
+Returns {name}`none` otherwise.
+
+This function is generic over all currently supported patterns.
+-/
+@[inline] def skipPrefix? (s : String) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+  (s.toSlice.skipPrefix? pat).map Pos.ofToSlice
+
+/--
+Returns the position after the longest prefix of {name}`s` for which {name}`pat` matches
+(potentially repeatedly).
+-/
+@[inline] def skipPrefixWhile (s : String) (pat : ρ) [ForwardPattern pat] : s.Pos :=
+  Pos.ofToSlice (s.toSlice.skipPrefixWhile pat)
+
+/--
+If {name}`pat` matches at {name}`pos`, returns the position after the end of the match.
+Returns {name}`none` otherwise.
+
+This function is generic over all currently supported patterns.
+-/
+@[inline]
+def Pos.skip? {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+  (pos.toSlice.skip? pat).map Pos.ofToSlice
+
+/--
+Advances {name}`pos` as long as {name}`pat` matches.
+-/
+@[inline]
+def Pos.skipWhile {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : s.Pos :=
+  Pos.ofToSlice (pos.toSlice.skipWhile pat)
+
 /--
 Checks whether the first string ({name}`s`) begins with the pattern ({name}`pat`).
 
@@ -258,6 +291,39 @@ Examples:
 @[inline] def endsWith (s : String) (pat : ρ) [BackwardPattern pat] : Bool :=
   s.toSlice.endsWith pat
 
+/--
+If {name}`pat` matches a suffix of {name}`s`, returns the position at the beginning of the suffix.
+Returns {name}`none` otherwise.
+
+This function is generic over all currently supported patterns.
+-/
+@[inline] def skipSuffix? (s : String) (pat : ρ) [BackwardPattern pat] : Option s.Pos :=
+  (s.toSlice.skipSuffix? pat).map Pos.ofToSlice
+
+/--
+Returns the position at the start of the longest suffix of {name}`s` for which {name}`pat` matches
+(potentially repeatedly).
+-/
+@[inline] def skipSuffixWhile (s : String) (pat : ρ) [BackwardPattern pat] : s.Pos :=
+  Pos.ofToSlice (s.toSlice.skipSuffixWhile pat)
+
+/--
+If {name}`pat` matches at {name}`pos`, returns the position after the end of the match.
+Returns {name}`none` otherwise.
+
+This function is generic over all currently supported patterns.
+-/
+@[inline]
+def Pos.revSkip? {s : String} (pos : s.Pos) (pat : ρ) [ForwardPattern pat] : Option s.Pos :=
+  (pos.toSlice.revSkip? pat).map Pos.ofToSlice
+
+/--
+Rewinds {name}`pos` as long as {name}`pat` matches.
+-/
+@[inline]
+def Pos.revSkipWhile {s : String} (pos : s.Pos) (pat : ρ) [BackwardPattern pat] : s.Pos :=
+  Pos.ofToSlice (pos.toSlice.revSkipWhile pat)
+
 /--
 Removes trailing whitespace from a string by returning a slice whose end position is the last
 non-whitespace character, or the start position if there is no non-whitespace character.

src/Init/Data/ToString/Extra.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.String.Defs
+public import Init.Data.Int.Repr
 
 public section
 
@@ -38,6 +39,4 @@ instance [ToString α] : ToString (Array α) where
 instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
 
 instance : ToString Int where
-  toString
-    | Int.ofNat m   => toString m
-    | Int.negSucc m => "-" ++ toString (m + 1)
+  toString := Int.repr

src/Init/Data/Vector/Attach.lean

@@ -100,7 +100,7 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
 
 @[simp] theorem pmap_push {P : α → Prop} {f : ∀ a, P a → β} {a : α} {xs : Vector α n} {h : ∀ b ∈ xs.push a, P b} :
     pmap f (xs.push a) h =
-      (pmap f xs (fun a m => by simp at h; exact h.1 _ m)).push (f a (h a (by simp))) := by
+      (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
   simp [pmap]
 
 @[simp] theorem attach_empty : (#v[] : Vector α 0).attach = #v[] := rfl
@@ -147,7 +147,7 @@ theorem attachWith_congr {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {
 
 @[simp] theorem attachWith_push {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
-      (xs.attachWith P (fun x h => by simp at H; exact H.1 _ h)).push ⟨a, H a (by simp)⟩ := by
+      (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
   rcases xs with ⟨xs, rfl⟩
   simp
 

src/Init/Grind/Config.lean

@@ -111,11 +111,10 @@ structure Config where
   ring := true
   /--
   Maximum number of steps performed by the `ring` solver.
-  A step is counted whenever one polynomial is used to simplify another.
-  For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
-  used to simplify the second to `-1 * y^3 + x * y`.
+  A step is counted whenever one polynomial is used to simplify another,
+  weighted by the number of terms in the resulting polynomial.
   -/
-  ringSteps := 10000
+  ringSteps := 100000
   /--
   When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
   `CommRing`.

src/Init/Grind/Interactive.lean

@@ -107,6 +107,9 @@ syntax (name := showLocalThms) "show_local_thms" : grind
 -/
 syntax (name := showTerm) "show_term " grindSeq : grind
 
+/-- Shows the pending goals. -/
+syntax (name := showGoals) "show_goals" : grind
+
 declare_syntax_cat grind_ref (behavior := both)
 
 syntax:max anchor : grind_ref
@@ -205,7 +208,7 @@ macro:1 x:grind tk:" <;> " y:grind:2 : grind => `(grind|
     with_annotate_state $tk skip
     all_goals $y:grind)
 
-/-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
+/-- `first (tac) ...` runs each `tac` until one succeeds, or else fails. -/
 syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "(" grindSeq ")")+) : grind
 
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/
@@ -304,5 +307,19 @@ syntax (name := symInternalizeAll) "internalize_all" : grind
 Only available in `sym =>` mode. -/
 syntax (name := symByContra) "by_contra" : grind
 
+/--
+`simp` applies the structural simplifier to the goal target.
+Only available in `sym =>` mode.
+
+- `simp` — uses the default (identity) variant
+- `simp myVariant` — uses a named variant registered via `register_sym_simp`
+- `simp [thm₁, thm₂, ...]` — default variant with extra rewrite theorems appended to `post`
+- `simp myVariant [thm₁, thm₂, ...]` — named variant with extra theorems
+-/
+syntax (name := symSimp) "simp" (ppSpace colGt ident)? (" [" ident,* "]")? : grind
+
+/-- `exact e` closes the main goal if its target type matches that of `e`. -/
+macro "exact " e:term : grind => `(grind| tactic => exact $e:term)
+
 end Grind
 end Lean.Parser.Tactic

src/Init/Grind/Ordered/Linarith.lean

@@ -17,6 +17,7 @@ import Init.Data.Nat.Lemmas
 import Init.Grind.Ordered.Order
 import Init.Omega
 import Init.WFTactics
+import Init.Data.Int.Repr
 
 @[expose] public section
 

src/Init/Grind/Ring/CommSolver.lean

@@ -22,6 +22,7 @@ import Init.Data.Nat.Linear
 import Init.Grind.Ordered.Order
 import Init.Omega
 import Init.WFTactics
+import Init.Data.Int.Repr
 
 @[expose] public section