-- Mathlib/Topology/Connected/Clopen.lean
theorem isConnected_iff_sUnion_disjoint_open {s : Set α} :
    IsConnected s ↔
      ∀ U : Finset (Set α), (∀ u v : Set α, u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen u) → (s ⊆ ⋃₀ ↑U) → ∃ u ∈ U, s ⊆ u

Proof state:
case refine_1.empty
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU : ∀ (u v : Set α), u ∈ ∅ → v ∈ ∅ → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ ∅, IsOpen u
hsU : s ⊆ ⋃₀ ↑∅
⊢ ∃ u ∈ ∅, s ⊆ u

Tactic:
exact absurd (by simpa using hsU) hne.not_subset_empty

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ (s.Nonempty ∧ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u

Tactic:
refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩

Result:
case refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
U : Finset (Set α)
hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ U, IsOpen u
hsU : s ⊆ ⋃₀ ↑U
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∃ u ∈ U, s ⊆ u

case refine_2
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
⊢ s.Nonempty

case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsuv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsuv : ¬(s ∩ (u ∩ v)).Nonempty
this : ¬(s ∩ (v ∩ u)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
simpa [*, or_imp, forall_and] using h {u, v}

Result:
no goals

Proof state:
case refine_1.insert.refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝ : s.Nonempty ∧ ∀ (a : Set α), IsOpen a → ∀ (b : Set α), IsOpen b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen a → ∀ (b : Set α), IsOpen b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen u ∧ ∀ x ∈ U, IsOpen x
hsU : s ⊆ u ∪ ⋃₀ ↑U
⊢ s ∩ (u ∩ ⋃₀ ↑U) = ∅

Tactic:
refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_

Result:
case refine_1.insert.refine_1
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
x✝¹ : s.Nonempty ∧ ∀ (a : Set α), IsOpen a → ∀ (b : Set α), IsOpen b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen a → ∀ (b : Set α), IsOpen b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH : (∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen u ∧ ∀ x ∈ U, IsOpen x
hsU : s ⊆ u ∪ ⋃₀ ↑U
x : α
x✝ : x ∈ s ∩ (u ∩ ⋃₀ ↑U)
hxs : x ∈ s
hxu : x ∈ u
v : Set α
hvU : v ∈ ↑U
hxv : x ∈ v
⊢ x ∈ ∅

Proof state:
case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsuv : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
have := hsuv

Result:
case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsuv this : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x✝ : s.Nonempty ∧ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU : ∀ (u v : Set α), u ∈ ∅ → v ∈ ∅ → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ ∅, IsOpen u
hsU : s ⊆ ⋃₀ ↑∅
⊢ s ⊆ ∅

Tactic:
simpa using hsU

Result:
no goals

Proof state:
case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsuv this : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
rw [inter_comm u] at this

Result:
case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) → (∀ u ∈ U, IsOpen u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsuv : ¬(s ∩ (u ∩ v)).Nonempty
this : ¬(s ∩ (v ∩ u)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v