Problem: Let $a_0,a_1,\dots ,a_n$ be numbers from the interval $(0,\pi/2)$
such that $\tan (a_0-\frac{\pi}{4})+ \tan (a_1-\frac{\pi}{4})
 + \dotsb +\tan (a_n-\frac{\pi}{4}) \ge  n-1$.
Prove that
\[ \tan a_0\tan a_1 \dotsm \tan a_n \ge n^{n+1}. \]

Solution: Let $x_i = \tan(a_i - \frac{\pi}{4})$.
Then we have that
\[ \tan a_i = \tan(a_i - 45\dg + 45\dg) = \frac{x_i + 1}{1 - x_i}. \]
If we further substitute $y_i = \frac{1 - x_i}{2} \in (0,1)$,
then we have to prove that the following statement:
\begin{claim*}
  If $\sum_0^n y_i \le 1$ and $y_i \ge 0$, we have
  \[ \prod_{i=1}^n \left( \frac{1}{y_i}-1 \right) \ge n^{n+1}. \]
\end{claim*}
\begin{proof}
  Homogenizing, we have to prove that
  \[ \prod_{i=1}^n \left( \frac{y_0+y_1+y_2+\dots+y_n}{y_i}-1 \right) \ge n^{n+1}. \]
  By AM-GM, we have
  \[ \frac{y_1+y_2+y_3+\dots+y_n}{y_0}
    \ge n \sqrt[n]{\frac{y_1y_2y_3\dots y_n}{y_1}}. \]
    Cyclic product works.
\end{proof}
\begin{remark*}
  Alternatively, the function $x \mapsto \log(1/x-1)$
  is a convex function on $(0,1)$ so Jensen inequality should also work.
\end{remark*}