chore(*): golf some proofs (#5983)
API changes:
* new lemmas `finset.card_filter_le`, `finset.compl_filter`, `finset.card_lt_univ_of_not_mem`, `fintype.card_le_of_embedding`, `fintype.card_lt_of_injective_not_surjective`;
* rename `finset.card_le_of_inj_on` → `finset.le_card_of_inj_on_range`;
* rename `card_lt_of_injective_of_not_mem` to `fintype.card_lt_of_injective_of_not_mem`;
* generalize `card_units_lt` to a `monoid_with_zero`.
