Theorem: IsPreconnected.subset_or_subset_of_closed (Sion/ForMathlib/Misc.lean)

State before:
α : Type u_1
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ⊆ u ∨ s ⊆ v
Tactic:
apply (isPreconnected_iff_subset_of_disjoint_closed.mp hs) u v hu hv hsuv
State after:
α : Type u_1
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ∩ (u ∩ v) = ∅

State before:
α : Type u_1
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hs : IsPreconnected s
⊢ s ∩ (u ∩ v) = ∅
Tactic:
rw [Set.disjoint_iff_inter_eq_empty.mp huv, Set.inter_empty]
State after:
no goals