<s>[INST] How do I prove $\tan1 < \frac{\pi}{2}$? Prove that the equation
$$\sin x \sin({\sin x}) = \frac{\pi}{2} \cos({\sin x})$$
has no real solutions.
Let $t=\sin x$, $-1\leq t\leq 1$. Then the expression above is equvalent to $t\sin t = \frac{\pi}{2} \cos t$. As the function $f(t)=t\sin t - \frac{\pi}{2} \cos t$ is even, and $t=0$ is not a solution, I have to prove that $f(t)$ has no positive roots ($t>0$).  So, for the left side $0<t\leq 1$ and $0<\sin t\leq \sin1$, then $t\sin t\leq \sin1$. For the right side $\cos t\geq \cos1$, so $\frac{\pi}{2} \cos t\geq \frac{\pi}{2} \cos1$. The objective is to prove that $\sin1<\frac{\pi}{2} \cos1$, or, equivalently, $\tan1 < \frac{\pi}{2}$.
I don't know how to approach this inequality. The arguments and the values are mixed up.
 [/INST] This is a Community Wiki repost of one of several deleted answers to a deleted question from last year: Compare $\arcsin (1)$ and $\tan (1)$.
[I have taken this opportunity to incorporate a simplification - but only a slight one - I made later in a comment.]
I would be pleased if we were allowed to revisit the other deleted answers, too.

One can write:
$$
\frac{1}{\sqrt{1 + \tan^21}} = \cos1 = 1 - 2\sin^2\frac{1}{2} >
\frac{17639}{32768} > \frac{17632}{32768} =
\frac{551}{1024},
$$
because
$$
\sin\frac{1}{2} <
\frac{1}{2} - \frac{1}{2^3\cdot3!} + \frac{1}{2^5\cdot5!} =
\frac{1920 - 80 + 1}{3840} < \frac{1845}{3840} = \frac{123}{256}.
$$
On the other hand, using Archimedes's lower bound,
$\pi > 3\tfrac{10}{71}$:
$$
\frac{1}{\sqrt{1 + \left(\sin^{-1}1\right)^2}} =
\frac{1}{\sqrt{1 + \left(\frac{\pi}{2}\right)^2}} <
\frac{1}{\sqrt{1 + \left(\frac{223}{142}\right)^2}} =
\frac{142}{\sqrt{69893}} <
\frac{142}{\sqrt{69696}} =
\frac{142}{264} = \frac{71}{132}.
$$
So, one can prove that $\tan1 < \sin^{-1}1$ by proving that:
$$
\frac{551}{1024} > \frac{71}{132},
$$
which simplifies to $33 \times 551 > 71 \times 256$, that is,
$18183 > 18176$ - which is true.
</s>