awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
obtain : ∀ (n : ℕ) (hn : B n ⊆ V), (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 ⟨n, hn⟩ := hB.mem_iff.1 hV

Premises used: Filter.HasAntitoneBasis.mem_iff, Iff.mp
-- 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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
⊢ Membership.mem (γ := Set α) (⋃ x ∈ t n, ball x (B n)) x

Tactic:
specialize ht n 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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
ht : Membership.mem (γ := Set α) (⋃ x ∈ t n, ball x (B n)) x
⊢ ∃ (i : α) (_ : i ∈ t n), x ∈ ball i (B n)

Tactic:
rw [mem_iUnion₂] at ht

Premises used: Set.mem_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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
ht : ∃ (i : α) (_ : i ∈ t n), x ∈ ball i (B n)
obtain :
  ∀ (y : α) (hy : y ∈ t n) (hyx : x ∈ ball y (B n)),
    (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 ⟨y, hy, hyx⟩ := ht
-- 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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ (ball x U ∩ ⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x)).Nonempty

Tactic:
⟨o n ⟨y, hy⟩ ⟨x, hyx, hx⟩, ?_, ?_⟩

Premises used: Subtype.mk, Set.Nonempty, And.intro, Exists.intro
-- 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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
refine_1 : o n (Subtype.mk (p := fun (x : α) ↦ x ∈ t n) y hy) ⋯ ∈ ball x U
refine_2 :
  Membership.mem (γ := Set α) (⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x))
    (o n (Subtype.mk (p := fun (x : α) ↦ x ∈ t n) y hy) ⋯)
⊢ (ball x U ∩ ⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x)).Nonempty

Tactic:
refine ⟨o n ⟨y, hy⟩ ⟨x, hyx, 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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
refine_1 : o n (Subtype.mk (p := fun (x : α) ↦ x ∈ t n) y hy) ⋯ ∈ ball x (B n ○ B n)
⊢ o n (Subtype.mk (p := fun (x : α) ↦ x ∈ t n) y hy) ⋯ ∈ ball x U

Tactic:
apply ball_mono ((SetRel.comp_subset_comp hn hn).trans hVU)

Premises used: SetRel.comp_subset_comp, UniformSpace.ball_mono, HasSubset.Subset.trans
-- 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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ o n (Subtype.mk (p := fun (x : α) ↦ x ∈ t n) y hy) ⋯ ∈ ball x (B n ○ B n)

Tactic:
mem_ball_comp (mem_ball_symmetry.2 hyx) (hox n ⟨y, hy⟩ ⟨x, hyx, hx⟩)

Premises used: Iff.mpr, UniformSpace.mem_ball_comp, Subtype.mk, UniformSpace.mem_ball_symmetry, And.intro, Exists.intro
-- 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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ o n (Subtype.mk (p := fun (x : α) ↦ x ∈ t n) y hy) ⋯ ∈ ball x (B n ○ B n)

Tactic:
exact mem_ball_comp (mem_ball_symmetry.2 hyx) (hox n ⟨y, hy⟩ ⟨x, hyx, hx⟩)

Premises used: Iff.mpr, UniformSpace.mem_ball_comp, Subtype.mk, UniformSpace.mem_ball_symmetry, And.intro, Exists.intro
-- 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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x))
    (o n (Subtype.mk (p := fun (x : α) ↦ x ∈ t n) y hy) ⋯)

Tactic:
mem_iUnion₂_of_mem ⟨y, hy⟩ (mem_range_self ⟨x, hyx, hx⟩)

Premises used: Set.mem_range_self, Set.mem_iUnion₂_of_mem, Subtype.mk
-- 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
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 ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVU : V ○ V ⊆ U
n : ℕ
hn : B n ⊆ V
y : α
hy : y ∈ t n
hyx : x ∈ ball y (B n)
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), ⋃ (x : (↑(t n) : Type u)), range (o n x))
    (o n (Subtype.mk (p := fun (x : α) ↦ x ∈ t n) y hy) ⋯)

