From fe1ad52f88a2b72913f9cb5f218146cb5a0c584f Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 5 Mar 2026 11:00:17 +0100
Subject: [PATCH] fix: export `String.find?` and `String.contains` lemmas
 (#12807)

This PR makes the lemmas about `String.find?` and `String.contains` that
were added recently into public declarations.
---
 src/Init/Data/String/Lemmas/Pattern/Find/Char.lean |  8 ++++++--
 src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean | 12 ++++++++----
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean
index 11ab2c2ddf..c32d3e1a01 100644
--- a/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean
+++ b/src/Init/Data/String/Lemmas/Pattern/Find/Char.lean
@@ -7,6 +7,8 @@ module
 
 prelude
 public import Init.Data.String.Slice
+public import Init.Data.String.Search
+public import Init.Data.String.Lemmas.Splits
 import Init.Data.String.Lemmas.Pattern.Find.Basic
 import Init.Data.String.Lemmas.Pattern.Char
 import Init.Data.String.Lemmas.Basic
@@ -17,6 +19,8 @@ import Init.Grind
 import Init.Data.Option.Lemmas
 import Init.Data.String.OrderInstances
 
+public section
+
 namespace String.Slice
 
 theorem find?_char_eq_some_iff {c : Char} {s : Slice} {pos : s.Pos} :
@@ -98,7 +102,7 @@ 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
+        ∀ pos'', pos ≤ pos'' → (h' : pos'' < pos') → pos''.get (by exact 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 ⟨?_, ?_⟩
@@ -157,7 +161,7 @@ theorem contains_char_eq_contains_beq {c : Char} {s : String} :
 
 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
+      ∃ h, pos.get h = c ∧ ∀ pos', (h' : pos' < pos) → pos'.get (by exact 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 ⟨?_, ?_⟩
diff --git a/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean b/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean
index e8a52711bc..f9ac4bb832 100644
--- a/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean
+++ b/src/Init/Data/String/Lemmas/Pattern/Find/Pred.lean
@@ -7,6 +7,8 @@ module
 
 prelude
 public import Init.Data.String.Slice
+public import Init.Data.String.Search
+public import Init.Data.String.Lemmas.Splits
 import all Init.Data.String.Slice
 import all Init.Data.String.Search
 import Init.Data.String.Lemmas.Pattern.Find.Basic
@@ -19,6 +21,8 @@ import Init.Grind
 import Init.Data.Option.Lemmas
 import Init.Data.String.OrderInstances
 
+public section
+
 namespace String.Slice
 
 theorem find?_bool_eq_some_iff {p : Char → Bool} {s : Slice} {pos : s.Pos} :
@@ -178,7 +182,7 @@ theorem Pos.find?_bool_eq_some_iff {p : Char → Bool} {s : String} {pos 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
+          p (pos''.get (by exact 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 ⟨?_, ?_⟩
@@ -231,7 +235,7 @@ theorem Pos.find?_prop_eq_some_iff {p : Char → Prop} [DecidablePred p] {s : St
     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
+          ¬ p (pos''.get (by exact Pos.ne_endPos_of_lt h')) := by
   simp only [Pos.find?_prop_eq_find?_decide, Pos.find?_bool_eq_some_iff, decide_eq_true_eq,
     decide_eq_false_iff_not]
 
@@ -256,7 +260,7 @@ theorem Pos.find?_prop_eq_none_iff_of_splits {p : Char → Prop} [DecidablePred
 
 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
+      ∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → p (pos'.get (by exact 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 ⟨?_, ?_⟩
@@ -281,7 +285,7 @@ theorem find?_bool_eq_some_iff_splits {p : Char → Bool} {s : String} {pos : s.
 
 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
+      ∃ h, p (pos.get h) ∧ ∀ pos', (h' : pos' < pos) → ¬ p (pos'.get (by exact Pos.ne_endPos_of_lt h')) := by
   simp only [find?_prop_eq_find?_decide, find?_bool_eq_some_iff, decide_eq_true_eq,
     decide_eq_false_iff_not]