diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 0e034e2af6..0a52edefce 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -1165,7 +1165,7 @@ Examples:
 def zipIdx (xs : Array α) (start := 0) : Array (α × Nat) :=
   xs.mapIdx fun i a => (a, start + i)
 
-@[deprecated zipIdx (since := "2025-01-21")] abbrev zipWithIndex := @zipIdx
+
 
 /--
 Returns the first element of the array for which the predicate `p` returns `true`, or `none` if no
@@ -1322,8 +1322,7 @@ def idxOfAux [BEq α] (xs : Array α) (v : α) (i : Nat) : Option (Fin xs.size)
   else none
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-@[deprecated idxOfAux (since := "2025-01-29")]
-abbrev indexOfAux := @idxOfAux
+
 
 /--
 Returns the index of the first element equal to `a`, or the size of the array if no element is equal
@@ -1338,8 +1337,7 @@ Examples:
 def finIdxOf? [BEq α] (xs : Array α) (v : α) : Option (Fin xs.size) :=
   idxOfAux xs v 0
 
-@[deprecated "`Array.indexOf?` has been deprecated, use `idxOf?` or `finIdxOf?` instead." (since := "2025-01-29")]
-abbrev indexOf? := @finIdxOf?
+
 
 /--
 Returns the index of the first element equal to `a`, or the size of the array if no element is equal
diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index 479a4054dc..a16e3b6f81 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -123,15 +123,9 @@ abbrev pop_toList := @Array.toList_pop
 @[simp, grind =] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
   apply ext'; simp only [toList_append, List.append_nil]
 
