fix: body refactor

This PR verifies the `String.startsWith` and `String.skipPrefix?`
functions for our various pattern types.

.claude/CLAUDE.md

@@ -1,7 +1,12 @@
 (In the following, use `sysctl -n hw.logicalcpu` instead of `nproc` on macOS)
 
+## Building
+
 To build Lean you should use `make -j$(nproc) -C build/release`.
 
+The build uses `ccache`, and in a sandbox `ccache` may complain about read-only file systems.
+Use `CCACHE_READONLY` and `CCACHE_TEMPDIR` instead of disabling ccache completely.
+
 ## Running Tests
 
 See `tests/README.md` for full documentation. Quick reference:
@@ -20,9 +25,24 @@ CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
 
 # Single test from tests/foo/bar/ (quick check during development)
-cd tests/foo/bar && ./run_test example_test.lean
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release -j "$(nproc)" test ARGS=-R testname'
 ```
 
+## Testing stage 2
+
+When requested to test stage 2, build it as follows:
+```
+make -C build/release stage2 -j$(nproc)
+```
+Stage 2 is *not* automatically invalidated by changes to `src/` which allows for faster iteration
+when fixing a specific file in the stage 2 build but for invalidating any files that already passed
+the stage 2 build as well as for final validation,
+```
+make -C build/release/stage2 clean-stdlib
+```
+must be run manually before building.
+
 ## New features
 
 When asked to implement new features:

CMakeLists.txt

@@ -79,7 +79,7 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   endif()
   find_program(LEANTAR leantar)
   if(NOT LEANTAR)
-    set(LEANTAR_VERSION v0.1.18)
+    set(LEANTAR_VERSION v0.1.19)
     if(CMAKE_SYSTEM_NAME MATCHES "Windows")
       set(LEANTAR_ARCHIVE_SUFFIX .zip)
       set(LEANTAR_TARGET x86_64-pc-windows-msvc)

doc/examples/compiler/run_test.sh

@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../../tests/env_test.sh
-
 leanmake --always-make bin
 
 capture ./build/bin/test hello world

doc/examples/run_test.sh

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

flake.nix

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

script/release_steps.py

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

src/CMakeLists.txt

@@ -118,6 +118,9 @@ option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires
 set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to lean --make")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
+# Temporary, core-only flags. Must be synced with stdlib_flags.h.
+string(APPEND LEAN_EXTRA_MAKE_OPTS " -Dbackward.do.legacy=false")
+
 if(LAZY_RC MATCHES "ON")
   set(LEAN_LAZY_RC "#define LEAN_LAZY_RC")
 endif()
@@ -942,6 +945,7 @@ install(
   PATTERN "*.hash" EXCLUDE
   PATTERN "*.trace" EXCLUDE
   PATTERN "*.rsp" EXCLUDE
+  PATTERN "*.filelist" EXCLUDE
 )
 
 # symlink source into expected installation location for go-to-definition, if file system allows it

src/Init/Control/Lawful/Basic.lean

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

src/Init/Conv.lean

@@ -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/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 a (.inl 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 x (.inl 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/Find.lean

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

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]
 

src/Init/Data/Bool.lean

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

src/Init/Data/Char/Lemmas.lean

@@ -86,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/Pow.lean

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

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

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

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

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

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

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

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

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

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

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

src/Init/Data/Iterators/PostconditionMonad.lean

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

src/Init/Data/List/Find.lean

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

src/Init/Data/List/Lemmas.lean

@@ -877,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/Nat/TakeDrop.lean

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

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

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

src/Init/Data/List/Sublist.lean

@@ -706,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⟩ =>
@@ -1299,6 +1304,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/Basic.lean

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

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

@@ -867,7 +867,7 @@ theorem and_le_right {n m : Nat} : n &&& m ≤ m :=
   le_of_testBit (by simp)
 
 theorem left_le_or {n m : Nat} : n ≤ n ||| m :=
-  le_of_testBit (by simpa using fun i => Or.inl)
+  le_of_testBit (by simp [imp_or_left_iff_true])
 
 theorem right_le_or {n m : Nat} : m ≤ n ||| m :=
-  le_of_testBit (by simpa using fun i => Or.inr)
+  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
 
@@ -37,6 +38,71 @@ theorem isDigit_digitChar : n.digitChar.isDigit = decide (n < 10) :=
     simp only [digitChar, ↓reduceIte, Nat.reduceEqDiff]
     (repeat' split) <;> simp
 
+private theorem digitChar_iff_aux :
+    ∀ n, (n.digitChar = '0' ↔ n = 0) ∧ (n.digitChar = '1' ↔ n = 1) ∧
+         (n.digitChar = '2' ↔ n = 2) ∧ (n.digitChar = '3' ↔ n = 3) ∧
+         (n.digitChar = '4' ↔ n = 4) ∧ (n.digitChar = '5' ↔ n = 5) ∧
+         (n.digitChar = '6' ↔ n = 6) ∧ (n.digitChar = '7' ↔ n = 7) ∧
+         (n.digitChar = '8' ↔ n = 8) ∧ (n.digitChar = '9' ↔ n = 9) ∧
+         (n.digitChar = 'a' ↔ n = 10) ∧ (n.digitChar = 'b' ↔ n = 11) ∧
+         (n.digitChar = 'c' ↔ n = 12) ∧ (n.digitChar = 'd' ↔ n = 13) ∧
+         (n.digitChar = 'e' ↔ n = 14) ∧ (n.digitChar = 'f' ↔ n = 15) ∧
+         (n.digitChar = '*' ↔ 16 ≤ n)
+  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | _ + 16 => by simp [digitChar]
+
+@[simp] theorem digitChar_eq_zero : n.digitChar = '0' ↔ n = 0 := (digitChar_iff_aux n).1
+@[simp] theorem digitChar_eq_one : n.digitChar = '1' ↔ n = 1 := (digitChar_iff_aux n).2.1
+@[simp] theorem digitChar_eq_two : n.digitChar = '2' ↔ n = 2 := (digitChar_iff_aux n).2.2.1
+@[simp] theorem digitChar_eq_three : n.digitChar = '3' ↔ n = 3 := (digitChar_iff_aux n).2.2.2.1
+@[simp] theorem digitChar_eq_four : n.digitChar = '4' ↔ n = 4 := (digitChar_iff_aux n).2.2.2.2.1
+@[simp] theorem digitChar_eq_five : n.digitChar = '5' ↔ n = 5 := (digitChar_iff_aux n).2.2.2.2.2.1
+@[simp] theorem digitChar_eq_six : n.digitChar = '6' ↔ n = 6 := (digitChar_iff_aux n).2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_seven : n.digitChar = '7' ↔ n = 7 := (digitChar_iff_aux n).2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_eight : n.digitChar = '8' ↔ n = 8 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_nine : n.digitChar = '9' ↔ n = 9 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_a : n.digitChar = 'a' ↔ n = 10 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_b : n.digitChar = 'b' ↔ n = 11 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_c : n.digitChar = 'c' ↔ n = 12 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_d : n.digitChar = 'd' ↔ n = 13 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_e : n.digitChar = 'e' ↔ n = 14 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_f : n.digitChar = 'f' ↔ n = 15 := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1
+@[simp] theorem digitChar_eq_star : n.digitChar = '*' ↔ 16 ≤ n := (digitChar_iff_aux n).2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2
+
+@[simp] theorem zero_eq_digitChar : '0' = n.digitChar ↔ n = 0 := digitChar_eq_zero |> eq_comm.trans
+@[simp] theorem one_eq_digitChar : '1' = n.digitChar ↔ n = 1 := digitChar_eq_one |> eq_comm.trans
+@[simp] theorem two_eq_digitChar : '2' = n.digitChar ↔ n = 2 := digitChar_eq_two |> eq_comm.trans
+@[simp] theorem three_eq_digitChar : '3' = n.digitChar ↔ n = 3 := digitChar_eq_three |> eq_comm.trans
+@[simp] theorem four_eq_digitChar : '4' = n.digitChar ↔ n = 4 := digitChar_eq_four |> eq_comm.trans
+@[simp] theorem five_eq_digitChar : '5' = n.digitChar ↔ n = 5 := digitChar_eq_five |> eq_comm.trans
+@[simp] theorem six_eq_digitChar : '6' = n.digitChar ↔ n = 6 := digitChar_eq_six |> eq_comm.trans
+@[simp] theorem seven_eq_digitChar : '7' = n.digitChar ↔ n = 7 := digitChar_eq_seven |> eq_comm.trans
+@[simp] theorem eight_eq_digitChar : '8' = n.digitChar ↔ n = 8 := digitChar_eq_eight |> eq_comm.trans
+@[simp] theorem nine_eq_digitChar : '9' = n.digitChar ↔ n = 9 := digitChar_eq_nine |> eq_comm.trans
+@[simp] theorem a_eq_digitChar : 'a' = n.digitChar ↔ n = 10 := digitChar_eq_a |> eq_comm.trans
+@[simp] theorem b_eq_digitChar : 'b' = n.digitChar ↔ n = 11 := digitChar_eq_b |> eq_comm.trans
+@[simp] theorem c_eq_digitChar : 'c' = n.digitChar ↔ n = 12 := digitChar_eq_c |> eq_comm.trans
+@[simp] theorem d_eq_digitChar : 'd' = n.digitChar ↔ n = 13 := digitChar_eq_d |> eq_comm.trans
+@[simp] theorem e_eq_digitChar : 'e' = n.digitChar ↔ n = 14 := digitChar_eq_e |> eq_comm.trans
+@[simp] theorem f_eq_digitChar : 'f' = n.digitChar ↔ n = 15 := digitChar_eq_f |> eq_comm.trans
+@[simp] theorem star_eq_digitChar : '*' = n.digitChar ↔ 16 ≤ n := digitChar_eq_star |> eq_comm.trans
+
+/-- Auxiliary theorem for `Nat.reduceDigitCharEq` simproc. -/
+protected theorem digitChar_ne {n : Nat} (c : Char)
+    (h : c != '0' && c != '1' && c != '2' && c != '3' && c != '4' && c != '5' &&
+         c != '6' && c != '7' && c != '8' && c != '9' && c != 'a' && c != 'b' &&
+         c != 'c' && c != 'd' && c != 'e' && c != 'f' && c != '*') : n.digitChar ≠ c := by
+  rintro rfl
+  match n with
+  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | _ + 16 => simp [digitChar] at h
+
+theorem toNat_digitChar_of_lt_ten {n : Nat} (hn : n < 10) : n.digitChar.toNat = 48 + n :=
+  match n with
+  | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 => by simp [digitChar]
+  | _ + 10 => by omega
+
+theorem toNat_digitChar_sub_48_of_lt_ten {n : Nat} (hn : n < 10) : n.digitChar.toNat - 48 = n := by
+  simp [toNat_digitChar_of_lt_ten hn]
+
 private theorem isDigit_of_mem_toDigitsCore
     (hc : c ∈ cs → c.isDigit) (hb₁ : 0 < b) (hb₂ : b ≤ 10) (h : c ∈ toDigitsCore b fuel n cs) :
     c.isDigit := by
@@ -53,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
@@ -129,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
@@ -154,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)
@@ -194,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/Factories.lean

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

src/Init/Data/Order/Opposite.lean

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

src/Init/Data/Order/PackageFactories.lean

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

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

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

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

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

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

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

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

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

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

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

src/Init/Data/String/Basic.lean

@@ -1266,9 +1266,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 +1689,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 +1924,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/Bootstrap.lean

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

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

@@ -230,7 +230,7 @@ Examples:
  * `"empty".isEmpty = false`
  * `" ".isEmpty = false`
 -/
-@[inline] def isEmpty (s : String) : Bool :=
+@[inline, expose] def isEmpty (s : String) : Bool :=
   s.utf8ByteSize == 0
 
 @[export lean_string_isempty]

src/Init/Data/String/Iterate.lean

@@ -462,4 +462,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/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/Iterate.lean

@@ -190,6 +190,17 @@ theorem forIn_eq_forIn_toList {m : Type u → Type v} [Monad m] [LawfulMonad m]
     ForIn.forIn s b f = ForIn.forIn s.copy.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 : 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
 
 /--
@@ -355,4 +366,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

@@ -57,4 +57,14 @@ theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.lengt
 theorem map_eq_empty {f : Char → Char} {s : String} : s.map f = "" ↔ s = "" := by
   simp [← toList_eq_nil_iff]
 
+@[simp]
+theorem map_map {f g : Char → Char} {s : String} : String.map g (String.map f s) = String.map (g ∘ f) s  := by
+  apply String.ext
+  simp [List.map_map]
+
+@[simp]
+theorem map_id {s : String} : String.map id s = s := by
+  apply String.ext
+  simp [List.map_id]
+
 end String

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

@@ -13,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/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/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,71 @@
+/-
+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 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]
+
+theorem dropPrefix?_eq_map_skipPrefix? {ρ : Type} {pat : ρ} [ForwardPattern pat] {s : Slice} :
+    s.dropPrefix? pat = (s.skipPrefix? pat).map s.sliceFrom := (rfl)
+
+@[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?]
+
+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)
+
+end String

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

@@ -0,0 +1,62 @@
+/-
+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]
+
+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?]
+
+end String

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

@@ -0,0 +1,98 @@
+/-
+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 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?]
+
+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 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?]
+
+end String

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

@@ -0,0 +1,110 @@
+/-
+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
+
+public section
+
+open String.Slice Pattern Model
+
+namespace String
+
+namespace Slice
+
+@[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 =>
+    rw [skipPrefix?_eq_forwardPatternSkipPrefix?, ForwardSliceSearcher.skipPrefix?_of_isEmpty h]
+    simp [(show pat.copy = "" by simpa), eq_comm]
+
+@[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 =>
+    rw [startsWith_eq_forwardPatternStartsWith, ForwardSliceSearcher.startsWith_of_isEmpty h]
+    simp [(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]
+
+@[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 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_eq_false_iff {pat : String} {s : Slice} :
+    s.startsWith pat = false ↔ ¬ (pat.toList <+: s.copy.toList) := by
+  simp [startsWith_string_eq_startsWith_toSlice]
+
+end Slice
+
+@[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
+
+@[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]
+
+@[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_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]
+
+end String

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

@@ -229,7 +229,7 @@ Examples:
 * `"Orange".toLower = "orange"`
 * `"ABc123".toLower = "abc123"`
 -/
-@[inline] def toLower (s : String) : String :=
+@[inline, expose] def toLower (s : String) : String :=
   s.map Char.toLower
 
 /--

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

@@ -328,6 +328,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 +364,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 +420,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 +454,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 +503,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 +688,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 +724,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 +759,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 +792,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 +840,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
@@ -906,21 +946,20 @@ Examples:
  * {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

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/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 a (.inl 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 x (.inl 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/Data/Vector/Find.lean

@@ -303,12 +303,12 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
 /-! ### findFinIdx? -/
 
 @[grind =]
-theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp; rfl
+theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
 
 @[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
-  simp; rfl
+  simp
 
 @[congr] theorem findFinIdx?_congr {p : α → Bool} {xs : Vector α n} {ys : Vector α n} (w : xs = ys) :
     findFinIdx? p xs = findFinIdx? p ys := by

src/Init/Data/Vector/Monadic.lean

@@ -53,7 +53,7 @@ theorem mapM_pure [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β) :
     (mk #[] rfl).mapM f = pure #v[] := by
   unfold mapM
   unfold mapM.go
-  simp; rfl
+  simp
 
 @[simp, grind =] theorem mapM_append [Monad m] [LawfulMonad m]
     {f : α → m β} {xs : Vector α n} {ys : Vector α n'} :

src/Init/Grind/Interactive.lean

@@ -262,5 +262,47 @@ Adds new case-splits using model-based theory combination.
 -/
 syntax (name := mbtc) "mbtc" : grind
 
+/-- `intro x₁ ... xₙ` introduces binders and internalizes them into the E-graph.
+Only available in `sym =>` mode.
+`intro` with no arguments introduces one binder with an inaccessible name.
+Use `intro (internalize := false)` or `intro~` to skip internalization. -/
+syntax (name := symIntro) "intro" (ppSpace "(" &"internalize" " := " (&"true" <|> &"false") ")")? (ppSpace colGt binderIdent)* : grind
+
+/-- `intro~ x₁ ... xₙ` is shorthand for `intro (internalize := false)`. -/
+syntax (name := symIntroLight) "intro" noWs "~" (ppSpace colGt binderIdent)* : grind
+
+macro_rules
+| `(grind| intro~ $ids*) => `(grind| intro (internalize := false) $ids*)
+
+/-- `intros` introduces all remaining binders and internalizes them.
+Only available in `sym =>` mode.
+Use `intros (internalize := false)` or `intros~` to skip internalization. -/
+syntax (name := symIntros) "intros" (ppSpace "(" &"internalize" " := " (&"true" <|> &"false") ")")? : grind
+
+/-- `intros~` is shorthand for `intros (internalize := false)`. -/
+syntax (name := symIntrosLight) "intros" noWs "~" : grind
+
+macro_rules
+| `(grind| intros~) => `(grind| intros (internalize := false))
+
+/-- `apply t` applies theorem `t` as a backward rule.
+Only available in `sym =>` mode.
+When used with `repeat`, the backward rule is cached for efficiency. -/
+syntax (name := symApply) "apply " term : grind
+
+/-- `internalize` internalizes hypotheses into the grind E-graph.
+Only available in `sym =>` mode.
+- `internalize` internalizes the next hypothesis.
+- `internalize <num>` internalizes the next `<num>` hypotheses. -/
+syntax (name := symInternalize) "internalize" (ppSpace num)? : grind
+
+/-- `internalize_all` internalizes all pending hypotheses into the grind E-graph.
+Only available in `sym =>` mode. -/
+syntax (name := symInternalizeAll) "internalize_all" : grind
+
+/-- `by_contra` applies proof by contradiction, negating the target and making it `False`.
+Only available in `sym =>` mode. -/
+syntax (name := symByContra) "by_contra" : grind
+
 end Grind
 end Lean.Parser.Tactic

src/Init/Grind/Tactics.lean

@@ -295,6 +295,24 @@ syntax (name := grindTrace)
   (" [" withoutPosition(grindParam,*) "]")?
   : tactic
 
+/--
+`sym` enters an interactive symbolic simulation mode built on `grind`.
+Unlike `grind =>`, it does not eagerly introduce hypotheses or apply by-contradiction,
+giving the user explicit control over `intro`, `apply`, and `internalize` steps.
+
+Example:
+```
+example (x : Nat) : myP x → myQ x := by
+  sym [myP_myQ] =>
+    intro h
+    finish
+```
+-/
+syntax (name := sym)
+  "sym" optConfig (&" only")?
+  (" [" withoutPosition(grindParam,*) "]")?
+  " => " grindSeq : tactic
+
 /--
 `cutsat` solves linear integer arithmetic goals.
 

src/Init/Notation.lean

@@ -722,7 +722,7 @@ syntax (name := runElab) "run_elab " doSeq : command
 
 /--
 The `run_meta doSeq` command executes code in `MetaM Unit`.
-This is the same as `#eval show MetaM Unit from do discard doSeq`.
+This is the same as `#eval show MetaM Unit from discard do doSeq`.
 
 (This is effectively a synonym for `run_elab` since `MetaM` lifts to `TermElabM`.)
 -/

