chore(topology/metric_space): add 2 lemmas, golf (#8861)

src/topology/metric_space/basic.lean

@@ -1618,6 +1618,9 @@ begin
   { exact bounded_closed_ball.subset hC }
 end
 
+lemma bounded.subset_ball (h : bounded s) (c : α) : ∃ r, s ⊆ closed_ball c r :=
+(bounded_iff_subset_ball c).1 h
+
 lemma bounded_closure_of_bounded (h : bounded s) : bounded (closure s) :=
 let ⟨C, h⟩ := h in
 ⟨C, λ a b ha hb, (is_closed_le' C).closure_subset $ map_mem_closure2 continuous_dist ha hb h⟩
@@ -1852,22 +1855,38 @@ end diam
 
 end metric
 
+lemma comap_dist_right_at_top_le_cocompact (x : α) : comap (λ y, dist y x) at_top ≤ cocompact α :=
+begin
+  refine filter.has_basis_cocompact.ge_iff.2 (λ s hs, mem_comap.2 _),
+  rcases hs.bounded.subset_ball x with ⟨r, hr⟩,
+  exact ⟨Ioi r, Ioi_mem_at_top r, λ y hy hys, (mem_closed_ball.1 $ hr hys).not_lt hy⟩
+end
+
+lemma comap_dist_left_at_top_le_cocompact (x : α) : comap (dist x) at_top ≤ cocompact α :=
+by simpa only [dist_comm _ x] using comap_dist_right_at_top_le_cocompact x
+
+lemma comap_dist_right_at_top_eq_cocompact [proper_space α] (x : α) :
+  comap (λ y, dist y x) at_top = cocompact α :=
+(comap_dist_right_at_top_le_cocompact x).antisymm $ (tendsto_dist_right_cocompact_at_top x).le_comap
+
+lemma comap_dist_left_at_top_eq_cocompact [proper_space α] (x : α) :
+  comap (dist x) at_top = cocompact α :=
+(comap_dist_left_at_top_le_cocompact x).antisymm $ (tendsto_dist_left_cocompact_at_top x).le_comap
+
+lemma tendsto_cocompact_of_tendsto_dist_comp_at_top {f : β → α} {l : filter β} (x : α)
+  (h : tendsto (λ y, dist (f y) x) l at_top) : tendsto f l (cocompact α) :=
+by { refine tendsto.mono_right _ (comap_dist_right_at_top_le_cocompact x), rwa tendsto_comap_iff }
+
 namespace int
 open metric
 
 /-- Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite. -/
 lemma tendsto_coe_cofinite : tendsto (coe : ℤ → ℝ) cofinite (cocompact ℝ) :=
 begin
-  simp only [filter.has_basis_cocompact.tendsto_right_iff, eventually_iff_exists_mem],
-  intros s hs,
-  obtain ⟨r, hr⟩ : ∃ r, s ⊆ closed_ball (0:ℝ) r,
-  { rw ← bounded_iff_subset_ball,
-    exact hs.bounded },
-  refine ⟨(coe ⁻¹' closed_ball (0:ℝ) r)ᶜ, _, _⟩,
-  { simp [mem_cofinite, real.closed_ball_eq, set.Icc_ℤ_finite] },
-  { rw ← compl_subset_compl at hr,
-    intros y hy,
-    exact hr hy }
+  refine tendsto_cocompact_of_tendsto_dist_comp_at_top (0 : ℝ) _,
+  simp only [filter.tendsto_at_top, eventually_cofinite, not_le, ← mem_ball],
+  change ∀ r : ℝ, finite (coe ⁻¹' (ball (0 : ℝ) r)),
+  simp [real.ball_eq, Ioo_ℤ_finite]
 end
 
 end int