nightly#102 adaptations for nightly-2025-10-29

Stream: nightly-testing

[github mathlib4 bot]

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

[Kevin Buzzard]

Wooah this is a monster. Can we deal with https://github.com/leanprover-community/mathlib4-nightly-testing/pull/99 first, and then 100, and then this one?

[Kim Morrison]

Oh dear, I hadn't realised they had been stacking up.

[Kim Morrison]

Okay, merged nightly#99.

[Kim Morrison]

and nightly#100 is sent to bors, after which I will merge bump/v4.26.0 back into this PR, and it will hopefully be easier to review.

[Kim Morrison]

Thanks Kevin for the help reviewing these!!

[Kim Morrison]

Hmm, after merging the earlier ones, nightly#102 is still huge. Mostly it is just updating deprecations using the fix_deprecations.sh script from #30994.

[Kevin Buzzard]

Kim Morrison said:

Thanks Kevin for the help reviewing these!!

I find that reviewing them makes it easier to bump FLT because many of the issues which arise in an FLT bump have already been exposed by the recent mathlib bump.

[Kevin Buzzard]

OK this one is reviewed. I tidied parts of it up, well, I thought it was tidying up, I'll let someone else decide if these changes from (iff_lemma).mp to (one_way_lemma) are a step forward. There's a merge conflict because Yael pushed a nice golf in Data.Finset.Image which renders your change from Subtype.eq to Subtype.ext moot.