A puzzler

Thanks to Bjorn Poonen
https://stacks.math.columbia.edu/tag/07NC#comment-5389

algebra.tex

@@ -30239,18 +30239,35 @@ \section{Applications of Zariski's Main Theorem}
 $$
 R_\mathfrak p^\wedge \otimes_R S' = (S'_{\mathfrak q'})^\wedge \times B'
 $$
-by Lemma \ref{lemma-completion-finite-extension}.
-Note that we have a commutative diagram
-$$
-\xymatrix{
-R_\mathfrak p^\wedge \otimes_R S \ar[r] & S_\mathfrak q^\wedge \\
-R_\mathfrak p^\wedge \otimes_R S' \ar[r] \ar[u] &
-(S'_{\mathfrak q'})^\wedge \ar[u]
-}
-$$
-where the right vertical is an isomorphism and the lower horizontal
-arrow is the projection map of the product decomposition above.
-The lemma follows.
+by Lemma \ref{lemma-completion-finite-extension}. Observe that under this
+product decomposition $g$ maps to a pair $(u, b')$ with
+$u \in (S'_{\mathfrak q'})^\wedge$ a unit because $g \not \in \mathfrak q'$.
+The product decomposition for $R_\mathfrak p^\wedge \otimes_R S'$
+induces a product decomposition
+$$
+R_\mathfrak p^\wedge \otimes_R S = A \times B
+$$
+Since $S'_g = S_g$ we also have
+$(R_\mathfrak p^\wedge \otimes_R S')_g = (R_\mathfrak p^\wedge \otimes_R S)_g$
+and since $g \mapsto (u, b')$ where $u$ is a unit we see that
+$(S'_{\mathfrak q'})^\wedge = A$. Since the isomorphism
+$S'_{\mathfrak q'} = S_\mathfrak q$ determines an isomorphism on
+completions this also tells us that $A = S_\mathfrak q^\wedge$.
+This finishes the proof, except that we should perform the sanity check
+that the induced map
+$\phi : R_\mathfrak p^\wedge \otimes_R S \to A = S_\mathfrak q^\wedge$
+is the natural one. For elements of the form $x \otimes 1$
+with $x \in R_\mathfrak p^\wedge$ this is clear as the natural
+map $R_\mathfrak p^\wedge \to S_\mathfrak q^\wedge$ factors through
+$(S'_{\mathfrak q'})^\wedge$. For elements of the form $1 \otimes y$
+with $y \in S$ we can argue that for some $n \geq 1$ the element
+$g^ny$ is the image of some $y' \in S'$. Thus $\phi(1 \otimes g^ny)$
+is the image of $y'$ by the composition
+$S' \to (S'_{\mathfrak q'})^\wedge \to S_\mathfrak q^\wedge$ which is
+equal to the image of $g^ny$ by the map $S \to S_\mathfrak q^\wedge$.
+Since $g$ maps to a unit this also
+implies that $\phi(1 \otimes y)$ has the correct value, i.e., the
+image of $y$ by $S \to S_\mathfrak q^\wedge$.
 \end{proof}