awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
⊢ IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
(isUniformEmbedding_iff _).trans <| and_comm.trans <| Iff.rfl.and isUniformInducing_iff

Premises used: isUniformEmbedding_iff, Iff.rfl, and_comm, Iff.and, Iff.trans, EMetric.isUniformInducing_iff
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : IsUniformInducing f
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
⟨uniformContinuous_iff.1 h.uniformContinuous, (isUniformInducing_iff.1 h).2⟩

Premises used: EMetric.uniformContinuous_iff, And.right, And.intro, Iff.mp, EMetric.isUniformInducing_iff, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : IsUniformEmbedding f
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
controlled_of_isUniformInducing h.toIsUniformInducing

Premises used: IsUniformEmbedding.toIsUniformInducing, EMetric.controlled_of_isUniformInducing
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Filter α
rw : Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
⊢ Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
rw [← neBot_iff]

Premises used: Filter.neBot_iff
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
uniformity_basis_edist.cauchy_iff

Premises used: uniformity_basis_edist, Set.Mem, setOf, Filter.HasBasis.cauchy_iff
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
exact uniformity_basis_edist.cauchy_iff

Premises used: uniformity_basis_edist, Filter.HasBasis.cauchy_iff
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
B : ℕ → ℝ≥0∞
hB : ∀ (n : ℕ), 0 < B n
H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (u n) (u m) < B N) → ∃ (x : α), Tendsto u atTop (𝓝 x)
⊢ CompleteSpace α

Tactic:
UniformSpace.complete_of_convergent_controlled_sequences
    (fun n => { p : α × α | edist p.1 p.2 < B n }) (fun n => edist_mem_uniformity <| hB n) H

Premises used: edist_mem_uniformity, setOf, Prod.fst, LT.lt, UniformSpace.complete_of_convergent_controlled_sequences, EDist.edist, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ (∀ (u : ℕ → α), CauchySeq u → ∃ (a : α), Tendsto u atTop (𝓝 a)) → CompleteSpace α

Tactic:
UniformSpace.complete_of_cauchySeq_tendsto

Premises used: UniformSpace.complete_of_cauchySeq_tendsto
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Tactic:
⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu x hx => ?_⟩

Premises used: edist_mem_uniformity, setOf, Prod.fst, LT.lt, Iff.intro, EDist.edist, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
refine :
  ∀ (H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε) (u : Set (α × α))
    (hu : u ∈ 𝓤 α) (x : β) (hx : x ∈ s), ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Tactic:
refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu x hx => ?_⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
rcases :
  ∀ (ε : ℝ≥0∞) (εpos : ε > 0) (hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u),
    ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩

Premises used: Iff.mp, mem_uniformity_edist
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
rcases :
  ∀ (t : Set β) (ht : t ∈ 𝓝[s] x) (Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε),
    ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases H ε εpos x hx with ⟨t, ht, Ht⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩

Premises used: Filter.Eventually.mono, And.intro, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε

Tactic:
⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => ?_⟩

Premises used: edist_mem_uniformity, setOf, Prod.fst, LT.lt, Iff.intro, EDist.edist, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
refine :
  ∀ (H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε) (u : Set (α × α)) (hu : u ∈ 𝓤 α),
    ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε

Tactic:
refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => ?_⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
rcases :
  ∀ (ε : ℝ≥0∞) (εpos : ε > 0) (hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u), ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Tactic:
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩

Premises used: Iff.mp, mem_uniformity_edist
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Tactic:
(H ε εpos).mono fun n hs x hx => hε (hs x hx)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Tactic:
exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Tactic:
simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, mem_univ,
    forall_const, nhdsWithin_univ]

Premises used: nhdsWithin_univ, EMetric.tendstoLocallyUniformlyOn_iff, Set.mem_univ, forall_const, tendstoLocallyUniformlyOn_univ
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε

Tactic:
simp only [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff, mem_univ, forall_const]

Premises used: tendstoUniformlyOn_univ, Set.mem_univ, EMetric.tendstoUniformlyOn_iff, forall_const
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
⊢ Inseparable x y ↔ edist x y = 0

Tactic:
simp [inseparable_iff_mem_closure, mem_closure_iff, edist_comm, forall_gt_iff_le]

Premises used: PseudoEMetricSpace.edist_comm, inseparable_iff_mem_closure, forall_gt_iff_le, EMetric.mem_closure_iff
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u_2
inst : EMetricSpace α
simp_rw : (∃ (x : α) (y : α), x ≠ y) ↔ NontrivialTopology α
simp_rw₁ : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (x : α) (y : α), ¬Inseparable x y
simp_rw₂ : (∃ (x : α) (y : α), x ≠ y) ↔ ∃ (x : α) (y : α), ¬edist x y = 0
⊢ Nontrivial α ↔ NontrivialTopology α

