feat: lemmas about String.find? and String.contains (#12777)

This PR adds lemmas about `String.find?` and `String.contains`.

src/Init/Data/String/Basic.lean

@@ -1978,6 +1978,7 @@ theorem Pos.ne_of_lt {s : String} {p q : s.Pos} : p < q → p ≠ q := by
 theorem Pos.lt_of_lt_of_le {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r := by
   simpa [Pos.lt_iff, Pos.le_iff] using Pos.Raw.lt_of_lt_of_le
 
+@[simp]
 theorem Pos.le_endPos {s : String} (p : s.Pos) : p ≤ s.endPos := by
   simpa [Pos.le_iff] using p.isValid.le_rawEndPos
 

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

@@ -16,6 +16,9 @@ import Init.ByCases
 import Init.Data.Iterators.Lemmas.Combinators.FilterMap
 import Init.Data.String.Lemmas.Basic
 import Init.Data.Iterators.Lemmas.Consumers.Loop
+public import Init.Data.String.Lemmas.Order
+import Init.Data.String.OrderInstances
+import Init.Data.Subtype.Basic
 
 set_option doc.verso true
 
@@ -47,6 +50,19 @@ theorem Model.positionsFrom_eq_cons {s : Slice} {p : s.Pos} (hp : p ≠ s.endPos
   rw [Model.positionsFrom]
   simp [hp]
 
+@[simp]
+theorem Model.mem_positionsFrom {s : Slice} {p : s.Pos} {q : { q : s.Pos // q ≠ s.endPos } } :
+    q ∈ Model.positionsFrom p ↔ p ≤ q := by
+  induction p using Pos.next_induction with
+  | next p h ih =>
+    rw [Model.positionsFrom_eq_cons h, List.mem_cons, ih]
+    simp [Subtype.ext_iff, Std.le_iff_lt_or_eq (a := p), or_comm, eq_comm]
+  | endPos => simp [q.property]
+
+theorem Model.mem_positionsFrom_startPos {s : Slice} {q : { q : s.Pos // q ≠ s.endPos} } :
+    q ∈ Model.positionsFrom s.startPos := by
+  simp
+
 theorem Model.map_get_positionsFrom_of_splits {s : Slice} {p : s.Pos} {t₁ t₂ : String}
     (hp : p.Splits t₁ t₂) : (Model.positionsFrom p).map (fun p => p.1.get p.2) = t₂.toList := by
   induction p using Pos.next_induction generalizing t₁ t₂ with
@@ -60,7 +76,6 @@ theorem Model.map_get_positionsFrom_startPos {s : Slice} :
     (Model.positionsFrom s.startPos).map (fun p => p.1.get p.2) = s.copy.toList :=
   Model.map_get_positionsFrom_of_splits (splits_startPos s)
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem toList_positionsFrom {s : Slice} {p : s.Pos} :
     (s.positionsFrom p).toList = Model.positionsFrom p := by
@@ -80,6 +95,38 @@ theorem toList_positions {s : Slice} : s.positions.toList = Model.positionsFrom
 theorem toList_chars {s : Slice} : s.chars.toList = s.copy.toList := by
   simp [chars, Model.map_get_positionsFrom_startPos]
 
+theorem mem_toList_copy_iff_exists_get {s : Slice} {c : Char} :
+    c ∈ s.copy.toList ↔ ∃ (p : s.Pos) (h : p ≠ s.endPos), p.get h = c := by
+  simp [← Model.map_get_positionsFrom_startPos]
+
+theorem Pos.Splits.mem_toList_left_iff {s : Slice} {pos : s.Pos} {t u : String} {c : Char}
+    (hs : pos.Splits t u) :
+    c ∈ t.toList ↔ ∃ pos', ∃ (h : pos' < pos), pos'.get (Pos.ne_endPos_of_lt h) = c := by
+  rw [hs.eq_left pos.splits, mem_toList_copy_iff_exists_get]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨p, hp, hpget⟩
+    have hlt : Pos.ofSliceTo p < pos := by
+      simpa using Pos.ofSliceTo_lt_ofSliceTo_iff.mpr ((Pos.lt_endPos_iff _).mpr hp)
+    exact ⟨_, hlt, by rwa [Pos.get_eq_get_ofSliceTo] at hpget⟩
+  · rintro ⟨pos', hlt, hget⟩
+    exact ⟨pos.sliceTo pos' (Std.le_of_lt hlt),
+      by simpa [← Pos.ofSliceTo_inj] using Std.ne_of_lt hlt,
+      by rw [Slice.Pos.get_eq_get_ofSliceTo]; simpa using hget⟩
+
+theorem Pos.Splits.mem_toList_right_iff {s : Slice} {pos : s.Pos} {t u : String} {c : Char}
+    (hs : pos.Splits t u) :
+    c ∈ u.toList ↔ ∃ pos', ∃ (_ : pos ≤ pos') (h : pos' ≠ s.endPos), pos'.get h = c := by
+  rw [hs.eq_right pos.splits, mem_toList_copy_iff_exists_get]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨p, hp, hpget⟩
+    exact ⟨Pos.ofSliceFrom p, Pos.le_ofSliceFrom,
+      fun h => hp (Pos.ofSliceFrom_inj.mp (h.trans (Pos.ofSliceFrom_endPos (pos := pos)).symm)),
+      by rwa [Pos.get_eq_get_ofSliceFrom] at hpget⟩
+  · rintro ⟨pos', hle, hne, hget⟩
+    exact ⟨pos.sliceFrom pos' hle,
+      fun h => hne (by simpa using congrArg Pos.ofSliceFrom h),
+      by rw [Pos.get_eq_get_ofSliceFrom]; simpa using hget⟩
+
 /--
 A list of all positions strictly before {name}`p`, ordered from largest to smallest.
 
@@ -115,7 +162,6 @@ theorem Model.map_get_revPositionsFrom_endPos {s : Slice} :
     (Model.revPositionsFrom s.endPos).map (fun p => p.1.get p.2) = s.copy.toList.reverse :=
   Model.map_get_revPositionsFrom_of_splits (splits_endPos s)
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem toList_revPositionsFrom {s : Slice} {p : s.Pos} :
     (s.revPositionsFrom p).toList = Model.revPositionsFrom p := by
@@ -168,6 +214,19 @@ theorem Model.positionsFrom_eq_cons {s : String} {p : s.Pos} (hp : p ≠ s.endPo
   rw [Model.positionsFrom]
   simp [hp]
 
+@[simp]
+theorem Model.mem_positionsFrom {s : String} {p : s.Pos} {q : { q : s.Pos // q ≠ s.endPos } } :
+    q ∈ Model.positionsFrom p ↔ p ≤ q := by
+  induction p using Pos.next_induction with
+  | next p h ih =>
+    rw [Model.positionsFrom_eq_cons h, List.mem_cons, ih]
+    simp [Subtype.ext_iff, Std.le_iff_lt_or_eq (a := p), or_comm, eq_comm]
+  | endPos => simp [q.property]
+
+theorem Model.mem_positionsFrom_startPos {s : String} {q : { q : s.Pos // q ≠ s.endPos} } :
+    q ∈ Model.positionsFrom s.startPos := by
+  simp
+
 theorem Model.positionsFrom_eq_map {s : String} {p : s.Pos} :
     Model.positionsFrom p = (Slice.Model.positionsFrom p.toSlice).map
       (fun p => ⟨Pos.ofToSlice p.1, by simpa [← Pos.toSlice_inj] using p.2⟩) := by
@@ -199,6 +258,38 @@ theorem toList_positions {s : String} : s.positions.toList = Model.positionsFrom
 theorem toList_chars {s : String} : s.chars.toList = s.toList := by
   simp [chars]
 
+theorem mem_toList_iff_exists_get {s : String} {c : Char} :
+    c ∈ s.toList ↔ ∃ (p : s.Pos) (h : p ≠ s.endPos), p.get h = c := by
+  simp [← Model.map_get_positionsFrom_startPos]
+
+theorem Pos.Splits.mem_toList_left_iff {s : String} {pos : s.Pos} {t u : String} {c : Char}
+    (hs : pos.Splits t u) :
+    c ∈ t.toList ↔ ∃ pos', ∃ (h : pos' < pos), pos'.get (Pos.ne_endPos_of_lt h) = c := by
+  rw [hs.eq_left pos.splits, Slice.mem_toList_copy_iff_exists_get]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨p, hp, hpget⟩
+    have hlt : Pos.ofSliceTo p < pos := by
+      simpa using Pos.ofSliceTo_lt_ofSliceTo_iff.mpr ((Slice.Pos.lt_endPos_iff _).mpr hp)
+    exact ⟨_, hlt, by rwa [Pos.get_eq_get_ofSliceTo] at hpget⟩
+  · rintro ⟨pos', hlt, hget⟩
+    exact ⟨pos.sliceTo pos' (Std.le_of_lt hlt),
+      fun h => Std.ne_of_lt hlt (by simpa using congrArg Pos.ofSliceTo h),
+      by rw [Pos.get_eq_get_ofSliceTo]; simpa using hget⟩
+
+theorem Pos.Splits.mem_toList_right_iff {s : String} {pos : s.Pos} {t u : String} {c : Char}
+    (hs : pos.Splits t u) :
+    c ∈ u.toList ↔ ∃ pos', ∃ (_ : pos ≤ pos') (h : pos' ≠ s.endPos), pos'.get h = c := by
+  rw [hs.eq_right pos.splits, Slice.mem_toList_copy_iff_exists_get]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨p, hp, hpget⟩
+    exact ⟨Pos.ofSliceFrom p, Pos.le_ofSliceFrom,
+      fun h => hp (Pos.ofSliceFrom_inj.mp (h.trans Pos.ofSliceFrom_endPos.symm)),
+      by rwa [Pos.get_eq_get_ofSliceFrom] at hpget⟩
+  · rintro ⟨pos', hle, hne, hget⟩
+    exact ⟨pos.sliceFrom pos' hle,
+      fun h => hne (by simpa using congrArg Pos.ofSliceFrom h),
+      by rw [Pos.get_eq_get_ofSliceFrom]; simpa using hget⟩
+
 /--
 A list of all positions strictly before {name}`p`, ordered from largest to smallest.
 

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

@@ -290,6 +290,70 @@ theorem Pos.ofSliceTo_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).P
     Pos.ofSliceTo p ≤ q ↔ ∀ h, p ≤ Pos.sliceTo p₀ q h := by
   simp [← Std.not_lt, Pos.lt_ofSliceTo_iff]
 
+theorem Slice.Pos.lt_sliceFrom_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} :
+    p < Slice.Pos.sliceFrom p₀ q h ↔ Pos.ofSliceFrom p < q := by
+  simp [ofSliceFrom_lt_iff, h]
+
+theorem Slice.Pos.sliceFrom_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} :
+    Slice.Pos.sliceFrom p₀ q h ≤ p ↔ q ≤ Pos.ofSliceFrom p := by
+  simp [← Std.not_lt, lt_sliceFrom_iff]
+
+theorem Slice.Pos.le_sliceFrom_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} :
+    p ≤ Slice.Pos.sliceFrom p₀ q h ↔ Pos.ofSliceFrom p ≤ q := by
+  simp [ofSliceFrom_le_iff, h]
+
+theorem Slice.Pos.sliceFrom_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} :
+    Slice.Pos.sliceFrom p₀ q h < p ↔ q < Pos.ofSliceFrom p := by
+  simp [← Std.not_le, le_sliceFrom_iff]
+
+theorem Pos.lt_sliceFrom_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} :
+    p < Pos.sliceFrom p₀ q h ↔ Pos.ofSliceFrom p < q := by
+  simp [ofSliceFrom_lt_iff, h]
+
+theorem Pos.sliceFrom_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} :
+    Pos.sliceFrom p₀ q h ≤ p ↔ q ≤ Pos.ofSliceFrom p := by
+  simp [← Std.not_lt, lt_sliceFrom_iff]
+
+theorem Pos.le_sliceFrom_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} :
+    p ≤ Pos.sliceFrom p₀ q h ↔ Pos.ofSliceFrom p ≤ q := by
+  simp [ofSliceFrom_le_iff, h]
+
+theorem Pos.sliceFrom_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h} :
+    Pos.sliceFrom p₀ q h < p ↔ q < Pos.ofSliceFrom p := by
+  simp [← Std.not_le, le_sliceFrom_iff]
+
+theorem Slice.Pos.sliceTo_le_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} :
+    Pos.sliceTo p₀ q h ≤ p ↔ q ≤ Pos.ofSliceTo p := by
+  simp [le_ofSliceTo_iff, h]
+
+theorem Slice.Pos.lt_sliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} :
+    p < Pos.sliceTo p₀ q h ↔ Pos.ofSliceTo p < q := by
+  simp [← Std.not_le, sliceTo_le_iff]
+
+theorem Slice.Pos.sliceTo_lt_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} :
+    Slice.Pos.sliceTo p₀ q h < p ↔ q < Pos.ofSliceTo p := by
+  simp [lt_ofSliceTo_iff, h]
+
+theorem Slice.Pos.le_sliceTo_iff {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} :
+    p ≤ Slice.Pos.sliceTo p₀ q h ↔ Pos.ofSliceTo p ≤ q := by
+  simp [← Std.not_lt, sliceTo_lt_iff]
+
+theorem Pos.sliceTo_le_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} :
+    Pos.sliceTo p₀ q h ≤ p ↔ q ≤ Pos.ofSliceTo p := by
+  simp [le_ofSliceTo_iff, h]
+
+theorem Pos.lt_sliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} :
+    p < Pos.sliceTo p₀ q h ↔ Pos.ofSliceTo p < q := by
+  simp [← Std.not_le, sliceTo_le_iff]
+
+theorem Pos.sliceTo_lt_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} :
+    Pos.sliceTo p₀ q h < p ↔ q < Pos.ofSliceTo p := by
+  simp [lt_ofSliceTo_iff, h]
+
+theorem Pos.le_sliceTo_iff {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h} :
+    p ≤ Pos.sliceTo p₀ q h ↔ Pos.ofSliceTo p ≤ q := by
+  simp [← Std.not_lt, sliceTo_lt_iff]
+
 theorem Slice.Pos.ofSliceTo_ne_endPos {s : Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos}
     (h : p ≠ (s.sliceTo p₀).endPos) : Pos.ofSliceTo p ≠ s.endPos := by
   refine (lt_endPos_iff _).1 (Std.lt_of_lt_of_le ?_ (le_endPos p₀))

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

