diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index 2a5d7d6f79ec3..07e483a9787ce 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -9,6 +9,7 @@ import analysis.normed.group.infinite_sum
 import data.matrix.basic
 import topology.algebra.module.basic
 import topology.instances.ennreal
+import topology.instances.rat
 import topology.sequences
 
 /-!
diff --git a/src/topology/instances/int.lean b/src/topology/instances/int.lean
new file mode 100644
index 0000000000000..94ebb57746533
--- /dev/null
+++ b/src/topology/instances/int.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import topology.metric_space.basic
+import order.filter.archimedean
+/-!
+# Topology on the integers
+
+The structure of a metric space on `ℤ` is introduced in this file, induced from `ℝ`.
+-/
+noncomputable theory
+open metric set filter
+
+namespace int
+
+instance : has_dist ℤ := ⟨λ x y, dist (x : ℝ) y⟩
+
+theorem dist_eq (x y : ℤ) : dist x y = |x - y| := rfl
+
+@[norm_cast, simp] theorem dist_cast_real (x y : ℤ) : dist (x : ℝ) y = dist x y := rfl
+
+lemma pairwise_one_le_dist : pairwise (λ m n : ℤ, 1 ≤ dist m n) :=
+begin
+  intros m n hne,
+  rw dist_eq, norm_cast, rwa [← zero_add (1 : ℤ), int.add_one_le_iff, abs_pos, sub_ne_zero]
+end
+
+lemma uniform_embedding_coe_real : uniform_embedding (coe : ℤ → ℝ) :=
+uniform_embedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
+
+lemma closed_embedding_coe_real : closed_embedding (coe : ℤ → ℝ) :=
+closed_embedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
+
+instance : metric_space ℤ := int.uniform_embedding_coe_real.comap_metric_space _
+
+theorem preimage_ball (x : ℤ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl
+
+theorem preimage_closed_ball (x : ℤ) (r : ℝ) :
+  coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl
+
+theorem ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ :=
+by rw [← preimage_ball, real.ball_eq_Ioo, preimage_Ioo]
+
+theorem closed_ball_eq_Icc (x : ℤ) (r : ℝ) : closed_ball x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ :=
+by rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc]
+
+instance : proper_space ℤ :=
+⟨ begin
+    intros x r,
+    rw closed_ball_eq_Icc,
+    exact (set.finite_Icc _ _).is_compact,
+  end ⟩
+
+@[simp] lemma cocompact_eq : cocompact ℤ = at_bot ⊔ at_top :=
+by simp only [← comap_dist_right_at_top_eq_cocompact (0 : ℤ), dist_eq, sub_zero, cast_zero,
+  ← cast_abs, ← @comap_comap _ _ _ _ abs, int.comap_coe_at_top, comap_abs_at_top]
+
+@[simp] lemma cofinite_eq : (cofinite : filter ℤ) = at_bot ⊔ at_top :=
+by rw [← cocompact_eq_cofinite, cocompact_eq]
+
+end int
diff --git a/src/topology/instances/nat.lean b/src/topology/instances/nat.lean
new file mode 100644
index 0000000000000..499dd3a9ccaad
--- /dev/null
+++ b/src/topology/instances/nat.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import topology.instances.int
+/-!
+# Topology on the natural numbers
+
+The structure of a metric space on `ℕ` is introduced in this file, induced from `ℝ`.
+-/
+noncomputable theory
+open metric set filter
+
+namespace nat
+
+noncomputable instance : has_dist ℕ := ⟨λ x y, dist (x : ℝ) y⟩
+
+theorem dist_eq (x y : ℕ) : dist x y = |x - y| := rfl
+
+lemma dist_coe_int (x y : ℕ) : dist (x : ℤ) (y : ℤ) = dist x y := rfl
+
+@[norm_cast, simp] theorem dist_cast_real (x y : ℕ) : dist (x : ℝ) y = dist x y := rfl
+
+lemma pairwise_one_le_dist : pairwise (λ m n : ℕ, 1 ≤ dist m n) :=
+begin
+  intros m n hne,
+  rw ← dist_coe_int,
+  apply int.pairwise_one_le_dist,
+  exact_mod_cast hne
+end
+
+lemma uniform_embedding_coe_real : uniform_embedding (coe : ℕ → ℝ) :=
+uniform_embedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
+
+lemma closed_embedding_coe_real : closed_embedding (coe : ℕ → ℝ) :=
+closed_embedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
+
+instance : metric_space ℕ := nat.uniform_embedding_coe_real.comap_metric_space _
+
+theorem preimage_ball (x : ℕ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl
+
+theorem preimage_closed_ball (x : ℕ) (r : ℝ) :
+  coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl
+
+theorem closed_ball_eq_Icc (x : ℕ) (r : ℝ) :
+  closed_ball x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊ :=
+begin
+  rcases le_or_lt 0 r with hr|hr,
+  { rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc],
+    exact add_nonneg (cast_nonneg x) hr },
+  { rw closed_ball_eq_empty.2 hr,
+    apply (Icc_eq_empty _).symm,
+    rw not_le,
+    calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ : by { apply floor_mono, linarith }
+    ... < ⌈↑x - r⌉₊ : by { rw [floor_coe, nat.lt_ceil], linarith } }
+end
+
+instance : proper_space ℕ :=
+⟨ begin
+    intros x r,
+    rw closed_ball_eq_Icc,
+    exact (set.finite_Icc _ _).is_compact,
+  end ⟩
+
+instance : noncompact_space ℕ :=
+noncompact_space_of_ne_bot $ by simp [filter.at_top_ne_bot]
+
+end nat
diff --git a/src/topology/instances/rat.lean b/src/topology/instances/rat.lean
new file mode 100644
index 0000000000000..eec32ff7596fa
--- /dev/null
+++ b/src/topology/instances/rat.lean
@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import topology.metric_space.basic
+import topology.instances.int
+import topology.instances.nat
+import topology.instances.real
+/-!
+# Topology on the ratonal numbers
+
+The structure of a metric space on `ℚ` is introduced in this file, induced from `ℝ`.
+-/
+noncomputable theory
+open metric set filter
+
+namespace rat
+
+instance : metric_space ℚ :=
+metric_space.induced coe rat.cast_injective real.metric_space
+
+theorem dist_eq (x y : ℚ) : dist x y = |x - y| := rfl
+
+@[norm_cast, simp] lemma dist_cast (x y : ℚ) : dist (x : ℝ) y = dist x y := rfl
+
+theorem uniform_continuous_coe_real : uniform_continuous (coe : ℚ → ℝ) :=
+uniform_continuous_comap
+
+theorem uniform_embedding_coe_real : uniform_embedding (coe : ℚ → ℝ) :=
+uniform_embedding_comap rat.cast_injective
+
+theorem dense_embedding_coe_real : dense_embedding (coe : ℚ → ℝ) :=
+uniform_embedding_coe_real.dense_embedding $
+λ x, mem_closure_iff_nhds.2 $ λ t ht,
+let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in
+let ⟨q, h⟩ := exists_rat_near x ε0 in
+⟨_, hε (mem_ball'.2 h), q, rfl⟩
+
+theorem embedding_coe_real : embedding (coe : ℚ → ℝ) := dense_embedding_coe_real.to_embedding
+
+theorem continuous_coe_real : continuous (coe : ℚ → ℝ) := uniform_continuous_coe_real.continuous
+
+end rat
+
+@[norm_cast, simp] theorem nat.dist_cast_rat (x y : ℕ) : dist (x : ℚ) y = dist x y :=
+by rw [← nat.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast
+
+lemma nat.uniform_embedding_coe_rat : uniform_embedding (coe : ℕ → ℚ) :=
+uniform_embedding_bot_of_pairwise_le_dist zero_lt_one $ by simpa using nat.pairwise_one_le_dist
+
+lemma nat.closed_embedding_coe_rat : closed_embedding (coe : ℕ → ℚ) :=
+closed_embedding_of_pairwise_le_dist zero_lt_one $ by simpa using nat.pairwise_one_le_dist
+
+@[norm_cast, simp] theorem int.dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y :=
+by rw [← int.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast
+
+lemma int.uniform_embedding_coe_rat : uniform_embedding (coe : ℤ → ℚ) :=
+uniform_embedding_bot_of_pairwise_le_dist zero_lt_one $ by simpa using int.pairwise_one_le_dist
+
+lemma int.closed_embedding_coe_rat : closed_embedding (coe : ℤ → ℚ) :=
+closed_embedding_of_pairwise_le_dist zero_lt_one $ by simpa using int.pairwise_one_le_dist
+
+instance : noncompact_space ℚ := int.closed_embedding_coe_rat.noncompact_space
+
+-- TODO(Mario): Find a way to use rat_add_continuous_lemma
+theorem rat.uniform_continuous_add : uniform_continuous (λp : ℚ × ℚ, p.1 + p.2) :=
+rat.uniform_embedding_coe_real.to_uniform_inducing.uniform_continuous_iff.2 $
+  by simp only [(∘), rat.cast_add]; exact real.uniform_continuous_add.comp
+    (rat.uniform_continuous_coe_real.prod_map rat.uniform_continuous_coe_real)
+
+theorem rat.uniform_continuous_neg : uniform_continuous (@has_neg.neg ℚ _) :=
+metric.uniform_continuous_iff.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
+  by rw dist_comm at h; simpa [rat.dist_eq] using h⟩
+
+instance : uniform_add_group ℚ :=
+uniform_add_group.mk' rat.uniform_continuous_add rat.uniform_continuous_neg
+
+instance : topological_add_group ℚ := by apply_instance
+
+instance : order_topology ℚ :=
+induced_order_topology _ (λ x y, rat.cast_lt) (@exists_rat_btwn _ _ _)
+
+lemma rat.uniform_continuous_abs : uniform_continuous (abs : ℚ → ℚ) :=
+metric.uniform_continuous_iff.2 $ λ ε ε0,
+  ⟨ε, ε0, λ a b h, lt_of_le_of_lt
+    (by simpa [rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩
+
+lemma rat.continuous_mul : continuous (λp : ℚ × ℚ, p.1 * p.2) :=
+rat.embedding_coe_real.continuous_iff.2 $ by simp [(∘)]; exact
+real.continuous_mul.comp ((rat.continuous_coe_real.prod_map rat.continuous_coe_real))
+
+instance : topological_ring ℚ :=
+{ continuous_mul := rat.continuous_mul, ..rat.topological_add_group }
+
+lemma rat.totally_bounded_Icc (a b : ℚ) : totally_bounded (Icc a b) :=
+begin
+  have := totally_bounded_preimage rat.uniform_embedding_coe_real (totally_bounded_Icc a b),
+  rwa (set.ext (λ q, _) : Icc _ _ = _), simp
+end
diff --git a/src/topology/instances/real.lean b/src/topology/instances/real.lean
index 4bfb9e5c67236..2756c58503f1d 100644
--- a/src/topology/instances/real.lean
+++ b/src/topology/instances/real.lean
@@ -10,6 +10,7 @@ import ring_theory.subring.basic
 import group_theory.archimedean
 import algebra.periodic
 import order.filter.archimedean
+import topology.instances.int
 
 /-!
 # Topological properties of ℝ
@@ -22,159 +23,6 @@ open_locale classical topological_space filter uniformity interval
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-instance : metric_space ℚ :=
-metric_space.induced coe rat.cast_injective real.metric_space
-
-namespace rat
-
-theorem dist_eq (x y : ℚ) : dist x y = |x - y| := rfl
-
-@[norm_cast, simp] lemma dist_cast (x y : ℚ) : dist (x : ℝ) y = dist x y := rfl
-
-theorem uniform_continuous_coe_real : uniform_continuous (coe : ℚ → ℝ) :=
-uniform_continuous_comap
-
-theorem uniform_embedding_coe_real : uniform_embedding (coe : ℚ → ℝ) :=
-uniform_embedding_comap rat.cast_injective
-
-theorem dense_embedding_coe_real : dense_embedding (coe : ℚ → ℝ) :=
-uniform_embedding_coe_real.dense_embedding $
-λ x, mem_closure_iff_nhds.2 $ λ t ht,
-let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in
-let ⟨q, h⟩ := exists_rat_near x ε0 in
-⟨_, hε (mem_ball'.2 h), q, rfl⟩
-
-theorem embedding_coe_real : embedding (coe : ℚ → ℝ) := dense_embedding_coe_real.to_embedding
-
-theorem continuous_coe_real : continuous (coe : ℚ → ℝ) := uniform_continuous_coe_real.continuous
-
-end rat
-
-namespace int
-
-instance : has_dist ℤ := ⟨λ x y, dist (x : ℝ) y⟩
-
-theorem dist_eq (x y : ℤ) : dist x y = |x - y| := rfl
-
-@[norm_cast, simp] theorem dist_cast_real (x y : ℤ) : dist (x : ℝ) y = dist x y := rfl
-
-@[norm_cast, simp] theorem dist_cast_rat (x y : ℤ) : dist (x : ℚ) y = dist x y :=
-by rw [← int.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast
-
-lemma pairwise_one_le_dist : pairwise (λ m n : ℤ, 1 ≤ dist m n) :=
-begin
-  intros m n hne,
-  rw dist_eq, norm_cast, rwa [← zero_add (1 : ℤ), int.add_one_le_iff, abs_pos, sub_ne_zero]
-end
-
-lemma uniform_embedding_coe_rat : uniform_embedding (coe : ℤ → ℚ) :=
-uniform_embedding_bot_of_pairwise_le_dist zero_lt_one $ by simpa using pairwise_one_le_dist
-
-lemma closed_embedding_coe_rat : closed_embedding (coe : ℤ → ℚ) :=
-closed_embedding_of_pairwise_le_dist zero_lt_one $ by simpa using pairwise_one_le_dist
-
-lemma uniform_embedding_coe_real : uniform_embedding (coe : ℤ → ℝ) :=
-uniform_embedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
-
-lemma closed_embedding_coe_real : closed_embedding (coe : ℤ → ℝ) :=
-closed_embedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
-
-instance : metric_space ℤ := int.uniform_embedding_coe_real.comap_metric_space _
-
-theorem preimage_ball (x : ℤ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl
-
-theorem preimage_closed_ball (x : ℤ) (r : ℝ) :
-  coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl
-
-theorem ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉ :=
-by rw [← preimage_ball, real.ball_eq_Ioo, preimage_Ioo]
-
-theorem closed_ball_eq_Icc (x : ℤ) (r : ℝ) : closed_ball x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋ :=
-by rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc]
-
-instance : proper_space ℤ :=
-⟨ begin
-    intros x r,
-    rw closed_ball_eq_Icc,
-    exact (set.finite_Icc _ _).is_compact,
-  end ⟩
-
-@[simp] lemma cocompact_eq : cocompact ℤ = at_bot ⊔ at_top :=
-by simp only [← comap_dist_right_at_top_eq_cocompact (0 : ℤ), dist_eq, sub_zero, cast_zero,
-  ← cast_abs, ← @comap_comap _ _ _ _ abs, int.comap_coe_at_top, comap_abs_at_top]
-
-@[simp] lemma cofinite_eq : (cofinite : filter ℤ) = at_bot ⊔ at_top :=
-by rw [← cocompact_eq_cofinite, cocompact_eq]
-
-end int
-
-
-namespace nat
-
-instance : has_dist ℕ := ⟨λ x y, dist (x : ℝ) y⟩
-
-theorem dist_eq (x y : ℕ) : dist x y = |x - y| := rfl
-
-lemma dist_coe_int (x y : ℕ) : dist (x : ℤ) (y : ℤ) = dist x y := rfl
-
-@[norm_cast, simp] theorem dist_cast_real (x y : ℕ) : dist (x : ℝ) y = dist x y := rfl
-
-@[norm_cast, simp] theorem dist_cast_rat (x y : ℕ) : dist (x : ℚ) y = dist x y :=
-by rw [← nat.dist_cast_real, ← rat.dist_cast]; congr' 1; norm_cast
-
-lemma pairwise_one_le_dist : pairwise (λ m n : ℕ, 1 ≤ dist m n) :=
-begin
-  intros m n hne,
-  rw ← dist_coe_int,
-  apply int.pairwise_one_le_dist,
-  exact_mod_cast hne
-end
-
-lemma uniform_embedding_coe_rat : uniform_embedding (coe : ℕ → ℚ) :=
-uniform_embedding_bot_of_pairwise_le_dist zero_lt_one $ by simpa using pairwise_one_le_dist
-
-lemma closed_embedding_coe_rat : closed_embedding (coe : ℕ → ℚ) :=
-closed_embedding_of_pairwise_le_dist zero_lt_one $ by simpa using pairwise_one_le_dist
-
-lemma uniform_embedding_coe_real : uniform_embedding (coe : ℕ → ℝ) :=
-uniform_embedding_bot_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
-
-lemma closed_embedding_coe_real : closed_embedding (coe : ℕ → ℝ) :=
-closed_embedding_of_pairwise_le_dist zero_lt_one pairwise_one_le_dist
-
-instance : metric_space ℕ := nat.uniform_embedding_coe_real.comap_metric_space _
-
-theorem preimage_ball (x : ℕ) (r : ℝ) : coe ⁻¹' (ball (x : ℝ) r) = ball x r := rfl
-
-theorem preimage_closed_ball (x : ℕ) (r : ℝ) :
-  coe ⁻¹' (closed_ball (x : ℝ) r) = closed_ball x r := rfl
-
-theorem closed_ball_eq_Icc (x : ℕ) (r : ℝ) :
-  closed_ball x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊ :=
-begin
-  rcases le_or_lt 0 r with hr|hr,
-  { rw [← preimage_closed_ball, real.closed_ball_eq_Icc, preimage_Icc],
-    exact add_nonneg (cast_nonneg x) hr },
-  { rw closed_ball_eq_empty.2 hr,
-    apply (Icc_eq_empty _).symm,
-    rw not_le,
-    calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ : by { apply floor_mono, linarith }
-    ... < ⌈↑x - r⌉₊ : by { rw [floor_coe, nat.lt_ceil], linarith } }
-end
-
-instance : proper_space ℕ :=
-⟨ begin
-    intros x r,
-    rw closed_ball_eq_Icc,
-    exact (set.finite_Icc _ _).is_compact,
-  end ⟩
-
-instance : noncompact_space ℕ :=
-noncompact_space_of_ne_bot $ by simp [at_top_ne_bot]
-
-end nat
-
-instance : noncompact_space ℚ := int.closed_embedding_coe_rat.noncompact_space
 instance : noncompact_space ℝ := int.closed_embedding_coe_real.noncompact_space
 
 theorem real.uniform_continuous_add : uniform_continuous (λp : ℝ × ℝ, p.1 + p.2) :=
@@ -182,32 +30,16 @@ metric.uniform_continuous_iff.2 $ λ ε ε0,
 let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abs ε0 in
 ⟨δ, δ0, λ a b h, let ⟨h₁, h₂⟩ := max_lt_iff.1 h in Hδ h₁ h₂⟩
 
--- TODO(Mario): Find a way to use rat_add_continuous_lemma
-theorem rat.uniform_continuous_add : uniform_continuous (λp : ℚ × ℚ, p.1 + p.2) :=
-rat.uniform_embedding_coe_real.to_uniform_inducing.uniform_continuous_iff.2 $
-  by simp only [(∘), rat.cast_add]; exact real.uniform_continuous_add.comp
-    (rat.uniform_continuous_coe_real.prod_map rat.uniform_continuous_coe_real)
 
 theorem real.uniform_continuous_neg : uniform_continuous (@has_neg.neg ℝ _) :=
 metric.uniform_continuous_iff.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
   by rw dist_comm at h; simpa [real.dist_eq] using h⟩
 
-theorem rat.uniform_continuous_neg : uniform_continuous (@has_neg.neg ℚ _) :=
-metric.uniform_continuous_iff.2 $ λ ε ε0, ⟨_, ε0, λ a b h,
-  by rw dist_comm at h; simpa [rat.dist_eq] using h⟩
-
 instance : uniform_add_group ℝ :=
 uniform_add_group.mk' real.uniform_continuous_add real.uniform_continuous_neg
 
-instance : uniform_add_group ℚ :=
-uniform_add_group.mk' rat.uniform_continuous_add rat.uniform_continuous_neg
-
  -- short-circuit type class inference
 instance : topological_add_group ℝ := by apply_instance
-instance : topological_add_group ℚ := by apply_instance
-
-instance : order_topology ℚ :=
-induced_order_topology _ (λ x y, rat.cast_lt) (@exists_rat_btwn _ _ _)
 
 instance : proper_space ℝ :=
 { is_compact_closed_ball := λx r, by { rw real.closed_ball_eq_Icc, apply is_compact_Icc } }
@@ -251,11 +83,6 @@ lemma real.uniform_continuous_abs : uniform_continuous (abs : ℝ → ℝ) :=
 metric.uniform_continuous_iff.2 $ λ ε ε0,
   ⟨ε, ε0, λ a b, lt_of_le_of_lt (abs_abs_sub_abs_le_abs_sub _ _)⟩
 
-lemma rat.uniform_continuous_abs : uniform_continuous (abs : ℚ → ℚ) :=
-metric.uniform_continuous_iff.2 $ λ ε ε0,
-  ⟨ε, ε0, λ a b h, lt_of_le_of_lt
-    (by simpa [rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩
-
 lemma real.tendsto_inv {r : ℝ} (r0 : r ≠ 0) : tendsto (λq, q⁻¹) (𝓝 r) (𝓝 r⁻¹) :=
 by rw ← abs_pos at r0; exact
 tendsto_of_uniform_continuous_subtype
@@ -302,13 +129,6 @@ tendsto_of_uniform_continuous_subtype
 instance : topological_ring ℝ :=
 { continuous_mul := real.continuous_mul, ..real.topological_add_group }
 
-lemma rat.continuous_mul : continuous (λp : ℚ × ℚ, p.1 * p.2) :=
-rat.embedding_coe_real.continuous_iff.2 $ by simp [(∘)]; exact
-real.continuous_mul.comp ((rat.continuous_coe_real.prod_map rat.continuous_coe_real))
-
-instance : topological_ring ℚ :=
-{ continuous_mul := rat.continuous_mul, ..rat.topological_add_group }
-
 instance : complete_space ℝ :=
 begin
   apply complete_of_cauchy_seq_tendsto,
@@ -324,12 +144,6 @@ end
 lemma real.totally_bounded_ball (x ε : ℝ) : totally_bounded (ball x ε) :=
 by rw real.ball_eq_Ioo; apply totally_bounded_Ioo
 
-lemma rat.totally_bounded_Icc (a b : ℚ) : totally_bounded (Icc a b) :=
-begin
-  have := totally_bounded_preimage rat.uniform_embedding_coe_real (totally_bounded_Icc a b),
-  rwa (set.ext (λ q, _) : Icc _ _ = _), simp
-end
-
 section
 
 lemma closure_of_rat_image_lt {q : ℚ} : closure ((coe:ℚ → ℝ) '' {x | q < x}) = {r | ↑q ≤ r} :=
diff --git a/src/topology/instances/real_vector_space.lean b/src/topology/instances/real_vector_space.lean
index 82fa5979dff9a..1787c9716d06c 100644
--- a/src/topology/instances/real_vector_space.lean
+++ b/src/topology/instances/real_vector_space.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import topology.algebra.module.basic
 import topology.instances.real
+import topology.instances.rat
 
 /-!
 # Continuous additive maps are `ℝ`-linear
diff --git a/src/topology/uniform_space/compare_reals.lean b/src/topology/uniform_space/compare_reals.lean
index 490e9e4b2412a..6570bd5fc763d 100644
--- a/src/topology/uniform_space/compare_reals.lean
+++ b/src/topology/uniform_space/compare_reals.lean
@@ -5,6 +5,7 @@ Authors: Patrick Massot
 -/
 import topology.uniform_space.absolute_value
 import topology.instances.real
+import topology.instances.rat
 import topology.uniform_space.completion
 
 /-!