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>

Author: agusakov

src/data/set/finite.lean

@@ -573,6 +573,10 @@ section
 
 local attribute [instance, priority 1] classical.prop_decidable
 
+lemma to_finset_compl {α : Type*} [fintype α] (s : set α) :
+  sᶜ.to_finset = (s.to_finset)ᶜ :=
+by ext; simp
+
 lemma to_finset_inter {α : Type*} [fintype α] (s t : set α) :
   (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
 by ext; simp