diff --git a/Mathlib/Data/String/Basic.lean b/Mathlib/Data/String/Basic.lean
index 7559cf41206de..12216a94ec0db 100644
--- a/Mathlib/Data/String/Basic.lean
+++ b/Mathlib/Data/String/Basic.lean
@@ -120,18 +120,22 @@ theorem toList_inj {s₁ s₂ : String} : s₁.toList = s₂.toList ↔ s₁ = s
   ⟨congr_arg mk, congr_arg toList⟩
 #align string.to_list_inj String.toList_inj
 
-theorem nil_asString_eq_empty : [].asString = "" :=
+theorem asString_nil : [].asString = "" :=
   rfl
-#align string.nil_as_string_eq_empty String.nil_asString_eq_empty
+#align string.nil_as_string_eq_empty String.asString_nil
+
+@[deprecated (since := "2024-06-04")] alias nil_asString_eq_empty := asString_nil
 
 @[simp]
 theorem toList_empty : "".toList = [] :=
   rfl
 #align string.to_list_empty String.toList_empty
 
-theorem asString_inv_toList (s : String) : s.toList.asString = s :=
+theorem asString_toList (s : String) : s.toList.asString = s :=
   rfl
-#align string.as_string_inv_to_list String.asString_inv_toList
+#align string.as_string_inv_to_list String.asString_toList
+
+@[deprecated (since := "2024-06-04")] alias asString_inv_toList := asString_toList
 
 #align string.to_list_singleton String.data_singleton
 
@@ -175,26 +179,32 @@ end String
 
 open String
 
-theorem List.toList_inv_asString (l : List Char) : l.asString.toList = l :=
+namespace List
+
+theorem toList_asString (l : List Char) : l.asString.toList = l :=
   rfl
-#align list.to_list_inv_as_string List.toList_inv_asString
+#align list.to_list_inv_as_string List.toList_asString
+
+@[deprecated (since := "2024-06-04")] alias toList_inv_asString := toList_asString
 
 @[simp]
-theorem List.length_asString (l : List Char) : l.asString.length = l.length :=
+theorem length_asString (l : List Char) : l.asString.length = l.length :=
   rfl
 #align list.length_as_string List.length_asString
 
 @[simp]
-theorem List.asString_inj {l l' : List Char} : l.asString = l'.asString ↔ l = l' :=
-  ⟨fun h ↦ by rw [← toList_inv_asString l, ← toList_inv_asString l', toList_inj, h],
+theorem asString_inj {l l' : List Char} : l.asString = l'.asString ↔ l = l' :=
+  ⟨fun h ↦ by rw [← toList_asString l, ← toList_asString l', toList_inj, h],
    fun h ↦ h ▸ rfl⟩
 #align list.as_string_inj List.asString_inj
 
+theorem asString_eq {l : List Char} {s : String} : l.asString = s ↔ l = s.toList := by
+  rw [← asString_toList s, asString_inj, asString_toList s]
+#align list.as_string_eq List.asString_eq
+
+end List
+
 @[simp]
 theorem String.length_data (s : String) : s.data.length = s.length :=
   rfl
 #align string.length_to_list String.length_data
-
-theorem List.asString_eq {l : List Char} {s : String} : l.asString = s ↔ l = s.toList := by
-  rw [← asString_inv_toList s, asString_inj, asString_inv_toList s]
-#align list.as_string_eq List.asString_eq
diff --git a/Mathlib/Data/String/Defs.lean b/Mathlib/Data/String/Defs.lean
index d8b8c55547b62..e2d887121b371 100644
--- a/Mathlib/Data/String/Defs.lean
+++ b/Mathlib/Data/String/Defs.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Keeley Hoek, Floris van Doorn, Chris Bailey
 -/
 import Batteries.Data.List.Basic
+import Batteries.Data.String.Basic
 import Mathlib.Mathport.Rename
 
 #align_import data.string.defs from "leanprover-community/mathlib"@"e7131068d9696deec51e6cd7668b6d9ac69af6a4"
@@ -53,11 +54,8 @@ def mapTokens (c : Char) (f : String → String) : String → String :=
   intercalate (singleton c) ∘ List.map f ∘ (·.split (· = c))
 #align string.map_tokens String.mapTokens
 
-/-- `getRest s t` returns `some r` if `s = t ++ r`.
-If `t` is not a prefix of `s`, it returns `none`. -/
-def getRest (s t : String) : Option String :=
-  List.asString <$> s.toList.getRest t.toList
-#align string.get_rest String.getRest
+@[deprecated (since := "2024-06-04")] alias getRest := dropPrefix?
+#align string.get_rest String.dropPrefix?
 
 #align string.popn String.drop