-- Mathlib/Topology/Connected/TotallyDisconnected.lean
theorem totallyDisconnectedSpace_iff_connectedComponent_subsingleton :
    TotallyDisconnectedSpace α ↔ ∀ x : α, (connectedComponent x).Subsingleton

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ (connectedComponent x).Subsingleton

Tactic:
apply h.1

Result:
case mp.a
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ connectedComponent x ⊆ univ

case mp.a
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) → TotallyDisconnectedSpace α

Tactic:
intro h

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ TotallyDisconnectedSpace α

Proof state:
case mp.a
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ connectedComponent x ⊆ univ

Tactic:
exact subset_univ _

Result:
no goals

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ TotallyDisconnectedSpace α

Tactic:
constructor

Result:
case mpr.isTotallyDisconnected_univ
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ IsTotallyDisconnected univ

Proof state:
case mpr.isTotallyDisconnected_univ.inl
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s_sub : ∅ ⊆ univ
hs : IsPreconnected ∅
⊢ ∅.Subsingleton

Tactic:
exact subsingleton_empty

Result:
no goals

Proof state:
case mpr.isTotallyDisconnected_univ
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
⊢ IsTotallyDisconnected univ

Tactic:
intro s s_sub hs

Result:
case mpr.isTotallyDisconnected_univ
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton

Proof state:
case mp.a
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)

Tactic:
exact isPreconnected_connectedComponent

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), (connectedComponent x).Subsingleton

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α → ∀ (x : α), (connectedComponent x).Subsingleton

case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) → TotallyDisconnectedSpace α

Proof state:
case mpr.isTotallyDisconnected_univ.inr.intro
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ s.Subsingleton

Tactic:
exact (h x).anti (hs.subset_connectedComponent x_in)

Result:
no goals

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ TotallyDisconnectedSpace α → ∀ (x : α), (connectedComponent x).Subsingleton

Tactic:
intro h x

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ (connectedComponent x).Subsingleton

Proof state:
case mpr.isTotallyDisconnected_univ
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)

Result:
case mpr.isTotallyDisconnected_univ.inl
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s_sub : ∅ ⊆ univ
hs : IsPreconnected ∅
⊢ ∅.Subsingleton

case mpr.isTotallyDisconnected_univ.inr.intro
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ s.Subsingleton