From 7b2942536174910ae5ceb693e624aaa6dfafa6de Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 12 Feb 2026 07:10:36 +0100
Subject: [PATCH] chore: simplify `Char.toString` to `String.singleton`
 (#12449)

This PR marks `String.toString_eq_singleton` as a `simp` lemma.
---
 src/Init/Data/Char/Lemmas.lean  | 1 +
 src/Init/Data/String/Basic.lean | 5 +++--
 2 files changed, 4 insertions(+), 2 deletions(-)

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