mathlib3

dc2f6bb9 - chore(topology/metric_space): remove instances that duplicate lemmas (#14639)

chore(topology/metric_space): remove instances that duplicate lemmas (#14639) We can use the structure projections directly as instances, rather than duplicating them with primed names. This removes; * `metric_space.to_uniform_space'` (was misnamed, now `pseudo_metric_space.to_uniform_space`) * `pseudo_metric_space.to_bornology'` (now `pseudo_metric_space.to_bornology`) * `pseudo_emetric_space.to_uniform_space'` (now `pseudo_metric_space.to_uniform_space`) * `emetric_space.to_uniform_space'` (redundant) Follows up from review comments in #13927