Lean-Workbook Plus 39832: Trigonometric identity

For every real $x$, $\sin^2x\cos^2x=\sin^2(2x)/4$ and $\sin^2x=(1-\cos(2x))/2$.

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