feat: Multiset.sum_lt_sum et al (#8707)

Lean discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Multiset.2Esum_lt_sum
leanprover-community · Nov 29, 2023 · f961562 · f961562
1 parent e761b4e
commit f961562
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 13 deletions.
diff --git a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
@@ -427,6 +427,25 @@ theorem pow_card_le_prod (h : ∀ x ∈ s, a ≤ x) : a ^ card s ≤ s.prod := b
 
 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.coe_map, Multiset.coe_prod]
+  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

diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean
@@ -442,23 +442,16 @@ section OrderedCancelCommMonoid
 variable [OrderedCancelCommMonoid M] {f g : ι → M} {s t : Finset ι}
 
 @[to_additive sum_lt_sum]
-theorem prod_lt_prod' (Hle : ∀ i ∈ s, f i ≤ g i) (Hlt : ∃ i ∈ s, f i < g i) :
-    ∏ i in s, f i < ∏ i in s, g i := by
-  classical
-    rcases Hlt with ⟨i, hi, hlt⟩
-    rw [← insert_erase hi, prod_insert (not_mem_erase _ _), prod_insert (not_mem_erase _ _)]
-    exact mul_lt_mul_of_lt_of_le hlt (prod_le_prod' fun j hj ↦ Hle j <| mem_of_mem_erase hj)
+theorem prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
+    ∏ i in s, f i < ∏ i in s, g i :=
+  Multiset.prod_lt_prod' hle hlt
 #align finset.prod_lt_prod' Finset.prod_lt_prod'
 #align finset.sum_lt_sum Finset.sum_lt_sum
 
 @[to_additive sum_lt_sum_of_nonempty]
-theorem prod_lt_prod_of_nonempty' (hs : s.Nonempty) (Hlt : ∀ i ∈ s, f i < g i) :
-    ∏ i in s, f i < ∏ i in s, g i := by
-  apply prod_lt_prod'
-  · intro i hi
-    apply le_of_lt (Hlt i hi)
-  cases' hs with i hi
-  exact ⟨i, hi, Hlt i hi⟩
+theorem prod_lt_prod_of_nonempty' (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) :
+    ∏ i in s, f i < ∏ i in s, g i :=
+  Multiset.prod_lt_prod_of_nonempty' (by aesop) hlt
 #align finset.prod_lt_prod_of_nonempty' Finset.prod_lt_prod_of_nonempty'
 #align finset.sum_lt_sum_of_nonempty Finset.sum_lt_sum_of_nonempty