diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
index 803c32af269d78..aabccdb4dc8364 100644
--- a/Mathlib/Algebra/BigOperators/Finprod.lean
+++ b/Mathlib/Algebra/BigOperators/Finprod.lean
@@ -604,21 +604,23 @@ 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
+
+@[deprecated (since := "2026-05-22")] alias finprod_le_finprod' := finprod_le_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 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
@@ -626,14 +628,14 @@ lemma finprod_le_finprod {M : Type*} [CommMonoidWithZero M] [PartialOrder M] [Ze
   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
 
@@ -1154,7 +1156,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
 
diff --git a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean b/Mathlib/Algebra/Group/Submonoid/Pointwise.lean
index f3c3a07ab3a768..b2652071c9106a 100644
--- a/Mathlib/Algebra/Group/Submonoid/Pointwise.lean
+++ b/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
diff --git a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
index cf94a12bd7304e..c33247383124a3 100644
--- a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@@ -105,10 +105,12 @@ variable {f g : ι → N} {s t : Finset ι}
 /-- In an ordered commutative monoid, if each factor `f i` of one finite product is less than or
 equal to the corresponding factor `g i` of another finite product, then
 `∏ i ∈ s, f i ≤ ∏ i ∈ s, g i`. -/
-@[to_additive (attr := gcongr) sum_le_sum]
-theorem prod_le_prod' [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i :=
+@[to_additive (attr := gcongr)]
+theorem prod_le_prod [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ g i) : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i :=
   Multiset.prod_map_le_prod_map f g h
 
+@[deprecated (since := "2026-05-22")] alias prod_le_prod' := prod_le_prod
+
 attribute [bound] sum_le_sum
 
 /-- In an ordered additive commutative monoid, if each summand `f i` of one finite sum is less than
@@ -117,52 +119,68 @@ or equal to the corresponding summand `g i` of another finite sum, then
 add_decl_doc sum_le_sum
 
 @[to_additive sum_nonneg]
-theorem one_le_prod' [MulLeftMono N] (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
-  le_trans (by rw [prod_const_one]) (prod_le_prod' h)
+theorem one_le_prod [MulLeftMono N] (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
+  le_trans (by rw [prod_const_one]) (prod_le_prod h)
+
+@[deprecated (since := "2026-05-22")] alias one_le_prod' := one_le_prod
 
-@[to_additive Finset.sum_nonneg']
+@[to_additive sum_nonneg']
 theorem one_le_prod'' [MulLeftMono N] (h : ∀ i : ι, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i :=
-  Finset.one_le_prod' fun i _ ↦ h i
+  Finset.one_le_prod fun i _ ↦ h i
+
+attribute [deprecated sum_nonneg (since := "2026-05-22")] sum_nonneg'
+attribute [deprecated one_le_prod (since := "2026-05-22")] one_le_prod''
 
-@[to_additive sum_nonpos]
-theorem prod_le_one' [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 :=
-  (prod_le_prod' h).trans_eq (by rw [prod_const_one])
+@[to_additive]
+theorem prod_le_one [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1 :=
+  (prod_le_prod h).trans_eq (by rw [prod_const_one])
+
+@[deprecated (since := "2026-05-22")] alias prod_le_one' := prod_le_one
 
-@[to_additive (attr := gcongr) sum_le_sum_of_subset_of_nonneg]
-theorem prod_le_prod_of_subset_of_one_le' [MulLeftMono N] (h : s ⊆ t)
+@[to_additive (attr := gcongr)]
+theorem prod_le_prod_of_subset_of_one_le [MulLeftMono N] (h : s ⊆ t)
     (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) : ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
   classical calc
       ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
-        le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
+        le_mul_of_one_le_left' <| 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]
 
+@[deprecated (since := "2026-05-22")]
+alias prod_le_prod_of_subset_of_one_le' := prod_le_prod_of_subset_of_one_le
+
 @[to_additive]
-theorem prod_le_prod_of_subset_of_le_one'
-    {ι : Type u_1} {N : Type u_5} [CommMonoid N] [Preorder N]
-    {f : ι → N} {s t : Finset ι} [MulLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
+lemma prod_le_prod_of_subset_of_le_one [MulLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → f i ≤ 1) :
     ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i :=
-  prod_le_prod_of_subset_of_one_le' (N := Nᵒᵈ) h hf
+  prod_le_prod_of_subset_of_one_le (N := Nᵒᵈ) h hf
 
-@[to_additive sum_mono_set_of_nonneg]
-theorem prod_mono_set_of_one_le' [MulLeftMono N] (hf : ∀ x, 1 ≤ f x) :
+@[deprecated (since := "2026-05-22")]
+alias prod_le_prod_of_subset_of_le_one' := prod_le_prod_of_subset_of_le_one
+
+@[to_additive]
+theorem prod_mono_set_of_one_le [MulLeftMono N] (hf : ∀ x, 1 ≤ f x) :
     Monotone fun s ↦ ∏ x ∈ s, f x :=
-  fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le' hst fun x _ _ ↦ hf x
+  fun _ _ hst ↦ prod_le_prod_of_subset_of_one_le hst fun x _ _ ↦ hf x
+
+@[deprecated (since := "2026-05-22")] alias prod_mono_set_of_one_le' := prod_mono_set_of_one_le
 
 @[to_additive]
-theorem prod_anti_set_of_le_one'
-    {ι : Type u_1} {N : Type u_5} [CommMonoid N] [Preorder N]
-    {f : ι → N} [MulLeftMono N] (hf : ∀ (x : ι), f x ≤ 1) :
+theorem prod_anti_set_of_le_one [MulLeftMono N] (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 simp [hf])
+  fun _ _ hst ↦ prod_le_prod_of_subset_of_le_one hst (by simp [hf])
 
-@[to_additive sum_le_univ_sum_of_nonneg]
-theorem prod_le_univ_prod_of_one_le' [MulLeftMono N] [Fintype ι] {s : Finset ι} (w : ∀ x, 1 ≤ f x) :
+@[deprecated (since := "2026-05-22")] alias prod_anti_set_of_le_one' := prod_anti_set_of_le_one
+
+@[to_additive]
+theorem prod_le_univ_prod_of_one_le [MulLeftMono N] [Fintype ι] {s : Finset ι} (w : ∀ x, 1 ≤ f x) :
     ∏ x ∈ s, f x ≤ ∏ x, f x :=
-  prod_le_prod_of_subset_of_one_le' (subset_univ s) fun a _ _ ↦ w a
+  prod_le_prod_of_subset_of_one_le (subset_univ s) fun a _ _ ↦ w a
 
-@[to_additive sum_eq_zero_iff_of_nonneg]
-theorem prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
+@[deprecated (since := "2026-05-22")]
+alias prod_le_univ_prod_of_one_le' := prod_le_univ_prod_of_one_le
+
+@[to_additive]
+theorem prod_eq_one_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
     {f : ι → N} {s : Finset ι} [MulLeftMono N] :
     (∀ i ∈ s, 1 ≤ f i) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) := by
   classical
@@ -170,22 +188,26 @@ theorem prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} [CommMonoid N]
       (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h), fun _ ↦ rfl⟩) ?_
     intro a s ha ih H
     have : ∀ i ∈ s, 1 ≤ f i := fun _ ↦ H _ ∘ mem_insert_of_mem
-    rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod' this),
+    rw [prod_insert ha, mul_eq_one_iff_of_one_le (H _ <| mem_insert_self _ _) (one_le_prod this),
       forall_mem_insert, ih this]
 
+@[deprecated (since := "2026-05-22")] alias prod_eq_one_iff_of_one_le' := prod_eq_one_iff_of_one_le
+
 @[to_additive sum_pos_iff_of_nonneg]
 lemma one_lt_prod_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
     {f : ι → N} {s : Finset ι} [MulLeftMono N] (hf : ∀ x ∈ s, 1 ≤ f x) :
     1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x := by
-  have hsum : 1 ≤ ∏ x ∈ s, f x := one_le_prod' hf
-  rw [hsum.lt_iff_ne', Ne, prod_eq_one_iff_of_one_le' hf, not_forall]
+  have hsum : 1 ≤ ∏ x ∈ s, f x := one_le_prod hf
+  rw [hsum.lt_iff_ne', Ne, prod_eq_one_iff_of_one_le hf, not_forall]
   simp +contextual [← exists_prop, -exists_const_iff, hf _ _ |>.lt_iff_ne']
 
-@[to_additive sum_eq_zero_iff_of_nonpos]
-theorem prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
+@[to_additive]
+theorem prod_eq_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
     {f : ι → N} {s : Finset ι} [MulLeftMono N] :
     (∀ i ∈ s, f i ≤ 1) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) :=
-  prod_eq_one_iff_of_one_le' (N := Nᵒᵈ)
+  prod_eq_one_iff_of_one_le (N := Nᵒᵈ)
+
+@[deprecated (since := "2026-05-22")] alias prod_eq_one_iff_of_le_one' := prod_eq_one_iff_of_le_one
 
 @[to_additive]
 lemma prod_lt_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N]
@@ -193,13 +215,15 @@ lemma prod_lt_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N] [P
     ∏ x ∈ s, f x < 1 ↔ ∃ x ∈ s, f x < 1 :=
   one_lt_prod_iff_of_one_le (N := Nᵒᵈ) hf
 
-@[to_additive single_le_sum]
-theorem single_le_prod' [MulLeftMono N] (hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a ∈ s) :
+@[to_additive]
+theorem single_le_prod [MulLeftMono N] (hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a ∈ s) :
     f a ≤ ∏ x ∈ s, f x :=
   calc
     f a = ∏ i ∈ {a}, f i := (prod_singleton _ _).symm
     _ ≤ ∏ i ∈ s, f i :=
-      prod_le_prod_of_subset_of_one_le' (singleton_subset_iff.2 h) fun i hi _ ↦ hf i hi
+      prod_le_prod_of_subset_of_one_le (singleton_subset_iff.2 h) fun i hi _ ↦ hf i hi
+
+@[deprecated (since := "2026-05-22")] alias single_le_prod' := single_le_prod
 
 @[to_additive]
 lemma mul_le_prod [MulLeftMono N] {i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi : i ∈ s) (hj : j ∈ s)
@@ -208,7 +232,7 @@ lemma mul_le_prod [MulLeftMono N] {i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi :
   calc
     f i * f j = ∏ k ∈ .cons i {j} (by simpa), f k := by rw [prod_cons, prod_singleton]
     _ ≤ ∏ k ∈ s, f k := by
-      refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk
+      refine prod_le_prod_of_subset_of_one_le ?_ fun k hk _ ↦ hf k hk
       simp [cons_subset, *]
 
 @[to_additive sum_le_card_nsmul]
@@ -229,28 +253,34 @@ theorem card_biUnion_le_card_mul [DecidableEq β] (s : Finset ι) (f : ι → Fi
 variable {ι' : Type*} [DecidableEq ι']
 
 @[to_additive sum_fiberwise_le_sum_of_sum_fiber_nonneg]
-theorem prod_fiberwise_le_prod_of_one_le_prod_fiber' [MulLeftMono N] {t : Finset ι'} {g : ι → ι'}
+theorem prod_fiberwise_le_prod_of_one_le_prod_fiber [MulLeftMono N] {t : Finset ι'} {g : ι → ι'}
     {f : ι → N} (h : ∀ y ∉ t, (1 : N) ≤ ∏ x ∈ s with g x = y, f x) :
     (∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤ ∏ x ∈ s, f x :=
   calc
     (∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤
         ∏ y ∈ t ∪ s.image g, ∏ x ∈ s with g x = y, f x :=
-      prod_le_prod_of_subset_of_one_le' subset_union_left fun y _ ↦ h y
+      prod_le_prod_of_subset_of_one_le subset_union_left fun y _ ↦ h y
     _ = ∏ x ∈ s, f x :=
       prod_fiberwise_of_maps_to (fun _ hx ↦ mem_union.2 <| Or.inr <| mem_image_of_mem _ hx) _
 
-@[to_additive sum_le_sum_fiberwise_of_sum_fiber_nonpos]
-theorem prod_le_prod_fiberwise_of_prod_fiber_le_one' [MulLeftMono N] {t : Finset ι'} {g : ι → ι'}
+@[deprecated (since := "2026-05-22")]
+alias prod_fiberwise_le_prod_of_one_le_prod_fiber' := prod_fiberwise_le_prod_of_one_le_prod_fiber
+
+@[to_additive]
+theorem prod_le_prod_fiberwise_of_prod_fiber_le_one [MulLeftMono N] {t : Finset ι'} {g : ι → ι'}
     {f : ι → N} (h : ∀ y ∉ t, ∏ x ∈ s with g x = y, f x ≤ 1) :
     ∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ s with g x = y, f x :=
-  prod_fiberwise_le_prod_of_one_le_prod_fiber' (N := Nᵒᵈ) h
+  prod_fiberwise_le_prod_of_one_le_prod_fiber (N := Nᵒᵈ) h
+
+@[deprecated (since := "2026-05-22")]
+alias prod_le_prod_fiberwise_of_prod_fiber_le_one' := prod_le_prod_fiberwise_of_prod_fiber_le_one
 
 @[to_additive]
 lemma prod_image_le_of_one_le [MulLeftMono N]
     {g : ι → ι'} {f : ι' → N} (hf : ∀ u ∈ s.image g, 1 ≤ f u) :
     ∏ u ∈ s.image g, f u ≤ ∏ u ∈ s, f (g u) := by
   rw [prod_comp f g]
-  refine prod_le_prod' fun a hag ↦ ?_
+  refine prod_le_prod fun a hag ↦ ?_
   obtain ⟨i, hi, hig⟩ := Finset.mem_image.mp hag
   apply le_self_pow (hf a hag)
   rw [← Nat.pos_iff_ne_zero, card_pos]
@@ -293,6 +323,8 @@ theorem abs_sum_of_nonneg {G : Type*} [AddCommGroup G] [LinearOrder G] [AddLeftM
     (hf : ∀ i ∈ s, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i := by
   rw [abs_of_nonneg (Finset.sum_nonneg hf)]
 
+set_option linter.deprecated false in
+@[deprecated abs_sum_of_nonneg (since := "2026-05-22")]
 theorem abs_sum_of_nonneg' {G : Type*} [AddCommGroup G] [LinearOrder G] [AddLeftMono G]
     {f : ι → G} {s : Finset ι}
     (hf : ∀ i, 0 ≤ f i) : |∑ i ∈ s, f i| = ∑ i ∈ s, f i := by
@@ -413,20 +445,24 @@ See also `Finset.single_le_sum`. -/]
 lemma single_le_prod_of_canonicallyOrdered {i : ι} (hi : i ∈ s) :
     f i ≤ ∏ j ∈ s, f j :=
   have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
-  single_le_prod' (fun _ _ ↦ one_le) hi
+  single_le_prod (fun _ _ ↦ one_le) hi
 
-@[to_additive sum_le_sum_of_subset]
-theorem prod_le_prod_of_subset' (h : s ⊆ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x :=
+@[to_additive]
+theorem prod_le_prod_of_subset (h : s ⊆ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x :=
   have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
-  prod_le_prod_of_subset_of_one_le' h fun _ _ _ ↦ one_le
+  prod_le_prod_of_subset_of_one_le h fun _ _ _ ↦ one_le
+
+@[deprecated (since := "2026-05-22")] alias prod_le_prod_of_subset' := prod_le_prod_of_subset
 
-@[to_additive sum_mono_set]
-theorem prod_mono_set' (f : ι → M) : Monotone fun s ↦ ∏ x ∈ s, f x := fun _ _ hs ↦
+@[to_additive]
+theorem prod_mono_set (f : ι → M) : Monotone fun s ↦ ∏ x ∈ s, f x := fun _ _ hs ↦
   have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
-  prod_le_prod_of_subset' hs
+  prod_le_prod_of_subset hs
 
-@[to_additive sum_le_sum_of_ne_zero]
-theorem prod_le_prod_of_ne_one' (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) :
+@[deprecated (since := "2026-05-22")] alias prod_mono_set' := prod_mono_set
+
+@[to_additive]
+theorem prod_le_prod_of_ne_one (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) :
     ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x := by
   have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
   classical calc
@@ -435,8 +471,10 @@ theorem prod_le_prod_of_ne_one' (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) :
       exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
     _ ≤ ∏ x ∈ t, f x :=
       mul_le_of_le_one_of_le
-        (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
-        (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])
+        (prod_le_one <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
+        (prod_le_prod_of_subset <| by simpa only [subset_iff, mem_filter, and_imp])
+
+@[deprecated (since := "2026-05-22")] alias prod_le_prod_of_ne_one' := prod_le_prod_of_ne_one
 
 @[to_additive sum_pos_iff]
 lemma one_lt_prod_iff {ι M : Type*} [CommMonoid M] [PartialOrder M] [CanonicallyOrderedMul M]
@@ -450,27 +488,31 @@ section OrderedCancelCommMonoid
 
 variable [CommMonoid M] [Preorder M] [IsOrderedCancelMonoid M] {f g : ι → M} {s t : Finset ι}
 
-@[to_additive sum_lt_sum]
-theorem prod_lt_prod' [MulLeftStrictMono M] (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
+@[to_additive]
+theorem prod_lt_prod [MulLeftStrictMono M] (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
     ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
-  Multiset.prod_lt_prod' hle hlt
+  Multiset.prod_lt_prod hle hlt
+
+@[deprecated (since := "2026-05-22")] alias prod_lt_prod' := prod_lt_prod
 
 /-- In an ordered commutative monoid, if each factor `f i` of one nontrivial finite product is
 strictly less than the corresponding factor `g i` of another nontrivial finite product, then
 `s.prod f < s.prod g`. -/
-@[to_additive (attr := gcongr) sum_lt_sum_of_nonempty]
-theorem prod_lt_prod_of_nonempty' [MulLeftStrictMono M] (hs : s.Nonempty)
+@[to_additive (attr := gcongr)]
+theorem prod_lt_prod_of_nonempty [MulLeftStrictMono M] (hs : s.Nonempty)
   (hlt : ∀ i ∈ s, f i < g i) :
     ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
-  Multiset.prod_lt_prod_of_nonempty' (by aesop) hlt
+  Multiset.prod_lt_prod_of_nonempty (by aesop) hlt
+
+@[deprecated (since := "2026-05-22")] alias prod_lt_prod_of_nonempty' := prod_lt_prod_of_nonempty
 
 /-- In an ordered additive commutative monoid, if each summand `f i` of one nontrivial finite sum is
 strictly less than the corresponding summand `g i` of another nontrivial finite sum, then
 `s.sum f < s.sum g`. -/
 add_decl_doc sum_lt_sum_of_nonempty
 
-@[to_additive sum_lt_sum_of_subset]
-theorem prod_lt_prod_of_subset' [MulLeftStrictMono M] (h : s ⊆ t) {i : ι} (ht : i ∈ t)
+@[to_additive]
+theorem prod_lt_prod_of_subset [MulLeftStrictMono M] (h : s ⊆ t) {i : ι} (ht : i ∈ t)
   (hs : i ∉ s) (hlt : 1 < f i)
     (hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j) : ∏ j ∈ s, f j < ∏ j ∈ t, f j := by
   classical calc
@@ -478,40 +520,44 @@ theorem prod_lt_prod_of_subset' [MulLeftStrictMono M] (h : s ⊆ t) {i : ι} (ht
       rw [prod_insert hs]
       exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
     _ ≤ ∏ j ∈ t, f j := by
-      apply prod_le_prod_of_subset_of_one_le'
+      apply prod_le_prod_of_subset_of_one_le
       · simp [Finset.insert_subset_iff, h, ht]
       · intro x hx h'x
         simp only [mem_insert, not_or] at h'x
         exact hle x hx h'x.2
 
-@[to_additive single_lt_sum]
-theorem single_lt_prod' [MulLeftStrictMono M] {i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s)
+@[deprecated (since := "2026-05-22")] alias prod_lt_prod_of_subset' := prod_lt_prod_of_subset
+
+@[to_additive]
+theorem single_lt_prod [MulLeftStrictMono M] {i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s)
     (hlt : 1 < f j) (hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k) : f i < ∏ k ∈ s, f k :=
   calc
     f i = ∏ k ∈ {i}, f k := by rw [prod_singleton]
     _ < ∏ k ∈ s, f k :=
-      prod_lt_prod_of_subset' (singleton_subset_iff.2 hi) hj (mt mem_singleton.1 hij) hlt
+      prod_lt_prod_of_subset (singleton_subset_iff.2 hi) hj (mt mem_singleton.1 hij) hlt
         fun k hks hki ↦ hle k hks (mt mem_singleton.2 hki)
 
+@[deprecated (since := "2026-05-22")] alias single_lt_prod' := single_lt_prod
+
 @[to_additive sum_pos]
 theorem one_lt_prod [MulLeftStrictMono M] (h : ∀ i ∈ s, 1 < f i) (hs : s.Nonempty) :
     1 < ∏ i ∈ s, f i :=
-  lt_of_le_of_lt (by rw [prod_const_one]) <| prod_lt_prod_of_nonempty' hs h
+  lt_of_le_of_lt (by rw [prod_const_one]) <| prod_lt_prod_of_nonempty hs h
 
 @[to_additive]
 theorem prod_lt_one [MulLeftStrictMono M] (h : ∀ i ∈ s, f i < 1) (hs : s.Nonempty) :
     ∏ i ∈ s, f i < 1 :=
-  (prod_lt_prod_of_nonempty' hs h).trans_le (by rw [prod_const_one])
+  (prod_lt_prod_of_nonempty hs h).trans_le (by rw [prod_const_one])
 
 @[to_additive sum_pos']
 theorem one_lt_prod' [MulLeftStrictMono M] (h : ∀ i ∈ s, 1 ≤ f i) (hs : ∃ i ∈ s, 1 < f i) :
     1 < ∏ i ∈ s, f i :=
-  prod_const_one.symm.trans_lt <| prod_lt_prod' h hs
+  prod_const_one.symm.trans_lt <| prod_lt_prod h hs
 
 @[to_additive]
 theorem prod_lt_one' [MulLeftStrictMono M] (h : ∀ i ∈ s, f i ≤ 1) (hs : ∃ i ∈ s, f i < 1) :
     ∏ i ∈ s, f i < 1 :=
-  prod_const_one.le.trans_lt' <| prod_lt_prod' h hs
+  prod_const_one.le.trans_lt' <| prod_lt_prod h hs
 
 @[to_additive]
 theorem prod_eq_prod_iff_of_le {ι M : Type*} [CommMonoid M] [PartialOrder M]
@@ -525,7 +571,7 @@ theorem prod_eq_prod_iff_of_le {ι M : Type*} [CommMonoid M] [PartialOrder M]
     rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
     exact
       mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a))
-        (Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)
+        (Finset.prod_le_prod fun i ↦ H i ∘ Finset.mem_insert_of_mem)
 
 @[to_additive] lemma prod_sdiff_le_prod_sdiff [DecidableEq ι] :
     ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
@@ -546,30 +592,37 @@ section LinearOrderedCancelCommMonoid
 
 variable [CommMonoid M] [LinearOrder M] {f g : ι → M} {s t : Finset ι}
 
-@[to_additive exists_lt_of_sum_lt]
-theorem exists_lt_of_prod_lt' [MulLeftMono M] (Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) :
+@[to_additive]
+theorem exists_lt_of_prod_lt [MulLeftMono M] (Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) :
     ∃ i ∈ s, f i < g i := by
   contrapose! Hlt with Hle
-  exact prod_le_prod' Hle
+  exact prod_le_prod Hle
+
+@[deprecated (since := "2026-05-22")] alias exists_lt_of_prod_lt' := exists_lt_of_prod_lt
 
 variable [IsOrderedCancelMonoid M]
 
-@[to_additive exists_le_of_sum_le]
-theorem exists_le_of_prod_le' (hs : s.Nonempty) (Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i) :
+@[to_additive]
+theorem exists_le_of_prod_le (hs : s.Nonempty) (Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i) :
     ∃ i ∈ s, f i ≤ g i := by
   contrapose! Hle with Hlt
-  exact prod_lt_prod_of_nonempty' hs Hlt
+  exact prod_lt_prod_of_nonempty hs Hlt
+
+@[deprecated (since := "2026-05-22")] alias exists_le_of_prod_le' := exists_le_of_prod_le
 
 @[to_additive exists_pos_of_sum_zero_of_exists_nonzero]
-theorem exists_one_lt_of_prod_one_of_exists_ne_one' (f : ι → M) (h₁ : ∏ i ∈ s, f i = 1)
+theorem exists_one_lt_of_prod_one_of_exists_ne_one (f : ι → M) (h₁ : ∏ i ∈ s, f i = 1)
     (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, 1 < f i := by
   contrapose! h₁
   obtain ⟨i, m, i_ne⟩ : ∃ i ∈ s, f i ≠ 1 := h₂
   apply ne_of_lt
   calc
-    ∏ j ∈ s, f j < ∏ j ∈ s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
+    ∏ j ∈ s, f j < ∏ j ∈ s, 1 := prod_lt_prod h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
     _ = 1 := prod_const_one
 
+@[deprecated (since := "2026-05-22")]
+alias exists_one_lt_of_prod_one_of_exists_ne_one' := exists_one_lt_of_prod_one_of_exists_ne_one
+
 end LinearOrderedCancelCommMonoid
 
 theorem apply_sup_le_sum [SemilatticeSup α] [OrderBot α]
@@ -605,35 +658,39 @@ namespace Fintype
 section OrderedCommMonoid
 variable [Fintype ι] [CommMonoid M] [Preorder M] [MulLeftMono M] {f : ι → M}
 
-@[to_additive (attr := mono) sum_mono]
-theorem prod_mono' : Monotone fun f : ι → M ↦ ∏ i, f i := fun _ _ hfg ↦
-  Finset.prod_le_prod' fun x _ ↦ hfg x
+@[to_additive (attr := mono)]
+theorem prod_mono : Monotone fun f : ι → M ↦ ∏ i, f i := fun _ _ hfg ↦
+  Finset.prod_le_prod fun x _ ↦ hfg x
+
+@[deprecated (since := "2026-05-22")] alias prod_mono' := prod_mono
 
 @[to_additive sum_nonneg]
-lemma one_le_prod (hf : 1 ≤ f) : 1 ≤ ∏ i, f i := Finset.one_le_prod' fun _ _ ↦ hf _
+lemma one_le_prod (hf : 1 ≤ f) : 1 ≤ ∏ i, f i := Finset.one_le_prod fun _ _ ↦ hf _
 
-@[to_additive] lemma prod_le_one (hf : f ≤ 1) : ∏ i, f i ≤ 1 := Finset.prod_le_one' fun _ _ ↦ hf _
+@[to_additive] lemma prod_le_one (hf : f ≤ 1) : ∏ i, f i ≤ 1 := Finset.prod_le_one fun _ _ ↦ hf _
 
 @[to_additive]
 lemma prod_eq_one_iff_of_one_le {ι M : Type*} [Fintype ι] [CommMonoid M] [PartialOrder M]
     [MulLeftMono M] {f : ι → M} (hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1 :=
-  (Finset.prod_eq_one_iff_of_one_le' fun i _ ↦ hf i).trans <| by simp [funext_iff]
+  (Finset.prod_eq_one_iff_of_one_le fun i _ ↦ hf i).trans <| by simp [funext_iff]
 
 @[to_additive]
 lemma prod_eq_one_iff_of_le_one {ι M : Type*} [Fintype ι] [CommMonoid M] [PartialOrder M]
     [MulLeftMono M] {f : ι → M} (hf : f ≤ 1) : ∏ i, f i = 1 ↔ f = 1 :=
-  (Finset.prod_eq_one_iff_of_le_one' fun i _ ↦ hf i).trans <| by simp [funext_iff]
+  (Finset.prod_eq_one_iff_of_le_one fun i _ ↦ hf i).trans <| by simp [funext_iff]
 
 end OrderedCommMonoid
 
 section OrderedCancelCommMonoid
 variable [Fintype ι] [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M}
 
-@[to_additive sum_strictMono]
-theorem prod_strictMono' : StrictMono fun f : ι → M ↦ ∏ x, f x :=
+@[to_additive]
+theorem prod_strictMono : StrictMono fun f : ι → M ↦ ∏ x, f x :=
   fun _ _ hfg ↦
   let ⟨hle, i, hlt⟩ := Pi.lt_def.mp hfg
-  Finset.prod_lt_prod' (fun i _ ↦ hle i) ⟨i, Finset.mem_univ i, hlt⟩
+  Finset.prod_lt_prod (fun i _ ↦ hle i) ⟨i, Finset.mem_univ i, hlt⟩
+
+@[deprecated (since := "2026-05-22")] alias prod_strictMono' := prod_strictMono
 
 @[to_additive sum_pos]
 lemma one_lt_prod (hf : 1 < f) : 1 < ∏ i, f i :=
diff --git a/Mathlib/Algebra/Order/BigOperators/Group/List.lean b/Mathlib/Algebra/Order/BigOperators/Group/List.lean
index 2e7559ef376614..885703124b126c 100644
--- a/Mathlib/Algebra/Order/BigOperators/Group/List.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Group/List.lean
@@ -24,49 +24,58 @@ 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
   | nil => rfl
   | cons hab ih ih' => simpa only [prod_cons] using mul_le_mul' hab ih'
 
+@[deprecated (since := "2026-05-22")] alias Forall₂.prod_le_prod' := Forall₂.prod_le_prod
+
 /-- 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]
+@[deprecated (since := "2026-05-22")] alias Sublist.prod_le_prod' := Sublist.prod_le_prod
+
+@[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]
+@[deprecated (since := "2026-05-22")]
+alias SublistForall₂.prod_le_prod' := SublistForall₂.prod_le_prod
+
+@[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
+
+@[deprecated (since := "2026-05-22")] alias prod_le_prod' := prod_le_prod
 
-@[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,22 +85,24 @@ 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 ‹_›
 
+@[deprecated (since := "2026-05-22")] alias prod_lt_prod' := prod_lt_prod
+
 @[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]
@@ -99,21 +110,25 @@ lemma pow_card_le_prod [Preorder M] [MulRightMono M]
     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]
+@[deprecated (since := "2026-05-22")] alias exists_lt_of_prod_lt' := exists_lt_of_prod_lt
+
+@[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
   contrapose! h
   exact prod_lt_prod_of_ne_nil hl _ _ h
 
+@[deprecated (since := "2026-05-22")] alias exists_le_of_prod_le' := exists_le_of_prod_le
+
 @[to_additive sum_nonneg]
 lemma one_le_prod_of_one_le [Preorder M] [MulLeftMono M] {l : List M}
     (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) : 1 ≤ l.prod := by
@@ -130,7 +145,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 +154,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
 
diff --git a/Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean b/Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
index be515afff9365f..daa89236a4fa1f 100644
--- a/Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@@ -118,18 +118,22 @@ 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
+
+@[deprecated (since := "2026-05-22")] alias prod_lt_prod' := prod_lt_prod
 
-@[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⟩
+
+@[deprecated (since := "2026-05-22")] alias prod_lt_prod_of_nonempty' := prod_lt_prod_of_nonempty
 
 end OrderedCancelCommMonoid
 
diff --git a/Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean b/Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean
index 038dc379e422b1..c54589f45271c7 100644
--- a/Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/GroupWithZero/Finset.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,7 +107,7 @@ 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
@@ -115,15 +115,15 @@ lemma prod_lt_prod (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i ≤ g i)
   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⟩
 
diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
index a2d67c703fbb11..dea9885add30fa 100644
--- a/Mathlib/Analysis/Analytic/Composition.lean
+++ b/Mathlib/Analysis/Analytic/Composition.lean
@@ -474,7 +474,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
diff --git a/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean b/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
index 5b01e03ea44e57..8e9be8a785b63e 100644
--- a/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
+++ b/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
@@ -138,7 +138,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
diff --git a/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean b/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
index 116249ba98ace2..516568a14b133d 100644
--- a/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
+++ b/Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean
@@ -228,7 +228,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)) :=
diff --git a/Mathlib/Analysis/Complex/Exponential.lean b/Mathlib/Analysis/Complex/Exponential.lean
index 1bf61e0671053f..2d2a66ff4905d8 100644
--- a/Mathlib/Analysis/Complex/Exponential.lean
+++ b/Mathlib/Analysis/Complex/Exponential.lean
@@ -681,7 +681,7 @@ lemma exp_le_two_add_div_two_sub {x : ℝ} (hx : 0 ≤ x) (hx' : x < 2) :
 
 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
 
diff --git a/Mathlib/Analysis/Complex/JensenFormula.lean b/Mathlib/Analysis/Complex/JensenFormula.lean
index cf6c3caf6b36d5..96ae24417c3227 100644
--- a/Mathlib/Analysis/Complex/JensenFormula.lean
+++ b/Mathlib/Analysis/Complex/JensenFormula.lean
@@ -412,7 +412,7 @@ theorem AnalyticOnNhd.sum_divisor_le {c : ℂ} {r R M : ℝ} {f : ℂ → ℂ} (
   calc
   -- Bound by the sum from Jensen's formula
   _ ≤ ∑ᶠ u, ((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) := by
-    refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
+    refine finsum_le_finsum ?_ ?_ fun u ↦ ?_
     · exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
         fun _ _ ↦ (by simp_all)
     · exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
diff --git a/Mathlib/Analysis/InnerProductSpace/Orientation.lean b/Mathlib/Analysis/InnerProductSpace/Orientation.lean
index 8dcdff2be957b9..62e127775a1d7a 100644
--- a/Mathlib/Analysis/InnerProductSpace/Orientation.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Orientation.lean
@@ -249,10 +249,7 @@ theorem abs_volumeForm_apply_le (v : Fin n → E) : |o.volumeForm v| ≤ ∏ i :
   let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
   have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det this v
   rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
-  apply Finset.prod_le_prod
-  · intro i _
-    positivity
-  intro i _
+  gcongr with i
   convert! abs_real_inner_le_norm (b i) (v i)
   simp [b.orthonormal.1 i]
 
diff --git a/Mathlib/Analysis/InnerProductSpace/Subspace.lean b/Mathlib/Analysis/InnerProductSpace/Subspace.lean
index 573d4c57e659df..f8dd20f3e1cbc8 100644
--- a/Mathlib/Analysis/InnerProductSpace/Subspace.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Subspace.lean
@@ -206,8 +206,7 @@ theorem OrthogonalFamily.summable_iff_norm_sq_summable [CompleteSpace E] (f : 
       intro s₁ hs₁ s₂ hs₂
       rw [← Finset.sum_sdiff_sub_sum_sdiff]
       refine (abs_sub _ _).trans_lt ?_
-      have : ∀ i, 0 ≤ ‖f i‖ ^ 2 := fun i : ι => sq_nonneg _
-      simp only [Finset.abs_sum_of_nonneg' this]
+      simp only [sq_nonneg, implies_true, Finset.abs_sum_of_nonneg]
       have : ((∑ i ∈ s₁ \ s₂, ‖f i‖ ^ 2) + ∑ i ∈ s₂ \ s₁, ‖f i‖ ^ 2) < √ε ^ 2 := by
         rw [← hV.norm_sq_sdiff_sum, sq_lt_sq, abs_of_nonneg (sqrt_nonneg _),
           abs_of_nonneg (norm_nonneg _)]
@@ -225,15 +224,11 @@ theorem OrthogonalFamily.summable_iff_norm_sq_summable [CompleteSpace E] (f : 
       have Hs₁ : ∑ x ∈ s₁ \ s₂, ‖f x‖ ^ 2 < ε ^ 2 / 2 := by
         convert! H _ hs₁ _ has
         have : s₁ ⊓ s₂ ⊆ s₁ := Finset.inter_subset_left
-        rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']
-        · simp
-        · exact fun i => sq_nonneg _
+        simp [← Finset.sum_sdiff this, Finset.abs_sum_of_nonneg]
       have Hs₂ : ∑ x ∈ s₂ \ s₁, ‖f x‖ ^ 2 < ε ^ 2 / 2 := by
         convert! H _ hs₂ _ has
         have : s₁ ⊓ s₂ ⊆ s₂ := Finset.inter_subset_right
-        rw [← Finset.sum_sdiff this, add_tsub_cancel_right, Finset.abs_sum_of_nonneg']
-        · simp
-        · exact fun i => sq_nonneg _
+        simp [← Finset.sum_sdiff this, Finset.abs_sum_of_nonneg]
       linarith
 
 end
diff --git a/Mathlib/Analysis/Normed/Ring/Basic.lean b/Mathlib/Analysis/Normed/Ring/Basic.lean
index 5ffd65f31cb975..22972ceb00cb5f 100644
--- a/Mathlib/Analysis/Normed/Ring/Basic.lean
+++ b/Mathlib/Analysis/Normed/Ring/Basic.lean
@@ -978,7 +978,7 @@ lemma iSup_prod_eq_prod_iSup_of_nonneg {f : (a : α) → ι a → ℝ} (hf₀ :
     obtain ⟨a, ha⟩ := isEmpty_pi.mp h
     exact ⟨a, by simp⟩
   refine le_antisymm ?_ ?_
-  · exact ciSup_le fun i ↦ Finset.prod_le_prod (by simp [hf₀])
+  · exact ciSup_le fun i ↦ Finset.prod_le_prod₀ (by simp [hf₀])
       fun a ha ↦ Finite.le_ciSup_of_le _ le_rfl
   · rw [Classical.nonempty_pi] at h
     have H a : ∃ i : ι a, f a i = ⨆ i, f a i := exists_eq_ciSup_of_finite
diff --git a/Mathlib/Analysis/Normed/Ring/InfiniteProd.lean b/Mathlib/Analysis/Normed/Ring/InfiniteProd.lean
index 90c5b07850a935..553934ed8de6bd 100644
--- a/Mathlib/Analysis/Normed/Ring/InfiniteProd.lean
+++ b/Mathlib/Analysis/Normed/Ring/InfiniteProd.lean
@@ -46,7 +46,7 @@ public theorem tendsto_tprod_one_add_of_dominated_convergence {𝓕 : Filter α}
       (fun i ↦ (norm_nonneg (g i)).trans (h_bound_g i)) h_sum)
       (tendsto_finsetProd · fun i _ ↦ hab i)
       (h_bound.mono fun n hn s ↦ (Finset.norm_prod_le s (f n)).trans
-      (Finset.prod_le_prod (by grind) (by grind)))
+      (Finset.prod_le_prod₀ (by grind) (by grind)))
   apply this.congr' (h_bound.mono fun n hn ↦ ?_)
   rw [tprod_one_add]
   exact summable_finsetProd_of_summable_norm <| h_sum.of_nonneg_of_le (by grind) hn
diff --git a/Mathlib/Analysis/ODE/DiscreteGronwall.lean b/Mathlib/Analysis/ODE/DiscreteGronwall.lean
index 1323eb13e81b5d..6ca9585f6a5825 100644
--- a/Mathlib/Analysis/ODE/DiscreteGronwall.lean
+++ b/Mathlib/Analysis/ODE/DiscreteGronwall.lean
@@ -84,7 +84,8 @@ theorem discrete_gronwall {n₀ : ℕ} (hun₀ : 0 ≤ u n₀)
     _ = (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i) := by rw [add_mul, sum_mul]
     _ ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * exp (∑ i ∈ Ico n₀ n, c i) := by
         gcongr <;> try exact add_nonneg hun₀ <| sum_nonneg <| by grind
-        simpa [exp_sum] using prod_le_prod (by grind) (by grind [add_one_le_exp])
+        rw [exp_sum]
+        exact prod_le_prod₀ (by grind) (by grind [add_one_le_exp])
 
 /-- Discrete Grönwall inequality, uniform bound: a single bound holding for all `n ∈ [n₀, n₁)`. -/
 theorem discrete_gronwall_Ico {n₀ n₁ : ℕ} (hun₀ : 0 ≤ u n₀)
diff --git a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean
index 3c827acbd101df..73a7356ab072d0 100644
--- a/Mathlib/Analysis/Polynomial/MahlerMeasure.lean
+++ b/Mathlib/Analysis/Polynomial/MahlerMeasure.lean
@@ -385,7 +385,7 @@ theorem norm_coeff_le_choose_mul_mahlerMeasure (n : ℕ) (p : ℂ[X]) :
     _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
       simp_rw [← coe_nnnorm]
       norm_cast
-      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
+      exact Finset.prod_le_prod_of_subset_of_one_le (toFinset_subset.mpr (subset_of_le hx.1))
         (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
     _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
       gcongr with a
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Extremal.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Extremal.lean
index 1af1d845979ab0..2eb9c7be31f2c9 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Extremal.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Extremal.lean
@@ -257,11 +257,11 @@ private theorem negOnePow_mul_iterateDerivativeC_nonneg
     {n k i : ℕ} (hi : i ≤ n) {x : ℝ} (hx : 1 ≤ x) :
     0 ≤ (-1) ^ i * iterateDerivativeC n k x i := by
   rw [iterateDerivativeC, ← mul_assoc]
-  refine mul_nonneg ?_ (Finset.sum_nonneg' ?_)
+  refine mul_nonneg ?_ (Finset.sum_nonneg fun t _ => ?_)
   · rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]
     exact le_of_lt <| mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k)
       (negOnePow_mul_leadingCoeffC_pos hi)
-  · exact fun t => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])
+  · exact Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])
 
 private theorem negOnePow_mul_iterateDerivativeC_pos
     {n k i : ℕ} (hk₁ : 0 < k) (hk₂ : k ≤ n) (hi : i ≤ n) {x : ℝ} (hx : 1 ≤ x) :
diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean
index 3e6f9b38f9ce90..a2fb6fb68ccee9 100644
--- a/Mathlib/Analysis/SpecificLimits/Basic.lean
+++ b/Mathlib/Analysis/SpecificLimits/Basic.lean
@@ -686,7 +686,7 @@ theorem tendsto_factorial_div_pow_self_atTop :
         Finset.prod_range_succ']
       simp only [one_mul, Nat.cast_add, zero_add, Nat.cast_one]
       refine
-            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_) <;>
+            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one₀ ?_ ?_) <;>
           intro x hx <;>
         rw [Finset.mem_range] at hx
       · positivity
diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
index 888e669c9737ed..6169a3da1bca03 100644
--- a/Mathlib/MeasureTheory/Constructions/Pi.lean
+++ b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -90,7 +90,7 @@ theorem piPremeasure_pi' {s : ∀ i, Set (α i)} : piPremeasure m (pi univ s) =
 
 theorem piPremeasure_pi_mono {s t : Set (∀ i, α i)} (h : s ⊆ t) :
     piPremeasure m s ≤ piPremeasure m t :=
-  Finset.prod_le_prod' fun _ _ => measure_mono (Set.image_mono h)
+  Finset.prod_le_prod fun _ _ => measure_mono (Set.image_mono h)
 
 theorem piPremeasure_pi_eval {s : Set (∀ i, α i)} :
     piPremeasure m (pi univ fun i => eval i '' s) = piPremeasure m s := by
@@ -558,7 +558,7 @@ instance _root_.IsUnifLocDoublingMeasure.pi {ι : Type*} [Fintype ι] {X : ι 
       IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul (μ i),
     eventually_mem_nhdsWithin] with r hr (hr₀ : 0 < r) x
   simpa (disch := positivity) [Finset.prod_mul_distrib, closedBall_pi, pi_pi]
-    using Fintype.prod_mono' fun i ↦ hr i (x i)
+    using Fintype.prod_mono fun i ↦ hr i (x i)
 
 instance IsUnifLocDoublingMeasure.volume_pi {ι : Type*} [Fintype ι] {X : ι → Type*}
     [∀ i, PseudoMetricSpace (X i)] [∀ i, MeasureSpace (X i)]
diff --git a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean
index ade03081e94b2a..a4e3ce09fa0cd8 100644
--- a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean
+++ b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean
@@ -135,7 +135,7 @@ lemma ext_of_lintegral_prod_mul_prod_boundedContinuousFunction
     refine tendsto_lintegral_filter_of_dominated_convergence 1
       (Eventually.of_forall <| by fun_prop) (Eventually.of_forall fun n ↦ ae_of_all _ fun ω ↦ ?_)
       (by simp) (ae_of_all _ this)
-    grw [Finset.prod_le_one (by simp), Finset.prod_le_one (by simp)]
+    grw [Finset.prod_le_one₀ (by simp), Finset.prod_le_one₀ (by simp)]
     · simp
     · exact fun j _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (ht j) _ _
     · exact fun i _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (hs i) _ _
@@ -146,7 +146,7 @@ lemma ext_of_lintegral_prod_mul_prod_boundedContinuousFunction
     refine tendsto_lintegral_filter_of_dominated_convergence 1
       (Eventually.of_forall <| by fun_prop) (Eventually.of_forall fun _ ↦ ae_of_all _ fun _ ↦ ?_)
       (by simp) (ae_of_all _ this)
-    grw [Finset.prod_le_one (by simp), Finset.prod_le_one (by simp)]
+    grw [Finset.prod_le_one₀ (by simp), Finset.prod_le_one₀ (by simp)]
     · simp
     · exact fun j _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (ht j) _ _
     · exact fun i _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (hs i) _ _
diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
index e1301292f1006f..6dfeb5142943b4 100644
--- a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
+++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
@@ -293,14 +293,14 @@ theorem volume_pi_le_prod_diam (s : Set (ι → ℝ)) :
       volume.mono <|
         Subset.trans (subset_pi_eval_image univ s) <| pi_mono fun _ _ => subset_closure
     _ = ∏ i, volume (closure <| Function.eval i '' s) := volume_pi_pi _
-    _ ≤ ∏ i : ι, ediam (Function.eval i '' s) :=
-      Finset.prod_le_prod' fun _ _ => (volume_le_diam _).trans_eq (ediam_closure _)
+    _ ≤ ∏ i : ι, ediam (Function.eval i '' s) := by
+      gcongr; exact (volume_le_diam _).trans_eq (ediam_closure _)
 
 theorem volume_pi_le_diam_pow (s : Set (ι → ℝ)) : volume s ≤ ediam s ^ Fintype.card ι :=
   calc
     volume s ≤ ∏ i : ι, ediam (Function.eval i '' s) := volume_pi_le_prod_diam s
-    _ ≤ ∏ _i : ι, (1 : ℝ≥0) * ediam s :=
-      (Finset.prod_le_prod' fun i _ => (LipschitzWith.eval i).ediam_image_le s)
+    _ ≤ ∏ _i : ι, (1 : ℝ≥0) * ediam s := by
+      gcongr with i; exact (LipschitzWith.eval i).ediam_image_le s
     _ = ediam s ^ Fintype.card ι := by
       simp only [ENNReal.coe_one, one_mul, Finset.prod_const, Fintype.card]
 
diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
index 2aeca2034d8903..e0597f13b97be8 100644
--- a/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
+++ b/Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
@@ -154,9 +154,7 @@ theorem MeasureTheory.volume_sum_rpow_lt_one (hp : 1 ≤ p) :
       .ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (card ι / p + 1)) := by
   have h₁ : 0 < p := by linarith
   have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)
-  have h₂ : ∀ x : ι → ℝ, 0 ≤ ∑ i, |x i| ^ p := by
-    refine fun _ => Finset.sum_nonneg' ?_
-    exact fun i => (fun _ => rpow_nonneg (abs_nonneg _) _) _
+  have h₂ (x : ι → ℝ) : 0 ≤ ∑ i, |x i| ^ p := by positivity
   -- We collect facts about `Lp` norms that will be used in `measure_lt_one_eq_integral_div_gamma`
   have eq_norm (x : ι → ℝ) : ‖toLp (.ofReal p) x‖ = (∑ i, |x i| ^ p) ^ (1 / p) := by
     simp [PiLp.norm_eq_sum (f := toLp (.ofReal p) x) (this.symm ▸ h₁), this]
@@ -176,7 +174,7 @@ theorem MeasureTheory.volume_sum_rpow_lt_one (hp : 1 ≤ p) :
       (∑ i, |x i| ^ p) ^ (1 / p)) nm_zero nm_neg nm_add (eq_zero _).mp (fun r x => nm_smul r x)
       (by linarith : 0 < p)) using 4
   · rw [rpow_lt_one_iff' _ (one_div_pos.mpr h₁)]
-    exact Finset.sum_nonneg' (fun _ => rpow_nonneg (abs_nonneg _) _)
+    positivity
   · simp_rw [← rpow_mul (h₂ _), div_mul_cancel₀ _ (ne_of_gt h₁), Real.rpow_one,
       ← Finset.sum_neg_distrib, exp_sum]
     rw [integral_fintype_prod_volume_eq_pow fun x : ℝ => exp (- |x| ^ p), integral_comp_abs
@@ -229,9 +227,7 @@ theorem Complex.volume_sum_rpow_lt_one {p : ℝ} (hp : 1 ≤ p) :
       .ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * card ι / p + 1)) := by
   have h₁ : 0 < p := by linarith
   have : (ENNReal.ofReal p).toReal = p := toReal_ofReal (le_of_lt h₁)
-  have h₂ : ∀ x : ι → ℂ, 0 ≤ ∑ i, ‖x i‖ ^ p := by
-    refine fun _ => Finset.sum_nonneg' ?_
-    exact fun i => (fun _ => rpow_nonneg (norm_nonneg _) _) _
+  have h₂ (x : ι → ℂ) : 0 ≤ ∑ i, ‖x i‖ ^ p := by positivity
   -- We collect facts about `Lp` norms that will be used in `measure_lt_one_eq_integral_div_gamma`
   have eq_norm (x : ι → ℂ) : ‖toLp (.ofReal p) x‖ = (∑ i, ‖x i‖ ^ p) ^ (1 / p) := by
     simp [PiLp.norm_eq_sum (f := toLp (.ofReal p) x) (this.symm ▸ h₁), this]
@@ -250,7 +246,7 @@ theorem Complex.volume_sum_rpow_lt_one {p : ℝ} (hp : 1 ≤ p) :
       (∑ i, ‖x i‖ ^ p) ^ (1 / p)) nm_zero nm_neg nm_add (eq_zero _).mp (fun r x => nm_smul r x)
       (by linarith : 0 < p) using 4
   · rw [rpow_lt_one_iff' _ (one_div_pos.mpr h₁)]
-    exact Finset.sum_nonneg' (fun _ => rpow_nonneg (norm_nonneg _) _)
+    positivity
   · simp_rw [← rpow_mul (h₂ _), div_mul_cancel₀ _ (ne_of_gt h₁), Real.rpow_one,
       ← Finset.sum_neg_distrib, Real.exp_sum]
     rw [integral_fintype_prod_volume_eq_pow fun x : ℂ => Real.exp (- ‖x‖ ^ p),
diff --git a/Mathlib/NumberTheory/Bertrand.lean b/Mathlib/NumberTheory/Bertrand.lean
index 89e05cf1c9edb1..25029ababf90aa 100644
--- a/Mathlib/NumberTheory/Bertrand.lean
+++ b/Mathlib/NumberTheory/Bertrand.lean
@@ -174,7 +174,7 @@ theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_large : 2 < n)
   rw [centralBinom_factorization_small n n_large no_prime, ← this, ←
     Finset.prod_filter_mul_prod_filter_not S (· ≤ sqrt (2 * n))]
   apply mul_le_mul'
-  · refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_
+  · refine (Finset.prod_le_prod fun p _ => (?_ : f p ≤ 2 * n)).trans ?_
     · exact pow_factorization_choose_le (mul_pos two_pos n_pos)
     have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by rw [card_Icc, Nat.add_sub_cancel]
     rw [Finset.prod_const]
@@ -182,11 +182,11 @@ theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_large : 2 < n)
     obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx
     exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, h2⟩
   · refine le_trans ?_ (primorial_le_four_pow (2 * n / 3))
-    refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_
+    refine (Finset.prod_le_prod fun p hp => (?_ : f p ≤ p)).trans ?_
     · obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp
       refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le
       exact Nat.factorization_choose_le_one (sqrt_lt'.mp <| not_le.1 h2)
-    refine Finset.prod_le_prod_of_subset_of_one_le' (Finset.filter_subset _ _) ?_
+    refine Finset.prod_le_prod_of_subset_of_one_le (Finset.filter_subset _ _) ?_
     exact fun p hp _ => (Finset.mem_filter.1 hp).2.one_lt.le
 
 namespace Nat
diff --git a/Mathlib/NumberTheory/Height/Basic.lean b/Mathlib/NumberTheory/Height/Basic.lean
index e5bdeb555ef6a8..4d740258a94fcf 100644
--- a/Mathlib/NumberTheory/Height/Basic.lean
+++ b/Mathlib/NumberTheory/Height/Basic.lean
@@ -382,7 +382,7 @@ lemma mulHeight_comp_le (f : ι → ι') (x : ι' → K) :
   · exact Multiset.prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _
   · exact Multiset.prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _)
       fun v _ ↦ H v
-  · exact finprod_le_finprod (hasFiniteMulSupport_iSup_nonarchAbsVal h₀)
+  · exact finprod_le_finprod₀ (hasFiniteMulSupport_iSup_nonarchAbsVal h₀)
       (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _)
       (hasFiniteMulSupport_iSup_nonarchAbsVal hx) fun v ↦ H v.val
 
@@ -834,7 +834,7 @@ lemma max_abv_sum_one_le [CharZero S] (v : AbsoluteValue R S) {ι : Type*} {s :
   · nth_rewrite 1 [← mul_one 1]
     gcongr
     · simp [hs]
-    · exact s.one_le_prod fun _ _ ↦ le_max_right ..
+    · exact s.one_le_prod₀ fun _ _ ↦ le_max_right ..
 
 /-- The "local" version of the height bound for arbitrary sums for nonarchimedean
 absolute values. -/
@@ -843,7 +843,7 @@ lemma max_abv_sum_one_le_of_isNonarchimedean {v : AbsoluteValue R S} (hv : IsNon
     max (v (∑ i ∈ s, x i)) 1 ≤ ∏ i ∈ s, max (v (x i)) 1 := by
   rcases s.eq_empty_or_nonempty with rfl | hs
   · simp
-  refine sup_le ?_ <| s.one_le_prod fun _ _ ↦ le_max_right ..
+  refine sup_le ?_ <| s.one_le_prod₀ fun _ _ ↦ le_max_right ..
   grw [hv.apply_sum_le_sup hs]
   exact sup'_le hs (fun i ↦ v (x i)) fun i hi ↦ le_prod_max_one hi fun i ↦ v (x i)
 
@@ -869,7 +869,7 @@ lemma mulHeight₁_sum_le {α : Type*} {s : Finset α} (hs : s.Nonempty) (x : α
   · exact finprod_nonneg fun _ ↦ by positivity
   · exact prod_map_nonneg fun _ h ↦ by positivity
   · exact prod_map_le_prod_map₀ _ _ (fun _ _ ↦ by positivity) fun _ _ ↦ max_abv_sum_one_le _ hs x
-  · exact finprod_le_finprod (by fun_prop) (fun _ ↦ by grind) (by fun_prop) <|
+  · exact finprod_le_finprod₀ (by fun_prop) (fun _ ↦ by grind) (by fun_prop) <|
       fun v ↦ max_abv_sum_one_le_of_isNonarchimedean (isNonarchimedean _ v.prop) _ x
 
 open Finset in
diff --git a/Mathlib/NumberTheory/Height/MvPolynomial.lean b/Mathlib/NumberTheory/Height/MvPolynomial.lean
index 3d515c98aa5365..9411b468dff2f4 100644
--- a/Mathlib/NumberTheory/Height/MvPolynomial.lean
+++ b/Mathlib/NumberTheory/Height/MvPolynomial.lean
@@ -148,7 +148,7 @@ theorem mulHeight_linearMap_apply_le [Nonempty ι] (A : ι' × ι → K) (x : ι
     exact v.iSup_abv_linearMap_apply_le A x
   · -- nonarchimedean part: reduce to "local" statement `linearMap_apply_bound_of_isNonarchimedean`
     rw [← finprod_mul_distrib (by fun_prop) (by fun_prop)]
-    refine finprod_le_finprod (by fun_prop)
+    refine finprod_le_finprod₀ (by fun_prop)
       (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _) (by fun_prop) fun v ↦ ?_
     exact (isNonarchimedean _ v.prop).iSup_abv_linearMap_apply_le A x
 
@@ -278,7 +278,7 @@ private lemma mulHeight_constantCoeff_le_mulHeightBound {p : ι' → MvPolynomia
     exact prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..)
       fun v _ ↦ Finite.ciSup_mono (H v)
   · have := (Function.ne_iff.mp h).nonempty
-    refine finprod_le_finprod (by fun_prop)
+    refine finprod_le_finprod₀ (by fun_prop)
       (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) ?_
     refine fun v ↦ Finite.ciSup_mono fun j ↦ ?_
     rw [show constantCoeff (p j) = coeff 0 (p j) from rfl]
@@ -337,7 +337,7 @@ theorem mulHeight_eval_le {N : ℕ} {p : ι' → MvPolynomial ι K} (hp : ∀ i,
     have := (Function.ne_iff.mp h₀).nonempty
     have F := hasFiniteMulSupport_iSup_nonarchAbsVal hx
     rw [finprod_pow F, ← finprod_mul_distrib (by fun_prop) (by fun_prop)]
-    refine finprod_le_finprod (by fun_prop)
+    refine finprod_le_finprod₀ (by fun_prop)
       (fun _ ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) fun v ↦ Real.iSup_le
       (fun j ↦ ?_) ?_
     · grw [(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x]
diff --git a/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean b/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
index 1f0acba649f289..68b39844dc21f5 100644
--- a/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
+++ b/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
@@ -383,7 +383,7 @@ theorem one_le_of_lt_one {w : InfinitePlace K} {a : (𝓞 K)} (ha : a ≠ 0)
   suffices (1 : ℝ) ≤ |Algebra.norm ℚ (a : K)| by
     contrapose! this
     rw [← InfinitePlace.prod_eq_abs_norm, ← Finset.prod_const_one]
-    refine Finset.prod_lt_prod_of_nonempty (fun _ _ ↦ ?_) (fun z _ ↦ ?_) Finset.univ_nonempty
+    refine Finset.prod_lt_prod_of_nonempty₀ (fun _ _ ↦ ?_) (fun z _ ↦ ?_) Finset.univ_nonempty
     · exact pow_pos (pos_iff.mpr ((Subalgebra.coe_eq_zero _).not.mpr ha)) _
     · refine pow_lt_one₀ (apply_nonneg _ _) ?_ (by rw [mult]; split_ifs <;> norm_num)
       by_cases hz : z = w
diff --git a/Mathlib/NumberTheory/Primorial.lean b/Mathlib/NumberTheory/Primorial.lean
index 147e83d499d4d4..b4678dfff72284 100644
--- a/Mathlib/NumberTheory/Primorial.lean
+++ b/Mathlib/NumberTheory/Primorial.lean
@@ -59,7 +59,7 @@ theorem primorial_pos (n : ℕ) : 0 < n# :=
 lemma primorial_ne_zero (n : ℕ) : n# ≠ 0 := (primorial_pos n).ne'
 
 theorem primorial_mono {m n : ℕ} (h : m ≤ n) : m# ≤ n# :=
-  prod_le_prod_of_subset_of_one_le' (by gcongr) (by grind)
+  prod_le_prod_of_subset_of_one_le (by gcongr) (by grind)
 
 theorem primorial_monotone : Monotone primorial := fun _ _ ↦ primorial_mono
 
@@ -106,7 +106,7 @@ lemma Squarefree.dvd_primorial {n : ℕ} (hn : Squarefree n) : n ∣ n# := by
   rwa [Nat.prod_primeFactors_of_squarefree hn] at this
 
 lemma lt_primorial_self {n : ℕ} (hn : 2 < n) : n < n# := by
-  have : 3 ≤ n# := single_le_prod' (f := id) (by grind [→ Prime.pos]) (by grind [prime_three])
+  have : 3 ≤ n# := single_le_prod (f := id) (by grind [→ Prime.pos]) (by grind [prime_three])
   let q := (n# - 1).minFac
   have : n < q := by
     by_contra! h1
diff --git a/Mathlib/NumberTheory/SelbergSieve.lean b/Mathlib/NumberTheory/SelbergSieve.lean
index af6311cc74e0c1..f3607da11f1b86 100644
--- a/Mathlib/NumberTheory/SelbergSieve.lean
+++ b/Mathlib/NumberTheory/SelbergSieve.lean
@@ -147,7 +147,7 @@ theorem nu_lt_one_of_dvd_prodPrimes {d : ℕ} (hdP : d ∣ s.prodPrimes) (hd_ne_
   calc
     s.nu d = ∏ p ∈ d.primeFactors, s.nu p := (prod_primeFactors_nu hdP).symm
     _ < ∏ p ∈ d.primeFactors, 1 := by
-      apply prod_lt_prod_of_nonempty
+      apply prod_lt_prod_of_nonempty₀
       · intro p hp
         simp only [mem_primeFactors] at hp
         apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)
diff --git a/Mathlib/NumberTheory/SiegelsLemma.lean b/Mathlib/NumberTheory/SiegelsLemma.lean
index 4e9706dd6411e9..edc018936dcb9e 100644
--- a/Mathlib/NumberTheory/SiegelsLemma.lean
+++ b/Mathlib/NumberTheory/SiegelsLemma.lean
@@ -146,7 +146,7 @@ private lemma card_S_lt_card_T [DecidableEq α] [DecidableEq β]
   calc
   ∏ x : α, (∑ x_1 : β, ↑B * ↑(A x x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A x x_1)⁻ + 1)
     ≤ ∏ x : α, (n * max 1 ‖A‖ * B + 1) := by
-      refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)
+      refine Finset.prod_le_prod₀ (fun i _ ↦ ?_) (fun i _ ↦ ?_)
       · have h := N_le_P_add_one A i
         rify at h
         linarith only [h]
diff --git a/Mathlib/NumberTheory/SmoothNumbers.lean b/Mathlib/NumberTheory/SmoothNumbers.lean
index 3ba37f37cc32d1..d39b12fb158a7a 100644
--- a/Mathlib/NumberTheory/SmoothNumbers.lean
+++ b/Mathlib/NumberTheory/SmoothNumbers.lean
@@ -445,7 +445,7 @@ lemma smoothNumbersUpTo_subset_image (N k : ℕ) :
     refine LE.le.trans ?_ (hm ▸ hn₁)
     nth_rw 1 [← mul_one (m ^ 2)]
     gcongr
-    exact Finset.one_le_prod' fun p hp ↦
+    exact Finset.one_le_prod fun p hp ↦
       (prime_of_mem_primesBelow <| Finset.mem_powerset.mp hs hp).one_le
 
 /-- The cardinality of the set of `k`-smooth numbers `≤ N` is bounded by `2^π(k-1) * √N`. -/
diff --git a/Mathlib/Probability/ProductMeasure.lean b/Mathlib/Probability/ProductMeasure.lean
index fd74a8110084c3..78211d60e26a26 100644
--- a/Mathlib/Probability/ProductMeasure.lean
+++ b/Mathlib/Probability/ProductMeasure.lean
@@ -445,7 +445,7 @@ lemma infinitePi_pi_of_countable {s : Set ι} (hs : Countable s) {t : (i : ι) 
       simpa using Set.pi_mono' (by simp) (Set.image_mono h)
     · exact ⟨{Nonempty.some s_ne}, by simp⟩
   · rw [ENNReal.tprod_eq_iInf_prod (by simp [prob_le_one])]
-    exact tendsto_atTop_iInf (prod_anti_set_of_le_one' (by simp [prob_le_one]))
+    exact tendsto_atTop_iInf (prod_anti_set_of_le_one (by simp [prob_le_one]))
 
 lemma infinitePi_pi_univ [Countable ι] {t : (i : ι) → Set (X i)}
     (mt : ∀ i : ι, MeasurableSet (t i)) :
diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
index 8171fbd7afb2de..5037acb51c9d82 100644
--- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
+++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
@@ -202,7 +202,7 @@ theorem sub_one_pow_totient_lt_cyclotomic_eval {n : ℕ} {q : ℝ} (hn' : 2 ≤
     simp [cyclotomic_nonneg n hq'.le]
   simp only [cyclotomic_eq_prod_X_sub_primitiveRoots hζ, eval_prod, eval_C, eval_X, eval_sub,
     nnnorm_prod, Units.mk0_prod]
-  convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
+  convert! Finset.prod_lt_prod (M := NNRealˣ) _ _
   swap; · exact fun _ => Units.mk0 (Real.toNNReal (q - 1)) (by simp [hq'])
   · simp only [Complex.card_primitiveRoots, prod_const, card_attach]
   · simp only [Finset.mem_attach, forall_true_left, Subtype.forall, ←
@@ -269,7 +269,7 @@ theorem cyclotomic_eval_lt_add_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤
     linarith
   simp only [cyclotomic_eq_prod_X_sub_primitiveRoots hζ, eval_prod, eval_C, eval_X, eval_sub,
     nnnorm_prod, Units.mk0_prod]
-  convert! Finset.prod_lt_prod' (M := NNRealˣ) _ _
+  convert! Finset.prod_lt_prod (M := NNRealˣ) _ _
   swap; · exact fun _ => Units.mk0 (Real.toNNReal (q + 1)) (by positivity)
   · simp [Complex.card_primitiveRoots]
   · simp only [Finset.mem_attach, forall_true_left, Subtype.forall, ←
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean b/Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean
index 4ec7ec8c950bd5..c2ad22c5bacc84 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean
@@ -573,7 +573,7 @@ theorem ENNReal.multipliable_of_le_one {f : α → ℝ≥0∞} (h₀ : ∀ i, f
 
 theorem ENNReal.hasProd_iInf_prod {f : α → ℝ≥0∞} (h₀ : ∀ i, f i ≤ 1) :
     HasProd f (⨅ s : Finset α, ∏ i ∈ s, f i) :=
-  tendsto_atTop_iInf (Finset.prod_anti_set_of_le_one' h₀)
+  tendsto_atTop_iInf (Finset.prod_anti_set_of_le_one h₀)
 
 theorem ENNReal.tprod_eq_iInf_prod {f : α → ℝ≥0∞} (h₀ : ∀ i, f i ≤ 1) :
     ∏' i, f i = ⨅ s : Finset α, ∏ i ∈ s, f i :=
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean
index d625839ecea1e3..c0831c1df45281 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean
@@ -53,7 +53,7 @@ variable [CommMonoid α] [Preorder α] [IsOrderedMonoid α]
 @[to_additive]
 theorem hasProd_le (h : ∀ i, f i ≤ g i) (hf : HasProd f a₁ L) (hg : HasProd g a₂ L) [L.NeBot] :
     a₁ ≤ a₂ :=
-  le_of_tendsto_of_tendsto' hf hg fun _ ↦ prod_le_prod' fun i _ ↦ h i
+  le_of_tendsto_of_tendsto' hf hg fun _ ↦ prod_le_prod fun i _ ↦ h i
 
 @[to_additive]
 theorem hasProd_mono (hf : HasProd f a₁ L) (hg : HasProd g a₂ L) (h : f ≤ g) [L.NeBot] : a₁ ≤ a₂ :=
@@ -93,12 +93,12 @@ protected lemma Multipliable.tprod_subtype_le {κ γ : Type*} [CommGroup γ] [Pa
 theorem prod_le_hasProd [L.NeBot] [L.LeAtTop] (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i)
     (hf : HasProd f a L) : ∏ i ∈ s, f i ≤ a := by
   refine ge_of_tendsto hf <| .filter_mono L.le_atTop <| eventually_atTop.2 ?_
-  exact ⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le' hst fun i _ hbs ↦ hs i hbs⟩
+  exact ⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le hst fun i _ hbs ↦ hs i hbs⟩
 
 @[to_additive]
 theorem isLUB_hasProd (h : ∀ i, 1 ≤ f i) (hf : HasProd f a) :
-    IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a := by
-  exact isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf
+    IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a :=
+  isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le h) hf
 
 @[to_additive]
 theorem le_hasProd [L.NeBot] [L.LeAtTop] (hf : HasProd f a L) (i : ι) (hb : ∀ j, j ≠ i → 1 ≤ f j) :
@@ -264,8 +264,8 @@ protected theorem Multipliable.tprod_ne_one_iff (hf : Multipliable f) :
 
 omit [IsOrderedMonoid α] in
 @[to_additive]
-theorem isLUB_hasProd' (hf : HasProd f a) : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a := by
-  exact isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf
+theorem isLUB_hasProd' (hf : HasProd f a) : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a :=
+  isLUB_of_tendsto_atTop (Finset.prod_mono_set f) hf
 
 end CanonicallyOrderedMul
 
@@ -285,21 +285,21 @@ theorem hasProd_of_isLUB_of_one_le [CommMonoid α] [LinearOrder α] [IsOrderedMo
     [TopologicalSpace α]
     [OrderTopology α] {f : ι → α} (i : α) (h : ∀ i, 1 ≤ f i)
     (hf : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) i) : HasProd f i :=
-  tendsto_atTop_isLUB (Finset.prod_mono_set_of_one_le' h) hf
+  tendsto_atTop_isLUB (Finset.prod_mono_set_of_one_le h) hf
 
 @[to_additive]
 theorem hasProd_of_isGLB_of_le_one [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α]
     [TopologicalSpace α]
     [OrderTopology α] {f : ι → α} (i : α) (h₀ : ∀ i, f i ≤ 1)
     (hf : IsGLB (Set.range fun s ↦ ∏ i ∈ s, f i) i) : HasProd f i :=
-  tendsto_atTop_isGLB (Finset.prod_anti_set_of_le_one' h₀) hf
+  tendsto_atTop_isGLB (Finset.prod_anti_set_of_le_one h₀) hf
 
 @[to_additive]
 theorem hasProd_of_isLUB [CommMonoid α] [LinearOrder α]
     [CanonicallyOrderedMul α] [TopologicalSpace α]
     [OrderTopology α] {f : ι → α} (b : α) (hf : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) b) :
     HasProd f b :=
-  tendsto_atTop_isLUB (Finset.prod_mono_set' f) hf
+  tendsto_atTop_isLUB (Finset.prod_mono_set f) hf
 
 @[to_additive]
 theorem multipliable_mabs_iff [CommGroup α] [LinearOrder α] [IsOrderedMonoid α]