awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
⊢ ∃ (i : ι), t ⊆ s i

Tactic:
⟨i, fun y hy => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
refine : ∀ (y : α) (hy : y ∈ t), y ∈ s i
⊢ ∃ (i : ι), t ⊆ s i

Tactic:
refine ⟨i, fun y hy => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
rcases : ∀ (j : ι) (hj : y ∈ s j), y ∈ s i
⊢ y ∈ s i

Tactic:
rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
j : ι
hj rwa rwa₁ rwa₂ rwa₃ : y ∈ s j
⊢ y ∈ s i

Tactic:
rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]

Premises used: Set.mk_mem_prod
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
obtain : ∀ (i : ι) (hi : t ⊆ s i), ∃ x ∈ S, l ≤ 𝓝 x
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
obtain ⟨i, hi⟩ : ∃ i, t ⊆ s i := by
    rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩
    rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩
    refine ⟨i, fun y hy => ?_⟩
    rcases mem_iUnion.1 (htS hy) with ⟨j, hj⟩
    rwa [hd i j x hi y hj (htU <| mk_mem_prod hx hy)]
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
rcases : ∀ (x : α) (hxs : x ∈ s i) (hlx : l ≤ 𝓝 x), ∃ x ∈ S, l ≤ 𝓝 x
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
rcases hs i l hl (le_principal_iff.2 <| mem_of_superset htl hi) with ⟨x, hxs, hlx⟩

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
x : α
hxs : x ∈ s i
hlx : l ≤ 𝓝 x
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
⟨x, mem_iUnion.2 ⟨i, hxs⟩, hlx⟩

Premises used: Iff.mpr, Set.mem_iUnion, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ (i : ι), s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
i : ι
hi : t ⊆ s i
x : α
hxs : x ∈ s i
hlx : l ≤ 𝓝 x
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
exact ⟨x, mem_iUnion.2 ⟨i, hxs⟩, hlx⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
inst : UniformSpace α
inst_1 : CompleteSpace α
f : Filter α
hf : Cauchy f
h : f ≤ 𝓟 univ
rcases : ∀ (x : α) (hx : f ≤ 𝓝 x), ∃ (x : α), Membership.mem (γ := Set α) univ x ∧ f ≤ 𝓝 x
⊢ ∃ (x : α), Membership.mem (γ := Set α) univ x ∧ f ≤ 𝓝 x

Tactic:
rcases CompleteSpace.complete hf with ⟨x, hx⟩

Premises used: CompleteSpace.complete
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
inst : UniformSpace α
inst_1 : CompleteSpace α
f : Filter α
hf : Cauchy f
h : f ≤ 𝓟 univ
x : α
hx : f ≤ 𝓝 x
⊢ ∃ (x : α), Membership.mem (γ := Set α) univ x ∧ f ≤ 𝓝 x

Tactic:
⟨x, mem_univ x, hx⟩

Premises used: And.intro, Exists.intro, Set.mem_univ
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
inst : UniformSpace α
inst_1 : CompleteSpace α
f : Filter α
hf : Cauchy f
h : f ≤ 𝓟 univ
x : α
hx : f ≤ 𝓝 x
⊢ ∃ (x : α), Membership.mem (γ := Set α) univ x ∧ f ≤ 𝓝 x

Tactic:
exact ⟨x, mem_univ x, hx⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace α
inst_2 : CompleteSpace β
f : Filter (α × β)
hf : Cauchy f
x1 : α
hx1 : map (fun (p : α × β) ↦ p.1) f ≤ 𝓝 x1
x2 : β
hx2 : map (fun (p : α × β) ↦ p.2) f ≤ 𝓝 x2
rw : Tendsto Prod.fst f (𝓝 x1) ∧ Tendsto Prod.snd f (𝓝 x2)
⊢ f ≤ 𝓝 (x1, x2)

Tactic:
rw [nhds_prod_eq, le_prod]

Premises used: Filter.le_prod, nhds_prod_eq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace α
inst_2 : CompleteSpace β
f : Filter (α × β)
hf : Cauchy f
x1 : α
hx1 : map (fun (p : α × β) ↦ p.1) f ≤ 𝓝 x1
x2 : β
hx2 : map (fun (p : α × β) ↦ p.2) f ≤ 𝓝 x2
left : Tendsto Prod.fst f (𝓝 x1)
right : Tendsto Prod.snd f (𝓝 x2)
⊢ Tendsto Prod.fst f (𝓝 x1) ∧ Tendsto Prod.snd f (𝓝 x2)

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace α
inst_2 : CompleteSpace β
f : Filter (α × β)
hf : Cauchy f
x1 : α
hx1 : map (fun (p : α × β) ↦ p.1) f ≤ 𝓝 x1
x2 : β
hx2 : map (fun (p : α × β) ↦ p.2) f ≤ 𝓝 x2
⊢ Tendsto Prod.fst f (𝓝 x1)

