no goals
α : Type u
β : Type v
ι : Type ?u.46668
π : ι → Type ?u.46673
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hx : x ∈ F
⊢ x ∈ connectedComponentIn F x
simp [connectedComponentIn_eq_image hx, mem_connectedComponent, hx]