Lean-Workbook Plus 71970: Trigonometric identity

For real $a,b,u,v$, $a\sin u+b\sin(u+v)=(a+b\cos v)\sin u+(b\sin v)\cos u$.

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