awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
⊢ interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)

Tactic:
have h_subset : interUnionBalls xs u U
      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
    fun x hx ↦ Set.mem_iInter.1 hx i
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
⊢ ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}

Tactic:
⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩

Premises used: Finset.range, SetLike.coe, HAdd.hAdd, And.intro, Exists.intro, Finset.finite_toSet, OfNat.ofNat, Finset.image
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
refine :
  ∀ (x : α) (hx : x ∈ interUnionBalls xs u U),
    Membership.mem (γ := Set α) (⋃ y ∈ (↑(Finset.image xs (Finset.range (u i + 1))) : Set α), {x : α | (x, y) ∈ U i}) x
⊢ ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}

Tactic:
refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
simp : Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : y ≤ u i), {x : α | (x, xs y) ∈ U i}) x
⊢ Membership.mem (γ := Set α) (⋃ y ∈ (↑(Finset.image xs (Finset.range (u i + 1))) : Set α), {x : α | (x, y) ∈ U i}) x

Tactic:
simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]

Premises used: Set.iUnion_iUnion_eq_right, Set.mem_Iio, Finset.coe_range, Set.mem_image, Finset.coe_image, Nat.lt_succ_iff, Set.iUnion_exists, Set.biUnion_and'
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : y ≤ u i), {x : α | (x, xs y) ∈ U i}) x

Tactic:
h_subset hx

Premises used: Set.Mem, setOf, UniformSpace.ball, Set.preimage, Prod.swap
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : y ≤ u i), {x : α | (x, xs y) ∈ U i}) x

Tactic:
exact h_subset hx
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
refine :
  ∀ (x : α) (hx : x ∈ interUnionBalls xs u U),
    Membership.mem (γ := Set α) (⋃ y ∈ (↑(Finset.image xs (Finset.range (u i + 1))) : Set α), {x : α | (x, y) ∈ U i}) x
refine₁ :
  ∀ (x : α) (hx : x ∈ interUnionBalls xs u U),
    Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : y ≤ u i), {x : α | (x, xs y) ∈ U i}) x
⊢ ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}

Tactic:
classical
  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
  exact h_subset hx

Premises used: Set.iUnion_iUnion_eq_right, Set.mem_Iio, Finset.coe_range, Set.mem_image, Finset.coe_image, Nat.lt_succ_iff, Set.iUnion_exists, Set.biUnion_and'
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
rw :
  TotallyBounded (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U)) ∧
    IsComplete (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))
⊢ IsCompact (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))

Tactic:
rw [isCompact_iff_totallyBounded_isComplete]

Premises used: isCompact_iff_totallyBounded_isComplete
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U)) ∧
    IsComplete (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))

Tactic:
⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩

Premises used: And.intro, TotallyBounded.closure, IsClosed.isComplete, isClosed_closure
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
refine : TotallyBounded (interUnionBalls xs u U)
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U)) ∧
    IsComplete (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))

Tactic:
refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)

Tactic:
totallyBounded_interUnionBalls H xs u

Premises used: totallyBounded_interUnionBalls
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)

Tactic:
exact totallyBounded_interUnionBalls H xs u

Premises used: totallyBounded_interUnionBalls
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
n : ℕ
⊢ setSeq hf (U := U) U_mem n ∈ f

Tactic:
(biInter_mem (finite_le_nat n)).2 fun m _ => (setSeqAux hf U_mem m).2.1

Premises used: Iff.mpr, Set.Mem, setOf, SequentiallyComplete.setSeq, And.left, SequentiallyComplete.setSeqAux, Filter.biInter_mem, Set.Iic, Subtype.property, Set.finite_le_nat
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
m n : ℕ
h : m ≤ n
⊢ setSeq hf (U := U) U_mem n ⊆ setSeq hf (U := U) U_mem m

Tactic:
biInter_subset_biInter_left <| Iic_subset_Iic.2 h

Premises used: Iff.mpr, Set.Iic_subset_Iic, SequentiallyComplete.setSeq, Set.biInter_subset_biInter_left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
n : ℕ
⊢ setSeq hf (U := U) U_mem n ⊆ (↑(setSeqAux hf (U := U) U_mem n) : Set α)

