awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Ultrafilter α
hf : (↑f : Filter α).TotallyBounded
⊢ Cauchy (↑f : Filter α)

Tactic:
⟨f.neBot', fun _ ht =>
    let ⟨t', ht'₁, ht'_symm, ht'_t⟩ := comp_symm_of_uniformity ht
    let ⟨i, hi, ht'_f⟩ := hf t' ht'₁
    have : ∃ y ∈ i, { x | (x, y) ∈ t' } ∈ f := (Ultrafilter.eventually_exists_mem_iff hi).1 ht'_f
    let ⟨y, _, hif⟩ := this
    have : {x | (x, y) ∈ t'} ×ˢ {x | (x, y) ∈ t'} ⊆ t' ○ t' :=
      fun ⟨_, _⟩ ⟨(h₁ : (_, y) ∈ t'), (h₂ : (_, y) ∈ t')⟩ => ⟨y, h₁, ht'_symm h₂⟩
    mem_of_superset (prod_mem_prod hif hif) (Subset.trans this ht'_t)⟩

Premises used: Ultrafilter.neBot', Cauchy, _private.0.Ultrafilter.cauchy_of_totallyBounded'.match_4, comp_symm_of_uniformity, Ultrafilter.eventually_exists_mem_iff, SProd.sprod, Set.Subset.trans, Membership.mem, Prod.mk, _private.0.Ultrafilter.cauchy_of_totallyBounded'.match_3, SetRel.comp, _private.0.Ultrafilter.cauchy_of_totallyBounded'.match_2, And.intro, Exists.intro, Iff.mp, Filter.prod_mem_prod, _private.0.Ultrafilter.cauchy_of_totallyBounded'.match_1, _private.0.Ultrafilter.cauchy_of_totallyBounded'.match_5, Ultrafilter.toFilter, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
f : Ultrafilter α
hs : TotallyBounded s
h : (↑f : Filter α) ≤ 𝓟 s
⊢ Cauchy (↑f : Filter α)

Tactic:
f.cauchy_of_totallyBounded' <| (Filter.totallyBounded_principal_iff.mpr hs).mono h

Premises used: Iff.mpr, Filter.totallyBounded_principal_iff, Filter.TotallyBounded.mono, Ultrafilter.cauchy_of_totallyBounded'
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
mp : g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
mpr : (∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c) → g.TotallyBounded
⊢ g.TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c

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

Premises used: Ultrafilter.of_le, Filter.TotallyBounded.mono, Ultrafilter.of, And.intro, Exists.intro, Ultrafilter.cauchy_of_totallyBounded', LE.le.trans, Ultrafilter.toFilter
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded → ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ 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.mono ((Ultrafilter.of_le f).trans hfs))⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
d : SetRel α α
hd : d ∈ 𝓤 α
mpr :
  ∀ (hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g),
    ∃ (f : Filter α), f.NeBot ∧ f ≤ g ∧ ∀ (c : Filter α) (_ : c ≤ f), ¬Cauchy c
⊢ ∃ (t : Set α), t.Finite ∧ d.preimage t ∈ g

Tactic:
contrapose! H with hd_cover
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
s t : Finset α
h : s ⊆ t
⊢ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ ≤ g ⊓ 𝓟 (d.preimage (↑s : Set α))ᶜ

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
⊢ Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ

Tactic:
have hb : Antitone fun t : Finset α ↦ g ⊓ 𝓟 (d.preimage t)ᶜ :=
      fun s t (h : s ⊆ t) => by beta_reduce; gcongr
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
⊢ f.NeBot

Tactic:
have : Filter.NeBot f :=
      (Filter.iInf_neBot_iff_of_directed' <| hb.directed_ge).mpr fun t =>
        Filter.notMem_iff_inf_principal_compl.mp <| hd_cover t t.finite_toSet
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this : f.NeBot
⊢ g ⊓ 𝓟 (d.preimage (↑∅ : Set α))ᶜ ≤ g

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this : f.NeBot
⊢ f ≤ g

Tactic:
have : f ≤ g := iInf_le_of_le ∅ (by simp)
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
⊢ ∃ (f : Filter α), f.NeBot ∧ f ≤ g ∧ ∀ (c : Filter α) (_ : c ≤ f), ¬Cauchy c

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
mpr : ∀ (c : Filter α) (hcf : c ≤ f) (hc : Cauchy c), False
⊢ ∃ (f : Filter α), f.NeBot ∧ f ≤ g ∧ ∀ (c : Filter α) (_ : c ≤ f), ¬Cauchy c

Tactic:
refine ⟨f, ‹_›, ‹_›, fun c hcf hc => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
mpr : ∀ (m : Set α) (hm : m ∈ c) (hmd : m ×ˢ m ⊆ d), False
⊢ False

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

Premises used: And.right, Iff.mp, Filter.mem_prod_same_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
mpr : ∀ (y : α) (hym : y ∈ m), False
⊢ False

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

Premises used: And.left, Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ {x : α | (x, y) ∈ d}ᶜ ∈ c

Tactic:
simpa [SetRel.preimage] using hcf.trans <| (iInf_le _ {y}).trans inf_le_right

Premises used: SetRel.preimage, LE.le.trans, iInf_le
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ {x : α | (x, y) ∈ d}ᶜ ∈ c

Tactic:
have : {x | (x, y) ∈ d}ᶜ ∈ c := by
      simpa [SetRel.preimage] using hcf.trans <| (iInf_le _ {y}).trans inf_le_right
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this_2 : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
this : {x : α | (x, y) ∈ d}ᶜ ∈ c
mpr : ∀ (z : α) (hzm : z ∈ m) (hyz : Membership.mem (γ := Set α) {x : α | (x, y) ∈ d}ᶜ z), False
⊢ False

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

Premises used: Filter.inter_mem, And.left, Filter.NeBot.nonempty_of_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this_2 : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
this : {x : α | (x, y) ∈ d}ᶜ ∈ c
z : α
hzm : z ∈ m
hyz : Membership.mem (γ := Set α) {x : α | (x, y) ∈ d}ᶜ z
⊢ False

Tactic:
hyz (hmd ⟨hzm, hym⟩)

Premises used: And.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α) (_ : t.Finite), d.preimage t ∉ g
f : Filter α := ⨅ (t : Finset α), g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
hb : Antitone (β := Filter α) fun (t : Finset α) ↦ g ⊓ 𝓟 (d.preimage (↑t : Set α))ᶜ
this_1 : f.NeBot
this_2 : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
this : {x : α | (x, y) ∈ d}ᶜ ∈ c
z : α
hzm : z ∈ m
hyz : Membership.mem (γ := Set α) {x : α | (x, y) ∈ d}ᶜ z
⊢ False

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

Premises used: And.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ g.TotallyBounded ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → Cauchy (↑f : Filter α)

Tactic:
⟨fun hg f hf => f.cauchy_of_totallyBounded' <| hg.mono hf,
    fun H => g.totallyBounded_iff_filter.2 ?_⟩

Premises used: Iff.mpr, Filter.totallyBounded_iff_filter, Filter.TotallyBounded.mono, Iff.intro, Ultrafilter.cauchy_of_totallyBounded'
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
refine :
  ∀ (H : ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → Cauchy (↑f : Filter α)) (f : Filter α),
    f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c
⊢ g.TotallyBounded ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → Cauchy (↑f : Filter α)

Tactic:
refine ⟨fun hg f hf => f.cauchy_of_totallyBounded' <| hg.mono hf,
    fun H => g.totallyBounded_iff_filter.2 ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → Cauchy (↑f : Filter α)
f : Filter α
hf : f.NeBot
hfs : f ≤ g
⊢ ∃ c ≤ f, Cauchy c

Tactic:
⟨Ultrafilter.of f, Ultrafilter.of_le f, H _ ((Ultrafilter.of_le f).trans hfs)⟩

Premises used: Ultrafilter.of_le, Ultrafilter.of, And.intro, Exists.intro, LE.le.trans, Ultrafilter.toFilter
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ g → Cauchy (↑f : Filter α)
f : Filter α
hf : f.NeBot
hfs : f ≤ g
⊢ ∃ c ≤ f, Cauchy c

Tactic:
exact ⟨Ultrafilter.of f, Ultrafilter.of_le f, H _ ((Ultrafilter.of_le f).trans hfs)⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
rw : (𝓟 s).TotallyBounded ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
rw₁ rw₂ :
  (∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c) ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c
⊢ TotallyBounded s ↔ ∀ (f : Filter α), f.NeBot → f ≤ 𝓟 s → ∃ c ≤ f, Cauchy c

Tactic:
rw [← Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_filter]

Premises used: Filter.totallyBounded_iff_filter, Filter.totallyBounded_principal_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
rw : (𝓟 s).TotallyBounded ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)
rw₁ rw₂ :
  (∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)) ↔
    ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)
