mathlib3

bd81d555 - feat(data/finsupp): add lemmas about `single` (#9894)

feat(data/finsupp): add lemmas about `single` (#9894) These are subset versions of the four lemmas related to `support_eq_singleton`. Co-authored-by: Johan Commelin <johan@commelin.net>