feat(data/finset/basic): perm_of_nodup_nodup_to_finset_eq (#7588)

Also `finset.exists_list_nodup_eq`.



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

src/data/finset/basic.lean

@@ -1602,6 +1602,10 @@ def to_finset (s : multiset α) : finset α := ⟨_, nodup_erase_dup s⟩
 theorem to_finset_eq {s : multiset α} (n : nodup s) : finset.mk s n = s.to_finset :=
 finset.val_inj.1 (erase_dup_eq_self.2 n).symm
 
+lemma nodup.to_finset_inj {l l' : multiset α} (hl : nodup l) (hl' : nodup l')
+  (h : l.to_finset = l'.to_finset) : l = l' :=
+by simpa [←to_finset_eq hl, ←to_finset_eq hl'] using h
+
 @[simp] theorem mem_to_finset {a : α} {s : multiset α} : a ∈ s.to_finset ↔ a ∈ s :=
 mem_erase_dup
 
@@ -1689,6 +1693,13 @@ lemma to_finset_eq_of_perm (l l' : list α) (h : l ~ l') :
   l.to_finset = l'.to_finset :=
 to_finset_eq_iff_perm_erase_dup.mpr h.erase_dup
 
+lemma perm_of_nodup_nodup_to_finset_eq {l l' : list α} (hl : nodup l) (hl' : nodup l')
+  (h : l.to_finset = l'.to_finset) : l ~ l' :=
+begin
+  rw ←multiset.coe_eq_coe,
+  exact multiset.nodup.to_finset_inj hl hl' h
+end
+
 @[simp] lemma to_finset_append {l l' : list α} :
   to_finset (l ++ l') = l.to_finset ∪ l'.to_finset :=
 begin
@@ -1705,6 +1716,13 @@ end list
 
 namespace finset
 
+lemma exists_list_nodup_eq [decidable_eq α] (s : finset α) :
+  ∃ (l : list α), l.nodup ∧ l.to_finset = s :=
+begin
+  obtain ⟨⟨l⟩, hs⟩ := s,
+  exact ⟨l, hs, (list.to_finset_eq _).symm⟩,
+end
+
 /-! ### map -/
 section map
 open function