chore(Algebra/Order/BigOperators): follow the ₀ naming convention

We have long agreed that `MonoidWithZero` lemmas corresponding to `Monoid` lemmas should be suffixed with `₀`, while currently it is the `Monoid` lemmas that are primed.

Author: YaelDillies

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -596,36 +596,36 @@ alias finsum_pos' := finsum_pos
 @[to_additive existing finsum_pos', deprecated (since := "2026-01-03")]
 alias one_lt_finprod' := one_lt_finprod
 
-/-- Monotonicity of `finprod`. See `finprod_le_finprod` for a variant where
+/-- Monotonicity of `finprod`. See `finprod_le_finprod₀` for a variant where
 `M` is a `CommMonoidWithZero`. -/
 @[to_additive /-- Monotonicity of `finsum.` -/]
-lemma finprod_le_finprod' [PartialOrder M] [MulLeftMono M] (hf : HasFiniteMulSupport f)
+lemma finprod_le_finprod [PartialOrder M] [MulLeftMono M] (hf : HasFiniteMulSupport f)
     (hg : HasFiniteMulSupport g) (h : f ≤ g) :
     ∏ᶠ a, f a ≤ ∏ᶠ a, g a := by
   have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype
   let s := (f.mulSupport ∪ g.mulSupport).toFinset
   rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
     finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]
-  exact Finset.prod_le_prod' fun i _ ↦ h i
+  exact Finset.prod_le_prod fun i _ ↦ h i
 
-/-- Monotonicity of `finprod`. See `finprod_le_finprod'` for a variant where
+/-- Monotonicity of `finprod`. See `finprod_le_finprod` for a variant where
 `M` is an ordered `CommMonoid`. -/
-lemma finprod_le_finprod {M : Type*} [CommMonoidWithZero M] [PartialOrder M] [ZeroLEOneClass M]
+lemma finprod_le_finprod₀ {M : Type*} [CommMonoidWithZero M] [PartialOrder M] [ZeroLEOneClass M]
     [PosMulMono M] {f g : α → M} (hf : HasFiniteMulSupport f) (hf₀ : ∀ a, 0 ≤ f a)
     (hg : HasFiniteMulSupport g) (h : f ≤ g) :
     ∏ᶠ a, f a ≤ ∏ᶠ a, g a := by
   have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype
   let s := (f.mulSupport ∪ g.mulSupport).toFinset
   rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
     finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]
-  exact Finset.prod_le_prod (fun i _ ↦ hf₀ i) fun i _ ↦ h i
+  exact Finset.prod_le_prod₀ (fun i _ ↦ hf₀ i) fun i _ ↦ h i
 
 lemma finprod_zero_le_one {M α : Type*} [CommMonoidWithZero M] [PartialOrder M]
     [ZeroLEOneClass M] [PosMulMono M] :
     ∏ᶠ _ : α, (0 : M) ≤ 1 := by
   rw [← finprod_one (α := α)]
   by_cases H : (fun _ : α ↦ (0 : M)).HasFiniteMulSupport
-  · exact finprod_le_finprod H (fun _ ↦ le_rfl) (by fun_prop) fun _ ↦ zero_le_one
+  · exact finprod_le_finprod₀ H (fun _ ↦ le_rfl) (by fun_prop) fun _ ↦ zero_le_one
   · rw [finprod_of_not_hasFiniteMulSupport H]
     exact finprod_one.symm.le
 
