-- Mathlib/Topology/Connected/TotallyDisconnected.lean
theorem isTotallyDisconnected_of_isClopen_set {X : Type*} [TopologicalSpace X]
    (hX : Pairwise fun x y => ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∉ U) :
    IsTotallyDisconnected (Set.univ : Set X)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
hU : IsClopen U
hxU : x ∈ U
hyU : y ∉ U
hS : (S ∩ (U ∩ Uᶜ)).Nonempty
⊢ False

Tactic:
rw [inter_compl_self, Set.inter_empty] at hS

Result:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
hU : IsClopen U
hxU : x ∈ U
hyU : y ∉ U
hS : ∅.Nonempty
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
hU : IsClopen U
hxU : x ∈ U
hyU : y ∉ U
⊢ False

Tactic:
specialize
  hS U Uᶜ hU.2 hU.compl.2 (fun a _ => em (a ∈ U)) ⟨x, hx, hxU⟩ ⟨y, hy, hyU⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
hU : IsClopen U
hxU : x ∈ U
hyU : y ∉ U
hS : (S ∩ (U ∩ Uᶜ)).Nonempty
⊢ False

Proof state:
case intro.intro.intro.intro
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
⊢ False

Tactic:
obtain ⟨U, hU, hxU, hyU⟩ := hX hxy

Result:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
hU : IsClopen U
hxU : x ∈ U
hyU : y ∉ U
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
U : Set X
hU : IsClopen U
hxU : x ∈ U
hyU : y ∉ U
hS : ∅.Nonempty
⊢ False

Tactic:
exact Set.not_nonempty_empty hS

Result:
no goals

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
⊢ S.Subsingleton

Tactic:
unfold Set.Subsingleton

Result:
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
⊢ ∀ ⦃x : X⦄, x ∈ S → ∀ ⦃y : X⦄, y ∈ S → x = y

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
h_contra : ∃ x ∈ S, ∃ y ∈ S, x ≠ y
⊢ False

Tactic:
rcases h_contra with ⟨x, hx, y, hy, hxy⟩

Result:
case intro.intro.intro.intro
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
hxy : x ≠ y
⊢ False

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
⊢ IsTotallyDisconnected univ

Tactic:
rintro S - hS

Result:
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
⊢ S.Subsingleton

Proof state:
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
⊢ ∀ ⦃x : X⦄, x ∈ S → ∀ ⦃y : X⦄, y ∈ S → x = y

Tactic:
by_contra! h_contra

Result:
X : Type u_3
inst✝ : TopologicalSpace X
hX : Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
S : Set X
hS : IsPreconnected S
h_contra : ∃ x ∈ S, ∃ y ∈ S, x ≠ y
⊢ False