Commit 2022-04-26 04:54 748ea79b

feat(order/filter/basic): more lemmas about filter.comap (#13619)

• add set.compl_def, set.finite_image_fst_and_snd_iff, and set.forall_finite_image_eval_iff;
• add filter.coext, an extensionality lemma that is more useful for "cofilters";
• rename filter.eventually_comap' to filter.eventually.comap;
• add filter.mem_comap', filter.mem_comap_iff_compl, and filter.compl_mem_comap;
• add filter.compl_mem_coprod, replace filter.compl_mem_Coprod_iff with a simpler filter.compl_mem_Coprod;
• add filter.map_top;
• use new lemmas to golf some proofs.