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