Tactic:
biInter_subset_of_mem self_mem_Iic

Premises used: Set.self_mem_Iic, Set.biInter_subset_of_mem, SequentiallyComplete.setSeq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
⊢ p ∈ U N

Tactic:
(setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩

Premises used: And.right, And.intro, SequentiallyComplete.setSeqAux, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
refine_1 : p.1 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)
refine_2 : p.2 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)
⊢ p ∈ U N

Tactic:
refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩

Premises used: And.right, And.intro, SequentiallyComplete.setSeqAux, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
refine_1 : p.1 ∈ setSeq hf (U := U) U_mem N
⊢ p.1 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)

Tactic:
apply setSeq_sub_aux

Premises used: SequentiallyComplete.setSeq_sub_aux
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
refine_2 : p.2 ∈ setSeq hf (U := U) U_mem N
⊢ p.2 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)

Tactic:
apply setSeq_sub_aux

Premises used: SequentiallyComplete.setSeq_sub_aux
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
⊢ p.1 ∈ setSeq hf (U := U) U_mem N

Tactic:
setSeq_mono hf U_mem hm hp.1

Premises used: SequentiallyComplete.setSeq_mono, And.left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
⊢ p.1 ∈ setSeq hf (U := U) U_mem N

Tactic:
exact setSeq_mono hf U_mem hm hp.1

Premises used: SequentiallyComplete.setSeq_mono, And.left
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
⊢ p.2 ∈ setSeq hf (U := U) U_mem N

Tactic:
setSeq_mono hf U_mem hn hp.2

Premises used: SequentiallyComplete.setSeq_mono, And.right
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
⊢ p.2 ∈ setSeq hf (U := U) U_mem N

Tactic:
exact setSeq_mono hf U_mem hn hp.2

Premises used: SequentiallyComplete.setSeq_mono, And.right
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
n : ℕ
⊢ seq hf (U := U) U_mem n ∈ setSeq hf (U := U) U_mem n

Tactic:
(hf.1.nonempty_of_mem (setSeq_mem hf U_mem n)).choose_spec

Premises used: Exists.choose_spec, Set.Mem, SequentiallyComplete.setSeq_mem, And.left, Filter.NeBot.nonempty_of_mem, SequentiallyComplete.seq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ (seq hf (U := U) U_mem m, seq hf (U := U) U_mem n) ∈ U N

Tactic:
setSeq_prod_subset hf U_mem hm hn ⟨seq_mem hf U_mem m, seq_mem hf U_mem n⟩

Premises used: SequentiallyComplete.seq_mem, And.intro, SequentiallyComplete.setSeq_prod_subset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
⊢ CauchySeq (seq hf (U := U) U_mem)

Tactic:
cauchySeq_of_controlled U U_le <| seq_pair_mem hf U_mem

Premises used: SequentiallyComplete.seq_pair_mem, cauchySeq_of_controlled
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
rcases : ∀ (m : ℕ) (hm : U m ⊆ s), ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t

Tactic:
rcases U_le s hs with ⟨m, hm⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
rcases :
  ∀ (n : ℕ) (hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)),
    ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t

Tactic:
rcases tendsto_atTop'.1 ha _ (mem_nhds_left a (U_mem m)) with ⟨n, hn⟩

Premises used: mem_nhds_left, Iff.mp, Filter.tendsto_atTop'
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t

Tactic:
⟨setSeq hf U_mem (max m n), setSeq_mem hf U_mem _, ?_, seq hf U_mem (max m n), ?_,
          seq_mem hf U_mem _⟩

Premises used: SequentiallyComplete.seq_mem, SequentiallyComplete.setSeq_mem, SequentiallyComplete.setSeq, Max.max, And.intro, Exists.intro, SequentiallyComplete.seq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
refine_1 : setSeq hf (U := U) U_mem (max m n) ×ˢ setSeq hf (U := U) U_mem (max m n) ⊆ s
refine_2 : (a, seq hf (U := U) U_mem (max m n)) ∈ s
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t

Tactic:
refine
        ⟨setSeq hf U_mem (max m n), setSeq_mem hf U_mem _, ?_, seq hf U_mem (max m n), ?_,
          seq_mem hf U_mem _⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
