X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
letI := pathSetoid X
case mp
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)

case mpr
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
constructor
case mp
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
case mp
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
⊢ PathConnectedSpace X → Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
intro h
case mp
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ ∀ (a b : ZerothHomotopy X), a = b
case mp
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
refine' ⟨(nonempty_quotient_iff _).mpr h.1, ⟨_⟩⟩
case mp.mk.mk
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
a✝ : ZerothHomotopy X
x : X
b✝ : ZerothHomotopy X
y : X
⊢ Quot.mk Setoid.r x = Quot.mk Setoid.r y
case mp
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
⊢ ∀ (a b : ZerothHomotopy X), a = b
rintro ⟨x⟩ ⟨y⟩
no goals
case mp.mk.mk
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : PathConnectedSpace X
a✝ : ZerothHomotopy X
x : X
b✝ : ZerothHomotopy X
y : X
⊢ Quot.mk Setoid.r x = Quot.mk Setoid.r y
exact Quotient.sound (PathConnectedSpace.Joined x y)
case mpr
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
⊢ Nonempty (Quotient (pathSetoid X)) ∧ Subsingleton (Quotient (pathSetoid X)) → PathConnectedSpace X
case mpr
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
⊢ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X) → PathConnectedSpace X
unfold ZerothHomotopy
case mpr.intro
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : Nonempty (Quotient (pathSetoid X))
h' : Subsingleton (Quotient (pathSetoid X))
⊢ PathConnectedSpace X
case mpr
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
⊢ Nonempty (Quotient (pathSetoid X)) ∧ Subsingleton (Quotient (pathSetoid X)) → PathConnectedSpace X
rintro ⟨h, h'⟩
case mpr.intro
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : Nonempty (Quotient (pathSetoid X))
h' : Subsingleton (Quotient (pathSetoid X))
⊢ PathConnectedSpace X
case mpr.intro
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : Nonempty (Quotient (pathSetoid X))
h' : Subsingleton (Quotient (pathSetoid X))
⊢ PathConnectedSpace X
skip
no goals
case mpr.intro
X : Type u_1
Y : Type ?u.687930
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.687945
F : Set X
this : Setoid X := pathSetoid X
h : Nonempty (Quotient (pathSetoid X))
h' : Subsingleton (Quotient (pathSetoid X))
⊢ PathConnectedSpace X
exact ⟨(nonempty_quotient_iff _).mp h, fun x y => Quotient.exact <| Subsingleton.elim ⟦x⟧ ⟦y⟧⟩