feat(data/set/finite): remove exists_finset_of_finite (#1782)

* feat(data/set/finite): remove exists_finset_of_finite

exists_finset_of_finite is a duplicate of finite.exists_finset_coe
At same time, provide a `can_lift` instance to lift sets to finsets.

* Add docstring

src/data/set/finite.lean

@@ -35,16 +35,19 @@ noncomputable def finite.to_finset {s : set α} (h : finite s) : finset α :=
 lemma finite.coe_to_finset {α} {s : set α} (h : finite s) : ↑h.to_finset = s :=
 by { ext, apply mem_to_finset }
 
-lemma exists_finset_of_finite {s : set α} (h : finite s) : ∃(s' : finset α), ↑s' = s :=
-⟨h.to_finset, h.coe_to_finset⟩
-
 theorem finite.exists_finset {s : set α} : finite s →
   ∃ s' : finset α, ∀ a : α, a ∈ s' ↔ a ∈ s
 | ⟨h⟩ := by exactI ⟨to_finset s, λ _, mem_to_finset⟩
 
 theorem finite.exists_finset_coe {s : set α} (hs : finite s) :
   ∃ s' : finset α, ↑s' = s :=
-let ⟨s', h⟩ := hs.exists_finset in ⟨s', set.ext h⟩
+⟨hs.to_finset, hs.coe_to_finset⟩
+
+/-- Finite sets can be lifted to finsets. -/
+instance : can_lift (set α) (finset α) :=
+{ coe := coe,
+  cond := finite,
+  prf := λ s hs, hs.exists_finset_coe }
 
 theorem finite_mem_finset (s : finset α) : finite {a | a ∈ s} :=
 ⟨fintype.of_finset s (λ _, iff.rfl)⟩