This question has been asked many times in math overflow, but I can't find justification in any of them in a particular step. I will be using the following theorems.
Theorem 1:
Let $A,B$ be rings and $M'$ be an $A$ module and $P'$ an $B$ module. Also let $N'$ be a $(A,B)$ bimodule.
Then
$(i)$: $M' \otimes _A N'$, $N' \otimes _ B P'$ are each naturally an $(A,B)$ bimodule.
$(ii)$ We have $(M' \otimes _ A (N' \otimes _B P') \cong (M' \otimes _A N') \otimes _B P'$ as $(A,B)$ bimodules (both expressions make sense by using $i$ twice on each side.
Let $A$ be a ring, $T = S^{-1} A$ some localization, and $M$ an $A$ module.
Theorem 2:
$S^{-1} M \cong T \otimes _A M$ as $T$ modules (where the right side has $T$ module structure from above since $T$ is an $(A,T)$ bimodule).
I will also be using the easy fact that $M \otimes _A N \cong N \otimes _A M$ for $A$ modules $N,M$ without mentioning when I use it.
We now attempt to prove the following:
Let $M,N$ be $A$ modules, then:
$S^{-1}(M \otimes _A N) \cong S^{-1}N \otimes _T S^{-1}M$ as $T$ modules.
'Proof':
I will claim that what will be problematic with the proof is the exact module structure on what we're dealing with, in particular $i$ gives a very specific module structure.
Usin theorem $2$, we wish to prove $T \otimes _A (M \otimes _A N) \cong (T \otimes _A N) \otimes _T (T\otimes _A M)$
We take the right side, which is isomorphic as a $T$ module to
$(N \otimes _A T) \otimes _T (T\otimes _A M)$ .
We now use theorem 1 as follows:
$A = A, B = T, M' = N, N' = T, P'= (T \otimes _A M)$, where $P$ has the $A$ module structure of the bimodule $(T \otimes _A M)$.
Thus we have a $T$-module isomorphism to
$N \otimes _A (T \otimes _T (T \otimes _A M))$
Where this thing is a $T$ module by using theorem $i$: using the $T$ module structure of $(T \otimes _T (T \otimes _A M))$, which in turn uses the $T$ module structure of the leftmost $T$ inside of it.
Now of course what we want to do is say
$(T \otimes _T (T \otimes _A M)) \cong (T \otimes _T T) \otimes _A M$, but we cannot use theorem 1, because as we mentioned the structure of this is as a $T$ module isn't what theorem 1 thinks (i.e with the middle $T$ being a $(A,T)$ module and it giving the $T$ module structure).
Now it is possible to get over this by just building the same isomorphism because in our hearts we know it's true of course, but this is annoying work and I keep finding myself getting into these situations. My question is are there more powerful assosicative tensor theorem I can prove once to save me the headache?
Best Answer
Since you are interested in localizations of modules, I am assuming $A$ is commutative. In trying to prove the isomorphism of interest, you are in a somewhat nicer more specialized setting than the one of your Theorem 1 in the sense that your ring $B$ (which is $S^{-1}A$) is an $A$-algebra. This ensures that any $B$-module has a unique compatible structure of $A$-module, which in particular makes $B$ into an $(A,B)$-bimodule and a $(B,A)$-bimodule, but precisely because $B$ is an $A$-algebra, the bimodule stuff is irrelevant (and I think maybe obfuscates things—I at least find keeping track of the various module structures in the general setting to be somewhat bewildering).
I am going to propose what I think is a somewhat simpler path to the result you are interested in, making explicit use of the formalism of extension of scalars from a ring $A$ to an $A$-algebra $B$ (everything I do is used constantly in commutative algebra).
For any $A$-module $M$, the extension of scalars of $M$ from $A$ to $B$ is the $A$-module $M_B:=B\otimes_AM$. It can be shown that $M_B$ carries a unique $B$-module structure satisfying $b^\prime\cdot(b\otimes m)=(bb^\prime)\otimes m$ for all $b,b^\prime\in B$ and $m\in M$ (the defining formula ensures that this $B$-module structure is compatible with the $A$-module structure).
Now, as you likely already know, if $M$ is a $B$-module and $N$ is an $A$-module, then $M\otimes_AN$ has a unique $B$-module structure satisfying $b(m\otimes n)=(bm)\otimes n$ for all $b\in B$, $m\in M$, and $n\in N$ (and, as before, this $B$-module structure is compatible with the $A$-module structure).
These constructions are related by the following tensor isomorphism (I don't know if there is a standard name for it, though I believe I have seen it referred to as "simplification by $A$" or something along those lines):
(i) For any $B$-module $M$ and any $A$-module $N$, there is a unique $B$-module isomorphism $M\otimes_AN\cong M\otimes_B(B\otimes_AN)$ satisfying $m\otimes n\mapsto m\otimes(1\otimes n)$.
Add to this the basic associativity isomorphism:
(ii) For $A$-modules $M$, $N$, and $P$, there is a unique $A$-module isomorphism $(M\otimes_AN)\otimes_AP\cong M\otimes_A(N\otimes_AP)$ satisfying $(m\otimes n)\otimes p\mapsto m(\otimes(n\otimes p)$.
The formulas used to characterize the isomorphisms in (i) and (ii) can be used to show that, for $A$-modules $M$ and $N$, the $A$-module isomorphism $(B\otimes_AM)\otimes_AN\cong B\otimes_A(M\otimes_AN)$ of (ii) is in fact $B$-linear, where the $B$-module structure on the source arises as in the second construction above via the $B$-module structure on $B\otimes_AM$, while the $B$-module structure on the target arises as in the first construction.
Now we can prove the general theorem asserting that extension of scalars is compatible with tensor products.
Theorem: For $A$-modules $M$ and $N$, there is a canonical $B$-module isomorphism
$$B\otimes_A(M\otimes_AN)\cong (B\otimes_AM)\otimes_B(B\otimes_AN).$$
Here the $B$-module structure on the left is the one obtained by the extension of scalars construction applied to $M\otimes_AN$ (or, equivalently, applying the second construction to the tensor product of the $A$-modules $B$ and $M\otimes_AN$), and the $B$-module structure on the right is the usual one on the tensor product of the $B$-modules $B\otimes_AM$ and $B\otimes_AN$ obtained by extension of scalars. Note that, using the notation from earlier for extension of scalars, the isomorphism can also be written $(M\otimes_AN)_B\cong M_B\otimes_BN_B$.
For the proof, we start with the (inverse of the) $A$-linear associativity isomorphism $B\otimes_A(M\otimes_AN) \cong(B\otimes_AM)\otimes_AN$, which, as we already observed, is $B$-linear. We now appy (i) with the $B$-module $M_B=B\otimes_AM$ and the $A$-module $N$ to obtain the $B$-linear isomorphism $(B\otimes_AM)\otimes_AN\cong(B\otimes_AM)\otimes_B(B\otimes_AN)$. Composing the last two isomorphisms gives the desired one (of course one can easily write down explicitly the effect of the isomorphism on a tensor in the source of the form $b\otimes(m\otimes n)$).
Now let $B=S^{-1}A$, so that, by your Theorem 2, we have a canonical $B$-module isomorphism $S^{-1}M\cong B\otimes_AM$ for any $A$-module $M$. (Observe that the content here is that the functor given by extension of scalars along $A\to S^{-1}A$ is naturally isomorphic to the localization functor sending an $A$-module $M$ to $S^{-1}M$). Combining this with the isomorphism of the theorem above gives
$$S^{-1}(M\otimes_AN)\cong B\otimes_A(M\otimes_AN) \cong (B\otimes_AM)\otimes_B(B\otimes_AN)\cong S^{-1}M\otimes_{S^{-1}A} S^{-1}N,$$
where the last isomorphism is the tensor product over $S^{-1}A$ of the $S^{-1}A$-linear isomorphisms $B\otimes_AM\cong S^{-1}M$ and $B\otimes_AN\cong S^{-1}N$.