Let $\Omega\subset\mathbb{R}^n$ be a bounded domain, $\partial\Omega\in C^\infty$. Let $\Delta$ be the standard Laplacian. Suppose $u\in H^1_0(\Omega)$ is a weak solution to $$\begin{cases}\Delta u=\sin(u)&\text{in }\Omega\\\quad u=0&\text{on }\partial\Omega.\end{cases}$$ Prove that $u\in C^\infty(\overline{\Omega})$.
I wanted to use the standard elliptic regularity theory. Since $\sin(u)\in L^\infty$, we see immediately that $u\in H^2(\Omega)$. Similarly, since $D(\sin(u))=\cos(u)Du$, we have $u\in H^3(\Omega)$. But then comes the trouble. $$D^2(\sin(u))=-\sin(u)|Du|^2+\cos(u)D^2u.$$ If $u\in H^3(\Omega)$ (which is all we have at present), then the best we can say is that $Du\in H^2(\Omega)$, so by Sobolev embedding $Du\in L^{\frac{2n}{n-4}}(\Omega)$ (supposing $n\geq5$, say). However, this does not imply $|Du|^2\in L^2(\Omega)$ if $\frac{n}{n-4}\leq2$, or $n\geq8$. Thus if $n$ is large we cannot proceed.
So how should we prove this?
By the way, do not use any potential theory for the Laplacian. The original problem was about a general uniformly elliptic operator with $C^\infty(\overline{\Omega})$-coefficients, and here I use $\Delta$ for simplicity.