feat(algebra/big_operators): add `finset.prod_comm'` (#14257)
* add a "dependent" version of `finset.prod_comm`;
* use it to prove the original lemma;
* slightly generalize `exists_eq_right_right` and `exists_eq_right_right'`;
* add two `simps` attributes.
