diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index d7bb36d35e..02d33d5aa6 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -176,9 +176,6 @@ theorem attach_map_val (xs : Array α) (f : α → β) :
   cases xs
   simp
 
-@[deprecated attach_map_val (since := "2025-02-17")]
-abbrev attach_map_coe := @attach_map_val
-
 -- The argument `xs : Array α` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (xs : Array α) : xs.attach.map Subtype.val = xs := by
   cases xs; simp
@@ -187,9 +184,6 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {xs : Array α} (H
     ((xs.attachWith p H).map fun (i : { i // p i}) => f i) = xs.map f := by
   cases xs; simp
 
-@[deprecated attachWith_map_val (since := "2025-02-17")]
-abbrev attachWith_map_coe := @attachWith_map_val
-
 theorem attachWith_map_subtype_val {p : α → Prop} {xs : Array α} (H : ∀ a ∈ xs, p a) :
     (xs.attachWith p H).map Subtype.val = xs := by
   cases xs; simp
@@ -401,9 +395,6 @@ theorem map_attach_eq_pmap {xs : Array α} {f : { x // x ∈ xs } → β} :
   cases xs
   ext <;> simp
 
-@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
-abbrev map_attach := @map_attach_eq_pmap
-
 @[grind =]
 theorem attach_filterMap {xs : Array α} {f : α → Option β} :
     (xs.filterMap f).attach = xs.attach.filterMap
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 8a17862c47..ebf062adb9 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -129,20 +129,11 @@ end Array
 
 namespace List
 
-@[deprecated Array.toArray_toList (since := "2025-02-17")]
-abbrev toArray_toList := @Array.toArray_toList
-
 -- This does not need to be a simp lemma, as already after the `whnfR` the right hand side is `as`.
 theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl
 
-@[deprecated toList_toArray (since := "2025-02-17")]
-abbrev _root_.Array.toList_toArray := @List.toList_toArray
-
 @[simp, grind =] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
 
-@[deprecated size_toArray (since := "2025-02-17")]
-abbrev _root_.Array.size_toArray := @List.size_toArray
-
 @[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := rfl
 
@@ -412,10 +403,6 @@ that requires a proof the array is non-empty.
 def back? (xs : Array α) : Option α :=
   xs[xs.size - 1]?
 
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), expose]
-def get? (xs : Array α) (i : Nat) : Option α :=
-  if h : i < xs.size then some xs[i] else none
-
 /--
 Swaps a new element with the element at the given index.
 
diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index 23752e43e9..f9faeb3d95 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -24,29 +24,6 @@ set_option linter.indexVariables true -- Enforce naming conventions for index va
 
 namespace Array
 
-/--
-Use the indexing notation `a[i]` instead.
-
-Access an element from an array without needing a runtime bounds checks,
-using a `Nat` index and a proof that it is in bounds.
-
-This function does not use `get_elem_tactic` to automatically find the proof that
-the index is in bounds. This is because the tactic itself needs to look up values in
-arrays.
--/
-@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]
-def get {α : Type u} (xs : @& Array α) (i : @& Nat) (h : LT.lt i xs.size) : α :=
-  xs.toList.get ⟨i, h⟩
-
-/--
-Use the indexing notation `a[i]!` instead.
-
-Access an element from an array, or panic if the index is out of bounds.
--/
-@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17"), expose]
-def get! {α : Type u} [Inhabited α] (xs : @& Array α) (i : @& Nat) : α :=
-  Array.getD xs i default
-
 theorem foldlM_toList.aux [Monad m]
     {f : β → α → m β} {xs : Array α} {i j} (H : xs.size ≤ i + j) {b} :
     foldlM.loop f xs xs.size (Nat.le_refl _) i j b = (xs.toList.drop j).foldlM f b := by
@@ -108,9 +85,6 @@ abbrev push_toList := @toList_push
 
 @[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
 
-@[deprecated toList_pop (since := "2025-02-17")]
-abbrev pop_toList := @Array.toList_pop
-
 @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl
 
 @[simp, grind =] theorem toList_append {xs ys : Array α} :
diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean
index e80209813c..226b91bcc2 100644
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@@ -278,9 +278,6 @@ theorem find?_flatten_eq_none_iff {xss : Array (Array α)} {p : α → Bool} :
     xss.flatten.find? p = none ↔ ∀ ys ∈ xss, ∀ x ∈ ys, !p x := by
   simp
 
-@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
-
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some array in `xs` contains `a`, and no earlier element of that array satisfies `p`.
@@ -306,9 +303,6 @@ theorem find?_flatten_eq_some_iff {xss : Array (Array α)} {p : α → Bool} {a
       ⟨zs.toList, bs.toList.map Array.toList, by simpa using h⟩,
         by simpa using h₁, by simpa using h₂⟩
 
-@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
-
 @[simp, grind =] theorem find?_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
@@ -318,17 +312,11 @@ theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
-@[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
-abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
-
 @[grind =]
 theorem find?_replicate :
     find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
 
-@[deprecated find?_replicate (since := "2025-03-18")]
-abbrev find?_mkArray := @find?_replicate
-
 @[simp] theorem find?_replicate_of_size_pos (h : 0 < n) :
     find? p (replicate n a) = if p a then some a else none := by
   simp [find?_replicate, Nat.ne_of_gt h]
@@ -346,34 +334,19 @@ abbrev find?_mkArray_of_pos := @find?_replicate_of_pos
 @[simp] theorem find?_replicate_of_neg (h : ¬ p a) : find? p (replicate n a) = none := by
   simp [find?_replicate, h]
 
-@[deprecated find?_replicate_of_neg (since := "2025-03-18")]
-abbrev find?_mkArray_of_neg := @find?_replicate_of_neg
-
 -- This isn't a `@[simp]` lemma since there is already a lemma for `l.find? p = none` for any `l`.
 theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [← List.toArray_replicate, Classical.or_iff_not_imp_left]
 
-@[deprecated find?_replicate_eq_none_iff (since := "2025-03-18")]
-abbrev find?_mkArray_eq_none_iff := @find?_replicate_eq_none_iff
-
 @[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   simp [← List.toArray_replicate]
 
-@[deprecated find?_replicate_eq_some_iff (since := "2025-03-18")]
-abbrev find?_mkArray_eq_some_iff := @find?_replicate_eq_some_iff
-
-@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
-abbrev find?_mkArray_eq_some := @find?_replicate_eq_some_iff
-
 @[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α → Bool} (h) :
     ((replicate n a).find? p).get h = a := by
   simp [← List.toArray_replicate]
 
-@[deprecated get_find?_replicate (since := "2025-03-18")]
-abbrev get_find?_mkArray := @get_find?_replicate
-
 @[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 008adc76e8..c5ec6e3b13 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -80,9 +80,6 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
 @[simp] theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
   ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩
 
-@[deprecated size_eq_zero_iff (since := "2025-02-24")]
-abbrev size_eq_zero := @size_eq_zero_iff
-
 theorem eq_empty_iff_size_eq_zero : xs = #[] ↔ xs.size = 0 :=
   size_eq_zero_iff.symm
 
@@ -107,17 +104,10 @@ theorem exists_mem_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) : 
 theorem size_pos_iff {xs : Array α} : 0 < xs.size ↔ xs ≠ #[] :=
   Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero_iff)
 
-@[deprecated size_pos_iff (since := "2025-02-24")]
-abbrev size_pos := @size_pos_iff
-
 theorem size_eq_one_iff {xs : Array α} : xs.size = 1 ↔ ∃ a, xs = #[a] := by
   cases xs
   simpa using List.length_eq_one_iff
 
-@[deprecated size_eq_one_iff (since := "2025-02-24")]
-abbrev size_eq_one := @size_eq_one_iff
-
-
 /-! ## L[i] and L[i]? -/
 
 theorem getElem?_eq_none_iff {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i := by
@@ -543,18 +533,12 @@ theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
 @[simp] theorem isEmpty_iff {xs : Array α} : xs.isEmpty ↔ xs = #[] := by
   cases xs <;> simp
 
-@[deprecated isEmpty_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_true := @isEmpty_iff
-
 @[grind →]
 theorem empty_of_isEmpty {xs : Array α} (h : xs.isEmpty) : xs = #[] := Array.isEmpty_iff.mp h
 
 @[simp] theorem isEmpty_eq_false_iff {xs : Array α} : xs.isEmpty = false ↔ xs ≠ #[] := by
   cases xs <;> simp
 
-@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
-
 theorem isEmpty_iff_size_eq_zero {xs : Array α} : xs.isEmpty ↔ xs.size = 0 := by
   rw [isEmpty_iff, size_eq_zero_iff]
 
@@ -2997,11 +2981,6 @@ theorem _root_.List.toArray_drop {l : List α} {k : Nat} :
     (l.drop k).toArray = l.toArray.extract k := by
   rw [List.drop_eq_extract, List.extract_toArray, List.size_toArray]
 
-@[deprecated extract_size (since := "2025-02-27")]
-theorem take_size {xs : Array α} : xs.take xs.size = xs := by
-  cases xs
-  simp
-
 /-! ### shrink -/
 
 @[simp] private theorem size_shrink_loop {xs : Array α} {n : Nat} : (shrink.loop n xs).size = xs.size - n := by
@@ -3587,8 +3566,6 @@ theorem foldr_eq_foldl_reverse {xs : Array α} {f : α → β → β} {b} :
   subst w
   rw [foldr_eq_foldl_reverse, foldl_push_eq_append rfl, map_reverse]
 
-@[deprecated foldr_push_eq_append (since := "2025-02-09")] abbrev foldr_flip_push_eq_append := @foldr_push_eq_append
-
 theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {xs : Array α} {a₁ a₂} :
      xs.foldl op (op a₁ a₂) = op a₁ (xs.foldl op a₂) := by
   rcases xs with ⟨l⟩
@@ -4713,44 +4690,3 @@ namespace List
       simp_all
 
 end List
-
-/-! ### Deprecations -/
-namespace Array
-
-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 getD_eq_getD_getElem? (since := "2025-02-12")] abbrev getD_eq_get? := @getD_eq_getD_getElem?
-
-set_option linter.deprecated false in
-@[deprecated getElem!_eq_getD (since := "2025-02-12")]
-theorem get!_eq_getD [Inhabited α] (xs : Array α) : xs.get! n = xs.getD n default := rfl
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead of `a.get! i`." (since := "2025-02-12")]
-theorem get!_eq_getD_getElem? [Inhabited α] (xs : Array α) (i : Nat) :
-    xs.get! i = xs[i]?.getD default := by
-  by_cases p : i < xs.size <;>
-  simp [get!, getD_eq_getD_getElem?, p]
-
-set_option linter.deprecated false in
-@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_getElem? := @get!_eq_getD_getElem?
-
-set_option linter.deprecated false in
-@[deprecated "`Array.get?` is deprecated, use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_get?_toList (xs : Array α) (i : Nat) : xs.get? i = xs.toList.get? i := by
-  simp [← getElem?_toList]
-
-set_option linter.deprecated false in
-@[deprecated get!_eq_getD_getElem? (since := "2025-02-12")] abbrev get!_eq_get? := @get!_eq_getD_getElem?
-
-/-! ### set -/
-
-@[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
-@[deprecated get_set_ne (since := "2025-02-27")] abbrev get_set_ne := @getElem_set_ne
-
-end Array
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 0f5ecc441e..a330a2f7ce 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -29,10 +29,6 @@ set_option linter.missingDocs true
 
 namespace BitVec
 
-@[inline, deprecated BitVec.ofNatLT (since := "2025-02-13"), inherit_doc BitVec.ofNatLT]
-protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n :=
-  BitVec.ofNatLT i p
-
 section Nat
 
 /--
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index eaeecfa675..24c3d742f4 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -74,10 +74,6 @@ theorem some_eq_getElem?_iff {l : BitVec w} : some a = l[n]? ↔ ∃ h : n < w,
 theorem getElem_of_getElem? {l : BitVec w} : l[n]? = some a → ∃ h : n < w, l[n] = a :=
   getElem?_eq_some_iff.mp
 
-set_option linter.missingDocs false in
-@[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
-abbrev getElem?_eq_some := @getElem?_eq_some_iff
-
 theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by
   simp
 
@@ -350,25 +346,14 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 @[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
   cases b <;> cases b' <;> rfl
 
-@[deprecated toNat_ofNatLT (since := "2025-02-13")]
-theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
-
 @[simp, grind =] theorem getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
   getLsbD (x#'lt) i = x.testBit i := by
   simp [getLsbD, BitVec.ofNatLT]
 
-@[deprecated getLsbD_ofNatLT (since := "2025-02-13")]
-theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
-  getLsbD (x#'lt) i = x.testBit i := getLsbD_ofNatLT x lt i
-
 @[simp, grind =] theorem getMsbD_ofNatLT {n x i : Nat} (h : x < 2^n) :
     getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
   simp [getMsbD, getLsbD]
 
-@[deprecated getMsbD_ofNatLT (since := "2025-02-13")]
-theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
-    getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := getMsbD_ofNatLT h
-
 @[grind =]
 theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n :=
   eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn])
@@ -6361,15 +6346,4 @@ theorem two_pow_ctz_le_toNat_of_ne_zero {x : BitVec w} (hx : x ≠ 0#w) :
   have hclz := getLsbD_true_ctz_of_ne_zero (x := x) hx
   exact Nat.ge_two_pow_of_testBit hclz
 
-/-! ### Deprecations -/
-
-set_option linter.missingDocs false
-
-@[deprecated toFin_uShiftRight (since := "2025-02-18")]
-abbrev toFin_uShiftRight := @toFin_ushiftRight
-
-
-
-
-
 end BitVec
diff --git a/src/Init/Data/Int/DivMod/Bootstrap.lean b/src/Init/Data/Int/DivMod/Bootstrap.lean
index 987d10c511..c12b63fb7d 100644
--- a/src/Init/Data/Int/DivMod/Bootstrap.lean
+++ b/src/Init/Data/Int/DivMod/Bootstrap.lean
@@ -206,9 +206,6 @@ theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a
   | Int.ofNat (b+1), _ =>
     rcases a with ⟨a⟩ <;> simp [Int.ediv, -natCast_ediv]
 
-@[deprecated ediv_nonneg_iff_of_pos (since := "2025-02-28")]
-abbrev div_nonneg_iff_of_pos := @ediv_nonneg_iff_of_pos
-
 /-! ### emod -/
 
 theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b
diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean
index 22c38835f8..7207efc808 100644
--- a/src/Init/Data/Int/Order.lean
+++ b/src/Init/Data/Int/Order.lean
@@ -1347,8 +1347,6 @@ theorem neg_of_sign_eq_neg_one : ∀ {a : Int}, sign a = -1 → a < 0
   | 0 => Int.mul_zero _
   | -[_+1] => Int.mul_neg_one _
 
-@[deprecated mul_sign_self (since := "2025-02-24")] abbrev mul_sign := @mul_sign_self
-
 @[simp] theorem sign_mul_self (i : Int) : sign i * i = natAbs i := by
   rw [Int.mul_comm, mul_sign_self]
 
diff --git a/src/Init/Data/Int/Pow.lean b/src/Init/Data/Int/Pow.lean
index b54caecd8a..475cf0fec4 100644
--- a/src/Init/Data/Int/Pow.lean
+++ b/src/Init/Data/Int/Pow.lean
@@ -50,14 +50,9 @@ protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := b
 
 instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := ⟨Int.pow_ne_zero (NeZero.ne _)⟩
 
-@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
-abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
-
-@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
-abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
-
+-- This can't be removed until the next update-stage0
 @[deprecated Nat.pow_pos (since := "2025-02-17")]
-abbrev pos_pow_of_pos := @Nat.pow_pos
+abbrev _root_.Nat.pos_pow_of_pos := @Nat.pow_pos
 
 @[simp, norm_cast]
 protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 1b8d75e28d..39f3bb0e38 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -149,9 +149,6 @@ theorem attach_map_val {l : List α} {f : α → β} :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   rw [attach, attachWith, map_pmap]; exact pmap_eq_map _
 
-@[deprecated attach_map_val (since := "2025-02-17")]
-abbrev attach_map_coe := @attach_map_val
-
 -- The argument `l : List α` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (l : List α) : l.attach.map Subtype.val = l :=
   attach_map_val.trans (List.map_id _)
@@ -160,9 +157,6 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {l : List α} (H :
     ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f := by
   rw [attachWith, map_pmap]; exact pmap_eq_map _
 
-@[deprecated attachWith_map_val (since := "2025-02-17")]
-abbrev attachWith_map_coe := @attachWith_map_val
-
 theorem attachWith_map_subtype_val {p : α → Prop} {l : List α} (H : ∀ a ∈ l, p a) :
     (l.attachWith p H).map Subtype.val = l :=
   (attachWith_map_val _).trans (List.map_id _)
@@ -254,13 +248,6 @@ theorem getElem?_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} (h
     · simp
     · simp only [pmap, getElem?_cons_succ, hl]
 
-set_option linter.deprecated false in
-@[deprecated List.getElem?_pmap (since := "2025-02-12")]
-theorem get?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    get? (pmap f l h) n = Option.pmap f (get? l n) fun x H => h x (mem_of_get? H) := by
-  simp only [get?_eq_getElem?]
-  simp [getElem?_pmap]
-
 -- The argument `f` is explicit to allow rewriting from right to left.
 @[simp, grind =]
 theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {i : Nat}
@@ -277,15 +264,6 @@ theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h
     · simp
     · simp [hl]
 
-@[deprecated getElem_pmap (since := "2025-02-13")]
-theorem get_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) {n : Nat}
-    (hn : n < (pmap f l h).length) :
-    get (pmap f l h) ⟨n, hn⟩ =
-      f (get l ⟨n, @length_pmap _ _ p f l h ▸ hn⟩)
-        (h _ (getElem_mem (@length_pmap _ _ p f l h ▸ hn))) := by
-  simp only [get_eq_getElem]
-  simp [getElem_pmap]
-
 @[simp, grind =]
 theorem getElem?_attachWith {xs : List α} {i : Nat} {P : α → Prop} {H : ∀ a ∈ xs, P a} :
     (xs.attachWith P H)[i]? = xs[i]?.pmap Subtype.mk (fun _ a => H _ (mem_of_getElem? a)) :=
@@ -466,9 +444,6 @@ theorem map_attach_eq_pmap {l : List α} {f : { x // x ∈ l } → β} :
     apply pmap_congr_left
     simp
 
-@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
-abbrev map_attach := @map_attach_eq_pmap
-
 @[grind =]
 theorem attach_filterMap {l : List α} {f : α → Option β} :
     (l.filterMap f).attach = l.attach.filterMap
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index f26a258425..bca9d04a13 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -289,16 +289,6 @@ theorem cons_lex_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false :
 @[simp] theorem lex_nil [BEq α] {as : List α} : lex as [] lt = false := by
   cases as <;> simp [nil_lex_nil, cons_lex_nil]
 
-@[deprecated nil_lex_nil (since := "2025-02-10")]
-theorem lex_nil_nil [BEq α] : lex ([] : List α) [] lt = false := rfl
-@[deprecated nil_lex_cons (since := "2025-02-10")]
-theorem lex_nil_cons [BEq α] {b} {bs : List α} : lex [] (b :: bs) lt = true := rfl
-@[deprecated cons_lex_nil (since := "2025-02-10")]
-theorem lex_cons_nil [BEq α] {a} {as : List α} : lex (a :: as) [] lt = false := rfl
-@[deprecated cons_lex_cons (since := "2025-02-10")]
-theorem lex_cons_cons [BEq α] {a b} {as bs : List α} :
-    lex (a :: as) (b :: bs) lt = (lt a b || (a == b && lex as bs lt)) := rfl
-
 /-! ## Alternative getters -/
 
 /-! ### getLast -/
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index 6c90595e63..c072f97401 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -21,65 +21,6 @@ namespace List
 
 /-! ## Alternative getters -/
 
-/-! ### get? -/
-
-/--
-Returns the `i`-th element in the list (zero-based).
-
-If the index is out of bounds (`i ≥ as.length`), this function returns `none`.
-Also see `get`, `getD` and `get!`.
--/
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), expose]
-def get? : (as : List α) → (i : Nat) → Option α
-  | a::_,  0   => some a
-  | _::as, n+1 => get? as n
-  | _,     _   => none
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
-theorem get?_nil : @get? α [] n = none := rfl
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
-theorem get?_cons_zero : @get? α (a::l) 0 = some a := rfl
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
-theorem get?_cons_succ : @get? α (a::l) (n+1) = get? l n := rfl
-
-set_option linter.deprecated false in
-@[deprecated "Use `List.ext_getElem?`." (since := "2025-02-12")]
-theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
-  | [], [], _ => rfl
-  | _ :: _, [], h => nomatch h 0
-  | [], _ :: _, h => nomatch h 0
-  | a :: l₁, a' :: l₂, h => by
-    have h0 : some a = some a' := h 0
-    injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
-
-/-! ### get! -/
-
-/--
-Returns the `i`-th element in the list (zero-based).
-
-If the index is out of bounds (`i ≥ as.length`), this function panics when executed, and returns
-`default`. See `get?` and `getD` for safer alternatives.
--/
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12"), expose]
-def get! [Inhabited α] : (as : List α) → (i : Nat) → α
-  | a::_,  0   => a
-  | _::as, n+1 => get! as n
-  | _,     _   => panic! "invalid index"
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_nil [Inhabited α] (n : Nat) : [].get! n = (default : α) := rfl
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_cons_succ [Inhabited α] (l : List α) (a : α) (n : Nat) :
-    (a::l).get! (n+1) = get! l n := rfl
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_cons_zero [Inhabited α] (l : List α) (a : α) : (a::l).get! 0 = a := rfl
-
 /-! ### getD -/
 
 /--
@@ -281,17 +222,6 @@ theorem getElem_append_right {as bs : List α} {i : Nat} (h₁ : as.length ≤ i
     cases i with simp [Nat.succ_sub_succ] <;> simp at h₁
     | succ i => apply ih; simp [h₁]
 
-@[deprecated "Deprecated without replacement." (since := "2025-02-13")]
-theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.length) : (as ++ [a] : List _).get i = a := by
-  cases i; rename_i i h'
-  induction as generalizing i with
-  | nil => cases i with
-    | zero => simp [List.get]
-    | succ => simp +arith at h'
-  | cons a as ih =>
-    cases i with simp at h
-    | succ i => apply ih; simp [h]
-
 theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   induction h with
   | head => simp +arith
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 77c0fca08e..a94ac7be12 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -360,9 +360,6 @@ theorem find?_flatten_eq_none_iff {xs : List (List α)} {p : α → Bool} :
     xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
   simp
 
-@[deprecated find?_flatten_eq_none_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_none := @find?_flatten_eq_none_iff
-
 /--
 If `find? p` returns `some a` from `xs.flatten`, then `p a` holds, and
 some list in `xs` contains `a`, and no earlier element of that list satisfies `p`.
@@ -403,9 +400,6 @@ theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a : 
     · exact h₁ l ml a m
     · exact h₂ a m
 
-@[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
-abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
-
 @[simp, grind =] theorem find?_flatMap {xs : List α} {f : α → List β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   simp [flatMap_def, findSome?_map]; rfl
@@ -434,16 +428,10 @@ theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
     (replicate n a).find? p = none ↔ n = 0 ∨ !p a := by
   simp [Classical.or_iff_not_imp_left]
 
-@[deprecated find?_replicate_eq_none_iff (since := "2025-02-03")]
-abbrev find?_replicate_eq_none := @find?_replicate_eq_none_iff
-
 @[simp] theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
     (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
   cases n <;> simp
 
-@[deprecated find?_replicate_eq_some_iff (since := "2025-02-03")]
-abbrev find?_replicate_eq_some := @find?_replicate_eq_some_iff
-
 @[simp] theorem get_find?_replicate {n : Nat} {a : α} {p : α → Bool} (h) : ((replicate n a).find? p).get h = a := by
   cases n with
   | zero => simp at h
@@ -836,9 +824,6 @@ theorem of_findIdx?_eq_some {xs : List α} {p : α → Bool} (w : xs.findIdx? p
     simp_all only [findIdx?_cons]
     split at w <;> cases i <;> simp_all
 
-@[deprecated of_findIdx?_eq_some (since := "2025-02-02")]
-abbrev findIdx?_of_eq_some := @of_findIdx?_eq_some
-
 theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
     ∀ i : Nat, match xs[i]? with | some a => ¬ p a | none => true := by
   intro i
@@ -854,9 +839,6 @@ theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
       apply ih
       split at w <;> simp_all
 
-@[deprecated of_findIdx?_eq_none (since := "2025-02-02")]
-abbrev findIdx?_of_eq_none := @of_findIdx?_eq_none
-
 @[simp, grind _=_] theorem findIdx?_map {f : β → α} {l : List β} : findIdx? p (l.map f) = l.findIdx? (p ∘ f) := by
   induction l with
   | nil => simp
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 4dbba13f0f..1f8912b077 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -107,9 +107,6 @@ theorem ne_nil_of_length_pos (_ : 0 < length l) : l ≠ [] := fun _ => nomatch l
 @[simp] theorem length_eq_zero_iff : length l = 0 ↔ l = [] :=
   ⟨eq_nil_of_length_eq_zero, fun h => h ▸ rfl⟩
 
-@[deprecated length_eq_zero_iff (since := "2025-02-24")]
-abbrev length_eq_zero := @length_eq_zero_iff
-
 theorem eq_nil_iff_length_eq_zero : l = [] ↔ length l = 0 :=
   length_eq_zero_iff.symm
 
@@ -142,18 +139,12 @@ theorem exists_cons_of_length_eq_add_one :
 theorem length_pos_iff {l : List α} : 0 < length l ↔ l ≠ [] :=
   Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero_iff)
 
-@[deprecated length_pos_iff (since := "2025-02-24")]
-abbrev length_pos := @length_pos_iff
-
 theorem ne_nil_iff_length_pos {l : List α} : l ≠ [] ↔ 0 < length l :=
   length_pos_iff.symm
 
 theorem length_eq_one_iff {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
-@[deprecated length_eq_one_iff (since := "2025-02-24")]
-abbrev length_eq_one := @length_eq_one_iff
-
 /-! ### cons -/
 
 -- The arguments here are intentionally explicit.
@@ -198,38 +189,6 @@ We simplify `l.get i` to `l[i.1]'i.2` and `l.get? i` to `l[i]?`.
 @[simp, grind =]
 theorem get_eq_getElem {l : List α} {i : Fin l.length} : l.get i = l[i.1]'i.2 := rfl
 
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_none : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => get?_eq_none (l := l) <| Nat.le_of_succ_le_succ h
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_get : ∀ {l : List α} {n} (h : n < l.length), l.get? n = some (get l ⟨n, h⟩)
-  | _ :: _, 0, _ => rfl
-  | _ :: l, _+1, _ => get?_eq_get (l := l) _
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_some_iff : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a :=
-  ⟨fun e =>
-    have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_eq_none hn ▸ e
-    ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩,
-  fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get?_eq_none_iff : l.get? n = none ↔ length l ≤ n :=
-  ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some_iff.2 ⟨h', rfl⟩), get?_eq_none⟩
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12"), simp]
-theorem get?_eq_getElem? {l : List α} {i : Nat} : l.get? i = l[i]? := by
-  simp only [getElem?_def]; split
-  · exact (get?_eq_get ‹_›)
-  · exact (get?_eq_none_iff.2 <| Nat.not_lt.1 ‹_›)
-
 /-! ### getElem!
 
 We simplify `l[i]!` to `(l[i]?).getD default`.
@@ -373,23 +332,6 @@ theorem getD_eq_getElem?_getD {l : List α} {i : Nat} {a : α} : getD l i a = (l
 theorem getD_cons_zero : getD (x :: xs) 0 d = x := by simp
 theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := by simp
 
-/-! ### get!
-
-We simplify `l.get! i` to `l[i]!`.
--/
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) i, l.get! i = l.getD i default
-  | [], _      => rfl
-  | _a::_, 0   => by simp [get!]
-  | _a::l, n+1 => by simpa using get!_eq_getD l n
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12"), simp]
-theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]! := by
-  simp [get!_eq_getD]
-
 /-! ### mem -/
 
 @[simp, grind ←] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
@@ -581,15 +523,9 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
 @[grind →]
 theorem nil_of_isEmpty {l : List α} (h : l.isEmpty) : l = [] := List.isEmpty_iff.mp h
 
-@[deprecated isEmpty_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_true := @isEmpty_iff
-
 @[simp] theorem isEmpty_eq_false_iff {l : List α} : l.isEmpty = false ↔ l ≠ [] := by
   cases l <;> simp
 
-@[deprecated isEmpty_eq_false_iff (since := "2025-02-17")]
-abbrev isEmpty_eq_false := @isEmpty_eq_false_iff
-
 theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
     xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
   cases xs <;> simp
@@ -2881,9 +2817,6 @@ theorem getLast_eq_head_reverse {l : List α} (h : l ≠ []) :
     l.getLast h = l.reverse.head (by simp_all) := by
   rw [← head_reverse]
 
-@[deprecated getLast_eq_iff_getLast?_eq_some (since := "2025-02-17")]
-abbrev getLast_eq_iff_getLast_eq_some := @getLast_eq_iff_getLast?_eq_some
-
 @[simp] theorem getLast?_eq_none_iff {xs : List α} : xs.getLast? = none ↔ xs = [] := by
   rw [getLast?_eq_head?_reverse, head?_eq_none_iff, reverse_eq_nil_iff]
 
@@ -3687,10 +3620,6 @@ theorem get_cons_succ' {as : List α} {i : Fin as.length} :
 theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos_iff.mp h)
   | _::_, _ => rfl
 
-set_option linter.deprecated false in
-@[deprecated "Use `a[0]?` instead." (since := "2025-02-12")]
-theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl
-
 /--
 If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`,
 `rw [h]` will give a "motive is not type correct" error, as it cannot rewrite the
@@ -3700,18 +3629,6 @@ such a rewrite, with `rw [get_of_eq h]`.
 theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) :
     get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl
 
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]?` instead." (since := "2025-02-12")]
-theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a
-  | _a::_, 0, rfl => rfl
-  | _::l, _+1, e => get!_of_get? (l := l) e
-
-set_option linter.deprecated false in
-@[deprecated "Use `a[i]!` instead." (since := "2025-02-12")]
-theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α)
-  | [], _, _ => rfl
-  | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h
-
 theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl
 
 theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by
@@ -3737,30 +3654,11 @@ theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a := by
   obtain ⟨n, h, e⟩ := getElem_of_mem h
   exact ⟨⟨n, h⟩, e⟩
 
-set_option linter.deprecated false in
-@[deprecated getElem?_of_mem (since := "2025-02-12")]
-theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a :=
-  let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩
-
 theorem get_mem : ∀ (l : List α) n, get l n ∈ l
   | _ :: _, ⟨0, _⟩ => .head ..
   | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..)
 
-set_option linter.deprecated false in
-@[deprecated mem_of_getElem? (since := "2025-02-12")]
-theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l :=
-  let ⟨_, e⟩ := get?_eq_some_iff.1 e; e ▸ get_mem ..
-
 theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a :=
   ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩
 
-set_option linter.deprecated false in
-@[deprecated mem_iff_getElem? (since := "2025-02-12")]
-theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by
-  simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get]
-
-/-! ### Deprecations -/
-
-
-
 end List
diff --git a/src/Init/Data/List/Nat/Basic.lean b/src/Init/Data/List/Nat/Basic.lean
index 604f3a7297..2f8e5a4b84 100644
--- a/src/Init/Data/List/Nat/Basic.lean
+++ b/src/Init/Data/List/Nat/Basic.lean
@@ -105,9 +105,6 @@ theorem length_leftpad {n : Nat} {a : α} {l : List α} :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
 
-@[deprecated length_leftpad (since := "2025-02-24")]
-abbrev leftpad_length := @length_leftpad
-
 theorem length_rightpad {n : Nat} {a : α} {l : List α} :
     (rightpad n a l).length = max n l.length := by
   simp [rightpad]
diff --git a/src/Init/Data/List/Nat/InsertIdx.lean b/src/Init/Data/List/Nat/InsertIdx.lean
index 18b80e380c..505695bb12 100644
--- a/src/Init/Data/List/Nat/InsertIdx.lean
+++ b/src/Init/Data/List/Nat/InsertIdx.lean
@@ -196,9 +196,6 @@ theorem getElem_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (hn : i < j)
         | zero => omega
         | succ j => simp
 
-@[deprecated getElem_insertIdx_of_gt (since := "2025-02-04")]
-abbrev getElem_insertIdx_of_ge := @getElem_insertIdx_of_gt
-
 @[grind =]
 theorem getElem_insertIdx {l : List α} {x : α} {i j : Nat} (h : j < (l.insertIdx i x).length) :
     (l.insertIdx i x)[j] =
@@ -261,9 +258,6 @@ theorem getElem?_insertIdx_of_gt {l : List α} {x : α} {i j : Nat} (h : i < j)
     (l.insertIdx i x)[j]? = l[j - 1]? := by
   rw [getElem?_insertIdx, if_neg (by omega), if_neg (by omega)]
 
-@[deprecated getElem?_insertIdx_of_gt (since := "2025-02-04")]
-abbrev getElem?_insertIdx_of_ge := @getElem?_insertIdx_of_gt
-
 end InsertIdx
 
 end List
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 06e3c2b1ce..7ce1a73c69 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -117,9 +117,6 @@ theorem take_set_of_le {a : α} {i j : Nat} {l : List α} (h : j ≤ i) :
     next h' => rw [getElem?_set_ne (by omega)]
     · rfl
 
-@[deprecated take_set_of_le (since := "2025-02-04")]
-abbrev take_set_of_lt := @take_set_of_le
-
 @[simp, grind =] theorem take_replicate {a : α} : ∀ {i n : Nat}, take i (replicate n a) = replicate (min i n) a
   | n, 0 => by simp
   | 0, m => by simp
@@ -165,9 +162,6 @@ theorem take_eq_take_iff :
   | x :: xs, 0, j + 1 => by simp [succ_min_succ]
   | x :: xs, i + 1, j + 1 => by simp [succ_min_succ, take_eq_take_iff]
 
-@[deprecated take_eq_take_iff (since := "2025-02-16")]
-abbrev take_eq_take := @take_eq_take_iff
-
 @[grind =]
 theorem take_add {l : List α} {i j : Nat} : l.take (i + j) = l.take i ++ (l.drop i).take j := by
   suffices take (i + j) (take i l ++ drop i l) = take i l ++ take j (drop i l) by
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 6ad2dcbd63..7b1309c110 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -165,9 +165,6 @@ theorem take_set {l : List α} {i j : Nat} {a : α} :
     | nil => simp
     | cons hd tl => cases j <;> simp_all
 
-@[deprecated take_set (since := "2025-02-17")]
-abbrev set_take := @take_set
-
 theorem drop_set {l : List α} {i j : Nat} {a : α} :
     (l.set j a).drop i = if j < i then l.drop i else (l.drop i).set (j - i) a := by
   induction i generalizing l j with
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index e09cc2a91b..e87836061f 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -791,18 +791,6 @@ protected theorem pow_le_pow_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i
     | Or.inr h =>
       h.symm ▸ Nat.le_refl _
 
-set_option linter.missingDocs false in
-@[deprecated Nat.pow_le_pow_left (since := "2025-02-17")]
-abbrev pow_le_pow_of_le_left := @Nat.pow_le_pow_left
-
-set_option linter.missingDocs false in
-@[deprecated Nat.pow_le_pow_right (since := "2025-02-17")]
-abbrev pow_le_pow_of_le_right := @Nat.pow_le_pow_right
-
-set_option linter.missingDocs false in
-@[deprecated Nat.pow_pos (since := "2025-02-17")]
-abbrev pos_pow_of_pos := @Nat.pow_pos
-
 @[simp] theorem zero_pow_of_pos (n : Nat) (h : 0 < n) : 0 ^ n = 0 := by
   cases n with
   | zero => cases h
@@ -882,9 +870,6 @@ protected theorem ne_zero_of_lt (h : b < a) : a ≠ 0 := by
   exact absurd h (Nat.not_lt_zero _)
   apply Nat.noConfusion
 
-@[deprecated Nat.ne_zero_of_lt (since := "2025-02-06")]
-theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := Nat.ne_zero_of_lt h
-
 theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (Nat.ne_zero_of_lt h)
 
diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean
index 1aa6f49a8b..e7eb74f6d0 100644
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -75,9 +75,6 @@ theorem attach_map_val (o : Option α) (f : α → β) :
     (o.attach.map fun (i : {i // o = some i}) => f i) = o.map f := by
   cases o <;> simp
 
-@[deprecated attach_map_val (since := "2025-02-17")]
-abbrev attach_map_coe := @attach_map_val
-
 @[simp, grind =]theorem attach_map_subtype_val (o : Option α) :
     o.attach.map Subtype.val = o :=
   (attach_map_val _ _).trans (congrFun Option.map_id _)
@@ -86,9 +83,6 @@ theorem attachWith_map_val {p : α → Prop} (f : α → β) (o : Option α) (H
     ((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f := by
   cases o <;> simp
 
-@[deprecated attachWith_map_val (since := "2025-02-17")]
-abbrev attachWith_map_coe := @attachWith_map_val
-
 @[simp, grind =] theorem attachWith_map_subtype_val {p : α → Prop} (o : Option α) (H : ∀ a, o = some a → p a) :
     (o.attachWith p H).map Subtype.val = o :=
   (attachWith_map_val _ _ _).trans (congrFun Option.map_id _)
@@ -187,9 +181,6 @@ theorem toArray_attachWith {p : α → Prop} {o : Option α} {h} :
     o.attach.map f = o.pmap (fun a (h : o = some a) => f ⟨a, h⟩) (fun _ h => h) := by
   cases o <;> simp
 
-@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
-abbrev map_attach := @map_attach_eq_pmap
-
 @[simp, grind =] theorem map_attachWith {l : Option α} {P : α → Prop} {H : ∀ (a : α), l = some a → P a}
     (f : { x // P x } → β) :
     (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean
index 3662c93acb..ca6c092b89 100644
--- a/src/Init/Data/SInt/Basic.lean
+++ b/src/Init/Data/SInt/Basic.lean
@@ -96,8 +96,7 @@ theorem Int8.toBitVec.inj : {x y : Int8} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `Int8` that is 2's complement equivalent to the `UInt8`. -/
 @[inline] def UInt8.toInt8 (i : UInt8) : Int8 := Int8.ofUInt8 i
-@[inline, deprecated UInt8.toInt8 (since := "2025-02-13"), inherit_doc UInt8.toInt8]
-def Int8.mk (i : UInt8) : Int8 := UInt8.toInt8 i
+
 /--
 Converts an arbitrary-precision integer to an 8-bit integer, wrapping on overflow or underflow.
 
@@ -159,8 +158,7 @@ Converts an 8-bit signed integer to a natural number, mapping all negative numbe
 Use `Int8.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def Int8.toNatClampNeg (i : Int8) : Nat := i.toInt.toNat
-@[inline, deprecated Int8.toNatClampNeg (since := "2025-02-13"), inherit_doc Int8.toNatClampNeg]
-def Int8.toNat (i : Int8) : Nat := i.toInt.toNat
+
 /-- Obtains the `Int8` whose 2's complement representation is the given `BitVec 8`. -/
 @[inline] def Int8.ofBitVec (b : BitVec 8) : Int8 := ⟨⟨b⟩⟩
 /--
@@ -449,8 +447,7 @@ theorem Int16.toBitVec.inj : {x y : Int16} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `Int16` that is 2's complement equivalent to the `UInt16`. -/
 @[inline] def UInt16.toInt16 (i : UInt16) : Int16 := Int16.ofUInt16 i
-@[inline, deprecated UInt16.toInt16 (since := "2025-02-13"), inherit_doc UInt16.toInt16]
-def Int16.mk (i : UInt16) : Int16 := UInt16.toInt16 i
+
 /--
 Converts an arbitrary-precision integer to a 16-bit signed integer, wrapping on overflow or underflow.
 
@@ -514,8 +511,7 @@ Converts a 16-bit signed integer to a natural number, mapping all negative numbe
 Use `Int16.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def Int16.toNatClampNeg (i : Int16) : Nat := i.toInt.toNat
-@[inline, deprecated Int16.toNatClampNeg (since := "2025-02-13"), inherit_doc Int16.toNatClampNeg]
-def Int16.toNat (i : Int16) : Nat := i.toInt.toNat
+
 /-- Obtains the `Int16` whose 2's complement representation is the given `BitVec 16`. -/
 @[inline] def Int16.ofBitVec (b : BitVec 16) : Int16 := ⟨⟨b⟩⟩
 /--
@@ -820,8 +816,7 @@ theorem Int32.toBitVec.inj : {x y : Int32} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `Int32` that is 2's complement equivalent to the `UInt32`. -/
 @[inline] def UInt32.toInt32 (i : UInt32) : Int32 := Int32.ofUInt32 i
-@[inline, deprecated UInt32.toInt32 (since := "2025-02-13"), inherit_doc UInt32.toInt32]
-def Int32.mk (i : UInt32) : Int32 := UInt32.toInt32 i
+
 /--
 Converts an arbitrary-precision integer to a 32-bit integer, wrapping on overflow or underflow.
 
@@ -886,8 +881,7 @@ Converts a 32-bit signed integer to a natural number, mapping all negative numbe
 Use `Int32.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def Int32.toNatClampNeg (i : Int32) : Nat := i.toInt.toNat
-@[inline, deprecated Int32.toNatClampNeg (since := "2025-02-13"), inherit_doc Int32.toNatClampNeg]
-def Int32.toNat (i : Int32) : Nat := i.toInt.toNat
+
 /-- Obtains the `Int32` whose 2's complement representation is the given `BitVec 32`. -/
 @[inline] def Int32.ofBitVec (b : BitVec 32) : Int32 := ⟨⟨b⟩⟩
 /--
@@ -1207,8 +1201,7 @@ theorem Int64.toBitVec.inj : {x y : Int64} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `Int64` that is 2's complement equivalent to the `UInt64`. -/
 @[inline] def UInt64.toInt64 (i : UInt64) : Int64 := Int64.ofUInt64 i
-@[inline, deprecated UInt64.toInt64 (since := "2025-02-13"), inherit_doc UInt64.toInt64]
-def Int64.mk (i : UInt64) : Int64 := UInt64.toInt64 i
+
 /--
 Converts an arbitrary-precision integer to a 64-bit integer, wrapping on overflow or underflow.
 
@@ -1278,8 +1271,7 @@ Converts a 64-bit signed integer to a natural number, mapping all negative numbe
 Use `Int64.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def Int64.toNatClampNeg (i : Int64) : Nat := i.toInt.toNat
-@[inline, deprecated Int64.toNatClampNeg (since := "2025-02-13"), inherit_doc Int64.toNatClampNeg]
-def Int64.toNat (i : Int64) : Nat := i.toInt.toNat
+
 /-- Obtains the `Int64` whose 2's complement representation is the given `BitVec 64`. -/
 @[inline] def Int64.ofBitVec (b : BitVec 64) : Int64 := ⟨⟨b⟩⟩
 /--
@@ -1613,8 +1605,7 @@ theorem ISize.toBitVec.inj : {x y : ISize} → x.toBitVec = y.toBitVec → x = y
 
 /-- Obtains the `ISize` that is 2's complement equivalent to the `USize`. -/
 @[inline] def USize.toISize (i : USize) : ISize := ISize.ofUSize i
-@[inline, deprecated USize.toISize (since := "2025-02-13"), inherit_doc USize.toISize]
-def ISize.mk (i : USize) : ISize := USize.toISize i
+
 /--
 Converts an arbitrary-precision integer to a word-sized signed integer, wrapping around on over- or
 underflow.
@@ -1647,8 +1638,7 @@ Converts a word-sized signed integer to a natural number, mapping all negative n
 Use `ISize.toBitVec` to obtain the two's complement representation.
 -/
 @[inline] def ISize.toNatClampNeg (i : ISize) : Nat := i.toInt.toNat
-@[inline, deprecated ISize.toNatClampNeg (since := "2025-02-13"), inherit_doc ISize.toNatClampNeg]
-def ISize.toNat (i : ISize) : Nat := i.toInt.toNat
+
 /-- Obtains the `ISize` whose 2's complement representation is the given `BitVec`. -/
 @[inline] def ISize.ofBitVec (b : BitVec System.Platform.numBits) : ISize := ⟨⟨b⟩⟩
 /--
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index d510749bf7..486055c39a 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -21,12 +21,7 @@ open Nat
 
 /-- Converts a `Fin UInt8.size` into the corresponding `UInt8`. -/
 @[inline] def UInt8.ofFin (a : Fin UInt8.size) : UInt8 := ⟨⟨a⟩⟩
-@[deprecated UInt8.ofBitVec (since := "2025-02-12"), inherit_doc UInt8.ofBitVec]
-def UInt8.mk (bitVec : BitVec 8) : UInt8 :=
-  UInt8.ofBitVec bitVec
-@[inline, deprecated UInt8.ofNatLT (since := "2025-02-13"), inherit_doc UInt8.ofNatLT]
-def UInt8.ofNatCore (n : Nat) (h : n < UInt8.size) : UInt8 :=
-  UInt8.ofNatLT n h
+
 
 /-- Converts an `Int` to a `UInt8` by taking the (non-negative remainder of the division by `2 ^ 8`. -/
 def UInt8.ofInt (x : Int) : UInt8 := ofNat (x % 2 ^ 8).toNat
@@ -190,12 +185,6 @@ instance : Min UInt8 := minOfLe
 
 /-- Converts a `Fin UInt16.size` into the corresponding `UInt16`. -/
 @[inline] def UInt16.ofFin (a : Fin UInt16.size) : UInt16 := ⟨⟨a⟩⟩
-@[deprecated UInt16.ofBitVec (since := "2025-02-12"), inherit_doc UInt16.ofBitVec]
-def UInt16.mk (bitVec : BitVec 16) : UInt16 :=
-  UInt16.ofBitVec bitVec
-@[inline, deprecated UInt16.ofNatLT (since := "2025-02-13"), inherit_doc UInt16.ofNatLT]
-def UInt16.ofNatCore (n : Nat) (h : n < UInt16.size) : UInt16 :=
-  UInt16.ofNatLT n h
 
 /-- Converts an `Int` to a `UInt16` by taking the (non-negative remainder of the division by `2 ^ 16`. -/
 def UInt16.ofInt (x : Int) : UInt16 := ofNat (x % 2 ^ 16).toNat
@@ -406,12 +395,6 @@ instance : Min UInt16 := minOfLe
 
 /-- Converts a `Fin UInt32.size` into the corresponding `UInt32`. -/
 @[inline] def UInt32.ofFin (a : Fin UInt32.size) : UInt32 := ⟨⟨a⟩⟩
-@[deprecated UInt32.ofBitVec (since := "2025-02-12"), inherit_doc UInt32.ofBitVec]
-def UInt32.mk (bitVec : BitVec 32) : UInt32 :=
-  UInt32.ofBitVec bitVec
-@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT]
-def UInt32.ofNatCore (n : Nat) (h : n < UInt32.size) : UInt32 :=
-  UInt32.ofNatLT n h
 
 /-- Converts an `Int` to a `UInt32` by taking the (non-negative remainder of the division by `2 ^ 32`. -/
 def UInt32.ofInt (x : Int) : UInt32 := ofNat (x % 2 ^ 32).toNat
@@ -585,12 +568,6 @@ def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0
 
 /-- Converts a `Fin UInt64.size` into the corresponding `UInt64`. -/
 @[inline] def UInt64.ofFin (a : Fin UInt64.size) : UInt64 := ⟨⟨a⟩⟩
-@[deprecated UInt64.ofBitVec (since := "2025-02-12"), inherit_doc UInt64.ofBitVec]
-def UInt64.mk (bitVec : BitVec 64) : UInt64 :=
-  UInt64.ofBitVec bitVec
-@[inline, deprecated UInt64.ofNatLT (since := "2025-02-13"), inherit_doc UInt64.ofNatLT]
-def UInt64.ofNatCore (n : Nat) (h : n < UInt64.size) : UInt64 :=
-  UInt64.ofNatLT n h
 
 /-- Converts an `Int` to a `UInt64` by taking the (non-negative remainder of the division by `2 ^ 64`. -/
 def UInt64.ofInt (x : Int) : UInt64 := ofNat (x % 2 ^ 64).toNat
@@ -799,12 +776,6 @@ instance : Min UInt64 := minOfLe
 
 /-- Converts a `Fin USize.size` into the corresponding `USize`. -/
 @[inline] def USize.ofFin (a : Fin USize.size) : USize := ⟨⟨a⟩⟩
-@[deprecated USize.ofBitVec (since := "2025-02-12"), inherit_doc USize.ofBitVec]
-def USize.mk (bitVec : BitVec System.Platform.numBits) : USize :=
-  USize.ofBitVec bitVec
-@[inline, deprecated USize.ofNatLT (since := "2025-02-13"), inherit_doc USize.ofNatLT]
-def USize.ofNatCore (n : Nat) (h : n < USize.size) : USize :=
-  USize.ofNatLT n h
 
 /-- Converts an `Int` to a `USize` by taking the (non-negative remainder of the division by `2 ^ numBits`. -/
 def USize.ofInt (x : Int) : USize := ofNat (x % 2 ^ System.Platform.numBits).toNat
@@ -812,14 +783,6 @@ def USize.ofInt (x : Int) : USize := ofNat (x % 2 ^ System.Platform.numBits).toN
 @[simp] theorem USize.le_size : 2 ^ 32 ≤ USize.size := by cases USize.size_eq <;> simp_all
 @[simp] theorem USize.size_le : USize.size ≤ 2 ^ 64 := by cases USize.size_eq <;> simp_all
 
-@[deprecated USize.size_le (since := "2025-02-24")]
-theorem usize_size_le : USize.size ≤ 18446744073709551616 :=
-  USize.size_le
-
-@[deprecated USize.le_size (since := "2025-02-24")]
-theorem le_usize_size : 4294967296 ≤ USize.size :=
-  USize.le_size
-
 /--
 Multiplies two word-sized unsigned integers, wrapping around on overflow.  Usually accessed via the
 `*` operator.
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
index 2f7b00cbbc..58294b9b83 100644
--- a/src/Init/Data/UInt/BasicAux.lean
+++ b/src/Init/Data/UInt/BasicAux.lean
@@ -26,8 +26,6 @@ open Nat
 
 /-- Converts a `UInt8` into the corresponding `Fin UInt8.size`. -/
 def UInt8.toFin (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin
-@[deprecated UInt8.toFin (since := "2025-02-12"), inherit_doc UInt8.toFin]
-def UInt8.val (x : UInt8) : Fin UInt8.size := x.toFin
 
 /--
 Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if
@@ -67,8 +65,6 @@ instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩
 
 /-- Converts a `UInt16` into the corresponding `Fin UInt16.size`. -/
 def UInt16.toFin (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin
-@[deprecated UInt16.toFin (since := "2025-02-12"), inherit_doc UInt16.toFin]
-def UInt16.val (x : UInt16) : Fin UInt16.size := x.toFin
 
 /--
 Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.
@@ -134,8 +130,6 @@ instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩
 
 /-- Converts a `UInt32` into the corresponding `Fin UInt32.size`. -/
 def UInt32.toFin (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin
-@[deprecated UInt32.toFin (since := "2025-02-12"), inherit_doc UInt32.toFin]
-def UInt32.val (x : UInt32) : Fin UInt32.size := x.toFin
 
 /--
 Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.
@@ -149,8 +143,7 @@ Examples:
 -/
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩
-@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT]
-def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := UInt32.ofNatLT n h
+
 /--
 Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if
 the number is too large.
@@ -210,23 +203,14 @@ theorem UInt32.ofNatLT_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UIn
   simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat,
     Fin.Internal.ofNat_eq_ofNat, Fin.ofNat, Nat.mod_eq_of_lt h2, imp_self]
 
-@[deprecated UInt32.ofNatLT_lt_of_lt (since := "2025-02-13")]
-theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
-     n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m := UInt32.ofNatLT_lt_of_lt h1 h2
-
 theorem UInt32.lt_ofNatLT_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
      m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := by
   simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.Internal.ofNat_eq_ofNat,
     Fin.ofNat, Nat.mod_eq_of_lt h2, imp_self]
 
-@[deprecated UInt32.lt_ofNatLT_of_lt (since := "2025-02-13")]
-theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) :
-     m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := UInt32.lt_ofNatLT_of_lt h1 h2
-
 /-- Converts a `UInt64` into the corresponding `Fin UInt64.size`. -/
 def UInt64.toFin (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin
-@[deprecated UInt64.toFin (since := "2025-02-12"), inherit_doc UInt64.toFin]
-def UInt64.val (x : UInt64) : Fin UInt64.size := x.toFin
+
 /--
 Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.
 
@@ -315,18 +299,9 @@ def UInt32.toUInt64 (a : UInt32) : UInt64 := ⟨⟨a.toNat, Nat.lt_trans a.toBit
 
 instance UInt64.instOfNat : OfNat UInt64 n := ⟨UInt64.ofNat n⟩
 
-@[deprecated USize.size_eq (since := "2025-02-24")]
-theorem usize_size_eq : USize.size = 4294967296 ∨ USize.size = 18446744073709551616 :=
-  USize.size_eq
-
-@[deprecated USize.size_pos (since := "2025-02-24")]
-theorem usize_size_pos : 0 < USize.size :=
-  USize.size_pos
-
 /-- Converts a `USize` into the corresponding `Fin USize.size`. -/
 def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin
-@[deprecated USize.toFin (since := "2025-02-12"), inherit_doc USize.toFin]
-def USize.val (x : USize) : Fin USize.size := x.toFin
+
 /--
 Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on
 overflow.
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index da178dc85d..9358b8a181 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -42,9 +42,6 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
 
   @[simp] theorem toNat_ofBitVec : (ofBitVec a).toNat = a.toNat := (rfl)
 
-  @[deprecated toNat_ofBitVec (since := "2025-02-12")]
-  theorem toNat_mk : (ofBitVec a).toNat = a.toNat := (rfl)
-
   @[simp] theorem toNat_ofNat' {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat ..
 
   -- Not `simp` because we have simprocs which will avoid the modulo.
@@ -52,34 +49,14 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
 
   @[simp] theorem toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT ..
 
-  @[deprecated toNat_ofNatLT (since := "2025-02-13")]
-  theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT ..
-
   @[simp] theorem toFin_val (x : $typeName) : x.toFin.val = x.toNat := (rfl)
-  @[deprecated toFin_val (since := "2025-02-12")]
-  theorem val_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := (rfl)
 
   @[simp] theorem toNat_toBitVec (x : $typeName) : x.toBitVec.toNat = x.toNat := (rfl)
   @[simp] theorem toFin_toBitVec (x : $typeName) : x.toBitVec.toFin = x.toFin := (rfl)
 
-  @[deprecated toNat_toBitVec (since := "2025-02-21")]
-  theorem toNat_toBitVec_eq_toNat (x : $typeName) : x.toBitVec.toNat = x.toNat := (rfl)
-
   @[simp] theorem ofBitVec_toBitVec : ∀ (a : $typeName), ofBitVec a.toBitVec = a
     | ⟨_, _⟩ => rfl
 
-  @[deprecated ofBitVec_toBitVec (since := "2025-02-21")]
-  theorem ofBitVec_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a :=
-    ofBitVec_toBitVec
-
-  @[deprecated ofBitVec_toBitVec_eq (since := "2025-02-12")]
-  theorem mk_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
-    | ⟨_, _⟩ => rfl
-
-  @[deprecated "Use `toNat_toBitVec` and `toNat_ofNat_of_lt`." (since := "2025-03-05")]
-  theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
-    Nat.mod_eq_of_lt
-
   theorem toBitVec_ofNat' (n : Nat) : (ofNat n).toBitVec = BitVec.ofNat _ n := (rfl)
 
   theorem toNat_ofNat_of_lt' {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
@@ -140,17 +117,10 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
   protected theorem eq_of_toFin_eq {a b : $typeName} (h : a.toFin = b.toFin) : a = b := by
     rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [toFin]
   open $typeName (eq_of_toFin_eq) in
-  @[deprecated eq_of_toFin_eq (since := "2025-02-12")]
-  protected theorem eq_of_val_eq {a b : $typeName} (h : a.toFin = b.toFin) : a = b :=
-    eq_of_toFin_eq h
 
   open $typeName (eq_of_toFin_eq) in
   protected theorem toFin_inj {a b : $typeName} : a.toFin = b.toFin ↔ a = b :=
     Iff.intro eq_of_toFin_eq (congrArg toFin)
-  open $typeName (toFin_inj) in
-  @[deprecated toFin_inj (since := "2025-02-12")]
-  protected theorem val_inj {a b : $typeName} : a.toFin = b.toFin ↔ a = b :=
-    toFin_inj
 
   open $typeName (eq_of_toBitVec_eq) in
   protected theorem toBitVec_ne_of_ne {a b : $typeName} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec :=
@@ -236,8 +206,6 @@ instance : LawfulOrderLT $typeName where
 
   @[simp]
   theorem toFin_ofNat (n : Nat) : toFin (no_index (OfNat.ofNat n)) = OfNat.ofNat n := (rfl)
-  @[deprecated toFin_ofNat (since := "2025-02-12")]
-  theorem val_ofNat (n : Nat) : toFin (no_index (OfNat.ofNat n)) = OfNat.ofNat n := (rfl)
 
   @[simp, int_toBitVec]
   theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := (rfl)
@@ -245,9 +213,6 @@ instance : LawfulOrderLT $typeName where
   @[simp]
   theorem ofBitVec_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := (rfl)
 
-  @[deprecated ofBitVec_ofNat (since := "2025-02-12")]
-  theorem mk_ofNat (n : Nat) : ofBitVec (BitVec.ofNat _ n) = OfNat.ofNat n := (rfl)
-
   @[simp, int_toBitVec] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := (rfl)
   @[simp, int_toBitVec] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := (rfl)
   @[simp, int_toBitVec] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := (rfl)
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 1c6c876f75..a93eea98b8 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -172,9 +172,6 @@ theorem attach_map_val (xs : Vector α n) (f : α → β) :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[deprecated attach_map_val (since := "2025-02-17")]
-abbrev attach_map_coe := @attach_map_val
-
 -- The argument `xs : Vector α n` is explicit to allow rewriting from right to left.
 theorem attach_map_subtype_val (xs : Vector α n) : xs.attach.map Subtype.val = xs := by
   rcases xs with ⟨xs, rfl⟩
@@ -185,9 +182,6 @@ theorem attachWith_map_val {p : α → Prop} {f : α → β} {xs : Vector α n}
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[deprecated attachWith_map_val (since := "2025-02-17")]
-abbrev attachWith_map_coe := @attachWith_map_val
-
 theorem attachWith_map_subtype_val {p : α → Prop} {xs : Vector α n} (H : ∀ a ∈ xs, p a) :
     (xs.attachWith p H).map Subtype.val = xs := by
   rcases xs with ⟨xs, rfl⟩
@@ -345,9 +339,6 @@ theorem map_attach_eq_pmap {xs : Vector α n} {f : { x // x ∈ xs } → β} :
   rcases xs with ⟨xs, rfl⟩
   ext <;> simp
 
-@[deprecated map_attach_eq_pmap (since := "2025-02-09")]
-abbrev map_attach := @map_attach_eq_pmap
-
 @[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {xs : Vector α n} (H₁ H₂) :
     pmap f (pmap g xs H₁) H₂ =
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index 296955e54a..c2256fefc1 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -250,11 +250,6 @@ theorem getElem_of_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx
     (c[i]? = some c[i]) ↔ True := by
   simp [h]
 
-@[deprecated getElem?_eq_none_iff (since := "2025-02-17")]
-abbrev getElem?_eq_none := @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
   simp only [getElem?_def]
diff --git a/src/Init/System/Promise.lean b/src/Init/System/Promise.lean
index 85ae890618..c257b29461 100644
--- a/src/Init/System/Promise.lean
+++ b/src/Init/System/Promise.lean
@@ -71,9 +71,6 @@ def Promise.result! (promise : @& Promise α) : Task α :=
   let _ : Nonempty α := promise.h
   promise.result?.map (sync := true) Option.getOrBlock!
 
-@[inherit_doc Promise.result!, deprecated Promise.result! (since := "2025-02-05")]
-def Promise.result := @Promise.result!
-
 /--
 Like `Promise.result`, but resolves to `dflt` if the promise is dropped without ever being resolved.
 -/
diff --git a/src/Lean/Elab/Tactic/BoolToPropSimps.lean b/src/Lean/Elab/Tactic/BoolToPropSimps.lean
index 4304ee5f6f..d809db591c 100644
--- a/src/Lean/Elab/Tactic/BoolToPropSimps.lean
+++ b/src/Lean/Elab/Tactic/BoolToPropSimps.lean
@@ -14,8 +14,3 @@ public section
 builtin_initialize bool_to_prop : Lean.Meta.SimpExtension ←
   Lean.Meta.registerSimpAttr `bool_to_prop
     "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
-
-@[deprecated bool_to_prop (since := "2025-02-10")]
-builtin_initialize boolToPropSimps : Lean.Meta.SimpExtension ←
-  Lean.Meta.registerSimpAttr `boolToPropSimps
-    "simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index 61ec17821d..fc9210c150 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -707,8 +707,3 @@ def evalOmega : Tactic
 builtin_initialize bitvec_to_nat : SimpExtension ←
   registerSimpAttr `bitvec_to_nat
     "simp lemmas converting `BitVec` goals to `Nat` goals"
-
-@[deprecated bitvec_to_nat (since := "2025-02-10")]
-builtin_initialize bvOmegaSimpExtension : SimpExtension ←
-  registerSimpAttr `bv_toNat
-    "simp lemmas converting `BitVec` goals to `Nat` goals, for the `bv_omega` preprocessor"
diff --git a/src/Lean/Elab/Tactic/Omega/OmegaM.lean b/src/Lean/Elab/Tactic/Omega/OmegaM.lean
index abed39f0d1..15698f461c 100644
--- a/src/Lean/Elab/Tactic/Omega/OmegaM.lean
+++ b/src/Lean/Elab/Tactic/Omega/OmegaM.lean
@@ -216,7 +216,7 @@ def analyzeAtom (e : Expr) : OmegaM (List Expr) := do
         | some _ =>
           let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Nat []) (.const ``instLTNat [])
             (toExpr (0 : Nat)) b
-          let pow_pos := mkApp3 (.const ``Nat.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
+          let pow_pos := mkApp3 (.const ``Nat.pow_pos []) b exp (← mkDecideProof b_pos)
           let cast_pos := mkApp2 (.const ``Int.ofNat_pos_of_pos []) k' pow_pos
           pure [mkApp3 (.const ``Int.emod_nonneg []) x k
                   (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos),
diff --git a/src/Lean/Util.lean b/src/Lean/Util.lean
index 8ced0e6a06..304b078ff6 100644
--- a/src/Lean/Util.lean
+++ b/src/Lean/Util.lean
@@ -32,7 +32,6 @@ public import Lean.Util.TestExtern
 public import Lean.Util.OccursCheck
 public import Lean.Util.HasConstCache
 public import Lean.Util.Heartbeats
-public import Lean.Util.SearchPath
 public import Lean.Util.SafeExponentiation
 public import Lean.Util.NumObjs
 public import Lean.Util.NumApps
diff --git a/src/Lean/Util/SearchPath.lean b/src/Lean/Util/SearchPath.lean
deleted file mode 100644
index 0ef4dc3eca..0000000000
--- a/src/Lean/Util/SearchPath.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
--/
-module
-
-prelude
-public import Lean.ToExpr
-public import Lean.Util.Path
-public import Lean.Elab.Term
-meta import Lean.Elab.Term
-
-public section
-
-open Lean
-
-/--
-Term elaborator that retrieves the current `SearchPath`.
-
-Typical usage is `searchPathRef.set compile_time_search_path%`.
-
-This must not be used in files that are potentially compiled on another machine and then imported.
-(That is, if used in an imported file it will embed the search path from whichever machine
-compiled the `.olean`.)
--/
-@[deprecated "Deprecated without replacement." (since := "2025-02-10")]
-elab "compile_time_search_path%" : term => do
-  logWarning "`compile_time_search_path%` is deprecated; use `initSearchPath (← findSysroot)` instead."
-  return toExpr (← searchPathRef.get)
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 53b4ea721b..1e6c941b97 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -1228,11 +1228,6 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
     m.toList.map Sigma.fst = m.keys :=
   Raw₀.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
 
-@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
-theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
-    m.toList.map Sigma.fst = m.keys :=
-  Raw₀.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
-
 @[simp, grind =]
 theorem length_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.length = m.size :=
@@ -1279,11 +1274,6 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
     (toList m).map Prod.fst = m.keys :=
   Raw₀.Const.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
 
-@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
-theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
-    (toList m).map Prod.fst = m.keys :=
-  Raw₀.Const.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
-
 @[simp, grind =]
 theorem length_toList [EquivBEq α] [LawfulHashable α] :
     (toList m).length = m.size :=
@@ -1501,14 +1491,6 @@ theorem forMUncurried_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : α × β 
     Const.forMUncurried f m = (Const.toList m).forM f :=
   Raw₀.Const.forM_eq_forM_toList ⟨m.1, m.2.size_buckets_pos⟩
 
-/--
-Deprecated, use `forMUncurried_eq_forM_toList` together with `forM_eq_forMUncurried` instead.
--/
-@[deprecated forMUncurried_eq_forM_toList (since := "2025-03-02")]
-theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
-    DHashMap.forM f m = (Const.toList m).forM (fun a => f a.1 a.2) :=
-  Raw₀.Const.forM_eq_forM_toList ⟨m.1, m.2.size_buckets_pos⟩
-
 theorem forIn_eq_forInUncurried [Monad m'] [LawfulMonad m']
     {f : α → β → δ → m' (ForInStep δ)} {init : δ} :
     DHashMap.forIn f init m = forInUncurried (fun a b => f a.1 a.2 b) init m := (rfl)
@@ -1518,39 +1500,6 @@ theorem forInUncurried_eq_forIn_toList [Monad m'] [LawfulMonad m']
     Const.forInUncurried f init m = ForIn.forIn (Const.toList m) init f :=
   Raw₀.Const.forIn_eq_forIn_toList ⟨m.1, m.2.size_buckets_pos⟩
 
-/--
-Deprecated, use `forInUncurried_eq_forIn_toList` together with `forIn_eq_forInUncurried` instead.
--/
-@[deprecated forInUncurried_eq_forIn_toList (since := "2025-03-02")]
-theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
-    {f : α × β → δ → m' (ForInStep δ)} {init : δ} :
-    Const.forInUncurried f init m = ForIn.forIn (Const.toList m) init f :=
-  Raw₀.Const.forIn_eq_forIn_toList ⟨m.1, m.2.size_buckets_pos⟩
-
-variable {m : DHashMap α (fun _ => Unit)}
-
-@[deprecated DHashMap.foldM_eq_foldlM_keys (since := "2025-02-28")]
-theorem foldM_eq_foldlM_keys [Monad m'] [LawfulMonad m']
-    {f : δ → α → m' δ} {init : δ} :
-    m.foldM (fun d a _ => f d a) init = m.keys.foldlM f init :=
-  Raw₀.foldM_eq_foldlM_keys ⟨m.1, m.2.size_buckets_pos⟩
-
-@[deprecated DHashMap.fold_eq_foldl_keys (since := "2025-02-28")]
-theorem fold_eq_foldl_keys {f : δ → α → δ} {init : δ} :
-    m.fold (fun d a _ => f d a) init = m.keys.foldl f init :=
-  Raw₀.fold_eq_foldl_keys ⟨m.1, m.2.size_buckets_pos⟩
-
-@[deprecated DHashMap.forM_eq_forM_keys (since := "2025-02-28")]
-theorem forM_eq_forM_keys [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
-    m.forM (fun a _ => f a) = m.keys.forM f :=
-  Raw₀.forM_eq_forM_keys ⟨m.1, m.2.size_buckets_pos⟩
-
-@[deprecated DHashMap.forIn_eq_forIn_keys (since := "2025-02-28")]
-theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m']
-    {f : α → δ → m' (ForInStep δ)} {init : δ} :
-    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keys init f :=
-  Raw₀.forIn_eq_forIn_keys ⟨m.1, m.2.size_buckets_pos⟩
-
 end Const
 
 theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 709796c7b8..60bdf43434 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1255,11 +1255,6 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.map Sigma.fst = m.keys := by
   apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩
 
-@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
-theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
-    m.toList.map Sigma.fst = m.keys := by
-  apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩
-
 @[simp]
 theorem toArray_keys (h : m.WF) :
     m.keys.toArray = m.keysArray :=
@@ -1349,11 +1344,6 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     (Raw.Const.toList m).map Prod.fst = m.keys := by
   apply Raw₀.Const.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩
 
-@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
-theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
-    (Raw.Const.toList m).map Prod.fst = m.keys := by
-  apply Raw₀.Const.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩
-
 @[simp, grind =]
 theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     (Raw.Const.toList m).length = m.size := by
@@ -1583,14 +1573,6 @@ theorem forMUncurried_eq_forM_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
     forMUncurried f m = (toList m).forM f :=
   Raw₀.Const.forM_eq_forM_toList ⟨m, h.size_buckets_pos⟩
 
-/--
-Deprecated, use `forMUncurried_eq_forM_toList` together with `forM_eq_forMUncurried` instead.
--/
-@[deprecated forMUncurried_eq_forM_toList (since := "2025-03-02")]
-theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] (h : m.WF) {f : (a : α) → β → m' PUnit} :
-    m.forM f = (Raw.Const.toList m).forM (fun a => f a.1 a.2) :=
-  Raw₀.Const.forM_eq_forM_toList ⟨m, h.size_buckets_pos⟩
-
 omit [BEq α] [Hashable α] in
 @[simp]
 theorem forIn_eq_forInUncurried [Monad m'] [LawfulMonad m']
@@ -1602,39 +1584,6 @@ theorem forInUncurried_eq_forIn_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
     forInUncurried f init m = ForIn.forIn (toList m) init f :=
   Raw₀.Const.forIn_eq_forIn_toList ⟨m, h.size_buckets_pos⟩
 
-/--
-Deprecated, use `forInUncurried_eq_forIn_toList` together with `forIn_eq_forInUncurried` instead.
--/
-@[deprecated forInUncurried_eq_forIn_toList (since := "2025-03-02")]
-theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
-    {f : (a : α) → β → δ → m' (ForInStep δ)} {init : δ} :
-    m.forIn f init = ForIn.forIn (Raw.Const.toList m) init (fun a b => f a.1 a.2 b) :=
-  Raw₀.Const.forIn_eq_forIn_toList ⟨m, h.size_buckets_pos⟩
-
-variable {m : Raw α (fun _ => Unit)}
-
-@[deprecated Raw.foldM_eq_foldlM_keys (since := "2025-02-28")]
-theorem foldM_eq_foldlM_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
-    {f : δ → α → m' δ} {init : δ} :
-    m.foldM (fun d a _ => f d a) init = m.keys.foldlM f init :=
-  Raw₀.foldM_eq_foldlM_keys ⟨m, h.size_buckets_pos⟩
-
-@[deprecated Raw.fold_eq_foldl_keys (since := "2025-02-28")]
-theorem fold_eq_foldl_keys (h : m.WF) {f : δ → α → δ} {init : δ} :
-    m.fold (fun d a _ => f d a) init = m.keys.foldl f init :=
-  Raw₀.fold_eq_foldl_keys ⟨m, h.size_buckets_pos⟩
-
-@[deprecated Raw.forM_eq_forM_keys (since := "2025-02-28")]
-theorem forM_eq_forM_keys [Monad m'] [LawfulMonad m'] (h : m.WF) {f : α → m' PUnit} :
-    m.forM (fun a _ => f a) = m.keys.forM f :=
-  Raw₀.forM_eq_forM_keys ⟨m, h.size_buckets_pos⟩
-
-@[deprecated Raw.forIn_eq_forIn_keys (since := "2025-02-28")]
-theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
-    {f : α → δ → m' (ForInStep δ)} {init : δ} :
-    m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keys init f :=
-  Raw₀.forIn_eq_forIn_keys ⟨m, h.size_buckets_pos⟩
-
 end Const
 
 theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean
index 28c6e6f2b0..b740d15cd1 100644
--- a/src/Std/Data/DTreeMap/Basic.lean
+++ b/src/Std/Data/DTreeMap/Basic.lean
@@ -213,10 +213,6 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 def get? [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) : Option (β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.get? a
 
-@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
-def find? [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) : Option (β a) :=
-  t.get? a
-
 /--
 Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.
 
@@ -235,10 +231,6 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 def get! [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) [Inhabited (β a)]  : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.get! a
 
-@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
-def find! [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) [Inhabited (β a)]  : β a :=
-  t.get! a
-
 /--
 Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 
@@ -248,10 +240,6 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 def getD [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (fallback : β a) : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.getD a fallback
 
-@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
-def findD [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (fallback : β a) : β a :=
-  t.getD a fallback
-
 /--
 Checks if a mapping for the given key exists and returns the key if it does, otherwise `none`.
 The result in the `some` case is guaranteed to be pointer equal to the key in the map.
@@ -708,10 +696,6 @@ def getThenInsertIfNew? (t : DTreeMap α β cmp) (a : α) (b : β) :
 def get? (t : DTreeMap α β cmp) (a : α) : Option β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get? t.inner a
 
-@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
-def find? (t : DTreeMap α β cmp) (a : α) : Option β :=
-  get? t a
-
 @[inline, inherit_doc DTreeMap.get]
 def get (t : DTreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get t.inner a h
@@ -720,18 +704,10 @@ def get (t : DTreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
 def get! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get! t.inner a
 
-@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
-def find! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
-  get! t a
-
 @[inline, inherit_doc DTreeMap.getD]
 def getD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.getD t.inner a fallback
 
-@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
-def findD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=
-  getD t a fallback
-
 @[inline, inherit_doc DTreeMap.minEntry?]
 def minEntry? (t : DTreeMap α β cmp) : Option (α × β) :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntry? t.inner
@@ -880,19 +856,11 @@ def filter (f : (a : α) → β a → Bool) (t : DTreeMap α β cmp) : DTreeMap
 def foldlM (f : δ → (a : α) → β a → m δ) (init : δ) (t : DTreeMap α β cmp) : m δ :=
   t.inner.foldlM f init
 
-@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
-def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (t : DTreeMap α β cmp) : m δ :=
-  t.foldlM f init
-
 /-- Folds the given function over the mappings in the map in ascending order. -/
 @[inline]
 def foldl (f : δ → (a : α) → β a → δ) (init : δ) (t : DTreeMap α β cmp) : δ :=
   t.inner.foldl f init
 
-@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
-def fold (f : δ → (a : α) → β a → δ) (init : δ) (t : DTreeMap α β cmp) : δ :=
-  t.foldl f init
-
 /-- Folds the given monadic function over the mappings in the map in descending order. -/
 @[inline]
 def foldrM (f : (a : α) → β a → δ → m δ) (init : δ) (t : DTreeMap α β cmp) : m δ :=
@@ -903,10 +871,6 @@ def foldrM (f : (a : α) → β a → δ → m δ) (init : δ) (t : DTreeMap α
 def foldr (f : (a : α) → β a → δ → δ) (init : δ) (t : DTreeMap α β cmp) : δ :=
   t.inner.foldr f init
 
-@[inline, inherit_doc foldr, deprecated foldr (since := "2025-02-12")]
-def revFold (f : δ → (a : α) → β a → δ) (init : δ) (t : DTreeMap α β cmp) : δ :=
-  foldr (fun k v acc => f acc k v) init t
-
 /-- Partitions a tree map into two tree maps based on a predicate. -/
 @[inline] def partition (f : (a : α) → β a → Bool)
     (t : DTreeMap α β cmp) : DTreeMap α β cmp × DTreeMap α β cmp :=
@@ -997,10 +961,6 @@ def ofList (l : List ((a : α) × β a)) (cmp : α → α → Ordering := by exa
     DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨Impl.ofList l, Impl.WF.empty.insertMany⟩
 
-@[inline, inherit_doc ofList, deprecated ofList (since := "2025-02-12")]
-def fromList (l : List ((a : α) × β a)) (cmp : α → α → Ordering) : DTreeMap α β cmp :=
-  ofList l cmp
-
 /-- Transforms the tree map into a list of mappings in ascending order. -/
 @[inline]
 def toArray (t : DTreeMap α β cmp) : Array ((a : α) × β a) :=
@@ -1012,10 +972,6 @@ def ofArray (a : Array ((a : α) × β a)) (cmp : α → α → Ordering := by e
     DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨Impl.ofArray a, Impl.WF.empty.insertMany⟩
 
-@[inline, inherit_doc ofArray, deprecated ofArray (since := "2025-02-12")]
-def fromArray (a : Array ((a : α) × β a)) (cmp : α → α → Ordering) : DTreeMap α β cmp :=
-  ofArray a cmp
-
 /--
 Modifies in place the value associated with a given key.
 
@@ -1056,11 +1012,6 @@ def mergeWith [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a)
     DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.mergeWith mergeFn t₂.inner t₁.wf.balanced |>.impl, t₁.wf.mergeWith⟩
 
-@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
-def mergeBy [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : DTreeMap α β cmp) :
-    DTreeMap α β cmp :=
-  mergeWith mergeFn t₁ t₂
-
 namespace Const
 
 variable {β : Type v}
@@ -1108,10 +1059,6 @@ def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : DTreeMap α β cm
   letI : Ord α := ⟨cmp⟩;
   ⟨Impl.Const.mergeWith mergeFn t₁.inner t₂.inner t₁.wf.balanced |>.impl, t₁.wf.constMergeWith⟩
 
-@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
-def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp :=
-  mergeWith mergeFn t₁ t₂
-
 end Const
 
 /--
diff --git a/src/Std/Data/DTreeMap/Raw/Basic.lean b/src/Std/Data/DTreeMap/Raw/Basic.lean
index c80f715c20..546e172baf 100644
--- a/src/Std/Data/DTreeMap/Raw/Basic.lean
+++ b/src/Std/Data/DTreeMap/Raw/Basic.lean
@@ -171,10 +171,6 @@ def erase (t : Raw α β cmp) (a : α) : Raw α β cmp :=
 def get? [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) : Option (β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.get? a
 
-@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
-def find? [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) : Option (β a) :=
-  t.get? a
-
 @[inline, inherit_doc DTreeMap.get]
 def get [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (h : a ∈ t) : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.get a h
@@ -183,18 +179,10 @@ def get [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (h : a ∈ t) : β a :=
 def get! [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) [Inhabited (β a)]  : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.get! a
 
-@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
-def find! [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) [Inhabited (β a)]  : β a :=
-  t.get! a
-
 @[inline, inherit_doc DTreeMap.getD]
 def getD [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (fallback : β a) : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.getD a fallback
 
-@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
-def findD [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (fallback : β a) : β a :=
-  t.getD a fallback
-
 @[inline, inherit_doc DTreeMap.getKey?]
 def getKey? (t : Raw α β cmp) (a : α) : Option α :=
   letI : Ord α := ⟨cmp⟩; t.inner.getKey? a
@@ -461,10 +449,6 @@ def getThenInsertIfNew? (t : Raw α β cmp) (a : α) (b : β) : Option β × Raw
 def get? (t : Raw α β cmp) (a : α) : Option β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get? t.inner a
 
-@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
-def find? (t : Raw α β cmp) (a : α) : Option β :=
-  get? t a
-
 @[inline, inherit_doc DTreeMap.Const.get]
 def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get t.inner a h
@@ -473,18 +457,10 @@ def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
 def get! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get! t.inner a
 
-@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
-def find! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
-  get! t a
-
 @[inline, inherit_doc DTreeMap.Const.getD]
 def getD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.getD t.inner a fallback
 
-@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
-def findD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
-  getD t a fallback
-
 @[inline, inherit_doc DTreeMap.Const.minEntry?]
 def minEntry? (t : Raw α β cmp) : Option (α × β) :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.minEntry? t.inner
@@ -618,18 +594,10 @@ def filter (f : (a : α) → β a → Bool) (t : Raw α β cmp) : Raw α β cmp
 def foldlM (f : δ → (a : α) → β a → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
   t.inner.foldlM f init
 
-@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
-def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
-  t.foldlM f init
-
 @[inline, inherit_doc DTreeMap.foldl]
 def foldl (f : δ → (a : α) → β a → δ) (init : δ) (t : Raw α β cmp) : δ :=
   t.inner.foldl f init
 
-@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
-def fold (f : δ → (a : α) → β a → δ) (init : δ) (t : Raw α β cmp) : δ :=
-  t.foldl f init
-
 @[inline, inherit_doc DTreeMap.foldrM]
 def foldrM (f : (a : α) → β a → δ → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
   t.inner.foldrM f init
@@ -638,10 +606,6 @@ def foldrM (f : (a : α) → β a → δ → m δ) (init : δ) (t : Raw α β cm
 def foldr (f : (a : α) → β a → δ → δ) (init : δ) (t : Raw α β cmp) : δ :=
   t.inner.foldr f init
 
-@[inline, inherit_doc foldr, deprecated foldr (since := "2025-02-12")]
-def revFold (f : δ → (a : α) → β a → δ) (init : δ) (t : Raw α β cmp) : δ :=
-  foldr (fun k v acc => f acc k v) init t
-
 @[inline, inherit_doc DTreeMap.partition]
 def partition (f : (a : α) → β a → Bool) (t : Raw α β cmp) : Raw α β cmp × Raw α β cmp :=
   t.foldl (init := (∅, ∅)) fun ⟨l, r⟩ a b =>
@@ -722,10 +686,6 @@ def ofList (l : List ((a : α) × β a)) (cmp : α → α → Ordering := by exa
   letI : Ord α := ⟨cmp⟩
   ⟨Impl.ofList l⟩
 
-@[inline, inherit_doc ofList, deprecated ofList (since := "2025-02-12")]
-def fromList (l : List ((a : α) × β a)) (cmp : α → α → Ordering) : Raw α β cmp :=
-  ofList l cmp
-
 @[inline, inherit_doc DTreeMap.toArray]
 def toArray (t : Raw α β cmp) : Array ((a : α) × β a) :=
   t.inner.toArray
@@ -736,10 +696,6 @@ def ofArray (a : Array ((a : α) × β a)) (cmp : α → α → Ordering := by e
   letI : Ord α := ⟨cmp⟩
   ⟨Impl.ofArray a⟩
 
-@[inline, inherit_doc ofArray, deprecated ofArray (since := "2025-02-12")]
-def fromArray (a : Array ((a : α) × β a)) (cmp : α → α → Ordering) : Raw α β cmp :=
-  ofArray a cmp
-
 @[inline, inherit_doc DTreeMap.modify]
 def modify [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (f : β a → β a) : Raw α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨t.inner.modify a f⟩
@@ -754,11 +710,6 @@ def mergeWith [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a)
     Raw α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.mergeWith! mergeFn t₂.inner⟩
 
-@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
-def mergeBy [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : Raw α β cmp) :
-    Raw α β cmp :=
-  mergeWith mergeFn t₁ t₂
-
 namespace Const
 open Internal (Impl)
 
@@ -800,10 +751,6 @@ def alter (t : Raw α β cmp) (a : α) (f : Option β → Option β) : Raw α β
 def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨Impl.Const.mergeWith! mergeFn t₁.inner t₂.inner⟩
 
-@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
-def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
-  mergeWith mergeFn t₁ t₂
-
 end Const
 
 @[inline, inherit_doc DTreeMap.insertMany]
diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean
index 875adf85cc..5511d31603 100644
--- a/src/Std/Data/ExtHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtHashMap/Lemmas.lean
@@ -1452,25 +1452,11 @@ theorem size_le_size_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Optio
         m[k']? :=
   ExtDHashMap.Const.get?_alter
 
-@[deprecated getElem?_alter (since := "2025-02-09")]
-theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
-    get? (alter m k f) k' =
-      if k == k' then
-        f (get? m k)
-      else
-        get? m k' :=
-  ExtDHashMap.Const.get?_alter
-
 @[simp]
 theorem getElem?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
     (alter m k f)[k]? = f m[k]? :=
   ExtDHashMap.Const.get?_alter_self
 
-@[deprecated getElem?_alter_self (since := "2025-02-09")]
-theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
-    get? (alter m k f) k = f (get? m k) :=
-  ExtDHashMap.Const.get?_alter_self
-
 @[grind =] theorem getElem_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
     {h : k' ∈ alter m k f} :
     (alter m k f)[k'] =
@@ -1482,18 +1468,6 @@ theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option 
         m[(k')]'h' :=
   ExtDHashMap.Const.get_alter (h := h)
 
-@[deprecated getElem_alter (since := "2025-02-09")]
-theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
-    {h : k' ∈ alter m k f} :
-    get (alter m k f) k' h =
-      if heq : k == k' then
-        haveI h' : (f (get? m k)).isSome := mem_alter_of_beq heq |>.mp h
-        f (get? m k) |>.get h'
-      else
-        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
-        get m k' h' :=
-  ExtDHashMap.Const.get_alter
-
 @[simp]
 theorem getElem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
     {h : k ∈ alter m k f} :
@@ -1501,13 +1475,6 @@ theorem getElem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Optio
     (alter m k f)[k] = (f m[k]?).get h' :=
   ExtDHashMap.Const.get_alter_self (h := h)
 
-@[deprecated getElem_alter_self (since := "2025-02-09")]
-theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
-    {h : k ∈ alter m k f} :
-    haveI h' : (f (get? m k)).isSome := mem_alter_self.mp h
-    get (alter m k f) k h = (f (get? m k)).get h' :=
-  ExtDHashMap.Const.get_alter_self
-
 @[grind =] theorem getElem!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
     {f : Option β → Option β} : (alter m k f)[k']! =
       if k == k' then
@@ -1516,25 +1483,11 @@ theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β
         m[k']! :=
   ExtDHashMap.Const.get!_alter
 
-@[deprecated getElem!_alter (since := "2025-02-09")]
-theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
-    {f : Option β → Option β} : get! (alter m k f) k' =
-      if k == k' then
-        f (get? m k) |>.get!
-      else
-        get! m k' :=
-  ExtDHashMap.Const.get!_alter
-
 @[simp]
 theorem getElem!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
     {f : Option β → Option β} : (alter m k f)[k]! = (f m[k]?).get! :=
   ExtDHashMap.Const.get!_alter_self
 
-@[deprecated getElem!_alter_self (since := "2025-02-09")]
-theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
-    {f : Option β → Option β} : get! (alter m k f) k = (f (get? m k)).get! :=
-  ExtDHashMap.Const.get!_alter_self
-
 @[grind =] theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β}
     {f : Option β → Option β} :
     getD (alter m k f) k' fallback =
@@ -1639,25 +1592,11 @@ theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
         m[k']? :=
   ExtDHashMap.Const.get?_modify
 
-@[deprecated getElem?_modify (since := "2025-02-09")]
-theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
-    get? (modify m k f) k' =
-      if k == k' then
-        get? m k |>.map f
-      else
-        get? m k' :=
-  ExtDHashMap.Const.get?_modify
-
 @[simp]
 theorem getElem?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
     (modify m k f)[k]? = m[k]?.map f :=
   ExtDHashMap.Const.get?_modify_self
 
-@[deprecated getElem?_modify_self (since := "2025-02-09")]
-theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
-    get? (modify m k f) k = (get? m k).map f :=
-  ExtDHashMap.Const.get?_modify_self
-
 @[grind =] theorem getElem_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
     {h : k' ∈ modify m k f} :
     (modify m k f)[k'] =
@@ -1669,18 +1608,6 @@ theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β →
         m[k'] :=
   ExtDHashMap.Const.get_modify (h := h)
 
-@[deprecated getElem_modify (since := "2025-02-09")]
-theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
-    {h : k' ∈ modify m k f} :
-    get (modify m k f) k' h =
-      if heq : k == k' then
-        haveI h' : k ∈ m := mem_congr heq |>.mpr <| mem_modify.mp h
-        f (get m k h')
-      else
-        haveI h' : k' ∈ m := mem_modify.mp h
-        get m k' h' :=
-  ExtDHashMap.Const.get_modify
-
 @[simp]
 theorem getElem_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β}
     {h : k ∈ modify m k f} :
@@ -1688,13 +1615,6 @@ theorem getElem_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β 
     (modify m k f)[k] = f m[k] :=
   ExtDHashMap.Const.get_modify_self (h := h)
 
-@[deprecated getElem_modify_self (since := "2025-02-09")]
-theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β}
-    {h : k ∈ modify m k f} :
-    haveI h' : k ∈ m := mem_modify.mp h
-    get (modify m k f) k h = f (get m k h') :=
-  ExtDHashMap.Const.get_modify_self
-
 @[grind =] theorem getElem!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
     (modify m k f)[k']! =
       if k == k' then
@@ -1703,25 +1623,11 @@ theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → 
         m[k']! :=
   ExtDHashMap.Const.get!_modify
 
-@[deprecated getElem!_modify (since := "2025-02-09")]
-theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
-    get! (modify m k f) k' =
-      if k == k' then
-        get? m k |>.map f |>.get!
-      else
-        get! m k' :=
-  ExtDHashMap.Const.get!_modify
-
 @[simp]
 theorem getElem!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} :
     (modify m k f)[k]! = (m[k]?.map f).get! :=
   ExtDHashMap.Const.get!_modify_self
 
-@[deprecated getElem!_modify_self (since := "2025-02-09")]
-theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} :
-    get! (modify m k f) k = ((get? m k).map f).get! :=
-  ExtDHashMap.Const.get!_modify_self
-
 @[grind =] theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} :
     getD (modify m k f) k' fallback =
       if k == k' then
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index dc48708758..7dff8c621d 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -912,11 +912,6 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
     m.toList.map Prod.fst = m.keys :=
   DHashMap.Const.map_fst_toList_eq_keys
 
-@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
-theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
-    m.toList.map Prod.fst = m.keys :=
-  DHashMap.Const.map_fst_toList_eq_keys
-
 @[simp, grind =]
 theorem length_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.length = m.size :=
@@ -1845,25 +1840,11 @@ theorem getElem?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option
         m[k']? :=
   DHashMap.Const.get?_alter
 
-@[deprecated getElem?_alter (since := "2025-02-09")]
-theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
-    get? (alter m k f) k' =
-      if k == k' then
-        f (get? m k)
-      else
-        get? m k' :=
-  DHashMap.Const.get?_alter
-
 @[simp]
 theorem getElem?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
     (alter m k f)[k]? = f m[k]? :=
   DHashMap.Const.get?_alter_self
 
-@[deprecated getElem?_alter_self (since := "2025-02-09")]
-theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
-    get? (alter m k f) k = f (get? m k) :=
-  DHashMap.Const.get?_alter_self
-
 @[grind =]
 theorem getElem_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
     {h : k' ∈ alter m k f} :
@@ -1876,18 +1857,6 @@ theorem getElem_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option
         m[(k')]'h' :=
   DHashMap.Const.get_alter
 
-@[deprecated getElem_alter (since := "2025-02-09")]
-theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
-    {h : k' ∈ alter m k f} :
-    get (alter m k f) k' h =
-      if heq : k == k' then
-        haveI h' : (f (get? m k)).isSome := mem_alter_of_beq heq |>.mp h
-        f (get? m k) |>.get h'
-      else
-        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
-        get m k' h' :=
-  DHashMap.Const.get_alter
-
 @[simp]
 theorem getElem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
     {h : k ∈ alter m k f} :
@@ -1895,13 +1864,6 @@ theorem getElem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Optio
     (alter m k f)[k] = (f m[k]?).get h' :=
   DHashMap.Const.get_alter_self
 
-@[deprecated getElem_alter_self (since := "2025-02-09")]
-theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
-    {h : k ∈ alter m k f} :
-    haveI h' : (f (get? m k)).isSome := mem_alter_self.mp h
-    get (alter m k f) k h = (f (get? m k)).get h' :=
-  DHashMap.Const.get_alter_self
-
 @[grind =]
 theorem getElem!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
     {f : Option β → Option β} : (alter m k f)[k']! =
@@ -1911,25 +1873,11 @@ theorem getElem!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited
         m[k']! :=
   DHashMap.Const.get!_alter
 
-@[deprecated getElem!_alter (since := "2025-02-09")]
-theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
-    {f : Option β → Option β} : get! (alter m k f) k' =
-      if k == k' then
-        f (get? m k) |>.get!
-      else
-        get! m k' :=
-  DHashMap.Const.get!_alter
-
 @[simp]
 theorem getElem!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
     {f : Option β → Option β} : (alter m k f)[k]! = (f m[k]?).get! :=
   DHashMap.Const.get!_alter_self
 
-@[deprecated getElem!_alter_self (since := "2025-02-09")]
-theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
-    {f : Option β → Option β} : get! (alter m k f) k = (f (get? m k)).get! :=
-  DHashMap.Const.get!_alter_self
-
 @[grind =]
 theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β}
     {f : Option β → Option β} :
@@ -2040,25 +1988,11 @@ theorem getElem?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β 
         m[k']? :=
   DHashMap.Const.get?_modify
 
-@[deprecated getElem?_modify (since := "2025-02-09")]
-theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
-    get? (modify m k f) k' =
-      if k == k' then
-        get? m k |>.map f
-      else
-        get? m k' :=
-  DHashMap.Const.get?_modify
-
 @[simp]
 theorem getElem?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
     (modify m k f)[k]? = m[k]?.map f :=
   DHashMap.Const.get?_modify_self
 
-@[deprecated getElem?_modify_self (since := "2025-02-09")]
-theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
-    get? (modify m k f) k = (get? m k).map f :=
-  DHashMap.Const.get?_modify_self
-
 @[grind =]
 theorem getElem_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
     {h : k' ∈ modify m k f} :
@@ -2071,18 +2005,6 @@ theorem getElem_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β →
         m[k'] :=
   DHashMap.Const.get_modify
 
-@[deprecated getElem_modify (since := "2025-02-09")]
-theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
-    {h : k' ∈ modify m k f} :
-    get (modify m k f) k' h =
-      if heq : k == k' then
-        haveI h' : k ∈ m := mem_congr heq |>.mpr <| mem_modify.mp h
-        f (get m k h')
-      else
-        haveI h' : k' ∈ m := mem_modify.mp h
-        get m k' h' :=
-  DHashMap.Const.get_modify
-
 @[simp]
 theorem getElem_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β}
     {h : k ∈ modify m k f} :
@@ -2090,13 +2012,6 @@ theorem getElem_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β 
     (modify m k f)[k] = f m[k] :=
   DHashMap.Const.get_modify_self
 
-@[deprecated getElem_modify_self (since := "2025-02-09")]
-theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β}
-    {h : k ∈ modify m k f} :
-    haveI h' : k ∈ m := mem_modify.mp h
-    get (modify m k f) k h = f (get m k h') :=
-  DHashMap.Const.get_modify_self
-
 @[grind =]
 theorem getElem!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
     (modify m k f)[k']! =
@@ -2106,25 +2021,11 @@ theorem getElem!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited
         m[k']! :=
   DHashMap.Const.get!_modify
 
-@[deprecated getElem!_modify (since := "2025-02-09")]
-theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
-    get! (modify m k f) k' =
-      if k == k' then
-        get? m k |>.map f |>.get!
-      else
-        get! m k' :=
-  DHashMap.Const.get!_modify
-
 @[simp]
 theorem getElem!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} :
     (modify m k f)[k]! = (m[k]?.map f).get! :=
   DHashMap.Const.get!_modify_self
 
-@[deprecated getElem!_modify_self (since := "2025-02-09")]
-theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} :
-    get! (modify m k f) k = ((get? m k).map f).get! :=
-  DHashMap.Const.get!_modify_self
-
 @[grind =]
 theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} :
     getD (modify m k f) k' fallback =
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 4a4c3d994b..ac17d4d2f0 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -930,11 +930,6 @@ theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.map Prod.fst = m.keys :=
   DHashMap.Raw.Const.map_fst_toList_eq_keys h.out
 
-@[deprecated map_fst_toList_eq_keys (since := "2025-02-28")]
-theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
-    m.toList.map Prod.fst = m.keys :=
-  DHashMap.Raw.Const.map_fst_toList_eq_keys h.out
-
 @[simp, grind =]
 theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.length = m.size :=
@@ -1872,25 +1867,11 @@ theorem getElem?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option
         m[k']? :=
   DHashMap.Raw.Const.get?_alter h.out
 
-@[deprecated getElem?_alter (since := "2025-02-09")]
-theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : m.WF) :
-    get? (alter m k f) k' =
-      if k == k' then
-        f (get? m k)
-      else
-        get? m k' :=
-  DHashMap.Raw.Const.get?_alter h.out
-
 @[simp]
 theorem getElem?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
     (h : m.WF) : (alter m k f)[k]? = f m[k]? :=
   DHashMap.Raw.Const.get?_alter_self h.out
 
-@[deprecated get?_alter_self (since := "2025-02-09")]
-theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
-    (h : m.WF) : get? (alter m k f) k = f (get? m k) :=
-  DHashMap.Raw.Const.get?_alter_self h.out
-
 @[grind =]
 theorem getElem_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
     (h : m.WF) {hc : k' ∈ alter m k f} :
@@ -1903,18 +1884,6 @@ theorem getElem_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option
         m[k']'h' :=
   DHashMap.Raw.Const.get_alter h.out (hc := hc)
 
-@[deprecated getElem_alter (since := "2025-02-09")]
-theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
-    (h : m.WF) {hc : k' ∈ alter m k f} :
-    get (alter m k f) k' hc =
-      if heq : k == k' then
-        haveI h' : (f (get? m k)).isSome := mem_alter_of_beq h heq |>.mp hc
-        f (get? m k) |>.get h'
-      else
-        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
-        get m k' h' :=
-  DHashMap.Raw.Const.get_alter h.out
-
 @[simp]
 theorem getElem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
     (h : m.WF) {hc : k ∈ alter m k f} :
@@ -1922,13 +1891,6 @@ theorem getElem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Optio
     (alter m k f)[k] = (f m[k]?).get h' :=
   DHashMap.Raw.Const.get_alter_self h.out (hc := hc)
 
-@[deprecated getElem_alter_self (since := "2025-02-09")]
-theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
-    (h : m.WF) {hc : k ∈ alter m k f} :
-    haveI h' : (f (get? m k)).isSome := mem_alter_self h |>.mp hc
-    get (alter m k f) k hc = (f (get? m k)).get h' :=
-  DHashMap.Raw.Const.get_alter_self h.out
-
 @[grind =]
 theorem getElem!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
     {f : Option β → Option β} (h : m.WF) : (alter m k f)[k']! =
@@ -1938,25 +1900,11 @@ theorem getElem!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited
         m[k']! :=
   DHashMap.Raw.Const.get!_alter h.out
 
-@[deprecated getElem!_alter (since := "2025-02-09")]
-theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
-    {f : Option β → Option β} (h : m.WF) : get! (alter m k f) k' =
-      if k == k' then
-        f (get? m k) |>.get!
-      else
-        get! m k' :=
-  DHashMap.Raw.Const.get!_alter h.out
-
 @[simp]
 theorem getElem!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
     {f : Option β → Option β} (h : m.WF) : (alter m k f)[k]! = (f m[k]?).get! :=
   DHashMap.Raw.Const.get!_alter_self h.out
 
-@[deprecated getElem!_alter_self (since := "2025-02-09")]
-theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
-    {f : Option β → Option β} (h : m.WF) : get! (alter m k f) k = (f (get? m k)).get! :=
-  DHashMap.Raw.Const.get!_alter_self h.out
-
 @[grind =]
 theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β}
     {f : Option β → Option β} (h : m.WF) : getD (alter m k f) k' fallback =
diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean
index 9762dc1007..33aa6c55dd 100644
--- a/src/Std/Data/TreeMap/Basic.lean
+++ b/src/Std/Data/TreeMap/Basic.lean
@@ -150,10 +150,6 @@ def erase (t : TreeMap α β cmp) (a : α) : TreeMap α β cmp :=
 def get? (t : TreeMap α β cmp) (a : α) : Option β :=
   DTreeMap.Const.get? t.inner a
 
-@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
-def find? (t : TreeMap α β cmp) (a : α) : Option β :=
-  get? t a
-
 @[inline, inherit_doc DTreeMap.Const.get]
 def get (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
   DTreeMap.Const.get t.inner a h
@@ -162,18 +158,10 @@ def get (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
 def get! (t : TreeMap α β cmp) (a : α) [Inhabited β] : β :=
   DTreeMap.Const.get! t.inner a
 
-@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
-def find! (t : TreeMap α β cmp) (a : α) [Inhabited β] : β :=
-  get! t a
-
 @[inline, inherit_doc DTreeMap.Const.getD]
 def getD (t : TreeMap α β cmp) (a : α) (fallback : β) : β :=
   DTreeMap.Const.getD t.inner a fallback
 
-@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
-def findD (t : TreeMap α β cmp) (a : α) (fallback : β) : β :=
-  getD t a fallback
-
 instance : GetElem? (TreeMap α β cmp) α β (fun m a => a ∈ m) where
   getElem m a h := m.get a h
   getElem? m a := m.get? a
@@ -455,18 +443,10 @@ def filter (f : α → β → Bool) (m : TreeMap α β cmp) : TreeMap α β cmp
 def foldlM (f : δ → (a : α) → β → m δ) (init : δ) (t : TreeMap α β cmp) : m δ :=
   t.inner.foldlM f init
 
-@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
-def foldM (f : δ → (a : α) → β → m δ) (init : δ) (t : TreeMap α β cmp) : m δ :=
-  t.foldlM f init
-
 @[inline, inherit_doc DTreeMap.foldl]
 def foldl (f : δ → (a : α) → β → δ) (init : δ) (t : TreeMap α β cmp) : δ :=
   t.inner.foldl f init
 
-@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
-def fold (f : δ → (a : α) → β → δ) (init : δ) (t : TreeMap α β cmp) : δ :=
-  t.foldl f init
-
 @[inline, inherit_doc DTreeMap.foldrM]
 def foldrM (f : (a : α) → β → δ → m δ) (init : δ) (t : TreeMap α β cmp) : m δ :=
   t.inner.foldrM f init
@@ -475,10 +455,6 @@ def foldrM (f : (a : α) → β → δ → m δ) (init : δ) (t : TreeMap α β
 def foldr (f : (a : α) → β → δ → δ) (init : δ) (t : TreeMap α β cmp) : δ :=
   t.inner.foldr f init
 
-@[inline, inherit_doc foldr, deprecated foldr (since := "2025-02-12")]
-def revFold (f : δ → (a : α) → β → δ) (init : δ) (t : TreeMap α β cmp) : δ :=
-  foldr (fun k v acc => f acc k v) init t
-
 @[inline, inherit_doc DTreeMap.partition]
 def partition (f : (a : α) → β → Bool) (t : TreeMap α β cmp) : TreeMap α β cmp × TreeMap α β cmp :=
   let p := t.inner.partition f; (⟨p.1⟩, ⟨p.2⟩)
@@ -529,10 +505,6 @@ def toList (t : TreeMap α β cmp) : List (α × β) :=
 def ofList (l : List (α × β)) (cmp : α → α → Ordering := by exact compare) : TreeMap α β cmp :=
   ⟨DTreeMap.Const.ofList l cmp⟩
 
-@[inline, inherit_doc ofList, deprecated ofList (since := "2025-02-12")]
-def fromList (l : List (α × β)) (cmp : α → α → Ordering) : TreeMap α β cmp :=
-  ofList l cmp
-
 @[inline, inherit_doc DTreeMap.Const.unitOfList]
 def unitOfList (l : List α) (cmp : α → α → Ordering := by exact compare) : TreeMap α Unit cmp :=
   ⟨DTreeMap.Const.unitOfList l cmp⟩
@@ -545,10 +517,6 @@ def toArray (t : TreeMap α β cmp) : Array (α × β) :=
 def ofArray (a : Array (α × β)) (cmp : α → α → Ordering := by exact compare) : TreeMap α β cmp :=
   ⟨DTreeMap.Const.ofArray a cmp⟩
 
-@[inline, inherit_doc ofArray, deprecated ofArray (since := "2025-02-12")]
-def fromArray (a : Array (α × β)) (cmp : α → α → Ordering) : TreeMap α β cmp :=
-  ofArray a cmp
-
 @[inline, inherit_doc DTreeMap.Const.unitOfArray]
 def unitOfArray (a : Array α) (cmp : α → α → Ordering := by exact compare) : TreeMap α Unit cmp :=
   ⟨DTreeMap.Const.unitOfArray a cmp⟩
@@ -565,10 +533,6 @@ def alter (t : TreeMap α β cmp) (a : α) (f : Option β → Option β) : TreeM
 def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
   ⟨DTreeMap.Const.mergeWith mergeFn t₁.inner t₂.inner⟩
 
-@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
-def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
-  mergeWith mergeFn t₁ t₂
-
 @[inline, inherit_doc DTreeMap.Const.insertMany]
 def insertMany {ρ} [ForIn Id ρ (α × β)] (t : TreeMap α β cmp) (l : ρ) : TreeMap α β cmp :=
   ⟨DTreeMap.Const.insertMany t.inner l⟩
diff --git a/src/Std/Data/TreeMap/Raw/Basic.lean b/src/Std/Data/TreeMap/Raw/Basic.lean
index 61586ae0fc..663a5e1cd2 100644
--- a/src/Std/Data/TreeMap/Raw/Basic.lean
+++ b/src/Std/Data/TreeMap/Raw/Basic.lean
@@ -162,10 +162,6 @@ def erase (t : Raw α β cmp) (a : α) : Raw α β cmp :=
 def get? (t : Raw α β cmp) (a : α) : Option β :=
   DTreeMap.Raw.Const.get? t.inner a
 
-@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
-def find? (t : Raw α β cmp) (a : α) : Option β :=
-  get? t a
-
 @[inline, inherit_doc DTreeMap.Raw.Const.get]
 def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
   DTreeMap.Raw.Const.get t.inner a h
@@ -174,18 +170,10 @@ def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
 def get! (t : Raw α β cmp) (a : α) [Inhabited β]  : β :=
   DTreeMap.Raw.Const.get! t.inner a
 
-@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
-def find! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
-  get! t a
-
 @[inline, inherit_doc DTreeMap.Raw.Const.getD]
 def getD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
   DTreeMap.Raw.Const.getD t.inner a fallback
 
-@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
-def findD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
-  getD t a fallback
-
 instance : GetElem? (Raw α β cmp) α β (fun m a => a ∈ m) where
   getElem m a h := m.get a h
   getElem? m a := m.get? a
@@ -445,18 +433,10 @@ def filter (f : α → β → Bool) (t : Raw α β cmp) : Raw α β cmp :=
 def foldlM (f : δ → (a : α) → β → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
   t.inner.foldlM f init
 
-@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
-def foldM (f : δ → (a : α) → β → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
-  t.foldlM f init
-
 @[inline, inherit_doc DTreeMap.Raw.foldl]
 def foldl (f : δ → (a : α) → β → δ) (init : δ) (t : Raw α β cmp) : δ :=
   t.inner.foldl f init
 
-@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
-def fold (f : δ → (a : α) → β → δ) (init : δ) (t : Raw α β cmp) : δ :=
-  t.foldl f init
-
 @[inline, inherit_doc DTreeMap.Raw.foldrM]
 def foldrM (f : (a : α) → β → δ → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
   t.inner.foldrM f init
@@ -465,10 +445,6 @@ def foldrM (f : (a : α) → β → δ → m δ) (init : δ) (t : Raw α β cmp)
 def foldr (f : (a : α) → β → δ → δ) (init : δ) (t : Raw α β cmp) : δ :=
   t.inner.foldr f init
 
-@[inline, inherit_doc foldr, deprecated foldr (since := "2025-02-12")]
-def revFold (f : δ → (a : α) → β → δ) (init : δ) (t : Raw α β cmp) : δ :=
-  foldr (fun k v acc => f acc k v) init t
-
 @[inline, inherit_doc DTreeMap.Raw.partition]
 def partition (f : (a : α) → β → Bool) (t : Raw α β cmp) : Raw α β cmp × Raw α β cmp :=
   let p := t.inner.partition f; (⟨p.1⟩, ⟨p.2⟩)
@@ -519,10 +495,6 @@ def toList (t : Raw α β cmp) : List (α × β) :=
 def ofList (l : List (α × β)) (cmp : α → α → Ordering := by exact compare) : Raw α β cmp :=
   ⟨DTreeMap.Raw.Const.ofList l cmp⟩
 
-@[inline, inherit_doc ofList, deprecated ofList (since := "2025-02-12")]
-def fromList (l : List (α × β)) (cmp : α → α → Ordering) : Raw α β cmp :=
-  ofList l cmp
-
 @[inline, inherit_doc DTreeMap.Const.unitOfList]
 def unitOfList (l : List α) (cmp : α → α → Ordering := by exact compare) : Raw α Unit cmp :=
   ⟨DTreeMap.Raw.Const.unitOfList l cmp⟩
@@ -535,10 +507,6 @@ def toArray (t : Raw α β cmp) : Array (α × β) :=
 def ofArray (a : Array (α × β)) (cmp : α → α → Ordering := by exact compare) : Raw α β cmp :=
   ⟨DTreeMap.Raw.Const.ofArray a cmp⟩
 
-@[inline, inherit_doc ofArray, deprecated ofArray (since := "2025-02-12")]
-def fromArray (a : Array (α × β)) (cmp : α → α → Ordering) : Raw α β cmp :=
-  ofArray a cmp
-
 @[inline, inherit_doc DTreeMap.Const.unitOfArray]
 def unitOfArray (a : Array α) (cmp : α → α → Ordering := by exact compare) : Raw α Unit cmp :=
   ⟨DTreeMap.Raw.Const.unitOfArray a cmp⟩
@@ -555,10 +523,6 @@ def alter (t : Raw α β cmp) (a : α) (f : Option β → Option β) : Raw α β
 def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
   ⟨DTreeMap.Raw.Const.mergeWith mergeFn t₁.inner t₂.inner⟩
 
-@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
-def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
-  mergeWith mergeFn t₁ t₂
-
 @[inline, inherit_doc DTreeMap.Raw.Const.insertMany]
 def insertMany {ρ} [ForIn Id ρ (α × β)] (t : Raw α β cmp) (l : ρ) : Raw α β cmp :=
   ⟨DTreeMap.Raw.Const.insertMany t.inner l⟩
diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean
index 0c06ace711..f9a085c3cc 100644
--- a/src/Std/Data/TreeSet/Basic.lean
+++ b/src/Std/Data/TreeSet/Basic.lean
@@ -385,19 +385,11 @@ ascending order.
 def foldlM {m δ} [Monad m] (f : δ → (a : α) → m δ) (init : δ) (t : TreeSet α cmp) : m δ :=
   t.inner.foldlM (fun c a _ => f c a) init
 
-@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
-def foldM (f : δ → (a : α) → m δ) (init : δ) (t : TreeSet α cmp) : m δ :=
-  t.foldlM f init
-
 /-- Folds the given function over the elements of the tree set in ascending order. -/
 @[inline]
 def foldl (f : δ → (a : α) → δ) (init : δ) (t : TreeSet α cmp) : δ :=
   t.inner.foldl (fun c a _ => f c a) init
 
-@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
-def fold (f : δ → (a : α) → δ) (init : δ) (t : TreeSet α cmp) : δ :=
-  t.foldl f init
-
 /--
 Monadically computes a value by folding the given function over the elements in the tree set in
 descending order.
@@ -411,10 +403,6 @@ def foldrM {m δ} [Monad m] (f : (a : α) → δ → m δ) (init : δ) (t : Tree
 def foldr (f : (a : α) → δ → δ) (init : δ) (t : TreeSet α cmp) : δ :=
   t.inner.foldr (fun a _ acc => f a acc) init
 
-@[inline, inherit_doc foldr, deprecated foldr (since := "2025-02-12")]
-def revFold (f : δ → (a : α) → δ) (init : δ) (t : TreeSet α cmp) : δ :=
-  foldr (fun a acc => f acc a) init t
-
 /-- Partitions a tree set into two tree sets based on a predicate. -/
 @[inline]
 def partition (f : (a : α) → Bool) (t : TreeSet α cmp) : TreeSet α cmp × TreeSet α cmp :=
@@ -458,10 +446,6 @@ def toList (t : TreeSet α cmp) : List α :=
 def ofList (l : List α) (cmp : α → α → Ordering := by exact compare) : TreeSet α cmp :=
   ⟨TreeMap.unitOfList l cmp⟩
 
-@[inline, inherit_doc ofList, deprecated ofList (since := "2025-02-12")]
-def fromList (l : List α) (cmp : α → α → Ordering) : TreeSet α cmp :=
-  ofList l cmp
-
 /-- Transforms the tree set into an array of elements in ascending order. -/
 @[inline]
 def toArray (t : TreeSet α cmp) : Array α :=
@@ -471,10 +455,6 @@ def toArray (t : TreeSet α cmp) : Array α :=
 def ofArray (a : Array α) (cmp : α → α → Ordering := by exact compare) : TreeSet α cmp :=
   ⟨TreeMap.unitOfArray a cmp⟩
 
-@[inline, inherit_doc ofArray, deprecated ofArray (since := "2025-02-12")]
-def fromArray (a : Array α) (cmp : α → α → Ordering) : TreeSet α cmp :=
-  ofArray a cmp
-
 /--
 Returns a set that contains all mappings of `t₁` and `t₂.
 
diff --git a/src/Std/Data/TreeSet/Raw/Basic.lean b/src/Std/Data/TreeSet/Raw/Basic.lean
index 1368de2621..beb71e6605 100644
--- a/src/Std/Data/TreeSet/Raw/Basic.lean
+++ b/src/Std/Data/TreeSet/Raw/Basic.lean
@@ -270,18 +270,10 @@ def filter (f : α → Bool) (t : Raw α cmp) : Raw α cmp :=
 def foldlM (f : δ → (a : α) → m δ) (init : δ) (t : Raw α cmp) : m δ :=
   t.inner.foldlM (fun c a _ => f c a) init
 
-@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
-def foldM (f : δ → (a : α) → m δ) (init : δ) (t : Raw α cmp) : m δ :=
-  t.foldlM f init
-
 @[inline, inherit_doc TreeSet.empty]
 def foldl (f : δ → (a : α) → δ) (init : δ) (t : Raw α cmp) : δ :=
   t.inner.foldl (fun c a _ => f c a) init
 
-@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
-def fold (f : δ → (a : α) → δ) (init : δ) (t : Raw α cmp) : δ :=
-  t.foldl f init
-
 @[inline, inherit_doc TreeSet.empty]
 def foldrM (f : (a : α) → δ → m δ) (init : δ) (t : Raw α cmp) : m δ :=
   t.inner.foldrM (fun a _ acc => f a acc) init
@@ -290,10 +282,6 @@ def foldrM (f : (a : α) → δ → m δ) (init : δ) (t : Raw α cmp) : m δ :=
 def foldr (f : (a : α) → δ → δ) (init : δ) (t : Raw α cmp) : δ :=
   t.inner.foldr (fun a _ acc => f a acc) init
 
-@[inline, inherit_doc foldr, deprecated foldr (since := "2025-02-12")]
-def revFold (f : δ → (a : α) → δ) (init : δ) (t : Raw α cmp) : δ :=
-  foldr (fun a acc => f acc a) init t
-
 @[inline, inherit_doc TreeSet.partition]
 def partition (f : (a : α) → Bool) (t : Raw α cmp) : Raw α cmp × Raw α cmp :=
   let p := t.inner.partition fun a _ => f a; (⟨p.1⟩, ⟨p.2⟩)
@@ -328,10 +316,6 @@ def toList (t : Raw α cmp) : List α :=
 def ofList (l : List α) (cmp : α → α → Ordering := by exact compare) : Raw α cmp :=
   ⟨TreeMap.Raw.unitOfList l cmp⟩
 
-@[inline, inherit_doc ofList, deprecated ofList (since := "2025-02-12")]
-def fromList (l : List α) (cmp : α → α → Ordering) : Raw α cmp :=
-  ofList l cmp
-
 @[inline, inherit_doc TreeSet.empty]
 def toArray (t : Raw α cmp) : Array α :=
   t.foldl (init := #[]) fun acc k => acc.push k
@@ -340,10 +324,6 @@ def toArray (t : Raw α cmp) : Array α :=
 def ofArray (a : Array α) (cmp : α → α → Ordering := by exact compare) : Raw α cmp :=
   ⟨TreeMap.Raw.unitOfArray a cmp⟩
 
-@[inline, inherit_doc ofArray, deprecated ofArray (since := "2025-02-12")]
-def fromArray (a : Array α) (cmp : α → α → Ordering) : Raw α cmp :=
-  ofArray a cmp
-
 @[inline, inherit_doc TreeSet.empty]
 def merge (t₁ t₂ : Raw α cmp) : Raw α cmp :=
   ⟨TreeMap.Raw.mergeWith (fun _ _ _ => ()) t₁.inner t₂.inner⟩
diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean
index 44e4eee2b0..664b36b1f0 100644
--- a/src/lake/Lake/Build/Fetch.lean
+++ b/src/lake/Lake/Build/Fetch.lean
@@ -24,10 +24,6 @@ using the `fetch` function defined in this module.
 
 namespace Lake
 
-/-- The internal core monad of Lake builds. **Not intended for user use.** -/
-@[deprecated "Deprecated without replacement." (since := "2025-02-22")]
-public abbrev CoreBuildM := BuildT LogIO
-
 /-- A type alias for `Option Package` that assists monad type class synthesis. -/
 @[expose] public def CurrPackage := Option Package
 
diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean
index df9fe6815f..4b7805a1a0 100644
--- a/tests/bench/liasolver.lean
+++ b/tests/bench/liasolver.lean
@@ -327,7 +327,7 @@ def error (msg : String) : IO α :=
   throw <| IO.userError s!"Error: {msg}."
 
 def Array.ithVal (xs : Array String) (i : Nat) (name : String) : IO Int := do
-  let some unparsed := xs.get? i
+  let some unparsed := xs[i]?
     | error s!"Missing {name}"
   let some parsed := String.toInt? unparsed
     | error s!"Invalid {name}: `{unparsed}`"
@@ -337,7 +337,7 @@ def main (args : List String) : IO UInt32 := do
   let some path := args.head?
     | error "Usage: liasolver <input file>"
   let lines ← IO.FS.lines path <&> Array.filter (¬·.isEmpty)
-  let some headerLine := lines.get? 0
+  let some headerLine := lines[0]?
     | error "No header line"
   let header := headerLine.splitOn.toArray
   let nEquations ← header.ithVal 0 "amount of equations"
diff --git a/tests/bench/qsort.lean b/tests/bench/qsort.lean
index f8470756b7..2865be86b7 100755
--- a/tests/bench/qsort.lean
+++ b/tests/bench/qsort.lean
@@ -10,7 +10,7 @@ def mkRandomArray : Nat → Elem → Array Elem → Array Elem
 partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
 | i =>
   if i < a.size - 1 then do
-    unless (a.get! i <= a.get! (i+1)) do  throw (IO.userError "array is not sorted");
+    unless (a[i]! <= a[i+1]!) do  throw (IO.userError "array is not sorted");
     checkSortedAux a (i+1)
   else
     pure ()
@@ -23,7 +23,7 @@ macro:max "↑" x:term:max : term => `(UInt32.toNat $x)
 @[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Idx) (pivot : α) : Array α → Idx → Idx → Idx × Array α
 | as, i, j =>
   if j < hi then
-    if lt (as.get! ↑j) pivot then
+    if lt (as[j.toNat]!) pivot then
       let as := as.swapIfInBounds ↑i ↑j;
       partitionAux lt hi pivot as (i+1) (j+1)
     else
@@ -35,10 +35,10 @@ macro:max "↑" x:term:max : term => `(UInt32.toNat $x)
 set_option pp.all true
 @[inline] def partition {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) (lo hi : Idx) : Idx × Array α :=
 let mid : Idx := (lo + hi) / 2;
-let as  := if lt (as.get! ↑mid) (as.get! ↑lo) then as.swapIfInBounds ↑lo ↑mid else as;
-let as  := if lt (as.get! ↑hi)  (as.get! ↑lo) then as.swapIfInBounds ↑lo ↑hi  else as;
-let as  := if lt (as.get! ↑mid) (as.get! ↑hi) then as.swapIfInBounds ↑mid ↑hi else as;
-let pivot := as.get! ↑hi;
+let as  := if lt (as[mid.toNat]!) (as[lo.toNat]!) then as.swapIfInBounds ↑lo ↑mid else as;
+let as  := if lt (as[hi.toNat]!)  (as[lo.toNat]!) then as.swapIfInBounds ↑lo ↑hi  else as;
+let as  := if lt (as[mid.toNat]!) (as[hi.toNat]!) then as.swapIfInBounds ↑mid ↑hi else as;
+let pivot := as[hi.toNat]!;
 partitionAux lt hi pivot as lo lo
 
 @[specialize] partial def qsortAux {α : Type} [Inhabited α] (lt : α → α → Bool) : Array α → Idx → Idx → Array α
diff --git a/tests/compiler/bytearray_bug.lean b/tests/compiler/bytearray_bug.lean
index 69cace5119..c8d1bc191e 100644
--- a/tests/compiler/bytearray_bug.lean
+++ b/tests/compiler/bytearray_bug.lean
@@ -1,5 +1,5 @@
 
 def main (xs : List String) : IO Unit :=
   let arr := (let e := ByteArray.empty; e.push (UInt8.ofNat 10));
-  let v := arr.data.get! 0;
+  let v := arr.data[0]!;
   IO.println v
diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean
index 1cb34bd990..4841955871 100644
--- a/tests/compiler/phashmap.lean
+++ b/tests/compiler/phashmap.lean
@@ -10,7 +10,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
diff --git a/tests/compiler/phashmap3.lean b/tests/compiler/phashmap3.lean
index 8492a8d4d3..3fb3f81bae 100644
--- a/tests/compiler/phashmap3.lean
+++ b/tests/compiler/phashmap3.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
diff --git a/tests/lean/307.lean b/tests/lean/307.lean
index 40433a3932..68ea1d4f13 100644
--- a/tests/lean/307.lean
+++ b/tests/lean/307.lean
@@ -15,10 +15,10 @@ def INT32_MIN : Int := -0x80000000
 
 @[noinline] def oneU8 : UInt8 := 1
 
-#reduce (UInt8.mod oneU8 0).val.val
+#reduce (UInt8.mod oneU8 0).toFin.val
 #eval (UInt8.mod oneU8 0)
 
-#reduce (UInt8.mod oneU8 0).val.val
+#reduce (UInt8.mod oneU8 0).toFin.val
 #eval (UInt8.mod oneU8 0)
 
 @[noinline] def int_div x y := Int.ediv x y
@@ -27,14 +27,14 @@ def INT32_MIN : Int := -0x80000000
 
 @[noinline] def oneU16 : UInt16 := 1
 
-#reduce (UInt16.mod oneU16 0).val.val
+#reduce (UInt16.mod oneU16 0).toFin.val
 #eval (UInt16.mod oneU16 0)
 
 @[noinline] def uint16_mod x y := UInt16.mod x y
 
 @[noinline] def oneU32 : UInt32 := 1
 
-#reduce (UInt32.mod oneU32 0).val.val
+#reduce (UInt32.mod oneU32 0).toFin.val
 #eval (UInt32.mod oneU32 0)
 
 @[noinline] def uint32_mod x y := UInt32.mod x y
@@ -42,7 +42,7 @@ def INT32_MIN : Int := -0x80000000
 
 @[noinline] def oneU64 : UInt64 := 1
 
-#reduce (UInt64.mod oneU64 0).val.val
+#reduce (UInt64.mod oneU64 0).toFin.val
 #eval (UInt64.mod oneU64 0)
 
 @[noinline] def uint64_mod x y := UInt64.mod x y
diff --git a/tests/lean/arrayGetU.lean b/tests/lean/arrayGetU.lean
index ce440ae3ed..354c680e74 100644
--- a/tests/lean/arrayGetU.lean
+++ b/tests/lean/arrayGetU.lean
@@ -1,5 +1,5 @@
 def f (a : Array Nat) (i : Nat) (v : Nat) (h : i < a.size) : Array Nat :=
-  a.set i (a.get i h + v)
+  a.set i (a[i] + v)
 
 set_option pp.proofs true
 
diff --git a/tests/lean/funind_errors.lean b/tests/lean/funind_errors.lean
index 6054ea4058..fb5d575a9e 100644
--- a/tests/lean/funind_errors.lean
+++ b/tests/lean/funind_errors.lean
@@ -8,7 +8,7 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
 where
   foo (i : Nat) (r : Array α) : Array α :=
     if h : i < as.size then
-      let a := as.get i h
+      let a := as[i]
       if p a then
         foo (i+1) (r.push a)
       else
diff --git a/tests/lean/funind_errors.lean.expected.out b/tests/lean/funind_errors.lean.expected.out
index 93ac09e68a..9ff7397ced 100644
--- a/tests/lean/funind_errors.lean.expected.out
+++ b/tests/lean/funind_errors.lean.expected.out
@@ -3,11 +3,11 @@ funind_errors.lean:22:7-22:23: error(lean.unknownIdentifier): Unknown constant `
 takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
   (case1 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
-      have a := as.get i h;
+      have a := as[i];
       p a = true → motive (i + 1) (r.push a) → motive i r)
   (case2 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
-      have a := as.get i h;
+      have a := as[i];
       ¬p a = true → motive i r)
   (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
 funind_errors.lean:38:7-38:20: error(lean.unknownIdentifier): Unknown constant `idEven.induct`
diff --git a/tests/lean/grind/experiments/bitvec.lean b/tests/lean/grind/experiments/bitvec.lean
index ca8f571077..9de44bfc74 100644
--- a/tests/lean/grind/experiments/bitvec.lean
+++ b/tests/lean/grind/experiments/bitvec.lean
@@ -302,25 +302,14 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 
 @[simp] theorem toNat_ofNatLT (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
 
-@[deprecated toNat_ofNatLT (since := "2025-02-13")]
-theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
-
 @[simp] theorem getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
   getLsbD (x#'lt) i = x.testBit i := by
   simp [getLsbD, BitVec.ofNatLT]
 
-@[deprecated getLsbD_ofNatLT (since := "2025-02-13")]
-theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
-  getLsbD (x#'lt) i = x.testBit i := getLsbD_ofNatLT x lt i
-
 @[simp] theorem getMsbD_ofNatLT {n x i : Nat} (h : x < 2^n) :
     getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
   simp [getMsbD, getLsbD]
 
-@[deprecated getMsbD_ofNatLT (since := "2025-02-13")]
-theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
-    getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := getMsbD_ofNatLT h
-
 @[simp, bitvec_to_nat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
   simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat]
 
@@ -5478,15 +5467,4 @@ instance instDecidableExistsBitVec :
   | 0, _, _ => inferInstance
   | _ + 1, _, _ => inferInstance
 
-/-! ### Deprecations -/
-
-set_option linter.missingDocs false
-
-@[deprecated toFin_uShiftRight (since := "2025-02-18")]
-abbrev toFin_uShiftRight := @toFin_ushiftRight
-
-
-
-
-
 end BitVec'
diff --git a/tests/lean/ref1.lean b/tests/lean/ref1.lean
index fce802e583..41614f8b01 100644
--- a/tests/lean/ref1.lean
+++ b/tests/lean/ref1.lean
@@ -10,7 +10,7 @@ n.forM $ fun i _ => do
 
 def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit := do
 let a ← r.swap ∅;
-a.size.forM (fun i _ => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
+a.size.forM (fun i _ => IO.println ("[" ++ toString i ++ "]: " ++ toString a[i]!));
 discard $ r.swap a;
 pure ()
 
diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean
index a537d5b6b7..5b138475df 100644
--- a/tests/lean/repr_issue.lean
+++ b/tests/lean/repr_issue.lean
@@ -3,7 +3,7 @@ def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat
 tryCatch
   (do modify $ fun (a : Array Nat) => a.set! 0 33;
       throw "error")
-  (fun _ => do let a ← get; pure $ a.get! 0)
+  (fun _ => do let a ← get; pure $ a[0]!)
 
 def ex₁ : StateT (Array Nat) (ExceptT String Id) Nat :=
 foo
diff --git a/tests/lean/run/1921.lean b/tests/lean/run/1921.lean
index 39cb992987..9df40ae8e5 100644
--- a/tests/lean/run/1921.lean
+++ b/tests/lean/run/1921.lean
@@ -1,5 +1,5 @@
 @[simp] theorem Array.size_singleton : #[a].size = 1 := rfl
-@[simp] theorem USize.not_size_le_one : ¬ USize.size ≤ 1 := by cases usize_size_eq <;> simp (config := { decide := true }) [*]
+@[simp] theorem USize.not_size_le_one : ¬ USize.size ≤ 1 := by cases USize.size_eq <;> simp (config := { decide := true }) [*]
 
 def f := #[true].any id 0 USize.size
 
diff --git a/tests/lean/run/305.lean b/tests/lean/run/305.lean
index 4ea31620d2..ee5b60cb48 100644
--- a/tests/lean/run/305.lean
+++ b/tests/lean/run/305.lean
@@ -21,7 +21,7 @@ namespace Cmd
 
   def subCmdByFullName? (c : Cmd) (fullName : Array String) : Option Cmd := do
     let mut c := c
-    guard <| c.name = fullName.get? 0
+    guard <| some c.name = fullName[0]?
     for subName in fullName[1...*] do
       c ← c.subCmd? subName
     return c
diff --git a/tests/lean/run/appFinalizeIssue.lean b/tests/lean/run/appFinalizeIssue.lean
index f1b13b5799..a21e7f71a9 100644
--- a/tests/lean/run/appFinalizeIssue.lean
+++ b/tests/lean/run/appFinalizeIssue.lean
@@ -9,7 +9,7 @@ instance : GetElem Lean.Syntax Nat Lean.Syntax where
   getElem' xs i := xs.getArg i
 
 instance : GetElem (Array α) Nat α where
-  getElem' xs i := xs.get i sorry
+  getElem' xs i := xs[i]'sorry
 
 open Lean
 
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
index c85294eb29..e989a53bc5 100644
--- a/tests/lean/run/array1.lean
+++ b/tests/lean/run/array1.lean
@@ -10,7 +10,7 @@ def w : Array Nat :=
 #check @Array.casesOn
 
 def f : Fin w.size → Nat :=
-  fun i => w.get i i.isLt
+  fun i => w[i]'(i.isLt)
 
 def arraySum (a : Array Nat) : Nat :=
 a.foldl Nat.add 0
diff --git a/tests/lean/run/coeOutParamIssue.lean b/tests/lean/run/coeOutParamIssue.lean
index 004468fdf2..7d413f0b59 100644
--- a/tests/lean/run/coeOutParamIssue.lean
+++ b/tests/lean/run/coeOutParamIssue.lean
@@ -6,7 +6,7 @@ class Get (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
 export Get (get)
 
 instance [Inhabited α] : Get (Array α) Nat α where
-  get xs i := xs.get! i
+  get xs i := xs[i]!
 
 instance : Coe Bool Nat where
   coe b := if b then 1 else 0
diff --git a/tests/lean/run/coeOutParamIssue2.lean b/tests/lean/run/coeOutParamIssue2.lean
index 5dd79c3b11..a95e179d1f 100644
--- a/tests/lean/run/coeOutParamIssue2.lean
+++ b/tests/lean/run/coeOutParamIssue2.lean
@@ -5,7 +5,7 @@ class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
 export GetElem (getElem)
 
 instance : GetElem (Array α) Nat α where
-  getElem xs i := xs.get i sorry
+  getElem xs i := xs[i]'sorry
 
 opaque f : Option Bool → Bool
 opaque g : Bool → Bool
diff --git a/tests/lean/run/discrTreeKey.lean b/tests/lean/run/discrTreeKey.lean
index 749260f041..a28d7a6bc2 100644
--- a/tests/lean/run/discrTreeKey.lean
+++ b/tests/lean/run/discrTreeKey.lean
@@ -44,8 +44,8 @@ open Nat List
 #check Nat.pred_succ
 #discr_tree_simp_key Nat.pred_succ
 
-#check get?_nil
-#discr_tree_simp_key get?_nil
+#check getElem?_nil
+#discr_tree_simp_key getElem?_nil
 
 #check or_cons
 #discr_tree_simp_key or_cons
diff --git a/tests/lean/run/dotNotationAndDefaultInstance.lean b/tests/lean/run/dotNotationAndDefaultInstance.lean
index 3fb21b0323..4a335f0699 100644
--- a/tests/lean/run/dotNotationAndDefaultInstance.lean
+++ b/tests/lean/run/dotNotationAndDefaultInstance.lean
@@ -6,7 +6,7 @@ class Get (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
 export Get (get)
 
 instance [Inhabited α] : Get (Array α) Nat α where
-  get xs i := xs.get! i
+  get xs i := xs[i]!
 
 example (as : Array (Nat × Bool)) : Bool :=
   (get as 0).2
diff --git a/tests/lean/run/forOutParamIssue.lean b/tests/lean/run/forOutParamIssue.lean
index 5e3909347c..2228105062 100644
--- a/tests/lean/run/forOutParamIssue.lean
+++ b/tests/lean/run/forOutParamIssue.lean
@@ -5,7 +5,7 @@ class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
 export GetElem (getElem)
 
 instance : GetElem (Array α) Nat α where
-  getElem xs i := xs.get i sorry
+  getElem xs i := xs[i]'sorry
 
 opaque f : Option Bool → Id Unit
 
diff --git a/tests/lean/run/grind_bitvec2.lean b/tests/lean/run/grind_bitvec2.lean
index 070560529a..a88b69ce6f 100644
--- a/tests/lean/run/grind_bitvec2.lean
+++ b/tests/lean/run/grind_bitvec2.lean
@@ -41,10 +41,6 @@ theorem some_eq_getElem?_iff {l : BitVec w} :
 theorem getElem_of_getElem? {l : BitVec w} :
     l[n]? = some a → ∃ h : n < w, l[n] = a := by grind
 
-set_option linter.missingDocs false in
-@[deprecated getElem?_eq_some_iff (since := "2025-02-17")]
-abbrev getElem?_eq_some := @_root_.getElem?_eq_some_iff
-
 theorem getElem?_eq_none_iff {l : BitVec w} : l[n]? = none ↔ w ≤ n := by grind
 
 theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by grind
@@ -248,24 +244,13 @@ theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  b
 theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
   decide
 
-@[deprecated toNat_ofNatLT (since := "2025-02-13")]
-theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
-
 theorem getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
     getLsbD (x#'lt) i = x.testBit i := by
   simp [getLsbD, BitVec.ofNatLT]
 
-@[deprecated getLsbD_ofNatLT (since := "2025-02-13")]
-theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
-  getLsbD (x#'lt) i = x.testBit i := getLsbD_ofNatLT x lt i
-
 theorem getMsbD_ofNatLT {n x i : Nat} (h : x < 2^n) :
     getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by grind
 
-@[deprecated getMsbD_ofNatLT (since := "2025-02-13")]
-theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
-    getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := getMsbD_ofNatLT h
-
 theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n :=
   eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn])
 
diff --git a/tests/lean/run/heapSort.lean b/tests/lean/run/heapSort.lean
index d7ed55aaa3..5b65410eef 100644
--- a/tests/lean/run/heapSort.lean
+++ b/tests/lean/run/heapSort.lean
@@ -84,7 +84,7 @@ def singleton (lt) (x : α) : BinaryHeap α lt := ⟨#[x]⟩
 def size {lt} (self : BinaryHeap α lt) : Nat := self.1.size
 
 /-- `O(1)`. Get an element in the heap by index. -/
-def get {lt} (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1.get i i.2
+def get {lt} (self : BinaryHeap α lt) (i : Fin self.size) : α := self.1[i]'i.2
 
 /-- `O(log n)`. Insert an element into a `BinaryHeap`, preserving the max-heap property. -/
 def insert {lt} (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where
@@ -96,7 +96,7 @@ def insert {lt} (self : BinaryHeap α lt) (x : α) : BinaryHeap α lt where
   simp [insert, size, size_heapifyUp]
 
 /-- `O(1)`. Get the maximum element in a `BinaryHeap`. -/
-def max {lt} (self : BinaryHeap α lt) : Option α := self.1.get? 0
+def max {lt} (self : BinaryHeap α lt) : Option α := self.1[0]?
 
 /-- Auxiliary for `popMax`. -/
 def popMaxAux {lt} (self : BinaryHeap α lt) : {a' : BinaryHeap α lt // a'.size = self.size - 1} :=
@@ -124,7 +124,7 @@ def extractMax {lt} (self : BinaryHeap α lt) : Option α × BinaryHeap α lt :=
   (self.max, self.popMax)
 
 theorem size_pos_of_max {lt} {self : BinaryHeap α lt} (e : self.max = some x) : 0 < self.size :=
-  Decidable.of_not_not fun h: ¬ 0 < self.1.size => by simp [BinaryHeap.max, Array.get?, h] at e
+  Decidable.of_not_not fun h: ¬ 0 < self.1.size => by simp [BinaryHeap.max, h] at e
 
 /-- `O(log n)`. Equivalent to `extractMax (self.insert x)`, except that extraction cannot fail. -/
 def insertExtractMax {lt} (self : BinaryHeap α lt) (x : α) : α × BinaryHeap α lt :=
diff --git a/tests/lean/run/kernelInterrupt.lean b/tests/lean/run/kernelInterrupt.lean
index 2cca0d3b96..59d961a689 100644
--- a/tests/lean/run/kernelInterrupt.lean
+++ b/tests/lean/run/kernelInterrupt.lean
@@ -13,7 +13,7 @@ open Lean
   let envPromise ← IO.Promise.new
   let tk ← IO.CancelToken.new
   let t := Task.spawn fun _ =>
-    let env := envPromise.result.get
+    let env := envPromise.result!.get
     let decl := .axiomDecl {
       name := `test
       levelParams := []
diff --git a/tests/lean/run/maze.lean b/tests/lean/run/maze.lean
index 03fe51ab6d..5f07dcdd09 100644
--- a/tests/lean/run/maze.lean
+++ b/tests/lean/run/maze.lean
@@ -126,7 +126,7 @@ partial def extractGameState : Lean.Expr → Lean.MetaM GameState
 
 def update2dArray {α : Type} : Array (Array α) → Coords → α → Array (Array α)
 | a, ⟨x,y⟩, v =>
-   Array.set! a y $ Array.set! (Array.get! a y) x v
+   Array.set! a y $ Array.set! a[y]! x v
 
 def update2dArrayMulti {α : Type} : Array (Array α) → List Coords → α → Array (Array α)
 | a, [], _ => a
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index a08fca4b01..59c964f786 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -863,7 +863,7 @@ check t;
 (match t.arrayLit? with
 | some (_, xs) => do
   checkM $ pure $ xs.length == 2;
-  (match (xs.get! 0).rawNatLit?, (xs.get! 1).rawNatLit? with
+  (match xs[0]!.rawNatLit?, xs[1]!.rawNatLit? with
   | some 1, some 2 => pure ()
   | _, _           => throwError "nat lits expected")
 | none => throwError "array lit expected")
diff --git a/tests/lean/run/simproc_timeout.lean b/tests/lean/run/simproc_timeout.lean
index 25277dd997..beb8d456b8 100644
--- a/tests/lean/run/simproc_timeout.lean
+++ b/tests/lean/run/simproc_timeout.lean
@@ -280,7 +280,7 @@ variable {α : Type _}
 
 variable [Primcodable α]
 
-theorem list_get? : Primrec₂ (@List.get? α) := sorry
+theorem list_get? : Primrec₂ (@List.get?Internal α) := sorry
 
 end Primrec
 
@@ -329,8 +329,8 @@ instance instDenumerable : Denumerable Code :=
 open Primrec
 
 private def lup (L : List (List (Option Nat))) (p : Nat × Code) (n : Nat) := do
-  let l ← L.get? (encode p)
-  let o ← l.get? n
+  let l ← L.get?Internal (encode p)
+  let o ← l.get?Internal n
   o
 
 -- This used to work in under 20000, but need over 6 million after leanprover/lean4#3124
diff --git a/tests/lean/run/splitIssue2.lean b/tests/lean/run/splitIssue2.lean
index b35c1c122b..3fe837be6f 100644
--- a/tests/lean/run/splitIssue2.lean
+++ b/tests/lean/run/splitIssue2.lean
@@ -9,7 +9,7 @@ namespace UnionFind
 
 /-- Parent of a union-find node, defaults to self when the node is a root -/
 def parentD (arr : Array UFNode) (i : Nat) : Nat :=
-  if h : i < arr.size then (arr.get i h).parent else i
+  if h : i < arr.size then arr[i].parent else i
 
 /-- Rank of a union-find node, defaults to 0 when the node is a root -/
 def rankD (arr : Array UFNode) (i : Nat) : Nat := 0
@@ -47,11 +47,11 @@ noncomputable def rankMax (self : UnionFind) := 0
 
 /-- Root of a union-find node. -/
 def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
-  let y := (self.arr.get x.1 x.2).parent
+  let y := self.arr[x.1].parent
   if h : y = x then
     x
   else
-    have : self.rankMax - self.rank (self.arr.get x.1 x.2).parent < self.rankMax - self.rank x :=
+    have : self.rankMax - self.rank self.arr[x.1].parent < self.rankMax - self.rank x :=
       sorry
     self.root ⟨y, sorry⟩
 termination_by self.rankMax - self.rank x
diff --git a/tests/lean/run/utf8英語.lean b/tests/lean/run/utf8英語.lean
index b55f0dfc11..6c128fc813 100644
--- a/tests/lean/run/utf8英語.lean
+++ b/tests/lean/run/utf8英語.lean
@@ -13,7 +13,7 @@ macro "test_extern'" t:term " => " v:term : command =>
 def checkGet (s : String) (arr : Array UInt8) :=
   (List.range s.utf8ByteSize).all fun i =>
     let c := if h : _ then s.getUtf8Byte i h else unreachable!
-    c == arr.get! i
+    c == arr[i]!
 
 macro "validate" arr:term " => " "↯" : command =>
   `(test_extern' String.validateUTF8 $arr => false)
diff --git a/tests/lean/sint_basic.lean b/tests/lean/sint_basic.lean
index dd7e36f9db..f6c5cfc0ea 100644
--- a/tests/lean/sint_basic.lean
+++ b/tests/lean/sint_basic.lean
@@ -10,8 +10,8 @@
 #eval Int8.ofNat 120 = 120
 #eval Int8.ofInt (-20) = -20
 #eval (Int8.ofInt (-2)).toInt = -2
-#eval (Int8.ofInt (-2)).toNat = 0
-#eval (Int8.ofInt (10)).toNat = 10
+#eval (Int8.ofInt (-2)).toNatClampNeg = 0
+#eval (Int8.ofInt (10)).toNatClampNeg = 10
 #eval (Int8.ofInt (10)).toInt = 10
 #eval Int8.ofNat (2^64) == 0
 #eval Int8.ofInt (-2^64) == 0
@@ -116,8 +116,8 @@ def myId8 (x : Int8) : Int8 := x
 #eval Int16.ofNat 120 = 120
 #eval Int16.ofInt (-20) = -20
 #eval (Int16.ofInt (-2)).toInt = -2
-#eval (Int16.ofInt (-2)).toNat = 0
-#eval (Int16.ofInt (10)).toNat = 10
+#eval (Int16.ofInt (-2)).toNatClampNeg = 0
+#eval (Int16.ofInt (10)).toNatClampNeg = 10
 #eval (Int16.ofInt (10)).toInt = 10
 #eval Int16.ofNat (2^64) == 0
 #eval Int16.ofInt (-2^64) == 0
@@ -198,8 +198,8 @@ def myId16 (x : Int16) : Int16 := x
 #eval Int32.ofNat 120 = 120
 #eval Int32.ofInt (-20) = -20
 #eval (Int32.ofInt (-2)).toInt = -2
-#eval (Int32.ofInt (-2)).toNat = 0
-#eval (Int32.ofInt (10)).toNat = 10
+#eval (Int32.ofInt (-2)).toNatClampNeg = 0
+#eval (Int32.ofInt (10)).toNatClampNeg = 10
 #eval (Int32.ofInt (10)).toInt = 10
 #eval Int32.ofNat (2^64) == 0
 #eval Int32.ofInt (-2^64) == 0
@@ -279,8 +279,8 @@ def myId32 (x : Int32) : Int32 := x
 #eval Int64.ofNat 120 = 120
 #eval Int64.ofInt (-20) = -20
 #eval (Int64.ofInt (-2)).toInt = -2
-#eval (Int64.ofInt (-2)).toNat = 0
-#eval (Int64.ofInt (10)).toNat = 10
+#eval (Int64.ofInt (-2)).toNatClampNeg = 0
+#eval (Int64.ofInt (10)).toNatClampNeg = 10
 #eval (Int64.ofInt (10)).toInt = 10
 #eval Int64.ofNat (2^64) == 0
 #eval Int64.ofInt (-2^64) == 0
@@ -361,8 +361,8 @@ def myId64 (x : Int64) : Int64 := x
 #eval ISize.ofNat 120 = 120
 #eval ISize.ofInt (-20) = -20
 #eval (ISize.ofInt (-2)).toInt = -2
-#eval (ISize.ofInt (-2)).toNat = 0
-#eval (ISize.ofInt (10)).toNat = 10
+#eval (ISize.ofInt (-2)).toNatClampNeg = 0
+#eval (ISize.ofInt (10)).toNatClampNeg = 10
 #eval (ISize.ofInt (10)).toInt = 10
 #eval ISize.ofNat (2^64) == 0
 #eval ISize.ofInt (-2^64) == 0
diff --git a/tests/lean/uintCtors.lean b/tests/lean/uintCtors.lean
index 64104bfebf..9cc3eb6b55 100644
--- a/tests/lean/uintCtors.lean
+++ b/tests/lean/uintCtors.lean
@@ -11,24 +11,24 @@ def UInt64.ofNatCore' (n : Nat) (h : n < UInt64.size) : UInt64 := {
 #eval UInt64.ofNatCore' 3 (by decide)
 
 #eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt8 }
-#eval (3 : UInt8).val
+#eval (3 : UInt8).toFin
 #eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt16 }
-#eval (3 : UInt16).val
+#eval (3 : UInt16).toFin
 #eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt32 }
-#eval (3 : UInt32).val
+#eval (3 : UInt32).toFin
 #eval toString $ { toBitVec := ⟨{ val := 3, isLt := (by decide) }⟩ : UInt64 }
-#eval (3 : UInt64).val
+#eval (3 : UInt64).toFin
 #eval toString $ { toBitVec := ⟨{ val := 3, isLt := (match System.Platform.numBits, System.Platform.numBits_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) }⟩ : USize }
-#eval (3 : USize).val
+#eval (3 : USize).toFin
 
 
 #eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt8 }
-#eval (4 : UInt8).val
+#eval (4 : UInt8).toFin
 #eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt16 }
-#eval (4 : UInt16).val
+#eval (4 : UInt16).toFin
 #eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt32 }
-#eval (4 : UInt32).val
+#eval (4 : UInt32).toFin
 #eval toString $ { toBitVec := ⟨{ val := 4, isLt := (by decide) }⟩ : UInt64 }
-#eval (4 : UInt64).val
+#eval (4 : UInt64).toFin
 #eval toString $ { toBitVec := ⟨{ val := 4, isLt := (match System.Platform.numBits, System.Platform.numBits_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) }⟩ : USize }
-#eval (4 : USize).val
+#eval (4 : USize).toFin