mathlib3

ba876475 - feat(data/set/finite): add lemma about to_finset of complement of set (#5881)

feat(data/set/finite): add lemma about to_finset of complement of set (#5881) Add lemma stating that taking to_finset of the complement of a set is the same thing as taking the complement of to_finset of the set. Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>