no goals
X : Type u_1
Y : Type ?u.625357
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.625372
F : Set X
x y : X
h : y ∈ pathComponent x
⊢ ↑(Joined.somePath h) 0 = x
simp
no goals
X : Type u_1
Y : Type ?u.625357
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y✝ z : X
ι : Type ?u.625372
F : Set X
x y : X
h : y ∈ pathComponent x
⊢ ↑(Joined.somePath h) 1 = y
simp