@@ -12,3 +12,4 @@ public import Init.Data.String.Lemmas.Pattern.Pred
 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

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

@@ -12,6 +12,7 @@ public import Init.Data.Iterators.Consumers.Collect
 import all Init.Data.String.Pattern.Basic
 import Init.Data.String.OrderInstances
 import Init.Data.String.Lemmas.IsEmpty
+import Init.Data.String.Lemmas.Basic
 import Init.Data.String.Lemmas.Order
 import Init.Data.String.Termination
 import Init.Data.Order.Lemmas
@@ -168,6 +169,24 @@ theorem IsLongestMatchAt.eq {pat : ρ} [ForwardPatternModel pat] {s : Slice} {st
     endPos = endPos' := by
   simpa using h.isLongestMatch_sliceFrom.eq h'.isLongestMatch_sliceFrom
 
+private theorem isLongestMatch_of_eq {pat : ρ} [ForwardPatternModel pat] {s t : Slice}
+    {pos : s.Pos} {pos' : t.Pos} (h_eq : s = t) (h_pos : pos.offset = pos'.offset)
+    (hm : IsLongestMatch pat pos) : IsLongestMatch pat pos' := by
+  subst h_eq; exact (Slice.Pos.ext h_pos) ▸ hm
+
+theorem isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat]
+    {s : Slice} {base : s.Pos} {startPos endPos : (s.sliceFrom base).Pos} :
+    IsLongestMatchAt pat startPos endPos ↔ IsLongestMatchAt pat (Pos.ofSliceFrom startPos) (Pos.ofSliceFrom endPos) := by
+  constructor
+  · intro h
+    refine ⟨Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff.mpr h.le, ?_⟩
+    exact isLongestMatch_of_eq Slice.sliceFrom_sliceFrom
+      (by simp [Pos.Raw.ext_iff]; omega) h.isLongestMatch_sliceFrom
+  · intro h
+    refine ⟨Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff.mp h.le, ?_⟩
+    exact isLongestMatch_of_eq Slice.sliceFrom_sliceFrom.symm
+      (by simp [Pos.Raw.ext_iff]; omega) h.isLongestMatch_sliceFrom
+
 theorem IsLongestMatch.isLongestMatchAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat] {s : Slice}
     {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos} (h : IsLongestMatch pat pos) :
     IsLongestMatchAt pat p₀ (Slice.Pos.ofSliceFrom pos) where
