awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
H' : ∀ (u : ℕ → α), CauchySeq u → ∃ (a : α), Tendsto u atTop (𝓝 a)
⊢ CompleteSpace α

Tactic:
let ⟨U', _, hU'⟩ := (𝓤 α).exists_antitone_seq
  complete_of_convergent_controlled_sequences U' (fun n => hU'.2 ⟨n, Subset.refl _⟩) fun u hu =>
    H' u <| cauchySeq_of_controlled U' (fun _ hs => hU'.1 hs) hu

Premises used: Iff.mpr, CompleteSpace, Set.Subset.refl, uniformity, _private.0.UniformSpace.complete_of_cauchySeq_tendsto.match_1, UniformSpace.complete_of_convergent_controlled_sequences, Exists.intro, Iff.mp, Filter.exists_antitone_seq, cauchySeq_of_controlled
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
a : α
rw : (Filter.comap (Prod.mk a) (𝓤 α)).IsCountablyGenerated
⊢ (𝓝 a).IsCountablyGenerated

Tactic:
rw [nhds_eq_comap_uniformity]

Premises used: nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
a : α
⊢ (Filter.comap (Prod.mk a) (𝓤 α)).IsCountablyGenerated

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
rcases : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
rcases exists_countable_dense α with ⟨s, hsc, hsd⟩

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
ℕ :
  ∀ (t : ℕ → SetRel α α) (hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm)
    (h_basis : (𝓤 α).HasAntitoneBasis t), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
obtain
    ⟨t : ℕ → SetRel α α, hto : ∀ i : ℕ, t i ∈ (𝓤 α).sets ∧ IsOpen (t i) ∧ (t i).IsSymm,
      h_basis : (𝓤 α).HasAntitoneBasis t⟩ :=
    (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis

Premises used: Filter.HasBasis.exists_antitone_subbasis, uniformity_hasBasis_open_symmetric
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
⊢ ∀ (i : ℕ), t i ∈ (𝓤 α).sets

Tactic:
choose ht_mem hto hts using hto
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
⊢ ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)

Tactic:
choose ht_mem hto hts using hto
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto₁ : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
⊢ ∀ (i : ℕ), (t i).IsSymm

Tactic:
choose ht_mem hto hts using hto
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ SecondCountableTopology α

Tactic:
⟨⟨⋃ x ∈ s, range fun k => ball x (t k), hsc.biUnion fun x _ => countable_range _, ?_⟩⟩

Premises used: Set.Countable.biUnion, SecondCountableTopology.mk, UniformSpace.ball, Set.countable_range, And.intro, Exists.intro, Set.range, Set.iUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
refine :
  Eq.{u + 1} (α := TopologicalSpace α) toTopologicalSpace (generateFrom (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)))
⊢ SecondCountableTopology α

Tactic:
refine ⟨⟨⋃ x ∈ s, range fun k => ball x (t k), hsc.biUnion fun x _ => countable_range _, ?_⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ Eq.{u + 1} (α := TopologicalSpace α) toTopologicalSpace (generateFrom (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)))

Tactic:
(isTopologicalBasis_of_isOpen_of_nhds ?_ ?_).eq_generateFrom

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
refine_1 :
  ∀ (u : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) u →
      IsOpen[uniformSpace.toTopologicalSpace] u
refine_2 :
  ∀ (a : α) (u : Set α),
    a ∈ u →
      IsOpen[uniformSpace.toTopologicalSpace] u →
        ∃ (v : Set α), Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) v ∧ a ∈ v ∧ v ⊆ u
⊢ Eq.{u + 1} (α := TopologicalSpace α) toTopologicalSpace (generateFrom (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)))

Tactic:
refine (isTopologicalBasis_of_isOpen_of_nhds ?_ ?_).eq_generateFrom

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, TopologicalSpace.IsTopologicalBasis.eq_generateFrom
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
refine_1 : ∀ (u : Set α), (∃ (i : α) (_ : i ∈ s) (y : ℕ), ball i (t y) = u) → IsOpen[uniformSpace.toTopologicalSpace] u
⊢ ∀ (u : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) u →
      IsOpen[uniformSpace.toTopologicalSpace] u

