Reorder order lemmas in modules

Thanks to Yuto Masamura
https://stacks.math.columbia.edu/tag/01CA#comment-6217

modules.tex

@@ -2488,6 +2488,39 @@ \section{Tensor product}
 Omitted.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-tensor-commute-colimits}
+Let $(X, \mathcal{O}_X)$ be a ringed space.
+For any $\mathcal{O}_X$-module $\mathcal{F}$ the functor
+$$
+\textit{Mod}(\mathcal{O}_X) \longrightarrow \textit{Mod}(\mathcal{O}_X)
+, \quad
+\mathcal{G} \longmapsto \mathcal{F} \otimes_{\mathcal{O}_X} \mathcal{G}
+$$
+commutes with arbitrary colimits.
+\end{lemma}
+
+\begin{proof}
+Let $I$ be a preordered set and let $\{\mathcal{G}_i\}$ be
+a system over $I$. Set $\mathcal{G} = \colim_i \mathcal{G}_i$.
+Recall that $\mathcal{G}$ is the sheaf associated to the presheaf
+$\mathcal{G}' : U \mapsto \colim_i \mathcal{G}_i(U)$, see
+Sheaves, Section \ref{sheaves-section-limits-sheaves}.
+By
+Lemma \ref{lemma-tensor-product-sheafification}
+the tensor product $\mathcal{F} \otimes_{\mathcal{O}_X} \mathcal{G}$
+is the sheafification of the presheaf
+$$
+U \longmapsto
+\mathcal{F}(U) \otimes_{\mathcal{O}_X(U)} \colim_i \mathcal{G}_i(U) =
+\colim_i \mathcal{F}(U) \otimes_{\mathcal{O}_X(U)} \mathcal{G}_i(U)
+$$
+where the equality sign is
+Algebra, Lemma \ref{algebra-lemma-tensor-products-commute-with-limits}.
+Hence the lemma follows from the description of colimits in
+$\textit{Mod}(\mathcal{O}_X)$, see Lemma \ref{lemma-limits-colimits}.
+\end{proof}
+
 \begin{lemma}
 \label{lemma-tensor-product-permanence}
 Let $(X, \mathcal{O}_X)$ be a ringed space.
@@ -2541,8 +2574,10 @@ \section{Tensor product}
 is exact. Using this we can prove (5). Namely, in this case there
 exists locally such an exact sequence with $\mathcal{F}_i$, $i = 1, 2$
 finite free. Hence the two terms
-$\mathcal{F}_2 \otimes_{\mathcal{O}_X} \mathcal{G}$
-are isomorphic to finite direct sums of $\mathcal{G}$.
+$\mathcal{F}_2 \otimes_{\mathcal{O}_X} \mathcal{G}$ and
+$\mathcal{F}_1 \otimes_{\mathcal{O}_X} \mathcal{G}$
+are isomorphic to finite direct sums of $\mathcal{G}$ (for example
+by Lemma \ref{lemma-tensor-commute-colimits}).
 Since finite direct sums are coherent sheaves, these are coherent
 and so is the cokernel of the map, see Lemma \ref{lemma-coherent-abelian}.
 
@@ -2570,39 +2605,6 @@ \section{Tensor product}
 The proof of the other statements is omitted.
 \end{proof}
 
-\begin{lemma}
-\label{lemma-tensor-commute-colimits}
-Let $(X, \mathcal{O}_X)$ be a ringed space.
-For any $\mathcal{O}_X$-module $\mathcal{F}$ the functor
-$$
-\textit{Mod}(\mathcal{O}_X) \longrightarrow \textit{Mod}(\mathcal{O}_X)
-, \quad
-\mathcal{G} \longmapsto \mathcal{F} \otimes_{\mathcal{O}_X} \mathcal{G}
-$$
-commutes with arbitrary colimits.
-\end{lemma}
-
-\begin{proof}
-Let $I$ be a preordered set and let $\{\mathcal{G}_i\}$ be
-a system over $I$. Set $\mathcal{G} = \colim_i \mathcal{G}_i$.
-Recall that $\mathcal{G}$ is the sheaf associated to the presheaf
-$\mathcal{G}' : U \mapsto \colim_i \mathcal{G}_i(U)$, see
-Sheaves, Section \ref{sheaves-section-limits-sheaves}.
-By
-Lemma \ref{lemma-tensor-product-sheafification}
-the tensor product $\mathcal{F} \otimes_{\mathcal{O}_X} \mathcal{G}$
-is the sheafification of the presheaf
-$$
-U \longmapsto
-\mathcal{F}(U) \otimes_{\mathcal{O}_X(U)} \colim_i \mathcal{G}_i(U) =
-\colim_i \mathcal{F}(U) \otimes_{\mathcal{O}_X(U)} \mathcal{G}_i(U)
-$$
-where the equality sign is
-Algebra, Lemma \ref{algebra-lemma-tensor-products-commute-with-limits}.
-Hence the lemma follows from the description of colimits in
-$\textit{Mod}(\mathcal{O}_X)$.
-\end{proof}
-