⊢ TotallyBounded s ↔ ∀ (f : Ultrafilter α), (↑f : Filter α) ≤ 𝓟 s → Cauchy (↑f : Filter α)

Tactic:
rw [← Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_ultrafilter]

Premises used: Filter.totallyBounded_principal_iff, Filter.totallyBounded_iff_ultrafilter
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ IsCompact s ↔ TotallyBounded s ∧ IsComplete s

Tactic:
⟨fun hs =>
    ⟨totallyBounded_iff_ultrafilter.2 fun f hf =>
        let ⟨_, _, fx⟩ := isCompact_iff_ultrafilter_le_nhds.1 hs f hf
        cauchy_nhds.mono fx,
      fun f fc fs =>
      let ⟨a, as, fa⟩ := @hs f fc.1 fs
      ⟨a, as, le_nhds_of_cauchy_adhp fc fa⟩⟩,
    fun ⟨ht, hc⟩ =>
    isCompact_iff_ultrafilter_le_nhds.2 fun f hf =>
      hc _ (totallyBounded_iff_ultrafilter.1 ht f hf) hf⟩

Premises used: Iff.mpr, Cauchy, le_nhds_of_cauchy_adhp, Cauchy.mono, Membership.mem, Exists, nhds, LE.le, isCompact_iff_ultrafilter_le_nhds, And, And.intro, _private.0.isCompact_iff_totallyBounded_isComplete.match_3, Iff.intro, Exists.intro, Iff.mp, _private.0.isCompact_iff_totallyBounded_isComplete.match_2, totallyBounded_iff_ultrafilter, _private.0.isCompact_iff_totallyBounded_isComplete.match_1, cauchy_nhds, Ultrafilter.toFilter, IsCompact
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : IsCompact s
⊢ TotallyBounded s