Tactic:
simp only [mem_iUnion₂, mem_range]

Premises used: Set.mem_range, Set.mem_iUnion₂
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
w : x ∈ s
k : ℕ
⊢ IsOpen[uniformSpace.toTopologicalSpace] (ball x (t k))

Tactic:
isOpen_ball x (hto k)

Premises used: UniformSpace.isOpen_ball
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
w : x ∈ s
k : ℕ
⊢ IsOpen[uniformSpace.toTopologicalSpace] (ball x (t k))

Tactic:
exact isOpen_ball x (hto k)

Premises used: UniformSpace.isOpen_ball
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
refine_2 : ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
⊢ ∃ (v : Set α), Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) v ∧ x ∈ v ∧ v ⊆ V

Tactic:
simp only [mem_iUnion₂, mem_range, exists_prop]

Premises used: Set.mem_range, exists_prop, Set.mem_iUnion₂
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
refine_2 :
  ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α) (hUV : ball x U ⊆ V),
    ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases UniformSpace.mem_nhds_iff.1 (IsOpen.mem_nhds hVo hxV) with ⟨U, hU, hUV⟩

Premises used: UniformSpace.mem_nhds_iff, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
refine_2 :
  ∀ (U' : Set (α × α)) (hU' : U' ∈ 𝓤 α),
    (∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U') →
      ∀ (hUU' : U' ○ U' ⊆ U), ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases comp_symm_of_uniformity hU with ⟨U', hU', _, hUU'⟩

Premises used: comp_symm_of_uniformity
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
refine_2 : ∀ (k : ℕ) (hk : t k ⊆ U'), ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases h_basis.toHasBasis.mem_iff.1 hU' with ⟨k, -, hk⟩

Premises used: Filter.HasBasis.mem_iff, Filter.HasAntitoneBasis.toHasBasis, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
refine_2 :
  ∀ (y : α) (hxy : y ∈ ball x (t k)) (hys : y ∈ s),
    ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases hsd.inter_open_nonempty (ball x <| t k) (isOpen_ball x (hto k))
        ⟨x, UniformSpace.mem_ball_self _ (ht_mem k)⟩ with
      ⟨y, hxy, hys⟩

Premises used: UniformSpace.isOpen_ball, UniformSpace.mem_ball_self, UniformSpace.ball, Dense.inter_open_nonempty, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
y : α
hxy : y ∈ ball x (t k)
hys : y ∈ s
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
⟨_, ⟨y, hys, k, rfl⟩, (t k).symm hxy, fun z hz => ?_⟩

Premises used: SetRel.symm, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
y : α
hxy : y ∈ ball x (t k)
hys : y ∈ s
refine_2 : ∀ (z : α) (hz : z ∈ ball y (t k)), z ∈ V
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
refine ⟨_, ⟨y, hys, k, rfl⟩, (t k).symm hxy, fun z hz => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
y : α
hxy : y ∈ ball x (t k)
hys : y ∈ s
z : α
hz : z ∈ ball y (t k)
⊢ z ∈ V

Tactic:
hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz))

Premises used: UniformSpace.ball_subset_of_comp_subset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
y : α
hxy : y ∈ ball x (t k)
hys : y ∈ s
z : α
hz : z ∈ ball y (t k)
⊢ z ∈ V

Tactic:
exact hUV (ball_subset_of_comp_subset (hk hxy) hUU' (hk hz))

Premises used: UniformSpace.ball_subset_of_comp_subset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
hs : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
obtain :
  ∀ (B : ℕ → SetRel α α) (hB : (𝓤 α).HasAntitoneBasis B),
    (∀ (n : ℕ), (B n).IsSymm) → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t

Tactic:
obtain ⟨B, hB, _⟩ := has_seq_basis α

Premises used: UniformSpace.has_seq_basis
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
hs : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right : ∀ (n : ℕ), (B n).IsSymm
⊢ ∀ (n : ℕ), ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x (B n)

Tactic:
replace hs (n : ℕ) := hs (B n) (hB.mem n)
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right : ∀ (n : ℕ), (B n).IsSymm
hs : ∀ (n : ℕ), ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x (B n)
choose :
  ∀ (t : (n : ℕ) → Set α) (tC : ∀ (n : ℕ), (t n).Countable) (ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)),
    ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t

Tactic:
choose t tC ht using hs
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right : ∀ (n : ℕ), (B n).IsSymm
t : (n : ℕ) → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
⊢ ∀ (n : ℕ), Countable.{u + 1} (↑(t n) : Type u)

Tactic:
have := fun n => (tC n).to_subtype
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right : ∀ (n : ℕ), (B n).IsSymm
t : (n : ℕ) → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable.{u + 1} (↑(t n) : Type u)
choose :
  ∀ (o : (n : ℕ) → (x : (↑(t n) : Type u)) → (hx : (ball (↑x : α) (B n) ∩ s).Nonempty) → α)
    (hox : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x : α) (B n))
    (hos : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ s),
    ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t

Tactic:
choose o hox hos using fun (n : ℕ) (x : t n) (hx : (ball x.1 (B n) ∩ s).Nonempty) => hx
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right : ∀ (n : ℕ), (B n).IsSymm
t : (n : ℕ) → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable.{u + 1} (↑(t n) : Type u)
o : (n : ℕ) → (x : (↑(t n) : Type u)) → (hx : (ball (↑x : α) (B n) ∩ s).Nonempty) → α
hox : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x : α) (B n)
hos : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t

