Lean-Workbook Plus 4590: Trigonometric identity

Express $\sqrt{2}$ in terms of cosine: $\sqrt{2} = 2\cos\left(\frac{\pi}{4}\right)$.

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