diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 950851505919..e1c7cb865863 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1792,7 +1792,7 @@ theorem setWidth_succ (x : BitVec w) :
     · simp_all
     · omega
 
-@[deprecated "Use the reverse direction of `cons_msb_setWidth`"]
+@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")]
 theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
   simp
 
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index d9da88e596f3..f1ee950b88b1 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -643,11 +643,11 @@ theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop)
     (@ite _ p h q (decide p)) = (decide p && q) := by
   split <;> simp_all
 
-@[deprecated ite_then_decide_self]
+@[deprecated ite_then_decide_self (since := "2024-08-29")]
 theorem ite_true_decide_same (p : Prop) [Decidable p] (b : Bool) :
   (if p then decide p else b) = (decide p || b) := ite_then_decide_self p b
 
-@[deprecated ite_false_decide_same]
+@[deprecated ite_false_decide_same (since := "2024-08-29")]
 theorem ite_false_decide_same (p : Prop) [Decidable p] (b : Bool) :
   (if p then b else decide p) = (decide p && b) := ite_else_decide_self p b
 
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index a8f975a98979..8899cb734665 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -271,11 +271,11 @@ def ofListWith (l : List (α × β)) (f : β → β → β) : HashMap α β :=
         | none   => m.insert p.fst p.snd
         | some v => m.insert p.fst $ f v p.snd)
 
-attribute [deprecated Std.HashMap] HashMap
-attribute [deprecated Std.HashMap.Raw] HashMapImp
-attribute [deprecated Std.HashMap.Raw.empty] mkHashMapImp
-attribute [deprecated Std.HashMap.empty] mkHashMap
-attribute [deprecated Std.HashMap.empty] HashMap.empty
-attribute [deprecated Std.HashMap.ofList] HashMap.ofList
+attribute [deprecated Std.HashMap (since := "2024-08-08")] HashMap
+attribute [deprecated Std.HashMap.Raw (since := "2024-08-08")] HashMapImp
+attribute [deprecated Std.HashMap.Raw.empty (since := "2024-08-08")] mkHashMapImp
+attribute [deprecated Std.HashMap.empty (since := "2024-08-08")] mkHashMap
+attribute [deprecated Std.HashMap.empty (since := "2024-08-08")] HashMap.empty
+attribute [deprecated Std.HashMap.ofList (since := "2024-08-08")] HashMap.ofList
 
 end Lean.HashMap
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
index b7dc0cc09477..795566a3b5c7 100644
--- a/src/Lean/Data/HashSet.lean
+++ b/src/Lean/Data/HashSet.lean
@@ -219,8 +219,8 @@ def merge {α : Type u} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α :
   t.fold (init := s) fun s a => s.insert a
   -- We don't use `insertMany` here because it gives weird universes.
 
-attribute [deprecated Std.HashSet] HashSet
-attribute [deprecated Std.HashSet.Raw] HashSetImp
-attribute [deprecated Std.HashSet.Raw.empty] mkHashSetImp
-attribute [deprecated Std.HashSet.empty] mkHashSet
-attribute [deprecated Std.HashSet.empty] HashSet.empty
+attribute [deprecated Std.HashSet (since := "2024-08-08")] HashSet
+attribute [deprecated Std.HashSet.Raw (since := "2024-08-08")] HashSetImp
+attribute [deprecated Std.HashSet.Raw.empty (since := "2024-08-08")] mkHashSetImp
+attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] mkHashSet
+attribute [deprecated Std.HashSet.empty (since := "2024-08-08")] HashSet.empty
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index a292033c17e1..225424a5f3cd 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -254,7 +254,7 @@ Apply `And.intro` as much as possible to goal `mvarId`.
 abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   splitAndCore mvarId
 
-@[deprecated splitAnd] -- 2024-03-17
+@[deprecated splitAnd (since := "2024-03-17")]
 def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   mvarId.splitAnd
 
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index 4a9afb333547..59fa81b39534 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -118,7 +118,7 @@ Tries to retrieve the mapping for the given key, returning `none` if no such map
 @[inline] def get? (m : HashMap α β) (a : α) : Option β :=
   DHashMap.Const.get? m.inner a
 
-@[deprecated get? "Use `m[a]?` or `m.get? a` instead", inherit_doc get?]
+@[deprecated get? "Use `m[a]?` or `m.get? a` instead" (since := "2024-08-07"), inherit_doc get?]
 def find? (m : HashMap α β) (a : α) : Option β :=
   m.get? a
 
@@ -145,7 +145,7 @@ Retrieves the mapping for the given key. Ensures that such a mapping exists by r
     (fallback : β) : β :=
   DHashMap.Const.getD m.inner a fallback
 
-@[deprecated getD, inherit_doc getD]
+@[deprecated getD (since := "2024-08-07"), inherit_doc getD]
 def findD (m : HashMap α β) (a : α) (fallback : β) : β :=
   m.getD a fallback
 
@@ -157,7 +157,7 @@ Tries to retrieve the mapping for the given key, panicking if no such mapping is
 @[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β :=
   DHashMap.Const.get! m.inner a
 
-@[deprecated get! "Use `m[a]!` or `m.get! a` instead", inherit_doc get!]
+@[deprecated get! "Use `m[a]!` or `m.get! a` instead" (since := "2024-08-07"), inherit_doc get!]
 def find! [Inhabited β] (m : HashMap α β) (a : α) : Option β :=
   m.get! a