Tactic:
assumption
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace α
inst_2 : CompleteSpace β
f : Filter (α × β)
hf : Cauchy f
x1 : α
hx1 : map (fun (p : α × β) ↦ p.1) f ≤ 𝓝 x1
x2 : β
hx2 : map (fun (p : α × β) ↦ p.2) f ≤ 𝓝 x2
⊢ Tendsto Prod.snd f (𝓝 x2)

Tactic:
assumption
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace (α × β)
h : Nonempty β
f : Filter α
hf : Cauchy f
y : β
a : α
b : β
hab : SProd.sprod (β := Filter β) f (pure y) ≤ 𝓝 (a, b)
⊢ f ≤ 𝓝 a

Tactic:
simpa only [map_fst_prod, nhds_prod_eq] using map_mono (m := Prod.fst) hab

Premises used: Filter.map_mono, nhds_prod_eq, Filter.map_fst_prod
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : CompleteSpace (α × β)
h : Nonempty α
f : Filter β
hf : Cauchy f
x a : α
b : β
hab : SProd.sprod (α := Filter α) (pure x) f ≤ 𝓝 (a, b)
⊢ f ≤ 𝓝 b

Tactic:
simpa only [map_snd_prod, nhds_prod_eq] using map_mono (m := Prod.snd) hab

Premises used: Filter.map_snd_prod, Filter.map_mono, nhds_prod_eq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : UniformSpace β
inst_1 : Nonempty α
inst_2 : Nonempty β
⊢ CompleteSpace (α × β) ↔ CompleteSpace α ∧ CompleteSpace β

Tactic:
⟨fun _ ↦ ⟨.fst_of_prod (β := β), .snd_of_prod (α := α)⟩, fun ⟨_, _⟩ ↦ .prod⟩

Premises used: CompleteSpace, CompleteSpace.prod, And.intro, Iff.intro, CompleteSpace.fst_of_prod, Prod, _private.0.completeSpace_prod_of_nonempty.match_1, CompleteSpace.snd_of_prod
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
h : IsComplete.{u} (α := α) univ
⊢ CompleteSpace α

Tactic:
⟨fun hf => let ⟨x, _, hx⟩ := h _ hf ((@principal_univ α).symm ▸ le_top); ⟨x, hx⟩⟩

Premises used: Exists, nhds, Filter.principal_univ, Eq.rec, CompleteSpace.mk, LE.le, le_top, Exists.intro, _private.0.completeSpace_of_isComplete_univ.match_1, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
⊢ CompleteSpace α ↔ IsComplete.{u} (α := α) univ

Tactic:
⟨@complete_univ α _, completeSpace_of_isComplete_univ⟩

Premises used: complete_univ, completeSpace_of_isComplete_univ, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
⊢ CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → ∃ (x : α), (↑l : Filter α) ≤ 𝓝 x

Tactic:
simp [completeSpace_iff_isComplete_univ, isComplete_iff_ultrafilter]

Premises used: isComplete_iff_ultrafilter, completeSpace_iff_isComplete_univ
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
l : Filter α
inst_1 : l.NeBot
⊢ Cauchy l ↔ ∃ (x : α), l ≤ 𝓝 x

Tactic:
⟨CompleteSpace.complete, fun ⟨_, hx⟩ => cauchy_nhds.mono hx⟩

Premises used: Cauchy, Cauchy.mono, _private.0.cauchy_iff_exists_le_nhds.match_1, CompleteSpace.complete, Iff.intro, cauchy_nhds
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : CompleteSpace α
l : Filter β
f : β → α
inst_1 : l.NeBot
⊢ Cauchy (map f l) ↔ ∃ (x : α), Tendsto f l (𝓝 x)

Tactic:
cauchy_iff_exists_le_nhds

Premises used: cauchy_iff_exists_le_nhds, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Preorder β
inst_1 : CompleteSpace α
u : β → α
H : CauchySeq u
⊢ ∃ (x : α), Tendsto u atTop (𝓝 x)

Tactic:
CompleteSpace.complete H

