feat(order/filter/cofinite): add lemmas, golf (#13394)
* add `filter.comap_le_cofinite`,
`function.injective.comap_cofinite_eq`, and
`filter.has_basis.coprod`;
* rename `at_top_le_cofinite` to `filter.at_top_le_cofinite`;
* golf `filter.coprod_cofinite` and `filter.Coprod_cofinite`, move
them below `filter.comap_cofinite_le`;
