no goals
X : Type u_1
Y : Type ?u.633769
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x✝ y z : X
ι : Type ?u.633784
F : Set X
x : X
⊢ pathComponentIn x univ = pathComponent x
simp [pathComponentIn, pathComponent, JoinedIn, Joined, exists_true_iff_nonempty]