Commit 2022-04-12 20:53 78ea75a0

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;