-- Mathlib/Topology/Connected/PathConnected.lean
theorem pathConnectedSpace_iff_zerothHomotopy :
    PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Tactic:
letI := pathSetoid X

Result:
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Tactic:
intro h

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Tactic:
constructor

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ Nonempty (Quotient (pathSetoid X)) ∧ Subsingleton (Quotient (pathSetoid X)) → PathConnectedSpace X

Tactic:
rintro ⟨h, h'⟩

Result:
case mpr.intro
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : Nonempty (Quotient (pathSetoid X))
h' : Subsingleton (Quotient (pathSetoid X))
⊢ PathConnectedSpace X

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X

Tactic:
unfold ZerothHomotopy

Result:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
⊢ Nonempty (Quotient (pathSetoid X)) ∧ Subsingleton (Quotient (pathSetoid X)) → PathConnectedSpace X

Proof state:
case mp.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
a✝ : ZerothHomotopy X
x : X
b✝ : ZerothHomotopy X
y : X
⊢ Quot.mk (⇑(pathSetoid X)) x = Quot.mk (⇑(pathSetoid X)) y

Tactic:
exact Quotient.sound (PathConnectedSpace.joined x y)

Result:
no goals

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

Tactic:
refine ⟨(nonempty_quotient_iff _).mpr h.1, ⟨?_⟩⟩

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ ∀ (a b : ZerothHomotopy X), a = b

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ ∀ (a b : ZerothHomotopy X), a = b

Tactic:
rintro ⟨x⟩ ⟨y⟩

Result:
case mp.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
a✝ : ZerothHomotopy X
x : X
b✝ : ZerothHomotopy X
y : X
⊢ Quot.mk (⇑(pathSetoid X)) x = Quot.mk (⇑(pathSetoid X)) y

Proof state:
case mpr.intro
X : Type u_1
inst✝ : TopologicalSpace X
this : Setoid X := pathSetoid X
h : Nonempty (Quotient (pathSetoid X))
h' : Subsingleton (Quotient (pathSetoid X))
⊢ PathConnectedSpace X

Tactic:
exact ⟨(nonempty_quotient_iff _).mp h, fun x y => Quotient.exact <| Subsingleton.elim ⟦x⟧ ⟦y⟧⟩

Result:
no goals