Lean-Workbook Plus 36620: Trigonometric identity

For every real $\theta$, $\sin(2\theta)=2/(\tan\theta+1/\tan\theta)$. Lean’s total tangent and division include the pole and zero cases.

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