Tactic:
(isCompact_iff_totallyBounded_isComplete.1 h).1

Premises used: isCompact_iff_totallyBounded_isComplete, And.left, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : IsCompact s
⊢ IsComplete s

Tactic:
(isCompact_iff_totallyBounded_isComplete.1 h).2

Premises used: isCompact_iff_totallyBounded_isComplete, And.right, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α_1 : Type u
β : Type v
uniformSpace : UniformSpace α_1
α : Type u
inst : UniformSpace α
inst_1 : CompactSpace α
f : Filter α
hf : Cauchy f
⊢ ∃ (x : α), f ≤ 𝓝 x

Tactic:
simpa using (isCompact_iff_totallyBounded_isComplete.1 isCompact_univ).2 _ hf

Premises used: isCompact_iff_totallyBounded_isComplete, And.right, isCompact_univ, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
ht : TotallyBounded s
hc : IsComplete s
⊢ IsCompact s

Tactic:
isCompact_iff_totallyBounded_isComplete.mpr ⟨ht, hc⟩

Premises used: Iff.mpr, isCompact_iff_totallyBounded_isComplete, And.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
s : Set α
ht : TotallyBounded s
hc : IsClosed[uniformSpace.toTopologicalSpace] s
⊢ IsCompact s

Tactic:
ht.isCompact_of_isComplete hc.isComplete

Premises used: TotallyBounded.isCompact_of_isComplete, IsClosed.isComplete
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
hf : f.TotallyBounded
⊢ IsCompact.{u} (X := α) {x : α | ClusterPt x f}

Tactic:
hf.totallyBounded_setOf_clusterPt.isCompact_of_isClosed isClosed_setOf_clusterPt

Premises used: isClosed_setOf_clusterPt, TotallyBounded.isCompact_of_isClosed, Filter.TotallyBounded.totallyBounded_setOf_clusterPt
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
⊢ (↑m : Filter α) ≤ f

