<s>[INST] An identity involving the Bessel function of the first kind $J_0$ Today, computing $\int_{0}^{\pi/2}\sin^2(\sin^2 x)\,dx$, I found an interesting identity:
$$\sum_{k\geq 0}\frac{(-1)^k(4k)!}{(2k)!^3 4^k}=\cos(1)\cdot\sum_{k\geq 0}\frac{(-1)^k}{k!^2 4^k}.$$
How would you prove it?
 [/INST] This answer is due to Giulio Francot, a friend of mine. His solution is extremely close to my original manipulations.

We have:
\begin{eqnarray*}
\int\limits_{0}^{\frac{\pi }{2}}\sin ^{2}(\sin ^{2}(x))dx 
&=&\int\limits_{0}^{\frac{\pi }{2}}\frac{1-\cos (2\sin ^{2}(x))}{2}dx \\
&=&\frac{
\pi }{4}-\frac{1}{2}\int\limits_{0}^{\frac{\pi }{2}}\sum\limits_{k\geq 0}
\frac{(-1)^{k}4^{k}}{(2k)!}\sin ^{4k}(x)dx \\
&=&\frac{\pi }{4}-\frac{1}{2}\sum\limits_{k\geq 0}\frac{(-1)^{k}4^{k}}{(2k)!
}\int\limits_{0}^{\frac{\pi }{2}}\sin ^{4k}(x)dx \\ 
&=&\frac{\pi }{4}-\frac{1}{2}
\sum\limits_{k\geq 0}\frac{(-1)^{k}4^{k}}{(2k)!}\frac{(4k)!}{
(4^{k}(2k)!)^{2}}\frac{\pi }{2} \\
&=&\frac{\pi }{4}-\frac{\pi }{4}\sum\limits_{k\geq 0}\frac{(-1)^{k}}{
((2k)!)^{3}}\frac{(4k)!}{4^{k}}.\tag{1}
\end{eqnarray*}
On the other hand:
\begin{eqnarray*}
\int\limits_{0}^{\frac{\pi }{2}}\sin ^{2}(\sin ^{2}(x))dx
&=&\int\limits_{0}^{\frac{\pi }{2}}\frac{1-\cos (2\sin ^{2}(x))}{2}
dx=\int\limits_{0}^{\frac{\pi }{2}}\frac{1-\cos (1-\cos (2x))}{2}dx \\
&=&\frac{\pi }{4}-\int\limits_{0}^{\frac{\pi }{2}}\frac{\cos (1)\cos (\cos
(2x))}{2}dx-\int\limits_{0}^{\frac{\pi }{2}}\frac{\sin (1)\sin (\cos (2x))}{
2}dx \\
&=&\frac{\pi }{4}-\frac{\cos (1)}{2}\int\limits_{0}^{\frac{\pi }{2}}\cos
(\cos (2x))dx=\frac{\pi }{4}-\frac{\cos (1)}{4}\int\limits_{0}^{\pi }\cos
(\cos (x))dx \\
&=&\frac{\pi }{4}-\frac{\cos (1)\pi }{4}J_{0}(1).\tag{2}
\end{eqnarray*}
</s>