Lean-Workbook Plus 35546: Trigonometric identity

For real $x\ne0,\pi/2$, $(\sin x/\cos x)(\sin x/\sin x)+(\cos x/\sin x)(\cos x/\cos x)=1/(\sin x\cos x)$. The statement uses Lean’s total division, so it also covers other zeros of sine or cosine.

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