nightly#56 adaptations for nightly-2025-09-05

Stream: nightly-testing

[github mathlib4 bot]

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

[Kevin Buzzard]

Hmm, I just merged nightly#53. Was that unwise? Will this now pick up a conflict? It's fine to merge

[Robin Arnez]

I think we only had toolchain changes the last two days, so this will just become a trivial change after the merge

[Kevin Buzzard]

Well it picked up conflicts unfortunately, and I don't know enough about the system behind what these PRs are doing to do next. I think what I've learnt is to not merge nightly#n if nightly#(n+1) has appeared.

[Kim Morrison]

The procedure now is:

git checkout bump/v4.24.0
git pull
git checkout bump/nightly-2025-09-05
git merge bump/v4.24.0
git push

(resolving conflicts as needed at the merge step).

[Kim Morrison]

(with the additional note that it doesn't matter how you merge conflicts in lake-manifest.json, just run lake update afterwards)

[Kim Morrison]

(Done: the diff is now just lean-toolchain and lake-manifest.json, so I have bors merged.)