nightly#121 adaptations for nightly-2025-11-20

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-11-20 nightly#121 Please review this PR. At the next toolchain release this diff will land in 'master'.

[Kevin Buzzard]

I sometimes merge these PRs but 95% of the changes made in this PR are completely beyond my pay grade so I'm not going to merge these. It would be good if someone could look at them or else nightly testing will just get more and more behind.

[Kim Morrison]

This one is fine: it has lots of changes to the String API, which Markus has prepared, and a few places where grind temporarily needed to be grind +revert, but some subsequent bug fixes will allow reverting this, which is on my TODO list.

[Kim Morrison]