Tactic:
exact mem_iUnion₂_of_mem ⟨y, hy⟩ (mem_range_self ⟨x, hyx, hx⟩)

Premises used: Set.mem_iUnion₂_of_mem
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, ball x U) univ
suffices : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, ball x U) univ
⊢ ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, ball x U)

Tactic:
simpa only [univ_subset_iff] using hs

Premises used: Set.univ_subset_iff
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, ball x U) univ
⊢ ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, ball x U)

Tactic:
have : ∀ U ∈ 𝓤 α, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, ball x U := by
    simpa only [univ_subset_iff] using hs
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, ball x U) univ
this : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, ball x U)
rcases : ∀ (t : Set α) (htc : t.Countable) (ht : univ ⊆ closure[uniformSpace.toTopologicalSpace] t), SeparableSpace α
⊢ SeparableSpace α

Tactic:
rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩

Premises used: Set.univ, UniformSpace.subset_countable_closure_of_almost_dense_set
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, ball x U) univ
this : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, ball x U)
t : Set α
htc : t.Countable
ht : univ ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ SeparableSpace α

Tactic:
⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩

Premises used: And.intro, Exists.intro, Set.mem_univ, TopologicalSpace.SeparableSpace.mk
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ t, ball x U) univ
this : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ Subset.{u} (α := Set α) univ (⋃ x ∈ t, ball x U)
t : Set α
htc : t.Countable
ht : univ ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ SeparableSpace α

Tactic:
exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
obtain :
  ∀ (t : Set α) (ht : t.Finite) (hst : s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ SetRel.inv U}),
    ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
obtain ⟨t, ht, hst⟩ := h (SetRel.inv U)
      (mem_of_superset (symmetrize_mem_uniformity hU) SetRel.symmetrize_subset_inv)

Premises used: SetRel.inv, symmetrize_mem_uniformity, SetRel.symmetrize_subset_inv, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
t : Set α
ht : t.Finite
hst : s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ SetRel.inv U}
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
⟨t, ht.countable, hst⟩

Premises used: And.intro, Exists.intro, Set.Finite.countable
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
U : Set (α × α)
hU : U ∈ 𝓤 α
t : Set α
ht : t.Finite
hst : s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ SetRel.inv U}
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
exact ⟨t, ht.countable, hst⟩
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
obtain : ∀ (t : Set α) (htc : t.Countable) (hts : s ⊆ closure[uniformSpace.toTopologicalSpace] t), IsSeparable s
⊢ IsSeparable s

Tactic:
obtain ⟨t, -, htc, hts⟩ := subset_countable_closure_of_almost_dense_set s fun U hU => by
    obtain ⟨t, ht, hst⟩ := h (SetRel.inv U)
      (mem_of_superset (symmetrize_mem_uniformity hU) SetRel.symmetrize_subset_inv)
    exact ⟨t, ht.countable, hst⟩

Premises used: UniformSpace.subset_countable_closure_of_almost_dense_set
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
t : Set α
htc : t.Countable
hts : s ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ IsSeparable s

Tactic:
⟨t, htc, hts⟩

Premises used: TopologicalSpace.IsSeparable, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Cauchy
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
s : Set α
h : TotallyBounded s
t : Set α
htc : t.Countable
hts : s ⊆ closure[uniformSpace.toTopologicalSpace] t
⊢ IsSeparable s

Tactic:
exact ⟨t, htc, hts⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U : SetRel α α
s t : Set α
⊢ (s, t) ∈ hausdorffEntourage U ↔ s ⊆ U.preimage t ∧ t ⊆ U.image s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
h : U ⊆ V
⊢ Subset.{u_1} (α := SetRel (Set α) (Set α)) {x : Set α × Set α | x.1 ⊆ U.preimage x.2 ∧ x.2 ⊆ U.image x.1}
    {x : Set α × Set α | x.1 ⊆ V.preimage x.2 ∧ x.2 ⊆ V.image x.1}

