feat(topology): shrinking lemma (#6478)
### Add a few versions of the shrinking lemma:
* `exists_subset_Union_closure_subset` and `exists_Union_eq_closure_subset`: shrinking lemma for general normal spaces;
* `exists_subset_Union_ball_radius_lt`, `exists_Union_ball_eq_radius_lt`, `exists_subset_Union_ball_radius_pos_lt`, `exists_Union_ball_eq_radius_pos_lt`: shrinking lemma for coverings by open balls in a proper metric space;
* `exists_locally_finite_subset_Union_ball_radius_lt`, `exists_locally_finite_Union_eq_ball_radius_lt`: given a positive function `R : X → ℝ`, finds a locally finite covering by open balls `ball (c i) (r' i)`, `r' i < R` and a subcovering by balls of strictly smaller radius `ball (c i) (r i)`, `0 < r i < r' i`.
### Other API changes
* add `@[simp]` to `set.compl_subset_compl`;
* add `is_closed_bInter` and `locally_finite.point_finite`;
* add `metric.closed_ball_subset_closed_ball`, `metric.uniformity_basis_dist_lt`, `exists_pos_lt_subset_ball`, and `exists_lt_subset_ball`;
* generalize `refinement_of_locally_compact_sigma_compact_of_nhds_basis` to `refinement_of_locally_compact_sigma_compact_of_nhds_basis_set`, replace arguments `(s : X → set X) (hs : ∀ x, s x ∈ 𝓝 x)` with a hint to use `filter.has_basis.restrict_subset` if needed.
* make `s` and `t` arguments of `normal_separation` implicit;
* add `normal_exists_closure_subset`;
* turn `sigma_compact_space_of_locally_compact_second_countable` into an `instance`.
