Inverse function theorem for etale morphisms Looking around stackexchange, it seems there are many related questions, but I'm a beginner and I can't find a proof on the internet (without going through the more general results in stacks project). 
If $X\rightarrow Y$ is an etale map, wikipedia (https://en.wikipedia.org/wiki/%C3%89tale_morphism#.C3.89tale_morphisms_and_the_inverse_function_theorem) says that, for each $y\in Y$ we can find an etale morphism $V\rightarrow Y$ containing $y$ in its image, such that $X\times_Y V\rightarrow V$ is a disjoint union of finitely many copies of $V$ mapping to $V$. Why is this true?
For example, if $X$ is the affine line with a doubled origin, and $Y$ is the usual affine line, then how do we do this in a neighbourhood of the origin?

If I try to mutter the words I've just googled, the best I can put together is something like: 
1) Base changing by $X\rightarrow Y$, the map $X\times_Y X\rightarrow X$ is also etale, and it has a section $s$.
2) By some cancellation property for etale morphisms, the section $s$ is also etale, hence is an open map. 
3) If we assume $X\rightarrow Y$ is also separated (not satisfied in example above), then $s$ is also a closed immersion, so it is an isomorphism onto a connected component of $X\times_Y X$. 
4) Now, remove that connected component and repeat this steps above. 
 A: Let $A$ be a strictly henselian DVR with maximal ideal $\mathfrak{m}$, residue field $k = A/\mathfrak{m}$, and fraction field $K$ (e.g. $A = k[[t]]$ where $k$ is a separably closed field). Set $Y = \operatorname{Spec} A$ and let $\xi \in Y$ be the closed point. Set $X = \operatorname{Spec} A \amalg \operatorname{Spec} K$ and let $f : X \to Y$ be the canonical map. Suppose there exists an etale neighborhood $g : V \to Y$ of $\xi$ such that $X \times_{f,Y,g} V$ is a disjoint union of finitely many copies of $V$. By EGA IV (18.5.11) (a) $\implies$ (b) and the fact that, since $k$ is separably closed, any smooth $k$-scheme has a $k$-point (Stacks Tag 055T), the map $g$ has a section $s : Y \to V$. Then $(X \times_{f,Y,g} V) \times_{V,s} Y \simeq X$ should be a disjoint union of finitely many copies of $Y$, which is false.
Instead we can find some Zariski open subset $U \subseteq X \times_{Y} V$ such that the restriction $U \to X \times_{Y} V \to V$ is a finite morphism, see EGA IV (18.12.1).
I think your example shows that we cannot guarantee that $X \times_{Y} V \to V$ is itself a finite morphism since it may not even be separated (Stacks Tag 02KU).