Tactic:
gcongr
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
⊢ Monotone.{u_1, u_1} (α := SetRel α α) hausdorffEntourage

Tactic:
fun _ _ => hausdorffEntourage_mono

Premises used: Monotone, hausdorffEntourage_mono
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
simp_rw :
  Eq.{u_1 + 1} (α := SetRel (Set α) (Set α))
    {x : Set α × Set α | x.1 ⊆ preimage SetRel.id x.2 ∧ x.2 ⊆ image SetRel.id x.1} SetRel.id
simp_rw₁ :
  Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) {x : Set α × Set α | x.1 ⊆ x.2 ∧ x.2 ⊆ image SetRel.id x.1} SetRel.id
simp_rw₂ : Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) {x : Set α × Set α | x.1 ⊆ x.2 ∧ x.2 ⊆ x.1} SetRel.id
simp_rw₃ : Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) {x : Set α × Set α | x.1 = x.2} SetRel.id
⊢ Eq.{u_1 + 1} (α := SetRel (Set α) (Set α)) (hausdorffEntourage SetRel.id) SetRel.id

Tactic:
simp_rw [hausdorffEntourage, preimage_id, image_id, ← subset_antisymm_iff, SetRel.id]

Premises used: SetRel.id, subset_antisymm_iff, SetRel.image_id, SetRel.preimage_id, hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst : U.IsRefl
⊢ (hausdorffEntourage U).IsRefl

Tactic:
⟨fun _ => ⟨U.self_subset_preimage _, U.self_subset_image _⟩⟩

Premises used: SetRel.self_subset_preimage, Std.Refl.mk, Prod.mk, SetRel.self_subset_image, Prod.fst, And.intro, Prod.snd
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U : SetRel α α
⊢ (hausdorffEntourage U).inv = hausdorffEntourage U.inv

Tactic:
Set.ext fun _ => And.comm

Premises used: Set.ext, And.comm
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
U : SetRel α α
inst : U.IsSymm
rw : (hausdorffEntourage U).inv = hausdorffEntourage U
rw₁ : hausdorffEntourage U.inv = hausdorffEntourage U
rw₂ rw₃ : hausdorffEntourage U = hausdorffEntourage U
⊢ (hausdorffEntourage U).IsSymm

Tactic:
rw [← inv_eq_self_iff, inv_hausdorffEntourage, inv_eq_self]

Premises used: inv_hausdorffEntourage, SetRel.inv_eq_self, SetRel.inv_eq_self_iff
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
a : hausdorffEntourage (U ○ V) ⊆ hausdorffEntourage U ○ hausdorffEntourage V
a₁ : hausdorffEntourage U ○ hausdorffEntourage V ⊆ hausdorffEntourage (U ○ V)
⊢ hausdorffEntourage (U ○ V) = hausdorffEntourage U ○ hausdorffEntourage V

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
a :
  ∀ (hst : (s, t).1 ⊆ (U ○ V).preimage (s, t).2) (hts : (s, t).2 ⊆ (U ○ V).image (s, t).1),
    (s, t) ∈ hausdorffEntourage U ○ hausdorffEntourage V
⊢ (s, t) ∈ hausdorffEntourage (U ○ V) → (s, t) ∈ hausdorffEntourage U ○ hausdorffEntourage V

Tactic:
⟨hst, hts⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : (s, t).1 ⊆ (U ○ V).preimage (s, t).2
hts : (s, t).2 ⊆ (U ○ V).image (s, t).1
a : ∃ (b : Set α), (s ⊆ U.preimage b ∧ b ⊆ U.image s) ∧ b ⊆ V.preimage t ∧ t ⊆ V.image b
⊢ (s, t) ∈ hausdorffEntourage U ○ hausdorffEntourage V

Tactic:
simp only [mem_comp, mem_hausdorffEntourage] at *

Premises used: SetRel.mem_comp, mem_hausdorffEntourage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
⊢ ∃ (b : Set α), (s ⊆ U.preimage b ∧ b ⊆ U.image s) ∧ b ⊆ V.preimage t ∧ t ⊆ V.image b

