mathlib

970b17bf - refactor(topology/metric_space): move lemmas about `paracompact_space` and the shrinking lemma to separate files (#8404)

refactor(topology/metric_space): move lemmas about `paracompact_space` and the shrinking lemma to separate files (#8404) Only a few files in `mathlib` actually depend on results about `paracompact_space`. With this refactor, only a few files depend on `topology/paracompact_space` and `topology/shrinking_lemma`. The main side effects are that `paracompact_of_emetric` and `normal_of_emetric` instances are not available without importing `topology.metric_space.emetric_paracompact` and the shrinking lemma for balls in a proper metric space is not available without `import topology.metric_space.shrinking_lemma`.