case a.h
X : Type u_1
Y : Type ?u.540911
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.540926
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x✝ : ↑I
⊢ ↑(reparam (refl x) f hfcont hf₀ hf₁) x✝ = ↑(refl x) x✝
X : Type u_1
Y : Type ?u.540911
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.540926
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ reparam (refl x) f hfcont hf₀ hf₁ = refl x
ext
no goals
case a.h
X : Type u_1
Y : Type ?u.540911
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.540926
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x✝ : ↑I
⊢ ↑(reparam (refl x) f hfcont hf₀ hf₁) x✝ = ↑(refl x) x✝
simp