case a.h
X : Type u_1
Y : Type ?u.306480
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.306495
γ✝ γ : Path x y
x✝ : ↑I
⊢ ↑(map γ (_ : Continuous id)) x✝ = ↑γ x✝
X : Type u_1
Y : Type ?u.306480
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.306495
γ✝ γ : Path x y
⊢ map γ (_ : Continuous id) = γ
ext
no goals
case a.h
X : Type u_1
Y : Type ?u.306480
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.306495
γ✝ γ : Path x y
x✝ : ↑I
⊢ ↑(map γ (_ : Continuous id)) x✝ = ↑γ x✝
rfl