fix(topology/metric_space): fix uniform structure on Pi types

[sgouezel]

The uniform structure induced from a metric space structure on a Pi type is currently not defeq to the product uniform structure. This is fixed in this PR. Before the PR,

lemma diamond {n : ℕ} : is_open (pi (univ : set (fin n)) (λi, (univ : set ℝ))) :=
begin
  have A : finite (univ : set (fin n)) := finite_univ,
  have B : ∀i : fin n, i ∈ univ → is_open (univ : set ℝ) := λi hi, is_open_univ,
  convert is_open_set_pi A B,
end

leaves the goal uniform_space.to_topological_space (fin n → ℝ) = Pi.topological_space. After the PR, there is no goal left.