@@ -198,6 +217,27 @@ theorem matchesAt_iff_exists_isMatch {pat : ρ} [ForwardPatternModel pat] {s : S
     ⟨Std.le_trans h₁ (by simpa [← Pos.ofSliceFrom_le_ofSliceFrom_iff] using hq.le_of_isMatch h₂),
      by simpa using hq⟩⟩
 
+@[simp]
+theorem not_matchesAt_endPos {pat : ρ} [ForwardPatternModel pat] {s : Slice} :
+    ¬ MatchesAt pat s.endPos := by
+  simp only [matchesAt_iff_exists_isMatch, Pos.endPos_le, exists_prop_eq]
+  intro h
+  simpa [← Pos.ofSliceFrom_inj] using h.ne_startPos
+
+theorem matchesAt_iff_matchesAt_ofSliceFrom {pat : ρ} [ForwardPatternModel pat] {s : Slice} {base : s.Pos}
+    {pos : (s.sliceFrom base).Pos} : MatchesAt pat pos ↔ MatchesAt pat (Pos.ofSliceFrom pos) := by
+  simp only [matchesAt_iff_exists_isLongestMatchAt]
+  constructor
+  · rintro ⟨endPos, h⟩
+    exact ⟨Pos.ofSliceFrom endPos, isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom.mp h⟩
+  · rintro ⟨endPos, h⟩
+    exact ⟨base.sliceFrom endPos (Std.le_trans Slice.Pos.le_ofSliceFrom h.le),
+           isLongestMatchAt_iff_isLongestMatchAt_ofSliceFrom.mpr (by simpa using h)⟩
+
+theorem IsLongestMatchAt.matchesAt {pat : ρ} [ForwardPatternModel pat] {s : Slice} {startPos endPos : s.Pos}
+    (h : IsLongestMatchAt pat startPos endPos) : MatchesAt pat startPos where
+  exists_isLongestMatchAt := ⟨_, h⟩
+
 open Classical in
 /--
 Noncomputable model function returning the end point of the longest match starting at the given

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

@@ -61,6 +61,16 @@ theorem matchesAt_iff {c : Char} {s : Slice} {pos : s.Pos} :
     MatchesAt c pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c := by
   simp [matchesAt_iff_exists_isLongestMatchAt, isLongestMatchAt_iff, exists_comm]
 
+theorem matchesAt_iff_splits {c : Char} {s : Slice} {pos : s.Pos} :
+    MatchesAt c pos ↔ ∃ t₁ t₂, pos.Splits t₁ (singleton c ++ t₂) := by
+  rw [matchesAt_iff]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨h, rfl⟩
+    exact ⟨_, _, pos.splits_next_right h⟩
+  · rintro ⟨t₁, t₂, hs⟩
+    have hne := hs.ne_endPos_of_singleton
+    exact ⟨hne, (singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm⟩
+
 theorem not_matchesAt_of_get_ne {c : Char} {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos}
     (hc : pos.get h ≠ c) : ¬ MatchesAt c pos := by
   simp [matchesAt_iff, hc]

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

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

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

@@ -0,0 +1,129 @@
+/-
+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.Slice
+public import Init.Data.String.Search
+public import Init.Data.String.Lemmas.Pattern.Basic
+import all Init.Data.String.Slice
+import all Init.Data.String.Search
+import Init.Data.Iterators.Lemmas.Consumers.Loop
+import Init.Data.String.Lemmas.Order
+import Init.Data.String.Lemmas.Basic
+import Init.Data.String.OrderInstances
+import Init.Grind
+
+public section
+
+open Std String.Slice Pattern Pattern.Model
+
+namespace String.Slice
+
+theorem Pattern.Model.find?_eq_some_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
+    [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
+    [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} :
+    s.find? pat = some pos ↔ MatchesAt pat pos ∧ (∀ pos', pos' < pos → ¬ MatchesAt pat pos') := by
+  rw [find?, ← Iter.findSome?_toList]
+  suffices ∀ (l : List (SearchStep s)) (pos : s.Pos) (hl : IsValidSearchFrom pat pos l) (pos' : s.Pos),
+      l.findSome? (fun | .matched s _ => some s | .rejected .. => none) = some pos' ↔
+        pos ≤ pos' ∧ MatchesAt pat pos' ∧ ∀ pos'', pos ≤ pos'' → pos'' < pos' → ¬ MatchesAt pat pos'' by
+    simpa using this (ToForwardSearcher.toSearcher pat s).toList s.startPos
+      (LawfulToForwardSearcherModel.isValidSearchFrom_toList s) pos
+  intro l pos hl pos'
+  induction hl with
+  | endPos => simp +contextual
+  | matched h₁ _ _ => have := h₁.matchesAt; grind
+  | mismatched => grind
+
+theorem Pattern.Model.find?_eq_none_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
+    [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
+    [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
+    s.find? pat = none ↔ ∀ (pos : s.Pos), ¬ MatchesAt pat pos := by
+  simp only [Option.eq_none_iff_forall_ne_some, ne_eq, find?_eq_some_iff, not_and,
+    Classical.not_forall, Classical.not_not]
+  refine ⟨fun _ pos => ?_, by grind⟩
+  induction pos using WellFounded.induction Pos.wellFounded_lt with grind
+
+@[simp]
+theorem isSome_find? {ρ : Type} (pat : ρ) {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
+    [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
+    [ToForwardSearcher pat σ] {s : Slice} : (s.find? pat).isSome = s.contains pat := by
+  rw [find?, contains, ← Iter.findSome?_toList, ← Iter.any_toList]
+  induction (ToForwardSearcher.toSearcher pat s).toList <;> grind
+
+@[simp]
+theorem find?_eq_none_iff {ρ : Type} (pat : ρ) {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
+    [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
+    [ToForwardSearcher pat σ] {s : Slice} : s.find? pat = none ↔ s.contains pat = false := by
+  rw [← Option.isNone_iff_eq_none, ← Option.isSome_eq_false_iff, isSome_find?]
+
+theorem Pattern.Model.contains_eq_false_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
+    [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
+    [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
+    s.contains pat = false ↔ ∀ (pos : s.Pos), ¬ MatchesAt pat pos := by
+  rw [← find?_eq_none_iff, Slice.find?_eq_none_iff]
+
+theorem Pattern.Model.contains_eq_true_iff {ρ : Type} (pat : ρ) [ForwardPatternModel pat] {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
+    [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
+    [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} :
+    s.contains pat ↔ ∃ (pos : s.Pos), MatchesAt pat pos := by
+  simp [← Bool.not_eq_false, contains_eq_false_iff]
+
+theorem Pos.find?_eq_find?_sliceFrom {ρ : Type} {pat : ρ} {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, IteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ]
+    {s : Slice} {p : s.Pos} :
+    p.find? pat = ((s.sliceFrom p).find? pat).map Pos.ofSliceFrom :=
+  (rfl)
+
+theorem Pattern.Model.posFind?_eq_some_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
+    [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
+    [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos pos' : s.Pos} :
+    pos.find? pat = some pos' ↔ pos ≤ pos' ∧ MatchesAt pat pos' ∧ (∀ pos'', pos ≤ pos'' → pos'' < pos' → ¬ MatchesAt pat pos'') := by
+  simp only [Pos.find?_eq_find?_sliceFrom, Option.map_eq_some_iff, find?_eq_some_iff,
+    matchesAt_iff_matchesAt_ofSliceFrom]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨pos', ⟨h₁, h₂⟩, rfl⟩
+    refine ⟨Pos.le_ofSliceFrom, h₁, fun p hp₁ hp₂ => ?_⟩
+    simpa using h₂ (Pos.sliceFrom _ _ hp₁) (Pos.sliceFrom_lt_iff.2 hp₂)
+  · rintro ⟨h₁, h₂, h₃⟩
+    refine ⟨Pos.sliceFrom _ _ h₁, ⟨by simpa using h₂, fun p hp₁ hp₂ => ?_⟩, by simp⟩
+    exact h₃ (Pos.ofSliceFrom p) Slice.Pos.le_ofSliceFrom (Pos.lt_sliceFrom_iff.1 hp₁) hp₂
+
+theorem Pattern.Model.posFind?_eq_none_iff {ρ : Type} {pat : ρ} [ForwardPatternModel pat] {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, Iterators.Finite (σ s) Id]
+    [∀ s, IteratorLoop (σ s) Id Id] [∀ s, LawfulIteratorLoop (σ s) Id Id]
+    [ToForwardSearcher pat σ] [LawfulToForwardSearcherModel pat] {s : Slice} {pos : s.Pos} :
+    pos.find? pat = none ↔ ∀ pos', pos ≤ pos' → ¬ MatchesAt pat pos' := by
+  rw [Pos.find?_eq_find?_sliceFrom, Option.map_eq_none_iff, Pattern.Model.find?_eq_none_iff]
+  simpa only [matchesAt_iff_matchesAt_ofSliceFrom] using ⟨fun h p hp =>
+    by simpa using h (Pos.sliceFrom _ _ hp), fun h p => by simpa using h _ Pos.le_ofSliceFrom⟩
+
+end Slice
+
+theorem Pos.find?_eq_find?_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, IteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ]
+    {s : String} {p : s.Pos} : p.find? pat = (p.toSlice.find? pat).map Pos.ofToSlice :=
+  (rfl)
+
+theorem find?_eq_find?_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, IteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ]
+    {s : String} : s.find? pat = (s.toSlice.find? pat).map Pos.ofToSlice :=
+  (rfl)
+
+theorem contains_eq_contains_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Type}
+    [∀ s, Iterator (σ s) Id (SearchStep s)] [∀ s, IteratorLoop (σ s) Id Id] [ToForwardSearcher pat σ]
+    {s : String} : s.contains pat = s.toSlice.contains pat :=
+  (rfl)
+
+end String

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

@@ -0,0 +1,174 @@
+/-
+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.Slice
+import Init.Data.String.Lemmas.Pattern.Find.Basic
+import Init.Data.String.Lemmas.Pattern.Char
+import Init.Data.String.Lemmas.Basic
+import Init.Data.String.Lemmas.Order
+import Init.Data.String.Termination
+import Init.Data.String.Lemmas.Iterate
+import Init.Grind
+import Init.Data.Option.Lemmas
+import Init.Data.String.OrderInstances
+
+namespace String.Slice
+
+theorem find?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} :
+    s.find? c = some pos ↔
+      ∃ h, pos.get h = c ∧ ∀ pos', (h' : pos' < pos) → pos'.get (Pos.ne_endPos_of_lt h') ≠ c := by
+  grind [Pattern.Model.find?_eq_some_iff, Pattern.Model.Char.matchesAt_iff]
+
+@[simp]
+theorem contains_char_eq {c : Char} {s : Slice} : s.contains c = decide (c ∈ s.copy.toList) := by
+  rw [Bool.eq_iff_iff, Pattern.Model.contains_eq_true_iff]
+  simp [Pattern.Model.Char.matchesAt_iff, mem_toList_copy_iff_exists_get]
+
+theorem find?_char_eq_some_iff_splits {c : Char} {s : Slice} {pos : s.Pos} :
+    s.find? c = some pos ↔ ∃ t u, pos.Splits t (singleton c ++ u) ∧ c ∉ t.toList := by
+  rw [find?_char_eq_some_iff]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨h, hget, hmin⟩
+    refine ⟨_, _, hget ▸ pos.splits_next_right h, fun hmem => ?_⟩
+    obtain ⟨pos', hlt, hpget⟩ := (hget ▸ pos.splits_next_right h).mem_toList_left_iff.mp hmem
+    exact absurd hpget (hmin _ hlt)
+  · rintro ⟨t, u, hs, hnotin⟩
+    have hne := hs.ne_endPos_of_singleton
+    exact ⟨hne, (singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm,
+      fun pos' hlt hget => hnotin (hs.mem_toList_left_iff.mpr ⟨pos', hlt, hget⟩)⟩
+
+theorem Pos.find?_char_eq_some_iff {c : Char} {s : Slice} {pos pos' : s.Pos} :
+    pos.find? c = some pos' ↔
+      pos ≤ pos' ∧ (∃ h, pos'.get h = c) ∧
+        ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → pos''.get (Pos.ne_endPos_of_lt h') ≠ c := by
+  grind [Pattern.Model.posFind?_eq_some_iff, Pattern.Model.Char.matchesAt_iff]
+
+theorem Pos.find?_char_eq_some_iff_splits {c : Char} {s : Slice} {pos : s.Pos}
+    {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} :
+    pos.find? c = some pos' ↔ ∃ v w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ c ∉ v.toList := by
+  rw [Pos.find?_char_eq_some_iff]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨hle, ⟨hne, hget⟩, hmin⟩
+    have hsplit := hget ▸ pos'.splits_next_right hne
+    obtain ⟨v, hv1, hv2⟩ := (hs.le_iff_exists_eq_append hsplit).mp hle
+    refine ⟨v, _, hsplit.of_eq hv1 rfl, fun hmem => ?_⟩
+    obtain ⟨_, hcopy⟩ :=
+      Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hv2, hsplit.of_eq hv1 rfl⟩
+    rw [← hcopy] at hmem
+    obtain ⟨p, hp, hpget⟩ := mem_toList_copy_iff_exists_get.mp hmem
+    have hlt : Pos.ofSlice p < pos' := by
+      simpa [← Slice.Pos.lt_endPos_iff, ← Pos.ofSlice_lt_ofSlice_iff] using hp
+    exact absurd (Pos.get_eq_get_ofSlice ▸ hpget) (hmin _ Pos.le_ofSlice hlt)
+  · rintro ⟨v, w, hsplit, hnotin⟩
+    have hne := hsplit.ne_endPos_of_singleton
+    have hu : u = v ++ (singleton c ++ w) :=
+      append_right_inj t |>.mp (hs.eq_append.symm.trans (by rw [hsplit.eq_append, append_assoc]))
+    have hle : pos ≤ pos' := (hs.le_iff_exists_eq_append hsplit).mpr ⟨v, rfl, hu⟩
+    refine ⟨hle,
+      ⟨hne, (singleton_append_inj.mp (hsplit.eq_right (pos'.splits_next_right hne))).1.symm⟩,
+      fun pos'' hle' hlt hget => hnotin ?_⟩
+    obtain ⟨_, hcopy⟩ :=
+      Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hu, hsplit⟩
+    rw [← hcopy]
+    exact mem_toList_copy_iff_exists_get.mpr
+      ⟨pos''.slice pos pos' hle' (Std.le_of_lt hlt),
+       fun h => Std.ne_of_lt hlt
+         (by rw [← Slice.Pos.ofSlice_slice (h₁ := hle') (h₂ := Std.le_of_lt hlt), h,
+                  Slice.Pos.ofSlice_endPos]),
+       by rw [Slice.Pos.get_eq_get_ofSlice]
+          simp [Slice.Pos.ofSlice_slice]
+          exact hget⟩
+
+theorem Pos.find?_char_eq_none_iff {c : Char} {s : Slice} {pos : s.Pos} :
+    pos.find? c = none ↔ ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → pos'.get h ≠ c := by
+  grind [Pattern.Model.posFind?_eq_none_iff, Pattern.Model.Char.matchesAt_iff]
+
+theorem Pos.find?_char_eq_none_iff_not_mem_of_splits {c : Char} {s : Slice} {pos : s.Pos}
+    {t u : String} (hs : pos.Splits t u) :
+    pos.find? c = none ↔ c ∉ u.toList := by
+  simp [Pos.find?_char_eq_none_iff, hs.mem_toList_right_iff]
+
+end Slice
+
+theorem Pos.find?_char_eq_some_iff {c : Char} {s : String} {pos pos' : s.Pos} :
+    pos.find? c = some pos' ↔
+      pos ≤ pos' ∧ (∃ h, pos'.get h = c) ∧
+        ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → pos''.get (Pos.ne_endPos_of_lt h') ≠ c := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.Pos.find?_char_eq_some_iff, ne_eq, endPos_toSlice]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨pos', ⟨h₁, ⟨h₂, rfl⟩, h₃⟩, rfl⟩
+    refine ⟨by simpa [Pos.ofToSlice_le_iff] using h₁,
+      ⟨by simpa [← Pos.ofToSlice_inj] using h₂, by simp [Pos.get_ofToSlice]⟩, ?_⟩
+    intro pos'' h₄ h₅
+    simpa using h₃ pos''.toSlice (by simpa [Pos.toSlice_le] using h₄) (by simpa using h₅)
+  · rintro ⟨h₁, ⟨h₂, hget⟩, h₃⟩
+    refine ⟨pos'.toSlice, ⟨by simpa [Pos.toSlice_le] using h₁,
+      ⟨by simpa [← Pos.toSlice_inj] using h₂, by simpa using hget⟩, fun p hp₁ hp₂ => ?_⟩,
+      by simp⟩
+    simpa using h₃ (Pos.ofToSlice p)
+      (by simpa [Pos.ofToSlice_le_iff] using hp₁) (by simpa using hp₂)
+
+theorem Pos.find?_char_eq_some_iff_splits {c : Char} {s : String} {pos : s.Pos}
+    {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} :
+    pos.find? c = some pos' ↔ ∃ v w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ c ∉ v.toList := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.Pos.find?_char_eq_some_iff_splits (Pos.splits_toSlice_iff.mpr hs)]
+  constructor
+  · rintro ⟨q, ⟨v, w, hsplit, hnotin⟩, rfl⟩
+    exact ⟨v, w, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hnotin⟩
+  · rintro ⟨v, w, hsplit, hnotin⟩
+    exact ⟨pos'.toSlice, ⟨v, w, Pos.splits_toSlice_iff.mpr hsplit, hnotin⟩, by simp⟩
+
+theorem Pos.find?_char_eq_none_iff {c : Char} {s : String} {pos : s.Pos} :
+    pos.find? c = none ↔ ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → pos'.get h ≠ c := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff,
+    Slice.Pos.find?_char_eq_none_iff, endPos_toSlice]
+  refine ⟨?_, ?_⟩
+  · intro h pos' h₁ h₂
+    simpa [Pos.get_ofToSlice] using
+      h pos'.toSlice (by simpa [Pos.toSlice_le] using h₁) (by simpa [← Pos.toSlice_inj] using h₂)
+  · intro h pos' h₁ h₂
+    simpa using h (Pos.ofToSlice pos')
+      (by simpa [Pos.ofToSlice_le_iff] using h₁) (by simpa [← Pos.ofToSlice_inj] using h₂)
+
+theorem Pos.find?_char_eq_none_iff_not_mem_of_splits {c : Char} {s : String} {pos : s.Pos}
+    {t u : String} (hs : pos.Splits t u) :
+    pos.find? c = none ↔ c ∉ u.toList := by
+  rw [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff]
+  exact Slice.Pos.find?_char_eq_none_iff_not_mem_of_splits (Pos.splits_toSlice_iff.mpr hs)
+
+theorem find?_char_eq_some_iff {c : Char} {s : String} {pos : s.Pos} :
+    s.find? c = some pos ↔
+      ∃ h, pos.get h = c ∧ ∀ pos', (h' : pos' < pos) → pos'.get (Pos.ne_endPos_of_lt h') ≠ c := by
+  simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_char_eq_some_iff, ne_eq,
+    endPos_toSlice, exists_and_right]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨pos, ⟨⟨h, rfl⟩, h'⟩, rfl⟩
+    refine ⟨⟨by simpa [← Pos.ofToSlice_inj] using h, by simp [Pos.get_ofToSlice]⟩, ?_⟩
+    intro pos' hp
+    simpa using h' pos'.toSlice hp
+  · rintro ⟨⟨h, hget⟩, hmin⟩
+    exact ⟨pos.toSlice, ⟨⟨by simpa [← Pos.toSlice_inj] using h, by simpa using hget⟩,
+      fun pos' hp => by simpa using hmin (Pos.ofToSlice pos') hp⟩, by simp⟩
+
+theorem find?_char_eq_some_iff_splits {c : Char} {s : String} {pos : s.Pos} :
+    s.find? c = some pos ↔ ∃ t u, pos.Splits t (singleton c ++ u) ∧ c ∉ t.toList := by
+  simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.find?_char_eq_some_iff_splits]
+  constructor
+  · rintro ⟨q, ⟨t, u, hsplit, hnotin⟩, rfl⟩
+    exact ⟨t, u, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hnotin⟩
+  · rintro ⟨t, u, hsplit, hnotin⟩
+    exact ⟨pos.toSlice, ⟨t, u, Pos.splits_toSlice_iff.mpr hsplit, hnotin⟩, by simp⟩
+
+@[simp]
+theorem contains_char_eq {c : Char} {s : String} : s.contains c = decide (c ∈ s.toList) := by
+  simp [contains_eq_contains_toSlice, Slice.contains_char_eq, copy_toSlice]
+
+end String

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

@@ -0,0 +1,367 @@
+/-
+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.Slice
+import Init.Data.String.Lemmas.Pattern.Find.Basic
+import Init.Data.String.Lemmas.Pattern.Pred
+import Init.Data.String.Lemmas.Basic
+import Init.Data.String.Lemmas.Order
+import Init.Data.String.Termination
+import Init.Data.String.Lemmas.Iterate
+import Init.Grind
+import Init.Data.Option.Lemmas
+import Init.Data.String.OrderInstances
+
+namespace String.Slice
+
+theorem find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
+    s.find? p = some pos ↔
+      ∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → p (pos'.get (Pos.ne_endPos_of_lt h')) = false := by
+  grind [Pattern.Model.find?_eq_some_iff, Pattern.Model.CharPred.matchesAt_iff]
+
+theorem find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
+    s.find? p = some pos ↔
+      ∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (Pos.ne_endPos_of_lt h')) := by
+  grind [Pattern.Model.find?_eq_some_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff]
+
+theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : Slice} {pos : s.Pos} :
+    s.find? p = some pos ↔
+      ∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, p d = false := by
+  rw [find?_bool_eq_some_iff]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨h, hp, hmin⟩
+    exact ⟨_, _, _, pos.splits_next_right h, hp, fun d hd => by
+      obtain ⟨pos', hlt, hpget⟩ := (pos.splits_next_right h).mem_toList_left_iff.mp hd
+      subst hpget; exact hmin _ hlt⟩
+  · rintro ⟨t, c, u, hs, hpc, hmin⟩
+    have hne := hs.ne_endPos_of_singleton
+    refine ⟨hne, ?_, fun pos' hlt => hmin _ (hs.mem_toList_left_iff.mpr ⟨pos', hlt, rfl⟩)⟩
+    rw [(singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm]
+    exact hpc
+
+theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : Slice}
+    {pos : s.Pos} :
+    s.find? p = some pos ↔
+      ∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, ¬ p d := by
+  rw [find?_prop_eq_some_iff]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨h, hp, hmin⟩
+    exact ⟨_, _, _, pos.splits_next_right h, hp, fun d hd => by
+      obtain ⟨pos', hlt, hpget⟩ := (pos.splits_next_right h).mem_toList_left_iff.mp hd
+      subst hpget; exact hmin _ hlt⟩
+  · rintro ⟨t, c, u, hs, hpc, hmin⟩
+    have hne := hs.ne_endPos_of_singleton
+    refine ⟨hne, ?_, fun pos' hlt => hmin _ (hs.mem_toList_left_iff.mpr ⟨pos', hlt, rfl⟩)⟩
+    rw [(singleton_append_inj.mp (hs.eq_right (pos.splits_next_right hne))).1.symm]
+    exact hpc
+
+@[simp]
+theorem contains_bool_eq {p : Char → Bool} {s : Slice} : s.contains p = s.copy.toList.any p := by
+  rw [Bool.eq_iff_iff, Pattern.Model.contains_eq_true_iff]
+  simp only [Pattern.Model.CharPred.matchesAt_iff, ne_eq, List.any_eq_true,
+    mem_toList_copy_iff_exists_get]
+  exact ⟨fun ⟨pos, h, hp⟩ => ⟨_, ⟨_, _, rfl⟩, hp⟩, fun ⟨_, ⟨p, h, h'⟩, hp⟩ => ⟨p, h, h' ▸ hp⟩⟩
+
+@[simp]
+theorem contains_prop_eq {p : Char → Prop} [DecidablePred p] {s : Slice} :
+    s.contains p = s.copy.toList.any p := by
+  rw [Bool.eq_iff_iff, Pattern.Model.contains_eq_true_iff]
+  simp only [Pattern.Model.CharPred.Decidable.matchesAt_iff, ne_eq, List.any_eq_true,
+    mem_toList_copy_iff_exists_get, decide_eq_true_eq]
+  exact ⟨fun ⟨pos, h, hp⟩ => ⟨_, ⟨_, _, rfl⟩, hp⟩, fun ⟨_, ⟨p, h, h'⟩, hp⟩ => ⟨p, h, h' ▸ hp⟩⟩
+
+theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos pos' : s.Pos} :
+    pos.find? p = some pos' ↔
+      pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
+        ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') →
+          p (pos''.get (Pos.ne_endPos_of_lt h')) = false := by
+  grind [Pattern.Model.posFind?_eq_some_iff, Pattern.Model.CharPred.matchesAt_iff]
+
+theorem Pos.find?_bool_eq_some_iff_splits {p : Char → Bool} {s : Slice} {pos : s.Pos}
+    {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} :
+    pos.find? p = some pos' ↔
+      ∃ v c w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧
+        ∀ d ∈ v.toList, p d = false := by
+  rw [Pos.find?_bool_eq_some_iff]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨hle, ⟨hne, hp⟩, hmin⟩
+    have hsplit := pos'.splits_next_right hne
+    obtain ⟨v, hv1, hv2⟩ := (hs.le_iff_exists_eq_append hsplit).mp hle
+    refine ⟨v, pos'.get hne, _, hsplit.of_eq hv1 rfl, hp, fun d hd => ?_⟩
+    obtain ⟨_, hcopy⟩ :=
+      Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hv2, hsplit.of_eq hv1 rfl⟩
+    rw [← hcopy] at hd
+    obtain ⟨q, hq, hqget⟩ := mem_toList_copy_iff_exists_get.mp hd
+    have hlt : Pos.ofSlice q < pos' := by
+      simpa [← Slice.Pos.lt_endPos_iff, ← Pos.ofSlice_lt_ofSlice_iff] using hq
+    subst hqget; rw [Slice.Pos.get_eq_get_ofSlice]; exact hmin _ Pos.le_ofSlice hlt
+  · rintro ⟨v, c, w, hsplit, hpc, hmin⟩
+    have hne := hsplit.ne_endPos_of_singleton
+    have hu : u = v ++ (singleton c ++ w) :=
+      append_right_inj t |>.mp (hs.eq_append.symm.trans (by rw [hsplit.eq_append, append_assoc]))
+    have hle : pos ≤ pos' := (hs.le_iff_exists_eq_append hsplit).mpr ⟨v, rfl, hu⟩
+    refine ⟨hle, ⟨hne, ?_⟩, fun pos'' hle' hlt => hmin _ ?_⟩
+    · rw [(singleton_append_inj.mp (hsplit.eq_right (pos'.splits_next_right hne))).1.symm]
+      exact hpc
+    · obtain ⟨_, hcopy⟩ :=
+        Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hu, hsplit⟩
+      rw [← hcopy]
+      exact mem_toList_copy_iff_exists_get.mpr
+        ⟨pos''.slice pos pos' hle' (Std.le_of_lt hlt),
+         fun h => Std.ne_of_lt hlt
+           (by rw [← Slice.Pos.ofSlice_slice (h₁ := hle') (h₂ := Std.le_of_lt hlt), h,
+                    Slice.Pos.ofSlice_endPos]),
+         by rw [Slice.Pos.get_eq_get_ofSlice]
+            simp [Slice.Pos.ofSlice_slice]⟩
+
+theorem Pos.find?_bool_eq_none_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
+    pos.find? p = none ↔
+      ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → p (pos'.get h) = false := by
+  grind [Pattern.Model.posFind?_eq_none_iff, Pattern.Model.CharPred.matchesAt_iff]
+
+theorem Pos.find?_bool_eq_none_iff_of_splits {p : Char → Bool} {s : Slice} {pos : s.Pos}
+    {t u : String} (hs : pos.Splits t u) :
+    pos.find? p = none ↔ ∀ c ∈ u.toList, p c = false := by
+  rw [Pos.find?_bool_eq_none_iff]
+  constructor
+  · intro h c hc
+    obtain ⟨pos', hle, hne, hget⟩ := hs.mem_toList_right_iff.mp hc
+    subst hget; exact h pos' hle hne
+  · intro h pos' hle hne
+    exact h _ (hs.mem_toList_right_iff.mpr ⟨pos', hle, hne, rfl⟩)
+
+theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : Slice}
+    {pos pos' : s.Pos} :
+    pos.find? p = some pos' ↔
+      pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
+        ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') →
+          ¬ p (pos''.get (Pos.ne_endPos_of_lt h')) := by
+  grind [Pattern.Model.posFind?_eq_some_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff]
+
+theorem Pos.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : Slice}
+    {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} :
+    pos.find? p = some pos' ↔
+      ∃ v c w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧ ∀ d ∈ v.toList, ¬ p d := by
+  rw [Pos.find?_prop_eq_some_iff]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨hle, ⟨hne, hp⟩, hmin⟩
+    have hsplit := pos'.splits_next_right hne
+    obtain ⟨v, hv1, hv2⟩ := (hs.le_iff_exists_eq_append hsplit).mp hle
+    refine ⟨v, pos'.get hne, _, hsplit.of_eq hv1 rfl, hp, fun d hd => ?_⟩
+    obtain ⟨_, hcopy⟩ :=
+      Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hv2, hsplit.of_eq hv1 rfl⟩
+    rw [← hcopy] at hd
+    obtain ⟨q, hq, hqget⟩ := mem_toList_copy_iff_exists_get.mp hd
+    have hlt : Pos.ofSlice q < pos' := by
+      simpa [← Slice.Pos.lt_endPos_iff, ← Pos.ofSlice_lt_ofSlice_iff] using hq
+    subst hqget; rw [Slice.Pos.get_eq_get_ofSlice]; exact hmin _ Pos.le_ofSlice hlt
+  · rintro ⟨v, c, w, hsplit, hpc, hmin⟩
+    have hne := hsplit.ne_endPos_of_singleton
+    have hu : u = v ++ (singleton c ++ w) :=
+      append_right_inj t |>.mp (hs.eq_append.symm.trans (by rw [hsplit.eq_append, append_assoc]))
+    have hle : pos ≤ pos' := (hs.le_iff_exists_eq_append hsplit).mpr ⟨v, rfl, hu⟩
+    refine ⟨hle, ⟨hne, ?_⟩, fun pos'' hle' hlt => hmin _ ?_⟩
+    · rw [(singleton_append_inj.mp (hsplit.eq_right (pos'.splits_next_right hne))).1.symm]
+      exact hpc
+    · obtain ⟨_, hcopy⟩ :=
+        Slice.copy_slice_eq_iff_splits.mpr ⟨t, _, hs.of_eq rfl hu, hsplit⟩
+      rw [← hcopy]
+      exact mem_toList_copy_iff_exists_get.mpr
+        ⟨pos''.slice pos pos' hle' (Std.le_of_lt hlt),
+         fun h => Std.ne_of_lt hlt
+           (by rw [← Slice.Pos.ofSlice_slice (h₁ := hle') (h₂ := Std.le_of_lt hlt), h,
+                    Slice.Pos.ofSlice_endPos]),
+         by rw [Slice.Pos.get_eq_get_ofSlice]
+            simp [Slice.Pos.ofSlice_slice]⟩
+
+theorem Pos.find?_prop_eq_none_iff {p : Char → Prop} [DecidablePred p] {s : Slice} {pos : s.Pos} :
+    pos.find? p = none ↔
+      ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → ¬ p (pos'.get h) := by
+  grind [Pattern.Model.posFind?_eq_none_iff, Pattern.Model.CharPred.Decidable.matchesAt_iff]
+
+theorem Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred p] {s : Slice}
+    {pos : s.Pos} {t u : String} (hs : pos.Splits t u) :
+    pos.find? p = none ↔ ∀ c ∈ u.toList, ¬ p c := by
+  rw [Pos.find?_prop_eq_none_iff]
+  constructor
+  · intro h c hc
+    obtain ⟨pos', hle, hne, hget⟩ := hs.mem_toList_right_iff.mp hc
+    subst hget; exact h pos' hle hne
+  · intro h pos' hle hne
+    exact h _ (hs.mem_toList_right_iff.mpr ⟨pos', hle, hne, rfl⟩)
+
+end String.Slice
+
+namespace String
+
+theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos pos' : s.Pos} :
+    pos.find? p = some pos' ↔
+      pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
+        ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') →
+          p (pos''.get (Pos.ne_endPos_of_lt h')) = false := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.Pos.find?_bool_eq_some_iff, endPos_toSlice]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨pos', ⟨h₁, ⟨h₂, hp⟩, h₃⟩, rfl⟩
+    refine ⟨by simpa [Pos.ofToSlice_le_iff] using h₁,
+      ⟨by simpa [← Pos.ofToSlice_inj] using h₂, by simpa [Pos.get_ofToSlice] using hp⟩, ?_⟩
+    intro pos'' h₄ h₅
+    simpa using h₃ pos''.toSlice (by simpa [Pos.toSlice_le] using h₄) (by simpa using h₅)
+  · rintro ⟨h₁, ⟨h₂, hp⟩, h₃⟩
+    refine ⟨pos'.toSlice, ⟨by simpa [Pos.toSlice_le] using h₁,
+      ⟨by simpa [← Pos.toSlice_inj] using h₂, by simpa using hp⟩, fun p hp₁ hp₂ => ?_⟩,
+      by simp⟩
+    simpa using h₃ (Pos.ofToSlice p)
+      (by simpa [Pos.ofToSlice_le_iff] using hp₁) (by simpa using hp₂)
+
+theorem Pos.find?_bool_eq_some_iff_splits {p : Char → Bool} {s : String} {pos : s.Pos}
+    {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} :
+    pos.find? p = some pos' ↔
+      ∃ v c w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧
+        ∀ d ∈ v.toList, p d = false := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.Pos.find?_bool_eq_some_iff_splits (Pos.splits_toSlice_iff.mpr hs)]
+  constructor
+  · rintro ⟨q, ⟨v, c, w, hsplit, hpc, hmin⟩, rfl⟩
+    exact ⟨v, c, w, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hpc, hmin⟩
+  · rintro ⟨v, c, w, hsplit, hpc, hmin⟩
+    exact ⟨pos'.toSlice, ⟨v, c, w, Pos.splits_toSlice_iff.mpr hsplit, hpc, hmin⟩, by simp⟩
+
+theorem Pos.find?_bool_eq_none_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
+    pos.find? p = none ↔
+      ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → p (pos'.get h) = false := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff,
+    Slice.Pos.find?_bool_eq_none_iff, endPos_toSlice]
+  refine ⟨?_, ?_⟩
+  · intro h pos' h₁ h₂
+    simpa [Pos.get_ofToSlice] using
+      h pos'.toSlice (by simpa [Pos.toSlice_le] using h₁) (by simpa [← Pos.toSlice_inj] using h₂)
+  · intro h pos' h₁ h₂
+    simpa using h (Pos.ofToSlice pos')
+      (by simpa [Pos.ofToSlice_le_iff] using h₁) (by simpa [← Pos.ofToSlice_inj] using h₂)
+
+theorem Pos.find?_bool_eq_none_iff_of_splits {p : Char → Bool} {s : String} {pos : s.Pos}
+    {t u : String} (hs : pos.Splits t u) :
+    pos.find? p = none ↔ ∀ c ∈ u.toList, p c = false := by
+  rw [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff]
+  exact Slice.Pos.find?_bool_eq_none_iff_of_splits (Pos.splits_toSlice_iff.mpr hs)
+
+theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : String}
+    {pos pos' : s.Pos} :
+    pos.find? p = some pos' ↔
+      pos ≤ pos' ∧ (∃ h, p (pos'.get h)) ∧
+        ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') →
+          ¬ p (pos''.get (Pos.ne_endPos_of_lt h')) := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.Pos.find?_prop_eq_some_iff, endPos_toSlice]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨pos', ⟨h₁, ⟨h₂, hp⟩, h₃⟩, rfl⟩
+    refine ⟨by simpa [Pos.ofToSlice_le_iff] using h₁,
+      ⟨by simpa [← Pos.ofToSlice_inj] using h₂, by simpa [Pos.get_ofToSlice] using hp⟩, ?_⟩
+    intro pos'' h₄ h₅
+    simpa using h₃ pos''.toSlice (by simpa [Pos.toSlice_le] using h₄) (by simpa using h₅)
+  · rintro ⟨h₁, ⟨h₂, hp⟩, h₃⟩
+    refine ⟨pos'.toSlice, ⟨by simpa [Pos.toSlice_le] using h₁,
+      ⟨by simpa [← Pos.toSlice_inj] using h₂, by simpa using hp⟩, fun p hp₁ hp₂ => ?_⟩,
+      by simp⟩
+    simpa using h₃ (Pos.ofToSlice p)
+      (by simpa [Pos.ofToSlice_le_iff] using hp₁) (by simpa using hp₂)
+
+theorem Pos.find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : String}
+    {pos : s.Pos} {t u : String} (hs : pos.Splits t u) {pos' : s.Pos} :
+    pos.find? p = some pos' ↔
+      ∃ v c w, pos'.Splits (t ++ v) (singleton c ++ w) ∧ p c ∧ ∀ d ∈ v.toList, ¬ p d := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.Pos.find?_prop_eq_some_iff_splits (Pos.splits_toSlice_iff.mpr hs)]
+  constructor
+  · rintro ⟨q, ⟨v, c, w, hsplit, hpc, hmin⟩, rfl⟩
+    exact ⟨v, c, w, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hpc, hmin⟩
+  · rintro ⟨v, c, w, hsplit, hpc, hmin⟩
+    exact ⟨pos'.toSlice, ⟨v, c, w, Pos.splits_toSlice_iff.mpr hsplit, hpc, hmin⟩, by simp⟩
+
+theorem Pos.find?_prop_eq_none_iff {p : Char → Prop} [DecidablePred p] {s : String}
+    {pos : s.Pos} :
+    pos.find? p = none ↔
+      ∀ pos', pos ≤ pos' → (h : pos' ≠ s.endPos) → ¬ p (pos'.get h) := by
+  simp only [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff,
+    Slice.Pos.find?_prop_eq_none_iff, endPos_toSlice]
+  refine ⟨?_, ?_⟩
+  · intro h pos' h₁ h₂
+    simpa [Pos.get_ofToSlice] using
+      h pos'.toSlice (by simpa [Pos.toSlice_le] using h₁) (by simpa [← Pos.toSlice_inj] using h₂)
+  · intro h pos' h₁ h₂
+    simpa using h (Pos.ofToSlice pos')
+      (by simpa [Pos.ofToSlice_le_iff] using h₁) (by simpa [← Pos.ofToSlice_inj] using h₂)
+
+theorem Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred p] {s : String}
+    {pos : s.Pos} {t u : String} (hs : pos.Splits t u) :
+    pos.find? p = none ↔ ∀ c ∈ u.toList, ¬ p c := by
+  rw [Pos.find?_eq_find?_toSlice, Option.map_eq_none_iff]
+  exact Slice.Pos.find?_prop_eq_none_iff_of_splits (Pos.splits_toSlice_iff.mpr hs)
+
+theorem find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos : s.Pos} :
+    s.find? p = some pos ↔
+      ∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → p (pos'.get (Pos.ne_endPos_of_lt h')) = false := by
+  simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_bool_eq_some_iff,
+    endPos_toSlice, exists_and_right]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨pos, ⟨⟨h, hp⟩, h'⟩, rfl⟩
+    refine ⟨⟨by simpa [← Pos.ofToSlice_inj] using h, by simpa [Pos.get_ofToSlice] using hp⟩, ?_⟩
+    intro pos' hp
+    simpa using h' pos'.toSlice hp
+  · rintro ⟨⟨h, hp⟩, hmin⟩
+    exact ⟨pos.toSlice, ⟨⟨by simpa [← Pos.toSlice_inj] using h, by simpa using hp⟩,
+      fun pos' hp => by simpa using hmin (Pos.ofToSlice pos') hp⟩, by simp⟩
+
+theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : String} {pos : s.Pos} :
+    s.find? p = some pos ↔
+      ∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, p d = false := by
+  simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.find?_bool_eq_some_iff_splits]
+  constructor
+  · rintro ⟨q, ⟨t, c, u, hsplit, hpc, hmin⟩, rfl⟩
+    exact ⟨t, c, u, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hpc, hmin⟩
+  · rintro ⟨t, c, u, hsplit, hpc, hmin⟩
+    exact ⟨pos.toSlice, ⟨t, c, u, Pos.splits_toSlice_iff.mpr hsplit, hpc, hmin⟩, by simp⟩
+
+theorem find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : String} {pos : s.Pos} :
+    s.find? p = some pos ↔
+      ∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (Pos.ne_endPos_of_lt h')) := by
+  simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff, Slice.find?_prop_eq_some_iff,
+    endPos_toSlice, exists_and_right]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨pos, ⟨⟨h, hp⟩, h'⟩, rfl⟩
+    refine ⟨⟨by simpa [← Pos.ofToSlice_inj] using h, by simpa [Pos.get_ofToSlice] using hp⟩, ?_⟩
+    intro pos' hp
+    simpa using h' pos'.toSlice hp
+  · rintro ⟨⟨h, hp⟩, hmin⟩
+    exact ⟨pos.toSlice, ⟨⟨by simpa [← Pos.toSlice_inj] using h, by simpa using hp⟩,
+      fun pos' hp => by simpa using hmin (Pos.ofToSlice pos') hp⟩, by simp⟩
+
+theorem find?_prop_eq_some_iff_splits {p : Char → Prop} [DecidablePred p] {s : String}
+    {pos : s.Pos} :
+    s.find? p = some pos ↔
+      ∃ t c u, pos.Splits t (singleton c ++ u) ∧ p c ∧ ∀ d ∈ t.toList, ¬ p d := by
+  simp only [find?_eq_find?_toSlice, Option.map_eq_some_iff,
+    Slice.find?_prop_eq_some_iff_splits]
+  constructor
+  · rintro ⟨q, ⟨t, c, u, hsplit, hpc, hmin⟩, rfl⟩
+    exact ⟨t, c, u, Slice.Pos.splits_ofToSlice_iff.mpr hsplit, hpc, hmin⟩
+  · rintro ⟨t, c, u, hsplit, hpc, hmin⟩
+    exact ⟨pos.toSlice, ⟨t, c, u, Pos.splits_toSlice_iff.mpr hsplit, hpc, hmin⟩, by simp⟩
+
+@[simp]
+theorem contains_bool_eq {p : Char → Bool} {s : String} : s.contains p = s.toList.any p := by
+  simp [contains_eq_contains_toSlice, Slice.contains_bool_eq, copy_toSlice]
+
+@[simp]
+theorem contains_prop_eq {p : Char → Prop} [DecidablePred p] {s : String} :
+    s.contains p = s.toList.any p := by
+  simp [contains_eq_contains_toSlice, Slice.contains_prop_eq, copy_toSlice]
+
+end String

src/Init/Data/String/Search.lean

@@ -125,7 +125,7 @@ Examples:
 -/
 @[inline]
 def find? (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : Option s.Pos :=
-  s.startPos.find? pattern
+  (s.toSlice.find? pattern).map Pos.ofToSlice
 
 /--
 Finds the position of the first match of the pattern {name}`pattern` in a slice {name}`s`. If there
@@ -140,7 +140,7 @@ Examples:
 -/
 @[inline]
 def find (s : String) (pattern : ρ) [ToForwardSearcher pattern σ] : s.Pos :=
-  s.startPos.find pattern
+  Pos.ofToSlice (s.toSlice.find pattern)
 
 /--
 Finds the position of the first match of the pattern {name}`pattern` in a slice {name}`s` that is
@@ -189,7 +189,7 @@ Examples:
 -/
 @[inline]
 def revFind? (s : String) (pattern : ρ) [ToBackwardSearcher pattern σ] : Option s.Pos :=
-  s.endPos.revFind? pattern
+  (s.toSlice.revFind? pattern).map Pos.ofToSlice
 
 @[export lean_string_posof]
 def Internal.posOfImpl (s : String) (c : Char) : Pos.Raw :=

tests/lean/interactive/compNamespace.lean

@@ -3,12 +3,12 @@ namespace LongNamespaceExample
 
 def x := 10
 
-#check LongNam
-            --^ completion
+#check LongName
+             --^ completion
 end LongNamespaceExample
 
-#check LongNam
-            --^ completion
+#check LongName
+             --^ completion
 end Foo
 
 #check Foo.
@@ -18,5 +18,5 @@ end Foo
               --^ completion
 open Foo
 
-#check LongNam
-            --^ completion
+#check LongName
+             --^ completion

tests/lean/interactive/compNamespace.lean.expected.out

@@ -1,29 +1,29 @@
 {"textDocument": {"uri": "file:///compNamespace.lean"},
- "position": {"line": 5, "character": 14}}
+ "position": {"line": 5, "character": 15}}
 {"items":
  [{"label": "LongNamespaceExample",
    "kind": 9,
    "detail": "namespace",
-   "data": ["file:///compNamespace.lean", 5, 14, 0]}],
+   "data": ["file:///compNamespace.lean", 5, 15, 0]}],
  "isIncomplete": false}
 Resolution of LongNamespaceExample:
 {"label": "LongNamespaceExample",
  "kind": 9,
  "detail": "namespace",
- "data": ["file:///compNamespace.lean", 5, 14, 0]}
+ "data": ["file:///compNamespace.lean", 5, 15, 0]}
 {"textDocument": {"uri": "file:///compNamespace.lean"},
- "position": {"line": 9, "character": 14}}
+ "position": {"line": 9, "character": 15}}
 {"items":
  [{"label": "LongNamespaceExample",
    "kind": 9,
    "detail": "namespace",
-   "data": ["file:///compNamespace.lean", 9, 14, 0]}],
+   "data": ["file:///compNamespace.lean", 9, 15, 0]}],
  "isIncomplete": false}
 Resolution of LongNamespaceExample:
 {"label": "LongNamespaceExample",
  "kind": 9,
  "detail": "namespace",
- "data": ["file:///compNamespace.lean", 9, 14, 0]}
+ "data": ["file:///compNamespace.lean", 9, 15, 0]}
 {"textDocument": {"uri": "file:///compNamespace.lean"},
  "position": {"line": 13, "character": 11}}
 {"items":
@@ -51,15 +51,15 @@ Resolution of LongNamespaceExample:
  "detail": "namespace",
  "data": ["file:///compNamespace.lean", 16, 16, 0]}
 {"textDocument": {"uri": "file:///compNamespace.lean"},
- "position": {"line": 20, "character": 14}}
+ "position": {"line": 20, "character": 15}}
 {"items":
  [{"label": "LongNamespaceExample",
    "kind": 9,
    "detail": "namespace",
-   "data": ["file:///compNamespace.lean", 20, 14, 0]}],
+   "data": ["file:///compNamespace.lean", 20, 15, 0]}],
  "isIncomplete": false}
 Resolution of LongNamespaceExample:
 {"label": "LongNamespaceExample",
  "kind": 9,
  "detail": "namespace",
- "data": ["file:///compNamespace.lean", 20, 14, 0]}
+ "data": ["file:///compNamespace.lean", 20, 15, 0]}