[Merged by Bors] - feat: missing nnratCast lemmas for RCLike#39620

eric-wieser wants to merge 2 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

eric-wieser:ofReal_nnratCasteric-wieser/mathlib4:ofReal_nnratCastCopy head branch name to clipboard