mathlib3

b9e9328e - feat(topology/metric_space/completion): completion of metric spaces (#743)