Is one sheafification enough for the module inverse image? Let $\newcommand{\G}{\mathcal{G}}\newcommand{\O}{\mathcal{O}} f: (X, \O_X) \to (Y, \O_Y)$ be a morphism of locally ringed spaces and $\G$ a sheaf of $\O_Y$ modules. The module inverse image of $\G$ is defined as
$$
f^* \G = f^{-1} \G \otimes_{f^{-1} \O_Y} \O_X
$$
There are three sheafifications involved here: one for the tensor product one for $f^{-1} \G$ and finally one for $f^{-1} O_Y$, since the inverse image $f^{-1} \G$ is defined as the sheafification of $f^+ \G$, where 
$$
f^+ \G (U) = \varinjlim_{V \supset f(U)} \G(V)
$$
My question is whether $f^* \G$ is equal to the sheafification of the presheaf $f^+ \G \,\hat\otimes_{f^+ \O_Y} \O_X$ (where $\hat\otimes$ denotes a tensor product without sheafification.
In particular I would be interested in some "high-level" argument which maybe applies to more general situations.
 A: The "high-level" argument would be related to such topics as the Yoneda lemma, the Yoneda embedding, representable functors, etc. in category theory.
At this level, the argument would go roughly along the lines of:
\begin{align*}
\operatorname{Hom}_{\mathcal{O}_X}(f^* \mathcal{G}, \mathcal{F}) & \simeq
\operatorname{Hom}_{\mathcal{O}_Y}(\mathcal{G}, f_* \mathcal{F}) \\
& \simeq \operatorname{Hom}_{\mathcal{O}_Y, psh}(\mathcal{G}, f_* \mathcal{F}) \\
& \simeq \operatorname{Hom}_{f^+ \mathcal{O}_Y, psh}(f^+ \mathcal{G}, \mathcal{F}) \\
& \simeq \operatorname{Hom}_{\mathcal{O}_X, psh}(f^+ \mathcal{G} \hat\otimes_{f^+ \mathcal{O}_Y} \mathcal{O}_X, \mathcal{F}) \\
& \simeq \operatorname{Hom}_{\mathcal{O}_x}([f^+ \mathcal{G} \hat\otimes_{f^+ \mathcal{O}_Y} \mathcal{O}_X]^+, \mathcal{F}).
\end{align*}
(Here for example, $\operatorname{Hom}_{\mathcal{O}_Y, psh}(-, -)$ represents the presheaf homomorphisms which are $\mathcal{O}_Y$-linear; and for a presheaf of $\mathcal{O}_X$-modules $\mathcal{F}$ then $\mathcal{F}^+$ is the sheafification as a sheaf of $\mathcal{O}_X$-modules.)
In this sequence, once you have established each isomorphism, and you have also verified that each is functorial in $\mathcal{F}$, then by Yoneda's lemma, it follows that the composite isomorphism of functors $\mathcal{O}_X{-}\mathrm{Mod} \to \mathrm{Set}$ is induced by a unique isomorphism of $\mathcal{O}_X$-modules $f^* \mathcal{G} \simeq [f^+ \mathcal{G} \hat\otimes_{f^+ \mathcal{O}_Y} \mathcal{O}_X]^+$.
(Another possible approach, which essentially boils down to the same thing in the end, is to show that both sides are left adjoints to the same functor, just expressed as different compositions on the "right adjoint side".)
