mathlib

748ea79b - feat(order/filter/basic): more lemmas about `filter.comap` (#13619)

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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>