chore(data/multiset/pi): correct names and reorder (#19050)
* `multiset.pi_cons_injective` is about `multiset.pi.cons` so should have a `.` in its name.
* `multiset.pi.cons_ext` is not an ext lemma, but more closely resembles eta-reduction.
This also groups together the lemmas about `pi.cons`.
