chore(Data/List): Use Std lemmas (#11711)

Make use of `Nat`-specific lemmas from Std rather than the general ones provided by mathlib. Also reverse the dependency between `Multiset.Nodup`/`Multiset.dedup` and `Multiset.sum` since only the latter needs algebra. Also rename `Algebra.BigOperators.Multiset.Abs` to `Algebra.BigOperators.Multiset.Order` and move some lemmas from `Algebra.BigOperators.Multiset.Basic` to it. The ultimate goal here is to carve out `Data`, `Algebra` and `Order` sublibraries.
leanprover-community · Mar 27, 2024 · 3713a3f · 3713a3f
1 parent 48efc23
commit 3713a3f
Show file tree

Hide file tree

Showing 25 changed files with 318 additions and 342 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -29,9 +29,9 @@ import Mathlib.Algebra.BigOperators.Finprod
 import Mathlib.Algebra.BigOperators.Finsupp
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Module
-import Mathlib.Algebra.BigOperators.Multiset.Abs
 import Mathlib.Algebra.BigOperators.Multiset.Basic
 import Mathlib.Algebra.BigOperators.Multiset.Lemmas
+import Mathlib.Algebra.BigOperators.Multiset.Order
 import Mathlib.Algebra.BigOperators.NatAntidiagonal
 import Mathlib.Algebra.BigOperators.Option
 import Mathlib.Algebra.BigOperators.Order

diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.BigOperators.Multiset.Lemmas
+import Mathlib.Algebra.BigOperators.Multiset.Order
 import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.Ring.Opposite
 import Mathlib.Data.Finset.Powerset

diff --git a/Mathlib/Algebra/BigOperators/Multiset/Abs.lean b/Mathlib/Algebra/BigOperators/Multiset/Abs.lean
diff --git a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
@@ -3,10 +3,9 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Mathlib.Algebra.Group.Hom.Basic
 import Mathlib.Algebra.GroupPower.Hom
-import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Algebra.Order.Monoid.OrderDual
-import Mathlib.Algebra.Ring.Divisibility.Basic
+import Mathlib.Data.List.BigOperators.Basic
 import Mathlib.Data.Multiset.Basic
 
 #align_import algebra.big_operators.multiset.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"
@@ -150,6 +149,12 @@ theorem prod_eq_pow_single [DecidableEq α] (a : α) (h : ∀ a' ≠ a, a' ∈ s
 #align multiset.prod_eq_pow_single Multiset.prod_eq_pow_single
 #align multiset.sum_eq_nsmul_single Multiset.sum_eq_nsmul_single
 
+@[to_additive]
+lemma prod_eq_one (h : ∀ x ∈ s, x = (1 : α)) : s.prod = 1 := by
+  induction' s using Quotient.inductionOn with l; simp [List.prod_eq_one h]
+#align multiset.prod_eq_one Multiset.prod_eq_one
+#align multiset.sum_eq_zero Multiset.sum_eq_zero
+
 @[to_additive]
 theorem pow_count [DecidableEq α] (a : α) : a ^ s.count a = (s.filter (Eq a)).prod := by
   rw [filter_eq, prod_replicate]
@@ -203,12 +208,6 @@ theorem prod_map_mul : (m.map fun i => f i * g i).prod = (m.map f).prod * (m.map
 #align multiset.prod_map_mul Multiset.prod_map_mul
 #align multiset.sum_map_add Multiset.sum_map_add
 
-@[simp]
-theorem prod_map_neg [HasDistribNeg α] (s : Multiset α) :
-    (s.map Neg.neg).prod = (-1) ^ card s * s.prod :=
-  Quotient.inductionOn s (by simp)
-#align multiset.prod_map_neg Multiset.prod_map_neg
-
 @[to_additive]
 theorem prod_map_pow {n : ℕ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n :=
   m.prod_hom' (powMonoidHom n : α →* α) f
@@ -279,30 +278,6 @@ theorem coe_sumAddMonoidHom : (sumAddMonoidHom : Multiset α → α) = sum :=
 
 end AddCommMonoid
 
-section CommMonoidWithZero
-
-variable [CommMonoidWithZero α]
-
-theorem prod_eq_zero {s : Multiset α} (h : (0 : α) ∈ s) : s.prod = 0 := by
-  rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩
-  simp [hs', Multiset.prod_cons]
-#align multiset.prod_eq_zero Multiset.prod_eq_zero
-
-variable [NoZeroDivisors α] [Nontrivial α] {s : Multiset α}
-
-@[simp]
-theorem prod_eq_zero_iff : s.prod = 0 ↔ (0 : α) ∈ s :=
-  Quotient.inductionOn s fun l => by
-    rw [quot_mk_to_coe, prod_coe]
-    exact List.prod_eq_zero_iff
-#align multiset.prod_eq_zero_iff Multiset.prod_eq_zero_iff
-
-theorem prod_ne_zero (h : (0 : α) ∉ s) : s.prod ≠ 0 :=
-  mt prod_eq_zero_iff.1 h
-#align multiset.prod_ne_zero Multiset.prod_ne_zero
-
-end CommMonoidWithZero
-
 section DivisionCommMonoid
 
 variable [DivisionCommMonoid α] {m : Multiset ι} {f g : ι → α}
@@ -349,194 +324,6 @@ theorem sum_map_mul_right : sum (s.map fun i => f i * a) = sum (s.map f) * a :=
 
 end NonUnitalNonAssocSemiring
 
-section NonUnitalSemiring
-
-variable [NonUnitalSemiring α]
-
-theorem dvd_sum {a : α} {s : Multiset α} : (∀ x ∈ s, a ∣ x) → a ∣ s.sum :=
-  Multiset.induction_on s (fun _ => dvd_zero _) fun x s ih h => by
-    rw [sum_cons]
-    exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy => h _ <| mem_cons.2 <| Or.inr hy)
-#align multiset.dvd_sum Multiset.dvd_sum
-
-end NonUnitalSemiring
-
-/-! ### Order -/
-
-
-section OrderedCommMonoid
-
-variable [OrderedCommMonoid α] {s t : Multiset α} {a : α}
-
-@[to_additive sum_nonneg]
-theorem one_le_prod_of_one_le : (∀ x ∈ s, (1 : α) ≤ x) → 1 ≤ s.prod :=
-  Quotient.inductionOn s fun l hl => by simpa using List.one_le_prod_of_one_le hl
-#align multiset.one_le_prod_of_one_le Multiset.one_le_prod_of_one_le
-#align multiset.sum_nonneg Multiset.sum_nonneg
-
-@[to_additive]
-theorem single_le_prod : (∀ x ∈ s, (1 : α) ≤ x) → ∀ x ∈ s, x ≤ s.prod :=
-  Quotient.inductionOn s fun l hl x hx => by simpa using List.single_le_prod hl x hx
-#align multiset.single_le_prod Multiset.single_le_prod
-#align multiset.single_le_sum Multiset.single_le_sum
-
-@[to_additive sum_le_card_nsmul]
-theorem prod_le_pow_card (s : Multiset α) (n : α) (h : ∀ x ∈ s, x ≤ n) : s.prod ≤ n ^ card s := by
-  induction s using Quotient.inductionOn
-  simpa using List.prod_le_pow_card _ _ h
-#align multiset.prod_le_pow_card Multiset.prod_le_pow_card
-#align multiset.sum_le_card_nsmul Multiset.sum_le_card_nsmul
-
-@[to_additive all_zero_of_le_zero_le_of_sum_eq_zero]
-theorem all_one_of_le_one_le_of_prod_eq_one :
-    (∀ x ∈ s, (1 : α) ≤ x) → s.prod = 1 → ∀ x ∈ s, x = (1 : α) :=
-  Quotient.inductionOn s (by
-    simp only [quot_mk_to_coe, prod_coe, mem_coe]
-    exact fun l => List.all_one_of_le_one_le_of_prod_eq_one)
-#align multiset.all_one_of_le_one_le_of_prod_eq_one Multiset.all_one_of_le_one_le_of_prod_eq_one
-#align multiset.all_zero_of_le_zero_le_of_sum_eq_zero Multiset.all_zero_of_le_zero_le_of_sum_eq_zero
-
-@[to_additive]
-theorem prod_le_prod_of_rel_le (h : s.Rel (· ≤ ·) t) : s.prod ≤ t.prod := by
-  induction' h with _ _ _ _ rh _ rt
-  · rfl
-  · rw [prod_cons, prod_cons]
-    exact mul_le_mul' rh rt
-#align multiset.prod_le_prod_of_rel_le Multiset.prod_le_prod_of_rel_le
-#align multiset.sum_le_sum_of_rel_le Multiset.sum_le_sum_of_rel_le
-
-@[to_additive]
-theorem prod_map_le_prod_map {s : Multiset ι} (f : ι → α) (g : ι → α) (h : ∀ i, i ∈ s → f i ≤ g i) :
-    (s.map f).prod ≤ (s.map g).prod :=
-  prod_le_prod_of_rel_le <| rel_map.2 <| rel_refl_of_refl_on h
-#align multiset.prod_map_le_prod_map Multiset.prod_map_le_prod_map
-#align multiset.sum_map_le_sum_map Multiset.sum_map_le_sum_map
-
-@[to_additive]
-theorem prod_map_le_prod (f : α → α) (h : ∀ x, x ∈ s → f x ≤ x) : (s.map f).prod ≤ s.prod :=
-  prod_le_prod_of_rel_le <| rel_map_left.2 <| rel_refl_of_refl_on h
-#align multiset.prod_map_le_prod Multiset.prod_map_le_prod
-#align multiset.sum_map_le_sum Multiset.sum_map_le_sum
-
-@[to_additive]
-theorem prod_le_prod_map (f : α → α) (h : ∀ x, x ∈ s → x ≤ f x) : s.prod ≤ (s.map f).prod :=
-  @prod_map_le_prod αᵒᵈ _ _ f h
-#align multiset.prod_le_prod_map Multiset.prod_le_prod_map
-#align multiset.sum_le_sum_map Multiset.sum_le_sum_map
-
-@[to_additive card_nsmul_le_sum]
-theorem pow_card_le_prod (h : ∀ x ∈ s, a ≤ x) : a ^ card s ≤ s.prod := by
-  rw [← Multiset.prod_replicate, ← Multiset.map_const]
-  exact prod_map_le_prod _ h
-#align multiset.pow_card_le_prod Multiset.pow_card_le_prod
-#align multiset.card_nsmul_le_sum Multiset.card_nsmul_le_sum
-
-end OrderedCommMonoid
-
-section OrderedCancelCommMonoid
-
-variable [OrderedCancelCommMonoid α] {s : Multiset ι} {f g : ι → α}
-
-@[to_additive sum_lt_sum]
-theorem prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
-    (s.map f).prod < (s.map g).prod := by
-  obtain ⟨l⟩ := s
-  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
-  exact List.prod_lt_prod' f g hle hlt
-
-@[to_additive sum_lt_sum_of_nonempty]
-theorem prod_lt_prod_of_nonempty' (hs : s ≠ ∅) (hfg : ∀ i ∈ s, f i < g i) :
-    (s.map f).prod < (s.map g).prod := by
-  obtain ⟨i, hi⟩ := exists_mem_of_ne_zero hs
-  exact prod_lt_prod' (fun i hi => le_of_lt (hfg i hi)) ⟨i, hi, hfg i hi⟩
-
-end OrderedCancelCommMonoid
-
-theorem prod_nonneg [OrderedCommSemiring α] {m : Multiset α} (h : ∀ a ∈ m, (0 : α) ≤ a) :
-    0 ≤ m.prod := by
-  revert h
-  refine' m.induction_on _ _
-  · rintro -
-    rw [prod_zero]
-    exact zero_le_one
-  intro a s hs ih
-  rw [prod_cons]
-  exact mul_nonneg (ih _ <| mem_cons_self _ _) (hs fun a ha => ih _ <| mem_cons_of_mem ha)
-#align multiset.prod_nonneg Multiset.prod_nonneg
-
-/-- Slightly more general version of `Multiset.prod_eq_one_iff` for a non-ordered `Monoid` -/
-@[to_additive
-      "Slightly more general version of `Multiset.sum_eq_zero_iff` for a non-ordered `AddMonoid`"]
-theorem prod_eq_one [CommMonoid α] {m : Multiset α} (h : ∀ x ∈ m, x = (1 : α)) : m.prod = 1 := by
-  induction' m using Quotient.inductionOn with l
-  simp [List.prod_eq_one h]
-#align multiset.prod_eq_one Multiset.prod_eq_one
-#align multiset.sum_eq_zero Multiset.sum_eq_zero
-
-@[to_additive]
-theorem le_prod_of_mem [CanonicallyOrderedCommMonoid α] {m : Multiset α} {a : α} (h : a ∈ m) :
-    a ≤ m.prod := by
-  obtain ⟨m', rfl⟩ := exists_cons_of_mem h
-  rw [prod_cons]
-  exact _root_.le_mul_right (le_refl a)
-#align multiset.le_prod_of_mem Multiset.le_prod_of_mem
-#align multiset.le_sum_of_mem Multiset.le_sum_of_mem
-
-@[to_additive le_sum_of_subadditive_on_pred]
-theorem le_prod_of_submultiplicative_on_pred [CommMonoid α] [OrderedCommMonoid β] (f : α → β)
-    (p : α → Prop) (h_one : f 1 = 1) (hp_one : p 1)
-    (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b))
-    (s : Multiset α) (hps : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod := by
-  revert s
-  refine' Multiset.induction _ _
-  · simp [le_of_eq h_one]
-  intro a s hs hpsa
-  have hps : ∀ x, x ∈ s → p x := fun x hx => hpsa x (mem_cons_of_mem hx)
-  have hp_prod : p s.prod := prod_induction p s hp_mul hp_one hps
-  rw [prod_cons, map_cons, prod_cons]
-  exact (h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod).trans (mul_le_mul_left' (hs hps) _)
-#align multiset.le_prod_of_submultiplicative_on_pred Multiset.le_prod_of_submultiplicative_on_pred
-#align multiset.le_sum_of_subadditive_on_pred Multiset.le_sum_of_subadditive_on_pred
-
-@[to_additive le_sum_of_subadditive]
-theorem le_prod_of_submultiplicative [CommMonoid α] [OrderedCommMonoid β] (f : α → β)
-    (h_one : f 1 = 1) (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) :
-    f s.prod ≤ (s.map f).prod :=
-  le_prod_of_submultiplicative_on_pred f (fun _ => True) h_one trivial (fun x y _ _ => h_mul x y)
-    (by simp) s (by simp)
-#align multiset.le_prod_of_submultiplicative Multiset.le_prod_of_submultiplicative
-#align multiset.le_sum_of_subadditive Multiset.le_sum_of_subadditive
-
-@[to_additive le_sum_nonempty_of_subadditive_on_pred]
-theorem le_prod_nonempty_of_submultiplicative_on_pred [CommMonoid α] [OrderedCommMonoid β]
-    (f : α → β) (p : α → Prop) (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b)
-    (hp_mul : ∀ a b, p a → p b → p (a * b)) (s : Multiset α) (hs_nonempty : s ≠ ∅)
-    (hs : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod := by
-  revert s
-  refine' Multiset.induction _ _
-  · intro h
-    exfalso
-    exact h rfl
-  rintro a s hs - hsa_prop
-  rw [prod_cons, map_cons, prod_cons]
-  by_cases hs_empty : s = ∅
-  · simp [hs_empty]
-  have hsa_restrict : ∀ x, x ∈ s → p x := fun x hx => hsa_prop x (mem_cons_of_mem hx)
-  have hp_sup : p s.prod := prod_induction_nonempty p hp_mul hs_empty hsa_restrict
-  have hp_a : p a := hsa_prop a (mem_cons_self a s)
-  exact (h_mul a _ hp_a hp_sup).trans (mul_le_mul_left' (hs hs_empty hsa_restrict) _)
-#align multiset.le_prod_nonempty_of_submultiplicative_on_pred Multiset.le_prod_nonempty_of_submultiplicative_on_pred
-#align multiset.le_sum_nonempty_of_subadditive_on_pred Multiset.le_sum_nonempty_of_subadditive_on_pred
-
-@[to_additive le_sum_nonempty_of_subadditive]
-theorem le_prod_nonempty_of_submultiplicative [CommMonoid α] [OrderedCommMonoid β] (f : α → β)
-    (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) (hs_nonempty : s ≠ ∅) :
-    f s.prod ≤ (s.map f).prod :=
-  le_prod_nonempty_of_submultiplicative_on_pred f (fun _ => True) (by simp [h_mul]) (by simp) s
-    hs_nonempty (by simp)
-#align multiset.le_prod_nonempty_of_submultiplicative Multiset.le_prod_nonempty_of_submultiplicative
-#align multiset.le_sum_nonempty_of_subadditive Multiset.le_sum_nonempty_of_subadditive
-
 @[simp]
 theorem sum_map_singleton (s : Multiset α) : (s.map fun a => ({a} : Multiset α)).sum = s :=
   Multiset.induction_on s (by simp) (by simp)

diff --git a/Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean b/Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean
@@ -14,18 +14,54 @@ import Mathlib.Algebra.BigOperators.Multiset.Basic
 variable {α : Type*}
 
 namespace Multiset
+section CommMonoid
+variable [CommMonoid α] {s : Multiset α} {a : α}
 
-theorem dvd_prod [CommMonoid α] {s : Multiset α} {a : α} : a ∈ s → a ∣ s.prod :=
+lemma dvd_prod : a ∈ s → a ∣ s.prod :=
   Quotient.inductionOn s (fun l a h => by simpa using List.dvd_prod h) a
 #align multiset.dvd_prod Multiset.dvd_prod
 
+@[simp] lemma prod_map_neg [HasDistribNeg α] (s : Multiset α) :
+    (s.map Neg.neg).prod = (-1) ^ card s * s.prod := Quotient.inductionOn s (by simp)
+#align multiset.prod_map_neg Multiset.prod_map_neg
+
+end CommMonoid
+
+section CommMonoidWithZero
+variable [CommMonoidWithZero α] {s : Multiset α}
+
+lemma prod_eq_zero (h : (0 : α) ∈ s) : s.prod = 0 := by
+  rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩; simp [hs', Multiset.prod_cons]
+#align multiset.prod_eq_zero Multiset.prod_eq_zero
+
+variable [NoZeroDivisors α] [Nontrivial α] {s : Multiset α}
+
+@[simp] lemma prod_eq_zero_iff : s.prod = 0 ↔ (0 : α) ∈ s :=
+  Quotient.inductionOn s fun l ↦ by rw [quot_mk_to_coe, prod_coe]; exact List.prod_eq_zero_iff
+#align multiset.prod_eq_zero_iff Multiset.prod_eq_zero_iff
+
+lemma prod_ne_zero (h : (0 : α) ∉ s) : s.prod ≠ 0 := mt prod_eq_zero_iff.1 h
+#align multiset.prod_ne_zero Multiset.prod_ne_zero
+
+end CommMonoidWithZero
+
 @[to_additive]
 theorem prod_eq_one_iff [CanonicallyOrderedCommMonoid α] {m : Multiset α} :
     m.prod = 1 ↔ ∀ x ∈ m, x = (1 : α) :=
   Quotient.inductionOn m fun l => by simpa using List.prod_eq_one_iff l
 #align multiset.prod_eq_one_iff Multiset.prod_eq_one_iff
 #align multiset.sum_eq_zero_iff Multiset.sum_eq_zero_iff
 
+section NonUnitalSemiring
+variable [NonUnitalSemiring α] {s : Multiset α} {a : α}
+
+lemma dvd_sum : (∀ x ∈ s, a ∣ x) → a ∣ s.sum :=
+  Multiset.induction_on s (fun _ ↦ dvd_zero _) fun x s ih h ↦ by
+    rw [sum_cons]
+    exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)
+#align multiset.dvd_sum Multiset.dvd_sum
+
+end NonUnitalSemiring
 end Multiset
 
 @[simp]