refactor: redefine String.replace

[TwoFX]

This PR defines String.Slice.replace and redefines String.replace to use the Slice version.

The new implementation is generic in the pattern, so it supports things like "education".replace isVowel "☃!" = "☃!d☃!c☃!t☃!☃!n". Since it uses the ForwardSearcher infrastructure, String patterns are searched using KMP, unlike the previous implementation which had quadratic runtime. As a side effect, the behavior when replacing an empty string now matches that of most other programming languages, namely "abc".replace "" "k" = "kakbkck".

[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 106b0fa661d96fd1fa6ff96e2ee5f55f23f307f2 --onto 19533ab1d4312903f98ff0429a5962db24ce402b. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-29 07:31:09)

[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 106b0fa661d96fd1fa6ff96e2ee5f55f23f307f2 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-29 07:31:11)