⊢ m ≤ max m n

Tactic:
have := le_max_left m n
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
this : m ≤ max m n
⊢ setSeq hf (U := U) U_mem (max m n) ×ˢ setSeq hf (U := U) U_mem (max m n) ⊆ s

Tactic:
Set.Subset.trans (setSeq_prod_subset hf U_mem this this) hm

Premises used: Set.Subset.trans, SequentiallyComplete.setSeq_prod_subset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
this : m ≤ max m n
⊢ setSeq hf (U := U) U_mem (max m n) ×ˢ setSeq hf (U := U) U_mem (max m n) ⊆ s

Tactic:
exact Set.Subset.trans (setSeq_prod_subset hf U_mem this this) hm

Premises used: Set.Subset.trans, SequentiallyComplete.setSeq_prod_subset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
⊢ (a, seq hf (U := U) U_mem (max m n)) ∈ s

Tactic:
hm (hn _ <| le_max_right m n)

Premises used: le_max_right
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
⊢ (a, seq hf (U := U) U_mem (max m n)) ∈ s

Tactic:
exact hm (hn _ <| le_max_right m n)

Premises used: le_max_right
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
obtain : ∀ (U' : ℕ → Set (α × α)) (hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s), CompleteSpace α
⊢ CompleteSpace α

Tactic:
obtain ⟨U', -, hU'⟩ := (𝓤 α).exists_antitone_seq

Premises used: uniformity, Filter.exists_antitone_seq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
⊢ ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α

Tactic:
have Hmem : ∀ n, U n ∩ U' n ∈ 𝓤 α := fun n => inter_mem (U_mem n) (hU'.2 ⟨n, Subset.refl _⟩)
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
⊢ CompleteSpace α

Tactic:
⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
    le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩

Premises used: CompleteSpace.mk, Exists.imp, SequentiallyComplete.le_nhds_of_seq_tendsto_nhds, SequentiallyComplete.seq
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
refine_1 :
  ∀ {f : Filter α} (hf : Cauchy f) (N m n : ℕ) (hm : N ≤ m) (hn : N ≤ n),
    (SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem m,
        SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem n) ∈
      U N
refine_2 : ∀ {f : Filter α} (hf : Cauchy f) (s : Set (α × α)) (hs : s ∈ 𝓤 α), ∃ (n : ℕ), U n ∩ U' n ⊆ s
⊢ CompleteSpace α

Tactic:
refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
    le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f : Filter α
hf : Cauchy f
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ (SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem m,
      SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem n) ∈
    U N

Tactic:
inter_subset_left (seq_pair_mem hf Hmem hm hn)

Premises used: Set.inter_subset_left, SequentiallyComplete.seq_pair_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f : Filter α
hf : Cauchy f
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ (SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem m,
      SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem n) ∈
    U N

Tactic:
exact inter_subset_left (seq_pair_mem hf Hmem hm hn)

Premises used: Set.inter_subset_left, SequentiallyComplete.seq_pair_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f : Filter α
hf : Cauchy f
s : Set (α × α)
hs : s ∈ 𝓤 α
refine_2 : ∀ (N : ℕ) (hN : U' N ⊆ s), ∃ (n : ℕ), U n ∩ U' n ⊆ s
⊢ ∃ (n : ℕ), U n ∩ U' n ⊆ s

Tactic:
rcases hU'.1 hs with ⟨N, hN⟩

Premises used: Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f : Filter α
hf : Cauchy f
s : Set (α × α)
hs : s ∈ 𝓤 α
N : ℕ
hN : U' N ⊆ s
⊢ ∃ (n : ℕ), U n ∩ U' n ⊆ s

Tactic:
⟨N, Subset.trans inter_subset_right hN⟩

Premises used: Set.Subset.trans, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f : Filter α
hf : Cauchy f
s : Set (α × α)
hs : s ∈ 𝓤 α
N : ℕ
hN : U' N ⊆ s
⊢ ∃ (n : ℕ), U n ∩ U' n ⊆ s

Tactic:
exact ⟨N, Subset.trans inter_subset_right hN⟩