no goals
α : Type u_1
β : Type u_2
γ : Type ?u.24737
δ : Type ?u.24740
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e✝ : LocalHomeomorph α β
e' : LocalHomeomorph β γ
e : LocalHomeomorph α β
x : α
hx : x ∈ e.source
x' : α
hx' : ↑(LocalHomeomorph.symm e) (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' ∈ {x}
rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']