<s>[INST] Where does the sum of $\sin(n)$ formula come from? I have seen Lagrange's formula for the sum of $\sin(n)$ from $1$ to $n$ during one of my classes last week, but I never saw how it came to be. I tried googling it to find a proof but couldn't seem to find any as it kept bringing up his other work instead and just statements of the formula rather than derivations/proofs.
I'm really interested to see where it comes from so if anyone has any nice proofs that would be appreciated.
Thank you!   
 [/INST] A comment on a follow-up question suggests using the following identity:
$$
 2 \sin \left(\tfrac12\right) \sin (k)
 = \cos\left(k - \tfrac12\right) - \cos\left(k + \tfrac12\right).
$$
Then
\begin{align}
2 \sin \left(\tfrac12\right)&\left(\sin(1) + \sin(2) + \sin(3) + \cdots + \sin(n-1) + \sin(n)\right) \\
&= \left(\cos\left(\tfrac12\right) - \cos\left(\tfrac32\right)\right)
+\left(\cos\left(\tfrac32\right) - \cos\left(\tfrac52\right)\right)
+\left(\cos\left(\tfrac52\right) - \cos\left(\tfrac72\right)\right)\\
& \qquad + \cdots
 +\left(\cos\left(n - \tfrac32\right) - \cos\left(n - \tfrac12\right)\right)
+\left(\cos\left(n - \tfrac12\right) - \cos\left(n + \tfrac12\right)\right) \\
&= \cos\left(\tfrac12\right) - \cos\left(n + \tfrac12\right) \\
&= \sin\left(\tfrac{n+1}2\right) \sin\left(\tfrac n2\right).
\end{align}
Therefore
$$
\sin(1) + \sin(2) + \cdots + \sin(n)
 = \frac{\sin\left(\frac{n+1}2\right) \sin\left(\frac n2\right)}
        {\sin\left(\frac12\right)}.
$$
There is another derivation of this formula
(using $2 \sin(1) \sin(k) = \cos(k-1) -\cos(k + 1)$)
in another answer.
</s>