The Stacks project

Suggested slogan: Henselization is left adjoint to the inclusion of Henselian rings in rings.

In the second proof, which at the end invokes a lemma that has locality hypotheses, you need to first indicate why $A^h$ is local. One way based on general principles beyond the local setting is to recall that for any pair $(B,J)$ the ideal $J^h$ of $B^h$ is contained in the Jacobson radical (by the henselian property for the pair $(B^h, J^h)$) and by construction $J^h = JB^h$ yet always $B^h/JA^h = B/J$ (so when $B$ is local with maximal ideal $J$, the ideal $J^h$ is maximal and so is the unique maximal ideal of $J^h$, moreover with the same residue field as $B$).

Note that in this argument, we are using two facts currently recorded in Lemma 0AGU, which currently appears just after the present Lemma in section 0EM7 (no circularity, since Lemma 0AGU doesn't use the present lemma, so their order should be swapped).

Also, this shows that before swapping the order of the two lemmas, the "first proof" isn't entirely satisfactory since it isn't giving that $\mathfrak{m}^h$ is also the maximal ideal (which would however be "known" if Lemma 0AGU were put before the present lemma, as recommended above).

Thanks and fixed here.