-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem totallyBounded_iff_filter {s : Set α} :
    TotallyBounded s ↔ ∀ f, NeBot f → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c

Proof state:
case mpr
α : Type u
uniformSpace : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
⊢ ∃ f, f.NeBot ∧ f ≤ 𝓟 s ∧ ∀ c ≤ f, ¬Cauchy c

Tactic:
set f := ⨅ t : Finset α, 𝓟 (s \ ⋃ y ∈ t, { x | (x, y) ∈ d })

Result:
case mpr
α : Type u
uniformSpace : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
f : Filter α := ⨅ t, 𝓟 (s \ ⋃ y ∈ t, {x | (x, y) ∈ d})
⊢ ∃ f, f.NeBot ∧ f ≤ 𝓟 s ∧ ∀ c ≤ f, ¬Cauchy c

Proof state:
α : Type u
uniformSpace : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
f : Filter α := ⨅ t, 𝓟 (s \ ⋃ y ∈ t, {x | (x, y) ∈ d})
hb : f.HasAntitoneBasis fun t => s \ ⋃ y ∈ t, {x | (x, y) ∈ d}
this : f.NeBot
⊢ 𝓟 (s \ ⋃ y ∈ ∅, {x | (x, y) ∈ d}) ≤ 𝓟 s

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u
uniformSpace : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
f : Filter α := ⨅ t, 𝓟 (s \ ⋃ y ∈ t, {x | (x, y) ∈ d})
hb : f.HasAntitoneBasis fun t => s \ ⋃ y ∈ t, {x | (x, y) ∈ d}
this : f.NeBot
⊢ ∃ f, f.NeBot ∧ f ≤ 𝓟 s ∧ ∀ c ≤ f, ¬Cauchy c

Tactic:
have : f ≤ 𝓟 s := iInf_le_of_le ∅ (by simp)

Result:
case mpr
α : Type u
uniformSpace : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
f : Filter α := ⨅ t, 𝓟 (s \ ⋃ y ∈ t, {x | (x, y) ∈ d})
hb : f.HasAntitoneBasis fun t => s \ ⋃ y ∈ t, {x | (x, y) ∈ d}
this✝ : f.NeBot
this : f ≤ 𝓟 s
⊢ ∃ f, f.NeBot ∧ f ≤ 𝓟 s ∧ ∀ c ≤ f, ¬Cauchy c

Proof state:
case mpr.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
f : Filter α := ⨅ t, 𝓟 (s \ ⋃ y ∈ t, {x | (x, y) ∈ d})
hb : f.HasAntitoneBasis fun t => s \ ⋃ y ∈ t, {x | (x, y) ∈ d}
this✝¹ : f.NeBot
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
this : s \ {x | (x, y) ∈ d} ∈ c
⊢ False

Tactic:
rcases hc.1.nonempty_of_mem (inter_mem hm this) with ⟨z, hzm, -, hyz⟩

Result:
case mpr.intro.intro.intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
s : Set α
d : Set (α × α)
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → ¬s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
f : Filter α := ⨅ t, 𝓟 (s \ ⋃ y ∈ t, {x | (x, y) ∈ d})
hb : f.HasAntitoneBasis fun t => s \ ⋃ y ∈ t, {x | (x, y) ∈ d}
this✝¹ : f.NeBot
this✝ : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
this : s \ {x | (x, y) ∈ d} ∈ c
z : α
hzm : z ∈ m
hyz : z ∉ {x | (x, y) ∈ d}
⊢ False

Proof state:
case mp
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ TotallyBounded s → ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c

Tactic:
exact fun H f hf hfs => ⟨Ultrafilter.of f, Ultrafilter.of_le f,
  (Ultrafilter.of f).cauchy_of_totallyBounded H ((Ultrafilter.of_le f).trans hfs)⟩

Result:
no goals