chore(*): more since := in deprecated (#13723)

Author: urkud

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -202,9 +202,8 @@ protected theorem intCast_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [A
   intCast_mem S n
 #align subalgebra.coe_int_mem Subalgebra.intCast_mem
 
--- 2024-04-05
-@[deprecated natCast_mem] alias coe_nat_mem := Subalgebra.natCast_mem
-@[deprecated intCast_mem] alias coe_int_mem := Subalgebra.intCast_mem
+@[deprecated natCast_mem (since := "2024-04-05")] alias coe_nat_mem := Subalgebra.natCast_mem
+@[deprecated intCast_mem (since := "2024-04-05")] alias coe_int_mem := Subalgebra.intCast_mem
 
 /-- The projection from a subalgebra of `A` to an additive submonoid of `A`. -/
 def toAddSubmonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A]

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -859,7 +859,7 @@ lemma unop_map_list_prod {F : Type*} [FunLike F M Nᵐᵒᵖ] [MonoidHomClass F
 namespace MonoidHom
 
 /-- A morphism into the opposite monoid acts on the product by acting on the reversed elements. -/
-@[deprecated _root_.unop_map_list_prod]
+@[deprecated _root_.unop_map_list_prod (since := "2023-01-10")]
 protected theorem unop_map_list_prod (f : M →* Nᵐᵒᵖ) (l : List M) :
     (f l.prod).unop = (l.map (MulOpposite.unop ∘ f)).reverse.prod :=
   unop_map_list_prod f l

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -579,9 +579,4 @@ noncomputable def commGroupWithZeroOfIsUnitOrEqZero [hM : CommMonoidWithZero M]
 
 end NoncomputableDefs
 
--- 2024-03-20
--- The names `div_mul_cancel`, `mul_div_cancel` and `mul_div_cancel_left` have been reused
--- @[deprecated] alias div_mul_cancel := div_mul_cancel₀
--- @[deprecated] alias mul_div_cancel := mul_div_cancel_right₀
--- @[deprecated] alias mul_div_cancel_left := mul_div_cancel_left₀
-@[deprecated] alias mul_div_cancel' := mul_div_cancel₀
+@[deprecated (since := "2024-03-20")] alias mul_div_cancel' := mul_div_cancel₀

Mathlib/Algebra/Module/Defs.lean

@@ -105,7 +105,7 @@ theorem two_smul : (2 : R) • x = x + x := by rw [← one_add_one_eq_two, add_s
 #align two_smul two_smul
 
 set_option linter.deprecated false in
-@[deprecated]
+@[deprecated (since := "2022-12-31")]
 theorem two_smul' : (2 : R) • x = bit0 x :=
   two_smul R x
 #align two_smul' two_smul'

Mathlib/Algebra/Order/Field/Basic.lean

@@ -293,11 +293,10 @@ lemma div_lt_div_of_pos_left (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a /
   simpa only [div_eq_mul_inv, mul_lt_mul_left ha, inv_lt_inv (hc.trans h) hc]
 #align div_lt_div_of_lt_left div_lt_div_of_pos_left
 
--- 2024-02-16
-@[deprecated] alias div_le_div_of_le_of_nonneg := div_le_div_of_nonneg_right
-@[deprecated] alias div_lt_div_of_lt := div_lt_div_of_pos_right
-@[deprecated] alias div_le_div_of_le_left := div_le_div_of_nonneg_left
-@[deprecated] alias div_lt_div_of_lt_left := div_lt_div_of_pos_left
+@[deprecated (since := "2024-02-16")] alias div_le_div_of_le_of_nonneg := div_le_div_of_nonneg_right
+@[deprecated (since := "2024-02-16")] alias div_lt_div_of_lt := div_lt_div_of_pos_right
+@[deprecated (since := "2024-02-16")] alias div_le_div_of_le_left := div_le_div_of_nonneg_left
+@[deprecated (since := "2024-02-16")] alias div_lt_div_of_lt_left := div_lt_div_of_pos_left
 
 @[deprecated div_le_div_of_nonneg_right (since := "2024-02-16")]
 lemma div_le_div_of_le (hc : 0 ≤ c) (hab : a ≤ b) : a / c ≤ b / c :=

Mathlib/Algebra/Order/Floor.lean

@@ -1741,11 +1741,14 @@ theorem natCast_ceil_eq_intCast_ceil  (ha : 0 ≤ a) : (⌈a⌉₊ : α) = ⌈a
   rw [← Int.ofNat_ceil_eq_ceil ha, Int.cast_natCast]
 #align nat.cast_ceil_eq_cast_int_ceil natCast_ceil_eq_intCast_ceil
 
--- 2024-02-14
-@[deprecated] alias Nat.cast_floor_eq_int_floor := Int.ofNat_floor_eq_floor
-@[deprecated] alias Nat.cast_ceil_eq_int_ceil := Int.ofNat_ceil_eq_ceil
-@[deprecated] alias Nat.cast_floor_eq_cast_int_floor := natCast_floor_eq_intCast_floor
-@[deprecated] alias Nat.cast_ceil_eq_cast_int_ceil := natCast_ceil_eq_intCast_ceil
+@[deprecated (since := "2024-02-14")] alias Nat.cast_floor_eq_int_floor := Int.ofNat_floor_eq_floor
+@[deprecated (since := "2024-02-14")] alias Nat.cast_ceil_eq_int_ceil := Int.ofNat_ceil_eq_ceil
+
+@[deprecated (since := "2024-02-14")]
+alias Nat.cast_floor_eq_cast_int_floor := natCast_floor_eq_intCast_floor
+
+@[deprecated (since := "2024-02-14")]
+alias Nat.cast_ceil_eq_cast_int_ceil := natCast_ceil_eq_intCast_ceil
 
 end FloorRingToSemiring
 

Mathlib/Algebra/Order/Monoid/Defs.lean

@@ -118,8 +118,8 @@ instance (priority := 100) OrderedCancelCommMonoid.toCancelCommMonoid : CancelCo
 end OrderedCancelCommMonoid
 
 set_option linter.deprecated false in
-@[deprecated] theorem bit0_pos [OrderedAddCommMonoid α] {a : α} (h : 0 < a) : 0 < bit0 a :=
-  add_pos' h h
+@[deprecated (since := "2022-11-28")]
+theorem bit0_pos [OrderedAddCommMonoid α] {a : α} (h : 0 < a) : 0 < bit0 a := add_pos' h h
 #align bit0_pos bit0_pos
 
 /-- A linearly ordered additive commutative monoid. -/

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

@@ -1695,12 +1695,12 @@ section Bit
 set_option linter.deprecated false
 variable [Add α] [Preorder α]
 
-@[deprecated]
+@[deprecated (since := "2022-11-20")]
 theorem bit0_mono [CovariantClass α α (· + ·) (· ≤ ·)] [CovariantClass α α (swap (· + ·)) (· ≤ ·)] :
     Monotone (bit0 : α → α) := fun _ _ h => add_le_add h h
 #align bit0_mono bit0_mono
 
-@[deprecated]
+@[deprecated (since := "2022-11-20")]
 theorem bit0_strictMono [CovariantClass α α (· + ·) (· < ·)]
     [CovariantClass α α (swap (· + ·)) (· < ·)] :
     StrictMono (bit0 : α → α) := fun _ _ h => add_lt_add h h

Mathlib/Algebra/Order/Monoid/WithTop.lean

@@ -369,10 +369,9 @@ instance addMonoidWithOne : AddMonoidWithOne (WithTop α) :=
 @[simp] lemma top_ne_natCast (n : ℕ) : (⊤ : WithTop α) ≠ n := top_ne_coe
 #align with_top.top_ne_nat WithTop.top_ne_natCast
 
--- 2024-04-05
-@[deprecated] alias coe_nat := coe_natCast
-@[deprecated] alias nat_ne_top := natCast_ne_top
-@[deprecated] alias top_ne_nat := top_ne_natCast
+@[deprecated (since := "2024-04-05")] alias coe_nat := coe_natCast
+@[deprecated (since := "2024-04-05")] alias nat_ne_top := natCast_ne_top
+@[deprecated (since := "2024-04-05")] alias top_ne_nat := top_ne_natCast
 
 end AddMonoidWithOne
 
@@ -570,10 +569,9 @@ instance addMonoidWithOne : AddMonoidWithOne (WithBot α) := WithTop.addMonoidWi
 @[simp] lemma bot_ne_natCast (n : ℕ) : (⊥ : WithBot α) ≠ n := bot_ne_coe
 #align with_bot.bot_ne_nat WithBot.bot_ne_natCast
 
--- 2024-04-05
-@[deprecated] alias coe_nat := coe_natCast
-@[deprecated] alias nat_ne_bot := natCast_ne_bot
-@[deprecated] alias bot_ne_nat := bot_ne_natCast
+@[deprecated (since := "2024-04-05")] alias coe_nat := coe_natCast
+@[deprecated (since := "2024-04-05")] alias nat_ne_bot := natCast_ne_bot
+@[deprecated (since := "2024-04-05")] alias bot_ne_nat := bot_ne_natCast
 
 end AddMonoidWithOne
 

Mathlib/Algebra/Order/Ring/Basic.lean

@@ -438,23 +438,29 @@ end LinearOrderedSemiring
 Those lemmas have been deprecated on 2023-12-23.
 -/
 
-@[deprecated] alias pow_mono := pow_right_mono
-@[deprecated] alias pow_le_pow := pow_le_pow_right
-@[deprecated] alias pow_le_pow_of_le_left := pow_le_pow_left
-@[deprecated] alias pow_lt_pow_of_lt_left := pow_lt_pow_left
-@[deprecated] alias strictMonoOn_pow := pow_left_strictMonoOn
-@[deprecated] alias pow_strictMono_right := pow_right_strictMono
-@[deprecated] alias pow_lt_pow := pow_lt_pow_right
-@[deprecated] alias pow_lt_pow_iff := pow_lt_pow_iff_right
-@[deprecated] alias pow_le_pow_iff := pow_le_pow_iff_right
-@[deprecated] alias self_lt_pow := lt_self_pow
-@[deprecated] alias strictAnti_pow := pow_right_strictAnti
-@[deprecated] alias pow_lt_pow_iff_of_lt_one := pow_lt_pow_iff_right_of_lt_one
-@[deprecated] alias pow_lt_pow_of_lt_one := pow_lt_pow_right_of_lt_one
-@[deprecated] alias lt_of_pow_lt_pow := lt_of_pow_lt_pow_left
-@[deprecated] alias le_of_pow_le_pow := le_of_pow_le_pow_left
-@[deprecated] alias self_le_pow := le_self_pow
-@[deprecated] alias Nat.pow_lt_pow_of_lt_right := pow_lt_pow_right
-@[deprecated] protected alias Nat.pow_right_strictMono := pow_right_strictMono
-@[deprecated] alias Nat.pow_le_iff_le_right := pow_le_pow_iff_right
-@[deprecated] alias Nat.pow_lt_iff_lt_right := pow_lt_pow_iff_right
+@[deprecated (since := "2023-12-23")] alias pow_mono := pow_right_mono
+@[deprecated (since := "2023-12-23")] alias pow_le_pow := pow_le_pow_right
+@[deprecated (since := "2023-12-23")] alias pow_le_pow_of_le_left := pow_le_pow_left
+@[deprecated (since := "2023-12-23")] alias pow_lt_pow_of_lt_left := pow_lt_pow_left
+@[deprecated (since := "2023-12-23")] alias strictMonoOn_pow := pow_left_strictMonoOn
+@[deprecated (since := "2023-12-23")] alias pow_strictMono_right := pow_right_strictMono
+@[deprecated (since := "2023-12-23")] alias pow_lt_pow := pow_lt_pow_right
+@[deprecated (since := "2023-12-23")] alias pow_lt_pow_iff := pow_lt_pow_iff_right
+@[deprecated (since := "2023-12-23")] alias pow_le_pow_iff := pow_le_pow_iff_right
+@[deprecated (since := "2023-12-23")] alias self_lt_pow := lt_self_pow
+@[deprecated (since := "2023-12-23")] alias strictAnti_pow := pow_right_strictAnti
+
+@[deprecated (since := "2023-12-23")]
+alias pow_lt_pow_iff_of_lt_one := pow_lt_pow_iff_right_of_lt_one
+
+@[deprecated (since := "2023-12-23")] alias pow_lt_pow_of_lt_one := pow_lt_pow_right_of_lt_one
+@[deprecated (since := "2023-12-23")] alias lt_of_pow_lt_pow := lt_of_pow_lt_pow_left
+@[deprecated (since := "2023-12-23")] alias le_of_pow_le_pow := le_of_pow_le_pow_left
+@[deprecated (since := "2023-12-23")] alias self_le_pow := le_self_pow
+@[deprecated (since := "2023-12-23")] alias Nat.pow_lt_pow_of_lt_right := pow_lt_pow_right
+
+@[deprecated (since := "2023-12-23")]
+protected alias Nat.pow_right_strictMono := pow_right_strictMono
+
+@[deprecated (since := "2023-12-23")] alias Nat.pow_le_iff_le_right := pow_le_pow_iff_right
+@[deprecated (since := "2023-12-23")] alias Nat.pow_lt_iff_lt_right := pow_lt_pow_iff_right