no goals
α : Type u_1
β : Type ?u.16113
γ : Type ?u.16116
ι : Type ?u.16119
inst✝ : TopologicalSpace α
s : Set α
⊢ (∃ S, S ⊆ {t | IsOpen t ∧ Dense t} ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ (t : Set α), t ∈ S → IsOpen t) ∧ (∀ (t : Set α), t ∈ S → Dense t) ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
simp_rw [subset_def, mem_setOf, forall_and, and_assoc]