mathlib

58903102 - feat(src/data/*): lemmas about emptiness for finset/multiset/vector coercions (#16113)

feat(src/data/*): lemmas about emptiness for finset/multiset/vector coercions (#16113) Adds basic lemmas about whether the result of `to_list` is empty for various data structures. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>