split(data/finset/prod): split off `data.finset.basic` (#10142)
Killing the giants. This moves `finset.product`, `finset.diag`, `finset.off_diag` to their own file, the theme being "finsets on `α × β`".
The copyright header now credits:
* Johannes Hölzl for ba95269a65a77c8ab5eae075f842fdad0c0a7aaf
* Mario Carneiro
* Oliver Nash for #4502
