How to find alternatives to deleted theorems?

Stream: mathlib4

[Matvey Lorkish]

Hello! Currently, I am updating a project from v4.7.0 to v4.21.0. In between versions, a lot of theorems and packages have been marked as deprecated or have been deleted entirely. I was looking through documentations and the changelog tool, yet I cannot find the package or theorem the deleted functionality was transferred to. Can someone tell me please how to find the corresponding theorems/packages?

[Weiyi Wang]

I wonder if it would be easier if you do this in multiple steps, like 4.7→4.11→4.16→4.21

[Matvey Lorkish]

that would be actually a good idea probably I will try it out

[Michael Rothgang]

To elaborate: whenever a theorem is renamed, a deprecated alias is put in place: this will warn you whenever you try to use the old theorem, and tell you about a replacement.

[Michael Rothgang]

These are removed after six months, i.e. roughly six Lean versions. So if you update in smaller steps, you can use those warnings to help you!

[Ruben Van de Velde]

Anything that's deprecated should have a pointer to what you should use instead

[Kim Morrison]

It's also often less confusing if you upgrade in smaller steps, and easier to for someone else to review. I've previously used a script that takes care of writing the commit messages and bumping the toolchain/dependencies by one every time I say "next"...