<s>[INST] Simplifying $\frac{1-4\cos80^\circ}{\tan20^\circ}$ I am working on simplifying the value
$$\frac{1-4\cos80^\circ}{\tan20^\circ}$$
I am looking for it to be expressed in terms of tangent, because the value seems to be $\tan40^\circ$. However, I can't find any obvious way to do so. How would  simplify it to express like such?
 [/INST] Let's call $t=\tan(x)$ with $x=20°=\frac{\pi}9$
From tan(3x) formula we get $\ \tan(3x)=\sqrt{3}=\dfrac{3t-t^3}{1-3t^2}$
Squaring this to get rid of the root, we get that $t$ is solution of the integer polynomial
$3(1-3t^2)^2=(3t-t^3)^2\iff$
$$t^6-33t^4+27t^2-3=0$$
Now we can use the $\tan(\theta/2)$ conversions from the initial equation

*

*$1-4\cos(4x)=5-8\cos(2x)^2=5-8\left(\frac{1-t^2}{1+t^2}\right)^2$

*$\tan(40°)=\tan(2x)=\frac{2t}{1-t^2}$
And we get
$\begin{align}(1-4\cos(4x))-\tan(x)\tan(2x)&=5-8\left(\frac{1-t^2}{1+t^2}\right)^2-\frac{2t^2}{1-t^2}\\\\
&=\frac{t^6-33t^4+27t^2-3}{(1-t^2)(1+t^2)^2}\end{align}$
Which is precisely $0$ according to the work above.
</s>