nightly#174 adaptations for nightly-2026-02-05

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2026-02-05 nightly#174

Please review this PR. At the next toolchain release this diff will land in 'master'.

[Kevin Buzzard]

OK so now we're running into problems, because this is two distinct big changes.

Can we get nightly#173 over the line first (I have reviewed and just have a couple of questions) and then perhaps ignore this one and hope that the next nightly diff is only +300 rather than +700, given that 173 is +400?

[Kim Morrison]

I've just sent nightly#173 to bors, then will get the diff sorted out here.

[Kim Morrison]

Okay, the diff is the real thing now.

[Kim Morrison]

I've put in a request at #mathlib4 > Technical Debt Counters @ 💬 for counters for all the new simp +instances and dsimp +instances which are now required. Help diagnosing and avoiding these very much appreciated.

[Kim Morrison]

It builds now

[Kim Morrison]

and I've reviewed the diff. Another set of eyes would be great, and we need to get this in as there's another batch of updates waiting!

[Kevin Buzzard]

CI is failing -- looks like we are declaring some lemmas twice?

[Kevin Buzzard]

OK I've gone through this and am happy to merge but CI is still failing.

[Kim Morrison]

I have fixed CI, and now merged.

[Kim Morrison]

Time for the next one!