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?