Recently fellow user Thorgott pointed out to me that flat restrictions of flat modules remain flat. That is, let $f : A \to B$ be a flat morphism of rings and $M$ be a flat $B$-module. Then considering $M$ as an $A$-module by basechanging along $f$, it is still flat.
The proof goes as follows: Let $Q \to N$ be an injection of $A$-module. Tensoring with $B$ over $A$, we obtain an injection $Q \otimes_A B \to N \otimes_A B$, by flatness of $B$ as an $A$-module using the module structure coming from $f$. We can further tensor with $M$ as a $B$-module to obtain an injection $(Q \otimes_A B) \otimes_B M \to (N \otimes_A B) \otimes_B M$ by using flatness of $M$ as a $B$-module this time. At this point Thorgott observes that $(N \otimes_A B) \otimes_B M$ is naturally isomorphic as $A$-modules to $N \otimes_A M$, with the isomorphism given by $(N \otimes_A B) \otimes_B M \to N \otimes_A M$, $(x \otimes_A b) \otimes_B m \mapsto x \otimes_A bm$. This is straightforward to check.
Here is a curious way to state the identity. Let $f_* : \mathsf{Mod}_B \to \mathsf{Mod}_A$ be restriction of scalars functor and $f^* : \mathsf{Mod}_A \to \mathsf{Mod}_B$ be extension of scalars functor. Then for an $A$-module $N$ and a $B$-module $M$, there is a natural isomorphism: $$N \otimes_A f_* M \cong_{\mathsf{Mod}_A} f_*(f^* N \otimes_B M)$$
Always being a bit bad at algebra I did not notice the straightforward isomorphism above, and kept noticing the formal similarity between this identity and the adjunction between $f^*$ and $f_*$, but mysteriously the $\operatorname{Hom}$ has been replaced with $\otimes$. Indeed, this does not seem to follow from $f^*$-$f_*$ adjunction and $\otimes$-$\operatorname{Hom}$ adjunction relations in any straightforward way.
Assume for a moment that there is a functor $f^! : \mathsf{Mod}_A \to \mathsf{Mod}_B$ which is right-adjoint to $f_*$, that is to say, $\operatorname{Hom}_A(f_* Y, X) \cong f_* \operatorname{Hom}_B(Y, f^! X)$ for any $A$-module $X$ and $B$-module $Y$. The following sequence of utterly symbolic calculation ensues in an unhinged attempt to prove the aforementioned identity:
$$\begin{aligned}\operatorname{Hom}_A(f_*(f^* N \otimes_B M), P) &\cong f_* \operatorname{Hom}_B(f^* N \otimes_B M, f^! P) \\ &\cong f_* \operatorname{Hom}_B(f^* N, \operatorname{Hom}_B(M, f^! P)) \\ &\cong \operatorname{Hom}_A(N, f_* \operatorname{Hom}_B(M, f^! P)) \\ &\cong \operatorname{Hom}_A(N, \operatorname{Hom}_A(f_* M, P)) \\ &\cong \operatorname{Hom}_A(N \otimes_A f_* M, P)\end{aligned}$$
Since this holds for every $A$-module $P$, we would have proved $f_*(f^* N \otimes_B M) \cong N \otimes_A f_* M$. Except there is no such functor $f^!$, and in fact such a right-adjoint $f^! : \mathsf{Sh}(\operatorname{Spec} A) \to \mathsf{Sh}(\operatorname{Spec} B)$ to $f_*$ does not even exist at the level of sheaves, much less quasicoherent sheaves (Edit: This is not correct, the identity above tells essentially that $f^!(-) = \operatorname{Hom}_A(B, -)$ is the right-adjoint. See Roland's comments below). But once we pass to the derived category of complexes of sheaves, $f^! : D(\operatorname{Spec} A) \to D(\operatorname{Spec} B)$ exists as a right-adjoint to the derived pushforward $Rf_*$, see eg here. So it seems we can do the above computation by passing to the derived category, in which case we obtain an analogous derived version of the relation, $\mathscr{F} \otimes^{L}_Y Rf_* \mathscr{G} \cong Rf_* (Lf^* \mathscr{F} \otimes_X^{L} \mathscr{G})$ for any morphism $f : X \to Y$ between quasi-separated quasi-compact schemes, and $\mathscr{F}$, $\mathscr{G}$ being sheaves of $\mathscr{O}_Y$, $\mathscr{O}_X$-modules respectively.
In our particular case, it seems we can simply take the homology at the $0$-th grade (or the $0$-th derived functors) to obtain the isomorphism at the level of modules even though the calculation was happening in the derived category of sheaves or whatever. My question is, does this madness actually work? And is there an example of a more useful scenario where these kind of abstract arguments lets one avoid elementwise manipulation to prove certain identities? It seems the point of six functors formalism is that since everything is axiomatized, one doesn't need to think much to write these identities down. How wrong am I? This might be an extremely dumb question, I have close to no experience with these things. Apologies in advance.