deprecated aliases

Author: YaelDillies

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -608,6 +608,8 @@ lemma finprod_le_finprod [PartialOrder M] [MulLeftMono M] (hf : HasFiniteMulSupp
     finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]
   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
 `M` is an ordered `CommMonoid`. -/
 lemma finprod_le_finprod₀ {M : Type*} [CommMonoidWithZero M] [PartialOrder M] [ZeroLEOneClass M]

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

@@ -109,6 +109,8 @@ equal to the corresponding factor `g i` of another finite product, then
 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
@@ -120,6 +122,8 @@ add_decl_doc sum_le_sum
 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 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
@@ -131,6 +135,8 @@ attribute [deprecated one_le_prod (since := "2026-05-22")] one_le_prod''
 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_prod_of_subset_of_one_le' := prod_le_one
+
 @[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
@@ -145,21 +151,31 @@ lemma prod_le_prod_of_subset_of_le_one [MulLeftMono N] (h : s ⊆ t) (hf : ∀ i
     ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i :=
   prod_le_prod_of_subset_of_one_le (N := Nᵒᵈ) h hf
 
+@[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
 
+@[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 [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])
 
+@[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
 
+@[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] :
@@ -172,6 +188,8 @@ theorem prod_eq_one_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N]
     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) :
@@ -186,6 +204,8 @@ theorem prod_eq_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid 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ᵒᵈ)
 
+@[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]
     {f : ι → N} {s : Finset ι} [MulLeftMono N] (hf : ∀ x ∈ s, f x ≤ 1) :
@@ -200,6 +220,8 @@ theorem single_le_prod [MulLeftMono N] (hf : ∀ i ∈ s, 1 ≤ f i) {a} (h : a
     _ ≤ ∏ i ∈ s, f i :=
       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)
     (hne : i ≠ j) :
@@ -238,12 +260,18 @@ theorem prod_fiberwise_le_prod_of_one_le_prod_fiber [MulLeftMono N] {t : Finset
     _ = ∏ x ∈ s, f x :=
       prod_fiberwise_of_maps_to (fun _ hx ↦ mem_union.2 <| Or.inr <| mem_image_of_mem _ hx) _
 
+@[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
 
+@[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) :
@@ -421,11 +449,15 @@ theorem prod_le_prod_of_subset (h : s ⊆ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t,
   have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
   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]
 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
 
+@[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
@@ -439,6 +471,8 @@ theorem prod_le_prod_of_ne_one (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) :
         (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]
     {f : ι → M} {s : Finset ι} : 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x :=
@@ -456,6 +490,8 @@ theorem prod_lt_prod [MulLeftStrictMono M] (hle : ∀ i ∈ s, f i ≤ g i) (hlt
     ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
   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`. -/
@@ -465,6 +501,8 @@ theorem prod_lt_prod_of_nonempty [MulLeftStrictMono M] (hs : s.Nonempty)
     ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
   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`. -/
@@ -485,6 +523,8 @@ theorem prod_lt_prod_of_subset [MulLeftStrictMono M] (h : s ⊆ t) {i : ι} (ht
         simp only [mem_insert, not_or] at h'x
         exact hle x hx h'x.2
 
+@[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 :=
@@ -494,6 +534,8 @@ theorem single_lt_prod [MulLeftStrictMono M] {i j : ι} (hij : j ≠ i) (hi : i
       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 :=
@@ -553,6 +595,8 @@ theorem exists_lt_of_prod_lt [MulLeftMono M] (Hlt : ∏ i ∈ s, f i < ∏ i ∈
   contrapose! Hlt with 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]
@@ -561,6 +605,8 @@ theorem exists_le_of_prod_le (hs : s.Nonempty) (Hle : ∏ i ∈ s, f i ≤ ∏ i
   contrapose! Hle with 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)
     (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, 1 < f i := by
@@ -571,6 +617,9 @@ theorem exists_one_lt_of_prod_one_of_exists_ne_one (f : ι → M) (h₁ : ∏ i
     ∏ 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 α]
@@ -610,6 +659,8 @@ variable [Fintype ι] [CommMonoid M] [Preorder M] [MulLeftMono M] {f : ι → M}
 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 _
 
@@ -636,6 +687,8 @@ theorem prod_strictMono : StrictMono fun f : ι → M ↦ ∏ x, f x :=
   let ⟨hle, i, hlt⟩ := Pi.lt_def.mp hfg
   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 :=
   Finset.one_lt_prod' (fun _ _ ↦ hf.le _) <| by simpa using (Pi.lt_def.1 hf).2

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

@@ -32,6 +32,8 @@ lemma Forall₂.prod_le_prod [Preorder M] [MulRightMono M]
   | 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`. -/
@@ -51,6 +53,8 @@ lemma Sublist.prod_le_prod [Preorder M] [MulRightMono M]
     simp only [prod_cons, forall_mem_cons] at h₁ ⊢
     grw [ih h₁.2]
 
+@[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]
@@ -59,12 +63,17 @@ lemma SublistForall₂.prod_le_prod [Preorder M]
   let ⟨_, hall, hsub⟩ := sublistForall₂_iff.1 h
   hall.prod_le_prod.trans <| hsub.prod_le_prod h₁
 
+@[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
 
+@[deprecated (since := "2026-05-22")] alias prod_le_prod' := prod_le_prod
+
 @[to_additive]
 lemma prod_lt_prod [Preorder M] [MulLeftStrictMono M]
     [MulLeftMono M] [MulRightStrictMono M]
@@ -79,6 +88,8 @@ lemma prod_lt_prod [Preorder M] [MulLeftStrictMono M]
     · 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]
@@ -106,6 +117,8 @@ lemma exists_lt_of_prod_lt [LinearOrder M] [MulRightMono M]
   contrapose! h
   exact prod_le_prod h
 
+@[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]
@@ -114,6 +127,8 @@ lemma exists_le_of_prod_le [LinearOrder M] [MulLeftStrictMono M]
   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

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

@@ -125,12 +125,16 @@ lemma prod_lt_prod (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g
   simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
   exact List.prod_lt_prod f g hle hlt
 
+@[deprecated (since := "2026-05-22")] alias prod_lt_prod' := prod_lt_prod
+
 @[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⟩
 
+@[deprecated (since := "2026-05-22")] alias prod_lt_prod_of_nonempty' := prod_lt_prod_of_nonempty
+
 end OrderedCancelCommMonoid
 
 section CanonicallyOrderedMul