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 <759412786bc533369b22377bf83fb9056c5b25b2@commelin.net>

leanprover-community/mathlib,leanprover-community/mathlib