feat: String.toList_map

[TwoFX]

This PR adds more theory about Splits for strings and deduces the first user-facing String lemma, String.toList_map.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 16d00059914c7a333e02dcb9d64b180d73931e0a --onto 1ce05b2a179eac8a902995c0caddc609c0169c49. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-31 17:24:13)

[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 16d00059914c7a333e02dcb9d64b180d73931e0a --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-31 17:24:15)