mathlib3

33179f7e - refactor(topology/metric_space/completion): change namespace (#12077)

refactor(topology/metric_space/completion): change namespace (#12077) Move lemmas about metric on `uniform_space.completion` from `metric.completion` namespace to `uniform_space.completion`.