batteries#1481 adaptations for nightly-2025-10-29

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-10-29 batteries#1481 Please review this PR. At the end of the month this diff will land in 'main'.

[Kim Morrison]

Notable in this update is Batteries/Data/String/Legacy.lean, which downstreams old definitions of operations on Strings, so as not to break the lemmas in Batteries about these operations.

[Kim Morrison]

Once this lands in main in ~2 weeks, I hope we can consider if some of this can be deprecated, so users (if such exist) can transition to the new string operations and their lemmas.