Premises used: Filter.Tendsto, CompleteSpace.complete
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
rwa : range u ⊆ K
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (y : β), u y ∈ K
⊢ u '' univ ⊆ K

Tactic:
rwa [image_univ, range_subset_iff]

Premises used: Set.image_univ, Set.range_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
f : Filter α
hf : Cauchy f
⊢ f ≤ 𝓝 f.lim

Tactic:
_root_.le_nhds_lim (CompleteSpace.complete hf)

Premises used: Set.Mem, le_nhds_lim, CompleteSpace.complete
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : Preorder β
inst_1 : CompleteSpace α
u : β → α
h : CauchySeq u
⊢ Tendsto u atTop (𝓝 (limUnder atTop u))

Tactic:
h.le_nhds_lim

Premises used: Set.Mem, Cauchy.le_nhds_lim, Filter.Tendsto, Filter.limUnder
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : CompleteSpace α
s : Set α
h : IsClosed[uniformSpace.toTopologicalSpace] s
⊢ IsComplete s

Tactic:
fun _ cf fs =>
  let ⟨x, hx⟩ := CompleteSpace.complete cf
  ⟨x, isClosed_iff_clusterPt.mp h x (cf.left.mono (le_inf hx fs)), hx⟩

Premises used: IsComplete, Filter.NeBot.mono, Membership.mem, Exists, nhds, LE.le, _private.0.cauchy_iff_exists_le_nhds.match_1, le_inf, And, And.left, CompleteSpace.complete, isClosed_iff_clusterPt, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
hf : Cauchy f
⊢ f.NeBot

Tactic:
rcases hf with ⟨f_ne_bot, f_le⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
hf : Cauchy f
f_ne_bot : f.NeBot
⊢ f ×ˢ f ≤ 𝓤 α

Tactic:
rcases hf with ⟨f_ne_bot, f_le⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
f_le : f ×ˢ f ≤ 𝓤 α
⊢ ∃ t₁ ∈ f, ∃ t₂ ∈ f, t₁ ×ˢ t₂ ⊆ SetRel.id

Tactic:
simp only [DiscreteUniformity.eq_principal_setRelId, le_principal_iff, mem_prod_iff] at f_le

Premises used: Filter.le_principal_iff, DiscreteUniformity.eq_principal_setRelId, Filter.mem_prod_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
f_le : ∃ t₁ ∈ f, ∃ t₂ ∈ f, t₁ ×ˢ t₂ ⊆ SetRel.id
obtain : ∀ (S : Set α) (hS : S ∈ f) (T : Set α) (hT : T ∈ f) (H : S ×ˢ T ⊆ SetRel.id), ∃ (x : α), f = pure x
⊢ ∃ (x : α), f = pure x

Tactic:
obtain ⟨S, hS, T, hT, H⟩ := f_le
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
S : Set α
hS : S ∈ f
T : Set α
hT : T ∈ f
H : S ×ˢ T ⊆ SetRel.id
obtain :
  ∀ (x : α) (hS hT : {x} ∈ f) (H : SProd.sprod (α := Set α) (β := Set α) {x} {x} ⊆ SetRel.id), ∃ (x : α), f = pure x
⊢ ∃ (x : α), f = pure x

Tactic:
obtain ⟨x, rfl, _, _, _⟩ := SetRel.exists_eq_singleton_of_prod_subset_id
    (f_ne_bot.nonempty_of_mem hS) (f_ne_bot.nonempty_of_mem hT) H

Premises used: SetRel.exists_eq_singleton_of_prod_subset_id, Filter.NeBot.nonempty_of_mem, rfl
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
x : α
hS hT : {x} ∈ f
H : SProd.sprod (α := Set α) (β := Set α) {x} {x} ⊆ SetRel.id
⊢ ∃ (x : α), f = pure x

Tactic:
⟨x, f_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩

Premises used: Iff.mpr, Filter.le_pure_iff, Filter.NeBot.le_pure_iff, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
x : α
hS hT : {x} ∈ f
H : SProd.sprod (α := Set α) (β := Set α) {x} {x} ⊆ SetRel.id
⊢ ∃ (x : α), f = pure x

Tactic:
exact ⟨x, f_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
hf : Cauchy f
obtain : ∀ (x : α) (hf : Cauchy (pure x)), ∃ (x_1 : α), pure x ≤ 𝓝 x_1
⊢ ∃ (x : α), f ≤ 𝓝 x

Tactic:
obtain ⟨x, rfl⟩ := eq_pure_of_cauchy hf

