diff --git a/src/Init/ByCases.lean b/src/Init/ByCases.lean
index 1396f9e953..f7f2036aae 100644
--- a/src/Init/ByCases.lean
+++ b/src/Init/ByCases.lean
@@ -42,24 +42,3 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
 @[simp] theorem dite_eq_ite [Decidable P] :
   (dite P (fun _ => a) (fun _ => b)) = ite P a b := rfl
-
-@[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
-theorem ite_some_none_eq_none [Decidable P] :
-    (if P then some x else none) = none ↔ ¬ P := by
-  simp only [ite_eq_right_iff, reduceCtorEq]
-  rfl
-
-@[deprecated "Use `Option.ite_none_right_eq_some`" (since := "2024-09-18")]
-theorem ite_some_none_eq_some [Decidable P] :
-    (if P then some x else none) = some y ↔ P ∧ x = y := by
-  split <;> simp_all
-
-@[deprecated "Use `dite_eq_right_iff" (since := "2024-09-18")]
-theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
-    (if h : P then some (x h) else none) = none ↔ ¬P := by
-  simp
-
-@[deprecated "Use `Option.dite_none_right_eq_some`" (since := "2024-09-18")]
-theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
-    (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
-  by_cases h : P <;> simp [h]
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 5ccee289cc..da65d36191 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -2527,9 +2527,6 @@ class Antisymm (r : α → α → Prop) : Prop where
   /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
   antisymm (a b : α) : r a b → r b a → a = b
 
-@[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
-abbrev _root_.Antisymm (r : α → α → Prop) : Prop := Std.Antisymm r
-
 /-- `Asymm X r` means that the binary relation `r` on `X` is asymmetric, that is,
 `r a b → ¬ r b a`. -/
 class Asymm (r : α → α → Prop) : Prop where
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 9e640a8f36..6ee24f6a4e 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -36,8 +36,6 @@ variable {α : Type u}
 
 namespace Array
 
-@[deprecated toList (since := "2024-09-10")] abbrev data := @toList
-
 /-! ### Preliminary theorems -/
 
 @[simp, grind] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
@@ -148,8 +146,6 @@ namespace Array
 
 theorem size_eq_length_toList {xs : Array α} : xs.size = xs.toList.length := rfl
 
-@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @List.toList_toArray
-
 /-! ### Externs -/
 
 /--
@@ -1487,8 +1483,6 @@ The resulting arrays are appended.
 def flatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β) :=
   as.foldlM (init := empty) fun bs a => do return bs ++ (← f a)
 
-@[deprecated flatMapM (since := "2024-10-16")] abbrev concatMapM := @flatMapM
-
 /--
 Applies a function that returns an array to each element of an array. The resulting arrays are
 appended.
@@ -1501,8 +1495,6 @@ Examples:
 def flatMap (f : α → Array β) (as : Array α) : Array β :=
   as.foldl (init := empty) fun bs a => bs ++ f a
 
-@[deprecated flatMap (since := "2024-10-16")] abbrev concatMap := @flatMap
-
 /--
 Appends the contents of array of arrays into a single array. The resulting array contains the same
 elements as the nested arrays in the same order.
diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index 13574abf47..e3819ffacf 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -159,34 +159,4 @@ theorem foldl_eq_foldl_toList {f : β → α → β} {init : β} {xs : Array α}
     xs.foldl f init = xs.toList.foldl f init:= by
   simp
 
-@[deprecated foldlM_toList (since := "2024-09-09")]
-abbrev foldlM_eq_foldlM_data := @foldlM_toList
-
-@[deprecated foldl_toList (since := "2024-09-09")]
-abbrev foldl_eq_foldl_data := @foldl_toList
-
-@[deprecated foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]
-abbrev foldrM_eq_reverse_foldlM_data := @foldrM_eq_reverse_foldlM_toList
-
-@[deprecated foldrM_toList (since := "2024-09-09")]
-abbrev foldrM_eq_foldrM_data := @foldrM_toList
-
-@[deprecated foldr_toList (since := "2024-09-09")]
-abbrev foldr_eq_foldr_data := @foldr_toList
-
-@[deprecated push_toList (since := "2024-09-09")]
-abbrev push_data := @push_toList
-
-@[deprecated toListImpl_eq (since := "2024-09-09")]
-abbrev toList_eq := @toListImpl_eq
-
-@[deprecated pop_toList (since := "2024-09-09")]
-abbrev pop_data := @toList_pop
-
-@[deprecated toList_append (since := "2024-09-09")]
-abbrev append_data := @toList_append
-
-@[deprecated toList_appendList (since := "2024-09-09")]
-abbrev appendList_data := @toList_appendList
-
 end Array
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 1e24809b70..95fe9e559d 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -4704,11 +4704,6 @@ theorem get!_eq_getD_getElem? [Inhabited α] (xs : Array α) (i : Nat) :
 set_option linter.deprecated false in
 @[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_getElem? := @get!_eq_getD_getElem?
 
-
-@[deprecated mem_of_back? (since := "2024-10-21")] abbrev mem_of_back?_eq_some := @mem_of_back?
-
-@[deprecated getElem?_size_le (since := "2024-10-21")] abbrev get?_len_le := @getElem?_size_le
-
 set_option linter.deprecated false in
 @[deprecated "`Array.get?` is deprecated, use `a[i]?` instead." (since := "2025-02-12")]
 theorem get?_eq_get?_toList (xs : Array α) (i : Nat) : xs.get? i = xs.toList.get? i := by
@@ -4717,45 +4712,11 @@ theorem get?_eq_get?_toList (xs : Array α) (i : Nat) : xs.get? i = xs.toList.ge
 set_option linter.deprecated false in
 @[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_get? := @get!_eq_getD_getElem?
 
-@[deprecated getElem?_push_lt (since := "2024-10-21")] abbrev get?_push_lt := @getElem?_push_lt
-
-@[deprecated getElem?_push_eq (since := "2024-10-21")] abbrev get?_push_eq := @getElem?_push_eq
-
-@[deprecated getElem?_push (since := "2024-10-21")] abbrev get?_push := @getElem?_push
-
-@[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
-
 @[deprecated getElem_set_self (since := "2025-01-17")]
 theorem get_set_eq (xs : Array α) (i : Nat) (v : α) (h : i < xs.size) :
     (xs.set i v h)[i]'(by simp [h]) = v := by
   simp only [set, ← getElem_toList, List.getElem_set_self]
 
-@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
-abbrev foldl_toList_eq_bind := @foldl_toList_eq_flatMap
-
-@[deprecated foldl_toList_eq_flatMap (since := "2024-10-16")]
-abbrev foldl_data_eq_bind := @foldl_toList_eq_flatMap
-
-@[deprecated getElem_mem (since := "2024-10-17")]
-abbrev getElem?_mem := @getElem_mem
-
-@[deprecated getElem_fin_eq_getElem_toList (since := "2024-10-17")]
-abbrev getElem_fin_eq_toList_get := @getElem_fin_eq_getElem_toList
-
-@[deprecated "Use reverse direction of `getElem?_toList`" (since := "2024-10-17")]
-abbrev getElem?_eq_toList_getElem? := @getElem?_toList
-
-@[deprecated getElem?_swap (since := "2024-10-17")] abbrev get?_swap := @getElem?_swap
-
-@[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
-@[deprecated getElem_push_lt (since := "2024-10-21")] abbrev get_push_lt := @getElem_push_lt
-@[deprecated getElem_push_eq (since := "2024-10-21")] abbrev get_push_eq := @getElem_push_eq
-
-@[deprecated back!_eq_back? (since := "2024-10-31")] abbrev back_eq_back? := @back!_eq_back?
-@[deprecated back!_push (since := "2024-10-31")] abbrev back_push := @back!_push
-@[deprecated eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]
-abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
-
 @[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_eq_setIfInBounds
 @[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
 @[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 7465f9a711..26fc0002d8 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -436,8 +436,6 @@ def setWidth' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
     apply Nat.lt_of_lt_of_le x.isLt
     exact Nat.pow_le_pow_right (by trivial) le)
 
-@[deprecated setWidth' (since := "2024-09-18"), inherit_doc setWidth'] abbrev zeroExtend' := @setWidth'
-
 /--
 Returns `zeroExtend (w+n) x <<< n` without needing to compute `x % 2^(2+n)`.
 -/
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index e8267360f3..6a57da700a 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -668,11 +668,6 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i
       getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp]
     by_cases hi : x.getLsbD i <;> simp [hi] <;> omega
 
-@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (since := "2024-09-18"),
-  inherit_doc setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]
-abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow :=
-  @setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow
-
 /--
 Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the
 same as truncating `y` to `s` bits, then zero extending to the original length,
@@ -699,10 +694,6 @@ theorem mulRec_eq_mul_signExtend_setWidth (x y : BitVec w) (s : Nat) :
       by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]
     rw [heq, ← BitVec.mul_add, ← setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]
 
-@[deprecated mulRec_eq_mul_signExtend_setWidth (since := "2024-09-18"),
-  inherit_doc mulRec_eq_mul_signExtend_setWidth]
-abbrev mulRec_eq_mul_signExtend_truncate := @mulRec_eq_mul_signExtend_setWidth
-
 theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
     (x * y).getLsbD i = (mulRec x y w).getLsbD i := by
   simp only [mulRec_eq_mul_signExtend_setWidth]
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 5b43d8a7ea..5f6c6910a7 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -3086,10 +3086,6 @@ theorem setWidth_succ (x : BitVec w) :
     · simp_all
     · omega
 
-@[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
-
 @[simp] theorem not_cons (x : BitVec w) (b : Bool) : ~~~(cons b x) = cons (!b) (~~~x) := by
   simp [cons]
 
@@ -5559,150 +5555,6 @@ abbrev toFin_uShiftRight := @toFin_ushiftRight
 @[deprecated signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")]
 abbrev signExtend_eq_not_setWidth_not_of_msb_false := @signExtend_eq_setWidth_of_msb_false
 
-@[deprecated truncate_eq_setWidth (since := "2024-09-18")]
-abbrev truncate_eq_zeroExtend := @truncate_eq_setWidth
-
-@[deprecated toNat_setWidth' (since := "2024-09-18")]
-abbrev toNat_zeroExtend' := @toNat_setWidth'
-
-@[deprecated toNat_setWidth (since := "2024-09-18")]
-abbrev toNat_zeroExtend := @toNat_setWidth
-
-@[deprecated toNat_setWidth (since := "2024-09-18")]
-abbrev toNat_truncate := @toNat_setWidth
-
-@[deprecated setWidth_eq (since := "2024-09-18")]
-abbrev zeroExtend_eq := @setWidth_eq
-
-@[deprecated setWidth_eq (since := "2024-09-18")]
-abbrev truncate_eq := @setWidth_eq
-
-@[deprecated setWidth_zero (since := "2024-09-18")]
-abbrev zeroExtend_zero := @setWidth_zero
-
-@[deprecated getElem_setWidth (since := "2024-09-18")]
-abbrev getElem_zeroExtend := @getElem_setWidth
-
-@[deprecated getElem_setWidth' (since := "2024-09-18")]
-abbrev getElem_zeroExtend' := @getElem_setWidth'
-
-@[deprecated getElem?_setWidth (since := "2024-09-18")]
-abbrev getElem?_zeroExtend := @getElem?_setWidth
-
-@[deprecated getElem?_setWidth' (since := "2024-09-18")]
-abbrev getElem?_zeroExtend' := @getElem?_setWidth'
-
-@[deprecated getLsbD_setWidth (since := "2024-09-18")]
-abbrev getLsbD_zeroExtend := @getLsbD_setWidth
-
-@[deprecated getLsbD_setWidth' (since := "2024-09-18")]
-abbrev getLsbD_zeroExtend' := @getLsbD_setWidth'
-
-@[deprecated getMsbD_setWidth_add (since := "2024-09-18")]
-abbrev getMsbD_zeroExtend_add := @getMsbD_setWidth_add
-
-@[deprecated getMsbD_setWidth' (since := "2024-09-18")]
-abbrev getMsbD_zeroExtend' := @getMsbD_setWidth'
-
-@[deprecated getElem_setWidth (since := "2024-09-18")]
-abbrev getElem_truncate := @getElem_setWidth
-
-@[deprecated getElem?_setWidth (since := "2024-09-18")]
-abbrev getElem?_truncate := @getElem?_setWidth
-
-@[deprecated getLsbD_setWidth (since := "2024-09-18")]
-abbrev getLsbD_truncate := @getLsbD_setWidth
-
-@[deprecated msb_setWidth (since := "2024-09-18")]
-abbrev msb_truncate := @msb_setWidth
-
-@[deprecated cast_setWidth (since := "2024-09-18")]
-abbrev cast_zeroExtend := @cast_setWidth
-
-@[deprecated cast_setWidth (since := "2024-09-18")]
-abbrev cast_truncate := @cast_setWidth
-
-@[deprecated setWidth_setWidth_of_le (since := "2024-09-18")]
-abbrev zeroExtend_zeroExtend_of_le := @setWidth_setWidth_of_le
-
-@[deprecated setWidth_eq (since := "2024-09-18")]
-abbrev truncate_eq_self := @setWidth_eq
-
-@[deprecated setWidth_cast (since := "2024-09-18")]
-abbrev truncate_cast := @setWidth_cast
-
-@[deprecated msb_setWidth (since := "2024-09-18")]
-abbrev mbs_zeroExtend := @msb_setWidth
-
-@[deprecated msb_setWidth' (since := "2024-09-18")]
-abbrev mbs_zeroExtend' := @msb_setWidth'
-
-@[deprecated setWidth_one_eq_ofBool_getLsb_zero (since := "2024-09-18")]
-abbrev zeroExtend_one_eq_ofBool_getLsb_zero := @setWidth_one_eq_ofBool_getLsb_zero
-
-@[deprecated setWidth_ofNat_one_eq_ofNat_one_of_lt (since := "2024-09-18")]
-abbrev zeroExtend_ofNat_one_eq_ofNat_one_of_lt := @setWidth_ofNat_one_eq_ofNat_one_of_lt
-
-@[deprecated setWidth_one (since := "2024-09-18")]
-abbrev truncate_one := @setWidth_one
-
-@[deprecated setWidth_ofNat_of_le (since := "2024-09-18")]
-abbrev truncate_ofNat_of_le := @setWidth_ofNat_of_le
-
-@[deprecated setWidth_or (since := "2024-09-18")]
-abbrev truncate_or := @setWidth_or
-
-@[deprecated setWidth_and (since := "2024-09-18")]
-abbrev truncate_and := @setWidth_and
-
-@[deprecated setWidth_xor (since := "2024-09-18")]
-abbrev truncate_xor := @setWidth_xor
-
-@[deprecated setWidth_not (since := "2024-09-18")]
-abbrev truncate_not := @setWidth_not
-
-@[deprecated signExtend_eq_setWidth_of_msb_false  (since := "2024-09-18")]
-abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_setWidth_of_msb_false
-
-@[deprecated signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]
-abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true
-
-@[deprecated signExtend_eq_setWidth_of_lt (since := "2024-09-18")]
-abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_le
-
-@[deprecated truncate_append (since := "2024-09-18")]
-abbrev truncate_append := @setWidth_append
-
-@[deprecated truncate_append_of_eq (since := "2024-09-18")]
-abbrev truncate_append_of_eq := @setWidth_append_of_eq
-
-@[deprecated truncate_cons (since := "2024-09-18")]
-abbrev truncate_cons := @setWidth_cons
-
-@[deprecated truncate_succ (since := "2024-09-18")]
-abbrev truncate_succ := @setWidth_succ
-
-@[deprecated truncate_add (since := "2024-09-18")]
-abbrev truncate_add := @setWidth_add
-
-@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (since := "2024-09-18")]
-abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false := @setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
-
-@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true (since := "2024-09-18")]
-abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true := @setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
-
-@[deprecated and_one_eq_setWidth_ofBool_getLsbD (since := "2024-09-18")]
-abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLsbD
-
-@[deprecated msb_sshiftRight (since := "2024-10-03")]
-abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight
-
-@[deprecated shiftLeft_zero (since := "2024-10-27")]
-abbrev shiftLeft_zero_eq := @shiftLeft_zero
-
-@[deprecated ushiftRight_zero (since := "2024-10-27")]
-abbrev ushiftRight_zero_eq := @ushiftRight_zero
-
 @[deprecated replicate_zero (since := "2025-01-08")]
 abbrev replicate_zero_eq := @replicate_zero
 
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index b6bf8565ee..7e97886210 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -90,8 +90,6 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   | cons x l ih =>
     rw [pmap, pmap, h _ mem_cons_self, ih fun a ha => h a (mem_cons_of_mem _ ha)]
 
-@[deprecated pmap_congr_left (since := "2024-09-06")] abbrev pmap_congr := @pmap_congr_left
-
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {l : List α} (H) :
     map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
   induction l
@@ -237,11 +235,6 @@ theorem attachWith_ne_nil_iff {l : List α} {P : α → Prop} {H : ∀ a ∈ l,
     l.attachWith P H ≠ [] ↔ l ≠ [] :=
   pmap_ne_nil_iff _ _
 
-@[deprecated pmap_eq_nil_iff (since := "2024-09-06")] abbrev pmap_eq_nil := @pmap_eq_nil_iff
-@[deprecated pmap_ne_nil_iff (since := "2024-09-06")] abbrev pmap_ne_nil := @pmap_ne_nil_iff
-@[deprecated attach_eq_nil_iff (since := "2024-09-06")] abbrev attach_eq_nil := @attach_eq_nil_iff
-@[deprecated attach_ne_nil_iff (since := "2024-09-06")] abbrev attach_ne_nil := @attach_ne_nil_iff
-
 @[simp]
 theorem getElem?_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} (h : ∀ a ∈ l, p a) (i : Nat) :
     (pmap f l h)[i]? = Option.pmap f l[i]? fun x H => h x (mem_of_getElem? H) := by
@@ -776,8 +769,6 @@ and simplifies these to the function directly taking the value.
   | nil => simp
   | cons a l ih => simp [ih, hf]
 
-@[deprecated flatMap_subtype (since := "2024-10-16")] abbrev bind_subtype := @flatMap_subtype
-
 @[simp] theorem findSome?_subtype {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.findSome? f = l.unattach.findSome? g := by
@@ -830,8 +821,6 @@ and simplifies these to the function directly taking the value.
   unfold unattach
   induction l <;> simp_all
 
-@[deprecated unattach_flatten (since := "2024-10-14")] abbrev unattach_join := @unattach_flatten
-
 @[simp] theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
     (List.replicate n x).unattach = List.replicate n x.1 := by
   simp [unattach, -map_subtype]
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 919f6cc628..13fee0b134 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -703,8 +703,6 @@ def flatten : List (List α) → List α
 @[simp, grind] theorem flatten_nil : List.flatten ([] : List (List α)) = [] := rfl
 @[simp, grind] theorem flatten_cons : (l :: L).flatten = l ++ L.flatten := rfl
 
-@[deprecated flatten (since := "2024-10-14"), inherit_doc flatten] abbrev join := @flatten
-
 /-! ### singleton -/
 
 /--
@@ -717,9 +715,6 @@ Examples:
 -/
 @[inline] protected def singleton {α : Type u} (a : α) : List α := [a]
 
-set_option linter.missingDocs false in
-@[deprecated singleton (since := "2024-10-16")] protected abbrev pure := @singleton
-
 /-! ### flatMap -/
 
 /--
@@ -736,13 +731,6 @@ Examples:
 @[simp, grind] theorem flatMap_cons {x : α} {xs : List α} {f : α → List β} :
   List.flatMap f (x :: xs) = f x ++ List.flatMap f xs := by simp [flatten, List.flatMap]
 
-set_option linter.missingDocs false in
-@[deprecated flatMap (since := "2024-10-16")] abbrev bind := @flatMap
-set_option linter.missingDocs false in
-@[deprecated flatMap_nil (since := "2024-10-16")] abbrev nil_flatMap := @flatMap_nil
-set_option linter.missingDocs false in
-@[deprecated flatMap_cons (since := "2024-10-16")] abbrev cons_flatMap := @flatMap_cons
-
 /-! ### replicate -/
 
 /--
@@ -2087,18 +2075,6 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 @[simp, grind] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
 @[simp, grind] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 
-/-- Sum of a list of natural numbers. -/
-@[deprecated List.sum (since := "2024-10-17")]
-protected def _root_.Nat.sum (l : List Nat) : Nat := l.foldr (·+·) 0
-
-set_option linter.deprecated false in
-@[deprecated sum_nil (since := "2024-10-17")]
-theorem _root_.Nat.sum_nil : Nat.sum ([] : List Nat) = 0 := rfl
-set_option linter.deprecated false in
-@[deprecated sum_cons (since := "2024-10-17")]
-theorem _root_.Nat.sum_cons (a : Nat) (l : List Nat) :
-    Nat.sum (a::l) = a + Nat.sum l := rfl
-
 /-! ### range -/
 
 /--
@@ -2220,8 +2196,6 @@ def min? [Min α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl min a
 
-@[inherit_doc min?, deprecated min? (since := "2024-09-29")] abbrev minimum? := @min?
-
 /-! ### max? -/
 
 /--
@@ -2236,8 +2210,6 @@ def max? [Max α] : List α → Option α
   | []    => none
   | a::as => some <| as.foldl max a
 
-@[inherit_doc max?, deprecated max? (since := "2024-09-29")] abbrev maximum? := @max?
-
 /-! ## Other list operations
 
 The functions are currently mostly used in meta code,
@@ -2410,8 +2382,6 @@ where
     | false => loop as a [] ((b::r).reverse::acc)
   | [], ag, r, acc => ((ag::r).reverse::acc).reverse
 
-@[deprecated splitBy (since := "2024-10-30"), inherit_doc splitBy] abbrev groupBy := @splitBy
-
 /-! ### removeAll -/
 
 /--
diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean
index cb38109d2f..2663f613cf 100644
--- a/src/Init/Data/List/Count.lean
+++ b/src/Init/Data/List/Count.lean
@@ -83,8 +83,6 @@ theorem countP_le_length : countP p l ≤ l.length := by
 @[simp] theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a := by
   simp only [countP_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]
 
-@[deprecated countP_pos_iff (since := "2024-09-09")] abbrev countP_pos := @countP_pos_iff
-
 @[simp] theorem one_le_countP_iff {p} : 1 ≤ countP p l ↔ ∃ a ∈ l, p a :=
   countP_pos_iff
 
@@ -165,8 +163,6 @@ theorem countP_filterMap {p : β → Bool} {f : α → Option β} {l : List α}
   simp only [countP_eq_length_filter, filter_flatten]
   simp [countP_eq_length_filter']
 
-@[deprecated countP_flatten (since := "2024-10-14")] abbrev countP_join := @countP_flatten
-
 theorem countP_flatMap {p : β → Bool} {l : List α} {f : α → List β} :
     countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by
   rw [List.flatMap, countP_flatten, map_map]
@@ -242,8 +238,6 @@ theorem count_singleton {a b : α} : count a [b] = if b == a then 1 else 0 := by
 theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
   simp only [count_eq_countP, countP_flatten, count_eq_countP']
 
-@[deprecated count_flatten (since := "2024-10-14")] abbrev count_join := @count_flatten
-
 @[simp] theorem count_reverse {a : α} {l : List α} : count a l.reverse = count a l := by
   simp only [count_eq_countP, countP_eq_length_filter, filter_reverse, length_reverse]
 
@@ -268,8 +262,6 @@ theorem count_concat_self {a : α} {l : List α} : count a (concat l a) = count
 theorem count_pos_iff {a : α} {l : List α} : 0 < count a l ↔ a ∈ l := by
   simp only [count, countP_pos_iff, beq_iff_eq, exists_eq_right]
 
-@[deprecated count_pos_iff (since := "2024-09-09")] abbrev count_pos_iff_mem := @count_pos_iff
-
 @[simp] theorem one_le_count_iff {a : α} {l : List α} : 1 ≤ count a l ↔ a ∈ l :=
   count_pos_iff
 
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 178cde63d8..e2647724a1 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -47,8 +47,6 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
 @[simp] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
   induction l <;> simp [findSome?_cons]; split <;> simp [*]
 
-@[deprecated findSome?_eq_none_iff (since := "2024-09-05")] abbrev findSome?_eq_none := @findSome?_eq_none_iff
-
 @[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : List α} :
     (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
   induction l with
@@ -386,17 +384,10 @@ abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   simp [flatMap_def, findSome?_map]; rfl
 
-@[deprecated find?_flatMap (since := "2024-10-16")] abbrev find?_bind := @find?_flatMap
-
 theorem find?_flatMap_eq_none_iff {xs : List α} {f : α → List β} {p : β → Bool} :
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
-@[deprecated find?_flatMap_eq_none_iff (since := "2024-10-16")]
-abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
-
-@[deprecated find?_flatMap_eq_none (since := "2024-10-16")] abbrev find?_bind_eq_none := @find?_flatMap_eq_none_iff
-
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
   · simp
@@ -1270,13 +1261,4 @@ theorem IsInfix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂
 
 end lookup
 
-/-! ### Deprecations -/
-
-@[deprecated head_flatten (since := "2024-10-14")] abbrev head_join := @head_flatten
-@[deprecated getLast_flatten (since := "2024-10-14")] abbrev getLast_join := @getLast_flatten
-@[deprecated find?_flatten (since := "2024-10-14")] abbrev find?_join := @find?_flatten
-@[deprecated find?_flatten_eq_none (since := "2024-10-14")] abbrev find?_join_eq_none := @find?_flatten_eq_none_iff
-@[deprecated find?_flatten_eq_some (since := "2024-10-14")] abbrev find?_join_eq_some := @find?_flatten_eq_some_iff
-@[deprecated findIdx?_flatten (since := "2024-10-14")] abbrev findIdx?_join := @findIdx?_flatten
-
 end List
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 1f19fde6c2..8751669f5f 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1143,8 +1143,6 @@ theorem forall_mem_map {f : α → β} {l : List α} {P : β → Prop} :
 @[simp] theorem map_eq_nil_iff {f : α → β} {l : List α} : map f l = [] ↔ l = [] := by
   constructor <;> exact fun _ => match l with | [] => rfl
 
-@[deprecated map_eq_nil_iff (since := "2024-09-05")] abbrev map_eq_nil := @map_eq_nil_iff
-
 @[grind →]
 theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = []) : l = [] :=
   map_eq_nil_iff.mp h
@@ -1186,14 +1184,10 @@ theorem map_eq_cons_iff {f : α → β} {l : List α} :
     · rintro ⟨a, l₁, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩⟩
       constructor <;> rfl
 
-@[deprecated map_eq_cons_iff (since := "2024-09-05")] abbrev map_eq_cons := @map_eq_cons_iff
-
 theorem map_eq_cons_iff' {f : α → β} {l : List α} :
     map f l = b :: l₂ ↔ l.head?.map f = some b ∧ l.tail?.map (map f) = some l₂ := by
   induction l <;> simp_all
 
-@[deprecated map_eq_cons' (since := "2024-09-05")] abbrev map_eq_cons' := @map_eq_cons_iff'
-
 @[simp] theorem map_eq_singleton_iff {f : α → β} {l : List α} {b : β} :
     map f l = [b] ↔ ∃ a, l = [a] ∧ f a = b := by
   simp [map_eq_cons_iff]
@@ -1218,11 +1212,6 @@ theorem map_eq_foldr {f : α → β} {l : List α} : map f l = foldr (fun a bs =
   | nil => simp
   | cons b l ih => cases i <;> simp_all
 
-@[deprecated "Use the reverse direction of `map_set`." (since := "2024-09-20")]
-theorem set_map {f : α → β} {l : List α} {i : Nat} {a : α} :
-    (map f l).set i (f a) = map f (l.set i a) := by
-  simp
-
 @[simp] theorem head_map {f : α → β} {l : List α} (w) :
     (map f l).head w = f (l.head (by simpa using w)) := by
   cases l
@@ -1324,8 +1313,6 @@ abbrev filter_length_eq_length := @length_filter_eq_length_iff
 @[simp] theorem filter_eq_nil_iff {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by
   simp only [eq_nil_iff_forall_not_mem, mem_filter, not_and]
 
-@[deprecated filter_eq_nil_iff (since := "2024-09-05")] abbrev filter_eq_nil := @filter_eq_nil_iff
-
 theorem forall_mem_filter {l : List α} {p : α → Bool} {P : α → Prop} :
     (∀ (i) (_ : i ∈ l.filter p), P i) ↔ ∀ (j) (_ : j ∈ l), p j → P j := by
   simp
@@ -1387,8 +1374,6 @@ theorem filter_eq_cons_iff {l} {a} {as} :
   · rintro ⟨l₁, l₂, rfl, h₁, h, h₂⟩
     simp [h₂, filter_cons, filter_eq_nil_iff.mpr h₁, h]
 
-@[deprecated filter_eq_cons_iff (since := "2024-09-05")] abbrev filter_eq_cons := @filter_eq_cons_iff
-
 theorem filter_congr {p q : α → Bool} :
     ∀ {l : List α}, (∀ x ∈ l, p x = q x) → filter p l = filter q l
   | [], _ => rfl
@@ -1548,8 +1533,6 @@ theorem forall_none_of_filterMap_eq_nil (h : filterMap f xs = []) : ∀ x ∈ xs
         simp_all
       · simp_all
 
-@[deprecated filterMap_eq_nil_iff (since := "2024-09-05")] abbrev filterMap_eq_nil := @filterMap_eq_nil_iff
-
 theorem filterMap_eq_cons_iff {l} {b} {bs} :
     filterMap f l = b :: bs ↔
       ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ (∀ x, x ∈ l₁ → f x = none) ∧ f a = some b ∧
@@ -1572,8 +1555,6 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
   · rintro ⟨l₁, a, l₂, rfl, h₁, h₂, h₃⟩
     simp_all [filterMap_eq_nil_iff.mpr h₁, filterMap_cons_some h₂]
 
-@[deprecated filterMap_eq_cons_iff (since := "2024-09-05")] abbrev filterMap_eq_cons := @filterMap_eq_cons_iff
-
 /-! ### append -/
 
 @[simp] theorem nil_append_fun : (([] : List α) ++ ·) = id := rfl
@@ -1830,14 +1811,10 @@ theorem filterMap_eq_append_iff {f : α → Option β} :
   · rintro ⟨l₁, l₂, rfl, rfl, rfl⟩
     simp
 
-@[deprecated filterMap_eq_append_iff (since := "2024-09-05")] abbrev filterMap_eq_append := @filterMap_eq_append_iff
-
 theorem append_eq_filterMap_iff {f : α → Option β} :
     L₁ ++ L₂ = filterMap f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂ := by
   rw [eq_comm, filterMap_eq_append_iff]
 
-@[deprecated append_eq_filterMap (since := "2024-09-05")] abbrev append_eq_filterMap := @append_eq_filterMap_iff
-
 theorem filter_eq_append_iff {p : α → Bool} :
     filter p l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂ := by
   rw [← filterMap_eq_filter, filterMap_eq_append_iff]
@@ -1846,8 +1823,6 @@ theorem append_eq_filter_iff {p : α → Bool} :
     L₁ ++ L₂ = filter p l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂ := by
   rw [eq_comm, filter_eq_append_iff]
 
-@[deprecated append_eq_filter_iff (since := "2024-09-05")] abbrev append_eq_filter := @append_eq_filter_iff
-
 @[simp, grind] theorem map_append {f : α → β} : ∀ {l₁ l₂}, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
   intro l₁; induction l₁ <;> intros <;> simp_all
 
@@ -1859,9 +1834,6 @@ theorem append_eq_map_iff {f : α → β} :
     L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
   rw [eq_comm, map_eq_append_iff]
 
-@[deprecated map_eq_append_iff (since := "2024-09-05")] abbrev map_eq_append := @map_eq_append_iff
-@[deprecated append_eq_map_iff (since := "2024-09-05")] abbrev append_eq_map := @append_eq_map_iff
-
 /-! ### concat
 
 Note that `concat_eq_append` is a `@[simp]` lemma, so `concat` should usually not appear in goals.
@@ -1893,8 +1865,6 @@ theorem concat_inj_left {l l' : List α} (a : α) : concat l a = concat l' a ↔
 theorem concat_inj_right {l : List α} {a a' : α} : concat l a = concat l a' ↔ a = a' :=
   ⟨last_eq_of_concat_eq, by simp⟩
 
-@[deprecated concat_inj (since := "2024-09-05")] abbrev concat_eq_concat := @concat_inj
-
 theorem concat_append {a : α} {l₁ l₂ : List α} : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by simp
 
 theorem append_concat {a : α} {l₁ l₂ : List α} : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
@@ -2108,8 +2078,6 @@ theorem flatMap_eq_nil_iff {l : List α} {f : α → List β} : l.flatMap f = []
   flatten_eq_nil_iff.trans <| by
     simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
 
-@[deprecated flatMap_eq_nil_iff (since := "2024-09-05")] abbrev bind_eq_nil := @flatMap_eq_nil_iff
-
 theorem forall_mem_flatMap {p : β → Prop} {l : List α} {f : α → List β} :
     (∀ (x) (_ : x ∈ l.flatMap f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b := by
   simp only [mem_flatMap, forall_exists_index, and_imp]
@@ -2188,12 +2156,6 @@ theorem contains_replicate [BEq α] {n : Nat} {a b : α} :
     simp only [replicate_succ, elem_cons]
     split <;> simp_all
 
-@[deprecated mem_replicate (since := "2024-09-05")]
-theorem decide_mem_replicate [BEq α] [LawfulBEq α] {a b : α} :
-    ∀ {n}, decide (b ∈ replicate n a) = ((¬ n == 0) && b == a) := by
-  have : DecidableEq α := instDecidableEqOfLawfulBEq
-  simp [Bool.beq_eq_decide_eq]
-
 @[grind →] theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
 theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
@@ -2206,8 +2168,6 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 @[simp] theorem replicate_eq_nil_iff {n : Nat} (a : α) : replicate n a = [] ↔ n = 0 := by
   cases n <;> simp
 
-@[deprecated replicate_eq_nil_iff (since := "2024-09-05")] abbrev replicate_eq_nil := @replicate_eq_nil_iff
-
 @[simp, grind] theorem getElem_replicate {a : α} {n : Nat} {i : Nat} (h : i < (replicate n a).length) :
     (replicate n a)[i] = a :=
   eq_of_mem_replicate (getElem_mem _)
@@ -2259,8 +2219,6 @@ theorem eq_replicate_iff {a : α} {n} {l : List α} :
   ⟨fun h => h ▸ ⟨length_replicate .., fun _ => eq_of_mem_replicate⟩,
    fun ⟨e, al⟩ => e ▸ eq_replicate_of_mem al⟩
 
-@[deprecated eq_replicate_iff (since := "2024-09-05")] abbrev eq_replicate := @eq_replicate_iff
-
 theorem map_eq_replicate_iff {l : List α} {f : α → β} {b : β} :
     l.map f = replicate l.length b ↔ ∀ x ∈ l, f x = b := by
   simp [eq_replicate_iff]
@@ -2302,8 +2260,6 @@ theorem append_eq_replicate_iff {l₁ l₂ : List α} {a : α} :
     { mp := fun h => ⟨fun b m => h b (Or.inl m), fun b m => h b (Or.inr m)⟩,
       mpr := fun h b x => Or.casesOn x (fun m => h.left b m) fun m => h.right b m }
 
-@[deprecated append_eq_replicate_iff (since := "2024-09-05")] abbrev append_eq_replicate := @append_eq_replicate_iff
-
 theorem replicate_eq_append_iff {l₁ l₂ : List α} {a : α} :
     replicate n a = l₁ ++ l₂ ↔
       l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a := by
@@ -2483,8 +2439,6 @@ theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse :
     xs.reverse = a :: ys ↔ xs = ys.reverse ++ [a] := by
   rw [reverse_eq_iff, reverse_cons]
 
-@[deprecated reverse_eq_cons_iff (since := "2024-09-05")] abbrev reverse_eq_cons := @reverse_eq_cons_iff
-
 @[simp, grind] theorem getLast?_reverse {l : List α} : l.reverse.getLast? = l.head? := by
   cases l <;> simp [getLast?_concat]
 
@@ -2535,8 +2489,6 @@ theorem getLast_of_mem_getLast? {l : List α} (hx : x ∈ l.getLast?) :
     xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by
   rw [reverse_eq_iff, reverse_append]
 
-@[deprecated reverse_eq_append_iff (since := "2024-09-05")] abbrev reverse_eq_append := @reverse_eq_append_iff
-
 @[grind _=_] theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
   rw [reverse_append]; rfl
 
@@ -2642,8 +2594,6 @@ theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
 
 theorem foldr_cons_nil {l : List α} : l.foldr cons [] = l := by simp
 
-@[deprecated foldr_cons_nil (since := "2024-09-04")] abbrev foldr_self := @foldr_cons_nil
-
 theorem foldl_map {f : β₁ → β₂} {g : α → β₂ → α} {l : List β₁} {init : α} :
     (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
   induction l generalizing init <;> simp [*]
@@ -2889,8 +2839,6 @@ theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔
   rw [getLast?_eq_head?_reverse, isSome_head?]
   simp
 
-@[deprecated mem_of_getLast? (since := "2024-10-21")] abbrev mem_of_getLast?_eq_some := @mem_of_getLast?
-
 @[simp, grind] theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
     l.reverse.getLast h = l.head (by simp_all) := by
   simp [getLast_eq_head_reverse]
@@ -3279,13 +3227,9 @@ theorem all_eq_not_any_not {l : List α} {p : α → Bool} : l.all p = !l.any (!
 @[simp, grind] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
   induction l <;> simp_all
 
-@[deprecated any_flatten (since := "2024-10-14")] abbrev any_join := @any_flatten
-
 @[simp, grind] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
   induction l <;> simp_all
 
-@[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
-
 @[simp, grind] theorem any_flatMap {l : List α} {f : α → List β} :
     (l.flatMap f).any p = l.any fun a => (f a).any p := by
   induction l <;> simp_all
@@ -3745,74 +3689,6 @@ theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a :=
 
 /-! ### Deprecations -/
 
-@[deprecated getElem_eq_getElem?_get (since := "2024-09-04")] abbrev getElem_eq_getElem? :=
-  @getElem_eq_getElem?_get
-@[deprecated flatten_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @flatten_eq_nil_iff
-@[deprecated flatten_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @flatten_ne_nil_iff
-@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons_iff := @flatten_eq_cons_iff
-@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @flatten_eq_cons_iff
-@[deprecated flatten_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @flatten_eq_append_iff
-@[deprecated mem_of_getElem? (since := "2024-09-06")] abbrev getElem?_mem := @mem_of_getElem?
-@[deprecated getElem_set_self (since := "2024-09-04")] abbrev getElem_set_eq := @getElem_set_self
-@[deprecated getElem?_set_self (since := "2024-09-04")] abbrev getElem?_set_eq := @getElem?_set_self
-@[deprecated set_eq_nil_iff (since := "2024-09-05")] abbrev set_eq_nil := @set_eq_nil_iff
-
-@[deprecated flatten_nil (since := "2024-10-14")] abbrev join_nil := @flatten_nil
-@[deprecated flatten_cons (since := "2024-10-14")] abbrev join_cons := @flatten_cons
-@[deprecated length_flatten (since := "2024-10-14")] abbrev length_join := @length_flatten
-@[deprecated flatten_singleton (since := "2024-10-14")] abbrev join_singleton := @flatten_singleton
-@[deprecated mem_flatten (since := "2024-10-14")] abbrev mem_join := @mem_flatten
-@[deprecated flatten_eq_nil_iff (since := "2024-10-14")] abbrev join_eq_nil_iff := @flatten_eq_nil_iff
-@[deprecated flatten_ne_nil_iff (since := "2024-10-14")] abbrev join_ne_nil_iff := @flatten_ne_nil_iff
-@[deprecated exists_of_mem_flatten (since := "2024-10-14")] abbrev exists_of_mem_join := @exists_of_mem_flatten
-@[deprecated mem_flatten_of_mem (since := "2024-10-14")] abbrev mem_join_of_mem := @mem_flatten_of_mem
-@[deprecated forall_mem_flatten (since := "2024-10-14")] abbrev forall_mem_join := @forall_mem_flatten
-@[deprecated flatten_eq_flatMap (since := "2024-10-14")] abbrev join_eq_bind := @flatten_eq_flatMap
-@[deprecated head?_flatten (since := "2024-10-14")] abbrev head?_join := @head?_flatten
-@[deprecated foldl_flatten (since := "2024-10-14")] abbrev foldl_join := @foldl_flatten
-@[deprecated foldr_flatten (since := "2024-10-14")] abbrev foldr_join := @foldr_flatten
-@[deprecated map_flatten (since := "2024-10-14")] abbrev map_join := @map_flatten
-@[deprecated filterMap_flatten (since := "2024-10-14")] abbrev filterMap_join := @filterMap_flatten
-@[deprecated filter_flatten (since := "2024-10-14")] abbrev filter_join := @filter_flatten
-@[deprecated flatten_filter_not_isEmpty (since := "2024-10-14")] abbrev join_filter_not_isEmpty := @flatten_filter_not_isEmpty
-@[deprecated flatten_filter_ne_nil (since := "2024-10-14")] abbrev join_filter_ne_nil := @flatten_filter_ne_nil
-@[deprecated flatten_append (since := "2024-10-14")] abbrev join_append := @flatten_append
-@[deprecated flatten_concat (since := "2024-10-14")] abbrev join_concat := @flatten_concat
-@[deprecated flatten_flatten (since := "2024-10-14")] abbrev join_join := @flatten_flatten
-@[deprecated flatten_eq_append_iff (since := "2024-10-14")] abbrev join_eq_append_iff := @flatten_eq_append_iff
-@[deprecated eq_iff_flatten_eq (since := "2024-10-14")] abbrev eq_iff_join_eq := @eq_iff_flatten_eq
-@[deprecated flatten_replicate_nil (since := "2024-10-14")] abbrev join_replicate_nil := @flatten_replicate_nil
-@[deprecated flatten_replicate_singleton (since := "2024-10-14")] abbrev join_replicate_singleton := @flatten_replicate_singleton
-@[deprecated flatten_replicate_replicate (since := "2024-10-14")] abbrev join_replicate_replicate := @flatten_replicate_replicate
-@[deprecated reverse_flatten (since := "2024-10-14")] abbrev reverse_join := @reverse_flatten
-@[deprecated flatten_reverse (since := "2024-10-14")] abbrev join_reverse := @flatten_reverse
-@[deprecated getLast?_flatten (since := "2024-10-14")] abbrev getLast?_join := @getLast?_flatten
-@[deprecated flatten_eq_flatMap (since := "2024-10-16")] abbrev flatten_eq_bind := @flatten_eq_flatMap
-@[deprecated flatMap_def (since := "2024-10-16")] abbrev bind_def := @flatMap_def
-@[deprecated flatMap_id (since := "2024-10-16")] abbrev bind_id := @flatMap_id
-@[deprecated mem_flatMap (since := "2024-10-16")] abbrev mem_bind := @mem_flatMap
-@[deprecated exists_of_mem_flatMap (since := "2024-10-16")] abbrev exists_of_mem_bind := @exists_of_mem_flatMap
-@[deprecated mem_flatMap_of_mem (since := "2024-10-16")] abbrev mem_bind_of_mem := @mem_flatMap_of_mem
-@[deprecated flatMap_eq_nil_iff (since := "2024-10-16")] abbrev bind_eq_nil_iff := @flatMap_eq_nil_iff
-@[deprecated forall_mem_flatMap (since := "2024-10-16")] abbrev forall_mem_bind := @forall_mem_flatMap
-@[deprecated flatMap_singleton (since := "2024-10-16")] abbrev bind_singleton := @flatMap_singleton
-@[deprecated flatMap_singleton' (since := "2024-10-16")] abbrev bind_singleton' := @flatMap_singleton'
-@[deprecated head?_flatMap (since := "2024-10-16")] abbrev head_bind := @head?_flatMap
-@[deprecated flatMap_append (since := "2024-10-16")] abbrev bind_append := @flatMap_append
-@[deprecated flatMap_assoc (since := "2024-10-16")] abbrev bind_assoc := @flatMap_assoc
-@[deprecated map_flatMap (since := "2024-10-16")] abbrev map_bind := @map_flatMap
-@[deprecated flatMap_map (since := "2024-10-16")] abbrev bind_map := @flatMap_map
-@[deprecated map_eq_flatMap (since := "2024-10-16")] abbrev map_eq_bind := @map_eq_flatMap
-@[deprecated filterMap_flatMap (since := "2024-10-16")] abbrev filterMap_bind := @filterMap_flatMap
-@[deprecated filter_flatMap (since := "2024-10-16")] abbrev filter_bind := @filter_flatMap
-@[deprecated flatMap_eq_foldl (since := "2024-10-16")] abbrev bind_eq_foldl := @flatMap_eq_foldl
-@[deprecated flatMap_replicate (since := "2024-10-16")] abbrev bind_replicate := @flatMap_replicate
-@[deprecated reverse_flatMap (since := "2024-10-16")] abbrev reverse_bind := @reverse_flatMap
-@[deprecated flatMap_reverse (since := "2024-10-16")] abbrev bind_reverse := @flatMap_reverse
-@[deprecated getLast?_flatMap (since := "2024-10-16")] abbrev getLast?_bind := @getLast?_flatMap
-@[deprecated any_flatMap (since := "2024-10-16")] abbrev any_bind := @any_flatMap
-@[deprecated all_flatMap (since := "2024-10-16")] abbrev all_bind := @all_flatMap
-
 @[deprecated get?_eq_none (since := "2024-11-29")] abbrev get?_len_le := @getElem?_eq_none
 @[deprecated getElem?_eq_some_iff (since := "2024-11-29")]
 abbrev getElem?_eq_some := @getElem?_eq_some_iff
diff --git a/src/Init/Data/List/MinMax.lean b/src/Init/Data/List/MinMax.lean
index 5b57936976..4c18f47c63 100644
--- a/src/Init/Data/List/MinMax.lean
+++ b/src/Init/Data/List/MinMax.lean
@@ -194,21 +194,4 @@ theorem foldl_max [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Asso
     {l : List α} {a : α} : l.foldl (init := a) max = max a (l.max?.getD a) := by
   cases l <;> simp [max?, foldl_assoc, Std.IdempotentOp.idempotent]
 
-@[deprecated min?_nil (since := "2024-09-29")] abbrev minimum?_nil := @min?_nil
-@[deprecated min?_cons (since := "2024-09-29")] abbrev minimum?_cons := @min?_cons
-@[deprecated min?_eq_none_iff (since := "2024-09-29")] abbrev mininmum?_eq_none_iff := @min?_eq_none_iff
-@[deprecated min?_mem (since := "2024-09-29")] abbrev minimum?_mem := @min?_mem
-@[deprecated le_min?_iff (since := "2024-09-29")] abbrev le_minimum?_iff := @le_min?_iff
-@[deprecated min?_eq_some_iff (since := "2024-09-29")] abbrev minimum?_eq_some_iff := @min?_eq_some_iff
-@[deprecated min?_replicate (since := "2024-09-29")] abbrev minimum?_replicate := @min?_replicate
-@[deprecated min?_replicate_of_pos (since := "2024-09-29")] abbrev minimum?_replicate_of_pos := @min?_replicate_of_pos
-@[deprecated max?_nil (since := "2024-09-29")] abbrev maximum?_nil := @max?_nil
-@[deprecated max?_cons (since := "2024-09-29")] abbrev maximum?_cons := @max?_cons
-@[deprecated max?_eq_none_iff (since := "2024-09-29")] abbrev maximum?_eq_none_iff := @max?_eq_none_iff
-@[deprecated max?_mem (since := "2024-09-29")] abbrev maximum?_mem := @max?_mem
-@[deprecated max?_le_iff (since := "2024-09-29")] abbrev maximum?_le_iff := @max?_le_iff
-@[deprecated max?_eq_some_iff (since := "2024-09-29")] abbrev maximum?_eq_some_iff := @max?_eq_some_iff
-@[deprecated max?_replicate (since := "2024-09-29")] abbrev maximum?_replicate := @max?_replicate
-@[deprecated max?_replicate_of_pos (since := "2024-09-29")] abbrev maximum?_replicate_of_pos := @max?_replicate_of_pos
-
 end List
diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean
index c530e099ed..61c79f21a4 100644
--- a/src/Init/Data/List/Nat/Basic.lean
+++ b/src/Init/Data/List/Nat/Basic.lean
@@ -227,11 +227,4 @@ theorem le_max?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
     a ≤ l.max?.getD k :=
   Option.get_eq_getD _ ▸ le_max?_get_of_mem h
 
-@[deprecated min?_eq_some_iff' (since := "2024-09-29")] abbrev minimum?_eq_some_iff' := @min?_eq_some_iff'
-@[deprecated min?_cons' (since := "2024-09-29")] abbrev minimum?_cons' := @min?_cons'
-@[deprecated min?_getD_le_of_mem (since := "2024-09-29")] abbrev minimum?_getD_le_of_mem := @min?_getD_le_of_mem
-@[deprecated max?_eq_some_iff' (since := "2024-09-29")] abbrev maximum?_eq_some_iff' := @max?_eq_some_iff'
-@[deprecated max?_cons' (since := "2024-09-29")] abbrev maximum?_cons' := @max?_cons'
-@[deprecated le_max?_getD_of_mem (since := "2024-09-29")] abbrev le_maximum?_getD_of_mem := @le_max?_getD_of_mem
-
 end List
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 59efb08c81..150cc0b594 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -184,8 +184,6 @@ theorem dropLast_take {i : Nat} {l : List α} (h : i < l.length) :
     (l.take i).dropLast = l.take (i - 1) := by
   simp only [dropLast_eq_take, length_take, Nat.le_of_lt h, Nat.min_eq_left, take_take, sub_le]
 
-@[deprecated map_eq_append_iff (since := "2024-09-05")] abbrev map_eq_append_split := @map_eq_append_iff
-
 theorem take_eq_dropLast {l : List α} {i : Nat} (h : i + 1 = l.length) :
     l.take i = l.dropLast := by
   induction l generalizing i with
diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean
index b804eaca49..46fec42cd3 100644
--- a/src/Init/Data/List/Pairwise.lean
+++ b/src/Init/Data/List/Pairwise.lean
@@ -174,15 +174,11 @@ theorem pairwise_flatten {L : List (List α)} :
     rw [and_comm, and_congr_left_iff]
     intros; exact ⟨fun h l' b c d e => h c d e l' b, fun h c d e l' b => h l' b c d e⟩
 
-@[deprecated pairwise_flatten (since := "2024-10-14")] abbrev pairwise_join := @pairwise_flatten
-
 theorem pairwise_flatMap {R : β → β → Prop} {l : List α} {f : α → List β} :
     List.Pairwise R (l.flatMap f) ↔
       (∀ a ∈ l, Pairwise R (f a)) ∧ Pairwise (fun a₁ a₂ => ∀ x ∈ f a₁, ∀ y ∈ f a₂, R x y) l := by
   simp [List.flatMap, pairwise_flatten, pairwise_map]
 
-@[deprecated pairwise_flatMap (since := "2024-10-14")] abbrev pairwise_bind := @pairwise_flatMap
-
 theorem pairwise_reverse {l : List α} :
     l.reverse.Pairwise R ↔ l.Pairwise (fun a b => R b a) := by
   induction l <;> simp [*, pairwise_append, and_comm]
diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
index dc481f6eab..42190d524a 100644
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -497,8 +497,6 @@ theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatt
   | swap => simp only [flatten_cons, ← append_assoc, perm_append_right_iff]; exact perm_append_comm ..
   | trans _ _ ih₁ ih₂ => exact trans ih₁ ih₂
 
-@[deprecated Perm.flatten (since := "2024-10-14")] abbrev Perm.join := @Perm.flatten
-
 theorem cons_append_cons_perm {a b : α} {as bs : List α} :
     a :: as ++ b :: bs ~ b :: as ++ a :: bs := by
   suffices [[a], as, [b], bs].flatten ~ [[b], as, [a], bs].flatten by simpa
@@ -511,8 +509,6 @@ theorem cons_append_cons_perm {a b : α} {as bs : List α} :
 theorem Perm.flatMap_right {l₁ l₂ : List α} (f : α → List β) (p : l₁ ~ l₂) : l₁.flatMap f ~ l₂.flatMap f :=
   (p.map _).flatten
 
-@[deprecated Perm.flatMap_right (since := "2024-10-16")] abbrev Perm.bind_right := @Perm.flatMap_right
-
 theorem Perm.eraseP (f : α → Bool) {l₁ l₂ : List α}
     (H : Pairwise (fun a b => f a → f b → False) l₁) (p : l₁ ~ l₂) : eraseP f l₁ ~ eraseP f l₂ := by
   induction p with
diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean
index 0c8d137588..89565e4450 100644
--- a/src/Init/Data/List/Sort/Lemmas.lean
+++ b/src/Init/Data/List/Sort/Lemmas.lean
@@ -306,8 +306,6 @@ theorem sorted_mergeSort
     apply sorted_mergeSort trans total
 termination_by l => l.length
 
-@[deprecated sorted_mergeSort (since := "2024-09-02")] abbrev mergeSort_sorted := @sorted_mergeSort
-
 /--
 If the input list is already sorted, then `mergeSort` does not change the list.
 -/
@@ -444,9 +442,6 @@ theorem sublist_mergeSort
         ((fun w => Sublist.of_sublist_append_right w h') fun b m₁ m₃ =>
           (Bool.eq_not_self true).mp ((rel_of_pairwise_cons hc m₁).symm.trans (h₃ b m₃))))
 
-@[deprecated sublist_mergeSort (since := "2024-09-02")]
-abbrev mergeSort_stable := @sublist_mergeSort
-
 /--
 Another statement of stability of merge sort.
 If a pair `[a, b]` is a sublist of `l` and `le a b`,
@@ -458,9 +453,6 @@ theorem pair_sublist_mergeSort
     (hab : le a b) (h : [a, b] <+ l) : [a, b] <+ mergeSort l le :=
   sublist_mergeSort trans total (pairwise_pair.mpr hab) h
 
-@[deprecated pair_sublist_mergeSort(since := "2024-09-02")]
-abbrev mergeSort_stable_pair := @pair_sublist_mergeSort
-
 theorem map_merge {f : α → β} {r : α → α → Bool} {s : β → β → Bool} {l l' : List α}
     (hl : ∀ a ∈ l, ∀ b ∈ l', r a b = s (f a) (f b)) :
     (l.merge l' r).map f = (l.map f).merge (l'.map f) s := by
diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean
index e640c64e7d..c208b7d15f 100644
--- a/src/Init/Data/List/Sublist.lean
+++ b/src/Init/Data/List/Sublist.lean
@@ -1092,11 +1092,4 @@ theorem prefix_iff_eq_take : l₁ <+: l₂ ↔ l₁ = take (length l₁) l₂ :=
 
 -- See `Init.Data.List.Nat.Sublist` for `suffix_iff_eq_append`, `prefix_take_iff`, and `suffix_iff_eq_drop`.
 
-/-! ### Deprecations -/
-
-@[deprecated sublist_flatten_of_mem (since := "2024-10-14")] abbrev sublist_join_of_mem := @sublist_flatten_of_mem
-@[deprecated sublist_flatten_iff (since := "2024-10-14")] abbrev sublist_join_iff := @sublist_flatten_iff
-@[deprecated flatten_sublist_iff (since := "2024-10-14")] abbrev flatten_join_iff := @flatten_sublist_iff
-@[deprecated infix_of_mem_flatten (since := "2024-10-14")] abbrev infix_of_mem_join := @infix_of_mem_flatten
-
 end List
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 533d21a195..54961416b6 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -131,8 +131,6 @@ theorem drop_eq_nil_iff {l : List α} {i : Nat} : l.drop i = [] ↔ l.length ≤
     · simp only [drop] at h
       simpa [Nat.succ_le_succ_iff] using hi h
 
-@[deprecated drop_eq_nil_iff (since := "2024-09-10")] abbrev drop_eq_nil_iff_le := @drop_eq_nil_iff
-
 @[simp]
 theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ k = 0 ∨ l = [] := by
   cases l <;> cases k <;> simp [Nat.succ_ne_zero]
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 21a8d0f32b..9848363464 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -524,8 +524,6 @@ theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n
 
 @[deprecated and_two_pow_sub_one_eq_mod (since := "2025-03-18")]
 abbrev and_pow_two_sub_one_eq_mod := @and_two_pow_sub_one_eq_mod
-@[deprecated and_two_pow_sub_one_eq_mod (since := "2024-09-11")]
-abbrev and_pow_two_is_mod := @and_two_pow_sub_one_eq_mod
 
 theorem and_two_pow_sub_one_of_lt_two_pow {x : Nat} (lt : x < 2^n) : x &&& 2^n - 1 = x := by
   rw [and_two_pow_sub_one_eq_mod]
@@ -533,8 +531,6 @@ theorem and_two_pow_sub_one_of_lt_two_pow {x : Nat} (lt : x < 2^n) : x &&& 2^n -
 
 @[deprecated and_two_pow_sub_one_of_lt_two_pow (since := "2025-03-18")]
 abbrev and_pow_two_sub_one_of_lt_two_pow := @and_two_pow_sub_one_of_lt_two_pow
-@[deprecated and_two_pow_sub_one_of_lt_two_pow (since := "2024-09-11")]
-abbrev and_two_pow_identity := @and_two_pow_sub_one_of_lt_two_pow
 
 @[simp] theorem and_mod_two_eq_one : (a &&& b) % 2 = 1 ↔ a % 2 = 1 ∧ b % 2 = 1 := by
   simp only [mod_two_eq_one_iff_testBit_zero]
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index 15a0788e4f..801e9c5f70 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -85,6 +85,8 @@ Examples:
 -/
 @[extern "lean_uint8_mod"]
 protected def UInt8.mod (a b : UInt8) : UInt8 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+
+-- Note: This is deprecated, but still used in the `HMod` instance below.
 set_option linter.missingDocs false in
 @[deprecated UInt8.mod (since := "2024-09-23")]
 protected def UInt8.modn (a : UInt8) (n : Nat) : UInt8 := ⟨Fin.modn a.toFin n⟩
@@ -297,6 +299,8 @@ Examples:
 -/
 @[extern "lean_uint16_mod"]
 protected def UInt16.mod (a b : UInt16) : UInt16 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+
+-- Note: This is deprecated, but still used in the `HMod` instance below.
 set_option linter.missingDocs false in
 @[deprecated UInt16.mod (since := "2024-09-23")]
 protected def UInt16.modn (a : UInt16) (n : Nat) : UInt16 := ⟨Fin.modn a.toFin n⟩
@@ -511,6 +515,8 @@ Examples:
 -/
 @[extern "lean_uint32_mod"]
 protected def UInt32.mod (a b : UInt32) : UInt32 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+
+-- Note: This is deprecated, but still used in the `HMod` instance below.
 set_option linter.missingDocs false in
 @[deprecated UInt32.mod (since := "2024-09-23")]
 protected def UInt32.modn (a : UInt32) (n : Nat) : UInt32 := ⟨Fin.modn a.toFin n⟩
@@ -687,6 +693,8 @@ Examples:
 -/
 @[extern "lean_uint64_mod"]
 protected def UInt64.mod (a b : UInt64) : UInt64 := ⟨BitVec.umod a.toBitVec b.toBitVec⟩
+
+-- Note: This is deprecated, but still used in the `HMod` instance below.
 set_option linter.missingDocs false in
 @[deprecated UInt64.mod (since := "2024-09-23")]
 protected def UInt64.modn (a : UInt64) (n : Nat) : UInt64 := ⟨Fin.modn a.toFin n⟩
@@ -894,6 +902,8 @@ Examples:
 -/
 @[extern "lean_usize_mod"]
 protected def USize.mod (a b : USize) : USize := ⟨a.toBitVec % b.toBitVec⟩
+
+-- Note: This is deprecated, but still used in the `HMod` instance below.
 set_option linter.missingDocs false in
 @[deprecated USize.mod (since := "2024-09-23")]
 protected def USize.modn (a : USize) (n : Nat) : USize := ⟨Fin.modn a.toFin n⟩
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index df4057ecb4..84e29067d6 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -184,20 +184,6 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
       · apply toNat_lt_size
       · simpa using h2
 
-  open $typeName (toNat_mod_lt modn) in
-  set_option linter.deprecated false in
-  @[deprecated toNat_mod_lt (since := "2024-09-24")]
-  protected theorem modn_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % m) < m := by
-    intro u
-    simp only [(· % ·)]
-    simp only [gt_iff_lt, toNat, modn, Fin.modn_val, BitVec.natCast_eq_ofNat, BitVec.toNat_ofNat,
-      Nat.reducePow]
-    rw [Nat.mod_eq_of_lt]
-    · apply Nat.mod_lt
-    · apply Nat.lt_of_le_of_lt
-      · apply Nat.mod_le
-      · apply Fin.is_lt
-
   protected theorem mod_lt (a : $typeName) {b : $typeName} : 0 < b → a % b < b := by
     simp only [lt_iff_toBitVec_lt, mod_def]
     apply BitVec.umod_lt
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index 55985e07f2..a93f5b0602 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -65,10 +65,6 @@ end Term
 
 def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool
 
-/-- Deprecated - `DerivingHandler` no longer assumes arguments -/
-@[deprecated DerivingHandler (since := "2024-09-09")]
-def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool
-
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler)) ← IO.mkRef {}
 
 /-- A `DerivingHandler` is called on the fully qualified names of all types it is running for
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index 225a50cec2..04593c88b6 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -131,18 +131,12 @@ Will NOT cause the whole build to fail if the release cannot be fetched.
 -/
 builtin_facet optGitHubReleaseFacet @ optRelease : Package => Bool
 
-@[deprecated optGitHubReleaseFacet (since := "2024-09-27")]
-abbrev Package.optReleaseFacet := optGitHubReleaseFacet
-
 /--
 A package's build archive from a GitHub release.
 Will cause the whole build to fail if the release cannot be fetched.
 -/
 builtin_facet gitHubReleaseFacet @ release : Package => Unit
 
-@[deprecated gitHubReleaseFacet (since := "2024-09-27")]
-abbrev Package.releaseFacet := gitHubReleaseFacet
-
 /-- A package's `extraDepTargets` mixed with its transitive dependencies'. -/
 builtin_facet extraDep : Package => Unit
 
diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean
index 2a057d7a57..d8bed677aa 100644
--- a/src/lake/Lake/Build/Info.lean
+++ b/src/lake/Lake/Build/Info.lean
@@ -277,12 +277,6 @@ abbrev gitHubRelease (self : Package) : BuildInfo :=
 abbrev optGitHubRelease (self : Package) : BuildInfo :=
   self.facetCore optGitHubReleaseFacet
 
-@[deprecated gitHubRelease (since := "2024-09-27")]
-abbrev release := @gitHubRelease
-
-@[deprecated optGitHubRelease (since := "2024-09-27")]
-abbrev optRelease := @optGitHubRelease
-
 @[inherit_doc extraDepFacet]
 abbrev extraDep (self : Package) : BuildInfo :=
   self.facetCore extraDepFacet
diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index 3ca2af008d..f2a67516b0 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -93,9 +93,6 @@ def Package.maybeFetchBuildCacheWithWarning (self : Package) := do
         let details ← self.optFacetDetails optReservoirBarrelFacet
         logVerbose s!"building from source; failed to fetch Reservoir build{details}"
 
-@[deprecated maybeFetchBuildCacheWithWarning (since := "2024-09-27")]
-def Package.fetchOptRelease := @maybeFetchBuildCacheWithWarning
-
 /--
 Build the `extraDepTargets` for the package.
 Also, if the package is a dependency, maybe fetch its build cache.
@@ -198,16 +195,10 @@ def Package.barrelFacetConfig : PackageFacetConfig reservoirBarrelFacet :=
 def Package.optGitHubReleaseFacetConfig : PackageFacetConfig optGitHubReleaseFacet :=
   mkOptBuildArchiveFacetConfig buildArchiveFile getReleaseUrl
 
-@[deprecated optGitHubReleaseFacetConfig (since := "2024-09-27")]
-abbrev Package.optReleaseFacetConfig := optGitHubReleaseFacetConfig
-
 /-- The `PackageFacetConfig` for the builtin `gitHubReleaseFacet`. -/
 def Package.gitHubReleaseFacetConfig : PackageFacetConfig gitHubReleaseFacet :=
   mkBuildArchiveFacetConfig optGitHubReleaseFacet "GitHub release"
 
-@[deprecated gitHubReleaseFacetConfig (since := "2024-09-27")]
-abbrev Package.releaseFacetConfig := gitHubReleaseFacetConfig
-
 /--
 Perform a build job after first checking for an (optional) cached build
 for the package (e.g., from Reservoir or GitHub).
@@ -220,9 +211,6 @@ def Package.afterBuildCacheAsync (self : Package) (build : JobM (Job α)) : Fetc
   else
     build
 
-@[deprecated afterBuildCacheAsync (since := "2024-09-27")]
-def Package.afterReleaseAsync := @afterBuildCacheAsync
-
 /--
  Perform a build after first checking for an (optional) cached build
  for the package (e.g., from Reservoir or GitHub).
@@ -235,9 +223,6 @@ def Package.afterBuildCacheSync (self : Package) (build : JobM α) : FetchM (Job
   else
     Job.async build
 
-@[deprecated afterBuildCacheSync (since := "2024-09-27")]
-def Package.afterReleaseSync := @afterBuildCacheSync
-
 /--
 A name-configuration map for the initial set of
 Lake package facets (e.g., `extraDep`).
diff --git a/tests/lean/run/4230.lean b/tests/lean/run/4230.lean
index a4c84df478..240ce46453 100644
--- a/tests/lean/run/4230.lean
+++ b/tests/lean/run/4230.lean
@@ -16,7 +16,7 @@ theorem foo (curr : Nat) (input : Array Nat) (output : Array Nat)
   unfold copy
   split
   . rw [foo]
-    . rw [Array.get_push_lt]
+    . rw [Array.getElem_push_lt]
     . omega
   . rfl
 termination_by?
diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean
index 7ecd652728..9f78080b92 100644
--- a/tests/lean/run/bigop.lean
+++ b/tests/lean/run/bigop.lean
@@ -22,8 +22,8 @@ class Enumerable (α : Type) where
 instance : Enumerable Bool where
   elems := [false, true]
 
-instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) where
-  elems := Enumerable.elems.bind fun (a : α) => Enumerable.elems.bind fun (b : β) => [(a, b)]
+instance {α β} [Enumerable α] [Enumerable β] : Enumerable (α × β) where
+  elems := Enumerable.elems.flatMap fun (a : α) => Enumerable.elems.flatMap fun (b : β) => [(a, b)]
 
 def finElems (n : Nat) : List (Fin n) :=
   match n with
diff --git a/tests/lean/run/simpHigherOrder.lean b/tests/lean/run/simpHigherOrder.lean
index d6e4ef96a3..7ced4facac 100644
--- a/tests/lean/run/simpHigherOrder.lean
+++ b/tests/lean/run/simpHigherOrder.lean
@@ -14,23 +14,27 @@ example (l : List Nat)  :
 
 theorem foldr_to_sum (l : List Nat) (f : Nat → Nat → Nat) (g : Nat → Nat)
   (h : ∀ acc x, f x acc = g x + acc) :
-  l.foldr f 0 = Nat.sum (l.map g) := by
-  rw [Nat.sum, List.foldr_map]
+  l.foldr f 0 = List.sum (l.map g) := by
+  rw [List.sum, List.foldr_map]
   congr
   funext x acc
   apply h
 
 -- this works:
 example (l : List Nat) :
-  l.foldr (fun x a => x*x + a) 0 = Nat.sum (l.map (fun x => x * x)) := by
+  l.foldr (fun x a => x*x + a) 0 = List.sum (l.map (fun x => x * x)) := by
   simp [foldr_to_sum]
 
 -- this does not, so such a pattern is still quite fragile
 
-/-- error: simp made no progress -/
+/--
+error: unsolved goals
+l : List Nat
+⊢ List.foldr (fun x a => a + x * x) 0 l = (List.map (fun x => x * x) l).sum
+-/
 #guard_msgs in
 example (l : List Nat) :
-  l.foldr (fun x a => a + x*x) 0 = Nat.sum (l.map (fun x => x * x)) := by
+  l.foldr (fun x a => a + x*x) 0 = List.sum (l.map (fun x => x * x)) := by
   simp [foldr_to_sum]
 
 -- but with stronger simp normal forms, it would work:
@@ -39,7 +43,7 @@ example (l : List Nat) :
 theorem add_eq_add_cancel (a x y : Nat) : (a + x = y + a) ↔  (x = y) := by omega
 
 example (l : List Nat) :
-  l.foldr (fun x a => a + x*x) 0 = Nat.sum (l.map (fun x => x * x)) := by
+  l.foldr (fun x a => a + x*x) 0 = List.sum (l.map (fun x => x * x)) := by
   simp [foldr_to_sum]