chore(*): Rename `prod_dvd_prod` (#11734)
In #11693 I introduced the counterpart for `multiset` of `finset.prod_dvd_prod`. It makes sense for these to have the same name, but there's already a different lemma called `multiset.prod_dvd_prod`, so the new lemma was named `multiset.prod_dvd_prod_of_dvd` instead. As discussed with @riccardobrasca and @ericrbg at #11693, this PR brings the names of the two counterpart lemmas into alignment, and also renames `multiset.prod_dvd_prod` to something more informative.
Renaming as follows:
`multiset.prod_dvd_prod` to `multiset.prod_dvd_prod_of_le`
`finset.prod_dvd_prod` to `finset.prod_dvd_prod_of_dvd`
