Find the new name for a renamed Mathlib lemma

Type the old name, or paste the unknown identifier line from your build. You get the replacement, the module, and the release where Mathlib removed the alias.

Old Mathlib name, or the whole unknown identifier line

Find the replacement

Try one

• mul_right_eq_self
• Inducing.specializes_iff
• List.last_ofFn_succ
• embedding_inclusion
• pow_bit0_pos

The map holds 17,917 deprecated Mathlib names across v4.0.0 to v4.35.0 (Mathlib commit 56a005855e). On the 145 raw build errors in the 7 pilot projects, the alias map alone resolved 0: most breakage after a bump is a changed signature or a reproof, which is why the benchmark lists the repairs.

Have a whole project? Scan it by GitHub address and see every line a bump breaks.