refactor(order/filter/bases): allow `ι : Sort*` (#8856)
* `ι` in `filter.has_basis (l : filter α) (p : ι → Prop) (s : ι → set )` now can be a `Sort *`;
* some lemmas now have "primed" versions that use `pprod` instead of `prod`;
* new lemma: `filter.has_basis_supr`.
I also added a few missing lemmas to `data.pprod` and golfed a couple of proofs.
