Lean-Workbook Plus 52387: Trigonometric identity

For real $\theta$ with $\cos\theta\ne0$, $\sqrt{\frac{1+1/\cos\theta}{1/\cos\theta-1}}=\sqrt{\frac{\cos\theta+1}{1-\cos\theta}}$. The formal equality uses Lean’s total square root and division at exceptional values.

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