@@ -1133,7 +1133,7 @@ theorem single_le_finprod {M : Type*} [CommMonoid M] [Preorder M] [IsOrderedMono
     (hf : HasFiniteMulSupport f) (h : ∀ j, 1 ≤ f j) : f i ≤ ∏ᶠ j, f j := by
   classical calc
       f i ≤ ∏ j ∈ insert i hf.toFinset, f j :=
-        Finset.single_le_prod' (fun j _ => h j) (Finset.mem_insert_self _ _)
+        Finset.single_le_prod (fun j _ => h j) (Finset.mem_insert_self _ _)
       _ = ∏ᶠ j, f j :=
         (finprod_eq_prod_of_mulSupport_toFinset_subset _ hf (Finset.subset_insert _ _)).symm
 

Mathlib/Algebra/Group/Submonoid/Pointwise.lean

@@ -296,6 +296,6 @@ theorem submonoid_closure (hpos : ∀ x : α, x ∈ s → 1 ≤ x) (h : s.IsPWO)
     IsPWO (Submonoid.closure s : Set α) := by
   rw [Submonoid.closure_eq_image_prod]
   refine (h.partiallyWellOrderedOn_sublistForall₂ (· ≤ ·)).image_of_monotone_on ?_
-  exact fun l1 _ l2 hl2 h12 => h12.prod_le_prod' fun x hx => hpos x <| hl2 x hx
+  exact fun l1 _ l2 hl2 h12 => h12.prod_le_prod fun x hx => hpos x <| hl2 x hx
 
 end Set.IsPWO

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -24,8 +24,8 @@ namespace List
 section Monoid
 variable [Monoid M]
 
-@[to_additive sum_le_sum]
-lemma Forall₂.prod_le_prod' [Preorder M] [MulRightMono M]
+@[to_additive]
+lemma Forall₂.prod_le_prod [Preorder M] [MulRightMono M]
     [MulLeftMono M] {l₁ l₂ : List M} (h : Forall₂ (· ≤ ·) l₁ l₂) :
     l₁.prod ≤ l₂.prod := by
   induction h with
@@ -35,38 +35,38 @@ lemma Forall₂.prod_le_prod' [Preorder M] [MulRightMono M]
 /-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are greater than or equal to one, then
 `l₁.prod ≤ l₂.prod`. One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 1 ≤ a` instead
 of `∀ a ∈ l₂, 1 ≤ a` but this lemma is not yet in `mathlib`. -/
-@[to_additive sum_le_sum /-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are nonnegative,
+@[to_additive /-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are nonnegative,
   then `l₁.sum ≤ l₂.sum`.
   One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 0 ≤ a` instead of `∀ a ∈ l₂, 0 ≤ a`
   but this lemma is not yet in `mathlib`. -/]
-lemma Sublist.prod_le_prod' [Preorder M] [MulRightMono M]
+lemma Sublist.prod_le_prod [Preorder M] [MulRightMono M]
     [MulLeftMono M] {l₁ l₂ : List M} (h : l₁ <+ l₂)
     (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) : l₁.prod ≤ l₂.prod := by
   induction h with
   | slnil => rfl
-  | cons a _ ih' =>
+  | cons a _ ih =>
     simp only [prod_cons, forall_mem_cons] at h₁ ⊢
