toolchain upgrade problems

Stream: mathlib4

[Dominic Steinitz]

Invalid field toPartialHomeomorph: The environment does not contain Trivialization.toPartialHomeomorph

leanprover/lean4:v4.27.0-rc1

but this worked in

leanprover/lean4:v4.24.0-rc1

Is there something which documents the changes and what to do about them? I would have expected a deprecation given I had no warning.

[Dominic Steinitz]

I am looking here at the moment: https://lean-lang.org/doc/reference/latest/releases/

[Dominic Steinitz]

I found nothing about trivialisations :-(

[Dominic Steinitz]

My guess of toOpenPartialHomeomorph seems to have worked

[Snir Broshi]

Zulip thread #mathlib4 > Generalizing `PartialHomeomorph`? @ 💬
PR #29113
They added a deprecation for PartialHomeomorph, but not for the casts for structs that extend it