mathlib3

68054185 - chore(data/rat,data/nat): modularize and reduce imports (#16810)

chore(data/rat,data/nat): modularize and reduce imports (#16810) While trying to understand the import tree leading to `data.rat.basic`, a small amount of modularization and import reduction. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>