Data.Rat.Lemmas mathlib4#1138

Stream: mathlib4

[Ruben Van de Velde]

This builds now, but I had to go back and forth a few times with ofInt_eq_cast in some proofs. It feels like there's still room for improvement there, but I don't really know anything about coercions in lean4