no goals
α : Type u
β : Type v
ι : Type ?u.187622
π : ι → Type ?u.187627
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t✝ : Set α
inst✝ : PreirreducibleSpace α
s t : Set α
⊢ IsOpen s → IsOpen t → Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s ∩ t)
simpa only [univ_inter, univ_subset_iff] using
  @PreirreducibleSpace.isPreirreducible_univ α _ _ s t