case intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : Set.Countable s
s_dense : Dense s
⊢ ∃ u, DenseRange u
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
⊢ ∃ u, DenseRange u
obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α
case intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : Set.Countable s
s_dense : Dense s
u : ℕ → α
hu : s ⊆ range u
⊢ ∃ u, DenseRange u
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : Set.Countable s
s_dense : Dense s
⊢ ∃ u, DenseRange u
cases' Set.countable_iff_exists_subset_range.mp hs with u hu
no goals
case intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : Set.Countable s
s_dense : Dense s
u : ℕ → α
hu : s ⊆ range u
⊢ ∃ u, DenseRange u
exact ⟨u, s_dense.mono hu⟩