chore: remove >6 month old deprecations (#9640)

2025-08-05 12:29:15 +10:00 · 2025-08-05 12:29:15 +10:00 · 6e06978961
commit 6e06978961
parent 8edcfbe776
43 changed files with 66 additions and 1201 deletions
--- 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
--- 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
--- 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
--- 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 α} :
--- 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
--- 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 -/
--- 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
--- 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 : α} :
--- 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 -/

--- 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
--- 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)]
--- 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 : α} :
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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.
--- 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. -/
--- 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]
--- 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} :
--- 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
--- 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
--- a/src/Init/System/Mutex.lean
+++ b/src/Init/System/Mutex.lean
@ -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
--- 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
--- 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
--- 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 :=
--- 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
--- 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} :
--- 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} :
--- 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 :=
--- 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

--- 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 -/

 /--
--- 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
--- 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
--- 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;
--- 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'
--- 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"
--- 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
--- 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']
--- 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
--- 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
--- 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