Premises used: DiscreteUniformity.eq_pure_of_cauchy, rfl
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
x : α
hf : Cauchy (pure x)
⊢ ∃ (x_1 : α), pure x ≤ 𝓝 x_1

Tactic:
⟨x, pure_le_nhds x⟩

Premises used: pure_le_nhds, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
x : α
hf : Cauchy (pure x)
⊢ ∃ (x_1 : α), pure x ≤ 𝓝 x_1

Tactic:
exact ⟨x, pure_le_nhds x⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : DiscreteUniformity α
f : Filter α
hf : Cauchy f
⊢ f = pure (cauchyConst hf)

Tactic:
(eq_pure_of_cauchy hf).choose_spec

Premises used: DiscreteUniformity.eq_pure_of_cauchy, Exists.choose_spec, Set.Mem, setOf, DiscreteUniformity.cauchyConst
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ (𝓟 s).TotallyBounded ↔ TotallyBounded s

Tactic:
simp only [Filter.TotallyBounded, mem_principal, SetRel.preimage_eq_biUnion, TotallyBounded]

Premises used: TotallyBounded, SetRel.preimage_eq_biUnion, Filter.mem_principal, Filter.TotallyBounded
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
rcases :
  ∀ (r : Set (α × α)) (hr : r ∈ 𝓤 α) (rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r) (rU : r ○ r ⊆ U),
    ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
rcases comp_symm_of_uniformity hU with ⟨r, hr, rs, rU⟩

Premises used: comp_symm_of_uniformity
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
rcases : ∀ (k : Set α) (fk : k.Finite) (ks : SetRel.preimage r k ∈ f), ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
rcases hf r hr with ⟨k, fk, ks⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
choose :
  ∀ (g : (x : (↑u : Type u)) → α) (hgs : ∀ (x : (↑u : Type u)), g x ∈ s)
    (hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r), ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
choose g hgs hgr using fun x : u => x.coe_prop.2

Premises used: Subtype.coe_prop, And.right
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
⟨range g, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Set.range
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
refine_1 : range g ⊆ s
refine_2 : (range g).Finite
refine_3 : U.preimage (range g) ∈ f
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
refine ⟨range g, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
⊢ range g ⊆ s

Tactic:
range_subset_iff.2 hgs

Premises used: Iff.mpr, Set.range_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
⊢ range g ⊆ s

Tactic:
exact range_subset_iff.2 hgs

Premises used: Iff.mpr, Set.range_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
refine_2 : ∀ (this : Fintype (↑u : Type u)), (range g).Finite
⊢ (range g).Finite

Tactic:
haveI : Fintype u := (fk.inter_of_left _).fintype
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
this : Fintype (↑u : Type u)
⊢ (range g).Finite

Tactic:
finite_range g

Premises used: Set.finite_range
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
this : Fintype (↑u : Type u)
⊢ (range g).Finite

Tactic:
exact finite_range g

Premises used: Set.finite_range
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
x : α
xs : x ∈ s
h : ∀ (y : α) (hy : y ∈ k) (xy : (x, y) ∈ r), x ∈ U.preimage (range g)
⊢ x ∈ SetRel.preimage r k → x ∈ U.preimage (range g)

Tactic:
⟨y, hy, xy⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
h : ∀ (x : α) (xs : x ∈ s) (y : α) (hy : y ∈ k) (xy : (x, y) ∈ r), x ∈ U.preimage (range g)
⊢ U.preimage (range g) ∈ f

Tactic:
filter_upwards [hs, ks] with x xs ⟨y, hy, xy⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
r : Set (α × α)
hr : r ∈ 𝓤 α
rs : ∀ {a b : α}, (a, b) ∈ r → (b, a) ∈ r
rU : r ○ r ⊆ U
k : Set α
fk : k.Finite
ks : SetRel.preimage r k ∈ f
u : Set α := k ∩ {y : α | ∃ x ∈ s, (x, y) ∈ r}
g : (x : (↑u : Type u)) → α
hgs : ∀ (x : (↑u : Type u)), g x ∈ s
hgr : ∀ (x : (↑u : Type u)), (g x, (↑x : α)) ∈ r
x : α
xs : x ∈ s
y : α
hy : y ∈ k
xy : (x, y) ∈ r
h : Membership.mem (γ := Set α) {a : α | ∃ (i : (↑u : Type u)), (a, g i) ∈ U} x
⊢ x ∈ U.preimage (range g)

Tactic:
simp_rw [SetRel.preimage, exists_range_iff]

Premises used: Set.exists_range_iff, SetRel.preimage