Lean-Workbook Plus 2102: Trigonometric identity

For every real angle $\theta$, the double-angle identity is $\sin(2\theta)=2\tan\theta/(1+\tan^2\theta)$, with the usual total real operations used by Lean.

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