-- Mathlib/Topology/Separation/Regular.lean
theorem connectedComponent_eq_iInter_isClopen [T2Space X] [CompactSpace X] (x : X) :
    connectedComponent x = ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s

Proof state:
case neg.h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
⊢ ⋂ s, ↑s ⊆ v

Tactic:
refine Subset.trans ?_ s.inter_subset_right

Result:
case neg.h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
⊢ ⋂ s, ↑s ⊆ s ∩ v

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, (fun s => ↑s) i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun s => ↑s) i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
obtain ⟨si, H2⟩ :=
  H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv)

Result:
case intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, (fun s => ↑s) i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun s => ↑s) i).Nonempty
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, (fun s => ↑s) i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Proof state:
case pos.h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ s, ↑s ⊆ a

Tactic:
suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ u
  from Disjoint.left_le_of_le_sup_right hab (huv.mono this hbv)

Result:
case pos.h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ s, ↑s ⊆ u

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  (∀ (u_1 : Finset { s // IsClopen s ∧ x ∈ s }), ((u ∪ v)ᶜ ∩ ⋂ i ∈ u_1, (fun s => ↑s) i).Nonempty) →
    ((u ∪ v)ᶜ ∩ ⋂ i, (fun s => ↑s) i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, (fun s => ↑s) i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, (fun s => ↑s) i).Nonempty
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
by_cases hxu : x ∈ u <;> [left; right]

Result:
case pos.h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ s, ↑s ⊆ a

case neg.h
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
a b : Set X
ha : IsClosed a
hb : IsClosed b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
⊢ ⋂ s, ↑s ⊆ b

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
⊢ IsPreconnected (⋂ Z, ↑Z)

Tactic:
have hs : @IsClosed X _ (⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, s) :=
  isClosed_iInter fun s => s.2.1.1

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
⊢ IsPreconnected (⋂ Z, ↑Z)