batteries#1629 adaptations for nightly-2026-01-24

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2026-01-24 batteries#1629

Please review this PR. At the end of the month this diff will land in 'main'.

[Kim Morrison]

@François G. Dorais, could we just merge these instead of closing? It seems no more work, and

1. Makes no difference to what main looks like, as we squash merge the bump/v4.28.0 branches.
2. Records in the git history for bump/v4.28.0 that we've successfully advanced batteries to each of these nightlies.
3. The release automation includes a guard condition that bump/v4.28.0 is actually up to date with the nightly-testing content, which fails (and causes me to have to manually reopen and merge the last of these PRs) if we close these PRs rather than merging them.