refactor(order/filter/basic): drop a lemma (#18254)
- Drop `filter.subtype_coe_map_comap_prod`. This lemma was used once in `mathlib` and Lean 4 has no `list_pair` instance that is used in its statement.
- Add `uniformity_set_coe`. For some reason, Lean fails to rewrite on `uniformity_subtype` in this context.
- Fix&golf a proof.
