nightly#23 adaptations for nightly-2025-07-29

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2025-07-29 nightly#23 Please review this PR. At the end of the month this diff will land in 'master'.

[Kim Morrison]

It worked, it worked! :-) :tada:

[Kim Morrison]

I merged this one, despite a CI failure in the noisy stdout check, because the PR itself contains a change to the noisy stdout check.