Context:
Let $X$ and $Y$ be connected qcqs schemes over an algebraically closed field $k$. Denote by $\pi_1(X)$, $\pi_1(Y)$ their étale fundamental groups (base points omitted). Grothendieck proved that $\pi_1(X\times_{\mathrm{Spec}(k)} Y)\cong \pi_1(X)\times \pi_1(Y)$, given that one of the schemes, say $X$, is proper over $k$, see SGA1, Exposé X, Corollaire 1.7.
In their Berkeley lectures, Lemma 16.1.2, Scholze and Weinstein claim that this formula still holds under the relaxed assumption on $X$ that base change along any algebraically closed extension $\mathrm{Spec}(k')\rightarrow \mathrm{Spec}(k)$ induces an equivalence $\mathrm{FEt}(X_{k'})\cong\mathrm{FEt}(X)$ of finite étale covers. Kedlaya called this property "$\pi_1$-properness" (c.f. here, Definition 4.1.12). Non-trivial facts are that any proper scheme over an algebraically closed field is $\pi_1$-proper, see Tag 0A49 and also any scheme over an algebraically closed field of characteristic 0, see Section 16.1. In particular, $\pi_1$-properness is a weaker notion than properness.
Kedlaya has written up a proof of the Künneth formula under the relaxed assumption of $\pi_1$-properness, see Corollary 4.1.23. Similar to Grothendieck's original proof, the idea is to conclude the formula from a "homotopy exact sequence" of étale fundamental groups. In this context, one has to establish an analogue of Stein factorization of proper maps. A key step for this is the following claim (slightly modified from Lemma 4.1.21, Equation (4.1.21.1)):
Claim:
Let $X'\rightarrow \mathrm{Spec}(k)$ be a qcqs $\pi_1$-proper morphism over an algebraically closed field $k$. Let $S\rightarrow \mathrm{Spec}(k)$ be some scheme over $k$. Write $X:=X'\times_{\mathrm{Spec}(k)} S \rightarrow S$. (In particular, $X\rightarrow S$ is a qcqs morphism of schemes with geometrically connected, $\pi_1$-proper geometric fibers.) Then, for any geometric point $\bar{s}\rightarrow S$, base change $$\mathrm{FEt}(X\times_S \mathrm{lim}_U U) \rightarrow \mathrm{FEt}(X\times_S \bar{s})$$ is an equivalence of categories, where the limit is taken over all affine étale neighborhoods of $\bar{s}$ in $S$.
Question: Does this claim hold true?
Attempts:
Essential surjectivity holds, since by $\pi_1$-properness, any finite étale cover of $X\times_S \bar{s}$ descends to a cover of $X'$, which we can base change to $X\times_S \mathrm{lim}_U U$.
What about fully faithfulness? First observe that the following equivalences hold independently of the assumptions: $$\mathrm{FEt}(X\times_S \mathrm{lim}_U U) \cong \mathrm{FEt}(X\times_S \mathrm{Spec}(\mathcal{O}_{S,\bar{s}})),$$ where $\mathcal{O}_{S,\bar{s}}$ is the strictly henselian local ring at $\bar{s}$. If $\kappa$ is its residue field, choose an algebraic closure $\bar{\kappa}$ of $\kappa$ and observe that $\kappa \rightarrow \bar{\kappa}$ is purely inseparable, hence a universal homeomorphism on spectra. So we have $$\mathrm{FEt}(X\times_S \mathrm{Spec}(\kappa)) \cong \mathrm{FEt}(X\times_S \mathrm{Spec}(\bar{\kappa}))$$ and further by $\pi_1$-properness of $X'\rightarrow \mathrm{Spec}(k)$ $$\mathrm{FEt}(X\times_S \mathrm{Spec}(\bar{\kappa})) \cong \mathrm{FEt}(X\times_S \bar{s}).$$ So, we are left to show that $$\mathrm{FEt}(X\times_S \mathrm{Spec}(\mathcal{O}_{S,\bar{s}})) \rightarrow \mathrm{FEt}(X\times_S \mathrm{Spec}(\kappa)),$$ is fully faithful. If $X\rightarrow S$ was proper, this would hold by Tag 0GS2. But what happens under the above assumptions? If $S=\mathrm{Spec}(k)$ for some field $k$, then the claim would hold, since $\mathcal{O}_{S,\bar{s}}$ would in fact be a separable closure of $k$. For an arbitrary base $S$, we at least know that $X\times_S \mathrm{Spec}(\mathcal{O}_{S,\bar{s}})$ and $X\times_S \mathrm{Spec}(\kappa)$ are connected as a base changes of the geometrically connected $X'\rightarrow \mathrm{Spec}(k)$. Then both categories in question are Galois categories and hence base change from one to the other is faithful (compose with a geometric fiber functor, which is faithful). Hence we are left to show fullness. I tried to show that connected covers are sent to connected covers, which is equivalent to fully faithfulness by Tag 0BN6, without success.
Many thanks in advance for any thoughts on this problem.
Sidenote: This is related to this post, but unlike them, I am concerned about the step of concluding the Künneth formula from invariance under base extension.
