$M{\otimes }_{R}R\mathrm{/}I\cong M\mathrm{/}IM$ naturally

The sequence $I\to R\to R\mathrm{/}I\to 0$ is exact. Tensoring on the right by $M$ and applying [L1] gives the exact sequence $I{\otimes }_{R}M\to R{\otimes }_{R}M\to (R\mathrm{/}I){\otimes }_{R}M\to 0$. The symmetry isomorphisms of [L6] carry it termwise to $M{\otimes }_{R}I\to M{\otimes }_{R}R\to M{\otimes }_R(R\mathrm{/}I)\to 0$, and since $\sigma$ commutes with the induced maps on elementary tensors, that sequence is exact too.

Under [L2], the image of $M{\otimes }_{R}I\to M{\otimes }_{R}R\cong M$ consists exactly of finite sums $im$, hence is $IM$ by [L3].

Exactness in step 1.1 identifies $M{\otimes }_R(R\mathrm{/}I)$ with the cokernel of the first map, which by step 2.1 is $M\mathrm{/}IM$; [L5] gives the resulting isomorphism.

Tracing $m\otimes (r+I)$ through the quotient gives $rm+IM$. Multiplication by an element of $I$ acts as zero on both sides, so the map and its inverse are $R\mathrm{/}I$-linear.

If $I=0$, step 4.1 is [L2]. If $I=R$, then [L3] gives $IM=M$ and $R\mathrm{/}I=0$, so both sides are zero.

This proves the natural $R$-linear and $R\mathrm{/}I$-linear isomorphism in every boundary case.