…tCast`

Reduce the diff of #11499

…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

…tCast` (#11552)

Reduce the diff of #11499

Reduce the diff of #11499

## Renames

All in the `Int` namespace:
* `ofNat_eq_cast` → `ofNat_eq_natCast`
* `cast_eq_cast_iff_Nat` → `natCast_inj`
* `natCast_eq_ofNat` → `ofNat_eq_natCast`
* `coe_nat_sub` → `natCast_sub`
* `coe_nat_nonneg` → `natCast_nonneg`
* `sign_coe_add_one` → `sign_natCast_add_one`
* `nat_succ_eq_int_succ` → `natCast_succ`
* `succ_neg_nat_succ` → `succ_neg_natCast_succ`
* `coe_pred_of_pos` → `natCast_pred_of_pos`
* `coe_nat_div` → `natCast_div`
* `coe_nat_ediv` → `natCast_ediv`
* `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero`
* `toNat_coe_nat` → `toNat_natCast`
* `toNat_coe_nat_add_one` → `toNat_natCast_add_one`
* `coe_nat_dvd` → `natCast_dvd_natCast`
* `coe_nat_dvd_left` → `natCast_dvd`
* `coe_nat_dvd_right` → `dvd_natCast`
* `le_coe_nat_sub` → `le_natCast_sub`
* `succ_coe_nat_pos` → `succ_natCast_pos`
* `coe_nat_modEq_iff` → `natCast_modEq_iff`
* `coe_natAbs` → `natCast_natAbs`
* `coe_nat_eq_zero` → `natCast_eq_zero`
* `coe_nat_ne_zero` → `natCast_ne_zero`
* `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos`
* `abs_coe_nat` → `abs_natCast`
* `coe_nat_nonpos_iff` → `natCast_nonpos_iff`

Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

…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

…tCast` (#11552)

Reduce the diff of #11499

Reduce the diff of #11499

## Renames

All in the `Int` namespace:
* `ofNat_eq_cast` → `ofNat_eq_natCast`
* `cast_eq_cast_iff_Nat` → `natCast_inj`
* `natCast_eq_ofNat` → `ofNat_eq_natCast`
* `coe_nat_sub` → `natCast_sub`
* `coe_nat_nonneg` → `natCast_nonneg`
* `sign_coe_add_one` → `sign_natCast_add_one`
* `nat_succ_eq_int_succ` → `natCast_succ`
* `succ_neg_nat_succ` → `succ_neg_natCast_succ`
* `coe_pred_of_pos` → `natCast_pred_of_pos`
* `coe_nat_div` → `natCast_div`
* `coe_nat_ediv` → `natCast_ediv`
* `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero`
* `toNat_coe_nat` → `toNat_natCast`
* `toNat_coe_nat_add_one` → `toNat_natCast_add_one`
* `coe_nat_dvd` → `natCast_dvd_natCast`
* `coe_nat_dvd_left` → `natCast_dvd`
* `coe_nat_dvd_right` → `dvd_natCast`
* `le_coe_nat_sub` → `le_natCast_sub`
* `succ_coe_nat_pos` → `succ_natCast_pos`
* `coe_nat_modEq_iff` → `natCast_modEq_iff`
* `coe_natAbs` → `natCast_natAbs`
* `coe_nat_eq_zero` → `natCast_eq_zero`
* `coe_nat_ne_zero` → `natCast_ne_zero`
* `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos`
* `abs_coe_nat` → `abs_natCast`
* `coe_nat_nonpos_iff` → `natCast_nonpos_iff`

Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

…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

…tCast` (#11552)

Reduce the diff of #11499

Reduce the diff of #11499

## Renames

All in the `Int` namespace:
* `ofNat_eq_cast` → `ofNat_eq_natCast`
* `cast_eq_cast_iff_Nat` → `natCast_inj`
* `natCast_eq_ofNat` → `ofNat_eq_natCast`
* `coe_nat_sub` → `natCast_sub`
* `coe_nat_nonneg` → `natCast_nonneg`
* `sign_coe_add_one` → `sign_natCast_add_one`
* `nat_succ_eq_int_succ` → `natCast_succ`
* `succ_neg_nat_succ` → `succ_neg_natCast_succ`
* `coe_pred_of_pos` → `natCast_pred_of_pos`
* `coe_nat_div` → `natCast_div`
* `coe_nat_ediv` → `natCast_ediv`
* `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero`
* `toNat_coe_nat` → `toNat_natCast`
* `toNat_coe_nat_add_one` → `toNat_natCast_add_one`
* `coe_nat_dvd` → `natCast_dvd_natCast`
* `coe_nat_dvd_left` → `natCast_dvd`
* `coe_nat_dvd_right` → `dvd_natCast`
* `le_coe_nat_sub` → `le_natCast_sub`
* `succ_coe_nat_pos` → `succ_natCast_pos`
* `coe_nat_modEq_iff` → `natCast_modEq_iff`
* `coe_natAbs` → `natCast_natAbs`
* `coe_nat_eq_zero` → `natCast_eq_zero`
* `coe_nat_ne_zero` → `natCast_ne_zero`
* `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos`
* `abs_coe_nat` → `abs_natCast`
* `coe_nat_nonpos_iff` → `natCast_nonpos_iff`

Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

…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

…tCast` (#11552)

Reduce the diff of #11499

Reduce the diff of #11499

## Renames

All in the `Int` namespace:
* `ofNat_eq_cast` → `ofNat_eq_natCast`
* `cast_eq_cast_iff_Nat` → `natCast_inj`
* `natCast_eq_ofNat` → `ofNat_eq_natCast`
* `coe_nat_sub` → `natCast_sub`
* `coe_nat_nonneg` → `natCast_nonneg`
* `sign_coe_add_one` → `sign_natCast_add_one`
* `nat_succ_eq_int_succ` → `natCast_succ`
* `succ_neg_nat_succ` → `succ_neg_natCast_succ`
* `coe_pred_of_pos` → `natCast_pred_of_pos`
* `coe_nat_div` → `natCast_div`
* `coe_nat_ediv` → `natCast_ediv`
* `sign_coe_nat_of_nonzero` → `sign_natCast_of_ne_zero`
* `toNat_coe_nat` → `toNat_natCast`
* `toNat_coe_nat_add_one` → `toNat_natCast_add_one`
* `coe_nat_dvd` → `natCast_dvd_natCast`
* `coe_nat_dvd_left` → `natCast_dvd`
* `coe_nat_dvd_right` → `dvd_natCast`
* `le_coe_nat_sub` → `le_natCast_sub`
* `succ_coe_nat_pos` → `succ_natCast_pos`
* `coe_nat_modEq_iff` → `natCast_modEq_iff`
* `coe_natAbs` → `natCast_natAbs`
* `coe_nat_eq_zero` → `natCast_eq_zero`
* `coe_nat_ne_zero` → `natCast_ne_zero`
* `coe_nat_ne_zero_iff_pos` → `natCast_ne_zero_iff_pos`
* `abs_coe_nat` → `abs_natCast`
* `coe_nat_nonpos_iff` → `natCast_nonpos_iff`

Also rename `Nat.coe_nat_dvd` to `Nat.cast_dvd_cast`

…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