-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.subset_of_closure_inter_subset (hs : IsPreconnected s) (hu : IsOpen u)
    (h'u : (s ∩ u).Nonempty) (h : closure u ∩ s ⊆ u) : s ⊆ u

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
A : s ⊆ u ∪ (closure u)ᶜ
⊢ s ⊆ u

Tactic:
apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u

Result:
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
A : s ⊆ u ∪ (closure u)ᶜ
⊢ Disjoint u (closure u)ᶜ

Proof state:
case pos
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∈ u
⊢ x ∈ u ∪ (closure u)ᶜ

Tactic:
exact Or.inl xu

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
⊢ x ∈ u ∪ (closure u)ᶜ

Tactic:
by_cases xu : x ∈ u

Result:
case pos
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∈ u
⊢ x ∈ u ∪ (closure u)ᶜ

case neg
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
⊢ x ∈ u ∪ (closure u)ᶜ

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
⊢ s ⊆ u ∪ (closure u)ᶜ

Tactic:
intro x hx

Result:
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
⊢ x ∈ u ∪ (closure u)ᶜ

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
A : s ⊆ u ∪ (closure u)ᶜ
⊢ Disjoint u (closure u)ᶜ

Tactic:
exact disjoint_compl_right.mono_right (compl_subset_compl.2 subset_closure)

Result:
no goals

Proof state:
case neg.h
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
h'x : x ∈ closure u
⊢ False

Tactic:
exact xu (h (mem_inter h'x hx))

Result:
no goals

Proof state:
case neg.h
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
⊢ x ∈ (closure u)ᶜ

Tactic:
intro h'x

Result:
case neg.h
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
h'x : x ∈ closure u
⊢ False

Proof state:
case neg
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
⊢ x ∈ u ∪ (closure u)ᶜ

Tactic:
right

Result:
case neg.h
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen u
h'u : (s ∩ u).Nonempty
h : closure u ∩ s ⊆ u
x : α
hx : x ∈ s
xu : x ∉ u
⊢ x ∈ (closure u)ᶜ