nightly#48 adaptations for nightly-2025-08-30

Stream: nightly-testing

[Kim Morrison]

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

[Kevin Buzzard]

I mostly-reviewed https://github.com/leanprover-community/mathlib4-nightly-testing/pull/47 here but the PR now has conflicts. This will be the same, I can't review the meta code and I'm reluctant to review the non-meta code because I feel I already did it once. Are we stuck?

[Kim Morrison]

Sorry about this. I will work on nightly#47 shortly.

[Kim Morrison]

By way of background: the next steps in this situation are:

• merge master in bump/v4.24.0, resolving conflicts to one's best ability
• merge bump/v4.24.0 into nightly#47
• get things working again, then merge nightly#47

Then repeat those steps for nightly#48, nightly#49, but this time merging nightly#47 rather than bump/v4.24.0 into nightly#48, and so on, until we've caught up!

[Kim Morrison]

@Heather Macbeth, @Michael Rothgang, there is a hint test here that used to report field_simp succeeded, but now doesn't.

Could I ask you to take a look on the nightly-testing branch and decide what, if anything, should be done with this test?

[Heather Macbeth]

Hmm: I'm on 16575b154651ef009f3ef5fe28b5c0f01a5f2c92 and I don't get the error. Let me wait and see what CI says.

[Kim Morrison]

Oh -- @Heather Macbeth, sorry I should have been more specific: I updated the test to get a green tick. The missing field_simp is in section field_simp of MathlibTest/hint.lean.

[Kim Morrison]

Hopefully nightly#48 is the next PR in line to review (diff should reflect only changes after nightly#47 now!) and merge.

[Heather Macbeth]

Kim Morrison said:

The missing field_simp is in section field_simp of MathlibTest/hint.lean.

Ah, I see. Yes, this is expected, see also the changes to the field_simp test file. The new field_simp requires CommGroupWithZero.

[Kim Morrison]

I've merged nightly#48.