Tactic:
simp_rw [nontrivial_iff, TopologicalSpace.nontrivial_iff_exists_not_inseparable,
    EMetric.inseparable_iff, edist_eq_zero]

Premises used: TopologicalSpace.nontrivial_iff_exists_not_inseparable, nontrivial_iff, edist_eq_zero, EMetric.inseparable_iff
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u_2
inst : EMetricSpace α
⊢ Subsingleton α ↔ IndiscreteTopology α

Tactic:
simpa [not_nontrivial_iff_subsingleton] using nontrivial_iff_nontrivialTopology (α := α).not

Premises used: not_nontrivial_iff_subsingleton, Iff.not, EMetric.nontrivial_iff_nontrivialTopology
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
x y z : α_1
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α_1
α : Type u_2
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
⊢ NontrivialTopology α

Tactic:
nontrivial_iff_nontrivialTopology.1 ‹_›

Premises used: EMetric.nontrivial_iff_nontrivialTopology, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (u m) (u n) < ε

Tactic:
uniformity_basis_edist.cauchySeq_iff

Premises used: uniformity_basis_edist, Filter.HasBasis.cauchySeq_iff, Set.Mem, setOf
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, edist (u n) (u N) < ε

Tactic:
uniformity_basis_edist.cauchySeq_iff'

Premises used: uniformity_basis_edist, Set.Mem, setOf, Filter.HasBasis.cauchySeq_iff'
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
⊢ CauchySeq u ↔ ∀ (ε : ℝ≥0), 0 < ε → ∃ (N : β), ∀ (n : β), N ≤ n → edist (u n) (u N) < (↑ε : ℝ≥0∞)

Tactic:
uniformity_basis_edist_nnreal.cauchySeq_iff'

Premises used: Set.Mem, setOf, Filter.HasBasis.cauchySeq_iff', uniformity_basis_edist_nnreal
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ ε > 0, ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε

Tactic:
⟨fun H _ε ε0 => H _ (edist_mem_uniformity ε0), fun H _r ru =>
    let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru
    let ⟨t, ft, h⟩ := H ε ε0
    ⟨t, ft, h.trans <| iUnion₂_mono fun _ _ _ => hε⟩⟩

Premises used: edist_mem_uniformity, setOf, Set.Finite, Membership.mem, Exists, HasSubset.Subset.trans, Prod.mk, HasSubset.Subset, Prod.fst, _private.0.EMetric.totallyBounded_iff.match_2, Set.iUnion₂_mono, And, And.intro, LT.lt, Iff.intro, Exists.intro, Iff.mp, EDist.edist, Prod.snd, _private.0.EMetric.totallyBounded_iff.match_1, Set.iUnion, mem_uniformity_edist
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε

Tactic:
⟨fun H _ε ε0 => (totallyBounded_iff_subset.1 H) _ (edist_mem_uniformity ε0), fun H _r ru =>
    let ⟨ε, ε0, hε⟩ := mem_uniformity_edist.1 ru
    let ⟨t, _, ft, h⟩ := H ε ε0
    ⟨t, ft, h.trans <| iUnion₂_mono fun _ _ _ => hε⟩⟩

Premises used: edist_mem_uniformity, setOf, Set.Finite, Membership.mem, Exists, HasSubset.Subset.trans, Prod.mk, HasSubset.Subset, _private.0.EMetric.totallyBounded_iff'.match_1, Prod.fst, _private.0.EMetric.totallyBounded_iff.match_2, Set.iUnion₂_mono, And, And.intro, LT.lt, Iff.intro, Exists.intro, Iff.mp, totallyBounded_iff_subset, EDist.edist, Prod.snd, Set.iUnion, mem_uniformity_edist
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
hs₁ : ∀ U ∈ 𝓤 α, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
apply UniformSpace.subset_countable_closure_of_almost_dense_set

Premises used: UniformSpace.subset_countable_closure_of_almost_dense_set
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
hs₁ :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U),
    ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U

Tactic:
obtain ⟨ε, hε, hεU⟩ := uniformity_basis_edist_le.mem_iff.1 hU

Premises used: Filter.HasBasis.mem_iff, uniformity_basis_edist_le, Iff.mp
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U
hs₁ :
  ∀ (t : Set α) (tC : t.Countable) (ht : s ⊆ ⋃ x ∈ t, closedEBall x ε),
    ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U

Tactic:
obtain ⟨t, tC, ht⟩ := hs ε hε
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U

Tactic:
⟨t, tC, ht.trans (iUnion₂_mono fun x hx y hy => UniformSpace.ball_mono hεU x ?_)⟩