-    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
-  | cons_cons a _ ih' =>
+    exact (ih h₁.2).trans (le_mul_of_one_le_left' h₁.1)
+  | cons_cons a _ ih =>
     simp only [prod_cons, forall_mem_cons] at h₁ ⊢
-    grw [ih' h₁.2]
+    grw [ih h₁.2]
 
-@[to_additive sum_le_sum]
-lemma SublistForall₂.prod_le_prod' [Preorder M]
+@[to_additive]
+lemma SublistForall₂.prod_le_prod [Preorder M]
     [MulRightMono M] [MulLeftMono M]
     {l₁ l₂ : List M} (h : SublistForall₂ (· ≤ ·) l₁ l₂) (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) :
     l₁.prod ≤ l₂.prod :=
   let ⟨_, hall, hsub⟩ := sublistForall₂_iff.1 h
-  hall.prod_le_prod'.trans <| hsub.prod_le_prod' h₁
+  hall.prod_le_prod.trans <| hsub.prod_le_prod h₁
 
-@[to_additive sum_le_sum]
-lemma prod_le_prod' [Preorder M] [MulRightMono M]
+@[to_additive]
+lemma prod_le_prod [Preorder M] [MulRightMono M]
     [MulLeftMono M] {l : List ι} {f g : ι → M} (h : ∀ i ∈ l, f i ≤ g i) :
     (l.map f).prod ≤ (l.map g).prod :=
-  Forall₂.prod_le_prod' <| by simpa
+  Forall₂.prod_le_prod <| by simpa
 
-@[to_additive sum_lt_sum]
-lemma prod_lt_prod' [Preorder M] [MulLeftStrictMono M]
+@[to_additive]
+lemma prod_lt_prod [Preorder M] [MulLeftStrictMono M]
     [MulLeftMono M] [MulRightStrictMono M]
     [MulRightMono M] {l : List ι} (f g : ι → M)
     (h₁ : ∀ i ∈ l, f i ≤ g i) (h₂ : ∃ i ∈ l, f i < g i) : (l.map f).prod < (l.map g).prod := by
@@ -76,38 +76,38 @@ lemma prod_lt_prod' [Preorder M] [MulLeftStrictMono M]
     simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
     simp only [mem_cons, exists_eq_or_imp] at h₂
     cases h₂
-    · exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
+    · exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod h₁.2)
     · exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›
 
 @[to_additive]
 lemma prod_lt_prod_of_ne_nil [Preorder M] [MulLeftStrictMono M]
     [MulLeftMono M] [MulRightStrictMono M]
     [MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M)
     (hlt : ∀ i ∈ l, f i < g i) : (l.map f).prod < (l.map g).prod :=
-  (prod_lt_prod' f g fun i hi => (hlt i hi).le) <|
+  (prod_lt_prod f g fun i hi => (hlt i hi).le) <|
     (exists_mem_of_ne_nil l hl).imp fun i hi => ⟨hi, hlt i hi⟩
 
 @[to_additive sum_le_card_nsmul]
 lemma prod_le_pow_card [Preorder M] [MulRightMono M]
     [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) :
     l.prod ≤ n ^ l.length := by
-  simpa only [map_id', map_const', prod_replicate] using prod_le_prod' h
+  simpa only [map_id', map_const', prod_replicate] using prod_le_prod h
 
 @[to_additive card_nsmul_le_sum]
 lemma pow_card_le_prod [Preorder M] [MulRightMono M]
     [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, n ≤ x) :
     n ^ l.length ≤ l.prod :=
   @prod_le_pow_card Mᵒᵈ _ _ _ _ l n h
 
-@[to_additive exists_lt_of_sum_lt]
-lemma exists_lt_of_prod_lt' [LinearOrder M] [MulRightMono M]
+@[to_additive]
+lemma exists_lt_of_prod_lt [LinearOrder M] [MulRightMono M]
     [MulLeftMono M] {l : List ι} (f g : ι → M)
     (h : (l.map f).prod < (l.map g).prod) : ∃ i ∈ l, f i < g i := by
   contrapose! h
-  exact prod_le_prod' h
+  exact prod_le_prod h
 
-@[to_additive exists_le_of_sum_le]
-lemma exists_le_of_prod_le' [LinearOrder M] [MulLeftStrictMono M]
+@[to_additive]
+lemma exists_le_of_prod_le [LinearOrder M] [MulLeftStrictMono M]
     [MulLeftMono M] [MulRightStrictMono M]
     [MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M)
     (h : (l.map f).prod ≤ (l.map g).prod) : ∃ x ∈ l, f x ≤ g x := by
@@ -130,7 +130,7 @@ lemma max_prod_le (l : List α) (f g : α → M) [LinearOrder M]
     [MulLeftMono M] [MulRightMono M] :
     max (l.map f).prod (l.map g).prod ≤ (l.map fun i ↦ max (f i) (g i)).prod := by
   rw [max_le_iff]
-  constructor <;> apply List.prod_le_prod' <;> intros
+  constructor <;> apply List.prod_le_prod <;> intros
   · apply le_max_left
   · apply le_max_right
 
@@ -139,7 +139,7 @@ lemma prod_min_le [LinearOrder M] [MulLeftMono M]
     [MulRightMono M] (l : List α) (f g : α → M) :
     (l.map fun i ↦ min (f i) (g i)).prod ≤ min (l.map f).prod (l.map g).prod := by
   rw [le_min_iff]
-  constructor <;> apply List.prod_le_prod' <;> intros
+  constructor <;> apply List.prod_le_prod <;> intros
   · apply min_le_left
   · apply min_le_right
 

Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -118,18 +118,18 @@ section OrderedCancelCommMonoid
 variable [CommMonoid α] [Preorder α] [IsOrderedCancelMonoid α] [MulLeftStrictMono α]
   {s : Multiset ι} {f g : ι → α}
 
-@[to_additive sum_lt_sum]
-lemma prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
+@[to_additive]
+lemma 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
+  exact List.prod_lt_prod f g hle hlt
 
-@[to_additive sum_lt_sum_of_nonempty]
-lemma prod_lt_prod_of_nonempty' (hs : s ≠ ∅) (hfg : ∀ i ∈ s, f i < g i) :
+@[to_additive]
+lemma 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⟩
+  exact prod_lt_prod (fun i hi => le_of_lt (hfg i hi)) ⟨i, hi, hfg i hi⟩
 
 end OrderedCancelCommMonoid
 

Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

@@ -32,10 +32,10 @@ lemma prod_nonneg (h0 : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ ∏ i ∈ s, f i :=
   prod_induction f (fun i ↦ 0 ≤ i) (fun _ _ ha hb ↦ mul_nonneg ha hb) zero_le_one h0
 
 /-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
-product of `f i` is less than or equal to the product of `g i`. See also `Finset.prod_le_prod'` for
+product of `f i` is less than or equal to the product of `g i`. See also `Finset.prod_le_prod` for
 the case of an ordered commutative multiplicative monoid. -/
 @[gcongr]
-lemma prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
+lemma prod_le_prod₀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i) :
     ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i := by
   induction s using Finset.cons_induction with
   | empty => simp
@@ -46,14 +46,14 @@ lemma prod_le_prod (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i)
     exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]
 
 /-- If each `f i`, `i ∈ s` belongs to `[0, 1]`, then their product is less than or equal to one.
-See also `Finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid. -/
-lemma prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 := by
-  convert! ← prod_le_prod h0 h1
+See also `Finset.prod_le_one` for the case of an ordered commutative multiplicative monoid. -/
+lemma prod_le_one₀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 := by
+  convert ← prod_le_prod₀ h0 h1
   exact Finset.prod_const_one
 
-/-- A version of `Finset.one_le_prod'` for `PosMulMono` in place of `MulLeftMono`. -/
-lemma one_le_prod (hf : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i := by
-  simpa using prod_le_prod (by simp) hf
+/-- A version of `Finset.one_le_prod` for `PosMulMono` in place of `MulLeftMono`. -/
+lemma one_le_prod₀ (hf : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i := by
+  simpa using prod_le_prod₀ (by simp) hf
 
 lemma le_prod_max_one {M : Type*} [CommMonoidWithZero M] [LinearOrder M] [ZeroLEOneClass M]
     [PosMulMono M] {i : ι} (hi : i ∈ s) (f : ι → M) :
@@ -64,21 +64,21 @@ lemma le_prod_max_one {M : Type*} [CommMonoidWithZero M] [LinearOrder M] [ZeroLE
   have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
     rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
     simp
-  exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind
+  exact this ▸ prod_le_prod₀ (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind
 
 @[gcongr]
-theorem prod_le_prod_of_subset_of_one_le (h : s ⊆ t)
+theorem prod_le_prod_of_subset_of_one_le₀ (h : s ⊆ t)
     (hf0 : ∀ i ∈ s, 0 ≤ f i)
     (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
   have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
   classical
   calc
       ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
-        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
+      le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod₀ <| by simpa only [mem_sdiff, and_imp]
       _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
       _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
 
-theorem prod_le_prod_of_subset_of_le_one (h : s ⊆ t) (hf0 : ∀ i ∈ t, 0 ≤ f i)
+theorem prod_le_prod_of_subset_of_le_one₀ (h : s ⊆ t) (hf0 : ∀ i ∈ t, 0 ≤ f i)
     (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
     ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i := by
   have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
@@ -87,16 +87,16 @@ theorem prod_le_prod_of_subset_of_le_one (h : s ⊆ t) (hf0 : ∀ i ∈ t, 0 ≤
     ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
     _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
     _ ≤ ∏ i ∈ s, f i :=
-      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))
+      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one₀ (by grind) (by grind))
 
-theorem prod_mono_set_of_one_le (hf : ∀ x, 1 ≤ f x) :
+theorem prod_mono_set_of_one_le₀ (hf : ∀ x, 1 ≤ f x) :
     Monotone fun s ↦ ∏ x ∈ s, f x :=
-  fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le hst
+  fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le₀ hst
     (fun i _ ↦ zero_le_one.trans (hf i)) (fun x _ _ ↦ hf x)
 
-theorem prod_anti_set_of_le_one (hf0 : ∀ (x : ι), 0 ≤ f x) (hf : ∀ (x : ι), f x ≤ 1) :
+theorem prod_anti_set_of_le_one₀ (hf0 : ∀ (x : ι), 0 ≤ f x) (hf : ∀ (x : ι), f x ≤ 1) :
     Antitone fun (s : Finset ι) => ∏ x ∈ s, f x :=
-  fun _ _ hst ↦ prod_le_prod_of_subset_of_le_one hst (by grind) (by simp [hf])
+  fun _ _ hst ↦ prod_le_prod_of_subset_of_le_one₀ hst (by grind) (by simp [hf])
 
 end PosMulMono
 
@@ -107,23 +107,23 @@ variable [PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R] [Nontrivial R]
 lemma prod_pos (h0 : ∀ i ∈ s, 0 < f i) : 0 < ∏ i ∈ s, f i :=
   prod_induction f (fun x ↦ 0 < x) (fun _ _ ha hb ↦ mul_pos ha hb) zero_lt_one h0
 
-lemma prod_lt_prod (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i ≤ g i)
+lemma prod_lt_prod₀ (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i ≤ g i)
     (hlt : ∃ i ∈ s, f i < g i) :
     ∏ i ∈ s, f i < ∏ i ∈ s, g i := by
   classical
   obtain ⟨i, hi, hilt⟩ := hlt
   rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]
   have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
   refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
-  · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
+  · exact prod_le_prod₀ (fun j hj => (hf j (mem_of_mem_erase hj)).le)
       (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
   · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
   · exact (hf i hi).le.trans hilt.le
 
-lemma prod_lt_prod_of_nonempty (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i < g i)
+lemma prod_lt_prod_of_nonempty₀ (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i < g i)
     (h_ne : s.Nonempty) :
     ∏ i ∈ s, f i < ∏ i ∈ s, g i := by
-  apply prod_lt_prod hf fun i hi => le_of_lt (hfg i hi)
+  apply prod_lt_prod₀ hf fun i hi => le_of_lt (hfg i hi)
   obtain ⟨i, hi⟩ := h_ne
   exact ⟨i, hi, hfg i hi⟩
 

Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean

@@ -467,7 +467,7 @@ theorem comp_summable_nnreal (q : FormalMultilinearSeries 𝕜 F G) (p : FormalM
     have B := calc
       (∏ i, ‖p (c.blocksFun i)‖₊) * rp ^ n = ∏ i, ‖p (c.blocksFun i)‖₊ * rp ^ c.blocksFun i := by
         simp only [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum, c.sum_blocksFun]
-      _ ≤ ∏ _i : Fin c.length, Cp := Finset.prod_le_prod' fun i _ => hCp _
+      _ ≤ ∏ _i : Fin c.length, Cp := by gcongr with i; exact hCp _
       _ = Cp ^ c.length := by simp
       _ ≤ Cp ^ n := pow_right_mono₀ hCp1 c.length_le
     calc

Mathlib/Analysis/Analytic/Composition.lean

@@ -150,7 +150,7 @@ theorem Asymptotics.IsLittleO.sum_range {α : Type*} [NormedAddCommGroup α] {f
     (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, g i := by
   have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)
   have B : ∀ n, ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i := fun n => by
-    rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
+    rw [Real.norm_eq_abs, abs_sum_of_nonneg]; exact fun _ _ ↦ hg _
   apply isLittleO_iff.2 fun ε εpos => _
   intro ε εpos
   obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b : ℕ, N ≤ b → ‖f b‖ ≤ ε / 2 * g b := by

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

@@ -227,7 +227,7 @@ theorem hasIntegral_GP_pderiv (f : (Fin (n + 1) → ℝ) → E)
         (Hmaps _ Hl hy)) volume).trans ?_
       refine (mul_le_mul_of_nonneg_right ?_ (half_pos ε0).le).trans_eq (one_mul _)
       rw [Box.coe_eq_pi, measureReal_def, Real.volume_pi_Ioc_toReal (Box.lower_le_upper _)]
-      refine prod_le_one (fun _ _ => sub_nonneg.2 <| Box.lower_le_upper _ _) fun j _ => ?_
+      refine prod_le_one₀ (fun _ _ => sub_nonneg.2 <| Box.lower_le_upper _ _) fun j _ => ?_
       calc
         J.upper (i.succAbove j) - J.lower (i.succAbove j) ≤
             dist (J.upper (i.succAbove j)) (J.lower (i.succAbove j)) :=

Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

@@ -671,7 +671,7 @@ lemma le_inv_mul_exp (x : ℝ) {c : ℝ} (hc : 0 < c) : x ≤ c⁻¹ * exp (c *
 
 theorem prod_one_add_le_exp_sum {ι : Type*} (s : Finset ι) {f : ι → ℝ}
     (hf : ∀ i, 0 ≤ f i) : ∏ i ∈ s, (1 + f i) ≤ exp (∑ i ∈ s, f i) :=
-  (Finset.prod_le_prod (fun i _ ↦ add_nonneg zero_le_one (hf i))
+  (Finset.prod_le_prod₀ (fun i _ ↦ add_nonneg zero_le_one (hf i))
     fun i _ ↦ (add_comm 1 (f i)).le.trans (add_one_le_exp _)).trans
     (exp_sum s f).symm.le