no goals
α : Type u
β : Type v
ι : Type ?u.76247
π : ι → Type ?u.76252
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
h :
  ∀ {ι : Type u} (Z : ι → Set α),
    (∀ (i : ι), IsClosed (Z i)) → (⋂ (i : ι), Z i) = ∅ → ∃ t, (⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
ι✝ : Type u
Z : ι✝ → Set α
⊢ (∀ (i : ι✝), IsClosed (Z i)) → (univ ∩ ⋂ (i : ι✝), Z i) = ∅ → ∃ t, (univ ∩ ⋂ (i : ι✝) (_ : i ∈ t), Z i) = ∅
simpa using h Z