<s>[INST] How would one discover this finite product identity? I recently found the following finite product identity in a table of products:
\begin{align}
  \prod_{k=0}^{n-1}\left[\sinh^2y+\sin^2\left(x+\frac{k\pi}{n}\right)\right]=2^{1-2n}(\cosh(2ny) -\cos(2nx))
\end{align}
I'd like to know how one would have gone about discovering this product identity (not just proving the identity) if one were handed the product.
This question is related to my other question Limit of a sequence of determinants. and would effectively answer that question as well.
 [/INST] Discovering such identities often is just recognising things one has already seen elsewhere.
The factors of the product are easily recognised as
$$\left\lvert\sin \left(x+\frac{k\pi}{n} +iy\right) \right\rvert^2$$
when one has some experience with complex analysis. Euler's formulae make the connection between the trigonometric and hyperbolic functions obvious,
$$\begin{align}
\sin z = \frac{e^{iz} - e^{-iz}}{2i};\; \sinh z = \frac{e^z - e^{-z}}{2}&\Rightarrow \sinh (iz) = i\sin z;\, \sin (iz) = i\sinh z,\\
\cos z = \frac{e^{iz}+e^{-iz}}{2};\; \cosh z = \frac{e^z + e^{-z}}{2} &\Rightarrow \cosh (iz) = \cos z;\; \cos (iz) = \cosh z.
\end{align}$$
Thus by the addition formula
$$\sin (x+iy) = \sin x \cos (iy) + \cos x\sin (iy) = \sin x \cosh y + \cos x \sinh y$$
and
$$\lvert\sin (x+iy)\rvert^2 = \sin^2 x \cosh^2 y + \cos^2 x \sinh^2 y,$$
which can be simplified to either $\sin^2 x + \sinh^2 y$ or $\cosh^2 y - \cos^2 x$ using the identities $\sin^2 x + \cos^2 x \equiv 1$ and $\cosh^2 y - \sinh^2 y \equiv 1$.
We can also write the right hand side in similar form, we have by the addition formulae $\cos (2\xi) = \cos^2\xi - \sin^2 \xi = 2\cos^2\xi - 1$ and $\cosh (2\eta) = \cosh^2 \eta + \sinh^2 \eta = 2\cosh^2\eta - 1$, whence
$$\cosh (2\eta) - \cos (2\xi) = 2(\cosh^2 \eta - \cos^2\xi) = 2\lvert \sin (\xi + i\eta)\rvert^2.$$
So if one knows the formula linked by Hans Lundmark,
$$\prod_{k=0}^{n-1} \sin \left(x + \frac{k\pi}{n}\right) = \frac{\sin (nx)}{2^{n-1}},\tag{1}$$
it directly follows from that (note that by the identity theorem, it holds for all $x \in\mathbb{C}$, not only for real $x$),
$$\prod_{k=0}^{n-1} \left\lvert \sin\left( z + \frac{k\pi}{n}\right)\right\rvert^2 = \left\lvert \frac{\sin (nz)}{2^{n-1}}\right\rvert^2 = \frac{\lvert \sin (nz)\rvert^2}{2^{2n-2}}.$$
If one doesn't know formula $(1)$ (and it's not one that is very well-known), one can work it out from the product without too much pain (knowing what should come out definitely helps, but even without that, one can find the right hand side from the product).
It is not a far-fetched idea to start with Euler's formula for the sine, and then to separate the $e^{ix}$ from the $e^{ik\pi/n}$ to arrive at
$$\begin{align}
\prod_{k=0}^{n-1} \sin \left(x + \frac{k\pi}{n}\right)
&= \prod_{k=0}^{n-1} \frac{e^{ix}e^{ik\pi/n} - e^{-ix}e^{-ik\pi/n}}{2i}\\
&= \frac{e^{-inx}e^{i\pi(n-1)/2}}{(2i)^n}\prod_{k=0}^{n-1}\left(e^{2ix} - e^{-2\pi ik/n}\right).\tag{2}
\end{align}$$
Writing $X = e^{2ix}$ and $\zeta_n = e^{2\pi i/n}$ for the primitive $n$-th root of unity, the last product reads
$$\prod_{k=0}^{n-1}\left(X - \zeta_n^k\right),$$
and that is well-known to be the factorisation of $X^n - 1$. Plugging that into $(2)$ and noting that $e^{i\pi(n-1)/2} = i^{n-1}$, we obtain
$$\prod_{k=0}^{n-1} \sin \left( x + \frac{k\pi}{n}\right) = \frac{e^{-inx}\left(e^{2inx}-1\right)}{2^ni} = \frac{e^{inx} - e^{-inx}}{2^ni} = \frac{\sin (nx)}{2^{n-1}}.$$
</s>