case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ p₁ : Path x₀ x₁
F : Homotopy p₀ p₁
t : ↑I
⊢ ↑(eval F 0) t = ↑p₀ t
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ p₁ : Path x₀ x₁
F : Homotopy p₀ p₁
⊢ eval F 0 = p₀
ext t
no goals
case a.h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ p₁ : Path x₀ x₁
F : Homotopy p₀ p₁
t : ↑I
⊢ ↑(eval F 0) t = ↑p₀ t
simp [eval]