Lean-Workbook Plus 7551: Trigonometric identity

Derive the identity $\sin(x)^4+\cos(x)^4=2\, \left( \cos \left( x \right) \right) ^{4}+1-2\, \left( \cos \left( x \right) \right) ^{2}$.

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