feat(data/finite/basic): add missing instances (#14913)
* Add `finite` instances for `prod`, `pprod`, `sigma`, and `psigma`.
* Don't depend on `classical.choice` in `finite_iff_nonempty_fintype`.
* Move `not_finite_iff_infinite` up, use it to golf some proofs.
