mathlib3

aeb7facf - feat(data/rat/cast): add lemmas, golf (#16194)

feat(data/rat/cast): add lemmas, golf (#16194) * add `rat.cast_strict_mono`, `rat.cast_strict_mono`, and `rat.cast_order_embedding`; * use these lemmas to prove `rat.cast_le` etc; * add `rat.preimage_cast_Ixx`.