**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][1], 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$-propernesss" (c.f. [here, Definition 4.1.12][2]). Non-trivial facts are that any proper scheme over an algebraically closed field is $\pi_1$-proper, see [Tag 0A49][3] and also any scheme over an algebraically closed field of characteristic 0, see [Section 16.1][4]. 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][5]. 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))][6]: 

**Claim:** 

Let $X'\rightarrow \mathrm{Spec}(k)$ be a $\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][7].
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][8], without success. 

Many thanks in advance for any thoughts on this problem.

Sidenote: This is related to [this post][9], but unlike them, I am concerned about the step of concluding the Künneth formula from invariance under base extension.


  [1]: https://www.math.uni-bonn.de/people/scholze/Berkeley.pdf#page=151
  [2]: https://swc-math.github.io/aws/2017/2017KedlayaNotes.pdf#page=94
  [3]: https://stacks.math.columbia.edu/tag/0A49
  [4]: https://www.math.uni-bonn.de/people/scholze/Berkeley.pdf#page=150
  [5]: https://swc-math.github.io/aws/2017/2017KedlayaNotes.pdf#page=97
  [6]: https://swc-math.github.io/aws/2017/2017KedlayaNotes.pdf#page=96
  [7]: https://stacks.math.columbia.edu/tag/0GS2
  [8]: https://stacks.math.columbia.edu/tag/0BN6
  [9]: https://mathoverflow.net/questions/379108/fundamental-group-of-a-product-in-characteristic-0