nightly#167 adaptations for nightly-2026-01-29

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2026-01-29 nightly#167

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

[Johan Commelin]

Almost all changes are due to the new +instances flag for (d)simp.
There are a few other innocent changes

One change is a grind regression that is not so nice. But also not terrible. And clearly flagged with an #adaptation_note.