fix(topology): simplify proof of Heine-Cantor (#3910)

src/order/complete_lattice.lean

@@ -310,6 +310,9 @@ theorem bsupr_le {p : ι → Prop} {f : Π i (h : p i), α} (h : ∀ i hi, f i h
   (⨆ i (hi : p i), f i hi) ≤ a :=
 supr_le $ λ i, supr_le $ h i
 
+theorem bsupr_le_supr (p : ι → Prop) (f : ι → α) : (⨆ i (H : p i), f i) ≤ ⨆ i, f i :=
+bsupr_le (λ i hi, le_supr f i)
+
 theorem supr_le_supr (h : ∀i, s i ≤ t i) : supr s ≤ supr t :=
 supr_le $ assume i, le_supr_of_le i (h i)
 
@@ -397,6 +400,9 @@ theorem le_binfi {p : ι → Prop} {f : Π i (h : p i), α} (h : ∀ i hi, a ≤
   a ≤ ⨅ i hi, f i hi :=
 le_infi $ λ i, le_infi $ h i
 
+theorem infi_le_binfi (p : ι → Prop) (f : ι → α) : (⨅ i, f i) ≤ ⨅ i (H : p i), f i :=
+le_binfi (λ i hi, infi_le f i)
+
 theorem infi_le_infi (h : ∀i, s i ≤ t i) : infi s ≤ infi t :=
 le_infi $ assume i, infi_le_of_le i (h i)
 

src/topology/uniform_space/compact_separated.lean

@@ -204,18 +204,12 @@ def uniform_space_of_compact_t2 {α : Type*} [topological_space α] [compact_spa
 continuous. -/
 lemma compact_space.uniform_continuous_of_continuous [compact_space α] [separated_space α]
   {f : α → β} (h : continuous f) : uniform_continuous f :=
-begin
-  calc
-  map (prod.map f f) (𝓤 α) = map (prod.map f f) (⨆ x, 𝓝 (x, x))  : by rw compact_space_uniformity
-                       ... =  ⨆ x, map (prod.map f f) (𝓝 (x, x)) : by rw map_supr
-                       ... ≤ ⨆ x, 𝓝 (f x, f x) : supr_le_supr (λ x, (h.prod_map h).continuous_at)
-                       ... ≤ ⨆ y, 𝓝 (y, y)     : _
-                       ... ≤ 𝓤 β                : nhds_le_uniformity,
-  rw ← supr_range,
-  simp only [and_imp, supr_le_iff, prod.forall, supr_exists, mem_range, prod.mk.inj_iff],
-  rintros _ _ ⟨y, rfl, rfl⟩,
-  exact le_supr (λ x, 𝓝 (x, x)) (f y),
-end
+calc
+map (prod.map f f) (𝓤 α) = map (prod.map f f) (⨆ x, 𝓝 (x, x))  : by rw compact_space_uniformity
+                     ... =  ⨆ x, map (prod.map f f) (𝓝 (x, x)) : by rw map_supr
+                     ... ≤ ⨆ x, 𝓝 (f x, f x)     : supr_le_supr (λ x, (h.prod_map h).continuous_at)
+                     ... ≤ ⨆ y, 𝓝 (y, y)         : supr_comp_le (λ y, 𝓝 (y, y)) f
+                     ... ≤ 𝓤 β                   : nhds_le_uniformity
 
 /-- Heine-Cantor: a continuous function on a compact separated set of a uniform space is
 uniformly continuous. -/