Lean-Workbook Plus 55626: Trigonometric identity

For every real $x$, $\frac{(\sin^2x+\cos^2x)^2-2\sin^2x\cos^2x}{\sin x\cos x}=\frac{2-\sin^2(2x)}{\sin(2x)}$. Lean’s total division includes zero denominators.

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