fix(topology/uniform_space): simplify continuity proof (#1396)

src/topology/uniform_space/basic.lean

@@ -445,21 +445,6 @@ lemma uniform_continuous_const [uniform_space β] {b : β} : uniform_continuous
 lemma uniform_continuous.comp [uniform_space β] [uniform_space γ] {f : α → β} {g : β → γ}
   (hg : uniform_continuous g) (hf : uniform_continuous f) : uniform_continuous (g ∘ f) :=
 hg.comp hf
-
-lemma uniform_continuous.continuous [uniform_space β] {f : α → β}
-  (hf : uniform_continuous f) : continuous f :=
-continuous_iff_continuous_at.mpr $ assume a,
-calc map f (nhds a) ≤
-    (map (λp:α×α, (f p.1, f p.2)) (𝓤 α)).lift' (λs:set (β×β), {y | (f a, y) ∈ s}) :
-  begin
-    rw [nhds_eq_uniformity, map_lift'_eq, map_lift'_eq2],
-    exact (lift'_mono' $ assume s hs b ⟨a', (ha' : (_, a') ∈ s), a'_eq⟩,
-      ⟨(a, a'), ha', show (f a, f a') = (f a, b), from a'_eq ▸ rfl⟩),
-    exact monotone_preimage,
-    exact monotone_preimage
-  end
-  ... ≤ nhds (f a) :
-    by rw [nhds_eq_uniformity]; exact lift'_mono hf (le_refl _)
 end uniform_space
 end
 
@@ -578,7 +563,7 @@ lemma uniform_space.comap_comap_comp {α β γ} [uγ : uniform_space γ] {f : α
   uniform_space.comap (g ∘ f) uγ = uniform_space.comap f (uniform_space.comap g uγ) :=
 by ext ; dsimp [uniform_space.comap] ; rw filter.comap_comap_comp
 
-lemma uniform_continuous_iff {α β} [uα : uniform_space α] [uβ : uniform_space β] (f : α → β) :
+lemma uniform_continuous_iff {α β} [uα : uniform_space α] [uβ : uniform_space β] {f : α → β} :
   uniform_continuous f ↔ uα ≤ uβ.comap f :=
 filter.map_le_iff_le_comap
 
@@ -599,6 +584,10 @@ lemma to_topological_space_mono {u₁ u₂ : uniform_space α} (h : u₁ ≤ u
 le_of_nhds_le_nhds $ assume a,
   by rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]; exact (lift'_mono h $ le_refl _)
 
+lemma uniform_continuous.continuous [uniform_space α] [uniform_space β] {f : α → β}
+  (hf : uniform_continuous f) : continuous f :=
+continuous_iff_le_induced.mpr $ to_topological_space_mono $ uniform_continuous_iff.1 hf
+
 lemma to_topological_space_bot : @uniform_space.to_topological_space α ⊥ = ⊥ := rfl
 
 lemma to_topological_space_top : @uniform_space.to_topological_space α ⊤ = ⊤ :=