Künneth formula for de Rham cohomology with respect to an integrable connection I am reading through https://stacks.math.columbia.edu/tag/0FM9 which proves that for $X,Y$ schemes over some base $S$ and $X \times _S Y \overset{p}{\rightarrow} X$ resp. $X \times _S Y \overset{q}{\rightarrow} Y$ the projection morphisms,  there is an isomorphism of complexes $$ \mathrm{Tot}(p^{-1} \Omega^{\bullet}_{X/S} \otimes_{f^{-1}\mathcal{O}_S} q^{-1} \Omega^{\bullet}_{Y/S}) \rightarrow \Omega_{X\times_S Y} ^{\bullet},$$ where $f:X \times_S Y \rightarrow S$ is the structure map. Now, I am wondering whether we can show something like this for de Rham complexes with respect to integrable connections, i.e. let $(E, \nabla_E)$ and $(F,\nabla_F)$ be vector bundles over $\mathcal{O}_X$ and $\mathcal{O}_Y$ with integrable connections. We then get an integrable connection $p^{\ast}\nabla_E \otimes q^{\ast}\nabla_F$ on $p^{\ast}E \otimes q^{\ast}F$ do we have an isomorphism of complexes $$\mathrm{Tot}(p^{-1}(E \otimes \Omega^{\bullet}_{X/S}) \otimes_{f^{-1}\mathcal{O}_S} q^{-1}(F \otimes  \Omega^{\bullet}_{Y/S})) \rightarrow  p^{\ast}E \otimes q^{\ast}F \otimes \Omega_{X\times_S Y} ^{\bullet},$$ with the differentials induced by the connections?
EDIT: There seem to be some problems with this StacksPorject section since 0FLS is wrong. Nevertheless, the isomorphism of complexes should still exist if we replace all inverse image functors by pull-backs and tensor over $\mathcal{O}_{X\times_S Y}$ instead of $f^{-1}\mathcal{O}_S$.
 A: The corrected formulation of the K"unneth formula in the Stacks project can also be used to given an answer this question. Let me explain.
Observe that the differentials in the de Rham complex $E \otimes \Omega^\bullet_{X/S}$ of $(E, \nabla_E)$ are differential operators of finite order and similarly for $(F, \nabla_F)$. The construction in Section 0G4A therefore produces a complex $T^\bullet$ on $X \times_S Y$ whose terms are
$$
T^n = \left(E \boxtimes F\right) \otimes_{\mathcal{O}_{X \times_S Y}} \left( \bigoplus_{n = a + b} \Omega^a_{X/S} \boxtimes \Omega^b_{Y/S}\right) = (E \boxtimes F) \otimes_{\mathcal{O}_{X \times_S Y}} \Omega^n_{X \times_S Y}
$$
A local calculation shows that the differentials of this complex are coming from the integrable connection $\nabla_{E \boxtimes F}$ we obtain on $E \boxtimes F$ using $\nabla_E$ and $\nabla_F$.
Asssume $S = \text{Spec}(A)$ is affine for simplicity. The discussion in Section 0G4A also constructs a cup product map in the derived category D(A)
$$
R\Gamma(X, E \otimes \Omega^\bullet_{X/S}) \otimes_A^\mathbf{L} R\Gamma(Y, F \otimes \Omega^\bullet_{Y/S}) \longrightarrow R\Gamma(X \times_S Y, (E \boxtimes F) \otimes \Omega_{X \times_S Y/S})
$$
on the (total) de Rham cohomology of the given modules with integrable connections. Of course this won't always be an isomorphism! But Lemma 0FLT shows that is an isomorphism when $X \to S$ and $Y \to S$ are smooth, quasi-compact, and have affine diagonal. If in addition $A$ is a field or more generally if the de Rham cohomology modules $H^i_{dR}(E) = H^i(R\Gamma(X, E \otimes \Omega^\bullet_{X/S}))$ are flat $A$-modules for all $i$, then we obtain the more familiar
$$
H^m_{dR}(E \boxtimes F) = \bigoplus_{m = i + j} H^i_{dR}(E) \otimes_A H^j_{dR}(F)
$$
Hope this helps.
A: if you are ok with changing the language a little bit, then this is on p. 47 in this book http://www.math.ubc.ca/~cautis/dmodules/hottaetal.pdf plus Saito's Theorem 0.1 in MHM https://www.ems-ph.org/journals/show_pdf.php?issn=0034-5318&vol=26&iss=2&rank=2.
Note that an $\mathcal{O}_X$-coherent sheaf is a D-module if and only it is a vector bundle with integrable connection. You can recover the D-module structure from your connection as follows: given $\mathscr{E} \to \Omega_X^1\otimes\mathscr{E}$ you can recover the D-module, i.e. the action of the tangent bundle via $\mathcal{T}_X\otimes \mathscr{E} \to \mathcal{T}_X\otimes\Omega_X^1\otimes\mathscr{E} \to \mathscr{E}$. For the sake of being pedantic, you can also check from Section 1.3 of the same book that for smooth morphisms, $f^*\scr{E}$ as a D-module will be the one coming from $(f^*\mathscr{E}, f^*\nabla)$. Now it should be the compatibility of de Rham fuctor with exterior product as in Theorem 0.1 of Saito. Perhaps for vector bundle with integrable connectoins Saito's theorem 0.1 was known before him?
As commented below this argument works for $S = \operatorname{Spec}\mathbb{C}$.
