Commit 2025-10-24 09:13 3d2dfe86
View on Github →feat(Data/Finset/Card): add some more Pigeonhole Principle theorems exists_ne_map_eq_of_card_image_lt and not_injOn_of_card_image_lt (#28077)
exists_ne_map_eq_of_card_image_lt is a special case of exists_ne_map_eq_of_card_lt_of_maps_to where t is s.image f, and not_injOn_of_card_image_lt is its variant using Set.InjOn. I ran into some cases where such theorems would save me some time.