feat(data/finset): sup_eq_bind (#5717)

`finset.sup s f` is equal to `finset.bind s f` when `f : α → finset β` is an indexed family of finite sets.  This is a proof of that with a couple supporting lemmas.  (There might be a more direct proof through the definitions of `sup` and `bind`, which are eventually in terms of `multiset.foldr`.)

I also moved `finset.mem_sup` to `multiset.mem_sup` and gave a new `finset.mem_sup` for indexed families of `finset`, where the old one was for indexed families of `multiset`.

Author: kmill

src/data/finset/basic.lean

@@ -1414,6 +1414,13 @@ by simp only [finset.subset_iff, multiset.subset_iff, multiset.mem_to_finset]
 
 end multiset
 
+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] }
+
+end finset
+
 namespace list
 variable [decidable_eq α]
 

src/data/finset/lattice.lean

@@ -86,35 +86,17 @@ lemma sup_coe {P : α → Prop}
   (@sup _ _ (subtype.semilattice_sup_bot Pbot Psup) t f : α) = t.sup (λ x, f x) :=
 by { classical, rw [comp_sup_eq_sup_comp coe]; intros; refl }
 
+@[simp] lemma sup_to_finset {α β} [decidable_eq β]
+  (s : finset α) (f : α → multiset β) :
+  (s.sup f).to_finset = s.sup (λ x, (f x).to_finset) :=
+comp_sup_eq_sup_comp multiset.to_finset to_finset_union rfl
+
 theorem subset_range_sup_succ (s : finset ℕ) : s ⊆ range (s.sup id).succ :=
 λ n hn, mem_range.2 $ nat.lt_succ_of_le $ le_sup hn
 
 theorem exists_nat_subset_range (s : finset ℕ) : ∃n : ℕ, s ⊆ range n :=
 ⟨_, s.subset_range_sup_succ⟩
 
-lemma mem_sup {α β} [decidable_eq β] {s : finset α} {f : α → multiset β}
-  {x : β} : x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v :=
-begin
-  classical,
-  apply s.induction_on,
-  { simp },
-  { intros a s has hxs,
-    rw [finset.sup_insert, multiset.sup_eq_union, multiset.mem_union],
-    split,
-    { intro hxi,
-      cases hxi with hf hf,
-      { refine ⟨a, _, hf⟩,
-        simp only [true_or, eq_self_iff_true, finset.mem_insert] },
-      { rcases hxs.mp hf with ⟨v, hv, hfv⟩,
-        refine ⟨v, _, hfv⟩,
-        simp only [hv, or_true, finset.mem_insert] } },
-    { rintros ⟨v, hv, hfv⟩,
-      rw [finset.mem_insert] at hv,
-      rcases hv with rfl | hv,
-      { exact or.inl hfv },
-      { refine or.inr (hxs.mpr ⟨v, hv, hfv⟩) } } },
-end
-
 lemma sup_subset {α β} [semilattice_sup_bot β] {s t : finset α} (hst : s ⊆ t) (f : α → β) :
   s.sup f ≤ t.sup f :=
 by classical;
@@ -432,8 +414,46 @@ begin
     refl }
 end
 
+lemma mem_sup {α β} [decidable_eq β] {s : finset α} {f : α → multiset β}
+  {x : β} : x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v :=
+begin
+  classical,
+  apply s.induction_on,
+  { simp },
+  { intros a s has hxs,
+    rw [finset.sup_insert, multiset.sup_eq_union, multiset.mem_union],
+    split,
+    { intro hxi,
+      cases hxi with hf hf,
+      { refine ⟨a, _, hf⟩,
+        simp only [true_or, eq_self_iff_true, finset.mem_insert] },
+      { rcases hxs.mp hf with ⟨v, hv, hfv⟩,
+        refine ⟨v, _, hfv⟩,
+        simp only [hv, or_true, finset.mem_insert] } },
+    { rintros ⟨v, hv, hfv⟩,
+      rw [finset.mem_insert] at hv,
+      rcases hv with rfl | hv,
+      { exact or.inl hfv },
+      { refine or.inr (hxs.mpr ⟨v, hv, hfv⟩) } } },
+end
+
 end multiset
 
+namespace finset
+
+lemma mem_sup {α β} [decidable_eq β] {s : finset α} {f : α → finset β}
+  {x : β} : x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v :=
+begin
+  change _ ↔ ∃ v ∈ s, x ∈ (f v).val,
+  rw [←multiset.mem_sup, ←multiset.mem_to_finset, sup_to_finset],
+  simp_rw [val_to_finset],
+end
+
+lemma sup_eq_bind {α β} [decidable_eq β] (s : finset α) (t : α → finset β) :
+  s.sup t = s.bind t :=
+by { ext, rw [mem_sup, mem_bind], }
+
+end finset
 
 section lattice
 variables {ι : Type*} {ι' : Sort*} [complete_lattice α]

src/data/mv_polynomial/variables.lean

@@ -152,7 +152,7 @@ lemma degrees_pow (p : mv_polynomial σ R) :
 
 lemma mem_degrees {p : mv_polynomial σ R} {i : σ} :
   i ∈ p.degrees ↔ ∃ d, p.coeff d ≠ 0 ∧ i ∈ d.support :=
-by simp only [degrees, finset.mem_sup, ← finsupp.mem_support_iff, coeff,
+by simp only [degrees, multiset.mem_sup, ← finsupp.mem_support_iff, coeff,
     finsupp.mem_to_multiset, exists_prop]
 
 lemma le_degrees_add {p q : mv_polynomial σ R} (h : p.degrees.disjoint q.degrees) :