feat: split and splitInclusive iterators are finite

[TwoFX]

This PR shows that the iterators returned by String.Slice.split and String.Slice.splitInclusive are finite as long as the forward matcher iterator for the pattern is finite (which we already know for all of our patterns).

At actually also completely redefines the iterators to avoid the inner loop in Internal.nextMatch which generates inefficient code. Instead, when encountering a mismach from the matcher, we skip the split iterator.

[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 69d8d63d58e56e873654341d4dddaac2c4a70737 --onto 4ce7ad19cea348506876685a19a7e0cca442c6d0. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-17 14:46:27)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 69d8d63d58e56e873654341d4dddaac2c4a70737 --onto 206eb73cd9de4b58abbb2eae20a41fd9b7af187b. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-20 07:43:14)

[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 69d8d63d58e56e873654341d4dddaac2c4a70737 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-17 14:46:29)