Lean-Workbook Plus 80657: Trigonometric identity

For real $\alpha,\theta$ with $\cos(2\alpha)=7/25$ and $\sin(2\alpha)=24/25$, $\cos(2\alpha+2\theta)=(7\cos(2\theta)-24\sin(2\theta))/25$.

Source: Lean-Workbook row lean_workbook_plus_80657 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.