mathlib

905beb08 - fix(topology/metric_space): fix uniform structure on Pi types (#1551)

fix(topology/metric_space): fix uniform structure on Pi types (#1551) * fix(topology/metric_space): fix uniform structure on pi tpype * cleanup * better construction of metric from emetric * use simp only instead of simp