Tactic:
⟨⋃ (n) (x), range (o n x), iUnion₂_subset fun _ _ => range_subset_iff.2 (hos _ _),
    countable_iUnion fun _ => countable_iUnion fun _ => countable_range _, fun x hx => ?_⟩

Premises used: Iff.mpr, Set.iUnion₂_subset, Set.countable_range, Set.countable_iUnion, And.intro, Exists.intro, Set.range, Set.range_subset_iff, Set.iUnion
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right : ∀ (n : ℕ), (B n).IsSymm
t : (n : ℕ) → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable.{u + 1} (↑(t n) : Type u)
o : (n : ℕ) → (x : (↑(t n) : Type u)) → (hx : (ball (↑x : α) (B n) ∩ s).Nonempty) → α
hox : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x : α) (B n)
hos : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ s
refine :
  ∀ (x : α) (hx : x ∈ s),
    Membership.mem (γ := Set α)
      (closure[uniformSpace.toTopologicalSpace] (⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x))) x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[uniformSpace.toTopologicalSpace] t

Tactic:
refine ⟨⋃ (n) (x), range (o n x), iUnion₂_subset fun _ _ => range_subset_iff.2 (hos _ _),
    countable_iUnion fun _ => countable_iUnion fun _ => countable_range _, fun x hx => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right : ∀ (n : ℕ), (B n).IsSymm
t : (n : ℕ) → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable.{u + 1} (↑(t n) : Type u)
o : (n : ℕ) → (x : (↑(t n) : Type u)) → (hx : (ball (↑x : α) (B n) ∩ s).Nonempty) → α
hox : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x : α) (B n)
hos : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
rw : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ ⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x)).Nonempty
⊢ Membership.mem (γ := Set α)
    (closure[uniformSpace.toTopologicalSpace] (⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x))) x

Tactic:
rw [mem_closure_iff_ball]

Premises used: UniformSpace.mem_closure_iff_ball
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right : ∀ (n : ℕ), (B n).IsSymm
t : (n : ℕ) → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable.{u + 1} (↑(t n) : Type u)
o : (n : ℕ) → (x : (↑(t n) : Type u)) → (hx : (ball (↑x : α) (B n) ∩ s).Nonempty) → α
hox : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x : α) (B n)
hos : ∀ (n : ℕ) (x : (↑(t n) : Type u)) (hx : (ball (↑x : α) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
U : Set (α × α)
hU : U ∈ 𝓤 α
obtain :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVU : V ○ V ⊆ U),
    (ball x U ∩ ⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x)).Nonempty
⊢ (ball x U ∩ ⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x)).Nonempty

Tactic:
obtain ⟨V, hV, hVU⟩ := comp_mem_uniformity_sets hU

Premises used: comp_mem_uniformity_sets