refactor: reduce duplication in string pattern lemmas

[TwoFX]

This PR takes a more principled approach in deriving String pattern lemmas by reducing to simpler cases similar to how the instances are defined.

This reduces duplication of complex arguments (at the expense of having to state more simple lemmas; however these lemmas are useful to users as well).

[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 59711e5cff9327526391097f7536587676e25b01 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-04 18:35:59)

[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 59711e5cff9327526391097f7536587676e25b01 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-04 18:36:01)