nightly#172 adaptations for nightly-2026-02-03

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2026-02-03 nightly#172

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

[Kim Morrison]

This is a complicated one. I attempted to implement this via a script, but it has too many "attribute [local instance] in file X requires an attribute [instance_reducible] in earlier file Y" to automate.

[Kim Morrison]

The basic change here is that you can not add instance or local instance after the fact anymore unless the original definition is instance_reducible (which is a new reducibility setting). It's not enforced right now, but our recommendation is that you set instance_reducible at the moment of definition, and never change it!

[Kim Morrison]

This is consequences of lean#12247 and lean#12263.

[Kevin Buzzard]

I reviewed https://github.com/leanprover-community/mathlib4-nightly-testing/pull/173 instead so probably this one can be closed?