Solution (source code)

= Solution

On a relatively compact ball, mollification commutes with the <Laplacian>, so $u_\varepsilon=u*\eta_\varepsilon$ is a smooth harmonic function. Repeated <interior derivative estimate for a harmonic function>[interior derivative estimates], together with the <Caccioppoli inequality>, bound every derivative of $u_\varepsilon$ on a smaller ball by the local $L^2$ norm of $u$, uniformly as $\varepsilon\downarrow0$. The <Arzela-Ascoli theorem> and a diagonal argument give a smooth local limit, while mollification gives $u_\varepsilon\to u$ in $L^2_{\rm loc}$. Thus the limit equals $u$ almost everywhere. After choosing this smooth representative, $u$ is harmonic pointwise. This is the <Weyl lemma> for an $H^1$ weak solution.