-- Mathlib/Topology/Connected/Basic.lean
theorem preconnectedSpace_iff_connectedComponent :
    PreconnectedSpace α ↔ ∀ x : α, connectedComponent x = univ

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), connectedComponent x = univ) → PreconnectedSpace α

Tactic:
intro h

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
⊢ PreconnectedSpace α

Proof state:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected ∅

Tactic:
exact isPreconnected_empty

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected univ

Tactic:
rw [univ_eq_empty_iff.mpr hα]

Result:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected ∅

Proof state:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))

Tactic:
exact isPreconnected_connectedComponent

Result:
no goals

Proof state:
case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ PreconnectedSpace α

Tactic:
exact ⟨by rw [univ_eq_empty_iff.mpr hα]; exact isPreconnected_empty⟩

Result:
no goals

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ

Tactic:
exact eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)

Result:
no goals

Proof state:
case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ PreconnectedSpace α

Tactic:
exact ⟨by rw [← h (Classical.choice hα)]; exact isPreconnected_connectedComponent⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected univ

Tactic:
rw [← h (Classical.choice hα)]

Result:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace α ↔ ∀ (x : α), connectedComponent x = univ

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ

case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), connectedComponent x = univ) → PreconnectedSpace α

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ

Tactic:
intro h x

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
h : PreconnectedSpace α
x : α
⊢ connectedComponent x = univ

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
⊢ PreconnectedSpace α

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Result:
case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ PreconnectedSpace α

case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ PreconnectedSpace α