…atCast` (#11499)

This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy.

Reduce the diff of #11203

…atCast` (#11499)

This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy.

Reduce the diff of #11203

…/`ratCast` (#11486)

Now that I am defining `NNRat.cast`, I want a definitive answer to this naming issue. Plenty of lemmas in mathlib already use `natCast`/`intCast`/`ratCast` over `nat_cast`/`int_cast`/`rat_cast`, and this matches with the general expectation that underscore-separated name parts correspond to a single declaration.

…atCast` (#11499)

This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy.

Reduce the diff of #11203

…/`ratCast` (#11486)

Now that I am defining `NNRat.cast`, I want a definitive answer to this naming issue. Plenty of lemmas in mathlib already use `natCast`/`intCast`/`ratCast` over `nat_cast`/`int_cast`/`rat_cast`, and this matches with the general expectation that underscore-separated name parts correspond to a single declaration.

…atCast` (#11499)

This is less exhaustive than its sibling #11486 because edge cases are harder to classify. No fundamental difficulty, just me being a bit fast and lazy.

Reduce the diff of #11203

…/`ratCast` (#11486)

Now that I am defining `NNRat.cast`, I want a definitive answer to this naming issue. Plenty of lemmas in mathlib already use `natCast`/`intCast`/`ratCast` over `nat_cast`/`int_cast`/`rat_cast`, and this matches with the general expectation that underscore-separated name parts correspond to a single declaration.

Explain the naming convention pushed for by leanprover-community/mathlib4#11486.

…/`ratCast` (#11486)

Now that I am defining `NNRat.cast`, I want a definitive answer to this naming issue. Plenty of lemmas in mathlib already use `natCast`/`intCast`/`ratCast` over `nat_cast`/`int_cast`/`rat_cast`, and this matches with the general expectation that underscore-separated name parts correspond to a single declaration.

…3368)

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 #10185 (comment) 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.

…3368)

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 #10185 (comment) 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.