Lean-Workbook Plus 5165: Trigonometric identity

For every real angle $\theta$, $\tan^2(\theta/2)=(1-\cos\theta)/(1+\cos\theta)$. This uses Lean’s totalized tangent and division: at a pole, division by zero is defined as zero, so the displayed equality also includes those cases.

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