Lean-Workbook Plus 16072: Trigonometric identity

Prove the identity $\cos 2kx \cdot \cos x = \frac {1}{2}\left[\cos \left(2k - 1\right)x + \cos \left(2k + 1\right)x\right]$.

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