feat(data/multiset/basic): add_eq_union_iff_disjoint (#8173)

src/data/multiset/basic.lean

@@ -2294,6 +2294,11 @@ by simp [disjoint, or_imp_distrib, forall_and_distrib]
   disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u :=
 by simp [disjoint, or_imp_distrib, forall_and_distrib]
 
+lemma add_eq_union_iff_disjoint [decidable_eq α] {s t : multiset α} :
+  s + t = s ∪ t ↔ disjoint s t :=
+by simp_rw [←inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
+            nat.min_eq_zero_iff, nat.add_eq_max_iff]
+
 lemma disjoint_map_map {f : α → γ} {g : β → γ} {s : multiset α} {t : multiset β} :
   disjoint (s.map f) (t.map g) ↔ (∀a∈s, ∀b∈t, f a ≠ g b) :=
 by { simp [disjoint, @eq_comm _ (f _) (g _)], refl }

src/data/nat/basic.lean

@@ -222,6 +222,46 @@ theorem le_zero_iff {i : ℕ} : i ≤ 0 ↔ i = 0 :=
 lemma zero_max {m : ℕ} : max 0 m = m :=
 max_eq_right (zero_le _)
 
+@[simp] lemma min_eq_zero_iff {m n : ℕ} : min m n = 0 ↔ m = 0 ∨ n = 0 :=
+begin
+  split,
+  { intro h,
+    cases le_total n m with H H,
+    { simpa [H] using or.inr h },
+    { simpa [H] using or.inl h } },
+  { rintro (rfl|rfl);
+    simp }
+end
+
+@[simp] lemma max_eq_zero_iff {m n : ℕ} : max m n = 0 ↔ m = 0 ∧ n = 0 :=
+begin
+  split,
+  { intro h,
+    cases le_total n m with H H,
+    { simp only [H, max_eq_left] at h,
+      exact ⟨h, le_antisymm (H.trans h.le) (zero_le _)⟩ },
+    { simp only [H, max_eq_right] at h,
+      exact ⟨le_antisymm (H.trans h.le) (zero_le _), h⟩ } },
+  { rintro ⟨rfl, rfl⟩,
+    simp }
+end
+
+lemma add_eq_max_iff {n m : ℕ} :
+  n + m = max n m ↔ n = 0 ∨ m = 0 :=
+begin
+  rw ←min_eq_zero_iff,
+  cases le_total n m with H H;
+  simp [H]
+end
+
+lemma add_eq_min_iff {n m : ℕ} :
+  n + m = min n m ↔ n = 0 ∧ m = 0 :=
+begin
+  rw ←max_eq_zero_iff,
+  cases le_total n m with H H;
+  simp [H]
+end
+
 lemma one_le_of_lt {n m : ℕ} (h : n < m) : 1 ≤ m :=
 lt_of_le_of_lt (nat.zero_le _) h