-- Mathlib/Topology/Connected/Clopen.lean
theorem isPreconnected_iff_subset_of_fully_disjoint_closed {s : Set α} (hs : IsClosed s) :
    IsPreconnected s ↔
      ∀ u v, IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v

Proof state:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∧ s ⊆ s ∨ s ⊆ v ∧ s ⊆ s
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
simp only [Subset.refl, and_true] at H1

Result:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
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
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
apply H u v hu hv hss

Result:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
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
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ∩ (u ∩ v) = ∅

Proof state:
case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ (u ∪ v) ∩ s

Tactic:
exact subset_inter hss Subset.rfl

Result:
no goals

Proof state:
case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∩ s ∪ v ∩ s

Tactic:
rw [← union_inter_distrib_right]

Result:
case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ (u ∪ v) ∩ s

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

Tactic:
refine isPreconnected_iff_subset_of_disjoint_closed.trans ⟨?_, ?_⟩ <;> intro H u v hu hv hss huv

Result:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
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
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ⊆ u ∨ s ⊆ v

case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
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
hss : s ⊆ u ∪ v
huv : Disjoint u v
⊢ s ∩ (u ∩ v) = ∅

Tactic:
rw [huv.inter_eq, inter_empty]

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
apply H1 (hu.inter hs) (hv.inter hs)

Result:
case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∩ s ∪ v ∩ s

case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ Disjoint (u ∩ s) (v ∩ s)

Proof state:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
have H1 := H (u ∩ s) (v ∩ s)

Result:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∩ s ∨ s ⊆ v ∩ s
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case refine_2.a
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∨ s ⊆ v
⊢ Disjoint (u ∩ s) (v ∩ s)

Tactic:
rwa [disjoint_iff_inter_eq_empty, ← inter_inter_distrib_right, inter_comm]

Result:
no goals

Proof state:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∩ s ∨ s ⊆ v ∩ s
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
rw [subset_inter_iff, subset_inter_iff] at H1

Result:
case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClosed s
H : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hss : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
H1 : IsClosed (u ∩ s) → IsClosed (v ∩ s) → s ⊆ u ∩ s ∪ v ∩ s → Disjoint (u ∩ s) (v ∩ s) → s ⊆ u ∧ s ⊆ s ∨ s ⊆ v ∧ s ⊆ s
⊢ s ⊆ u ∨ s ⊆ v