Premises used: UniformSpace.ball_mono, HasSubset.Subset.trans, Set.iUnion₂_mono, And.intro, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
hs₁ : ∀ (x : α) (hx : x ∈ t) (y : α) (hy : y ∈ closedEBall x ε), y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U

Tactic:
refine ⟨t, tC, ht.trans (iUnion₂_mono fun x hx y hy => UniformSpace.ball_mono hεU x ?_)⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ≥0∞
hε : 0 < ε
hεU : {p : α × α | edist p.1 p.2 ≤ ε} ⊆ U
t : Set α
tC : t.Countable
ht : s ⊆ ⋃ x ∈ t, closedEBall x ε
x : α
hx : x ∈ t
y : α
hy : y ∈ closedEBall x ε
hs₁ : ∀ (hy : edist y x ≤ ε), y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
hs₂ hs₃ hs₄ hs₅ : ∀ (hy : edist x y ≤ ε), y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}
⊢ y ∈ UniformSpace.ball x {p : α × α | edist p.1 p.2 ≤ ε}

Tactic:
rwa [mem_closedEBall, edist_comm] at hy

Premises used: PseudoEMetricSpace.edist_comm, Metric.mem_closedEBall
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
subset_countable_closure_of_almost_dense_set s fun ε hε => ?_

Premises used: EMetric.subset_countable_closure_of_almost_dense_set
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
refine : ∀ (ε : ℝ≥0∞) (hε : ε > 0), ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
refine subset_countable_closure_of_almost_dense_set s fun ε hε => ?_

Premises used: EMetric.subset_countable_closure_of_almost_dense_set
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
rcases :
  ∀ (t : Set α) (htf : t.Finite) (hst : s ⊆ ⋃ y ∈ t, eball y ε),
    ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε

Tactic:
rcases totallyBounded_iff'.1 hs.totallyBounded ε hε with ⟨t, -, htf, hst⟩

Premises used: IsCompact.totallyBounded, Iff.mp, EMetric.totallyBounded_iff'
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
t : Set α
htf : t.Finite
hst : s ⊆ ⋃ y ∈ t, eball y ε
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε

Tactic:
⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => eball_subset_closedEBall⟩

Premises used: Metric.eball_subset_closedEBall, HasSubset.Subset.trans, Set.iUnion₂_mono, And.intro, Exists.intro, Set.Finite.countable
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
ε : ℝ≥0∞
hε : ε > 0
t : Set α
htf : t.Finite
hst : s ⊆ ⋃ y ∈ t, eball y ε
⊢ ∃ (t : Set α), t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε

Tactic:
exact ⟨t, htf.countable, hst.trans <| iUnion₂_mono fun _ _ => eball_subset_closedEBall⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
this : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
UniformSpace.secondCountable_of_separable α

Premises used: UniformSpace.secondCountable_of_separable
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
this : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
exact UniformSpace.secondCountable_of_separable α

Premises used: UniformSpace.secondCountable_of_separable
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
suffices : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
choose :
  ∀ (T : (n : ℕ) → Set α),
    (∀ (n : ℕ), T n ⊆ compactCovering α n) →
      ∀ (hTc : ∀ (n : ℕ), (T n).Countable)
        (hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)),
        SeparableSpace α
⊢ SeparableSpace α

Tactic:
choose T _ hTc hsubT using fun n =>
    subset_countable_closure_of_compact (isCompact_compactCovering α n)

Premises used: isCompact_compactCovering, EMetric.subset_countable_closure_of_compact
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
T : (n : ℕ) → Set α
h : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
⊢ SeparableSpace α

Tactic:
⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => ?_⟩⟩

Premises used: Set.countable_iUnion, And.intro, Exists.intro, TopologicalSpace.SeparableSpace.mk, Set.iUnion
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
T : (n : ℕ) → Set α
h : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
refine :
  ∀ (x : α),
    Membership.mem (γ := Set α) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (n : ℕ), T n)) x
⊢ SeparableSpace α

Tactic:
refine ⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => ?_⟩⟩
-- Module: Mathlib.Topology.EMetricSpace.Basic
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x_1 y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst_1 : SigmaCompactSpace α
T : (n : ℕ) → Set α
h : ∀ (n : ℕ), T n ⊆ compactCovering α n
hTc : ∀ (n : ℕ), (T n).Countable
hsubT : ∀ (n : ℕ), compactCovering α n ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (T n)
x : α
rcases :
  ∀ (n : ℕ) (hn : x ∈ compactCovering α n),
    Membership.mem (γ := Set α) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (n : ℕ), T n)) x
⊢ Membership.mem (γ := Set α) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (n : ℕ), T n)) x

Tactic:
rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩

Premises used: Set.iUnion_eq_univ_iff, iUnion_compactCovering, Iff.mp