case intro
X : Type u_3
Y : Type u_1
Z : Type u_2
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)
X : Type u_3
Y : Type u_1
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(Y, Z)
hf : Nullhomotopic f
g : C(X, Y)
⊢ Nullhomotopic (comp f g)
cases' hf with y hy
case intro
X : Type u_3
Y : Type u_1
Z : Type u_2
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)
case intro
X : Type u_3
Y : Type u_1
Z : Type u_2
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)
use y
no goals
case intro
X : Type u_3
Y : Type u_1
Z : Type u_2
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)
exact Homotopic.hcomp (Homotopic.refl g) hy