-- 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.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

Tactic:
exact hyz (hmd ⟨hzm, hym⟩)

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
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
⊢ False

Tactic:
rcases mem_prod_same_iff.1 (hc.2 hd) with ⟨m, hm, hmd⟩

Result:
case mpr.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
⊢ False

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
this : f ≤ 𝓟 s
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ s \ {x | (x, y) ∈ d} ∈ c

Tactic:
simpa using hcf (hb.mem {y})

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})
⊢ ∃ f, f.NeBot ∧ f ≤ 𝓟 s ∧ ∀ c ≤ f, ¬Cauchy c

Tactic:
have hb : HasAntitoneBasis f fun t : Finset α ↦ s \ ⋃ y ∈ t, { x | (x, y) ∈ d } :=
  .iInf_principal fun _ _ ↦ diff_subset_diff_right ∘ biUnion_subset_biUnion_left

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}
⊢ ∃ f, f.NeBot ∧ f ≤ 𝓟 s ∧ ∀ c ≤ f, ¬Cauchy c

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

Tactic:
intro H d hd

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

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
⊢ False

Tactic:
have : s \ {x | (x, y) ∈ d} ∈ c := by simpa using hcf (hb.mem {y})

Result:
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

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

Tactic:
contrapose! H with hd_cover

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, f.NeBot ∧ f ≤ 𝓟 s ∧ ∀ c ≤ f, ¬Cauchy c

Proof state:
case mpr.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
⊢ False

Tactic:
rcases hc.1.nonempty_of_mem hm with ⟨y, hym⟩

Result:
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
⊢ False

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}
⊢ ∃ f, f.NeBot ∧ f ≤ 𝓟 s ∧ ∀ c ≤ f, ¬Cauchy c

Tactic:
have : Filter.NeBot f := hb.1.neBot_iff.2 fun _ ↦
  diff_nonempty.2 <| hd_cover _ (Finset.finite_toSet _)

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
⊢ ∃ f, f.NeBot ∧ 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 : 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

Tactic:
refine ⟨f, ‹_›, ‹_›, fun c hcf hc => ?_⟩

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
c : Filter α
hcf : c ≤ f
hc : Cauchy c
⊢ False

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

Tactic:
constructor

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

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