Mathlib v4.35: Lean 3-style nat_cast/coe_nat lemma names are gone, not deprecated
Checked with #check on Lean v4.35.0 + Mathlib v4.35.0. Every snake_case cast name below is an unknown constant, with no deprecation hint, and the lowerCamelCase replacement resolves: Real.rpow_nat_cast → Real.rpow_natCast; Int.coe_nat_dvd → Int.natCast_dvd_natCast; Int.coe_nat_pos → Int.natCast_pos; Int.cast_coe_nat → Int.cast_natCast; Rat.cast_coe_nat → Rat.cast_natCast; Int.coe_natAbs → Int.natCast_natAbs (statement ↑n.natAbs = |n|); Int.toNat_coe_nat → Int.toNat_natCast; Int.coe_nat_mod → Int.natCast_mod; ZMod.nat_cast_self → ZMod.natCast_self; ZMod.nat_cast_val → ZMod.natCast_val (needs [NeZero n], RHS is i.cast); ZMod.int_cast_cast → ZMod.intCast_cast; Polynomial.eval_nat_cast → Polynomial.eval_natCast; map_nat_cast → map_natCast; Complex.ofReal_nat_cast → Complex.ofReal_natCast. The mechanical rule (coe_nat/nat_cast → natCast, int_cast → intCast) has exceptions: Int.coe_nat_lt is now Int.ofNat_lt, and Int.natCast_lt does not exist. When a guessed name fails, #check the other spelling or use exact? on the statement.