The Stacks project

Proof. Consider $V \to Y$ étale, $\{ U_ i \to X \times _ Y V\} $ an étale covering, and $v \in V$. We have to find a $V' \to V$ and decomposition and maps as in Lemma 59.43.2. We may shrink $V$ and $Y$, hence we may assume that $V$ and $Y$ are affine. Since $X$ is finite over $Y$, this also implies that $X$ is affine. During the proof we may (finitely often) replace $(V, v)$ by an étale neighbourhood $(V', v')$ and correspondingly the covering $\{ U_ i \to X \times _ Y V\} $ by $\{ V' \times _ V U_ i \to X \times _ Y V'\} $.

Since $X \times _ Y V \to V$ is finite there exist finitely many (pairwise distinct) points $x_1, \ldots , x_ n \in X \times _ Y V$ mapping to $v$. We may apply More on Morphisms, Lemma 37.41.5 to $X \times _ Y V \to V$ and the points $x_1, \ldots , x_ n$ lying over $v$ and find an étale neighbourhood $(V', v') \to (V, v)$ such that

with $T_ a \to V'$ finite with exactly one point $p_ a$ lying over $v'$ and moreover $\kappa (v') \subset \kappa (p_ a)$ purely inseparable, and such that $R \to V'$ has empty fibre over $v'$. Because $X \to Y$ is finite, also $R \to V'$ is finite. Hence after shrinking $V'$ we may assume that $R = \emptyset $. Thus we may assume that $X \times _ Y V = X_1 \amalg \ldots \amalg X_ n$ with exactly one point $x_ l \in X_ l$ lying over $v$ with moreover $\kappa (v) \subset \kappa (x_ l)$ purely inseparable. Note that this property is preserved under refinement of the étale neighbourhood $(V, v)$.

For each $l$ choose an $i_ l$ and a point $u_ l \in U_{i_ l}$ mapping to $x_ l$. Now we apply property (A) for the finite morphism $X \times _ Y V \to V$ and the étale morphisms $U_{i_ l} \to X \times _ Y V$ and the points $u_ l$. This is permissible by Lemma 59.42.3 This gives produces an étale neighbourhood $(V', v') \to (V, v)$ and decompositions

and $X$-morphisms $a_ l : W_ l \to U_{i_ l}$ whose image contains $u_{i_ l}$. Here is a picture:

After replacing $(V, v)$ by $(V', v')$ we conclude that each $x_ l$ is contained in an open and closed neighbourhood $W_ l$ such that the inclusion morphism $W_ l \to X \times _ Y V$ factors through $U_ i \to X \times _ Y V$ for some $i$. Replacing $W_ l$ by $W_ l \cap X_ l$ we see that these open and closed sets are disjoint and moreover that $\{ x_1, \ldots , x_ n\} \subset W_1 \cup \ldots \cup W_ n$. Since $X \times _ Y V \to V$ is finite we may shrink $V$ and assume that $X \times _ Y V = W_1 \amalg \ldots \amalg W_ n$ as desired. $\square$