-- Mathlib/Topology/Metrizable/Uniformity.lean
/-- A totally bounded set is separable in countably generated uniform spaces. This can be obtained
from the more general `EMetric.subset_countable_closure_of_almost_dense_set`. -/
lemma TotallyBounded.isSeparable [UniformSpace X] [i : IsCountablyGenerated (𝓤 X)]
    {s : Set X} (h : TotallyBounded s) : TopologicalSpace.IsSeparable s

Proof state:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
⊢ TopologicalSpace.IsSeparable s

Tactic:
have h' : ∀ ε > 0, ∃ t, Set.Countable t ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε := by
  intro ε hε
  obtain ⟨t, ht⟩ := h ε hε
  refine ⟨t, ht.1.countable, subset_trans ht.2 ?_⟩
  gcongr
  exact EMetric.ball_subset_closedBall

Result:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
h' : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε
⊢ TopologicalSpace.IsSeparable s

Proof state:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
h' : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε
⊢ TopologicalSpace.IsSeparable s

Tactic:
obtain ⟨t, _, htc, hts⟩ := EMetric.subset_countable_closure_of_almost_dense_set s h'

Result:
case intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
h' : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε
t : Set X
left✝ : t ⊆ s
htc : t.Countable
hts : s ⊆ _root_.closure t
⊢ TopologicalSpace.IsSeparable s

Proof state:
case intro
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
ε : ENNReal
hε : ε > 0
t : Set X
ht : t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
⊢ ⋃ y ∈ t, EMetric.ball y ε ⊆ ⋃ y ∈ t, EMetric.closedBall y ε

Tactic:
gcongr

Result:
case intro.h.h
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
ε : ENNReal
hε : ε > 0
t : Set X
ht : t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
i✝¹ : X
i✝ : i✝¹ ∈ t
⊢ EMetric.ball i✝¹ ε ⊆ EMetric.closedBall i✝¹ ε

Proof state:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
⊢ ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε

Tactic:
intro ε hε

Result:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
ε : ENNReal
hε : ε > 0
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε

Proof state:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
h : TotallyBounded s
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
⊢ TopologicalSpace.IsSeparable s

Tactic:
rw [EMetric.totallyBounded_iff] at h

Result:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
⊢ TopologicalSpace.IsSeparable s

Proof state:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
h : TotallyBounded s
⊢ TopologicalSpace.IsSeparable s

Tactic:
letI := (UniformSpace.pseudoMetricSpace (X := X)).toPseudoEMetricSpace

Result:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
h : TotallyBounded s
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
⊢ TopologicalSpace.IsSeparable s

Proof state:
case intro.h.h
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
ε : ENNReal
hε : ε > 0
t : Set X
ht : t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
i✝¹ : X
i✝ : i✝¹ ∈ t
⊢ EMetric.ball i✝¹ ε ⊆ EMetric.closedBall i✝¹ ε

Tactic:
exact EMetric.ball_subset_closedBall

Result:
no goals

Proof state:
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
ε : ENNReal
hε : ε > 0
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε

Tactic:
obtain ⟨t, ht⟩ := h ε hε

Result:
case intro
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
ε : ENNReal
hε : ε > 0
t : Set X
ht : t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε

Proof state:
case intro
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
ε : ENNReal
hε : ε > 0
t : Set X
ht : t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε

Tactic:
refine ⟨t, ht.1.countable, subset_trans ht.2 ?_⟩

Result:
case intro
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
ε : ENNReal
hε : ε > 0
t : Set X
ht : t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
⊢ ⋃ y ∈ t, EMetric.ball y ε ⊆ ⋃ y ∈ t, EMetric.closedBall y ε

Proof state:
case intro.intro.intro
X : Type u_1
inst✝ : UniformSpace X
i : (𝓤 X).IsCountablyGenerated
s : Set X
this : PseudoEMetricSpace X := PseudoMetricSpace.toPseudoEMetricSpace
h : ∀ ε > 0, ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε
h' : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ y ∈ t, EMetric.closedBall y ε
t : Set X
left✝ : t ⊆ s
htc : t.Countable
hts : s ⊆ _root_.closure t
⊢ TopologicalSpace.IsSeparable s

Tactic:
exact ⟨t, htc, hts⟩

Result:
no goals