[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
⊢ SimplyConnectedSpace X ↔ Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
rw [simply_connected_def, equiv_punit_iff_unique]
[GOAL]
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (Nonempty (FundamentalGroupoid X) ∧ ∀ (x y : FundamentalGroupoid X), Nonempty (Unique (x ⟶ y))) ↔
    Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SimplyConnectedSpace X
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
rw [simply_connected_iff_unique_homotopic] at *
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty X ∧ ∀ (x y : X), Nonempty (Unique (Path.Homotopic.Quotient x y))
x y : X
⊢ Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
tauto
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y → PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
[PROOFSTEP]
intro
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
[PROOFSTEP]
constructor
[GOAL]
case left
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y
[PROOFSTEP]
infer_instance
[GOAL]
case right
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
[PROOFSTEP]
infer_instance
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y
[PROOFSTEP]
cases h
[GOAL]
case intro
Y : Type u_1
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y
[PROOFSTEP]
rw [simply_connected_iff_unique_homotopic]
[GOAL]
case intro
Y : Type u_1
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ Nonempty Y ∧ ∀ (x y : Y), Nonempty (Unique (Path.Homotopic.Quotient x y))
[PROOFSTEP]
exact ⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), Path.Homotopic p₁ p₂
[PROOFSTEP]
convert simply_connected_iff_paths_homotopic (Y := Y)
[GOAL]
case h.e'_2.h.e'_2.h.h.a
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), Path.Homotopic p₁ p₂) ↔ Subsingleton (Path.Homotopic.Quotient a✝¹ a✝)
[PROOFSTEP]
simp [Path.Homotopic.Quotient, Setoid.eq_top_iff]
[GOAL]
case h.e'_2.h.e'_2.h.h.a
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝¹ a✝ : Y
⊢ (∀ (p₁ p₂ : Path a✝¹ a✝), Path.Homotopic p₁ p₂) ↔ ∀ (x y : Path a✝¹ a✝), Setoid.Rel (Path.Homotopic.setoid a✝¹ a✝) x y
[PROOFSTEP]
rfl
