fix(src/algebra/big_operators/multiset): unify prod_le_pow_card and prod_le_of_forall_le (#12589)

using the name `prod_le_pow_card` as per https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/duplicate.20lemmas
but use the phrasing of prod_le_of_forall_le with non-implicit
`multiset`, as that is how it is used.

Author: nomeata

src/algebra/big_operators/multiset.lean

@@ -267,11 +267,11 @@ quotient.induction_on s $ λ l hl, by simpa using list.one_le_prod_of_one_le hl
 lemma single_le_prod : (∀ x ∈ s, (1 : α) ≤ x) → ∀ x ∈ s, x ≤ s.prod :=
 quotient.induction_on s $ λ l hl x hx, by simpa using list.single_le_prod hl x hx
 
-@[to_additive]
-lemma prod_le_of_forall_le (s : multiset α) (n : α) (h : ∀ x ∈ s, x ≤ n) : s.prod ≤ n ^ s.card :=
+@[to_additive sum_le_card_nsmul]
+lemma prod_le_pow_card (s : multiset α) (n : α) (h : ∀ x ∈ s, x ≤ n) : s.prod ≤ n ^ s.card :=
 begin
   induction s using quotient.induction_on,
-  simpa using list.prod_le_of_forall_le _ _ h,
+  simpa using list.prod_le_pow_card _ _ h,
 end
 
 @[to_additive all_zero_of_le_zero_le_of_sum_eq_zero]
@@ -304,10 +304,6 @@ lemma prod_le_sum_prod (f : α → α) (h : ∀ x, x ∈ s → x ≤ f x) : s.pr
 lemma pow_card_le_prod (h : ∀ x ∈ s, a ≤ x) : a ^ s.card ≤ s.prod :=
 by { rw [←multiset.prod_repeat, ←multiset.map_const], exact prod_map_le_prod _ h }
 
-@[to_additive sum_le_card_nsmul]
-lemma prod_le_pow_card (h : ∀ x ∈ s, x ≤ a) : s.prod ≤ a ^ s.card :=
-@pow_card_le_prod (order_dual α) _ _ _ h
-
 end ordered_comm_monoid
 
 lemma prod_nonneg [ordered_comm_semiring α] {m : multiset α} (h : ∀ a ∈ m, (0 : α) ≤ a) :

src/algebra/big_operators/order.lean

@@ -169,24 +169,24 @@ calc f a = ∏ i in {a}, f i : prod_singleton.symm
      ... ≤ ∏ i in s, f i   :
   prod_le_prod_of_subset_of_one_le' (singleton_subset_iff.2 h) $ λ i hi _, hf i hi
 
-@[to_additive]
-lemma prod_le_of_forall_le (s : finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) :
+@[to_additive sum_le_card_nsmul]
+lemma prod_le_pow_card (s : finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) :
   s.prod f ≤ n ^ s.card :=
 begin
-  refine (multiset.prod_le_of_forall_le (s.val.map f) n _).trans _,
+  refine (multiset.prod_le_pow_card (s.val.map f) n _).trans _,
   { simpa using h },
   { simpa }
 end
 
-@[to_additive]
-lemma le_prod_of_forall_le (s : finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) :
+@[to_additive card_nsmul_le_sum]
+lemma pow_card_le_prod (s : finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) :
   n ^ s.card ≤ s.prod f :=
-@finset.prod_le_of_forall_le _ (order_dual N) _ _ _ _ h
+@finset.prod_le_pow_card _ (order_dual N) _ _ _ _ h
 
 lemma card_bUnion_le_card_mul [decidable_eq β] (s : finset ι) (f : ι → finset β) (n : ℕ)
   (h : ∀ a ∈ s, (f a).card ≤ n) :
   (s.bUnion f).card ≤ s.card * n :=
-card_bUnion_le.trans $ sum_le_of_forall_le _ _ _ h
+card_bUnion_le.trans $ sum_le_card_nsmul _ _ _ h
 
 variables {ι' : Type*} [decidable_eq ι']
 
@@ -264,7 +264,7 @@ times how many they are. -/
 lemma sum_card_inter_le (h : ∀ a ∈ s, (B.filter $ (∈) a).card ≤ n) :
   ∑ t in B, (s ∩ t).card ≤ s.card * n :=
 begin
-  refine le_trans _ (s.sum_le_of_forall_le _ _ h),
+  refine le_trans _ (s.sum_le_card_nsmul _ _ h),
   simp_rw [←filter_mem_eq_inter, card_eq_sum_ones, sum_filter],
   exact sum_comm.le,
 end
@@ -281,7 +281,7 @@ times how many they are. -/
 lemma le_sum_card_inter (h : ∀ a ∈ s, n ≤ (B.filter $ (∈) a).card) :
   s.card * n ≤ ∑ t in B, (s ∩ t).card :=
 begin
-  apply (s.le_sum_of_forall_le _ _ h).trans,
+  apply (s.card_nsmul_le_sum _ _ h).trans,
   simp_rw [←filter_mem_eq_inter, card_eq_sum_ones, sum_filter],
   exact sum_comm.le,
 end

src/algebra/polynomial/big_operators.lean

@@ -96,7 +96,7 @@ begin
     have h : nat_degree tl.prod ≤ n * tl.length,
     { refine (nat_degree_list_prod_le _).trans _,
       rw [←tl.length_map nat_degree, mul_comm],
-      refine list.sum_le_of_forall_le _ _ _,
+      refine list.sum_le_card_nsmul _ _ _,
       simpa using hl' },
     have hdn : nat_degree hd ≤ n := hl _ (list.mem_cons_self _ _),
     rcases hdn.eq_or_lt with rfl|hdn',

src/combinatorics/double_counting.lean

@@ -61,10 +61,10 @@ lemma card_mul_le_card_mul [Π a b, decidable (r a b)]
   (hn : ∀ b ∈ t, (s.bipartite_below r b).card ≤ n) :
   s.card * m ≤ t.card * n :=
 calc
-    _ ≤ ∑ a in s, (t.bipartite_above r a).card : s.le_sum_of_forall_le _ _ hm
+    _ ≤ ∑ a in s, (t.bipartite_above r a).card : s.card_nsmul_le_sum _ _ hm
   ... = ∑ b in t, (s.bipartite_below r b).card
       : sum_card_bipartite_above_eq_sum_card_bipartite_below _
-  ... ≤ _ : t.sum_le_of_forall_le _ _ hn
+  ... ≤ _ : t.sum_le_card_nsmul _ _ hn
 
 lemma card_mul_le_card_mul' [Π a b, decidable (r a b)]
   (hn : ∀ b ∈ t, n ≤ (s.bipartite_below r b).card)

src/data/list/prod_monoid.lean

@@ -35,8 +35,8 @@ begin
   exact list.eq_repeat.mpr ⟨rfl, h⟩,
 end
 
-@[to_additive]
-lemma prod_le_of_forall_le [ordered_comm_monoid α] (l : list α) (n : α) (h : ∀ (x ∈ l), x ≤ n) :
+@[to_additive sum_le_card_nsmul]
+lemma prod_le_pow_card [ordered_comm_monoid α] (l : list α) (n : α) (h : ∀ (x ∈ l), x ≤ n) :
   l.prod ≤ n ^ l.length :=
 begin
   induction l with y l IH,

src/linear_algebra/matrix/polynomial.lean

@@ -49,7 +49,7 @@ begin
         { rw [sg, units.neg_smul, one_smul, nat_degree_neg] } }
   ... ≤ ∑ (i : n), nat_degree (((X : α[X]) • A.map C + B.map C) (g i) i) :
     nat_degree_prod_le (finset.univ : finset n) (λ (i : n), (X • A.map C + B.map C) (g i) i)
-  ... ≤ finset.univ.card • 1 : finset.sum_le_of_forall_le _ _ 1 (λ (i : n) _, _)
+  ... ≤ finset.univ.card • 1 : finset.sum_le_card_nsmul _ _ 1 (λ (i : n) _, _)
   ... ≤ fintype.card n : by simpa,
   calc  nat_degree (((X : α[X]) • A.map C + B.map C) (g i) i)
       = nat_degree ((X : α[X]) * C (A (g i) i) + C (B (g i) i)) : by simp