From b6e6c84fb5e995639290f464edb5d55d38c2b60d Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 25 Aug 2021 18:32:52 +0000
Subject: [PATCH] feat(data/finset/basic): to_list (#8797)

Produce a list of the elements of a finite set using choice.
---
 src/data/finset/basic.lean | 37 ++++++++++++++++++++++++++++++-------
 src/data/finset/sort.lean  |  3 +++
 2 files changed, 33 insertions(+), 7 deletions(-)

diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean
index 55a08a513d741..000f7b3d060f9 100644
--- a/src/data/finset/basic.lean
+++ b/src/data/finset/basic.lean
@@ -1765,13 +1765,6 @@ 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
@@ -2490,6 +2483,36 @@ subtype.ext_iff_val.1 (@hif ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ (subtype.eq ha
 
 end card
 
+section to_list
+
+/-- Produce a list of the elements in the finite set using choice. -/
+@[reducible] noncomputable def to_list (s : finset α) : list α := s.1.to_list
+
+lemma nodup_to_list (s : finset α) : s.to_list.nodup :=
+by { rw [to_list, ←multiset.coe_nodup, multiset.coe_to_list], exact s.nodup }
+
+@[simp] lemma mem_to_list {a : α} (s : finset α) : a ∈ s.to_list ↔ a ∈ s :=
+by { rw [to_list, ←multiset.mem_coe, multiset.coe_to_list], exact iff.rfl }
+
+@[simp] lemma length_to_list (s : finset α) : s.to_list.length = s.card :=
+by { rw [to_list, ←multiset.coe_card, multiset.coe_to_list], refl }
+
+@[simp] lemma to_list_empty : (∅ : finset α).to_list = [] :=
+by simp [to_list]
+
+@[simp, norm_cast]
+lemma coe_to_list (s : finset α) : (s.to_list : multiset α) = s.val :=
+by { classical, ext, simp }
+
+@[simp] lemma to_list_to_finset [decidable_eq α] (s : finset α) : s.to_list.to_finset = s :=
+by { ext, simp }
+
+lemma exists_list_nodup_eq [decidable_eq α] (s : finset α) :
+  ∃ (l : list α), l.nodup ∧ l.to_finset = s :=
+⟨s.to_list, s.nodup_to_list, s.to_list_to_finset⟩
+
+end to_list
+
 section bUnion
 /-!
 ### bUnion
diff --git a/src/data/finset/sort.lean b/src/data/finset/sort.lean
index 46684f5b8c2a1..613496fa940ec 100644
--- a/src/data/finset/sort.lean
+++ b/src/data/finset/sort.lean
@@ -43,6 +43,9 @@ multiset.mem_sort _
 @[simp] theorem length_sort {s : finset α} : (sort r s).length = s.card :=
 multiset.length_sort _
 
+lemma sort_perm_to_list (s : finset α) : sort r s ~ s.to_list :=
+by { rw ←multiset.coe_eq_coe, simp only [coe_to_list, sort_eq] }
+
 end sort
 
 section sort_linear_order