feat(data/{finset,finsupp,multiset}): more assorted lemmas (#4006)

Another grab bag of facts from the Witt vector branch.

Coauthored by: Johan Commelin <johan@commelin.net>

<!-- put comments you want to keep out of the PR commit here -->


Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/finset/basic.lean

@@ -422,6 +422,10 @@ theorem subset_union_left (s₁ s₂ : finset α) : s₁ ⊆ s₁ ∪ s₂ := λ
 
 theorem subset_union_right (s₁ s₂ : finset α) : s₂ ⊆ s₁ ∪ s₂ := λ x, mem_union_right _
 
+lemma union_subset_union {s1 t1 s2 t2 : finset α} (h1 : s1 ⊆ t1) (h2 : s2 ⊆ t2) :
+  s1 ∪ s2 ⊆ t1 ∪ t2 :=
+by { intros x hx, rw finset.mem_union at hx ⊢, tauto }
+
 theorem union_comm (s₁ s₂ : finset α) : s₁ ∪ s₂ = s₂ ∪ s₁ :=
 ext $ λ x, by simp only [mem_union, or_comm]
 
@@ -1203,9 +1207,17 @@ finset.ext $ by simp
   to_finset (s ∩ t) = to_finset s ∩ to_finset t :=
 finset.ext $ by simp
 
+@[simp] lemma to_finset_union (s t : multiset α) :
+  (s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
+by ext; simp
+
 theorem to_finset_eq_empty {m : multiset α} : m.to_finset = ∅ ↔ m = 0 :=
 finset.val_inj.symm.trans multiset.erase_dup_eq_zero
 
+@[simp] lemma to_finset_subset (m1 m2 : multiset α) :
+  m1.to_finset ⊆ m2.to_finset ↔ m1 ⊆ m2 :=
+by simp only [finset.subset_iff, multiset.subset_iff, multiset.mem_to_finset]
+
 end multiset
 
 namespace list
@@ -2099,3 +2111,21 @@ theorem to_finset_card_of_nodup {l : list α} (h : l.nodup) : l.to_finset.card =
 congr_arg card $ (@multiset.erase_dup_eq_self α _ l).2 h
 
 end list
+
+namespace multiset
+
+lemma disjoint_to_finset [decidable_eq α] (m1 m2 : multiset α) :
+  _root_.disjoint m1.to_finset m2.to_finset ↔ m1.disjoint m2 :=
+begin
+  rw finset.disjoint_iff_ne,
+  split,
+  { intro h,
+    intros a ha1 ha2,
+    rw ← multiset.mem_to_finset at ha1 ha2,
+    exact h _ ha1 _ ha2 rfl },
+  { rintros h a ha b hb rfl,
+    rw multiset.mem_to_finset at ha hb,
+    exact h ha hb }
+end
+
+end multiset

src/data/finset/fold.lean

@@ -106,6 +106,20 @@ end
 
 omit hc ha
 
+@[simp]
+lemma fold_union_empty_singleton [decidable_eq α] (s : finset α) :
+  finset.fold (∪) ∅ singleton s = s :=
+begin
+  apply finset.induction_on s,
+  { simp only [fold_empty], },
+  { intros a s has ih, rw [fold_insert has, ih, insert_eq], }
+end
+
+@[simp]
+lemma fold_sup_bot_singleton [decidable_eq α] (s : finset α) :
+  finset.fold (⊔) ⊥ singleton s = s :=
+fold_union_empty_singleton s
+
 section order
 variables [decidable_linear_order β] (c : β)
 

src/data/finset/lattice.lean

@@ -90,6 +90,36 @@ theorem subset_range_sup_succ (s : finset ℕ) : s ⊆ range (s.sup id).succ :=
 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;
+calc t.sup f = (s ∪ t).sup f : by rw [finset.union_eq_right_iff_subset.mpr hst]
+         ... = s.sup f ⊔ t.sup f : by rw finset.sup_union
+         ... ≥ s.sup f : le_sup_left
+
 end sup
 
 lemma sup_eq_supr [complete_lattice β] (s : finset α) (f : α → β) : s.sup f = (⨆a∈s, f a) :=

src/data/finsupp/basic.lean

@@ -1313,6 +1313,10 @@ lemma mem_support_single [has_zero β] (a a' : α) (b : β) :
   else ⟨by rw if_neg h at H; exact mem_singleton.1 H, h⟩,
 λ ⟨h1, h2⟩, show a ∈ ite _ _ _, by rw [if_neg h2]; exact mem_singleton.2 h1⟩
 
+@[simp] lemma mem_to_multiset (f : α →₀ ℕ) (i : α) :
+  i ∈ f.to_multiset ↔ i ∈ f.support :=
+by rw [← multiset.count_ne_zero, finsupp.count_to_multiset, finsupp.mem_support_iff]
+
 end multiset
 
 /-! ### Declarations about `curry` and `uncurry` -/

src/data/multiset/basic.lean

@@ -1646,6 +1646,9 @@ by_contradiction $ λ h', h $ count_pos.1 (nat.pos_of_ne_zero h')
 theorem count_eq_zero {a : α} {s : multiset α} : count a s = 0 ↔ a ∉ s :=
 iff_not_comm.1 $ count_pos.symm.trans pos_iff_ne_zero
 
+theorem count_ne_zero {a : α} {s : multiset α} : count a s ≠ 0 ↔ a ∈ s :=
+by simp [ne.def, count_eq_zero]
+
 @[simp] theorem count_repeat (a : α) (n : ℕ) : count a (repeat a n) = n :=
 by simp [repeat]