From ce073771b14ebdcf2846fc00e597cb54c5352b24 Mon Sep 17 00:00:00 2001
From: Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Tue, 24 Mar 2026 18:51:06 +0100
Subject: [PATCH] feat: `String.drop` lemmas (#13109)

This PR adds lemmas about the `String` operations `drop`, `dropEnd`,
`take`, `takeEnd`.
---
 src/Init/Data/String/Lemmas.lean          |  1 +
 src/Init/Data/String/Lemmas/TakeDrop.lean | 86 +++++++++++++++++++++++
 2 files changed, 87 insertions(+)
 create mode 100644 src/Init/Data/String/Lemmas/TakeDrop.lean

diff --git a/src/Init/Data/String/Lemmas.lean b/src/Init/Data/String/Lemmas.lean
index 57ce958d8f..eedcd4311f 100644
--- a/src/Init/Data/String/Lemmas.lean
+++ b/src/Init/Data/String/Lemmas.lean
@@ -19,6 +19,7 @@ public import Init.Data.String.Lemmas.Iterate
 public import Init.Data.String.Lemmas.Intercalate
 public import Init.Data.String.Lemmas.Iter
 public import Init.Data.String.Lemmas.Hashable
+public import Init.Data.String.Lemmas.TakeDrop
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
 import Init.Data.Char.Lemmas
diff --git a/src/Init/Data/String/Lemmas/TakeDrop.lean b/src/Init/Data/String/Lemmas/TakeDrop.lean
new file mode 100644
index 0000000000..83735c6d6c
--- /dev/null
+++ b/src/Init/Data/String/Lemmas/TakeDrop.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.TakeDrop
+import all Init.Data.String.Slice
+import all Init.Data.String.TakeDrop
+import Init.Data.String.Lemmas.Splits
+
+public section
+
+namespace String
+
+namespace Slice
+
+theorem drop_eq_sliceFrom {s : Slice} {n : Nat} : s.drop n = s.sliceFrom (s.startPos.nextn n) :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_drop {s : Slice} {n : Nat} : (s.drop n).copy.toList = s.copy.toList.drop n := by
+  simp [drop_eq_sliceFrom, (s.splits_nextn_startPos n).copy_sliceFrom_eq]
+
+theorem dropEnd_eq_sliceTo {s : Slice} {n : Nat} : s.dropEnd n = s.sliceTo (s.endPos.prevn n) :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_dropEnd {s : Slice} {n : Nat} :
+    (s.dropEnd n).copy.toList = s.copy.toList.take (s.copy.length - n) := by
+  simp [dropEnd_eq_sliceTo, (s.splits_prevn_endPos n).copy_sliceTo_eq]
+
+theorem take_eq_sliceTo {s : Slice} {n : Nat} : s.take n = s.sliceTo (s.startPos.nextn n) :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_take {s : Slice} {n : Nat} : (s.take n).copy.toList = s.copy.toList.take n := by
+  simp [take_eq_sliceTo, (s.splits_nextn_startPos n).copy_sliceTo_eq]
+
+theorem takeEnd_eq_sliceFrom {s : Slice} {n : Nat} : s.takeEnd n = s.sliceFrom (s.endPos.prevn n) :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_takeEnd {s : Slice} {n : Nat} :
+    (s.takeEnd n).copy.toList = s.copy.toList.drop (s.copy.length - n) := by
+  simp [takeEnd_eq_sliceFrom, (s.splits_prevn_endPos n).copy_sliceFrom_eq]
+
+end Slice
+
+@[simp]
+theorem drop_toSlice {s : String} {n : Nat} : s.toSlice.drop n = s.drop n :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_drop {s : String} {n : Nat} : (s.drop n).copy.toList = s.toList.drop n := by
+  simp [← drop_toSlice]
+
+@[simp]
+theorem dropEnd_toSlice {s : String} {n : Nat} : s.toSlice.dropEnd n = s.dropEnd n :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_dropEnd {s : String} {n : Nat} :
+    (s.dropEnd n).copy.toList = s.toList.take (s.length - n) := by
+  simp [← dropEnd_toSlice]
+
+@[simp]
+theorem take_toSlice {s : String} {n : Nat} : s.toSlice.take n = s.take n :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_take {s : String} {n : Nat} : (s.take n).copy.toList = s.toList.take n := by
+  simp [← take_toSlice]
+
+@[simp]
+theorem takeEnd_toSlice {s : String} {n : Nat} : s.toSlice.takeEnd n = s.takeEnd n :=
+  (rfl)
+
+@[simp]
+theorem toList_copy_takeEnd {s : String} {n : Nat} :
+    (s.takeEnd n).copy.toList = s.toList.drop (s.length - n) := by
+  simp [← takeEnd_toSlice]
+
+end String