Lean-Workbook Plus 21372: Trigonometric identity

Prove the identity: $\cos{x}+\cos{y}=2\cos{\frac{x+y}{2}}\cos{\frac{x-y}{2}}$.

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