no goals
α : Type u
β : Type v
ι : Type ?u.69212
π : ι → Type ?u.69217
inst✝¹ : TopologicalSpace α
s✝ t✝ u v : Set α
inst✝ : PreconnectedSpace α
s t : Set α
⊢ IsOpen s → IsOpen t → s ∪ t = univ → Set.Nonempty s → Set.Nonempty t → Set.Nonempty (s ∩ t)
simpa only [univ_inter, univ_subset_iff] using @PreconnectedSpace.isPreconnected_univ α _ _ s t