From 59f3156eb1e6dc959aa5fd6b0004231d506ebcf2 Mon Sep 17 00:00:00 2001
From: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Date: Mon, 23 Mar 2026 09:21:38 +0000
Subject: [PATCH] chore: variants of `String.toNat?` lemmas

---
 src/Std/Data/String/ToInt.lean | 16 ++++++++++++++++
 src/Std/Data/String/ToNat.lean | 16 ++++++++++++++++
 2 files changed, 32 insertions(+)

diff --git a/src/Std/Data/String/ToInt.lean b/src/Std/Data/String/ToInt.lean
index 1c48c977db45..83b28de6d013 100644
--- a/src/Std/Data/String/ToInt.lean
+++ b/src/Std/Data/String/ToInt.lean
@@ -98,18 +98,34 @@ end Slice
 public theorem isInt_toSlice {s : String} : s.toSlice.isInt = s.isInt :=
   (rfl)
 
+@[simp]
+public theorem isInt_comp_toSlice : String.Slice.isInt ∘ String.toSlice = String.isInt := by
+  ext; simp
+
 @[simp]
 public theorem toInt?_toSlice {s : String} : s.toSlice.toInt? = s.toInt? :=
   (rfl)
 
+@[simp]
+public theorem toInt?_comp_toSlice : String.Slice.toInt? ∘ String.toSlice = String.toInt? := by
+  ext; simp
+
 @[simp]
 public theorem Slice.isInt_copy {s : Slice} : s.copy.isInt = s.isInt := by
   simpa [← isInt_toSlice] using Slice.isInt_congr (by simp)
 
+@[simp]
+public theorem Slice.isInt_comp_copy : String.isInt ∘ String.Slice.copy = String.Slice.isInt := by
+  ext; simp
+
 @[simp]
 public theorem Slice.toInt?_copy {s : Slice} : s.copy.toInt? = s.toInt? := by
   simpa [← isInt_toSlice] using Slice.toInt?_congr (by simp)
 
+@[simp]
+public theorem Slice.toInt?_comp_copy : String.toInt? ∘ String.Slice.copy = String.Slice.toInt? := by
+  ext; simp
+
 public theorem toInt?_eq_some_iff {s : String} {a : Int} :
     s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = (b : Int)) ∨ ∃ t, s = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -(b : Int) := by
   simp [← toInt?_toSlice, Slice.toInt?_eq_some_iff]
diff --git a/src/Std/Data/String/ToNat.lean b/src/Std/Data/String/ToNat.lean
index 990f07a9f342..b214c149453a 100644
--- a/src/Std/Data/String/ToNat.lean
+++ b/src/Std/Data/String/ToNat.lean
@@ -221,18 +221,34 @@ namespace String
 public theorem isNat_toSlice {s : String} : s.toSlice.isNat = s.isNat :=
   (rfl)
 
+@[simp]
+public theorem isNat_comp_toSlice : String.Slice.isNat ∘ String.toSlice = String.isNat := by
+  ext; simp
+
 @[simp]
 public theorem toNat?_toSlice {s : String} : s.toSlice.toNat? = s.toNat? :=
   (rfl)
 
+@[simp]
+public theorem toNat?_comp_toSlice : String.Slice.toNat? ∘ String.toSlice = String.toNat? := by
+  ext; simp
+
 @[simp]
 public theorem Slice.isNat_copy {s : Slice} : s.copy.isNat = s.isNat := by
   simpa [← isNat_toSlice] using Slice.isNat_congr (by simp)
 
+@[simp]
+public theorem Slice.isNat_comp_copy : String.isNat ∘ String.Slice.copy = String.Slice.isNat := by
+  ext; simp
+
 @[simp]
 public theorem Slice.toNat?_copy {s : Slice} : s.copy.toNat? = s.toNat? := by
   simpa [← isNat_toSlice] using Slice.toNat?_congr (by simp)
 
+@[simp]
+public theorem Slice.toNat?_comp_copy : String.toNat? ∘ String.Slice.copy = String.Slice.toNat? := by
+  ext; simp
+
 public theorem isNat_iff {s : String} :
     s.isNat = true ↔
       s ≠ "" ∧