Lean-Workbook Plus 12099: Trigonometric identity

The complementary-angle identity gives $\sin 50^\circ=\cos 40^\circ$. The Lean statement writes these angles in radians as $50\pi/180$ and $40\pi/180$.

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