[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
y : Y
⊢ Homotopic (const X y) (const X y)
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : Nullhomotopic f
g : C(Y, Z)
⊢ Nullhomotopic (comp g f)
[PROOFSTEP]
cases' hf with y hy
[GOAL]
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : Homotopic f (const X y)
⊢ Nullhomotopic (comp g f)
[PROOFSTEP]
use g y
[GOAL]
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
g : C(Y, Z)
y : Y
hy : Homotopic f (const X y)
⊢ Homotopic (comp g f) (const X (↑g y))
[PROOFSTEP]
exact Homotopic.hcomp hy (Homotopic.refl g)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
hf : Nullhomotopic f
g : C(X, Y)
⊢ Nullhomotopic (comp f g)
[PROOFSTEP]
cases' hf with y hy
[GOAL]
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : Homotopic f (const Y y)
⊢ Nullhomotopic (comp f g)
[PROOFSTEP]
use y
[GOAL]
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
g : C(X, Y)
y : Z
hy : Homotopic f (const Y y)
⊢ Homotopic (comp f g) (const X y)
[PROOFSTEP]
exact Homotopic.hcomp (Homotopic.refl g) hy
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
⊢ Nullhomotopic (ContinuousMap.id X)
[PROOFSTEP]
obtain ⟨hv⟩ := ContractibleSpace.hequiv_unit X
[GOAL]
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ Nullhomotopic (ContinuousMap.id X)
[PROOFSTEP]
use hv.invFun ()
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : ContractibleSpace X
hv : X ≃ₕ Unit
⊢ Homotopic (ContinuousMap.id X) (const X (↑hv.invFun ()))
[PROOFSTEP]
convert hv.left_inv.symm
[GOAL]
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y ↔ Nullhomotopic (ContinuousMap.id Y)
[PROOFSTEP]
constructor
[GOAL]
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ ContractibleSpace Y → Nullhomotopic (ContinuousMap.id Y)
[PROOFSTEP]
intro
[GOAL]
case mp
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : ContractibleSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y)
[PROOFSTEP]
apply id_nullhomotopic
[GOAL]
case mpr
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ Nullhomotopic (ContinuousMap.id Y) → ContractibleSpace Y
[PROOFSTEP]
rintro ⟨p, h⟩
[GOAL]
case mpr.intro
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ ContractibleSpace Y
[PROOFSTEP]
refine
  {
    hequiv_unit' :=
      ⟨{  toFun := ContinuousMap.const _ ()
          invFun := ContinuousMap.const _ p
          left_inv := ?_
          right_inv := ?_ }⟩ }
[GOAL]
case mpr.intro.refine_1
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Unit p) (const Y ())) (ContinuousMap.id Y)
[PROOFSTEP]
exact h.symm
[GOAL]
case mpr.intro.refine_2
Y : Type u_1
inst✝ : TopologicalSpace Y
p : Y
h : Homotopic (ContinuousMap.id Y) (const Y p)
⊢ Homotopic (comp (const Y ()) (const Unit p)) (ContinuousMap.id Unit)
[PROOFSTEP]
convert Homotopic.refl (ContinuousMap.id Unit)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
⊢ PathConnectedSpace X
[PROOFSTEP]
obtain ⟨p, ⟨h⟩⟩ := id_nullhomotopic X
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
⊢ PathConnectedSpace X
[PROOFSTEP]
have : ∀ x, Joined p x := fun x => ⟨(h.evalAt x).symm⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
⊢ PathConnectedSpace X
[PROOFSTEP]
rw [pathConnectedSpace_iff_eq]
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
⊢ ∃ x, pathComponent x = Set.univ
[PROOFSTEP]
use p
[GOAL]
case h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
⊢ pathComponent p = Set.univ
[PROOFSTEP]
ext
[GOAL]
case h.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ContractibleSpace X
p : X
h : Homotopy (ContinuousMap.id X) (const X p)
this : ∀ (x : X), Joined p x
x✝ : X
⊢ x✝ ∈ pathComponent p ↔ x✝ ∈ Set.univ
[PROOFSTEP]
tauto