Tactic:
⟨U.image s ∩ V.preimage t, ⟨?_, Set.inter_subset_left⟩, ⟨Set.inter_subset_right, ?_⟩⟩

Premises used: Set.inter_subset_left, Inter.inter, And.intro, Exists.intro, SetRel.image, SetRel.preimage, Set.inter_subset_right
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
a : s ⊆ U.preimage (U.image s ∩ V.preimage t)
a₁ : t ⊆ V.image (U.image s ∩ V.preimage t)
⊢ ∃ (b : Set α), (s ⊆ U.preimage b ∧ b ⊆ U.image s) ∧ b ⊆ V.preimage t ∧ t ⊆ V.image b

Tactic:
refine ⟨U.image s ∩ V.preimage t, ⟨?_, Set.inter_subset_left⟩, ⟨Set.inter_subset_right, ?_⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
x : α
hx : x ∈ s
a : ∀ (z : α) (hz : z ∈ t) (y : α) (hxy : (x, y) ∈ U) (hyz : (y, z) ∈ V), x ∈ U.preimage (U.image s ∩ V.preimage t)
⊢ x ∈ U.preimage (U.image s ∩ V.preimage t)

Tactic:
obtain ⟨z, hz, y, hxy, hyz⟩ := hst hx
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
x : α
hx : x ∈ s
z : α
hz : z ∈ t
y : α
hxy : (x, y) ∈ U
hyz : (y, z) ∈ V
⊢ x ∈ U.preimage (U.image s ∩ V.preimage t)

Tactic:
⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hxy⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, SetRel.preimage
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
x : α
hx : x ∈ s
z : α
hz : z ∈ t
y : α
hxy : (x, y) ∈ U
hyz : (y, z) ∈ V
⊢ x ∈ U.preimage (U.image s ∩ V.preimage t)

Tactic:
exact ⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hxy⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
z : α
hz : z ∈ t
a : ∀ (x : α) (hx : x ∈ s) (y : α) (hxy : (x, y) ∈ U) (hyz : (y, z) ∈ V), z ∈ V.image (U.image s ∩ V.preimage t)
⊢ z ∈ V.image (U.image s ∩ V.preimage t)

Tactic:
obtain ⟨x, hx, y, hxy, hyz⟩ := hts hz
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
z : α
hz : z ∈ t
x : α
hx : x ∈ s
y : α
hxy : (x, y) ∈ U
hyz : (y, z) ∈ V
⊢ z ∈ V.image (U.image s ∩ V.preimage t)

Tactic:
⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hyz⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, SetRel.image
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s t : Set α
hst : s ⊆ (U ○ V).preimage t
hts : t ⊆ (U ○ V).image s
z : α
hz : z ∈ t
x : α
hx : x ∈ s
y : α
hxy : (x, y) ∈ U
hyz : (y, z) ∈ V
⊢ z ∈ V.image (U.image s ∩ V.preimage t)

Tactic:
exact ⟨y, ⟨⟨x, hx, hxy⟩, ⟨z, hz, hyz⟩⟩, hyz⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
U V : SetRel α α
s₁ s₃ : Set α
a :
  ∀ (s₂ : Set α) (h₁₂ : (s₁, s₂).1 ⊆ U.preimage (s₁, s₂).2) (h₂₁ : (s₁, s₂).2 ⊆ U.image (s₁, s₂).1)
    (h₂₃ : (s₂, s₃).1 ⊆ V.preimage (s₂, s₃).2) (h₃₂ : (s₂, s₃).2 ⊆ V.image (s₂, s₃).1),
    (s₁, s₃) ∈ hausdorffEntourage (U ○ V)
⊢ (s₁, s₃) ∈ hausdorffEntourage U ○ hausdorffEntourage V → (s₁, s₃) ∈ hausdorffEntourage (U ○ V)

Tactic:
⟨s₂, ⟨h₁₂, h₂₁⟩, ⟨h₂₃, h₃₂⟩⟩