case intro.intro.intro
α : Type u_1
β : Type ?u.15710
γ : Type ?u.15713
ι : Type ?u.15716
inst✝ : TopologicalSpace α
T : Set (Set α)
To : ∀ (t : Set α), t ∈ T → IsOpen t
Tct : Set.Countable T
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual α
α : Type u_1
β : Type ?u.15710
γ : Type ?u.15713
ι : Type ?u.15716
inst✝ : TopologicalSpace α
s : Set α
ho : IsGδ s
hd : Dense s
⊢ s ∈ residual α
rcases ho with ⟨T, To, Tct, rfl⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type ?u.15710
γ : Type ?u.15713
ι : Type ?u.15716
inst✝ : TopologicalSpace α
T : Set (Set α)
To : ∀ (t : Set α), t ∈ T → IsOpen t
Tct : Set.Countable T
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual α
exact
  (countable_sInter_mem Tct).mpr fun t tT =>
    residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))