mathlib

b142b697 - feat(data/list/count): add lemma `count_le_count_map` (#11148)

feat(data/list/count): add lemma `count_le_count_map` (#11148) Generalises `count_map_map`: for any `f : α → β` (not necessarily injective), `count x l ≤ count (f x) (map f l)`