-@[deprecated append_empty (since := "2025-01-13")]
-abbrev append_nil := @append_empty
-
 @[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
   apply ext'; simp only [toList_append, List.nil_append]
 
-@[deprecated empty_append (since := "2025-01-13")]
-abbrev nil_append := @empty_append
-
 @[simp, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
@@ -142,7 +136,6 @@ abbrev nil_append := @empty_append
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing xs <;> simp [*]
 
-@[deprecated toList_appendList (since := "2024-12-11")]
-abbrev appendList_toList := @toList_appendList
+
 
 end Array
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 2ed9bc44da..e40c96e1e6 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -837,16 +837,10 @@ theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α}
   cases as
   simp
 
-@[deprecated mem_of_contains_eq_true (since := "2024-12-12")]
-abbrev mem_of_elem_eq_true := @mem_of_contains_eq_true
-
 theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true := by
   cases as
   simpa using h
 
-@[deprecated contains_eq_true_of_mem (since := "2024-12-12")]
-abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
-
 @[simp] theorem elem_eq_contains [BEq α] {a : α} {xs : Array α} :
     elem a xs = xs.contains a := by
   simp [elem]
@@ -904,15 +898,9 @@ theorem all_push {xs : Array α} {a : α} {p : α → Bool} :
   cases xs
   simp
 
-@[deprecated getElem_set_self (since := "2024-12-11")]
-abbrev getElem_set_eq := @getElem_set_self
-
 @[simp] theorem getElem?_set_self {xs : Array α} {i : Nat} (h : i < xs.size) {v : α} :
     (xs.set i v)[i]? = some v := by simp [h]
 
-@[deprecated getElem?_set_self (since := "2024-12-11")]
-abbrev getElem?_set_eq := @getElem?_set_self
-
 @[simp] theorem getElem_set_ne {xs : Array α} {i : Nat} (h' : i < xs.size) {v : α} {j : Nat}
     (pj : j < xs.size) (h : i ≠ j) :
     (xs.set i v)[j]'(by simp [*]) = xs[j] := by
@@ -1003,9 +991,6 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
 theorem setIfInBounds_def (xs : Array α) (i : Nat) (a : α) :
     xs.setIfInBounds i a = if h : i < xs.size then xs.set i a else xs := rfl
 
-@[deprecated set!_eq_setIfInBounds (since := "2024-12-12")]
-abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds
-
 @[simp, grind] theorem size_setIfInBounds {xs : Array α} {i : Nat} {a : α} :
     (xs.setIfInBounds i a).size = xs.size := by
   if h : i < xs.size  then
@@ -1027,9 +1012,6 @@ abbrev set!_is_setIfInBounds := @set!_eq_setIfInBounds
   simp at h
   simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_self]
 
-@[deprecated getElem_setIfInBounds_self (since := "2024-12-11")]
-abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
-
 @[simp] theorem getElem_setIfInBounds_ne {xs : Array α} {i : Nat} {a : α} {j : Nat}
     (hj : j < xs.size) (h : i ≠ j) :
     (xs.setIfInBounds i a)[j]'(by simpa using hj) = xs[j] := by
@@ -1049,9 +1031,6 @@ theorem getElem?_setIfInBounds_self_of_lt {xs : Array α} {i : Nat} {a : α} (h
     (xs.setIfInBounds i a)[i]? = some a := by
   simp [h]
 
-@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
-abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
-
 @[simp] theorem getElem?_setIfInBounds_ne {xs : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
     (xs.setIfInBounds i a)[j]? = xs[j]? := by
   simp [getElem?_setIfInBounds, h]
@@ -1377,23 +1356,6 @@ theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] {f : α → m β} {xs : Ar
     toList <$> xs.mapM f = xs.toList.mapM f := by
   simp [mapM_eq_mapM_toList]
 
-@[deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]
-theorem mapM_map_eq_foldl {as : Array α} {f : α → β} {i : Nat} :
-    mapM.map (m := Id) (pure <| f ·) as i b = pure (as.foldl (start := i) (fun acc a => acc.push (f a)) b) := by
-  unfold mapM.map
-  split <;> rename_i h
-  · ext : 1
-    dsimp [foldl, foldlM]
-    rw [mapM_map_eq_foldl, dif_pos (by omega), foldlM.loop, dif_pos h]
-    -- Calling `split` here gives a bad goal.
-    have : size as - i = Nat.succ (size as - i - 1) := by omega
-    rw [this]
-    simp [foldl, foldlM, Nat.sub_add_eq]
-  · dsimp [foldl, foldlM]
-    rw [dif_pos (by omega), foldlM.loop, dif_neg h]
-    rfl
-termination_by as.size - i
-
 /--
 Use this as `induction ass using array₂_induction` on a hypothesis of the form `ass : Array (Array α)`.
 The hypothesis `ass` will be replaced with a hypothesis `ass : List (List α)`,
@@ -2999,9 +2961,6 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} :
   · rw [size_extract, Nat.min_self, Nat.sub_zero]
   · intros; rw [getElem_extract]; congr; rw [Nat.zero_add]
 
-@[deprecated extract_size (since := "2025-01-19")]
-abbrev extract_all := @extract_size
-
 theorem extract_empty_of_stop_le_start {xs : Array α} {start stop : Nat} (h : stop ≤ start) :
     xs.extract start stop = #[] := by
   simp only [extract, Nat.sub_eq, emptyWithCapacity_eq]
@@ -4734,27 +4693,10 @@ end List
 /-! ### Deprecations -/
 namespace Array
 
-@[deprecated size_toArray (since := "2024-12-11")]
-theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp
-
-@[deprecated getElem?_eq_getElem (since := "2024-12-11")]
-theorem getElem?_lt
-    (xs : Array α) {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] := dif_pos h
-
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
-theorem getElem?_ge
-    (xs : Array α) {i : Nat} (h : i ≥ xs.size) : xs[i]? = none := dif_neg (Nat.not_lt_of_le h)
-
 set_option linter.deprecated false in
 @[deprecated "`get?` is deprecated" (since := "2025-02-12"), simp]
 theorem get?_eq_getElem? (xs : Array α) (i : Nat) : xs.get? i = xs[i]? := rfl
 
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
-theorem getElem?_len_le (xs : Array α) {i : Nat} (h : xs.size ≤ i) : xs[i]? = none := by
-  simp [h]
-
-@[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
-
 @[deprecated getD_eq_getD_getElem? (since := "2025-02-12")] abbrev getD_eq_get? := @getD_eq_getD_getElem?
 
 set_option linter.deprecated false in
@@ -4779,64 +4721,9 @@ 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_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 Array.getElem_toList (since := "2024-12-08")]
-theorem getElem_eq_getElem_toList {xs : Array α} (h : i < xs.size) : xs[i] = xs.toList[i] := rfl
-
-@[deprecated Array.getElem?_toList (since := "2024-12-08")]
-theorem getElem?_eq_getElem?_toList (xs : Array α) (i : Nat) : xs[i]? = xs.toList[i]? := by
-  rw [getElem?_def]
-  split <;> simp_all
-
-@[deprecated LawfulGetElem.getElem?_def (since := "2024-12-08")]
-theorem getElem?_eq {xs : Array α} {i : Nat} :
-    xs[i]? = if h : i < xs.size then some xs[i] else none := by
-  rw [getElem?_def]
-
-/-! ### map -/
-
-@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]
-theorem map_induction (xs : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0)
-    (p : Fin xs.size → β → Prop) (hs : ∀ i, motive i.1 → p i (f xs[i]) ∧ motive (i+1)) :
-    motive xs.size ∧
-      ∃ eq : (xs.map f).size = xs.size, ∀ i h, p ⟨i, h⟩ ((xs.map f)[i]) := by
-  have t := foldl_induction (as := xs) (β := Array β)
-    (motive := fun i xs => motive i ∧ xs.size = i ∧ ∀ i h2, p i xs[i.1])
-    (init := #[]) (f := fun acc a => acc.push (f a)) ?_ ?_
-  obtain ⟨m, eq, w⟩ := t
-  · refine ⟨m, by simp, ?_⟩
-    intro i h
-    simp only [eq] at w
-    specialize w ⟨i, h⟩ h
-    simpa using w
-  · exact ⟨h0, rfl, nofun⟩
-  · intro i bs ⟨m, ⟨eq, w⟩⟩
-    refine ⟨?_, ?_, ?_⟩
-    · exact (hs _ m).2
-    · simp_all
-    · intro j h
-      simp at h ⊢
-      by_cases h' : j < size bs
-      · rw [getElem_push]
-        simp_all
-      · rw [getElem_push, dif_neg h']
-        simp only [show j = i by omega]
-        exact (hs _ m).1
-
-set_option linter.deprecated false in
-@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]
-theorem map_spec (xs : Array α) (f : α → β) (p : Fin xs.size → β → Prop)
-    (hs : ∀ i, p i (f xs[i])) :
-    ∃ eq : (xs.map f).size = xs.size, ∀ i h, p ⟨i, h⟩ ((xs.map f)[i]) := by
-  simpa using map_induction xs f (fun _ => True) trivial p (by simp_all)
-
 /-! ### set -/
 
-@[deprecated getElem?_set_eq (since := "2025-02-27")] abbrev get?_set_eq := @getElem?_set_self
+@[deprecated getElem?_set_self (since := "2025-02-27")] abbrev get?_set_eq := @getElem?_set_self
 @[deprecated getElem?_set_ne (since := "2025-02-27")] abbrev get?_set_ne := @getElem?_set_ne
 @[deprecated getElem?_set (since := "2025-02-27")] abbrev get?_set := @getElem?_set
 @[deprecated get_set (since := "2025-02-27")] abbrev get_set := @getElem_set
diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean
index f425d9aa94..ee6150a800 100644
--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -60,7 +60,7 @@ theorem mapFinIdx_spec {xs : Array α} {f : (i : Nat) → α → (h : i < xs.siz
 @[simp, grind =] theorem size_zipIdx {xs : Array α} {k : Nat} : (xs.zipIdx k).size = xs.size :=
   Array.size_mapFinIdx
 
-@[deprecated size_zipIdx (since := "2025-01-21")] abbrev size_zipWithIndex := @size_zipIdx
+
 
 @[simp, grind =] theorem getElem_mapFinIdx {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} {i : Nat}
     (h : i < (xs.mapFinIdx f).size) :
@@ -132,23 +132,20 @@ namespace Array
     (xs.zipIdx k)[i] = (xs[i]'(by simp_all), k + i) := by
   simp [zipIdx]
 
-@[deprecated getElem_zipIdx (since := "2025-01-21")]
-abbrev getElem_zipWithIndex := @getElem_zipIdx
+
 
 @[simp, grind =] theorem zipIdx_toArray {l : List α} {k : Nat} :
     l.toArray.zipIdx k = (l.zipIdx k).toArray := by
   ext i hi₁ hi₂ <;> simp
 
-@[deprecated zipIdx_toArray (since := "2025-01-21")]
-abbrev zipWithIndex_toArray := @zipIdx_toArray
+
 
 @[simp, grind =] theorem toList_zipIdx {xs : Array α} {k : Nat} :
     (xs.zipIdx k).toList = xs.toList.zipIdx k := by
   rcases xs with ⟨xs⟩
   simp
 
-@[deprecated toList_zipIdx (since := "2025-01-21")]
-abbrev toList_zipWithIndex := @toList_zipIdx
+
 
 theorem mk_mem_zipIdx_iff_le_and_getElem?_sub {k i : Nat} {x : α} {xs : Array α} :
     (x, i) ∈ xs.zipIdx k ↔ k ≤ i ∧ xs[i - k]? = some x := by
@@ -173,11 +170,7 @@ theorem mem_zipIdx_iff_getElem? {x : α × Nat} {xs : Array α} :
     x ∈ xs.zipIdx ↔ xs[x.2]? = some x.1 := by
   rw [mk_mem_zipIdx_iff_getElem?]
 
-@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
-abbrev mk_mem_zipWithIndex_iff_getElem? := @mk_mem_zipIdx_iff_getElem?
 
-@[deprecated mem_zipIdx_iff_getElem? (since := "2025-01-21")]
-abbrev mem_zipWithIndex_iff_getElem? := @mem_zipIdx_iff_getElem?
 
 /-! ### mapFinIdx -/
 
@@ -222,8 +215,7 @@ theorem mapFinIdx_eq_zipIdx_map {xs : Array α} {f : (i : Nat) → α → (h : i
         f i x (by simp [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
   ext <;> simp
 
-@[deprecated mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]
-abbrev mapFinIdx_eq_zipWithIndex_map := @mapFinIdx_eq_zipIdx_map
+
 
 @[simp]
 theorem mapFinIdx_eq_empty_iff {xs : Array α} {f : (i : Nat) → α → (h : i < xs.size) → β} :
@@ -332,8 +324,7 @@ theorem mapIdx_eq_zipIdx_map {xs : Array α} {f : Nat → α → β} :
     xs.mapIdx f = xs.zipIdx.map fun ⟨a, i⟩ => f i a := by
   ext <;> simp
 
-@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-21")]
-abbrev mapIdx_eq_zipWithIndex_map := @mapIdx_eq_zipIdx_map
+
 
 @[grind =]
 theorem mapIdx_append {xs ys : Array α} :
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index dc6425d3aa..2eb9e9c1b8 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -5842,13 +5842,8 @@ set_option linter.missingDocs false
 @[deprecated toFin_uShiftRight (since := "2025-02-18")]
 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 replicate_zero (since := "2025-01-08")]
-abbrev replicate_zero_eq := @replicate_zero
 
-@[deprecated replicate_succ (since := "2025-01-08")]
-abbrev replicate_succ_eq := @replicate_succ
+
 
 end BitVec
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index f6fcd6c77c..f01e65d6d9 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -242,8 +242,7 @@ instance instLT [LT α] : LT (List α) := ⟨List.lt⟩
 instance decidableLT [DecidableEq α] [LT α] [DecidableLT α] (l₁ l₂ : List α) :
     Decidable (l₁ < l₂) := decidableLex (· < ·) l₁ l₂
 
-@[deprecated decidableLT (since := "2024-12-13"), inherit_doc decidableLT]
-abbrev hasDecidableLt := @decidableLT
+
 
 /--
 Non-strict ordering of lists with respect to a strict ordering of their elements.
@@ -1722,14 +1721,8 @@ Examples:
 -/
 def idxOf [BEq α] (a : α) : List α → Nat := findIdx (· == a)
 
-/-- Returns the index of the first element equal to `a`, or the length of the list otherwise. -/
-@[deprecated idxOf (since := "2025-01-29")] abbrev indexOf := @idxOf
-
 @[simp] theorem idxOf_nil [BEq α] : ([] : List α).idxOf x = 0 := rfl
 
-@[deprecated idxOf_nil (since := "2025-01-29")]
-theorem indexOf_nil [BEq α] : ([] : List α).idxOf x = 0 := rfl
-
 /-! ### findIdx? -/
 
 /--
@@ -1760,10 +1753,6 @@ Examples:
 -/
 @[inline] def idxOf? [BEq α] (a : α) : List α → Option Nat := findIdx? (· == a)
 
-/-- Return the index of the first occurrence of `a` in the list. -/
-@[deprecated idxOf? (since := "2025-01-29")]
-abbrev indexOf? := @idxOf?
-
 /-! ### findFinIdx? -/
 
 /--
@@ -2119,22 +2108,6 @@ def range' : (start len : Nat) → (step : Nat := 1) → List Nat
   | _, 0, _ => []
   | s, n+1, step => s :: range' (s+step) n step
 
-/-! ### iota -/
-
-/--
-`O(n)`. `iota n` is the numbers from `1` to `n` inclusive, in decreasing order.
-* `iota 5 = [5, 4, 3, 2, 1]`
--/
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
-def iota : Nat → List Nat
-  | 0       => []
-  | m@(n+1) => m :: iota n
-
-set_option linter.deprecated false in
-@[simp] theorem iota_zero : iota 0 = [] := rfl
-set_option linter.deprecated false in
-@[simp] theorem iota_succ : iota (i+1) = (i+1) :: iota i := rfl
-
 /-! ### zipIdx -/
 
 /--
@@ -2153,38 +2126,6 @@ def zipIdx : (l : List α) → (n : Nat := 0) → List (α × Nat)
 @[simp] theorem zipIdx_nil : ([] : List α).zipIdx i = [] := rfl
 @[simp] theorem zipIdx_cons : (a::as).zipIdx i = (a, i) :: as.zipIdx (i+1) := rfl
 
-/-! ### enumFrom -/
-
-/--
-`O(|l|)`. `enumFrom n l` is like `enum` but it allows you to specify the initial index.
-* `enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]`
--/
-@[deprecated "Use `zipIdx` instead; note the signature change." (since := "2025-01-21")]
-def enumFrom : Nat → List α → List (Nat × α)
-  | _, [] => nil
-  | n, x :: xs   => (n, x) :: enumFrom (n + 1) xs
-
-set_option linter.deprecated false in
-@[deprecated zipIdx_nil (since := "2025-01-21"), simp]
-theorem enumFrom_nil : ([] : List α).enumFrom i = [] := rfl
-set_option linter.deprecated false in
-@[deprecated zipIdx_cons (since := "2025-01-21"), simp]
-theorem enumFrom_cons : (a::as).enumFrom i = (i, a) :: as.enumFrom (i+1) := rfl
-
-/-! ### enum -/
-
-set_option linter.deprecated false in
-/--
-`O(|l|)`. `enum l` pairs up each element with its index in the list.
-* `enum [a, b, c] = [(0, a), (1, b), (2, c)]`
--/
-@[deprecated "Use `zipIdx` instead; note the signature change." (since := "2025-01-21")]
-def enum : List α → List (Nat × α) := enumFrom 0
-
-set_option linter.deprecated false in
-@[deprecated zipIdx_nil (since := "2025-01-21"), simp]
-theorem enum_nil : ([] : List α).enum = [] := rfl
-
 /-! ## Minima and maxima -/
 
 /-! ### min? -/
@@ -2604,25 +2545,6 @@ Examples:
     exact go s n (m + 1)
   exact (go s n 0).symm
 
-/-! ### iota -/
-
-/-- Tail-recursive version of `List.iota`. -/
-@[deprecated "Use `List.range' 1 n` instead of `iota n`." (since := "2025-01-20")]
-def iotaTR (n : Nat) : List Nat :=
-  let rec go : Nat → List Nat → List Nat
-    | 0, r => r.reverse
-    | m@(n+1), r => go n (m::r)
-  go n []
-
-set_option linter.deprecated false in
-@[csimp]
-theorem iota_eq_iotaTR : @iota = @iotaTR :=
-  have aux (n : Nat) (r : List Nat) : iotaTR.go n r = r.reverse ++ iota n := by
-    induction n generalizing r with
-    | zero => simp [iota, iotaTR.go]
-    | succ n ih => simp [iota, iotaTR.go, ih, append_assoc]
-  funext fun n => by simp [iotaTR, aux]
-
 /-! ## Other list operations -/
 
 /-! ### intersperse -/
diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean
index 516dbe12fa..751ee00d77 100644
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -57,15 +57,9 @@ theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.er
       rintro x h' rfl
       simp_all
 
-@[deprecated eraseP_eq_nil_iff (since := "2025-01-30")]
-abbrev eraseP_eq_nil := @eraseP_eq_nil_iff
-
 theorem eraseP_ne_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x] := by
   simp
 
-@[deprecated eraseP_ne_nil_iff (since := "2025-01-30")]
-abbrev eraseP_ne_nil := @eraseP_ne_nil_iff
-
 theorem exists_of_eraseP : ∀ {l : List α} {a} (_ : a ∈ l) (_ : p a),
     ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁ ++ a :: l₂ ∧ l.eraseP p = l₁ ++ l₂
   | b :: l, _, al, pa =>
@@ -352,17 +346,11 @@ theorem erase_eq_eraseP [LawfulBEq α] (a : α) : ∀ (l : List α), l.erase a =
   rw [erase_eq_eraseP]
   simp
 
-@[deprecated erase_eq_nil_iff (since := "2025-01-30")]
-abbrev erase_eq_nil := @erase_eq_nil_iff
-
 theorem erase_ne_nil_iff [LawfulBEq α] {xs : List α} {a : α} :
     xs.erase a ≠ [] ↔ xs ≠ [] ∧ xs ≠ [a] := by
   rw [erase_eq_eraseP]
   simp
 
-@[deprecated erase_ne_nil_iff (since := "2025-01-30")]
-abbrev erase_ne_nil := @erase_ne_nil_iff
-
 theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
     ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂ := by
   let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _)
@@ -582,8 +570,7 @@ theorem eraseIdx_eq_take_drop_succ :
   | a::l, 0
   | a::l, i + 1 => simp
 
-@[deprecated eraseIdx_eq_nil_iff (since := "2025-01-30")]
-abbrev eraseIdx_eq_nil := @eraseIdx_eq_nil_iff
+
 
 theorem eraseIdx_ne_nil_iff {l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2 ≤ l.length ∨ (l.length = 1 ∧ i ≠ 0) := by
   match l with
@@ -591,8 +578,7 @@ theorem eraseIdx_ne_nil_iff {l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2
   | [a]
   | a::b::l => simp
 
-@[deprecated eraseIdx_ne_nil_iff (since := "2025-01-30")]
-abbrev eraseIdx_ne_nil := @eraseIdx_ne_nil_iff
+
 
 @[grind]
 theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l
@@ -700,7 +686,6 @@ theorem erase_eq_eraseIdx_of_idxOf [BEq α] [LawfulBEq α]
     rw [eq_comm, eraseIdx_eq_self]
     exact Nat.le_of_eq (idxOf_eq_length h).symm
 
-@[deprecated erase_eq_eraseIdx_of_idxOf (since := "2025-01-29")]
-abbrev erase_eq_eraseIdx_of_indexOf := @erase_eq_eraseIdx_of_idxOf
+
 
 end List
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index fd2a094125..6ef1c81604 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -1098,15 +1098,9 @@ theorem idxOf_cons [BEq α] :
   dsimp [idxOf]
   simp [findIdx_cons]
 
-@[deprecated idxOf_cons (since := "2025-01-29")]
-abbrev indexOf_cons := @idxOf_cons
-
 @[simp] theorem idxOf_cons_self [BEq α] [ReflBEq α] {l : List α} : (a :: l).idxOf a = 0 := by
   simp [idxOf_cons]
 
-@[deprecated idxOf_cons_self (since := "2025-01-29")]
-abbrev indexOf_cons_self := @idxOf_cons_self
-
 @[grind =]
 theorem idxOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
     (l₁ ++ l₂).idxOf a = if a ∈ l₁ then l₁.idxOf a else l₂.idxOf a + l₁.length := by
@@ -1117,8 +1111,7 @@ theorem idxOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
   · rw [if_neg]
     simpa using h
 
-@[deprecated idxOf_append (since := "2025-01-29")]
-abbrev indexOf_append := @idxOf_append
+
 
 theorem idxOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.idxOf a = l.length := by
   induction l with
@@ -1128,8 +1121,7 @@ theorem idxOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.
     simp only [idxOf_cons, cond_eq_if, beq_iff_eq]
     split <;> simp_all
 
-@[deprecated idxOf_eq_length (since := "2025-01-29")]
-abbrev indexOf_eq_length := @idxOf_eq_length
+
 
 theorem idxOf_lt_length_of_mem [BEq α] [EquivBEq α] {l : List α} (h : a ∈ l) : l.idxOf a < l.length := by
   induction l with
@@ -1159,8 +1151,7 @@ theorem idxOf_lt_length_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
 
 grind_pattern idxOf_lt_length_iff => l.idxOf a, l.length
 
-@[deprecated idxOf_lt_length_of_mem (since := "2025-01-29")]
-abbrev indexOf_lt_length := @idxOf_lt_length_of_mem
+
 
 /-! ### finIdxOf?
 
@@ -1231,8 +1222,7 @@ The lemmas below should be made consistent with those for `findIdx?` (and proved
   · rintro w x h rfl
     contradiction
 
-@[deprecated idxOf?_eq_none_iff (since := "2025-01-29")]
-abbrev indexOf?_eq_none_iff := @idxOf?_eq_none_iff
+
 
 @[simp, grind =]
 theorem isSome_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
diff --git a/src/Init/Data/List/Impl.lean b/src/Init/Data/List/Impl.lean
index f3724757f8..4183198f2a 100644
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -564,24 +564,7 @@ def zipIdxTR (l : List α) (n : Nat := 0) : List (α × Nat) :=
 
 /-! ### enumFrom -/
 
-/-- Tail recursive version of `List.enumFrom`. -/
-@[deprecated zipIdxTR (since := "2025-01-21")]
-def enumFromTR (n : Nat) (l : List α) : List (Nat × α) :=
-  let as := l.toArray
-  (as.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + as.size, [])).2
 
-set_option linter.deprecated false in
-@[deprecated zipIdx_eq_zipIdxTR (since := "2025-01-21"), csimp]
-theorem enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR := by
-  funext α n l; simp only [enumFromTR]
-  let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
-  let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
-    | [], n => rfl
-    | a::as, n => by
-      rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., foldr, go as]
-      simp [enumFrom, f]
-  rw [← Array.foldr_toList]
-  simp +zetaDelta [go]
 
 /-! ## Other list operations -/
 
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index a04524b274..a88c49f835 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1586,9 +1586,7 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t :=
   mt mem_append.1 $ not_or.mpr ⟨h₁, h₂⟩
 
-@[deprecated mem_append (since := "2025-01-13")]
-theorem mem_append_eq {a : α} {s t : List α} : (a ∈ s ++ t) = (a ∈ s ∨ a ∈ t) :=
-  propext mem_append
+
 
 /--
 See also `eq_append_cons_of_mem`, which proves a stronger version
@@ -1698,7 +1696,7 @@ theorem getLast_concat {a : α} : ∀ {l : List α}, getLast (l ++ [a]) (by simp
 @[simp] theorem append_eq_nil_iff : p ++ q = [] ↔ p = [] ∧ q = [] := by
   cases p <;> simp
 
-@[deprecated append_eq_nil_iff (since := "2025-01-13")] abbrev append_eq_nil := @append_eq_nil_iff
+
 
 theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
   simp
@@ -2268,8 +2266,7 @@ theorem map_const' {l : List α} {b : β} : map (fun _ => b) l = replicate l.len
     simp only [mem_append, mem_replicate, ne_eq]
     rintro (⟨-, rfl⟩ | ⟨_, rfl⟩) <;> rfl
 
-@[deprecated replicate_append_replicate (since := "2025-01-16")]
-abbrev append_replicate_replicate := @replicate_append_replicate
+
 
 theorem append_eq_replicate_iff {l₁ l₂ : List α} {a : α} :
     l₁ ++ l₂ = replicate n a ↔
@@ -2657,8 +2654,6 @@ theorem foldl_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   · simp
   · simp [*]
 
-@[deprecated foldl_map_hom (since := "2025-01-20")] abbrev foldl_map' := @foldl_map_hom
-
 theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β → β} {a : α} {l : List α}
     (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
     (l.map g).foldr f' (g a) = g (l.foldr f a) := by
@@ -2666,8 +2661,6 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   · simp
   · simp [*]
 
-@[deprecated foldr_map_hom (since := "2025-01-20")] abbrev foldr_map' := @foldr_map_hom
-
 @[simp] theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b : β} {l l' : List α} :
     (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
   induction l <;> simp [*]
@@ -3735,12 +3728,6 @@ theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a :=
 
 /-! ### Deprecations -/
 
-@[deprecated _root_.isSome_getElem? (since := "2024-12-09")]
-theorem isSome_getElem? {l : List α} {i : Nat} : l[i]?.isSome ↔ i < l.length := by
-  simp
 
-@[deprecated _root_.isNone_getElem? (since := "2024-12-09")]
-theorem isNone_getElem? {l : List α} {i : Nat} : l[i]?.isNone ↔ l.length ≤ i := by
-  simp
 
 end List
diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean
index 01af5ff06b..088199899d 100644
--- a/src/Init/Data/List/Lex.lean
+++ b/src/Init/Data/List/Lex.lean
@@ -163,8 +163,7 @@ instance [LT α] [Trans (· < · : α → α → Prop) (· < ·) (· < ·)] :
     Trans (· < · : List α → List α → Prop) (· < ·) (· < ·) where
   trans h₁ h₂ := List.lt_trans h₁ h₂
 
-@[deprecated List.le_antisymm (since := "2024-12-13")]
-protected abbrev lt_antisymm := @List.le_antisymm
+
 
 protected theorem lt_of_le_of_lt [LT α]
     [i₀ : Std.Irrefl (· < · : α → α → Prop)]
diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean
index b672312596..36dbe352dc 100644
--- a/src/Init/Data/List/MapIdx.lean
+++ b/src/Init/Data/List/MapIdx.lean
@@ -182,8 +182,7 @@ theorem mapFinIdx_eq_zipIdx_map {l : List α} {f : (i : Nat) → α → (h : i <
         f i x (by rw [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1) := by
   apply ext_getElem <;> simp
 
-@[deprecated mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]
-abbrev mapFinIdx_eq_zipWithIndex_map := @mapFinIdx_eq_zipIdx_map
+
 
 @[simp]
 theorem mapFinIdx_eq_nil_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
@@ -220,7 +219,7 @@ theorem mapFinIdx_eq_cons_iff {l : List α} {b : β} {f : (i : Nat) → α → (
   cases l with
   | nil => simp
   | cons x l' =>
-    simp only [mapFinIdx_cons, cons.injEq, 
+    simp only [mapFinIdx_cons, cons.injEq,
       ]
     constructor
     · rintro ⟨rfl, rfl⟩
@@ -384,8 +383,7 @@ theorem mapIdx_eq_zipIdx_map {l : List α} {f : Nat → α → β} :
   simp only [getElem?_mapIdx, Option.map, getElem?_map, getElem?_zipIdx]
   split <;> simp
 
-@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-21")]
-abbrev mapIdx_eq_enum_map := @mapIdx_eq_zipIdx_map
+
 
 @[simp, grind =]
 theorem mapIdx_cons {l : List α} {a : α} :
diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean
index 354dbbd06f..4a2579c560 100644
--- a/src/Init/Data/List/Monadic.lean
+++ b/src/Init/Data/List/Monadic.lean
@@ -261,13 +261,7 @@ theorem foldrM_filter [Monad m] [LawfulMonad m] {p : α → Bool} {g : α → β
 
 /-! ### forM -/
 
-@[deprecated forM_nil (since := "2025-01-31")]
-theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl
 
-@[deprecated forM_cons (since := "2025-01-31")]
-theorem forM_cons' [Monad m] :
-    (a::as).forM f = (f a >>= fun _ => as.forM f : m PUnit) :=
-  List.forM_cons
 
 @[simp, grind =] theorem forM_append [Monad m] [LawfulMonad m] {l₁ l₂ : List α} {f : α → m PUnit} :
     forM (l₁ ++ l₂) f = (do forM l₁ f; forM l₂ f) := by
diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean
index 6a5ca02d72..9088628db3 100644
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@@ -90,9 +90,6 @@ theorem map_sub_range' {a s : Nat} (h : a ≤ s) (n : Nat) :
   rintro rfl
   omega
 
-@[deprecated range'_eq_singleton_iff (since := "2025-01-29")]
-abbrev range'_eq_singleton := @range'_eq_singleton_iff
-
 theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k) := by
   induction n generalizing s xs ys with
   | zero => simp
@@ -230,152 +227,6 @@ theorem count_range {a n} :
   rw [range_eq_range', count_range_1']
   simp
 
-/-! ### iota -/
-
-section
-set_option linter.deprecated false
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
-theorem iota_eq_reverse_range' : ∀ n : Nat, iota n = reverse (range' 1 n)
-  | 0 => rfl
-  | n + 1 => by simp [iota, range'_concat, iota_eq_reverse_range' n, reverse_append, Nat.add_comm]
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem length_iota (n : Nat) : length (iota n) = n := by simp [iota_eq_reverse_range']
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem iota_eq_nil {n : Nat} : iota n = [] ↔ n = 0 := by
-  cases n <;> simp
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
-theorem iota_ne_nil {n : Nat} : iota n ≠ [] ↔ n ≠ 0 := by
-  cases n <;> simp
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem mem_iota {m n : Nat} : m ∈ iota n ↔ 0 < m ∧ m ≤ n := by
-  simp [iota_eq_reverse_range', Nat.add_comm, Nat.lt_succ]
-  omega
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem iota_inj : iota n = iota n' ↔ n = n' := by
-  constructor
-  · intro h
-    have h' := congrArg List.length h
-    simp at h'
-    exact h'
-  · rintro rfl
-    simp
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
-theorem iota_eq_cons_iff : iota n = a :: xs ↔ n = a ∧ 0 < n ∧ xs = iota (n - 1) := by
-  simp [iota_eq_reverse_range']
-  simp [range'_eq_append_iff, reverse_eq_iff]
-  constructor
-  · rintro ⟨k, h, rfl, h'⟩
-    rw [eq_comm, range'_eq_singleton] at h'
-    simp only [reverse_inj, range'_inj, or_true, and_true]
-    omega
-  · rintro ⟨rfl, h, rfl⟩
-    refine ⟨n - 1, by simp, rfl, ?_⟩
-    rw [eq_comm, range'_eq_singleton]
-    omega
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
-theorem iota_eq_append_iff : iota n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = (range' (k + 1) (n - k)).reverse ∧ ys = iota k := by
-  simp only [iota_eq_reverse_range']
-  rw [reverse_eq_append_iff]
-  rw [range'_eq_append_iff]
-  simp only [reverse_eq_iff]
-  constructor
-  · rintro ⟨k, h, rfl, rfl⟩
-    simp; omega
-  · rintro ⟨k, h, rfl, rfl⟩
-    exact ⟨k, by simp; omega⟩
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
-theorem pairwise_gt_iota (n : Nat) : Pairwise (· > ·) (iota n) := by
-  simpa only [iota_eq_reverse_range', pairwise_reverse] using pairwise_lt_range'
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
-theorem nodup_iota (n : Nat) : Nodup (iota n) :=
-  (pairwise_gt_iota n).imp Nat.ne_of_gt
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem head?_iota (n : Nat) : (iota n).head? = if n = 0 then none else some n := by
-  cases n <;> simp
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem head_iota (n : Nat) (h) : (iota n).head h = n := by
-  cases n with
-  | zero => simp at h
-  | succ n => simp
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem tail_iota (n : Nat) : (iota n).tail = iota (n - 1) := by
-  cases n <;> simp
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem reverse_iota : reverse (iota n) = range' 1 n := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    rw [iota_succ, reverse_cons, ih, range'_1_concat, Nat.add_comm]
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem getLast?_iota (n : Nat) : (iota n).getLast? = if n = 0 then none else some 1 := by
-  rw [getLast?_eq_head?_reverse]
-  simp [head?_range']
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem getLast_iota (n : Nat) (h) : (iota n).getLast h = 1 := by
-  rw [getLast_eq_head_reverse]
-  simp
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20")]
-theorem find?_iota_eq_none {n : Nat} {p : Nat → Bool} :
-    (iota n).find? p = none ↔ ∀ i, 0 < i → i ≤ n → !p i := by
-  simp
-
-@[deprecated "Use `(List.range' 1 n).reverse` instead of `iota n`." (since := "2025-01-20"), simp]
-theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
-    (iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j := by
-  rw [find?_eq_some_iff_append]
-  simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc, cons_append,
-    nil_append, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_reverse, mem_range'_1,
-    and_congr_right_iff]
-  intro h
-  constructor
-  · rintro ⟨as, ⟨xs, h⟩, h'⟩
-    constructor
-    · replace h : i ∈ range' 1 n := by
-        rw [h]
-        exact mem_append_cons_self
-      simpa using h
-    · rw [range'_eq_append_iff] at h
-      simp [reverse_eq_iff] at h
-      obtain ⟨k, h₁, rfl, h₂⟩ := h
-      rw [eq_comm, range'_eq_cons_iff, reverse_eq_iff] at h₂
-      obtain ⟨rfl, -, rfl⟩ := h₂
-      intro j j₁ j₂
-      apply h'
-      simp; omega
-  · rintro ⟨⟨i₁, i₂⟩, h⟩
-    refine ⟨(range' (i+1) (n-i)).reverse, ⟨(range' 1 (i-1)).reverse, ?_⟩, ?_⟩
-    · simp [← range'_succ]
-      rw [range'_eq_append_iff]
-      refine ⟨i-1, ?_⟩
-      constructor
-      · omega
-      · simp
-        omega
-    · simp
-      intros a a₁ a₂
-      apply h
-      · omega
-      · omega
-
-end
-
 /-! ### zipIdx -/
 
 @[simp, grind =]
@@ -512,237 +363,4 @@ theorem zipIdx_eq_append_iff {l : List α} {k : Nat} :
     refine ⟨l₁', l₂', range' k l₁'.length, range' (k + l₁'.length) l₂'.length, ?_⟩
     simp
 
-/-! ### enumFrom -/
-
-section
-set_option linter.deprecated false
-
-@[deprecated zipIdx_singleton (since := "2025-01-21"), simp]
-theorem enumFrom_singleton (x : α) (n : Nat) : enumFrom n [x] = [(n, x)] :=
-  rfl
-
-@[deprecated head?_zipIdx (since := "2025-01-21"), simp]
-theorem head?_enumFrom (n : Nat) (l : List α) :
-    (enumFrom n l).head? = l.head?.map fun a => (n, a) := by
-  simp [head?_eq_getElem?]
-
-@[deprecated getLast?_zipIdx (since := "2025-01-21"), simp]
-theorem getLast?_enumFrom (n : Nat) (l : List α) :
-    (enumFrom n l).getLast? = l.getLast?.map fun a => (n + l.length - 1, a) := by
-  simp [getLast?_eq_getElem?]
-  cases l <;> simp
-
-@[deprecated mk_add_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
-theorem mk_add_mem_enumFrom_iff_getElem? {n i : Nat} {x : α} {l : List α} :
-    (n + i, x) ∈ enumFrom n l ↔ l[i]? = some x := by
-  simp [mem_iff_get?]
-
-@[deprecated mk_mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-21")]
-theorem mk_mem_enumFrom_iff_le_and_getElem?_sub {n i : Nat} {x : α} {l : List α} :
-    (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = some x := by
-  if h : n ≤ i then
-    rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩
-    simp [mk_add_mem_enumFrom_iff_getElem?, Nat.add_sub_cancel_left]
-  else
-    have : ∀ k, n + k ≠ i := by rintro k rfl; simp at h
-    simp [h, mem_iff_get?, this]
-
-@[deprecated le_snd_of_mem_zipIdx (since := "2025-01-21")]
-theorem le_fst_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
-    n ≤ x.1 :=
-  (mk_mem_enumFrom_iff_le_and_getElem?_sub.1 h).1
-
-@[deprecated snd_lt_add_of_mem_zipIdx (since := "2025-01-21")]
-theorem fst_lt_add_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
-    x.1 < n + length l := by
-  rcases mem_iff_get.1 h with ⟨i, rfl⟩
-  simpa using i.isLt
-
-@[deprecated map_zipIdx (since := "2025-01-21")]
-theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
-    map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by
-  induction l generalizing n <;> simp_all
-
-@[deprecated fst_mem_of_mem_zipIdx (since := "2025-01-21")]
-theorem snd_mem_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.2 ∈ l :=
-  enumFrom_map_snd n l ▸ mem_map_of_mem h
-
-@[deprecated fst_eq_of_mem_zipIdx (since := "2025-01-21")]
-theorem snd_eq_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
-    x.2 = l[x.1 - n]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) := by
-  induction l generalizing n with
-  | nil => cases h
-  | cons hd tl ih =>
-    cases h with
-    | head _ => simp
-    | tail h m =>
-      specialize ih m
-      have : x.1 - n = x.1 - (n + 1) + 1 := by
-        have := le_fst_of_mem_enumFrom m
-        omega
-      simp [this, ih]
-
-@[deprecated mem_zipIdx (since := "2025-01-21")]
-theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enumFrom j) :
-    j ≤ i ∧ i < j + xs.length ∧
-      x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) :=
-  ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_eq_of_mem_enumFrom h⟩
-
-@[deprecated zipIdx_map (since := "2025-01-21")]
-theorem enumFrom_map (n : Nat) (l : List α) (f : α → β) :
-    enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f) := by
-  induction l with
-  | nil => rfl
-  | cons hd tl IH =>
-    rw [map_cons, enumFrom_cons', enumFrom_cons', map_cons, map_map, IH, map_map]
-    rfl
-
-@[deprecated zipIdx_append (since := "2025-01-21")]
-theorem enumFrom_append (xs ys : List α) (n : Nat) :
-    enumFrom n (xs ++ ys) = enumFrom n xs ++ enumFrom (n + xs.length) ys := by
-  induction xs generalizing ys n with
-  | nil => simp
-  | cons x xs IH =>
-    rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, Nat.add_right_comm,
-      Nat.add_assoc]
-
-@[deprecated zipIdx_eq_cons_iff (since := "2025-01-21")]
-theorem enumFrom_eq_cons_iff {l : List α} {n : Nat} :
-    l.enumFrom n = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (n, a) ∧ l' = enumFrom (n + 1) as := by
-  rw [enumFrom_eq_zip_range', zip_eq_cons_iff]
-  constructor
-  · rintro ⟨l₁, l₂, h, rfl, rfl⟩
-    rw [range'_eq_cons_iff] at h
-    obtain ⟨rfl, -, rfl⟩ := h
-    exact ⟨x.2, l₂, by simp [enumFrom_eq_zip_range']⟩
-  · rintro ⟨a, as, rfl, rfl, rfl⟩
-    refine ⟨range' (n+1) as.length, as, ?_⟩
-    simp [enumFrom_eq_zip_range', range'_succ]
-
-@[deprecated zipIdx_eq_append_iff (since := "2025-01-21")]
-theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
-    l.enumFrom n = l₁ ++ l₂ ↔
-      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enumFrom n ∧ l₂ = l₂'.enumFrom (n + l₁'.length) := by
-  rw [enumFrom_eq_zip_range', zip_eq_append_iff]
-  constructor
-  · rintro ⟨ws, xs, ys, zs, h, h', rfl, rfl, rfl⟩
-    rw [range'_eq_append_iff] at h'
-    obtain ⟨k, -, rfl, rfl⟩ := h'
-    simp only [length_range'] at h
-    obtain rfl := h
-    refine ⟨ys, zs, rfl, ?_⟩
-    simp only [enumFrom_eq_zip_range', length_append, true_and]
-    congr
-    omega
-  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
-    simp only [enumFrom_eq_zip_range']
-    refine ⟨range' n l₁'.length, range' (n + l₁'.length) l₂'.length, l₁', l₂', ?_⟩
-    simp
-
-end
-
-/-! ### enum -/
-
-section
-set_option linter.deprecated false
-
-@[deprecated zipIdx_eq_nil_iff (since := "2025-01-21"), simp]
-theorem enum_eq_nil_iff {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
-
-@[deprecated zipIdx_singleton (since := "2025-01-21"), simp]
-theorem enum_singleton (x : α) : enum [x] = [(0, x)] := rfl
-
-@[deprecated length_zipIdx (since := "2025-01-21"), simp]
-theorem enum_length : (enum l).length = l.length :=
-  enumFrom_length
-
-@[deprecated getElem?_zipIdx (since := "2025-01-21"), simp]
-theorem getElem?_enum (l : List α) (i : Nat) : (enum l)[i]? = l[i]?.map fun a => (i, a) := by
-  rw [enum, getElem?_enumFrom, Nat.zero_add]
-
-@[deprecated getElem_zipIdx (since := "2025-01-21"), simp]
-theorem getElem_enum (l : List α) (i : Nat) (h : i < l.enum.length) :
-    l.enum[i] = (i, l[i]'(by simpa [enum_length] using h)) := by
-  simp [enum]
-
-@[deprecated head?_zipIdx (since := "2025-01-21"), simp] theorem head?_enum (l : List α) :
-    l.enum.head? = l.head?.map fun a => (0, a) := by
-  simp [head?_eq_getElem?]
-
-@[deprecated getLast?_zipIdx (since := "2025-01-21"), simp]
-theorem getLast?_enum (l : List α) :
-    l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a) := by
-  simp [getLast?_eq_getElem?]
-
-@[deprecated tail_zipIdx (since := "2025-01-21"), simp]
-theorem tail_enum (l : List α) : (enum l).tail = enumFrom 1 l.tail := by
-  simp [enum]
-
-@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-21")]
-theorem mk_mem_enum_iff_getElem? {i : Nat} {x : α} {l : List α} : (i, x) ∈ enum l ↔ l[i]? = some x := by
-  simp [enum, mk_mem_enumFrom_iff_le_and_getElem?_sub]
-
-@[deprecated mem_zipIdx_iff_getElem? (since := "2025-01-21")]
-theorem mem_enum_iff_getElem? {x : Nat × α} {l : List α} : x ∈ enum l ↔ l[x.1]? = some x.2 :=
-  mk_mem_enum_iff_getElem?
-
-@[deprecated snd_lt_of_mem_zipIdx (since := "2025-01-21")]
-theorem fst_lt_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.1 < length l := by
-  simpa using fst_lt_add_of_mem_enumFrom h
-
-@[deprecated fst_mem_of_mem_zipIdx (since := "2025-01-21")]
-theorem snd_mem_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) : x.2 ∈ l :=
-  snd_mem_of_mem_enumFrom h
-
-@[deprecated fst_eq_of_mem_zipIdx (since := "2025-01-21")]
-theorem snd_eq_of_mem_enum {x : Nat × α} {l : List α} (h : x ∈ enum l) :
-    x.2 = l[x.1]'(fst_lt_of_mem_enum h) :=
-  snd_eq_of_mem_enumFrom h
-
-@[deprecated mem_zipIdx (since := "2025-01-21")]
-theorem mem_enum {x : α} {i : Nat} {xs : List α} (h : (i, x) ∈ xs.enum) :
-    i < xs.length ∧ x = xs[i]'(fst_lt_of_mem_enum h) :=
-  by simpa using mem_enumFrom h
-
-@[deprecated map_zipIdx (since := "2025-01-21")]
-theorem map_enum (f : α → β) (l : List α) : map (Prod.map id f) (enum l) = enum (map f l) :=
-  map_enumFrom f 0 l
-
-@[deprecated zipIdx_map_snd (since := "2025-01-21"), simp]
-theorem enum_map_fst (l : List α) : map Prod.fst (enum l) = range l.length := by
-  simp only [enum, enumFrom_map_fst, range_eq_range']
-
-@[deprecated zipIdx_map_fst (since := "2025-01-21"), simp]
-theorem enum_map_snd (l : List α) : map Prod.snd (enum l) = l :=
-  enumFrom_map_snd _ _
-
-@[deprecated zipIdx_map (since := "2025-01-21")]
-theorem enum_map (l : List α) (f : α → β) : (l.map f).enum = l.enum.map (Prod.map id f) :=
-  enumFrom_map _ _ _
-
-@[deprecated zipIdx_append (since := "2025-01-21")]
-theorem enum_append (xs ys : List α) : enum (xs ++ ys) = enum xs ++ enumFrom xs.length ys := by
-  simp [enum, enumFrom_append]
-
-@[deprecated zipIdx_eq_zip_range' (since := "2025-01-21")]
-theorem enum_eq_zip_range (l : List α) : l.enum = (range l.length).zip l :=
-  zip_of_prod (enum_map_fst _) (enum_map_snd _)
-
-@[deprecated unzip_zipIdx_eq_prod (since := "2025-01-21"), simp]
-theorem unzip_enum_eq_prod (l : List α) : l.enum.unzip = (range l.length, l) := by
-  simp only [enum_eq_zip_range, unzip_zip, length_range]
-
-@[deprecated zipIdx_eq_cons_iff (since := "2025-01-21")]
-theorem enum_eq_cons_iff {l : List α} :
-    l.enum = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (0, a) ∧ l' = enumFrom 1 as := by
-  rw [enum, enumFrom_eq_cons_iff]
-
-@[deprecated zipIdx_eq_append_iff (since := "2025-01-21")]
-theorem enum_eq_append_iff {l : List α} :
-    l.enum = l₁ ++ l₂ ↔
-      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enum ∧ l₂ = l₂'.enumFrom l₁'.length := by
-  simp [enum, enumFrom_eq_append_iff]
-
-end
-
 end List
diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean
index 9b30b3b568..e345d32ffb 100644
--- a/src/Init/Data/List/Range.lean
+++ b/src/Init/Data/List/Range.lean
@@ -39,13 +39,9 @@ theorem range'_succ {s n step} : range' s (n + 1) step = s :: range' (s + step)
 @[simp] theorem range'_eq_nil_iff : range' s n step = [] ↔ n = 0 := by
   rw [← length_eq_zero_iff, length_range']
 
-@[deprecated range'_eq_nil_iff (since := "2025-01-29")] abbrev range'_eq_nil := @range'_eq_nil_iff
-
 theorem range'_ne_nil_iff (s : Nat) {n step : Nat} : range' s n step ≠ [] ↔ n ≠ 0 := by
   cases n <;> simp
 
-@[deprecated range'_ne_nil_iff (since := "2025-01-29")] abbrev range'_ne_nil := @range'_ne_nil_iff
-
 @[simp] theorem range'_zero : range' s 0 step = [] := by
   simp
 
@@ -295,107 +291,4 @@ theorem zipIdx_eq_map_add {l : List α} {i : Nat} :
   | nil => rfl
   | cons _ _ ih => simp [ih (i := i + 1), zipIdx_succ, Nat.add_assoc, Nat.add_comm 1]
 
-/-! ### enumFrom -/
-
-section
-set_option linter.deprecated false
-
-@[deprecated zipIdx_eq_nil_iff (since := "2025-01-21"), simp]
-theorem enumFrom_eq_nil {n : Nat} {l : List α} : List.enumFrom n l = [] ↔ l = [] := by
-  cases l <;> simp
-
-@[deprecated length_zipIdx (since := "2025-01-21"), simp]
-theorem enumFrom_length : ∀ {n} {l : List α}, (enumFrom n l).length = l.length
-  | _, [] => rfl
-  | _, _ :: _ => congrArg Nat.succ enumFrom_length
-
-@[deprecated getElem?_zipIdx (since := "2025-01-21"), simp]
-theorem getElem?_enumFrom :
-    ∀ i (l : List α) j, (enumFrom i l)[j]? = l[j]?.map fun a => (i + j, a)
-  | _, [], _ => rfl
-  | _, _ :: _, 0 => by simp
-  | n, _ :: l, m + 1 => by
-    simp only [enumFrom_cons, getElem?_cons_succ]
-    exact (getElem?_enumFrom (n + 1) l m).trans <| by rw [Nat.add_right_comm]; rfl
-
-@[deprecated getElem_zipIdx (since := "2025-01-21"), simp]
-theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).length) :
-    (l.enumFrom n)[i] = (n + i, l[i]'(by simpa [enumFrom_length] using h)) := by
-  simp only [enumFrom_length] at h
-  rw [getElem_eq_getElem?_get]
-  simp only [getElem?_enumFrom, getElem?_eq_getElem h]
-  simp
-
-@[deprecated tail_zipIdx (since := "2025-01-21"), simp]
-theorem tail_enumFrom (l : List α) (n : Nat) : (enumFrom n l).tail = enumFrom (n + 1) l.tail := by
-  induction l generalizing n with
-  | nil => simp
-  | cons _ l ih => simp [enumFrom_cons]
-
-@[deprecated map_snd_add_zipIdx_eq_zipIdx (since := "2025-01-21"), simp]
-theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
-    map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
-  ext_getElem? fun i ↦ by simp [Nat.add_comm, Nat.add_left_comm]; rfl
-
-@[deprecated map_snd_add_zipIdx_eq_zipIdx (since := "2025-01-21"), simp]
-theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) :
-    map (Prod.map (· + n) id) (enum l) = enumFrom n l :=
-  map_fst_add_enumFrom_eq_enumFrom l _ _
-
-@[deprecated zipIdx_cons' (since := "2025-01-21"), simp]
-theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
-    enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
-  rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]
-
-@[deprecated zipIdx_map_snd (since := "2025-01-21"), simp]
-theorem enumFrom_map_fst (n) :
-    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
-  | [] => rfl
-  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
-
-@[deprecated zipIdx_map_fst (since := "2025-01-21"), simp]
-theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
-  | _, [] => rfl
-  | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
-
-@[deprecated zipIdx_eq_zip_range' (since := "2025-01-21")]
-theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
-  zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
-
-@[deprecated unzip_zipIdx_eq_prod (since := "2025-01-21"), simp]
-theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
-    (l.enumFrom n).unzip = (range' n l.length, l) := by
-  simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
-
-end
-
-/-! ### enum -/
-
-section
-set_option linter.deprecated false
-
-@[deprecated zipIdx_cons (since := "2025-01-21")]
-theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
-
-@[deprecated zipIdx_cons (since := "2025-01-21")]
-theorem enum_cons' (x : α) (xs : List α) :
-    enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
-  enumFrom_cons' _ _ _
-
-@[deprecated "These are now both `l.zipIdx 0`" (since := "2025-01-21")]
-theorem enum_eq_enumFrom {l : List α} : l.enum = l.enumFrom 0 := rfl
-
-@[deprecated "Use the reverse direction of `map_snd_add_zipIdx_eq_zipIdx` instead" (since := "2025-01-21")]
-theorem enumFrom_eq_map_enum (l : List α) (n : Nat) :
-    enumFrom n l = (enum l).map (Prod.map (· + n) id) := by
-  induction l generalizing n with
-  | nil => simp
-  | cons x xs ih =>
-    simp only [enumFrom_cons, ih, enum_cons, map_cons, Prod.map_apply, Nat.zero_add, id_eq, map_map,
-      cons.injEq, map_inj_left, Function.comp_apply, Prod.forall, Prod.mk.injEq, and_true, true_and]
-    intro a b _
-    exact (succ_add a n).symm
-
-end
-
 end List
diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean
index c6fc85a9ec..9e3e5f5d95 100644
--- a/src/Init/Data/List/Sort/Lemmas.lean
+++ b/src/Init/Data/List/Sort/Lemmas.lean
@@ -359,7 +359,7 @@ where go : ∀ (i : Nat) (l : List α),
       omega
 termination_by _ l => l.length
 
-@[deprecated mergeSort_zipIdx (since := "2025-01-21")] abbrev mergeSort_enum := @mergeSort_zipIdx
+
 
 theorem mergeSort_cons {le : α → α → Bool}
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean
index 8c436b53cd..5eb080d2b2 100644
--- a/src/Init/Data/List/Zip.lean
+++ b/src/Init/Data/List/Zip.lean
@@ -42,7 +42,7 @@ theorem zipWith_self {f : α → α → δ} : ∀ {l : List α}, zipWith f l l =
   | [] => rfl
   | _ :: _ => congrArg _ zipWith_self
 
-@[deprecated zipWith_self (since := "2025-01-29")] abbrev zipWith_same := @zipWith_self
+
 
 /--
 See also `getElem?_zipWith'` for a variant
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 519f75d500..548e8be953 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -36,7 +36,7 @@ instance : LT String :=
 instance decidableLT (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
   List.decidableLT s₁.data s₂.data
 
-@[deprecated decidableLT (since := "2024-12-13")] abbrev decLt := @decidableLT
+
 
 /--
 Non-strict inequality on strings, typically used via the `≤` operator.
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 3e04bc66e3..f7e90ba3c8 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -310,8 +310,7 @@ def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : N
 @[inline, expose] def zipIdx (xs : Vector α n) (k : Nat := 0) : Vector (α × Nat) n :=
   ⟨xs.toArray.zipIdx k, by simp⟩
 
-@[deprecated zipIdx (since := "2025-01-21")]
-abbrev zipWithIndex := @zipIdx
+
 
 @[inline, expose] def zip (as : Vector α n) (bs : Vector β n) : Vector (α × β) n :=
   ⟨as.toArray.zip bs.toArray, by simp⟩
@@ -433,8 +432,7 @@ no element of the index matches the given value.
 @[inline, expose] def finIdxOf? [BEq α] (xs : Vector α n) (x : α) : Option (Fin n) :=
   (xs.toArray.finIdxOf? x).map (Fin.cast xs.size_toArray)
 
-@[deprecated finIdxOf? (since := "2025-01-29")]
-abbrev indexOf? := @finIdxOf?
+
 
 /-- Finds the first index of a given value in a vector using a predicate. Returns `none` if the
 no element of the index matches the given value. -/
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index deb7898913..458cee79ad 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -120,8 +120,7 @@ theorem toArray_mk {xs : Array α} (h : xs.size = n) : (Vector.mk xs h).toArray
 @[simp] theorem findFinIdx?_mk {xs : Array α} (h : xs.size = n) (f : α → Bool) :
     (Vector.mk xs h).findFinIdx? f = (xs.findFinIdx? f).map (Fin.cast h) := rfl
 
-@[deprecated finIdxOf?_mk (since := "2025-01-29")]
-abbrev indexOf?_mk := @finIdxOf?_mk
+
 
 @[simp] theorem findM?_mk [Monad m] {xs : Array α} (h : xs.size = n) (f : α → m Bool) :
     (Vector.mk xs h).findM? f = xs.findM? f := rfl
@@ -217,8 +216,7 @@ abbrev indexOf?_mk := @finIdxOf?_mk
 @[simp] theorem zipIdx_mk {xs : Array α} (h : xs.size = n) (k : Nat := 0) :
     (Vector.mk xs h).zipIdx k = Vector.mk (xs.zipIdx k) (by simp [h]) := rfl
 
-@[deprecated zipIdx_mk (since := "2025-01-21")]
-abbrev zipWithIndex_mk := @zipIdx_mk
+
 
 @[simp] theorem mk_zipWith_mk {f : α → β → γ} {as : Array α} {bs : Array β}
     (h : as.size = n) (h' : bs.size = n) :
@@ -1244,8 +1242,7 @@ instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈
 @[simp] theorem getElem_set_self {xs : Vector α n} {i : Nat} {x : α} (hi : i < n) :
     (xs.set i x hi)[i] = x := by simp [getElem_set]
 
-@[deprecated getElem_set_self (since := "2024-12-12")]
-abbrev getElem_set_eq := @getElem_set_self
+
 
 @[simp] theorem getElem_set_ne {xs : Vector α n} {x : α} (hi : i < n) (hj : j < n) (h : i ≠ j) :
     (xs.set i x hi)[j] = xs[j] := by simp [getElem_set, h]
@@ -1306,8 +1303,7 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
 @[simp] theorem getElem_setIfInBounds_self {xs : Vector α n} {x : α} (hi : i < n) :
     (xs.setIfInBounds i x)[i] = x := by simp [getElem_setIfInBounds]
 
-@[deprecated getElem_setIfInBounds_self (since := "2024-12-12")]
-abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
+
 
 @[simp] theorem getElem_setIfInBounds_ne {xs : Vector α n} {x : α} (hj : j < n) (h : i ≠ j) :
     (xs.setIfInBounds i x)[j] = xs[j] := by simp [getElem_setIfInBounds, h]
diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean
index 8e62dd6e59..8e355a687b 100644
--- a/src/Init/Data/Vector/MapIdx.lean
+++ b/src/Init/Data/Vector/MapIdx.lean
@@ -97,18 +97,7 @@ theorem mem_zipIdx_iff_getElem? {x : α × Nat} {xs : Vector α n} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.mem_zipIdx_iff_getElem?]
 
-@[deprecated toList_zipIdx (since := "2025-01-27")]
-abbrev toList_zipWithIndex := @toList_zipIdx
-@[deprecated getElem_zipIdx (since := "2025-01-27")]
-abbrev getElem_zipWithIndex := @getElem_zipIdx
-@[deprecated mk_mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-27")]
-abbrev mk_mem_zipWithIndex_iff_le_and_getElem?_sub := @mk_mem_zipIdx_iff_le_and_getElem?_sub
-@[deprecated mk_mem_zipIdx_iff_getElem? (since := "2025-01-27")]
-abbrev mk_mem_zipWithIndex_iff_getElem? := @mk_mem_zipIdx_iff_getElem?
-@[deprecated mem_zipIdx_iff_le_and_getElem?_sub (since := "2025-01-27")]
-abbrev mem_zipWithIndex_iff_le_and_getElem?_sub := @mem_zipIdx_iff_le_and_getElem?_sub
-@[deprecated mem_zipIdx_iff_getElem? (since := "2025-01-27")]
-abbrev mem_zipWithIndex_iff_getElem? := @mem_zipIdx_iff_getElem?
+
 
 /-! ### mapFinIdx -/
 
@@ -256,8 +245,7 @@ theorem mapIdx_eq_zipIdx_map {xs : Vector α n} {f : Nat → α → β} :
     xs.mapIdx f = xs.zipIdx.map fun ⟨a, i⟩ => f i a := by
   ext <;> simp
 
-@[deprecated mapIdx_eq_zipIdx_map (since := "2025-01-27")]
-abbrev mapIdx_eq_zipWithIndex_map := @mapIdx_eq_zipIdx_map
+
 
 @[grind =]
 theorem mapIdx_append {xs : Vector α n} {ys : Vector α m} :
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 8efcba8294..0b3b990388 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -253,8 +253,7 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
 @[deprecated getElem?_eq_none_iff (since := "2025-02-17")]
 abbrev getElem?_eq_none := @getElem?_eq_none_iff
 
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
-abbrev isNone_getElem? := @getElem?_eq_none_iff
+
 
 @[simp, grind =] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
     (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by
diff --git a/src/Init/System.lean b/src/Init/System.lean
index 923e3b2bd1..2306a4c740 100644
--- a/src/Init/System.lean
+++ b/src/Init/System.lean
@@ -9,7 +9,6 @@ prelude
 public import Init.System.IO
 public import Init.System.Platform
 public import Init.System.Uri
-public import Init.System.Mutex
 public import Init.System.Promise
 
 public section
diff --git a/src/Init/System/Mutex.lean b/src/Init/System/Mutex.lean
deleted file mode 100644
index 0e0b1a1e4f..0000000000
--- a/src/Init/System/Mutex.lean
+++ /dev/null
@@ -1,134 +0,0 @@
-/-
-Copyright (c) 2022 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
--/
-module
-
-prelude
-public import Init.System.IO
-public import Init.Control.StateRef
-
-public section
-
-
-set_option linter.deprecated false
-
-namespace IO
-
-private opaque BaseMutexImpl : NonemptyType.{0}
-
-/--
-Mutual exclusion primitive (a lock).
-
-If you want to guard shared state, use `Mutex α` instead.
--/
-@[deprecated "Use Std.BaseMutex from Std.Sync.Mutex instead" (since := "2024-12-02")]
-def BaseMutex : Type := BaseMutexImpl.type
-
-instance : Nonempty BaseMutex := by exact BaseMutexImpl.property
-
-/-- Creates a new `BaseMutex`. -/
-@[extern "lean_io_basemutex_new", deprecated "Use Std.BaseMutex.new from Std.Sync.Mutex instead" (since := "2024-12-02")]
-opaque BaseMutex.new : BaseIO BaseMutex
-
-/--
-Locks a `BaseMutex`.  Waits until no other thread has locked the mutex.
-
-The current thread must not have already locked the mutex.
-Reentrant locking is undefined behavior (inherited from the C++ implementation).
--/
-@[extern "lean_io_basemutex_lock", deprecated "Use Std.BaseMutex.lock from Std.Sync.Mutex instead" (since := "2024-12-02")]
-opaque BaseMutex.lock (mutex : @& BaseMutex) : BaseIO Unit
-
-/--
-Unlocks a `BaseMutex`.
-
-The current thread must have already locked the mutex.
-Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).
--/
-@[extern "lean_io_basemutex_unlock", deprecated "Use Std.BaseMutex.unlock from Std.Sync.Mutex instead" (since := "2024-12-02")]
-opaque BaseMutex.unlock (mutex : @& BaseMutex) : BaseIO Unit
-
-private opaque CondvarImpl : NonemptyType.{0}
-
-/-- Condition variable. -/
-@[deprecated "Use Std.Condvar from Std.Sync.Mutex instead" (since := "2024-12-02")]
-def Condvar : Type := CondvarImpl.type
-
-instance : Nonempty Condvar := by exact CondvarImpl.property
-
-/-- Creates a new condition variable. -/
-@[extern "lean_io_condvar_new", deprecated "Use Std.Condvar.new from Std.Sync.Mutex instead" (since := "2024-12-02")]
-opaque Condvar.new : BaseIO Condvar
-
-/-- Waits until another thread calls `notifyOne` or `notifyAll`. -/
-@[extern "lean_io_condvar_wait", deprecated "Use Std.Condvar.wait from Std.Sync.Mutex instead" (since := "2024-12-02")]
-opaque Condvar.wait (condvar : @& Condvar) (mutex : @& BaseMutex) : BaseIO Unit
-
-/-- Wakes up a single other thread executing `wait`. -/
-@[extern "lean_io_condvar_notify_one", deprecated "Use Std.Condvar.notifyOne from Std.Sync.Mutex instead" (since := "2024-12-02")]
-opaque Condvar.notifyOne (condvar : @& Condvar) : BaseIO Unit
-
-/-- Wakes up all other threads executing `wait`. -/
-@[extern "lean_io_condvar_notify_all", deprecated "Use Std.Condvar.notifyAll from Std.Sync.Mutex instead" (since := "2024-12-02")]
-opaque Condvar.notifyAll (condvar : @& Condvar) : BaseIO Unit
-
-/-- Waits on the condition variable until the predicate is true. -/
-@[deprecated "Use Std.Condvar.waitUntil from Std.Sync.Mutex instead" (since := "2024-12-02")]
-def Condvar.waitUntil [Monad m] [MonadLift BaseIO m]
-    (condvar : Condvar) (mutex : BaseMutex) (pred : m Bool) : m Unit := do
-  while !(← pred) do
-    condvar.wait mutex
-
-/--
-Mutual exclusion primitive (lock) guarding shared state of type `α`.
-
-The type `Mutex α` is similar to `IO.Ref α`,
-except that concurrent accesses are guarded by a mutex
-instead of atomic pointer operations and busy-waiting.
--/
-@[deprecated "Use Std.Mutex from Std.Sync.Mutex instead" (since := "2024-12-02")]
-structure Mutex (α : Type) where private mk ::
-  private ref : IO.Ref α
-  mutex : BaseMutex
-  deriving Nonempty
-
-instance : CoeOut (Mutex α) BaseMutex where coe := Mutex.mutex
-
-/-- Creates a new mutex. -/
-@[deprecated "Use Std.Mutex.new from Std.Sync.Mutex instead" (since := "2024-12-02")]
-def Mutex.new (a : α) : BaseIO (Mutex α) :=
-  return { ref := ← mkRef a, mutex := ← BaseMutex.new }
-
-/--
-`AtomicT α m` is the monad that can be atomically executed inside a `Mutex α`,
-with outside monad `m`.
-The action has access to the state `α` of the mutex (via `get` and `set`).
--/
-@[deprecated "Use Std.AtomicT from Std.Sync.Mutex instead" (since := "2024-12-02")]
-abbrev AtomicT := StateRefT' IO.RealWorld
-
-/-- `mutex.atomically k` runs `k` with access to the mutex's state while locking the mutex. -/
-@[deprecated "Use Std.Mutex.atomically from Std.Sync.Mutex instead" (since := "2024-12-02")]
-def Mutex.atomically [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
-    (mutex : Mutex α) (k : AtomicT α m β) : m β := do
-  try
-    mutex.mutex.lock
-    k mutex.ref
-  finally
-    mutex.mutex.unlock
-
-/--
-`mutex.atomicallyOnce condvar pred k` runs `k`,
-waiting on `condvar` until `pred` returns true.
-Both `k` and `pred` have access to the mutex's state.
--/
-@[deprecated "Use Std.Mutex.atomicallyOnce from Std.Sync.Mutex instead" (since := "2024-12-02")]
-def Mutex.atomicallyOnce [Monad m] [MonadLiftT BaseIO m] [MonadFinally m]
-    (mutex : Mutex α) (condvar : Condvar)
-    (pred : AtomicT α m Bool) (k : AtomicT α m β) : m β :=
-  let _ : MonadLift BaseIO (AtomicT α m) := ⟨liftM⟩
-  mutex.atomically do
-    condvar.waitUntil mutex pred
-    k
diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index 8eb7a6b0b8..e0352eeccd 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -26,10 +26,7 @@ private def Environment.addDeclAux (env : Environment) (opts : Options) (decl :
     (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
   env.addDeclCore (Core.getMaxHeartbeats opts).toUSize decl cancelTk? (!debug.skipKernelTC.get opts)
 
-@[deprecated "use `Lean.addDecl` instead to ensure new namespaces are registered" (since := "2024-12-03")]
-def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration)
-    (cancelTk? : Option IO.CancelToken := none) : Except Kernel.Exception Environment :=
-  Environment.addDeclAux env opts decl cancelTk?
+
 
 private def isNamespaceName : Name → Bool
   | .str .anonymous _ => true
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 2ea7f5cdd6..221639fb8a 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -354,8 +354,7 @@ def setDiagnostics (env : Environment) (diag : Diagnostics) : Environment :=
 
 end Kernel.Environment
 
-@[deprecated Kernel.Exception (since := "2024-12-12")]
-abbrev KernelException := Kernel.Exception
+
 
 inductive ConstantKind where
   | defn | thm | «axiom» | «opaque» | quot | induct | ctor | recursor
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index ee72f4af83..0bdabafeb4 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -2596,17 +2596,6 @@ theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (
     (m.alter k f).getKey! k = if (f (m.get? k)).isSome then k else default := by
   simp only [getKey!_alter, beq_self_eq_true, reduceIte]
 
-@[deprecated getKey_eq (since := "2025-01-05")]
-theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
-    {h : k' ∈ m.alter k f} :
-    (m.alter k f).getKey k' h =
-      if heq : k == k' then
-        k
-      else
-        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
-        m.getKey k' h' :=
-  Raw₀.getKey_alter ⟨m.1, _⟩ m.2 h
-
 theorem getKey_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)}
     {h : k ∈ m.alter k f} : (m.alter k f).getKey k h = k := by
   simp
@@ -2945,17 +2934,6 @@ theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k →
     (m.modify k f).getKey! k = if k ∈ m then k else default :=
   Raw₀.getKey!_modify_self ⟨m.1, _⟩ m.2
 
-@[deprecated getKey_eq (since := "2025-01-05")]
-theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
-    {h : k' ∈ m.modify k f} :
-    (m.modify k f).getKey k' h =
-      if k == k' then
-        k
-      else
-        haveI h' : k' ∈ m := mem_modify.mp h
-        m.getKey k' h' :=
-  Raw₀.getKey_modify ⟨m.1, _⟩ m.2 h
-
 @[simp]
 theorem getKey_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
     {h : k ∈ m.modify k f} : (m.modify k f).getKey k h = k :=
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index a19f0cd23b..3ee0a5d48d 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -3101,18 +3101,6 @@ theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k →
   simp only [mem_iff_contains]
   simp_to_raw using Raw₀.getKey!_modify_self
 
-@[deprecated getKey_eq (since := "2025-01-05")]
-theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
-    (h : m.WF) : {hc : k' ∈ m.modify k f} →
-    (m.modify k f).getKey k' hc =
-      if k == k' then
-        k
-      else
-        haveI h' : k' ∈ m := mem_modify h |>.mp hc
-        m.getKey k' h' := by
-  simp only [mem_iff_contains]
-  simp_to_raw using Raw₀.getKey_modify
-
 @[simp]
 theorem getKey_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
     (h : m.WF) {hc : k ∈ m.modify k f} : (m.modify k f).getKey k hc = k := by
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index d9bf5047f4..fae78bc714 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -2377,17 +2377,6 @@ theorem getKey!_alter_self [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k :
     (t.alter k f).getKey! k = if (f (t.get? k)).isSome then k else default :=
   Impl.getKey!_alter_self t.wf
 
-@[deprecated getKey_eq (since := "2025-01-05")]
-theorem getKey_alter [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k k' : α}
-    {f : Option (β k) → Option (β k)} {hc : k' ∈ t.alter k f} :
-    (t.alter k f).getKey k' hc =
-      if heq : cmp k k' = .eq then
-        k
-      else
-        haveI h' : k' ∈ t := mem_alter_of_not_compare_eq heq |>.mp hc
-        t.getKey k' h' :=
-  Impl.getKey_alter t.wf
-
 @[simp]
 theorem getKey_alter_self [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α}
     {f : Option (β k) → Option (β k)} {hc : k ∈ t.alter k f} :
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 5295204e83..41fb38d5e1 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -2412,17 +2412,6 @@ theorem getKey!_alter_self [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h :
     (t.alter k f).getKey! k = if (f (t.get? k)).isSome then k else default :=
   Impl.getKey!_alter!_self h
 
-@[deprecated getKey_eq (since := "2025-01-05")]
-theorem getKey_alter [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k k' : α}
-    {f : Option (β k) → Option (β k)} {hc : k' ∈ t.alter k f} :
-    (t.alter k f).getKey k' hc =
-      if heq : cmp k k' = .eq then
-        k
-      else
-        haveI h' : k' ∈ t := mem_alter_of_not_compare_eq h heq |>.mp hc
-        t.getKey k' h' :=
-  Impl.getKey_alter! h
-
 @[simp]
 theorem getKey_alter_self [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k : α}
     {f : Option (β k) → Option (β k)} {hc : k ∈ t.alter k f} :
diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean
index 00c9d690d3..81d6be269a 100644
--- a/src/Std/Data/ExtDHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtDHashMap/Lemmas.lean
@@ -2286,17 +2286,6 @@ theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (
     (m.alter k f).getKey! k = if (f (m.get? k)).isSome then k else default :=
   m.inductionOn fun _ => DHashMap.getKey!_alter_self
 
-@[deprecated getKey_eq (since := "2025-01-05")]
-theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
-    {h : k' ∈ m.alter k f} :
-    (m.alter k f).getKey k' h =
-      if heq : k == k' then
-        k
-      else
-        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
-        m.getKey k' h' := by
-  split <;> simp_all
-
 @[simp]
 theorem getKey_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)}
     {h : k ∈ m.alter k f} : (m.alter k f).getKey k h = k :=
@@ -2624,17 +2613,6 @@ theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k →
     (m.modify k f).getKey! k = if k ∈ m then k else default :=
   m.inductionOn fun _ => DHashMap.getKey!_modify_self
 
-@[deprecated getKey_eq (since := "2025-01-05")]
-theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
-    {h : k' ∈ m.modify k f} :
-    (m.modify k f).getKey k' h =
-      if k == k' then
-        k
-      else
-        haveI h' : k' ∈ m := mem_modify.mp h
-        m.getKey k' h' := by
-  split <;> simp_all
-
 @[simp]
 theorem getKey_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k}
     {h : k ∈ m.modify k f} : (m.modify k f).getKey k h = k :=
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index f7e0313f38..1846b2fb5f 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -337,7 +337,7 @@ theorem BitVec.ult_max' (a : BitVec w) : (BitVec.ult a (-1#w)) = (!(a == -1#w))
   rw [lt_ult, ← BitVec.neg_one_eq_allOnes] at this
   by_cases (a.ult (-1#w)) <;> simp_all
 
-attribute [bv_normalize] BitVec.replicate_zero_eq
+attribute [bv_normalize] BitVec.replicate_zero
 attribute [bv_normalize] BitVec.add_eq_xor
 attribute [bv_normalize] BitVec.mul_eq_and
 
diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 850cc98e5f..f03546762b 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -358,13 +358,7 @@ def buildFileUnlessUpToDate'
     clearFileHash file
   setTrace (← fetchFileTrace file text)
 
-@[deprecated buildFileUnlessUpToDate' (since := "2024-12-06")]
-abbrev buildFileUnlessUpToDate
-  (file : FilePath) (depTrace : BuildTrace) (build : JobM PUnit) (text := false)
-: JobM BuildTrace := do
-  setTrace depTrace
-  buildFileUnlessUpToDate' file build text
-  getTrace
+
 
 /--
 Copies `file` to the Lake cache with the file extension `ext`, and
@@ -542,30 +536,6 @@ If `text := true`, `file` is handled as a text file rather than a binary file.
     addTrace (← extraDepTrace)
     buildArtifactUnlessUpToDate file (build depInfo) text
 
-/--
-Build `file` using `build` after `deps` have built if any of their traces change.
-
-If `text := true`, `file` is handled as a text file rather than a binary file.
--/
-@[inline, deprecated buildFileAfterDep (since := "2024-12-06")]
-abbrev buildFileAfterDepList
-  (file : FilePath) (deps : List (Job α)) (build : List α → JobM PUnit)
-  (extraDepTrace : JobM _ := pure BuildTrace.nil) (text := false)
-: SpawnM (Job FilePath) := do
-  buildFileAfterDep file (.collectList deps) build extraDepTrace text
-
-/--
-Build `file` using `build` after `deps` have built if any of their traces change.
-
-If `text := true`, `file` is handled as a text file rather than a binary file.
--/
-@[inline, deprecated buildFileAfterDep (since := "2024-12-06")]
-def buildFileAfterDepArray
-  (file : FilePath) (deps : Array (Job α)) (build : Array α → JobM PUnit)
-  (extraDepTrace : JobM _ := pure BuildTrace.nil) (text := false)
-: SpawnM (Job FilePath) := do
-  buildFileAfterDep file (.collectArray deps) build extraDepTrace text
-
 /-! ## Common Builds -/
 
 /--
diff --git a/src/lake/Lake/Build/Job/Monad.lean b/src/lake/Lake/Build/Job/Monad.lean
index 2bf3c31755..52992578cf 100644
--- a/src/lake/Lake/Build/Job/Monad.lean
+++ b/src/lake/Lake/Build/Job/Monad.lean
@@ -168,11 +168,7 @@ protected def mapM
       withLoggedIO (f a) fetch pkg? stack store ctx {s with trace}
     | .error n s => return .error n s
 
-@[deprecated Job.mapM (since := "2024-12-06")]
-protected abbrev bindSync
-  [OptDataKind β] (self : Job α) (f : α → JobM β)
-  (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) := self.mapM f prio sync
+
 
 /--
 Apply `f` asynchronously to the job's output
@@ -195,11 +191,7 @@ def bindM
       | .error e sa => return Task.pure (.error e sa)
     | .error e sa => return Task.pure (.error e sa)
 
-@[deprecated bindM (since := "2024-12-06")]
-protected abbrev bindAsync
-  [OptDataKind β] (self : Job α) (f : α → SpawnM (Job β))
-  (prio := Task.Priority.default) (sync := false)
-: SpawnM (Job β) := self.bindM (fun a => f a) prio sync
+
 
 /--
 `a.zipWith f b` produces a new job `c` that applies `f` to the
@@ -253,98 +245,3 @@ def collectArray (jobs : Array (Job α)) (traceCaption := "<collection>") : Job
   jobs.foldl (zipWith Array.push) (traceRoot (Array.mkEmpty jobs.size) traceCaption)
 
 end Job
-
-/-! ## BuildJob (deprecated) -/
-
-/-- A Lake build job. -/
-abbrev BuildJob α := Job α
-
-namespace BuildJob
-
-@[inline, deprecated "Obsolete." (since := "2024-12-06")]
-def mk (job : Job (α × BuildTrace)) : BuildJob α :=
-  job.mapOk fun (a, trace) s => .ok a {s with trace}
-
-@[inline, deprecated "Obsolete." (since := "2024-12-06")]
-def ofJob (job : Job BuildTrace) : BuildJob Unit :=
-  job.mapOk fun trace s => .ok () {s with trace}
-
-abbrev toJob (self : BuildJob α) : Job α :=
-  self
-
-@[deprecated Job.nil (since := "2024-12-06")]
-abbrev nil : BuildJob Unit :=
-  Job.pure ()
-
-@[deprecated Job.map (since := "2024-12-06")]
-protected abbrev pure [OptDataKind α] (a : α) : BuildJob α :=
-  Job.pure a
-
-instance : Pure BuildJob := ⟨Job.pure⟩
-
-@[deprecated Job.map (since := "2024-12-06")]
-protected abbrev map [OptDataKind β] (f : α → β) (self : BuildJob α) : BuildJob β :=
-  self.toJob.map f
-
-instance : Functor BuildJob where
-  map := Job.map
-
-@[inline, deprecated "Removed without replacement." (since := "2024-12-06")]
-def mapWithTrace [OptDataKind β] (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β :=
-  self.toJob.mapOk fun a s =>
-    let (b, trace) := f a s.trace
-    .ok b {s with trace}
-
-@[inline, deprecated Job.mapM (since := "2024-12-06")]
-protected def bindSync
-  [OptDataKind β] (self : BuildJob α) (f : α → BuildTrace → JobM (β × BuildTrace))
-  (prio : Task.Priority := .default) (sync := false)
-: SpawnM (Job β) :=
-  self.toJob.mapM (prio := prio) (sync := sync) fun a => do
-    let (b, trace) ← f a (← getTrace)
-    setTrace trace
-    return b
-
-@[inline, deprecated Job.bindM (since := "2024-12-06")]
-protected def bindAsync
-  [OptDataKind β] (self : BuildJob α) (f : α → BuildTrace → SpawnM (Job β))
-  (prio : Task.Priority := .default) (sync := false)
- : SpawnM (Job β)  :=
-  self.toJob.bindM (prio := prio) (sync := sync) fun a => do
-    f a (← getTrace)
-
-@[deprecated Job.wait? (since := "2024-12-06")]
-protected abbrev wait? (self : BuildJob α) : BaseIO (Option α) :=
-  self.toJob.wait?
-
-@[deprecated Job.add (since := "2024-12-06")]
-abbrev add (self : BuildJob α) (other : BuildJob β) : BuildJob α :=
-  self.toJob.add other.toJob
-
-@[deprecated Job.mix (since := "2024-12-06")]
-abbrev mix (self : BuildJob α) (other : BuildJob β) : BuildJob Unit :=
-  self.toJob.mix other.toJob
-
-@[deprecated Job.mixList (since := "2024-12-06")]
-abbrev mixList (jobs : List (BuildJob α)) : Id (BuildJob Unit) :=
-  return Job.mixList jobs
-
-@[deprecated Job.mixArray (since := "2024-12-06")]
-abbrev mixArray (jobs : Array (BuildJob α)) : Id (BuildJob Unit) :=
-  return Job.mixArray jobs
-
-@[deprecated Job.zipWith (since := "2024-12-06")]
-abbrev zipWith
-  [OptDataKind γ] (f : α → β → γ) (self : BuildJob α) (other : BuildJob β)
-: BuildJob γ :=
-  self.toJob.zipWith f other.toJob
-
-@[deprecated Job.collectList (since := "2024-12-06")]
-abbrev collectList (jobs : List (BuildJob α)) : Id (BuildJob (List α)) :=
-  return Job.collectList jobs
-
-@[deprecated Job.collectArray (since := "2024-12-06")]
-abbrev collectArray (jobs : Array (BuildJob α)) : Id (BuildJob (Array α)) :=
-  return Job.collectArray jobs
-
-attribute [deprecated Job (since := "2024-12-06")] BuildJob
diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean
index 82f687d18d..ab7b83c705 100644
--- a/src/lake/Lake/Load/Manifest.lean
+++ b/src/lake/Lake/Load/Manifest.lean
@@ -251,7 +251,7 @@ def save (self : Manifest) (manifestFile : FilePath) : IO PUnit := do
   let contents := Json.pretty self.toJson
   IO.FS.writeFile manifestFile <| contents.push '\n'
 
-@[deprecated save (since := "2024-12-17")] abbrev saveToFile := @save
+
 
 /-- Deserialize package entries from a (partial) JSON manifest. -/
 def decodeEntries (data : Json)  : Except String (Array PackageEntry) := do
diff --git a/tests/compiler/phashmap2.lean b/tests/compiler/phashmap2.lean
index b412509a1c..0cba2cf1e2 100644
--- a/tests/compiler/phashmap2.lean
+++ b/tests/compiler/phashmap2.lean
@@ -9,7 +9,7 @@ partial def formatMap : Node Nat Nat → Format
   keys.size.fold
     (fun i _ fmt =>
       let k := keys[i];
-      let v := vals.get! i;
+      let v := vals[i]!;
       let p := if i > 0 then fmt ++ format "," ++ Format.line else fmt;
       p ++ "c@" ++ Format.paren (format k ++ " => " ++ format v))
     Format.nil
@@ -28,7 +28,7 @@ partial def formatMap : Node Nat Nat → Format
 def main : IO Unit :=
 do
 let a : Array Nat := [1, 2, 3].toArray;
-IO.println (a.indexOf? 2);
+IO.println (a.idxOf? 2);
 let m : Map := PersistentHashMap.empty;
 let m := m.insert 1 1;
 let m := m.insert 33 2;
diff --git a/tests/lean/grind/experiments/bitvec.lean b/tests/lean/grind/experiments/bitvec.lean
index dde6ba0cf1..ac2a1c491d 100644
--- a/tests/lean/grind/experiments/bitvec.lean
+++ b/tests/lean/grind/experiments/bitvec.lean
@@ -5485,13 +5485,8 @@ set_option linter.missingDocs false
 @[deprecated toFin_uShiftRight (since := "2025-02-18")]
 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 replicate_zero (since := "2025-01-08")]
-abbrev replicate_zero_eq := @replicate_zero
 
-@[deprecated replicate_succ (since := "2025-01-08")]
-abbrev replicate_succ_eq := @replicate_succ
+
 
 end BitVec'
diff --git a/tests/lean/repr.lean b/tests/lean/repr.lean
index bce39c0531..742ea29450 100644
--- a/tests/lean/repr.lean
+++ b/tests/lean/repr.lean
@@ -1,13 +1,15 @@
 --
 
+def iota (n : Nat) := List.range' 1 n |>.reverse
+
 #eval repr (1, 2, 3)
 #eval repr (some 1, some (some true))
-#eval List.iota 10 |>.map some |>.map some
-#eval List.iota 15 |>.map fun x => (x, some x)
+#eval iota 10 |>.map some |>.map some
+#eval iota 15 |>.map fun x => (x, some x)
 #eval repr ("hello", 1, true, false, 'a', "testing tuples", "another string", "another string", "testing bigger tuples that should not fit in a single line", 20)
-#eval List.iota 50 |>.toArray
-#eval List.iota 20 |>.map fun i => if i % 2 == 0 then Except.ok (some i) else Except.error "no even"
+#eval iota 50 |>.toArray
+#eval iota 20 |>.map fun i => if i % 2 == 0 then Except.ok (some i) else Except.error "no even"
 
 instance : ReprAtom (Except String (Option Nat)) := ⟨⟩
 
-#eval List.iota 20 |>.map fun i => if i % 2 == 0 then Except.ok (some i) else Except.error "no even"
+#eval iota 20 |>.map fun i => if i % 2 == 0 then Except.ok (some i) else Except.error "no even"
diff --git a/tests/lean/run/1020.lean b/tests/lean/run/1020.lean
index 6556d34b06..d664791843 100644
--- a/tests/lean/run/1020.lean
+++ b/tests/lean/run/1020.lean
@@ -21,5 +21,5 @@ def allPairsFixed (xs : List α) (ys : List β) : List (α × β) :=
 example : (allPairsFixed [1, 2, 3] ['a', 'b']) = [(1, 'b'), (1, 'a'), (2, 'b'), (2, 'a'), (3, 'b'), (3, 'a')] :=
   rfl
 
-example : (allPairsFixed (List.iota 3) (List.iota 4) |>.length) = 12 :=
+example : (allPairsFixed (List.range 3) (List.range 4) |>.length) = 12 :=
   rfl
diff --git a/tests/lean/run/2670.lean b/tests/lean/run/2670.lean
index d533c89bfc..de1757e5b3 100644
--- a/tests/lean/run/2670.lean
+++ b/tests/lean/run/2670.lean
@@ -10,6 +10,10 @@ def enumFromTR' (n : Nat) (l : List α) : List (Nat × α) :=
   let arr := l.toArray
   (arr.foldr (fun a (n, acc) => (n-1, (n-1, a) :: acc)) (n + arr.size, [])).2
 
+def enumFrom : Nat → List α → List (Nat × α)
+  | _, [] => []
+  | n, x :: xs   => (n, x) :: enumFrom (n + 1) xs
+
 open List in
 theorem enumFrom_eq_enumFromTR' : @enumFrom = @enumFromTR' := by
   funext α n l; simp only [enumFromTR']
diff --git a/tests/lean/run/945.lean b/tests/lean/run/945.lean
index 26f055711a..0acb3f5dac 100644
--- a/tests/lean/run/945.lean
+++ b/tests/lean/run/945.lean
@@ -1,5 +1,5 @@
-@[simp] def iota : Nat → List Nat
+@[simp] def range : Nat → List Nat
   | 0       => []
-  | m@(n+1) => m :: iota n
+  | m@(n+1) => m :: range n
 
-attribute [simp] List.iota
+attribute [simp] List.range
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index d9680cb70a..f4b964923f 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -342,7 +342,7 @@ set_option pp.analyze.trustSubtypeMk true in
 #testDelabN List.partition.loop
 #testDelabN StateT.modifyGet
 #testDelabN Nat.gcd_one_left
-#testDelabN List.hasDecidableLt
+#testDelabN List.decidableLT
 #testDelabN Lean.Xml.parse
 #testDelabN Add.noConfusionType
 #testDelabN List.filterMapM.loop
diff --git a/tests/lean/run/discrTreeKey.lean b/tests/lean/run/discrTreeKey.lean
index 9ba34beb95..749260f041 100644
--- a/tests/lean/run/discrTreeKey.lean
+++ b/tests/lean/run/discrTreeKey.lean
@@ -60,7 +60,7 @@ open Nat List
 #discr_tree_simp_key singleton_append
 
 #check append_nil
-#discr_tree_simp_key append_eq_nil
+#discr_tree_simp_key append_eq_nil_iff
 
 #check mapM_nil
 #discr_tree_simp_key mapM_nil