[proofplan] We construct explicit $S$-module homomorphisms $\varphi: M \otimes_R N \to M \otimes_S (S \otimes_R N)$ and $\psi: M \otimes_S (S \otimes_R N) \to M \otimes_R N$, each arising from the universal property of the appropriate tensor product. We then verify that $\psi \circ \varphi$ and $\varphi \circ \psi$ are both the identity by checking on pure tensors, which span the respective modules. [/proofplan]

[step:Construct $\varphi: M \otimes_R N \to M \otimes_S (S \otimes_R N)$ via $R$-bilinearity] Define the map $\Phi: M \times N \to M \otimes_S (S \otimes_R N)$ by $\Phi(m, n) = m \otimes (1_S \otimes n)$. We verify that $\Phi$ is $R$-bilinear. For $m, m' \in M$, $n, n' \in N$, and $r \in R$: **Additivity in the first variable:** \begin{align*} \Phi(m + m', n) = (m + m') \otimes (1_S \otimes n) = m \otimes (1_S \otimes n) + m' \otimes (1_S \otimes n) = \Phi(m, n) + \Phi(m', n). \end{align*} **Additivity in the second variable:** \begin{align*} \Phi(m, n + n') = m \otimes (1_S \otimes (n + n')) = m \otimes (1_S \otimes n + 1_S \otimes n') = m \otimes (1_S \otimes n) + m \otimes (1_S \otimes n') = \Phi(m, n) + \Phi(m, n'). \end{align*} **$R$-balance:** For $r \in R$, we must show $\Phi(mr, n) = \Phi(m, rn)$, where $mr$ denotes the action of $r$ on $M$ via the structure map $f: R \to S$ (i.e., $mr = f(r) \cdot m$). We have: \begin{align*} \Phi(f(r) \cdot m, n) &= (f(r) \cdot m) \otimes (1_S \otimes n) = m \otimes (f(r) \cdot (1_S \otimes n)) = m \otimes (f(r) \otimes n), \end{align*} where the second equality uses the $S$-balance property of $\otimes_S$ (pulling the scalar $f(r) \in S$ from the left factor to the right factor), and \begin{align*} \Phi(m, rn) = m \otimes (1_S \otimes rn) = m \otimes (f(r) \otimes n), \end{align*} where the last equality uses $R$-balance in $S \otimes_R N$: $1_S \otimes rn = f(r) \cdot 1_S \otimes n = f(r) \otimes n$. Therefore $\Phi(f(r) \cdot m, n) = \Phi(m, rn)$. By the universal property of $M \otimes_R N$, there is a unique $R$-module homomorphism \begin{align*} \varphi: M \otimes_R N \to M \otimes_S (S \otimes_R N), \quad m \otimes n \mapsto m \otimes (1_S \otimes n). \end{align*} We verify $\varphi$ is $S$-linear. For $s \in S$ and a pure tensor $m \otimes n \in M \otimes_R N$: \begin{align*} \varphi(s \cdot (m \otimes n)) = \varphi((sm) \otimes n) = (sm) \otimes (1_S \otimes n) = s \cdot (m \otimes (1_S \otimes n)) = s \cdot \varphi(m \otimes n), \end{align*} where $s \cdot (m \otimes n) = (sm) \otimes n$ because $M$ is an $S$-module and the $S$-action on $M \otimes_R N$ is through the first factor. Since pure tensors span $M \otimes_R N$, $\varphi$ is $S$-linear. [/step]

[step:Construct $\psi: M \otimes_S (S \otimes_R N) \to M \otimes_R N$ in two stages]We build $\psi$ in two stages using the universal property of the tensor product. **Stage 1: For each fixed $m \in M$, construct $H_m: S \otimes_R N \to M \otimes_R N$.** Define $\Theta_m: S \times N \to M \otimes_R N$ by $\Theta_m(s, n) = (sm) \otimes n$. This is $R$-bilinear: for $r \in R$, \begin{align*} \Theta_m(s + s', n) &= (s + s')m \otimes n = (sm) \otimes n + (s'm) \otimes n = \Theta_m(s, n) + \Theta_m(s', n), \\ \Theta_m(s, n + n') &= (sm) \otimes (n + n') = (sm) \otimes n + (sm) \otimes n' = \Theta_m(s, n) + \Theta_m(s, n'), \\ \Theta_m(f(r) \cdot s, n) &= (f(r) s \cdot m) \otimes n = (s \cdot m) \otimes rn = \Theta_m(s, rn), \end{align*} where the last line uses $f(r)s \cdot m = s \cdot f(r) m = s \cdot (f(r)m)$ (commutativity of $S$) and then the $R$-balance relation in $M \otimes_R N$: $(sf(r)m) \otimes n = (sm) \otimes rn$, since $f(r)m = m \cdot f(r)$ gives $(sf(r)m) \otimes n = (sm) \otimes rn$ by the relation $f(r) \cdot (sm) \otimes n = (sm) \otimes f(r) \cdot n$ after noting $f(r) \cdot m = m$ with $r$ acting on $N$. More precisely: $(f(r)s)m \otimes n = s(f(r)m) \otimes n$ and $sm \otimes rn = s m \otimes rn$, and the $R$-balance condition in $M \otimes_R N$ gives $f(r) \cdot (sm) \otimes n = (sm) \otimes rn$ since $r$ acts on $M$ via $f(r)$ and $r$ acts on $N$ directly. By the universal property of $S \otimes_R N$, there exists a unique $R$-module homomorphism \begin{align*} H_m: S \otimes_R N \to M \otimes_R N, \quad s \otimes n \mapsto (sm) \otimes n. \end{align*} **Stage 2: Construct $\psi$ from the family $(H_m)_{m \in M}$.** Define $\Psi: M \times (S \otimes_R N) \to M \otimes_R N$ by $\Psi(m, x) = H_m(x)$. We verify $\Psi$ is $S$-bilinear: *Additivity in the first variable:* $\Psi(m + m', s \otimes n) = H_{m+m'}(s \otimes n) = (s(m + m')) \otimes n = (sm) \otimes n + (sm') \otimes n = H_m(s \otimes n) + H_{m'}(s \otimes n)$. Since $S \otimes_R N$ is spanned by pure tensors and each $H_m$ is additive, $\Psi(m + m', x) = \Psi(m, x) + \Psi(m', x)$ for all $x$. *Additivity in the second variable:* $\Psi(m, x + y) = H_m(x + y) = H_m(x) + H_m(y) = \Psi(m, x) + \Psi(m, y)$. *$S$-balance:* For $s' \in S$: $\Psi(s'm, s \otimes n) = H_{s'm}(s \otimes n) = (s \cdot s'm) \otimes n = (ss'm) \otimes n$ and $\Psi(m, s' \cdot (s \otimes n)) = \Psi(m, s's \otimes n) = H_m(s's \otimes n) = (s's \cdot m) \otimes n = (ss'm) \otimes n$, using commutativity of $S$. By the universal property of $M \otimes_S (S \otimes_R N)$, there is a unique $S$-module homomorphism \begin{align*} \psi: M \otimes_S (S \otimes_R N) \to M \otimes_R N, \quad m \otimes (s \otimes n) \mapsto (sm) \otimes n. \end{align*}[/step]

[guided]The construction of $\psi$ is more involved than that of $\varphi$ because the tensor product $M \otimes_S (S \otimes_R N)$ has two layers: first the $R$-tensor $S \otimes_R N$, and then the $S$-tensor with $M$. We cannot simply write down a bilinear map from $M \times S \times N$ because the middle term $S \otimes_R N$ is itself a tensor product, not a bare module. The two-stage approach resolves this. In Stage 1, we fix $m$ and use the universal property of $S \otimes_R N$ to define $H_m$ as a map out of the inner tensor product. In Stage 2, we use the universal property of $M \otimes_S (-)$ to assemble the family $(H_m)$ into a single map $\psi$ out of the outer tensor product. Each stage consumes exactly one universal property, so there is no ambiguity. On a pure tensor $m \otimes (s \otimes n)$, the composite formula is: \begin{align*} \psi(m \otimes (s \otimes n)) = H_m(s \otimes n) = (sm) \otimes n. \end{align*} This is the "obvious" inverse: it moves the scalar $s$ from $S \otimes_R N$ into the $S$-action on $M$.[/guided]

[step:Verify $\psi \circ \varphi = \operatorname{id}_{M \otimes_R N}$] On a pure tensor $m \otimes n \in M \otimes_R N$: \begin{align*} (\psi \circ \varphi)(m \otimes n) = \psi(m \otimes (1_S \otimes n)) = (1_S \cdot m) \otimes n = m \otimes n. \end{align*} Since pure tensors span $M \otimes_R N$ as an $R$-module and $\psi \circ \varphi$ is $R$-linear, we conclude $\psi \circ \varphi = \operatorname{id}_{M \otimes_R N}$. [/step]

[step:Verify $\varphi \circ \psi = \operatorname{id}_{M \otimes_S (S \otimes_R N)}$] The module $M \otimes_S (S \otimes_R N)$ is spanned as an $S$-module by elements of the form $m \otimes (s \otimes n)$. On such an element: \begin{align*} (\varphi \circ \psi)(m \otimes (s \otimes n)) &= \varphi((sm) \otimes n) = (sm) \otimes (1_S \otimes n). \end{align*} We must show this equals $m \otimes (s \otimes n)$ in $M \otimes_S (S \otimes_R N)$. Using the $S$-balance property of $\otimes_S$: \begin{align*} (sm) \otimes (1_S \otimes n) = m \otimes (s \cdot (1_S \otimes n)) = m \otimes (s \otimes n), \end{align*} where $s \cdot (1_S \otimes n) = s \otimes n$ because $S$ acts on $S \otimes_R N$ by multiplication on the first factor. Therefore $(\varphi \circ \psi)(m \otimes (s \otimes n)) = m \otimes (s \otimes n)$. Since elements of the form $m \otimes (s \otimes n)$ span $M \otimes_S (S \otimes_R N)$ and $\varphi \circ \psi$ is $S$-linear, we conclude $\varphi \circ \psi = \operatorname{id}_{M \otimes_S (S \otimes_R N)}$. [/step]

[step:Conclude that $\varphi$ is an $S$-module isomorphism] Since $\varphi$ is an $S$-module homomorphism with $S$-linear two-sided inverse $\psi$ (i.e., $\psi \circ \varphi = \operatorname{id}$ and $\varphi \circ \psi = \operatorname{id}$), $\varphi$ is an $S$-module isomorphism $M \otimes_R N \xrightarrow{\sim} M \otimes_S (S \otimes_R N)$ sending $m \otimes n \mapsto m \otimes (1_S \otimes n)$. [/step]