-- 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 intro.refine_3
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
⊢ ⋂ U ∈ si, ↑U ⊆ u ∪ v

Tactic:
rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
  ← not_nonempty_iff_eq_empty]

Result:
no goals

Proof state:
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

Tactic:
refine ⟨⋂ U ∈ si, Subtype.val U, ?_, ?_, ?_⟩

Result:
case intro.refine_1
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
⊢ IsClopen (⋂ U ∈ si, ↑U)

case intro.refine_2
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
⊢ x ∈ ⋂ U ∈ si, ↑U

case intro.refine_3
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
⊢ ⋂ U ∈ si, ↑U ⊆ u ∪ v

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

Tactic:
rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs]

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed (⋂ s, ↑s)
⊢ ∀ (u v : Set X), IsClosed u → IsClosed v → ⋂ s, ↑s ⊆ u ∪ v → Disjoint u v → ⋂ s, ↑s ⊆ u ∨ ⋂ s, ↑s ⊆ v

Proof state:
case intro.refine_2
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
⊢ x ∈ ⋂ U ∈ si, ↑U

Tactic:
exact mem_iInter₂.2 fun s _ => s.2.2

Result:
no goals

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
⊢ ∃ s, IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v

Tactic:
have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty
  (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s) 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)
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

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
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∈ u
⊢ ⋂ s, ↑s ⊆ s ∩ u

Tactic:
exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
  ⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩

Result:
no goals

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 ⊆ b

Tactic:
suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ v
  from (huv.symm.mono this hau).left_le_of_le_sup_left hab

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 ⊆ v

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
⊢ ⋂ Z, ↑Z ⊆ connectedComponent x

Tactic:
refine IsPreconnected.subset_connectedComponent ?_ (mem_iInter.2 fun s => s.2.2)

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

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
⊢ connectedComponent x = ⋂ s, ↑s

Tactic:
apply Subset.antisymm connectedComponent_subset_iInter_isClopen

Result:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
⊢ ⋂ Z, ↑Z ⊆ connectedComponent x