-- Mathlib/Topology/UniformSpace/Completion.lean
theorem denseRange_pureCauchy : DenseRange (pureCauchy : α → CauchyFilter α) := fun f => by
  have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs =>
    let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs
    let ⟨t', ht'₁, ht'₂⟩ := comp_mem_uniformity_sets ht''₁
    have : t' ∈ f.val ×ˢ f.val := f.property.right ht'₁
    let ⟨t, ht, (h : t ×ˢ t ⊆ t')⟩ := mem_prod_same_iff.mp this
    let ⟨x, (hx : x ∈ t)⟩ := f.property.left.nonempty_of_mem ht
    have : t'' ∈ f.val ×ˢ pure x :=
      mem_prod_iff.mpr
        ⟨t, ht, { y : α | (x, y) ∈ t' }, h <| mk_mem_prod hx hx,
          fun ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩ =>
          ht'₂ <| prod_mk_mem_compRel (@h (a, x) ⟨h₁, hx⟩) h₂⟩
    ⟨x, ht''₂ <| by dsimp [gen]; exact this⟩
  simp only [closure_eq_cluster_pts, ClusterPt, nhds_eq_uniformity, lift'_inf_principal_eq,
    Set.inter_comm _ (range pureCauchy), mem_setOf_eq]
  refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)
  · exact monotone_const.inter monotone_preimage
  · let ⟨y, hy⟩ := h_ex s hs
    have : pureCauchy y ∈ range pureCauchy ∩ { y : CauchyFilter α | (f, y) ∈ s } :=
      ⟨mem_range_self y, hy⟩
    exact ⟨_, this⟩

Proof state:
case refine_1
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ Monotone fun t => range pureCauchy ∩ UniformSpace.ball f t

Tactic:
exact monotone_const.inter monotone_preimage

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
y : α
hy : (f, pureCauchy y) ∈ s
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty

Tactic:
have : pureCauchy y ∈ range pureCauchy ∩ { y : CauchyFilter α | (f, y) ∈ s } :=
  ⟨mem_range_self y, hy⟩

Result:
case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
y : α
hy : (f, pureCauchy y) ∈ s
this : pureCauchy y ∈ range pureCauchy ∩ {y | (f, y) ∈ s}
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty

Proof state:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ ((𝓤 (CauchyFilter α)).lift' fun t => range pureCauchy ∩ UniformSpace.ball f t).NeBot

Tactic:
refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)

Result:
case refine_1
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ Monotone fun t => range pureCauchy ∩ UniformSpace.ball f t

case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty

Proof state:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ f ∈ closure (range pureCauchy)

Tactic:
simp only [closure_eq_cluster_pts, ClusterPt, nhds_eq_uniformity, lift'_inf_principal_eq,
  Set.inter_comm _ (range pureCauchy), mem_setOf_eq]

Result:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ ((𝓤 (CauchyFilter α)).lift' fun t => range pureCauchy ∩ UniformSpace.ball f t).NeBot

Proof state:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
⊢ f ∈ closure (range pureCauchy)

Tactic:
have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs =>
  let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs
  let ⟨t', ht'₁, ht'₂⟩ := comp_mem_uniformity_sets ht''₁
  have : t' ∈ f.val ×ˢ f.val := f.property.right ht'₁
  let ⟨t, ht, (h : t ×ˢ t ⊆ t')⟩ := mem_prod_same_iff.mp this
  let ⟨x, (hx : x ∈ t)⟩ := f.property.left.nonempty_of_mem ht
  have : t'' ∈ f.val ×ˢ pure x :=
    mem_prod_iff.mpr
      ⟨t, ht, { y : α | (x, y) ∈ t' }, h <| mk_mem_prod hx hx,
        fun ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩ =>
        ht'₂ <| prod_mk_mem_compRel (@h (a, x) ⟨h₁, hx⟩) h₂⟩
  ⟨x, ht''₂ <| by dsimp [gen]; exact this⟩

Result:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
⊢ f ∈ closure (range pureCauchy)

Proof state:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ (f, pureCauchy x) ∈ gen t''

Tactic:
dsimp [gen]

Result:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ t'' ∈ ↑f ×ˢ ↑(pureCauchy x)

Proof state:
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ t'' ∈ ↑f ×ˢ ↑(pureCauchy x)

Tactic:
exact this

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty

Tactic:
let ⟨y, hy⟩ := h_ex s hs

Result:
case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
y : α
hy : (f, pureCauchy y) ∈ s
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty

Proof state:
case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
y : α
hy : (f, pureCauchy y) ∈ s
this : pureCauchy y ∈ range pureCauchy ∩ {y | (f, y) ∈ s}
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty

Tactic:
exact ⟨_, this⟩

Result:
no goals