awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : CauchySeq u
⊢ CauchySeq.{u, 0} (α := α) fun (n : ℕ) ↦ u (n + k)

Tactic:
exact h.comp_tendsto (tendsto_add_atTop_nat k)

Premises used: Filter.tendsto_add_atTop_nat, CauchySeq.comp_tendsto
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
rw :
  Tendsto (Prod.map u u) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
rw [cauchySeq_iff_tendsto, ← prod_atTop_atTop_eq]

Premises used: Filter.prod_atTop_atTop_eq, cauchySeq_iff_tendsto
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ Tendsto (Prod.map u u) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
(atTop_basis.prod_self.tendsto_iff h).trans ?_

Premises used: Filter.atTop_basis, Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod_self, Iff.trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
refine :
  (∀ (ib : γ), p ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia ×ˢ Ici ia, Prod.map u u x ∈ s ib) ↔
    ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
⊢ Tendsto (Prod.map u u) (SProd.sprod (α := Filter β) (β := Filter β) atTop atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
refine (atTop_basis.prod_self.tendsto_iff h).trans ?_

Premises used: Filter.atTop_basis, Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod_self, Iff.trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ (∀ (ib : γ), p ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia ×ˢ Ici ia, Prod.map u u x ∈ s ib) ↔
    ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
simp only [true_and, Prod.forall, mem_prod_eq,
    mem_Ici, and_imp, Prod.map, @forall_comm (_ ≤ _) β]

Premises used: Set.mem_prod_eq, and_imp, forall_comm, Prod.map, Set.mem_Ici, Prod.forall, true_and
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i

Tactic:
H.cauchySeq_iff.trans ⟨fun h i hi => ?_, fun h i hi => ?_⟩

Premises used: Filter.HasBasis.cauchySeq_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
refine_1 :
  ∀ (h : ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i) (i : γ) (hi : p i),
    ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
refine_2 :
  ∀ (h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i) (i : γ) (hi : p i),
    ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
⊢ CauchySeq u ↔ ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i

Tactic:
refine H.cauchySeq_iff.trans ⟨fun h i hi => ?_, fun h i hi => ?_⟩

Premises used: Filter.HasBasis.cauchySeq_iff, Iff.intro, Iff.trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
i : γ
hi : p i
⊢ ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i

Tactic:
(h i hi).imp fun N hN n hn => hN n hn N le_rfl

Premises used: Exists.imp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
i : γ
hi : p i
⊢ ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i

Tactic:
exact (h i hi).imp fun N hN n hn => hN n hn N le_rfl

Premises used: Exists.imp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
refine_2 :
  ∀ (t : Set (α × α)) (ht : t ∈ 𝓤 α) (ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) (hts : t ○ t ⊆ s i),
    ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
rcases comp_symm_of_uniformity (H.mem_of_mem hi) with ⟨t, ht, ht', hts⟩

Premises used: comp_symm_of_uniformity, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
refine_2 : ∀ (j : γ) (hj : p j) (hjt : s j ⊆ t), ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
rcases H.mem_iff.1 ht with ⟨j, hj, hjt⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
(h j hj).imp fun N hN m hm n hn => hts ⟨u N, hjt ?_, ht' <| hjt ?_⟩

Premises used: Exists.imp, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
refine_2 : ∀ (N : β) (hN : ∀ n ≥ N, (u n, u N) ∈ s j) (m : β) (hm : N ≤ m) (n : β) (hn : N ≤ n), (u m, u N) ∈ s j
refine_2₁ : ∀ (N : β) (hN : ∀ n ≥ N, (u n, u N) ∈ s j) (m : β) (hm : N ≤ m) (n : β) (hn : N ≤ n), (u n, u N) ∈ s j
⊢ ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
refine (h j hj).imp fun N hN m hm n hn => hts ⟨u N, hjt ?_, ht' <| hjt ?_⟩

Premises used: Exists.imp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
N : β
hN : ∀ n ≥ N, (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ (u m, u N) ∈ s j

Tactic:
hN m hm
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
N : β
hN : ∀ n ≥ N, (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ (u n, u N) ∈ s j

Tactic:
hN n hn
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst : Nonempty β
inst_1 : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
H : (𝓤 α).HasBasis p s
h : ∀ (i : γ), p i → ∃ (N : β), ∀ n ≥ N, (u n, u N) ∈ s i
i : γ
hi : p i
t : Set (α × α)
ht : t ∈ 𝓤 α
ht' : ∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t
hts : t ○ t ⊆ s i
j : γ
hj : p j
hjt : s j ⊆ t
N : β
hN : ∀ n ≥ N, (u n, u N) ∈ s j
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ (u m, u N) ∈ s j

Tactic:
exacts [hN m hm, hN n hn]
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ (n : β), U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
rw : ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s
⊢ s ∈ map (Prod.map f f) atTop

Tactic:
rw [mem_map, mem_atTop_sets]

Premises used: Filter.mem_atTop_sets, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ (n : β), U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
obtain : ∀ (N : β) (hN : U N ⊆ s), ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s
⊢ ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s

Tactic:
obtain ⟨N, hN⟩ := hU s hs
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ (n : β), U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
⊢ ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s

Tactic:
⟨(N, N), fun mn hmn => ?_⟩

Premises used: Prod.mk, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ (n : β), U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
refine : ∀ (mn : β × β) (hmn : mn ≥ (N, N)), mn ∈ Prod.map f f ⁻¹' s
⊢ ∃ (a : β × β), ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s

Tactic:
refine ⟨(N, N), fun mn hmn => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ (n : β), U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
mn : β × β
hmn : mn ≥ (N, N)
obtain : ∀ (m n : β) (hmn : (m, n) ≥ (N, N)), (m, n) ∈ Prod.map f f ⁻¹' s
⊢ mn ∈ Prod.map f f ⁻¹' s

Tactic:
obtain ⟨m, n⟩ := mn
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ (n : β), U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
m n : β
hmn : (m, n) ≥ (N, N)
⊢ (m, n) ∈ Prod.map f f ⁻¹' s

Tactic:
hN (hf hmn.1 hmn.2)

Premises used: Set.Mem, setOf, And.right, Set.preimage, And.left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : SemilatticeSup β
inst_1 : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ (n : β), U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
m n : β
hmn : (m, n) ≥ (N, N)
⊢ (m, n) ∈ Prod.map f f ⁻¹' s

Tactic:
exact hN (hf hmn.1 hmn.2)

Premises used: And.right, And.left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ IsComplete s ↔ ∀ (l : Filter α), Cauchy l → l ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x l

Tactic:
forall₃_congr fun _ hl _ => exists_congr fun _ => and_congr_right fun _ =>
    le_nhds_iff_adhp_of_cauchy hl

Premises used: le_nhds_iff_adhp_of_cauchy, IsComplete, forall₃_congr, and_congr_right, exists_congr
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x

Tactic:
⟨fun h l => h l, fun H => isComplete_iff_clusterPt.2 fun l hl hls => ?_⟩

Premises used: Iff.mpr, isComplete_iff_clusterPt, Iff.intro, Ultrafilter.toFilter
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
refine :
  ∀ (H : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x)
    (l : Filter α) (hl : Cauchy l) (hls : l ≤ 𝓟 s), ∃ x ∈ s, ClusterPt x l
⊢ IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x

Tactic:
refine ⟨fun h l => h l, fun H => isComplete_iff_clusterPt.2 fun l hl hls => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
⊢ l.NeBot

Tactic:
haveI := hl.1
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
rcases : ∀ (x : α) (hxs : x ∈ s) (hxl : (↑(Ultrafilter.of l) : Filter α) ≤ 𝓝 x), ∃ x ∈ s, ClusterPt x l
⊢ ∃ x ∈ s, ClusterPt x l

Tactic:
rcases H (Ultrafilter.of l) hl.ultrafilter_of ((Ultrafilter.of_le l).trans hls) with ⟨x, hxs, hxl⟩

Premises used: Ultrafilter.of_le, Cauchy.ultrafilter_of, Ultrafilter.of, LE.le.trans
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
x : α
hxs : x ∈ s
hxl : (↑(Ultrafilter.of l) : Filter α) ≤ 𝓝 x
⊢ ∃ x ∈ s, ClusterPt x l

Tactic:
⟨x, hxs, (ClusterPt.of_le_nhds hxl).mono (Ultrafilter.of_le l)⟩

Premises used: ClusterPt.mono, ClusterPt.of_le_nhds, Ultrafilter.of_le, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
H : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
l : Filter α
hl : Cauchy l
hls : l ≤ 𝓟 s
this : l.NeBot
x : α
hxs : x ∈ s
hxl : (↑(Ultrafilter.of l) : Filter α) ≤ 𝓝 x
⊢ ∃ x ∈ s, ClusterPt x l

Tactic:
exact ⟨x, hxs, (ClusterPt.of_le_nhds hxl).mono (Ultrafilter.of_le l)⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ (∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → (↑l : Filter α) ≤ 𝓟 s → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x) ↔
    ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → s ∈ l → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x

Tactic:
simp only [le_principal_iff, Ultrafilter.mem_coe]

Premises used: Filter.le_principal_iff, Ultrafilter.mem_coe
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : IsComplete s
ht : IsComplete t
simp :
  ∀ (hs : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → s ∈ l → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x)
    (ht : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → t ∈ l → ∃ x ∈ t, (↑l : Filter α) ≤ 𝓝 x) (l : Ultrafilter α),
    Cauchy (↑l : Filter α) → (s ∈ l → ∃ x ∈ s ∪ t, (↑l : Filter α) ≤ 𝓝 x) ∧ (t ∈ l → ∃ x ∈ s ∪ t, (↑l : Filter α) ≤ 𝓝 x)
⊢ IsComplete (s ∪ t)

Tactic:
simp only [isComplete_iff_ultrafilter', Ultrafilter.union_mem_iff, or_imp] at *

Premises used: Ultrafilter.union_mem_iff, or_imp, isComplete_iff_ultrafilter'
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → s ∈ l → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
ht : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → t ∈ l → ∃ x ∈ t, (↑l : Filter α) ≤ 𝓝 x
⊢ ∀ (l : Ultrafilter α),
    Cauchy (↑l : Filter α) → (s ∈ l → ∃ x ∈ s ∪ t, (↑l : Filter α) ≤ 𝓝 x) ∧ (t ∈ l → ∃ x ∈ s ∪ t, (↑l : Filter α) ≤ 𝓝 x)

Tactic:
fun l hl =>
    ⟨fun hsl => (hs l hl hsl).imp fun x hx => ⟨Or.inl hx.1, hx.2⟩, fun htl =>
      (ht l hl htl).imp fun x hx => ⟨Or.inr hx.1, hx.2⟩⟩

Premises used: Exists.imp, And.intro, Or.inl, Or.inr
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
s t : Set α
hs : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → s ∈ l → ∃ x ∈ s, (↑l : Filter α) ≤ 𝓝 x
ht : ∀ (l : Ultrafilter α), Cauchy (↑l : Filter α) → t ∈ l → ∃ x ∈ t, (↑l : Filter α) ≤ 𝓝 x
⊢ ∀ (l : Ultrafilter α),
    Cauchy (↑l : Filter α) → (s ∈ l → ∃ x ∈ s ∪ t, (↑l : Filter α) ≤ 𝓝 x) ∧ (t ∈ l → ∃ x ∈ s ∪ t, (↑l : Filter α) ≤ 𝓝 x)

Tactic:
exact fun l hl =>
    ⟨fun hsl => (hs l hl hsl).imp fun x hx => ⟨Or.inl hx.1, hx.2⟩, fun htl =>
      (ht l hl htl).imp fun x hx => ⟨Or.inr hx.1, hx.2⟩⟩
-- 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
set :
  let S : Set α := ⋃ (i : ι), s i;
  IsComplete S
⊢ IsComplete.{u} (α := α) (⋃ (i : ι), s i)

Tactic:
set S := ⋃ i, s i
-- 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 : l ≤ 𝓟 S
⊢ S ∈ l

Tactic:
rw [le_principal_iff] at hls

Premises used: Filter.le_principal_iff
-- 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
⊢ l.NeBot

Tactic:
obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl

Premises used: cauchy_iff, 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
⊢ ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s

Tactic:
obtain ⟨hl_ne, hl'⟩ := cauchy_iff.1 hl

Premises used: cauchy_iff, 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
rcases : ∀ (t : Set α) (htl : t ∈ l) (htU : t ×ˢ t ⊆ U), ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U
⊢ ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U

Tactic:
rcases hl' U hU with ⟨t, htl, htU⟩
-- 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 α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U

Tactic:
⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩

Premises used: Set.Subset.trans, Filter.inter_mem, Inter.inter, And.intro, Exists.intro, Set.inter_subset_right
-- 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 α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
refine : (t ∩ S) ×ˢ (t ∩ S) ⊆ t ×ˢ t
⊢ ∃ t ⊆ S, t ∈ l ∧ t ×ˢ t ⊆ U

Tactic:
refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
-- 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 α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
hs₁ ht : t ∩ S ⊆ t
⊢ (t ∩ S) ×ˢ (t ∩ S) ⊆ t ×ˢ t

Tactic:
gcongr
-- 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 α
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ t ∩ S ⊆ t

Tactic:
apply inter_subset_left

Premises used: Set.inter_subset_left
-- 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
obtain : ∀ (t : Set α) (htS : t ⊆ S) (htl : t ∈ l) (htU : t ×ˢ t ⊆ U), ∃ x ∈ S, l ≤ 𝓝 x
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
obtain ⟨t, htS, htl, htU⟩ : ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U := by
    rcases hl' U hU with ⟨t, htl, htU⟩
    refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
    gcongr <;> apply inter_subset_left
-- 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
rcases : ∀ (x : α) (hx : x ∈ t), ∃ (i : ι), t ⊆ s i
⊢ ∃ (i : ι), t ⊆ s i

Tactic:
rcases Filter.nonempty_of_mem htl with ⟨x, hx⟩

Premises used: Filter.nonempty_of_mem
-- 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
rcases : ∀ (i : ι) (hi : x ∈ s i), ∃ (i : ι), t ⊆ s i
⊢ ∃ (i : ι), t ⊆ s i

Tactic:
rcases mem_iUnion.1 (htS hx) with ⟨i, hi⟩

Premises used: Set.mem_iUnion, Iff.mp