feat: String.toNat? lemmas

[TwoFX]

This PR redefines the String.isNat function to use less state and perform short-circuiting. It then verifies the String.isNat and String.toNat? functions.

Recall that isNat and toNat? allow _ as a digit separator. This is why we get the complicated statement

public theorem isNat_iff {s : String} :
    s.isNat = true ↔
      s ≠ "" ∧
      (∀ c ∈ s.toList, c.isDigit ∨ c = '_') ∧
      ¬ ['_', '_'] <:+: s.toList ∧
      s.toList.head? ≠ some '_' ∧
      s.toList.getLast? ≠ some '_'

For toNat?, we prove the fully general

public theorem toNat?_eq_some_ofDigitChars {s : String} (h : s.isNat = true) :
    s.toNat? = some (Nat.ofDigitChars 10 (s.toList.filter (· != '_')) 0)

as well as the useful (Nat.repr n).toNat? = some n (and the corollary that Nat.repr is injective).

For people implementing formatting routines that involve digit separators, we have

public theorem isNat_of_isDigit {s : String} (hne : s ≠ "")
    (hdigit : ∀ c ∈ s.toList, c.isDigit) : s.isNat = true

public theorem isNat_append_underscore_append {s t : String}
    (hs : s.isNat = true) (ht : t.isNat = true) :
    (s ++ "_" ++ t).isNat = true

public theorem toNat?_append_underscore_append_eq_some {s t : String} {n m : Nat}
    (hs : s.toNat? = some n) (ht : t.toNat? = some m) :
   (s ++ "_" ++ t).toNat? =
      some (10 ^ (t.toList.filter (· != '_')).length * n + m)

The missing bit here is (s.leftpad k '0').toNat? = s.toNat?, which is missing because we don't have String.leftpad (yet). For any reasonable definition of leftpad, this will follow from toNat?_eq_some_ofDigitChars since we prove the necessary ingredients about ofDigitChars.

There are some rough edges around ofDigitChars, and in the future it will be nice to connect this all to mathlib's Nat.digits and Nat.ofDigits, which are similar but different.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fe1ad52f88a2b72913f9cb5f218146cb5a0c584f --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-06 15:23:10)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fe1ad52f88a2b72913f9cb5f218146cb5a0c584f --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-06 15:23:11)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-17 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-18 16:45:58)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12828 build failed against this PR. (2026-03-18 17:38:45) View Log