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$.