feat(data/rat): add `@[simp]` to `rat.num_div_denom` (#7393)
I have an equation in rational numbers that I want to turn into an equation in integers, and everything `simp`s away nicely except the equation `x.num / x.denom = x`. Marking `rat.num_div_denom` as `simp` should fix that, and I don't expect it will break anything. (`rat.num_denom : rat.mk x.num x.denom = x` is already a `simp` lemma.)
Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60x.2Enum.20.2F.20x.2Edenom.20.3D.20x.60
