diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean
index f064f01613..e8727e877e 100644
--- a/src/Init/Data/Char/Lemmas.lean
+++ b/src/Init/Data/Char/Lemmas.lean
@@ -83,6 +83,7 @@ def notLTTotal : Std.Total (¬ · < · : Char → Char → Prop) where
 @[simp]
 theorem toUInt8_val {c : Char} : c.val.toUInt8 = c.toUInt8 := rfl
 
+@[simp]
 theorem toString_eq_singleton {c : Char} : c.toString = String.singleton c := rfl
 
 end Char
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index f95ecc87af..362f5532e0 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -3085,7 +3085,8 @@ end String
 
 namespace Char
 
-@[simp] theorem length_toString (c : Char) : c.toString.length = 1 := by
-  simp [toString_eq_singleton]
+@[deprecated String.length_singleton (since := "2026-02-12")]
+theorem length_toString (c : Char) : c.toString.length = 1 := by
+  simp
 
 end Char