Totally boundedness

Stream: Is there code for X?

[Moritz Doll]

I want to show that totally bounded has the following characterization:

import topology.algebra.uniform_group
import topology.uniform_space.cauchy

open_locale topological_space uniformity pointwise

variables {α : Type*}
variables [uniform_space α] [group α] [uniform_group α]

lemma test (A : set α) : totally_bounded A ↔
  ∀ (U : set α) (hU : U ∈ 𝓝 (1 : α)),
  ∃ (t : set α), t.finite ∧ A ⊆ ⋃ (y : α) (h : y ∈ t), y • U :=
begin
  split; intros h U hU,
  {
    let m := (λ (x : α × α), x.snd / x.fst),
    have hU' : m ⁻¹' U ∈ filter.comap m (𝓝 1) := filter.preimage_mem_comap hU,
    rw ←uniformity_eq_comap_nhds_one α at hU',
    specialize h (m ⁻¹' U) hU',
    rcases h with ⟨s, hs, h⟩,
    refine ⟨s, hs, _⟩,
    refine h.trans _,
    refine set.Union₂_mono _,
    intros a ha b hb,
    simp only [set.mem_preimage, set.mem_set_of_eq] at hb,
    sorry,
  },
  rw [uniformity_eq_comap_nhds_one α, filter.mem_comap] at hU,
  rcases hU with ⟨V, hV, hU⟩,
  specialize h V hV,
  rcases h with ⟨s, hs, h⟩,
  use [s, hs],
  refine h.trans _,
  refine set.Union₂_mono _,
  intros a ha b hb,
  refine hU _,
  simp only [set.mem_preimage],
  sorry,
end

The proof does not quite work (uniformity_eq_comap_nhds_one has to be replaced with a flipped version). It looks too ugly to be the correct way to do that anyways. Is there a better way to prove this?

[Yury G. Kudryashov]

We should add filter.has_basis.totally_bounded_iff.