Background:
I've seen two versions of the homotopy exact sequence for etale fundamental groups. One from Stacks:
Stacks 0BTX: Let $k$ be a field with algebraic closure $\overline{k}$. Let $X$ be a quasi-compact and quasi-separated scheme over $k$. If the base change $X_{\overline{k}}$ is connected, then there is a short exact sequence $$ 1\to \pi_1(X_{\overline{k}}) \to \pi_1(X)\to \pi_1(\operatorname{Spec} k) \to 1$$ of profinite topological groups.
And one from SGA:
SGA I, Theoreme 6.1 of chapter IX: Suppose $S$ is the spectrum of an Artinian ring $A$ with residue field $k$, $\overline{k}$ an algebraic closure of $k$, $X$ a $S$-scheme, $X_0=X\times_A k$, $\overline{X}_0=X\times_A \overline{k}$, $\overline{a}$ a geometric point of $\overline{X}$, $a$ the image in $X$, and $b$ the image in $S$. We suppose that $X_0$ is quasi-compact and geometrically connected over $k$ (N.B. if $X$ is proper over $S$, this means that $H^0(X_0,\mathcal{O}_{X_0})$ is an artinian local ring whose residue field is radicial over $k$). Then the canonical sequence of homomorphisms $$1\to \pi_1(\overline{X}_0,\overline{a})\to \pi_1(X,a)\to \pi_1(S,b) \to 1$$ is exact, and we have $$\pi_1(S,b)\stackrel{\sim}{\leftarrow}\pi_1(k,\overline{k})= Gal(\overline{k},k).$$
A key step in both of these proofs is the following lemma:
Lemma: Let $X$ be quasi-compact and geometrically connected. If we have a finite etale cover $\overline{Y}$ of $\overline{X}=X\times_k \operatorname{Spec}\overline{k}$, then it comes from a finite etale cover of $X\times_k \operatorname{Spec} K$, where $k\subset K$ is a finite extension.
Stacks adds the assumption that $X$ is quasi-separated, and SGA omits this assumption. In the case when $X$ is assumed quasi-separated, I think I understand how to show this lemma and I can even write down a recipe for producing the extension we need: using the fact that $X$ is quasi-compact and quasi-separated in combination with the definition of etale morphisms as locally of finite presentation, we can pick a finite affine open cover $U_i=\operatorname{Spec} A_i$ of $X$ and get a finite affine open cover $\overline{U_i}=U_i\times_k \operatorname{Spec} \overline{k}$ of $\overline{Y}$ by spectra of rings of the form $(A_i\otimes_k \overline{k})[x_1,\cdots,x_n]/(f_1,\cdots,f_m)$ which gives us a finite list of coefficients from $\overline{k}$ needed to define the $\overline{U_i}$. Covering $U_i\cap U_j$ with a finite number of open affines $U_{ijk}$ since $X$ is quasi-separated, we see that there's a finite number of coefficients from $\overline{k}$ necessary to define the maps $\overline{U_{ijk}}\to \overline{U_i}$ and $\overline{U_{ijk}}\to \overline{U_j}$, and we can apply the same trick to get a finite list of coefficients of $\overline{k}$ needed to define the data we use to patch together the $\overline{U_i}$ into $\overline{Y}$. We end up with a finite list of elements of $\overline{k}$ which are enough to specify all the data needed to put together $\overline{Y}$, and we can define our cover over a finite extension of $k$ containing all these elements.
Question: How can I prove the lemma when $X$ is not quasi-separated? SGA leaves the proof of the lemma to the reader, and it appears to me that my strategy fails without the quasi-separated hypothesis (some $U_i\cap U_j$ could fail to be quasi-compact and then I would have to deal with a potentially infinite list of elements of $\overline{k}$). Stacks' copy of the lemma seems to rely on quasi-separatedness in an essential way, and I don't see how to remove it.