src/Init/Prelude.lean

@@ -3004,7 +3004,7 @@ Examples:
  * `([] : List String).length = 0`
  * `["green", "brown"].length = 2`
 -/
-def List.length : List α → Nat
+@[implicit_reducible] def List.length : List α → Nat
   | nil       => 0
   | cons _ as => HAdd.hAdd (length as) 1
 
@@ -4674,7 +4674,7 @@ inductive Name where
   /-- The "anonymous" name. -/
   | anonymous : Name
   /--
-  A string name. The name `Lean.Meta.run` is represented at
+  A string name. The name `Lean.Meta.run` is represented as
   ```lean
   .str (.str (.str .anonymous "Lean") "Meta") "run"
   ```

src/Init/PropLemmas.lean

@@ -72,6 +72,12 @@ theorem and_and_right : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c := by rw [and_
 theorem and_iff_left  (hb : b) : a ∧ b ↔ a := Iff.intro And.left  (And.intro · hb)
 theorem and_iff_right (ha : a) : a ∧ b ↔ b := Iff.intro And.right (And.intro ha ·)
 
+@[simp] theorem and_imp_left_iff_true {P Q : Prop} : (P ∧ Q → P) ↔ True := by
+  simpa using And.left
+
+@[simp] theorem and_imp_right_iff_true {P Q : Prop} : (P ∧ Q → Q) ↔ True := by
+  simp
+
 /-! ## or -/
 
 theorem or_self_iff : a ∨ a ↔ a := or_self _ ▸ .rfl
@@ -94,6 +100,12 @@ theorem or_rotate : a ∨ b ∨ c ↔ b ∨ c ∨ a := by simp only [or_left_com
 theorem or_iff_left  (hb : ¬b) : a ∨ b ↔ a := or_iff_left_iff_imp.mpr  hb.elim
 theorem or_iff_right (ha : ¬a) : a ∨ b ↔ b := or_iff_right_iff_imp.mpr ha.elim
 
+theorem imp_or_left_iff_true {P Q : Prop} : (P → P ∨ Q) ↔ True := by
+  simpa using Or.inl
+
+theorem imp_or_right_iff_true {P Q : Prop} : (Q → P ∨ Q) ↔ True := by
+  simpa using Or.inr
+
 /-! ## distributivity -/
 
 theorem not_imp_of_and_not : a ∧ ¬b → ¬(a → b)
@@ -344,12 +356,34 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
 @[simp] theorem exists_prop_eq' {p : (a : α) → a' = a → Prop} :
     (∃ (a : α) (h : a' = a), p a h) ↔ p a' rfl := by simp [@eq_comm _ a']
 
-@[simp] theorem forall_eq_or_imp : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a := by
+@[simp] theorem forall_eq_or_imp {P Q : α → Prop} :
+    (∀ a, a = a' ∨ Q a → P a) ↔ P a' ∧ ∀ a, Q a → P a := by
   simp only [or_imp, forall_and, forall_eq]
 
+theorem forall_eq_or_imp' {P Q : α → Prop} {a' : α} :
+    (∀ (a : α), a' = a ∨ Q a → P a) ↔ P a' ∧ ∀ (a : α), Q a → P a := by
+  simp only [or_imp, forall_and, forall_eq']
+
+theorem forall_or_eq_imp {P Q : α → Prop} :
+    (∀ a, Q a ∨ a = a' → P a) ↔ (∀ a, Q a → P a) ∧ P a' := by
+  simp only [or_imp, forall_and, forall_eq]
+
+theorem forall_or_eq_imp' {P Q : α → Prop} :
+    (∀ a, Q a ∨ a' = a → P a) ↔ (∀ a, Q a → P a) ∧ P a' := by
+  simp only [or_imp, forall_and, forall_eq']
+
 @[simp] theorem exists_eq_or_imp : (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a := by
   simp only [or_and_right, exists_or, exists_eq_left]
 
+@[simp] theorem exists_eq_or_imp' : (∃ a, (a' = a ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a := by
+  simp only [or_and_right, exists_or, exists_eq_left']
+
+@[simp] theorem exists_or_eq_imp : (∃ a, (q a ∨ a = a') ∧ p a) ↔ (∃ a, q a ∧ p a) ∨ p a' := by
+  simp only [or_and_right, exists_or, exists_eq_left]
+
+@[simp] theorem exists_or_eq_imp' : (∃ a, (q a ∨ a' = a) ∧ p a) ↔ (∃ a, q a ∧ p a) ∨ p a' := by
+  simp only [or_and_right, exists_or, exists_eq_left']
+
 @[simp] theorem exists_eq_right_right : (∃ (a : α), p a ∧ q a ∧ a = a') ↔ p a' ∧ q a' := by
   simp [← and_assoc]
 
@@ -404,6 +438,22 @@ theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' :
 @[simp] theorem forall_self_imp (P : Prop) (Q : P → Prop) : (∀ p : P, P → Q p) ↔ ∀ p, Q p :=
   ⟨fun h p => h p p, fun h _ p => h p⟩
 
+theorem forall_or_imp_or_self_right_right {P Q R : α → Prop} :
+    (∀ a, P a ∨ Q a → R a ∨ Q a) ↔ (∀ a, P a → R a ∨ Q a) := by
+  simp only [or_imp, imp_or_right_iff_true, and_true]
+
+theorem forall_or_imp_or_self_right_left {P Q R : α → Prop} :
+    (∀ a, P a ∨ Q a → Q a ∨ R a) ↔ (∀ a, P a → Q a ∨ R a) := by
+  simp only [or_imp, imp_or_left_iff_true, and_true]
+
+theorem forall_or_imp_or_self_left_right {P Q R : α → Prop} :
+    (∀ a, Q a ∨ P a → R a ∨ Q a) ↔ (∀ a, P a → R a ∨ Q a) := by
+  simp only [or_imp, imp_or_right_iff_true, true_and]
+
+theorem forall_or_imp_or_self_left_left {P Q R : α → Prop} :
+    (∀ a, Q a ∨ P a → Q a ∨ R a) ↔ (∀ a, P a → Q a ∨ R a) := by
+  simp only [or_imp, imp_or_left_iff_true, true_and]
+
 end quantifiers
 
 /-! ## membership -/

src/Init/Tactics.lean

@@ -2353,9 +2353,6 @@ after reduction to close the goal.
 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" (location)? : tactic
 
@@ -2373,9 +2370,6 @@ fails.
 The proofs produced by `decide_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 := decide_cbv) "decide_cbv" : tactic
 

src/Lean/Compiler/ExternAttr.lean

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

src/Lean/Compiler/LCNF/InferBorrow.lean

@@ -81,7 +81,10 @@ where
     ps.map fun p => { p with borrow := p.type.isPossibleRef }
 
   initParamsIfNotExported (exported : Bool) (ps : Array (Param .impure)) : Array (Param .impure) :=
-    if exported then ps else initParams ps
+    if exported then
+      ps.map ({ · with borrow := false })
+    else
+      initParams ps
 
   goCode (declName : Name) (code : Code .impure) : InitM Unit := do
     match code with

src/Lean/Compiler/NameDemangling.lean

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

src/Lean/Elab/Idbg.lean

@@ -235,8 +235,8 @@ def idbgCompileAndEval (α : Type) [Nonempty α]
   | .error msg => throw (.userError s!"idbg evalConst failed: {msg}")
 
 /-- Connect to the debug server, receive expressions, evaluate, send results. Loops forever. -/
-@[nospecialize, export lean_idbg_client_loop] def idbgClientLoopImpl {α : Type} [Nonempty α]
-    (siteId : String) (imports : Array Import) (apply : α → String) : IO Unit := do
+@[nospecialize, export lean_idbg_client_loop] def idbgClientLoopImpl
+    (siteId : String) (imports : Array Import) (apply : NonScalar → String) : IO Unit := do
   let baseEnv ← idbgLoadEnv imports
   let port := idbgPort siteId
   let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) port
@@ -249,7 +249,7 @@ def idbgCompileAndEval (α : Type) [Nonempty α]
       let json ← IO.ofExcept (Json.parse msg)
       let type ← IO.ofExcept (exprFromJson? (← IO.ofExcept (json.getObjVal? "type")))
       let value ← IO.ofExcept (exprFromJson? (← IO.ofExcept (json.getObjVal? "value")))
-      let fnVal ← idbgCompileAndEval α baseEnv type value
+      let fnVal ← idbgCompileAndEval NonScalar baseEnv type value
       let result := apply fnVal
       sendMsg client result
       let t ← client.shutdown |>.toIO

src/Lean/Elab/Print.lean

@@ -50,7 +50,7 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   let id' ← match privateToUserName? id with
     | some id' =>
       m := m ++ "private "
-      pure id'
+      if getPPPrivateNames (← getOptions) then pure id else pure id'
     | none =>
       pure id
 

src/Lean/Elab/Tactic/Cbv.lean

@@ -18,7 +18,7 @@ open Lean.Meta.Tactic.Cbv
 
 @[builtin_tactic Lean.Parser.Tactic.cbv] def evalCbv : Tactic := fun stx => withMainContext do
   if cbv.warning.get (← getOptions) then
-    logWarningAt stx "The `cbv` tactic is experimental and still under development. Avoid using it in production projects"
+    logWarningAt stx "The `cbv` usage warning option is enabled. Disable it by setting `set_option cbv.warning false`."
   let (fvarIds, simplifyTarget) ← match expandOptLocation stx[1] with
     | Location.targets hyps simplifyTarget => pure (← getFVarIds hyps, simplifyTarget)
     | Location.wildcard => pure (← (← getMainGoal).getNondepPropHyps, true)
@@ -31,7 +31,7 @@ open Lean.Meta.Tactic.Cbv
   match stx with
   | `(tactic| decide_cbv) => withMainContext do
     if cbv.warning.get (← getOptions) then
-      logWarningAt stx "The `decide_cbv` tactic is experimental and still under development. Avoid using it in production projects"
+      logWarningAt stx "The `decide_cbv` usage warning option is enabled. Disable it by setting `set_option cbv.warning false`."
     liftMetaFinishingTactic fun mvar => do
       let [mvar'] ← mvar.applyConst ``of_decide_eq_true | throwError "Could not apply `of_decide_eq_true`"
       cbvDecideGoal mvar'

src/Lean/Elab/Tactic/Conv/Cbv.lean

@@ -18,7 +18,7 @@ open Lean.Meta.Tactic.Cbv
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.cbv] public def evalCbv : Tactic := fun stx => withMainContext do
   if cbv.warning.get (← getOptions) then
-    logWarningAt stx "The `cbv` tactic is experimental and still under development. Avoid using it in production projects"
+    logWarningAt stx "The `cbv` usage warning option is enabled. Disable it by setting `set_option cbv.warning false`."
   let lhs ← getLhs
   let evalResult ← cbvEntry lhs
   match evalResult with

src/Lean/Elab/Tactic/Grind.lean

@@ -15,3 +15,4 @@ public import Lean.Elab.Tactic.Grind.Config
 public import Lean.Elab.Tactic.Grind.Lint
 public import Lean.Elab.Tactic.Grind.LintExceptions
 public import Lean.Elab.Tactic.Grind.Annotated
+public import Lean.Elab.Tactic.Grind.Sym

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -8,6 +8,8 @@ prelude
 public import Lean.Elab.Tactic.Basic
 public import Lean.Meta.Tactic.Grind.Main
 import Lean.Meta.Tactic.Grind.Intro
+public import Lean.Meta.Sym.Apply
+public import Lean.Meta.Sym.Util
 import Init.Omega
 public section
 namespace Lean.Elab.Tactic.Grind
@@ -18,13 +20,21 @@ structure Context extends Tactic.Context where
   sctx    : Meta.Sym.Context
   methods : Grind.Methods
   params  : Grind.Params
+  sym     : Bool := false
 
 open Meta.Grind (Goal)
 
+structure Cache where
+  /-- Cache for `BackwardRule`s created from declaration names (sym mode only). -/
+  backwardRuleName : PHashMap Name Sym.BackwardRule := {}
+  /-- Cache for `BackwardRule`s created from elaborated terms, keyed by syntax byte position range (sym mode only). -/
+  backwardRuleSyntax : PHashMap (Nat × Nat) Sym.BackwardRule := {}
+
 structure State where
   symState   : Meta.Sym.State
   grindState : Meta.Grind.State
   goals      : List Goal
+  cache      : Cache := {}
 
 structure SavedState where
   term   : Term.SavedState
@@ -377,7 +387,7 @@ def mkEvalTactic' (elaborator : Name) (params : Params) : TermElabM (Goal → TS
 def mkEvalTactic (params : Params) : TacticM (Goal → TSyntax `grind → GrindM (List Goal)) := do
   mkEvalTactic' (← read).elaborator params
 
-def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM α) : TacticM (α × State) := do
+def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM α) (sym : Bool := false) : TacticM (α × State) := do
   let evalTactic ← mkEvalTactic params
   /-
   **Note**: We don't want to close branches using `sorry` after applying `intros + assertAll`.
@@ -385,10 +395,17 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM
   -/
   let params' := { params with config.useSorry := false }
   let (methods, ctx, sctx, state) ← liftMetaM <| GrindM.runAtGoal mvarId params' (evalTactic? := some evalTactic) fun goal => do
-      let a : Action := Action.intros 0 >> Action.assertAll
-      let goals ← match (← a.run goal) with
-        | .closed _ => pure []
-        | .stuck gs => pure gs
+      let goals ←
+        if sym then
+          /- In sym mode, skip eager intros + by-contradiction. The user controls intro/internalize.
+             Preprocess for maximal term sharing, required by Sym operations (introN, BackwardRule.apply, etc.). -/
+          let mvarId ← Sym.preprocessMVar goal.mvarId
+          pure [{ goal with mvarId }]
+        else
+          let a : Action := Action.intros 0 >> Action.assertAll
+          match (← a.run goal) with
+          | .closed _ => pure []
+          | .stuck gs => pure gs
       let methods ← getMethods
       let ctx ← readThe Meta.Grind.Context
       /- Restore original config -/
@@ -398,6 +415,6 @@ def GrindTacticM.runAtGoal (mvarId : MVarId) (params : Params) (k : GrindTacticM
       let symState ← getThe Sym.State
       return (methods, ctx, sctx, { grindState, symState, goals })
   let tctx ← read
-  k { tctx with methods, ctx, sctx, params } |>.run state
+  k { tctx with methods, ctx, sctx, params, sym } |>.run state
 
 end Lean.Elab.Tactic.Grind

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -102,6 +102,12 @@ If the goal is not inconsistent and progress has been made,
 -/
 def evalCheck (tacticName : Name) (k : GoalM Bool)
     (pp? : Goal → MetaM (Option MessageData)) : GrindTacticM Unit := do
+  /- In sym mode, introduce remaining binders + by-contradiction + internalize
+     so that satellite solvers (lia, ring, linarith) see all hypotheses.
+     This matches the behavior of these tactics in default tactic mode
+     where `lia` can close `x > 1 → x + y + z > 0` directly. -/
+  if (← read).sym then
+    liftAction <| Action.intros 0 >> Action.assertAll
   let recover := (← read).recover
   liftGoalM do
     let progress ← k

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -242,15 +242,21 @@ def mkGrindParams
     params := { params with config.clean := false }
   return params
 
+def checkTerminalAsSorry (mvarId : MVarId) : TacticM Bool := do
+  if debug.terminalTacticsAsSorry.get (← getOptions) then
+    mvarId.admit
+    replaceMainGoal []
+    return true
+  else
+    return false
+
 def grind
     (mvarId : MVarId) (config : Grind.Config)
     (only : Bool)
     (ps   :  TSyntaxArray ``Parser.Tactic.grindParam)
     (seq? : Option (TSyntax `Lean.Parser.Tactic.Grind.grindSeq))
     : TacticM Unit := do
-  if debug.terminalTacticsAsSorry.get (← getOptions) then
-    mvarId.admit
-    return ()
+  if (← checkTerminalAsSorry mvarId) then return ()
   mvarId.withContext do
     let params ← mkGrindParams config only ps mvarId
     let params := if Grind.grind.unusedLemmaThreshold.get (← getOptions) > 0 then
@@ -260,7 +266,7 @@ def grind
       let finalize (result : Grind.Result) : TacticM Unit := do
         if result.hasFailed then
           throwError "`grind` failed\n{← result.toMessageData}"
-        return ()
+        replaceMainGoal []
       if let some seq := seq? then
         let (result, _) ← Grind.GrindTacticM.runAtGoal mvarId' params do
           Grind.evalGrindTactic seq
@@ -286,9 +292,7 @@ def evalGrindCore
   let params := if let some params := params? then params.getElems else #[]
   if Grind.grind.warning.get (← getOptions) then
     logWarningAt ref "The `grind` tactic is new and its behavior may change in the future. This project has used `set_option grind.warning true` to discourage its use."
-  withMainContext do
-    grind (← getMainGoal) config only params seq?
-    replaceMainGoal []
+  grind (← getMainGoal) config only params seq?
 
 /-- Position for the `[..]` child syntax in the `grind` tactic. -/
 def grindParamsPos := 3
@@ -343,6 +347,25 @@ private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (
   let config ← elabGrindConfig' config interactive
   evalGrindCore stx config only params seq
 
+@[builtin_tactic Lean.Parser.Tactic.sym] def evalSym : Tactic := fun stx => do
+  recordExtraModUse (isMeta := false) `Init.Grind.Tactics
+  let `(tactic| sym $config:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]? => $seq:grindSeq) := stx
+    | throwUnsupportedSyntax
+  let config ← elabGrindConfig' config true
+  let only' := only.isSome
+  let params := if let some params := params then params.getElems else #[]
+  let mvarId ← getMainGoal
+  if (← checkTerminalAsSorry mvarId) then return ()
+  mvarId.withContext do
+    let params ← mkGrindParams config only' params mvarId
+    Grind.withProtectedMCtx config mvarId fun mvarId' => do
+      let (result, _) ← Grind.GrindTacticM.runAtGoal mvarId' params (sym := true) do
+        Grind.evalGrindTactic seq
+        let goal? := if let goal :: _ := (← get).goals then some goal else none
+        Grind.liftGrindM <| Grind.mkResult params goal?
+      if result.hasFailed then
+        throwError "`sym` failed\n{← result.toMessageData}"
+
 def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorry := true) : TacticM (Array (TSyntax `tactic)) := withMainContext do
   let `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params?:grindParam,*] ]?) := stx
     | throwUnsupportedSyntax

src/Lean/Elab/Tactic/Grind/Sym.lean

@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+import Lean.Elab.Tactic.Grind.Basic
+import Lean.Meta.Sym.Grind
+import Lean.Meta.Tactic.Apply
+import Lean.Elab.SyntheticMVars
+namespace Lean.Elab.Tactic.Grind
+open Meta Grind
+
+private def ensureSym : GrindTacticM Unit := do
+  unless (← read).sym do
+    throwError "tactic is only available in `sym =>` mode"
+
+/-- Lift a `SymM` computation into `GrindTacticM`. -/
+private def liftSymM (k : Sym.SymM α) : GrindTacticM α := do
+  -- GrindM := ... Sym.SymM, so SymM auto-lifts to GrindM
+  liftGrindM k
+
+private def evalIntroCore (internalize : Bool) (ids : TSyntaxArray `Lean.binderIdent) : GrindTacticM Unit := do
+  ensureSym
+  let goal ← getMainGoal
+  let goal ←
+    if ids.isEmpty then
+      match (← liftSymM <| Grind.Goal.introN goal 1) with
+      | .goal _ goal => pure goal
+      | .failed => throwError "`intro` failed, no binders to introduce"
+    else
+      let names ← ids.mapM fun id => match id with
+        | `(binderIdent| $name:ident) => pure name.getId
+        | `(binderIdent| $_) => mkFreshBinderNameForTactic `h
+      match (← liftSymM <| Grind.Goal.intros goal names) with
+      | .goal _ goal => pure goal
+      | .failed => throwError "`intro` failed"
+  let goal ← if internalize then liftGrindM <| Grind.Goal.internalizeAll goal else pure goal
+  replaceMainGoal [goal]
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symIntro] def evalSymIntro : GrindTactic := fun stx => do
+  -- syntax: "intro" ("(" &"internalize" " := " (&"true" <|> &"false") ")")? binderIdent*
+  match stx with
+  | `(grind| intro $ids:binderIdent*) => evalIntroCore true ids
+  | `(grind| intro (internalize := false) $ids:binderIdent*) => evalIntroCore false ids
+  | `(grind| intro (internalize := true) $ids:binderIdent*) => evalIntroCore true ids
+  | _ => throwUnsupportedSyntax
+
+private def evalIntrosCore (internalize : Bool) : GrindTacticM Unit := do
+  ensureSym
+  let goal ← getMainGoal
+  match (← liftSymM <| Grind.Goal.intros goal #[]) with
+  | .goal _ goal =>
+    let goal ← if internalize then liftGrindM <| Grind.Goal.internalizeAll goal else pure goal
+    replaceMainGoal [goal]
+  | .failed => throwError "`intros` failed"
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symIntros] def evalSymIntros : GrindTactic := fun stx => do
+  match stx with
+  | `(grind| intros) => evalIntrosCore true
+  | `(grind| intros (internalize := false)) => evalIntrosCore false
+  | `(grind| intros (internalize := true)) => evalIntrosCore true
+  | _ => throwUnsupportedSyntax
+
+/-- Get or create a `BackwardRule` for a declaration, using the name cache. -/
+private def getOrCreateBackwardRule (declName : Name) : GrindTacticM Sym.BackwardRule := do
+  if let some rule := (← get).cache.backwardRuleName.find? declName then
+    return rule
+  let rule ← Sym.mkBackwardRuleFromDecl declName
+  modify fun s => { s with cache.backwardRuleName := s.cache.backwardRuleName.insert declName rule }
+  return rule
+
+/-- Get or create a `BackwardRule` for a term, using the syntax position cache. -/
+private def getOrCreateBackwardRuleFromTerm (term : Syntax) : GrindTacticM Sym.BackwardRule := do
+  let startPos := term.getPos?.map (·.byteIdx) |>.getD 0
+  let endPos := term.getTailPos?.map (·.byteIdx) |>.getD 0
+  let pos := (startPos, endPos)
+  if let some rule := (← get).cache.backwardRuleSyntax.find? pos then
+    return rule
+  let e ← withMainContext do
+    let e ← Term.elabTerm term none
+    Term.synthesizeSyntheticMVars (postpone := .no)
+    instantiateMVars e
+  let rule ← Sym.mkBackwardRuleFromExpr e
+  modify fun s => { s with cache.backwardRuleSyntax := s.cache.backwardRuleSyntax.insert pos rule }
+  return rule
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symApply] def evalSymApply : GrindTactic := fun stx => do
+  ensureSym
+  let `(grind| apply $term:term) := stx | throwUnsupportedSyntax
+  let goal ← getMainGoal
+  goal.withContext do
+  -- Try to interpret as a declaration name for efficient caching
+  let rule ← match term with
+  | `($id:ident) =>
+    try
+      let declName ← realizeGlobalConstNoOverload id
+      getOrCreateBackwardRule declName
+    catch _ =>
+      getOrCreateBackwardRuleFromTerm term
+  | _ =>
+    getOrCreateBackwardRuleFromTerm term
+  match (← liftSymM <| Grind.Goal.apply goal rule) with
+  | .goals subgoals => replaceMainGoal subgoals
+  | .failed => throwError "`apply` failed, rule is not applicable"
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symInternalize] def evalSymInternalize : GrindTactic := fun stx => do
+  ensureSym
+  let goal ← getMainGoal
+  let num := if stx[1].isNone then 1 else stx[1][0].toNat
+  let goal ← liftGrindM <| Grind.Goal.internalize goal num
+  replaceMainGoal [goal]
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symInternalizeAll] def evalSymInternalizeAll : GrindTactic := fun _ => do
+  ensureSym
+  let goal ← getMainGoal
+  let goal ← liftGrindM <| Grind.Goal.internalizeAll goal
+  replaceMainGoal [goal]
+
+@[builtin_grind_tactic Parser.Tactic.Grind.symByContra] def evalSymByContra : GrindTactic := fun _ => do
+  ensureSym
+  let goal ← getMainGoal
+  let target ← goal.mvarId.getType
+  if target.isFalse then
+    throwError "`by_contra` failed, target is already `False`"
+  -- If target is not a proposition, apply exfalso first
+  let mvarId ← if (← isProp target) then pure goal.mvarId else goal.mvarId.exfalso
+  let some mvarId ← mvarId.byContra?
+    | throwError "`by_contra` failed"
+  -- byContra? produces `⊢ ¬target → False`, introduce the negated hypothesis
+  let (_, mvarId) ← mvarId.intro1
+  let goal := { goal with mvarId }
+  -- Internalize the negated hypothesis so the E-graph can detect contradictions
+  let goal ← liftGrindM <| Grind.Goal.internalizeAll goal
+  replaceMainGoal [goal]
+
+end Lean.Elab.Tactic.Grind

src/Lean/Elab/Tactic/Induction.lean

@@ -999,9 +999,13 @@ def evalInduction : Tactic := fun stx =>
   match expandInduction? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
-    let (targets, toTag) ← elabElimTargets stx[1].getSepArgs
-    let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := true)
-    let targets ← withMainContext <| addImplicitTargets elimInfo targets
+    -- Disable tactic incrementality during setup to prevent nested `by` blocks (e.g. in `using`)
+    -- from consuming the snapshot meant for `evalAlts`.
+    let (targets, toTag, elimInfo) ← Term.withoutTacticIncrementality true do
+      let (targets, toTag) ← elabElimTargets stx[1].getSepArgs
+      let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := true)
+      let targets ← withMainContext <| addImplicitTargets elimInfo targets
+      return (targets, toTag, elimInfo)
     evalInductionCore stx elimInfo targets toTag
 
 
@@ -1081,8 +1085,10 @@ def evalFunInduction : Tactic := fun stx =>
   match expandInduction? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
-    let (elimInfo, targets) ← elabFunTarget (cases := false) stx[1]
-    let targets ← generalizeTargets targets
+    let (elimInfo, targets) ← Term.withoutTacticIncrementality true do
+      let (elimInfo, targets) ← elabFunTarget (cases := false) stx[1]
+      let targets ← generalizeTargets targets
+      return (elimInfo, targets)
     evalInductionCore stx elimInfo targets
 
 /--
@@ -1122,9 +1128,11 @@ def evalCases : Tactic := fun stx =>
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
     -- syntax (name := cases) "cases " elimTarget,+ (" using " term)? (inductionAlts)? : tactic
-    let (targets, toTag) ← elabElimTargets stx[1].getSepArgs
-    let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := false)
-    let targets ← withMainContext <| addImplicitTargets elimInfo targets
+    let (targets, toTag, elimInfo) ← Term.withoutTacticIncrementality true do
+      let (targets, toTag) ← elabElimTargets stx[1].getSepArgs
+      let elimInfo ← withMainContext <| getElimNameInfo stx[2] targets (induction := false)
+      let targets ← withMainContext <| addImplicitTargets elimInfo targets
+      return (targets, toTag, elimInfo)
     evalCasesCore stx elimInfo targets toTag
 
 @[builtin_tactic Lean.Parser.Tactic.funCases, builtin_incremental]
@@ -1132,8 +1140,10 @@ def evalFunCases : Tactic := fun stx =>
   match expandInduction? stx with
   | some stxNew => withMacroExpansion stx stxNew <| evalTactic stxNew
   | _ => focus do
-    let (elimInfo, targets) ← elabFunTarget (cases := true) stx[1]
-    let targets ← generalizeTargets targets
+    let (elimInfo, targets) ← Term.withoutTacticIncrementality true do
+      let (elimInfo, targets) ← elabFunTarget (cases := true) stx[1]
+      let targets ← generalizeTargets targets
+      return (elimInfo, targets)
     evalCasesCore stx elimInfo targets
 
 builtin_initialize

src/Lean/Elab/Tactic/Try.lean

@@ -623,6 +623,7 @@ private def evalSuggestSimpAllTrace : TryTactic := fun tac => do
   | _ => throwUnsupportedSyntax
 
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_eval_suggest_tactic"] -- forward definition to avoid mutual block
 opaque evalSuggest : TryTactic
 

src/Lean/Environment.lean

@@ -752,6 +752,7 @@ private def lakeAdd (env : Environment) (cinfo : ConstantInfo) : Environment :=
   }
 
 -- forward reference due to too many cyclic dependencies
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_is_reserved_name"]
 private opaque isReservedName (env : Environment) (name : Name) : Bool
 
@@ -1768,6 +1769,7 @@ private def looksLikeOldCodegenName : Name → Bool
   | .str _ s => s.startsWith "_cstage" || s.startsWith "_spec_" || s.startsWith "_elambda"
   | _        => false
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_get_ir_extra_const_names"]
 private opaque getIRExtraConstNames (env : Environment) (level : OLeanLevel) (includeDecls := false) : Array Name
 
@@ -1804,6 +1806,7 @@ def mkModuleData (env : Environment) (level : OLeanLevel := .private) : IO Modul
     constNames, constants, entries
   }
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_ir_export_entries"]
 private opaque exportIREntries (env : Environment) : Array (Name × Array EnvExtensionEntry)
 
@@ -1862,6 +1865,7 @@ private def setImportedEntries (states : Array EnvExtensionState) (mods : Array
           { s with importedEntries := s.importedEntries.set! modIdx entries }
   return states
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
   "Forward declaration" needed for updating the attribute table with user-defined attributes.
   User-defined attributes are declared using the `initialize` command. The `initialize` command is just syntax sugar for the `init` attribute.
@@ -1872,9 +1876,12 @@ private def setImportedEntries (states : Array EnvExtensionState) (mods : Array
   Later, we set this method with code that adds the user-defined attributes that were imported after we initialized `attributeExtension`.
 -/
 @[extern "lean_update_env_attributes"] opaque updateEnvAttributes : Environment → IO Environment
+
+set_option compiler.ignoreBorrowAnnotation true in
 /-- "Forward declaration" for retrieving the number of builtin attributes. -/
 @[extern "lean_get_num_attributes"] opaque getNumBuiltinAttributes : IO Nat
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_run_init_attrs"]
 private opaque runInitAttrs (env : Environment) (opts : Options) : IO Unit
 
@@ -2399,6 +2406,7 @@ def displayStats (env : Environment) : IO Unit := do
 @[extern "lean_eval_const"]
 private unsafe opaque evalConstCore (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_eval_check_meta"]
 private opaque evalCheckMeta (env : Environment) (constName : Name) : Except String Unit
 

src/Lean/Expr.lean

@@ -253,7 +253,7 @@ instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (S
 instance : Inhabited (FVarIdMap α) where
   default := {}
 
-/-- Universe metavariable Id   -/
+/-- Expression metavariable Id   -/
 structure MVarId where
   name : Name
   deriving Inhabited, BEq, Hashable
@@ -301,8 +301,8 @@ inductive Expr where
   of a variable in the expression where there is a variable binder
   above it (i.e. introduced by a `lam`, `forallE`, or `letE`).
 
-  The `deBruijnIndex` parameter is the *de-Bruijn* index for the bound
-  variable. See [the Wikipedia page on de-Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index)
+  The `deBruijnIndex` parameter is the *de Bruijn* index for the bound
+  variable. See [the Wikipedia page on de Bruijn indices](https://en.wikipedia.org/wiki/De_Bruijn_index)
   for additional information.
 
   For example, consider the expression `fun x : Nat => forall y : Nat, x = y`.
@@ -321,16 +321,16 @@ inductive Expr where
   | bvar (deBruijnIndex : Nat)
 
   /--
-  The `fvar` constructor represent free variables. These *free* variable
-  occurrences are not bound by an earlier `lam`, `forallE`, or `letE`
+  The `fvar` constructor represents free variables. Such a *free* variable
+  occurrence is not bound by an earlier `lam`, `forallE`, or `letE`
   constructor and its binder exists in a local context only.
 
-  Note that Lean uses the *locally nameless approach*. See [McBride and McKinna](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.2479&rep=rep1&type=pdf)
+  Note that Lean uses the *locally nameless approach*. See [McBride and McKinna](https://doi.org/10.1145/1017472.1017477)
   for additional details.
 
   When "visiting" the body of a binding expression (i.e. `lam`, `forallE`, or `letE`),
   bound variables are converted into free variables using a unique identifier,
-  and their user-facing name, type, value (for `LetE`), and binder annotation
+  and their user-facing name, type, value (for `letE`), and binder annotation
   are stored in the `LocalContext`.
   -/
   | fvar (fvarId : FVarId)
@@ -363,7 +363,7 @@ inductive Expr where
   A function application.
 
   For example, the natural number one, i.e. `Nat.succ Nat.zero` is represented as
-  ``Expr.app (.const `Nat.succ []) (.const .zero [])``.
+  ``Expr.app (.const `Nat.succ []) (.const `Nat.zero [])``.
   Note that multiple arguments are represented using partial application.
 
   For example, the two argument application `f x y` is represented as
@@ -383,7 +383,7 @@ inductive Expr where
   | lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)
 
   /--
-  A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may dependent
+  A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may depend
   on `a`. Note that this constructor is also used to represent non-dependent arrows
   where `β` does not depend on `a`.
 

src/Lean/Meta/Basic.lean

@@ -760,6 +760,7 @@ have to hard-code the true arity of these definitions here, and make sure the C
 We have used another hack based on `IO.Ref`s in the past, it was safer but less efficient.
 -/
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Reduces an expression to its *weak head normal form*.
 This is when the "head" of the top-level expression has been fully reduced.
@@ -768,6 +769,7 @@ The result may contain subexpressions that have not been reduced.
 See `Lean.Meta.whnfImp` for the implementation.
 -/
 @[extern "lean_whnf"] opaque whnf : Expr → MetaM Expr
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns the inferred type of the given expression. Assumes the expression is type-correct.
 
@@ -822,8 +824,11 @@ def e3 : Expr := .app (.const ``Nat.zero []) (.const ``Nat.zero [])
 See `Lean.Meta.inferTypeImp` for the implementation of `inferType`.
 -/
 @[extern "lean_infer_type"] opaque inferType : Expr → MetaM Expr
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_is_expr_def_eq"] opaque isExprDefEqAux : Expr → Expr → MetaM Bool
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_is_level_def_eq"] opaque isLevelDefEqAux : Level → Level → MetaM Bool
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_synth_pending"] protected opaque synthPending : MVarId → MetaM Bool
 
 def whnfForall (e : Expr) : MetaM Expr := do
@@ -2498,6 +2503,7 @@ def isDefEqD (t s : Expr) : MetaM Bool :=
 def isDefEqI (t s : Expr) : MetaM Bool :=
   withReducibleAndInstances <| isDefEq t s
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns `true` if `mvarId := val` was successfully assigned.
 This method uses the same assignment validation performed by `isDefEq`, but it does not check whether the types match.
@@ -2710,7 +2716,14 @@ where
         -- catch all exceptions
         let _ : MonadExceptOf _ MetaM := MonadAlwaysExcept.except
         observing do
-          withDeclNameForAuxNaming constName do
+          -- Re-privatize private `constName` under the current module so that auxiliary
+          -- declarations generated during realization get names scoped to the realizing module,
+          -- not the original defining module. This prevents name collisions when the same
+          -- constant is realized independently from two modules that are later imported together
+          -- (diamond import pattern).
+          let namePrefix :=
+            if isPrivateName constName then mkPrivateName env constName else constName
+          withDeclNameForAuxNaming namePrefix do
             withoutExporting (when := isPrivateName constName) do
               realize
           -- Meta code working on a non-exported declaration should usually do so inside

src/Lean/Meta/Match/MatchEqsExt.lean

@@ -46,12 +46,14 @@ Forward definition of `getEquationsForImpl`.
 We want to use `getEquationsFor` in the simplifier,
 getEquationsFor` depends on `mkEquationsFor` which uses the simplifier.
 -/
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_get_match_equations_for"]
 opaque getEquationsFor (matchDeclName : Name) : MetaM MatchEqns
 
 /-
 Forward definition of `genMatchCongrEqnsImpl`.
 -/
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_get_congr_match_equations_for"]
 opaque genMatchCongrEqns (matchDeclName : Name) : MetaM (Array Name)
 

src/Lean/Meta/Sym/Eta.lean

@@ -30,12 +30,12 @@ then returns `f`. Otherwise, returns `e`.
 Returns the original expression when not reducible to enable pointer equality checks.
 -/
 public def etaReduce (e : Expr) : Expr :=
-  go e 0
+  if e.isLambda then go e 0 else e
 where
   go (body : Expr) (n : Nat) : Expr :=
     match body with
     | .lam _ _ b _ => go b (n+1)
-    | _ => if n == 0 then e else etaReduceAux body n 0 e
+    | _ => etaReduceAux body n 0 e
 
 /-- Returns `true` if `e` can be eta-reduced. Uses pointer equality for efficiency. -/
 public def isEtaReducible (e : Expr) : Bool :=

src/Lean/Meta/Sym/Pattern.lean

@@ -17,7 +17,7 @@ import Lean.Meta.Sym.ProofInstInfo
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.Offset
 import Lean.Meta.Sym.Eta
-import Lean.Meta.AbstractMVars
+import Lean.Meta.Sym.Util
 import Init.Data.List.MapIdx
 import Init.Data.Nat.Linear
 import Std.Do.Triple.Basic
@@ -31,7 +31,9 @@ framework (`Sym`). The design prioritizes performance by using a two-phase appro
 # Phase 1 (Syntactic Matching)
 - Patterns use de Bruijn indices for expression variables and renamed level params (`_uvar.0`, `_uvar.1`, ...) for universe variables
 - Matching is purely structural after reducible definitions are unfolded during preprocessing
-- Universe levels treat `max` and `imax` as uninterpreted functions (no AC reasoning)
+- Universe levels are eagerly normalized in patterns and normalized on the target side during matching
+- `tryApproxMaxMax` handles `max` commutativity when one argument matches structurally. It is relevant
+  for constraints such as `max ?u a =?= max a b`
 - Binders and term metavariables are deferred to Phase 2
 
 # Phase 2 (Pending Constraints)
@@ -107,6 +109,7 @@ def preprocessDeclPattern (declName : Name) : MetaM (List Name × Expr) := do
   let us := levelParams.map mkLevelParam
   let type ← instantiateTypeLevelParams info.toConstantVal us
   let type ← preprocessType type
+  let type ← normalizeLevels type
   return (levelParams, type)
 
 def preprocessExprPattern (e : Expr) (levelParams₀ : List Name) : MetaM (List Name × Expr) := do
@@ -115,6 +118,7 @@ def preprocessExprPattern (e : Expr) (levelParams₀ : List Name) : MetaM (List
   let us := levelParams.map mkLevelParam
   let type := type.instantiateLevelParams levelParams₀ us
   let type ← preprocessType type
+  let type ← normalizeLevels type
   return (levelParams, type)
 
 /--
@@ -261,45 +265,6 @@ public def mkEqPatternFromDecl (declName : Name) : MetaM (Pattern × Expr) := do
     let_expr Eq _ lhs rhs := type | throwError "conclusion is not a equality{indentExpr type}"
     return (lhs, rhs)
 
-/--
-Like `mkPatternCore` but takes a lambda expression instead of a forall type.
-Uses `lambdaBoundedTelescope` to open binders and detect instance/proof arguments.
--/
-def mkPatternCoreFromLambda (lam : Expr) (levelParams : List Name)
-    (varTypes : Array Expr) (pattern : Expr) : MetaM Pattern := do
-  let fnInfos ← mkProofInstInfoMapFor pattern
-  let checkTypeMask := mkCheckTypeMask pattern varTypes.size
-  let checkTypeMask? := if checkTypeMask.all (· == false) then none else some checkTypeMask
-  let varInfos? ← lambdaBoundedTelescope lam varTypes.size fun xs _ =>
-    mkProofInstArgInfo? xs
-  return { levelParams, varTypes, pattern, fnInfos, varInfos?, checkTypeMask? }
-
-def mkPatternFromLambda (levelParams : List Name) (lam : Expr) : MetaM Pattern := do
-  let rec go (pattern : Expr) (varTypes : Array Expr) : MetaM Pattern := do
-    if let .lam _ d b _ := pattern then
-      return (← go b (varTypes.push d))
-    let pattern ← preprocessType pattern
-    mkPatternCoreFromLambda lam levelParams varTypes pattern
-  go lam #[]
-
-/--
-Creates a `Pattern` from an expression containing metavariables.
-
-Metavariables in `e` become pattern variables (wildcards). For example,
-`Nat.succ ?m` produces a pattern matching `Nat.succ _` with discrimination
-tree keys `[Nat.succ, *]`.
-
-This is used for user-registered simproc patterns where the user provides
-an expression with underscores (elaborated as metavariables) to specify
-what the simproc should match.
--/
-public def mkSimprocPatternFromExpr (e : Expr) : MetaM Pattern := do
-  let result ← abstractMVars e
-  let levelParams := result.paramNames.mapIdx fun i _ => Name.num uvarPrefix i
-  let us := levelParams.toList.map mkLevelParam
-  let expr := result.expr.instantiateLevelParamsArray result.paramNames us.toArray
-  mkPatternFromLambda levelParams.toList expr
-
 structure UnifyM.Context where
   pattern   : Pattern
   unify     : Bool := true
@@ -365,35 +330,42 @@ def assignLevel (uidx : Nat) (u : Level) : UnifyM Bool := do
     modify fun s => { s with uAssignment := s.uAssignment.set! uidx (some u) }
     return true
 
-def processLevel (u : Level) (v : Level) : UnifyM Bool := do
-  match u, v with
-  | .zero, .zero => return true
-  | .succ u, .succ v => processLevel u v
-  | .zero, .succ _ => return false
-  | .succ _, .zero => return false
-  | .zero, .max v₁ v₂ => processLevel .zero v₁ <&&> processLevel .zero v₂
-  | .max u₁ u₂, .zero => processLevel u₁ .zero <&&> processLevel u₂ .zero
-  | .zero, .imax _ v => processLevel .zero v
-  | .imax _ u, .zero => processLevel u .zero
-  | .max u₁ u₂, .max v₁ v₂ => processLevel u₁ v₁ <&&> processLevel u₂ v₂
-  | .imax u₁ u₂, .imax v₁ v₂ => processLevel u₁ v₁ <&&> processLevel u₂ v₂
-  | .param uName, _ =>
-    if let some uidx := isUVar? uName then
-      assignLevel uidx v
-    else if u == v then
-      return true
-    else if v.isMVar && (← read).unify then
-      pushLevelPending u v
-      return true
-    else
-      return false
-  | .mvar _, _ | _, .mvar _ =>
-    if (← read).unify then
-      pushLevelPending u v
-      return true
-    else
-      return false
-  | _, _ => return false
+def processLevel (u : Level) (v : Level) : UnifyM Bool :=
+  go u v.normalize
+where
+  go (u : Level) (v : Level) : UnifyM Bool := do
+    match u, v with
+    | .zero, .zero => return true
+    | .succ u, .succ v => go u v
+    | .zero, .succ _ => return false
+    | .succ _, .zero => return false
+    | .zero, .max v₁ v₂ => go .zero v₁ <&&> go .zero v₂
+    | .max u₁ u₂, .zero => go u₁ .zero <&&> go u₂ .zero
+    | .zero, .imax _ v => go .zero v
+    | .imax _ u, .zero => go u .zero
+    | .max u₁ u₂, .max v₁ v₂ =>
+      -- tryApproxMaxMax: find a shared concrete arg between both sides
+      if u₂ == v₁ then go u₁ v₂
+      else if u₁ == v₂ then go u₂ v₁
+      else go u₁ v₁ <&&> go u₂ v₂
+    | .imax u₁ u₂, .imax v₁ v₂ => go u₁ v₁ <&&> go u₂ v₂
+    | .param uName, _ =>
+      if let some uidx := isUVar? uName then
+        assignLevel uidx v
+      else if u == v then
+        return true
+      else if v.isMVar && (← read).unify then
+        pushLevelPending u v
+        return true
+      else
+        return false
+    | .mvar _, _ | _, .mvar _ =>
+      if (← read).unify then
+        pushLevelPending u v
+        return true
+      else
+        return false
+    | _, _ => return false
 
 def processLevels (us : List Level) (vs : List Level) : UnifyM Bool := do
   match us, vs with
@@ -542,7 +514,7 @@ def tryAssignLevelMVar (u : Level) (v : Level) : MetaM Bool := do
 
 /--
 Structural definitional equality for universe levels.
-Treats `max` and `imax` as uninterpreted functions (no AC reasoning).
+Uses `tryApproxMaxMax` to handle `max` commutativity when one argument matches structurally.
 Attempts metavariable assignment in both directions if structural matching fails.
 -/
 def isLevelDefEqS (u : Level) (v : Level) : MetaM Bool := do
@@ -556,7 +528,10 @@ def isLevelDefEqS (u : Level) (v : Level) : MetaM Bool := do
   | .max u₁ u₂, .zero => isLevelDefEqS u₁ .zero <&&> isLevelDefEqS u₂ .zero
   | .zero, .imax _ v => isLevelDefEqS .zero v
   | .imax _ u, .zero => isLevelDefEqS u .zero
-  | .max u₁ u₂, .max v₁ v₂ => isLevelDefEqS u₁ v₁ <&&> isLevelDefEqS u₂ v₂
+  | .max u₁ u₂, .max v₁ v₂ =>
+    if u₂ == v₁ then isLevelDefEqS u₁ v₂
+    else if u₁ == v₂ then isLevelDefEqS u₂ v₁
+    else isLevelDefEqS u₁ v₁ <&&> isLevelDefEqS u₂ v₂
   | .imax u₁ u₂, .imax v₁ v₂ => isLevelDefEqS u₁ v₁ <&&> isLevelDefEqS u₂ v₂
   | _, _ => tryAssignLevelMVar u v <||> tryAssignLevelMVar v u
 
@@ -598,6 +573,7 @@ structure DefEqM.Context where
 
 abbrev DefEqM := ReaderT DefEqM.Context SymM
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Structural definitional equality. It is much cheaper than `isDefEq`.
 

src/Lean/Meta/Sym/Simp/DiscrTree.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Sym.Pattern
 public import Lean.Meta.DiscrTree.Basic
 import Lean.Meta.Sym.Offset
+import Lean.Meta.Sym.Eta
 import Init.Omega
 namespace Lean.Meta.Sym
 open DiscrTree
@@ -154,7 +155,7 @@ partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Array α) :
     else if h : csize = 0 then
       result
     else
-      let e     := todo.back!
+      let e     := etaReduce todo.back!
       let todo  := todo.pop
       let first := cs[0] /- Recall that `Key.star` is the minimal key -/
       if csize = 1 then
@@ -184,6 +185,7 @@ public def getMatch (d : DiscrTree α) (e : Expr) : Array α :=
   let result := match d.root.find? .star with
   | none              => .mkEmpty initCapacity
   | some (.node vs _) => vs
+  let e := etaReduce e
   match d.root.find? (getKey e) with
   | none   => result
   | some c => getMatchLoop (pushArgsTodo #[] e) c result
@@ -196,6 +198,7 @@ This is useful for rewriting: if a pattern matches `f x` but `e` is `f x y z`, w
 still apply the rewrite and return `(value, 2)` indicating 2 extra arguments.
 -/
 public partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : Array (α × Nat) :=
+  let e := etaReduce e
   let result := getMatch d e
   let result := result.map (·, 0)
   if !e.isApp then

src/Lean/Meta/Sym/Simp/SimpM.lean

@@ -227,6 +227,7 @@ def SimpM.run' (x : SimpM α) (methods : Methods := {}) (config : Config := {})
   let initialLCtxSize := (← getLCtx).decls.size
   x methods.toMethodsRef { initialLCtxSize, config } |>.run' {}
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_sym_simp"] -- Forward declaration
 opaque simp : Simproc