nightly#177 adaptations for nightly-2026-02-15-rev1

Stream: nightly-testing

[github mathlib4 bot]

chore: adaptations for nightly-2026-02-15-rev1 nightly#177

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

[Kim Morrison]

Unfortunately nightly#176 rotted, and we now need to merge this one. I've taken dealt with the review comments from nightly#176, and merge that into this.

I think this is good to merge. If anyone is available to look at this?

[Kim Morrison]

(If you're happy, please just merge, rather than leaving me to do it, so I can to the subsequent bumps immediately when I start tomorrow.)

[Johan Commelin]

@Kim Morrison do you have a minute to respond to the lia-vs-grind question?

[Matthew Ballard]

I stared for 15 minutes and don't understand the applications vs the examples vs the doc-string for univ_out_params

[Kim Morrison]

Johan Commelin said:

Kim Morrison do you have a minute to respond to the lia-vs-grind question?

I replied on the comment, but this was that lia was accidentally over-powered, and using using non-lia features of grind. This was fixed in lean#11744, and these changes are just "being honest about what we're using".

[Kim Morrison]

Matthew Ballard said:

I stared for 15 minutes and don't understand the applications vs the examples vs the doc-string for univ_out_params

I'm not sure if you saw lean#12487 or not, which was a subsequent update to the doc-string. If that's still not helpful, let me know and we'll try again.