Tactic:
have hmf : m ≤ f := Ultrafilter.of_le f
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : (↑m : Filter α) ≤ f
⊢ Cauchy (↑m : Filter α)

Tactic:
have hm := m.cauchy_of_totallyBounded' (hf.mono hmf)
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : (↑m : Filter α) ≤ f
hm : Cauchy (↑m : Filter α)
obtain : ∀ (x : α) (hx : (↑m : Filter α) ≤ 𝓝 x), ∃ (x : α), ClusterPt x f
⊢ ∃ (x : α), ClusterPt x f

Tactic:
obtain ⟨x, hx⟩ := CompleteSpace.complete hm

Premises used: CompleteSpace.complete
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : (↑m : Filter α) ≤ f
hm : Cauchy (↑m : Filter α)
x : α
hx : (↑m : Filter α) ≤ 𝓝 x
⊢ ClusterPt x (↑m : Filter α)

Tactic:
rw [le_nhds_iff_adhp_of_cauchy hm] at hx

Premises used: le_nhds_iff_adhp_of_cauchy
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : (↑m : Filter α) ≤ f
hm : Cauchy (↑m : Filter α)
x : α
hx : ClusterPt x (↑m : Filter α)
⊢ ∃ (x : α), ClusterPt x f

Tactic:
⟨x, hx.mono hmf⟩

Premises used: ClusterPt.mono, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
inst_1 : f.NeBot
hf : f.TotallyBounded
m : Ultrafilter α := Ultrafilter.of f
hmf : (↑m : Filter α) ≤ f
hm : Cauchy (↑m : Filter α)
x : α
hx : ClusterPt x (↑m : Filter α)
⊢ ∃ (x : α), ClusterPt x f

Tactic:
exact ⟨x, hx.mono hmf⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
obtain :
  ∀ (n : ℕ) (hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a), ∃ (t : Set α), t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ a}
⊢ ∃ (t : Set α), t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ a}

Tactic:
obtain ⟨n, hn⟩ := cauchySeq_iff.1 hs a ha

Premises used: Iff.mp, cauchySeq_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∃ (t : Set α), t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ a}

Tactic:
⟨s '' { k | k ≤ n }, (finite_le_nat _).image _, ?_⟩

Premises used: setOf, Set.Finite.image, LE.le, And.intro, Exists.intro, Set.image, Set.finite_le_nat
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
refine : range s ⊆ ⋃ y ∈ s '' {k : ℕ | k ≤ n}, {x : α | (x, y) ∈ a}
⊢ ∃ (t : Set α), t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ a}

Tactic:
refine ⟨s '' { k | k ≤ n }, (finite_le_nat _).image _, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
rw :
  ∀ (y : ℕ),
    Membership.mem (γ := Set α)
      (⋃ (y : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} y), {x : α | (x, s y) ∈ a}) (s y)
⊢ range s ⊆ ⋃ y ∈ s '' {k : ℕ | k ≤ n}, {x : α | (x, y) ∈ a}

Tactic:
rw [range_subset_iff, biUnion_image]

Premises used: Set.range_subset_iff, Set.biUnion_image
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
rw :
  ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
⊢ Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} y), {x : α | (x, s y) ∈ a})
    (s m)

Tactic:
rw [mem_iUnion₂]

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
inl :
  ∀ (hm : m ≤ n),
    ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
      Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
inr :
  ∀ (hm : n ≤ m),
    ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
      Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
⊢ ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)

Tactic:
rcases le_total m n with hm | hm

Premises used: le_total
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
hm : m ≤ n
⊢ ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)

Tactic:
⟨m, hm, refl_mem_uniformity ha⟩

Premises used: refl_mem_uniformity, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
hm : n ≤ m
⊢ ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)

Tactic:
⟨n, le_refl n, hn m hm n le_rfl⟩

Premises used: le_refl, le_rfl, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
hm : m ≤ n
⊢ ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)

Tactic:
exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
rw : ∀ (i : ℕ), p i → ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}
⊢ TotallyBounded (interUnionBalls xs u U)

Tactic:
rw [Filter.HasBasis.totallyBounded_iff H]

Premises used: Filter.HasBasis.totallyBounded_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
_ : p i → ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}
⊢ p i → ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}

Tactic:
_