nightly#103 adaptations for nightly-2025-11-02

Stream: nightly-testing

[Kim Morrison]

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

[Kevin Buzzard]

Hmm, the diff for this doesn't look right to me, nightly#102 is now merged and that was a huge PR, but I am still seeing many of the changes merged in that PR showing up as diffs in this one.

[Kim Morrison]

Sigh. I'm merging bump/v4.26.0 into nightly#103 now. The script should have done that, but perhaps nightly#102 hadn't quite landed yet.

[Kim Morrison]

Unfortunately your .mp changes are all causing merge conflicts, so I get to do them again. :-)

[Kim Morrison]

The diff now looks much saner.

[Kevin Buzzard]

I left some comments (I'm done reviewing)

[Kim Morrison]

Thanks very much for the sanity checks. (Various insanities were correctly noted, so I'll do another pass before merging...)

[Kim Morrison]

LGTM except for a bad merge in Mathlib/Algebra/Homology/Embedding/Connect.lean, which I'm just hand-testing after reverting.

[Kim Morrison]