`x ↦ comap coe (𝓝 x)` is a right inverse to the separation quotient map `Cauchy α → completion α` and sends a point to the unique maximal Cauchy filter that (uniquely) tends to it.

uniform_completion.lean

import topology.uniform_space.completion

variables {α : Type*} [uniform_space α]

open uniform_space filter
open_locale topological_space

lemma Cauchy.tendsto_nhds_self (F : Cauchy α) : F.1.tendsto Cauchy.pure_cauchy (𝓝 F) :=
begin
  rw uniform.tendsto_nhds_left,
  intros s hs,
  obtain ⟨t, ht, hts⟩ := Cauchy.mem_uniformity'.1 hs,
  obtain ⟨r, hr, hrt⟩ := (cauchy_iff'.1 F.2).2 t ht,
  rw filter.mem_map_iff_exists_image,
  use [r, hr],
  rw set.image_subset_iff,
  intros x hx, apply hts,
  rw filter.mem_prod_iff,
  use [r, hx, r, hr],
  rintro ⟨x, y⟩ ⟨hx, hy⟩,
  exact hrt x hx y hy,
end

lemma forall_cauchy (x : completion α) :
  ∀ F : Cauchy α, x = quotient.mk' F → F.1.tendsto coe (𝓝 x) :=
by { rintro F rfl, exact (continuous_quotient_mk.tendsto _).comp F.tendsto_nhds_self }

lemma exists_cauchy (x : completion α) :
  ∃ F : filter α, cauchy F ∧ F.tendsto coe (𝓝 x) :=
by { rcases x, exact ⟨x.1, x.2, forall_cauchy _ _ rfl⟩ }

def preferred_cauchy (x : completion α) : {F : Cauchy α // tendsto coe F.1 (𝓝 x)} :=
⟨⟨comap coe (𝓝 x), cauchy_nhds.comap' (completion.uniform_inducing_coe α).comap_uniformity.le
  (completion.dense_inducing_coe.comap_nhds_ne_bot x)⟩, tendsto_comap⟩

def preferred_cauchy' (x : Cauchy α) : {F : Cauchy α // tendsto Cauchy.pure_cauchy F.1 (𝓝 x)} :=
⟨⟨comap _ (𝓝 x), cauchy_nhds.comap' Cauchy.uniform_inducing_pure_cauchy.comap_uniformity.le
  (Cauchy.dense_inducing_pure_cauchy.comap_nhds_ne_bot x)⟩, tendsto_comap⟩

lemma preferred_cauchy'_eq_cauchy (x : Cauchy α) :
  (preferred_cauchy' x).1 = (preferred_cauchy $ quotient.mk' x).1 :=
begin
  ext1, change filter.comap _ _ = comap _ _,
  conv_rhs { rw [completion.coe_eq, ← filter.comap_comap] },
  erw ← inducing.nhds_eq_comap,
  exact uniform_inducing.inducing ⟨uniform_space.comap_quotient_eq_uniformity⟩,
end

lemma tendsto_unique {x y : completion α} (F : filter α) (hF : F.ne_bot)
  (h : F.tendsto coe (𝓝 x) ∧ F.tendsto coe (𝓝 y)) : x = y :=
begin
  rw [tendsto, tendsto, ← le_inf_iff] at h,
  apply t2_iff_nhds.1,
  { rw ← separated_iff_t2, apply_instance },
  { exact ne_bot_of_le h },
end

/-- For a Cauchy filter `F`, it's image in the completion is the unique limit of `F.map coe`. -/
lemma mk_eq_iff_tendsto {F : Cauchy α} {x : completion α} :
  x = quotient.mk' F ↔ F.1.tendsto coe (𝓝 x) :=
⟨forall_cauchy x F, λ h, tendsto_unique F.1 F.2.1 ⟨h, forall_cauchy _ _ rfl⟩⟩

/-- `preferred_cauchy` is a right inverse to `quotient.mk`. -/
lemma mk_preferred_cauchy (x : completion α) : x = quotient.mk' (preferred_cauchy x) :=
let ⟨⟨F, hc⟩, ht⟩ := preferred_cauchy x in tendsto_unique F hc.1 ⟨ht, forall_cauchy _ _ rfl⟩

/-- `preferred_cauchy x` is the unique maximal Cauchy filter in the class of `x : completion α`.-/
lemma self_le_preferred_cauchy_mk (x : Cauchy α) : x.1 ≤ (preferred_cauchy $ quotient.mk' x).1.1 :=
filter.map_le_iff_le_comap.1 (forall_cauchy _ _ rfl)

def inv_mk (x : completion α) := {F : Cauchy α // x = quotient.mk' F}

lemma exists_unique_max (x : completion α) : ∃! F : inv_mk x, ∀ F' : inv_mk x, F'.1.1 ≤ F.1.1 :=
begin
  let F := preferred_cauchy x,
  have he := mk_eq_iff_tendsto.2 F.2,
  apply exists_unique_of_exists_of_unique,
  { use [F.1, he], intro F',
    convert self_le_preferred_cauchy_mk F'.1,
    swap 3, { rw ← F'.2, refl },
    all_goals { ext, rw ← F'.2, apply mk_eq_iff_tendsto } },
  { intros F F' h h', ext, exact ⟨@h F' _, @h' F _⟩ },
end

/-- Irrelevant to the above development. -/
lemma separation_setoid_eq_inseparable_setoid {α} [uniform_space α] :
  uniform_space.separation_setoid α = inseparable_setoid α :=
begin
  ext, change (a,b) ∈ separation_rel α ↔ inseparable a b,
  rw inseparable_iff_forall_open,
  split; intro h,
  { intros s hs, suffices : _,
    { split, revert a b h,
      exacts [this, this _ _ $ (uniform_space.separation_setoid α).symm' h] },
    { clear h a b, exact λ a b h ha, h _ (_root_.is_open_uniformity.1 hs a ha) rfl } },
  { exact uniformity_has_basis_open.mem_separation_rel.2 (λ s hs, (h {x | (a, x) ∈ s} $ 
      (continuous.prod.mk a).is_open_preimage _ hs.2).1 $ refl_mem_uniformity hs.1) },
end

Has this file made it into mathlib?

Has this file made it into mathlib?

To my knowledge, no.