Commit 2024-05-30 11:57 a5844cab
View on Github →chore: add deprecation dates for nat_cast
and int_cast
lemmas (#13368)
Deprecations have been forgotten in #11486. We add them in this PR.
Methodology: start from the last commit of #11486, use the script by @adomani in https://github.com/leanprover-community/mathlib4/pull/10185#issuecomment-1925481325 to generate deprecation aliases (I am also adding an updated version of the script in a comment below) and commit. Then cherry pick this last commit on master and fix whatever has changed in between. This is not perfect as declarations which have been moved since #11486 won't get their deprecated alias, but this should be good enough.