Prove that functions that are zero at infinity are uniformly continuous, using filters.

uniform_continuous_zero_at_infty_filter.lean

import topology.uniform_space.basic
import topology.homeomorph

open_locale topological_space uniformity filter
open filter uniform_space set

variables {α β : Type*} [uniform_space α] [uniform_space β]

lemma is_compact.nhds_set_diagonal₁ {α} [uniform_space α] {s : set α} (hs : is_compact s) :
  𝓝ˢ ((λ x, (x, x)) '' s) = 𝓤 α ⊓ 𝓝ˢ (prod.fst ⁻¹' s) := 
begin
  apply le_antisymm,
  { refine le_inf ((nhds_set_mono _).trans nhds_set_diagonal_le_uniformity) (nhds_set_mono _);
    rintros p ⟨x, hx, rfl⟩, exacts [rfl, hx] },
  have := (𝓤 α).basis_sets.prod_self.comap _,
  rw ← uniformity_prod_eq_comap_prod at this,
  refine ((hs.image $ by continuity).nhds_set_basis_uniformity this).ge_iff.2 (λ U hU, _),
  obtain ⟨V, hV, hVU⟩ := comp_mem_uniformity_sets hU,
  rw mem_inf_iff_superset,
  refine ⟨V, hV, prod.fst ⁻¹' (⋃ y ∈ s, ball y V), mem_nhds_set_iff_forall.2 _, _⟩,
  { rintro ⟨x, y⟩ (hx : x ∈ s),
    apply continuous_fst.continuous_at.preimage_mem_nhds,
    exact mem_of_superset (ball_mem_nhds _ hV) (subset_bUnion_of_mem hx) },
  { rintro ⟨x, y⟩ ⟨h, h'⟩, obtain ⟨z, hz, hp⟩ := mem_Union₂.1 h',
    refine mem_Union₂.2 ⟨_, ⟨z, hz, rfl⟩, hVU ⟨z, _, _⟩, hVU ⟨x, _, _⟩⟩,
    exacts [refl_mem_uniformity hV, hp, hp, h] },
end

lemma is_compact.nhds_set_diagonal₂ {s : set α} (hs : is_compact s) :
  𝓝ˢ ((λ x, (x, x)) '' s) = 𝓤 α ⊓ 𝓝ˢ (prod.snd ⁻¹' s) := 
begin
  rw ← comap_swap_uniformity,
  convert congr_arg (filter.comap $ prod.swap) hs.nhds_set_diagonal₁;
    nth_rewrite 0 (homeomorph.prod_comm α α).inducing.nhds_set_eq_comap,
  congr' 2, { ext, rw image_image, refl },
  rw filter.comap_inf, congr,
  rw [← homeomorph.coe_to_equiv, equiv.image_eq_preimage, preimage_preimage], refl,
end

lemma filter.le_of_inf_principal_compl_le {f g : filter α}
  (h : ∀ s ∈ g, f ⊓ 𝓟 sᶜ ≤ g) : f ≤ g :=
λ t ht, by simpa only [mem_inf_principal', compl_compl, union_self] using h t ht ht

lemma continuous.uniform_continuous_of_zero_at_infty {f : α → β} [has_zero β]
  (h_cont : continuous f) (h_zero : tendsto f (cocompact α) (𝓝 0)) : uniform_continuous f :=
map_le_iff_le_comap.2 $ filter.le_of_inf_principal_compl_le $ λ s hs, begin
  have := h_zero.prod_map h_zero,
  rw [← nhds_prod_eq, tendsto, map_le_iff_le_comap] at this,
  obtain ⟨t, ht, hts⟩ := has_basis_cocompact.prod_self.mem_iff.1
    (this $ comap_mono (nhds_le_uniformity _) hs),
  have : 𝓟 sᶜ ≤ 𝓝ˢ (prod.fst ⁻¹' t ∪ prod.snd ⁻¹' t) :=
    principal_le_nhds_set.trans (nhds_set_mono $ λ x hx, _), swap,
  { rw mem_union, contrapose! hx, exact λ h, h (hts hx) },
  apply (inf_le_inf_left _ this).trans,
  rw [nhds_set_union, inf_sup_left, ← ht.nhds_set_diagonal₁, ← ht.nhds_set_diagonal₂, sup_idem],
  refine Sup_le (λ F, _),
  rintro ⟨_, ⟨x, hx, rfl⟩, rfl⟩,
  rw ← map_le_iff_le_comap,
  exact le_trans (h_cont.prod_map h_cont).continuous_at (nhds_le_uniformity _),
end