case a.h
X : Type u_1
Y : Type ?u.109539
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.109554
γ✝ γ : Path x y
t : ↑I
⊢ ↑(symm (symm γ)) t = ↑γ t
X : Type u_1
Y : Type ?u.109539
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.109554
γ✝ γ : Path x y
⊢ symm (symm γ) = γ
ext t
case a.h
X : Type u_1
Y : Type ?u.109539
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.109554
γ✝ γ : Path x y
t : ↑I
⊢ ↑γ (σ (σ t)) = ↑γ t
case a.h
X : Type u_1
Y : Type ?u.109539
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.109554
γ✝ γ : Path x y
t : ↑I
⊢ ↑(symm (symm γ)) t = ↑γ t
show γ (σ (σ t)) = γ t
no goals
case a.h
X : Type u_1
Y : Type ?u.109539
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.109554
γ✝ γ : Path x y
t : ↑I
⊢ ↑γ (σ (σ t)) = ↑γ t
rw [unitInterval.symm_symm]