-- Mathlib/Topology/Connected/Clopen.lean
theorem isPreconnected_iff_subset_of_disjoint_closed :
    IsPreconnected s ↔
      ∀ u v, IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
by_contra H

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv

Result:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
hyu : y ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
hyu : y ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩

Result:
no goals

Proof state:
case mpr.inl.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩

Result:
no goals

Proof state:
case mpr.inr.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

Result:
no goals

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
huv : (∃ a ∈ s, a ∉ u) ∧ ∃ a ∈ s, a ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty

Tactic:
intro u v hu hv hs hsu hsv

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
rw [isPreconnected_closed_iff] at h

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu

Result:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
simp only [not_subset] at huv

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
huv : (∃ a ∈ s, a ∉ u) ∧ ∃ a ∈ s, a ∉ v
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
contrapose! huv

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
⊢ False

Tactic:
apply H

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsv with ⟨x, hxs, hxv⟩

Result:
case mpr.inl.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsu with ⟨x, hxs, hxu⟩

Result:
case mpr.inr.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty