mathlib3

620af85a - refactor(topology/instances): put `ℕ`, `ℤ`, and `ℚ` in separate files (#12207)

refactor(topology/instances): put `ℕ`, `ℤ`, and `ℚ` in separate files (#12207) The goal here is to make `metric_space ℕ` and `metric_space ℤ` available earlier, so that I can state `has_bounded_smul ℕ A` somewhere reasonable. No lemmas have been added, deleted, or changed here - they've just been moved out of `topology/instances/real` and into `topology/instances/{nat,int,rat,real}`. The resulting import structure is: * `rat_lemmas` → `rat` * `rat` → {`real`, `int`, `nat`} * `real` → {`int`} * `nat` → {`int`}