feat(data/finset/basic): val_le_iff_val_subset (#10603)

I'm not sure if we have something like this already on mathlib. The application of `val_le_of_val_subset` that I have in mind is to deduce

```
theorem polynomial.card_roots'' {F : Type u} [field F]{p : polynomial F}(h : p ≠ 0)
{Z : finset F} (hZ : ∀ z ∈ Z, polynomial.eval z p = 0) : Z.card ≤ p.nat_degree
```
from [polynomial.card_roots' ](https://github.com/leanprover-community/mathlib/blob/1376f53dacd3c3ccd3c345b6b8552cce96c5d0c8/src/data/polynomial/ring_division.lean#L318)

If this approach seems right, I will send the proof of `polynomial.card_roots''` in a follow up PR.



Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>

src/data/finset/basic.lean

@@ -1782,6 +1782,9 @@ namespace finset
 @[simp] lemma val_to_finset [decidable_eq α] (s : finset α) : s.val.to_finset = s :=
 by { ext, rw [multiset.mem_to_finset, ←mem_def] }
 
+lemma val_le_iff_val_subset {a : finset α} {b : multiset α} :
+  a.val ≤ b ↔ a.val ⊆ b := multiset.le_iff_subset a.nodup
+
 end finset
 
 namespace list

src/data/multiset/basic.lean

@@ -2032,6 +2032,9 @@ by induction n; simp [*, succ_nsmul', succ_mul, zero_nsmul]
 theorem count_pos {a : α} {s : multiset α} : 0 < count a s ↔ a ∈ s :=
 by simp [count, countp_pos]
 
+theorem one_le_count_iff_mem {a : α} {s : multiset α} : 1 ≤ count a s ↔ a ∈ s :=
+by rw [succ_le_iff, count_pos]
+
 @[simp, priority 980]
 theorem count_eq_zero_of_not_mem {a : α} {s : multiset α} (h : a ∉ s) : count a s = 0 :=
 by_contradiction $ λ h', h $ count_pos.1 (nat.pos_of_ne_zero h')