oops

This PR adds a simple implementation of MePo, from "Lightweight
relevance filtering for machine-generated resolution problems" by Meng
and Paulson.

This needs tuning, but is already useful as a baseline or test case.

---------

Co-authored-by: Thomas Zhu <thomas.zhu.sh@hotmail.com>

src/Init/Data/Array/Attach.lean

@@ -95,16 +95,16 @@ well-founded recursion mechanism to prove that the function terminates.
   intro a m h₁ h₂
   congr
 
-@[simp, grind =] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
+@[simp] theorem pmap_empty {P : α → Prop} (f : ∀ a, P a → β) : pmap f #[] (by simp) = #[] := rfl
 
-@[simp, grind =] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
+@[simp] theorem pmap_push {P : α → Prop} (f : ∀ a, P a → β) (a : α) (xs : Array α) (h : ∀ b ∈ xs.push a, P b) :
     pmap f (xs.push a) h =
       (pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
   simp [pmap]
 
-@[simp, grind =] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
+@[simp] theorem attach_empty : (#[] : Array α).attach = #[] := rfl
 
-@[simp, grind =] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
+@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #[], P x) : (#[] : Array α).attachWith P H = #[] := rfl
 
 @[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
     l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
@@ -125,13 +125,11 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   simp only [List.pmap_toArray, mk.injEq]
   rw [List.pmap_congr_left _ h]
 
-@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {xs : Array α} (H) :
     map g (pmap f xs H) = pmap (fun a h => g (f a h)) xs H := by
   cases xs
   simp [List.map_pmap]
 
-@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs : Array α} (H) :
     pmap g (map f xs) H = pmap (fun a h => g (f a) h) xs fun _ h => H _ (mem_map_of_mem h) := by
   cases xs
@@ -147,14 +145,14 @@ theorem attachWith_congr {xs ys : Array α} (w : xs = ys) {P : α → Prop} {H :
   subst w
   simp
 
-@[simp, grind =] theorem attach_push {a : α} {xs : Array α} :
+@[simp] theorem attach_push {a : α} {xs : Array α} :
     (xs.push a).attach =
       (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   cases xs
   rw [attach_congr (List.push_toArray _ _)]
   simp [Function.comp_def]
 
-@[simp, grind =] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp] theorem attachWith_push {a : α} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
       (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   cases xs
@@ -176,9 +174,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 +182,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
@@ -294,25 +286,23 @@ theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp, grind =] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp] theorem pmap_attach {xs : Array α} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f xs.attach H =
       xs.pmap (P := fun a => ∃ h : a ∈ xs, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   ext <;> simp
 
-@[simp, grind =] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp] theorem pmap_attachWith {xs : Array α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (xs.attachWith q H₁) H₂ =
       xs.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
   ext <;> simp
 
-@[grind =]
 theorem foldl_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) :
     (xs.pmap f H).foldl g x = xs.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
-@[grind =]
 theorem foldr_pmap {xs : Array α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : β → γ → γ) (x : γ) :
     (xs.pmap f H).foldr g x = xs.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
@@ -370,20 +360,18 @@ theorem foldr_attach {xs : Array α} {f : α → β → β} {b : β} :
   ext
   simpa using fun a => List.mem_of_getElem? a
 
-@[grind =]
 theorem attach_map {xs : Array α} {f : α → β} :
     (xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   cases xs
   ext <;> simp
 
-@[grind =]
 theorem attachWith_map {xs : Array α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ xs.map f → P b) :
     (xs.map f).attachWith P H = (xs.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases xs
   simp [List.attachWith_map]
 
-@[simp, grind =] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp] theorem map_attachWith {xs : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
     {f : { x // P x } → β} :
     (xs.attachWith P H).map f = xs.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   cases xs <;> simp_all
@@ -401,9 +389,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
@@ -439,7 +424,6 @@ theorem filter_attachWith {q : α → Prop} {xs : Array α} {p : {x // q x} →
   cases xs
   simp [Function.comp_def, List.filter_map]
 
-@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {xs} (H₁ H₂) :
     pmap f (pmap g xs H₁) H₂ =
       pmap (α := { x // x ∈ xs }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) xs.attach
@@ -447,7 +431,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   cases xs
   simp [List.pmap_pmap, List.pmap_map]
 
-@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
+@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs ys : Array ι}
     (h : ∀ a ∈ xs ++ ys, p a) :
     (xs ++ ys).pmap f h =
       (xs.pmap f fun a ha => h a (mem_append_left ys ha)) ++
@@ -462,7 +446,7 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp, grind =] theorem attach_append {xs ys : Array α} :
+@[simp] theorem attach_append {xs ys : Array α} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   cases xs
@@ -470,62 +454,59 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs ys : Arr
   rw [attach_congr (List.append_toArray _ _)]
   simp [List.attach_append, Function.comp_def]
 
-@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
+@[simp] theorem attachWith_append {P : α → Prop} {xs ys : Array α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp [attachWith]
 
-@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
-@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
   cases xs
   simp
 
-@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
   cases xs
   simp
 
-@[simp, grind =] theorem attach_reverse {xs : Array α} :
+@[simp] theorem attach_reverse {xs : Array α} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   rw [attach_congr List.reverse_toArray]
   simp
 
-@[grind =]
 theorem reverse_attach {xs : Array α} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   simp
 
-@[simp, grind =] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
+@[simp] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
   cases xs
   simp
 
-@[simp, grind =] theorem back?_attachWith {P : α → Prop} {xs : Array α}
+@[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
-@[simp, grind =]
+@[simp]
 theorem back?_attach {xs : Array α} :
     xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs

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.
 

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 α} :

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} :

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
@@ -371,6 +361,7 @@ abbrev getElem?_mkArray := @getElem?_replicate
 
 /-! ### mem -/
 
+@[grind ←]
 theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
 
 @[simp, grind =] theorem mem_push {xs : Array α} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by
@@ -542,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]
 
@@ -2996,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
@@ -3586,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⟩
@@ -4712,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

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

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

src/Init/Data/ByteArray/Basic.lean

@@ -34,12 +34,6 @@ instance : Inhabited ByteArray where
 instance : EmptyCollection ByteArray where
   emptyCollection := ByteArray.empty
 
-@[simp, grind =]
-theorem empty_eq_emptyc : @empty = ∅ := rfl
-
-@[simp, grind =]
-theorem emptyWithCapacity_eq_emptyc : @emptyWithCapacity n = ∅ := rfl
-
 @[extern "lean_sarray_size", simp]
 def usize (a : @& ByteArray) : USize :=
   a.size.toUSize

src/Init/Data/ByteArray/Lemmas.lean

@@ -11,10 +11,15 @@ public import Init.Data.Array.Extract
 
 public section
 
-theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
+-- At present the preferred normal form for empty byte arrays is `ByteArray.empty`
+@[simp]
+theorem emptyc_eq_empty : (∅ : ByteArray) = ByteArray.empty := rfl
 
 @[simp]
-theorem ByteArray.data_emptyc : (∅ : ByteArray).data = #[] := rfl
+theorem emptyWithCapacity_eq_empty : ByteArray.emptyWithCapacity 0 = ByteArray.empty := rfl
+
+@[simp]
+theorem ByteArray.data_empty : ByteArray.empty.data = #[] := rfl
 
 @[simp]
 theorem ByteArray.data_extract {a : ByteArray} {b e : Nat} :
@@ -30,7 +35,7 @@ theorem ByteArray.extract_zero_size {b : ByteArray} : b.extract 0 b.size = b :=
   simp
 
 @[simp]
-theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ∅ := by
+theorem ByteArray.extract_same {b : ByteArray} {i : Nat} : b.extract i i = ByteArray.empty := by
   ext1
   simp [Nat.min_le_left]
 
@@ -52,11 +57,8 @@ theorem ByteArray.data_append {l l' : ByteArray} :
     (l ++ l').data = l.data ++ l'.data := by
   simp [← Array.toList_inj]
 
-theorem ByteArray.size_empty : ByteArray.empty.size = 0 := by
-  simp [← ByteArray.size_data]
-
 @[simp]
-theorem ByteArray.size_emptyc : (∅ : ByteArray).size = 0 := by
+theorem ByteArray.size_empty : ByteArray.empty.size = 0 := by
   simp [← ByteArray.size_data]
 
 @[simp]
@@ -64,7 +66,7 @@ theorem List.data_toByteArray {l : List UInt8} :
     l.toByteArray.data = l.toArray := by
   rw [List.toByteArray]
   suffices ∀ a b, (List.toByteArray.loop a b).data = b.data ++ a.toArray by
-    simpa using this l ∅
+    simpa using this l ByteArray.empty
   intro a b
   fun_induction List.toByteArray.loop a b with simp_all
 
@@ -74,15 +76,15 @@ theorem List.size_toByteArray {l : List UInt8} :
   simp [← ByteArray.size_data]
 
 @[simp]
-theorem List.toByteArray_nil : List.toByteArray [] = ∅ := rfl
+theorem List.toByteArray_nil : List.toByteArray [] = ByteArray.empty := rfl
 
 @[simp]
-theorem ByteArray.empty_append {b : ByteArray} : ∅ ++ b = b := by
+theorem ByteArray.empty_append {b : ByteArray} : ByteArray.empty ++ b = b := by
   ext1
   simp
 
 @[simp]
-theorem ByteArray.append_empty {b : ByteArray} : b ++ ∅ = b := by
+theorem ByteArray.append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
   ext1
   simp
 
@@ -91,7 +93,7 @@ theorem ByteArray.size_append {a b : ByteArray} : (a ++ b).size = a.size + b.siz
   simp [← size_data]
 
 @[simp]
-theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ∅ := by
+theorem ByteArray.size_eq_zero_iff {a : ByteArray} : a.size = 0 ↔ a = ByteArray.empty := by
   refine ⟨fun h => ?_, fun h => h ▸ ByteArray.size_empty⟩
   ext1
   simp [← Array.size_eq_zero_iff, h]
@@ -126,23 +128,23 @@ theorem ByteArray.size_extract {a : ByteArray} {b e : Nat} :
   simp [← size_data]
 
 @[simp]
-theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ∅ ↔ min j b.size ≤ i := by
+theorem ByteArray.extract_eq_empty_iff {b : ByteArray} {i j : Nat} : b.extract i j = ByteArray.empty ↔ min j b.size ≤ i := by
   rw [← size_eq_zero_iff, size_extract]
   omega
 
 @[simp]
-theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ∅ := by
+theorem ByteArray.extract_add_left {b : ByteArray} {i j : Nat} : b.extract (i + j) i = ByteArray.empty := by
   simp only [extract_eq_empty_iff]
   exact Nat.le_trans (Nat.min_le_left _ _) (by simp)
 
 @[simp]
 theorem ByteArray.append_eq_empty_iff {a b : ByteArray} :
-    a ++ b = ∅ ↔ a = ∅ ∧ b = ∅ := by
+    a ++ b = ByteArray.empty ↔ a = ByteArray.empty ∧ b = ByteArray.empty := by
   simp [← size_eq_zero_iff, size_append]
 
 @[simp]
 theorem List.toByteArray_eq_empty {l : List UInt8} :
-    l.toByteArray = ∅ ↔ l = [] := by
+    l.toByteArray = ByteArray.empty ↔ l = [] := by
   simp [← ByteArray.size_eq_zero_iff]
 
 theorem ByteArray.append_right_inj {ys₁ ys₂ : ByteArray} (xs : ByteArray) :
@@ -247,10 +249,8 @@ theorem ByteArray.append_assoc {a b c : ByteArray} : a ++ b ++ c = a ++ (b ++ c)
   simp
 
 @[simp]
-theorem ByteArray.toList_empty : (∅ : ByteArray).toList = [] := by
-  simp [ByteArray.toList]
-  rw [toList.loop]
-  simp
+theorem ByteArray.toList_empty : ByteArray.empty.toList = [] := by
+  simp [ByteArray.toList, ByteArray.toList.loop]
 
 theorem ByteArray.copySlice_eq_append {src : ByteArray} {srcOff : Nat} {dest : ByteArray} {destOff len : Nat} {exact : Bool} :
     ByteArray.copySlice src srcOff dest destOff len exact =

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

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]
 

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

src/Init/Data/List/Attach.lean

@@ -95,14 +95,12 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   | cons x l ih =>
     rw [pmap, pmap, h _ mem_cons_self, ih fun a ha => h a (mem_cons_of_mem _ ha)]
 
-@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {l : List α} (H) :
     map g (pmap f l H) = pmap (fun a h => g (f a h)) l H := by
   induction l
   · rfl
   · simp only [*, pmap, map]
 
-@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {l : List α} (H) :
     pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem h) := by
   induction l
@@ -149,9 +147,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 +155,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 +246,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 +262,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)) :=
@@ -307,13 +283,13 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp, grind =] theorem pmap_attach {l : List α} {p : {x // x ∈ l} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp] theorem pmap_attach {l : List α} {p : {x // x ∈ l} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f l.attach H =
       l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   apply ext_getElem <;> simp
 
-@[simp, grind =] theorem pmap_attachWith {l : List α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp] theorem pmap_attachWith {l : List α} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (l.attachWith q H₁) H₂ =
       l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
@@ -371,26 +347,24 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by
   cases xs <;> simp
 
-@[grind =]
 theorem foldl_pmap {l : List α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
     (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
-@[grind =]
 theorem foldr_pmap {l : List α} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
     (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
   rw [pmap_eq_map_attach, foldr_map]
 
-@[simp, grind =] theorem foldl_attachWith
+@[simp] theorem foldl_attachWith
     {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x } → β} {b} :
     (l.attachWith q H).foldl f b = l.attach.foldl (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b := by
   induction l generalizing b with
   | nil => simp
   | cons a l ih => simp [ih, foldl_map]
 
-@[simp, grind =] theorem foldr_attachWith
+@[simp] theorem foldr_attachWith
     {l : List α} {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x } → β → β} {b} :
     (l.attachWith q H).foldr f b = l.attach.foldr (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b := by
   induction l generalizing b with
@@ -429,18 +403,16 @@ theorem foldr_attach {l : List α} {f : α → β → β} {b : β} :
   | nil => simp
   | cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]
 
-@[grind =]
 theorem attach_map {l : List α} {f : α → β} :
     (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   induction l <;> simp [*]
 
-@[grind =]
 theorem attachWith_map {l : List α} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ l.map f → P b) :
     (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   induction l <;> simp [*]
 
-@[simp, grind =] theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
+@[simp] theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
     {f : { x // P x } → β} :
     (l.attachWith P H).map f = l.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   induction l <;> simp_all
@@ -466,10 +438,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
       fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩) := by
@@ -500,7 +468,6 @@ theorem attach_filterMap {l : List α} {f : α → Option β} :
       ext
       simp
 
-@[grind =]
 theorem attach_filter {l : List α} (p : α → Bool) :
     (l.filter p).attach = l.attach.filterMap
       fun x => if w : p x.1 then some ⟨x.1, mem_filter.mpr ⟨x.2, w⟩⟩ else none := by
@@ -512,7 +479,7 @@ theorem attach_filter {l : List α} (p : α → Bool) :
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
 
-@[simp, grind =]
+@[simp]
 theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} → Option β} (H) :
     (l.attachWith q H).filterMap f = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩) := by
   induction l with
@@ -521,7 +488,7 @@ theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} →
     simp only [attachWith_cons, filterMap_cons]
     split <;> simp_all [Function.comp_def]
 
-@[simp, grind =]
+@[simp]
 theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bool} (H) :
     (l.attachWith q H).filter p =
       (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩) := by
@@ -531,14 +498,13 @@ theorem filter_attachWith {q : α → Prop} {l : List α} {p : {x // q x} → Bo
     simp only [attachWith_cons, filter_cons]
     split <;> simp_all [Function.comp_def, filter_map]
 
-@[grind =]
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f : ∀ b, q b → γ} {l} (H₁ H₂) :
     pmap f (pmap g l H₁) H₂ =
       pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
         (fun a _ => H₁ a a.2) := by
   simp [pmap_eq_map_attach, attach_map]
 
-@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {l₁ l₂ : List ι}
+@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {l₁ l₂ : List ι}
     (h : ∀ a ∈ l₁ ++ l₂, p a) :
     (l₁ ++ l₂).pmap f h =
       (l₁.pmap f fun a ha => h a (mem_append_left l₂ ha)) ++
@@ -555,50 +521,47 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {l₁ l₂ :
       l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
   pmap_append _
 
-@[simp, grind =] theorem attach_append {xs ys : List α} :
+@[simp] theorem attach_append {xs ys : List α} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_append_left ys h⟩) ++
       ys.attach.map fun ⟨x, h⟩ => ⟨x, mem_append_right xs h⟩ := by
   simp only [attach, attachWith, map_pmap, pmap_append]
   congr 1 <;>
   exact pmap_congr_left _ fun _ _ _ _ => rfl
 
-@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs ys : List α}
+@[simp] theorem attachWith_append {P : α → Prop} {xs ys : List α}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp only [attachWith, pmap_append]
 
-@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
+@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
-@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : List α}
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : List α}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse :=
   pmap_reverse ..
 
-@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : List α}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) :=
   reverse_pmap ..
 
-@[simp, grind =] theorem attach_reverse {xs : List α} :
+@[simp] theorem attach_reverse {xs : List α} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
   apply pmap_congr_left
   intros
   rfl
 
-@[grind =]
 theorem reverse_attach {xs : List α} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   simp only [attach, attachWith, reverse_pmap, map_pmap]
@@ -652,7 +615,7 @@ theorem countP_attachWith {p : α → Prop} {q : α → Bool} {l : List α} (H :
     (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
   simp only [← Function.comp_apply (g := Subtype.val), ← countP_map, attachWith_map_subtype_val]
 
-@[simp]
+@[simp, grind =]
 theorem count_attach [BEq α] {l : List α} {a : {x // x ∈ l}} :
     l.attach.count a = l.count ↑a :=
   Eq.trans (countP_congr fun _ _ => by simp) <| countP_attach

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

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

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

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,26 +332,9 @@ 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] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
+@[simp, grind ←] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
 
 @[simp, grind =] theorem mem_cons : a ∈ b :: l ↔ a = b ∨ a ∈ l :=
   ⟨fun h => by cases h <;> simp [Membership.mem, *],
@@ -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

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]

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

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

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

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)
 

src/Init/Data/Option/Attach.lean

@@ -75,10 +75,7 @@ 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 α) :
+@[simp] theorem attach_map_subtype_val (o : Option α) :
     o.attach.map Subtype.val = o :=
   (attach_map_val _ _).trans (congrFun Option.map_id _)
 
@@ -86,10 +83,7 @@ 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) :
+@[simp] 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 _)
 
@@ -174,23 +168,23 @@ theorem toArray_attachWith {p : α → Prop} {o : Option α} {h} :
     o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by
   cases o <;> simp [toList]
 
-@[grind =] theorem attach_map {o : Option α} (f : α → β) :
+@[grind =]
+theorem attach_map {o : Option α} (f : α → β) :
     (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some_iff.2 ⟨_, h, rfl⟩⟩) := by
   cases o <;> simp
 
-@[grind =] theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
+@[grind =]
+theorem attachWith_map {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), o.map f = some b → P b} :
     (o.map f).attachWith P H = (o.attachWith (P ∘ f) (fun _ h => H _ (map_eq_some_iff.2 ⟨_, h, rfl⟩))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases o <;> simp
 
-@[grind =] theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } → β) :
+@[grind =]
+theorem map_attach_eq_pmap {o : Option α} (f : { x // o = some x } → β) :
     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}
+@[simp] 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
   cases l <;> simp_all
@@ -206,12 +200,12 @@ theorem map_attach_eq_attachWith {o : Option α} {p : α → Prop} (f : ∀ a, o
     o.attach.map (fun x => ⟨x.1, f x.1 x.2⟩) = o.attachWith p f := by
   cases o <;> simp_all
 
-@[grind =] theorem attach_bind {o : Option α} {f : α → Option β} :
+theorem attach_bind {o : Option α} {f : α → Option β} :
     (o.bind f).attach =
       o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, bind_eq_some_iff.2 ⟨_, h, h'⟩⟩ := by
   cases o <;> simp
 
-@[grind =] theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
+theorem bind_attach {o : Option α} {f : {x // o = some x} → Option β} :
     o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩ := by
   cases o <;> simp
 
@@ -219,7 +213,7 @@ theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → o = some a → Op
     o.pbind f = o.attach.bind fun ⟨x, h⟩ => f x h := by
   cases o <;> simp
 
-@[grind =] theorem attach_filter {o : Option α} {p : α → Bool} :
+theorem attach_filter {o : Option α} {p : α → Bool} :
     (o.filter p).attach =
       o.attach.bind fun ⟨x, h⟩ => if h' : p x then some ⟨x, by simp_all⟩ else none := by
   cases o with
@@ -235,12 +229,12 @@ theorem pbind_eq_bind_attach {o : Option α} {f : (a : α) → o = some a → Op
     · rintro ⟨h, rfl⟩
       simp [h]
 
-@[grind =] theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
+theorem filter_attachWith {P : α → Prop} {o : Option α} {h : ∀ x, o = some x → P x} {q : α → Bool} :
     (o.attachWith P h).filter q =
       (o.filter q).attachWith P (fun _ h' => h _ (eq_some_of_filter_eq_some h')) := by
   cases o <;> simp [filter_some] <;> split <;> simp
 
-@[grind =] theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
+theorem filter_attach {o : Option α} {p : {x // o = some x} → Bool} :
     o.attach.filter p = o.pbind fun a h => if p ⟨a, h⟩ then some ⟨a, h⟩ else none := by
   cases o <;> simp [filter_some]
 
@@ -284,7 +278,7 @@ theorem toArray_pmap {p : α → Prop} {o : Option α} {f : (a : α) → p a →
     (o.pmap f h).toArray = o.attach.toArray.map (fun x => f x.1 (h _ x.2)) := by
   cases o <;> simp
 
-@[grind =] theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
+theorem attach_pfilter {o : Option α} {p : (a : α) → o = some a → Bool} :
     (o.pfilter p).attach =
       o.attach.pbind fun x h => if h' : p x (by simp_all) then
         some ⟨x.1, by simpa [pfilter_eq_some_iff] using ⟨_, h'⟩⟩ else none := by

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

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.

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.

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)

src/Init/Data/Vector/Attach.lean

@@ -97,16 +97,16 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
   intro a m h₁ h₂
   congr
 
-@[simp, grind =] theorem pmap_empty {P : α → Prop} {f : ∀ a, P a → β} : pmap f #v[] (by simp) = #v[] := rfl
+@[simp] theorem pmap_empty {P : α → Prop} {f : ∀ a, P a → β} : pmap f #v[] (by simp) = #v[] := rfl
 
-@[simp, grind =] theorem pmap_push {P : α → Prop} {f : ∀ a, P a → β} {a : α} {xs : Vector α n} {h : ∀ b ∈ xs.push a, P b} :
+@[simp] theorem pmap_push {P : α → Prop} {f : ∀ a, P a → β} {a : α} {xs : Vector α n} {h : ∀ b ∈ xs.push a, P b} :
     pmap f (xs.push a) h =
       (pmap f xs (fun a m => by simp at h; exact h a (.inl m))).push (f a (h a (by simp))) := by
   simp [pmap]
 
-@[simp, grind =] theorem attach_empty : (#v[] : Vector α 0).attach = #v[] := rfl
+@[simp] theorem attach_empty : (#v[] : Vector α 0).attach = #v[] := rfl
 
-@[simp, grind =] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #v[], P x) : (#v[] : Vector α 0).attachWith P H = #v[] := rfl
+@[simp] theorem attachWith_empty {P : α → Prop} (H : ∀ x ∈ #v[], P x) : (#v[] : Vector α 0).attachWith P H = #v[] := rfl
 
 @[simp]
 theorem pmap_eq_map {p : α → Prop} {f : α → β} {xs : Vector α n} (H) :
@@ -120,13 +120,11 @@ theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a,
   apply Array.pmap_congr_left
   simpa using h
 
-@[grind =]
 theorem map_pmap {p : α → Prop} {g : β → γ} {f : ∀ a, p a → β} {xs : Vector α n} (H) :
     map g (pmap f xs H) = pmap (fun a h => g (f a h)) xs H := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.map_pmap]
 
-@[grind =]
 theorem pmap_map {p : β → Prop} {g : ∀ b, p b → γ} {f : α → β} {xs : Vector α n} (H) :
     pmap g (map f xs) H = pmap (fun a h => g (f a) h) xs fun _ h => H _ (mem_map_of_mem h) := by
   rcases xs with ⟨xs, rfl⟩
@@ -142,13 +140,13 @@ theorem attachWith_congr {xs ys : Vector α n} (w : xs = ys) {P : α → Prop} {
   subst w
   simp
 
-@[simp, grind =] theorem attach_push {a : α} {xs : Vector α n} :
+@[simp] theorem attach_push {a : α} {xs : Vector α n} :
     (xs.push a).attach =
       (xs.attach.map (fun ⟨x, h⟩ => ⟨x, mem_push_of_mem a h⟩)).push ⟨a, by simp⟩ := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.map_attach_eq_pmap]
 
-@[simp, grind =] theorem attachWith_push {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
+@[simp] theorem attachWith_push {a : α} {xs : Vector α n} {P : α → Prop} {H : ∀ x ∈ xs.push a, P x} :
     (xs.push a).attachWith P H =
       (xs.attachWith P (fun x h => by simp at H; exact H x (.inl h))).push ⟨a, H a (by simp)⟩ := by
   rcases xs with ⟨xs, rfl⟩
@@ -172,9 +170,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 +180,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⟩
@@ -258,26 +250,24 @@ theorem getElem_attach {xs : Vector α n} {i : Nat} (h : i < n) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
-@[simp, grind =] theorem pmap_attach {xs : Vector α n} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
+@[simp] theorem pmap_attach {xs : Vector α n} {p : {x // x ∈ xs} → Prop} {f : ∀ a, p a → β} (H) :
     pmap f xs.attach H =
       xs.pmap (P := fun a => ∃ h : a ∈ xs, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
   rcases xs with ⟨xs, rfl⟩
   ext <;> simp
 
-@[simp, grind =] theorem pmap_attachWith {xs : Vector α n} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
+@[simp] theorem pmap_attachWith {xs : Vector α n} {p : {x // q x} → Prop} {f : ∀ a, p a → β} (H₁ H₂) :
     pmap f (xs.attachWith q H₁) H₂ =
       xs.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
         (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
   ext <;> simp
 
-@[grind =]
 theorem foldl_pmap {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : γ → β → γ) (x : γ) :
     (xs.pmap f H).foldl g x = xs.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
   rw [pmap_eq_map_attach, foldl_map]
 
-@[grind =]
 theorem foldr_pmap {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β}
     (H : ∀ (a : α), a ∈ xs → P a) (g : β → γ → γ) (x : γ) :
     (xs.pmap f H).foldr g x = xs.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
@@ -313,20 +303,18 @@ theorem foldr_attach {xs : Vector α n} {f : α → β → β} {b : β} :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[grind =]
 theorem attach_map {xs : Vector α n} {f : α → β} :
     (xs.map f).attach = xs.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem h⟩) := by
   cases xs
   ext <;> simp
 
-@[grind =]
 theorem attachWith_map {xs : Vector α n} {f : α → β} {P : β → Prop} (H : ∀ (b : β), b ∈ xs.map f → P b) :
     (xs.map f).attachWith P H = (xs.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.attachWith_map]
 
-@[simp, grind =] theorem map_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
+@[simp] theorem map_attachWith {xs : Vector α n} {P : α → Prop} {H : ∀ (a : α), a ∈ xs → P a}
     {f : { x // P x } → β} :
     (xs.attachWith P H).map f = xs.attach.map fun ⟨x, h⟩ => f ⟨x, H _ h⟩ := by
   rcases xs with ⟨xs, rfl⟩
@@ -345,10 +333,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₂ =
       pmap (α := { x // x ∈ xs }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) xs.attach
@@ -356,7 +340,7 @@ theorem pmap_pmap {p : α → Prop} {q : β → Prop} {g : ∀ a, p a → β} {f
   rcases xs with ⟨xs, rfl⟩
   ext <;> simp
 
-@[simp, grind =] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs : Vector ι n} {ys : Vector ι m}
+@[simp] theorem pmap_append {p : ι → Prop} {f : ∀ a : ι, p a → α} {xs : Vector ι n} {ys : Vector ι m}
     (h : ∀ a ∈ xs ++ ys, p a) :
     (xs ++ ys).pmap f h =
       (xs.pmap f fun a ha => h a (mem_append_left ys ha)) ++
@@ -371,69 +355,66 @@ theorem pmap_append' {p : α → Prop} {f : ∀ a : α, p a → β} {xs : Vector
       xs.pmap f h₁ ++ ys.pmap f h₂ :=
   pmap_append _
 
-@[simp, grind =] theorem attach_append {xs : Vector α n} {ys : Vector α m} :
+@[simp] theorem attach_append {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => (⟨x, mem_append_left ys h⟩ : { x // x ∈ xs ++ ys })) ++
       ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys })) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
   simp [Array.map_attach_eq_pmap]
 
-@[simp, grind =] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
+@[simp] theorem attachWith_append {P : α → Prop} {xs : Vector α n} {ys : Vector α m}
     {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
     (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
       ys.attachWith P (fun a h => H a (mem_append_right xs h)) := by
   simp [attachWith]
 
-@[simp, grind =] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
+@[simp] theorem pmap_reverse {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
     (H : ∀ (a : α), a ∈ xs.reverse → P a) :
     xs.reverse.pmap f H = (xs.pmap f (fun a h => H a (by simpa using h))).reverse := by
   induction xs <;> simp_all
 
-@[grind =]
 theorem reverse_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h)) := by
   rw [pmap_reverse]
 
-@[simp, grind =] theorem attachWith_reverse {P : α → Prop} {xs : Vector α n}
+@[simp] theorem attachWith_reverse {P : α → Prop} {xs : Vector α n}
     {H : ∀ (a : α), a ∈ xs.reverse → P a} :
     xs.reverse.attachWith P H =
       (xs.attachWith P (fun a h => H a (by simpa using h))).reverse := by
   cases xs
   simp
 
-@[grind =]
 theorem reverse_attachWith {P : α → Prop} {xs : Vector α n}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) := by
   cases xs
   simp
 
-@[simp, grind =] theorem attach_reverse {xs : Vector α n} :
+@[simp] theorem attach_reverse {xs : Vector α n} :
     xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   rw [attach_congr (reverse_mk ..)]
   simp [Array.map_attachWith]
 
-@[grind =]
 theorem reverse_attach {xs : Vector α n} :
     xs.attach.reverse = xs.reverse.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases xs
   simp [Array.map_attach_eq_pmap]
 
-@[simp, grind =] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
+@[simp] theorem back?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
     (H : ∀ (a : α), a ∈ xs → P a) :
     (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m) := by
   cases xs
   simp
 
-@[simp, grind =] theorem back?_attachWith {P : α → Prop} {xs : Vector α n}
+@[simp] theorem back?_attachWith {P : α → Prop} {xs : Vector α n}
     {H : ∀ (a : α), a ∈ xs → P a} :
     (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
-@[simp, grind =]
+@[simp]
 theorem back?_attach {xs : Vector α n} :
     xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs

src/Init/Data/Vector/Lemmas.lean

@@ -879,11 +879,13 @@ set_option linter.indexVariables false in
   rcases xs with ⟨xs, rfl⟩
   simp
 
+@[grind =]
 theorem getElem_push {xs : Vector α n} {x : α} {i : Nat} (h : i < n + 1) :
     (xs.push x)[i] = if h : i < n then xs[i] else x := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.getElem_push]
 
+@[grind =]
 theorem getElem?_push {xs : Vector α n} {x : α} {i : Nat} : (xs.push x)[i]? = if i = n then some x else xs[i]? := by
   simp [getElem?_def, getElem_push]
   (repeat' split) <;> first | rfl | omega
@@ -907,6 +909,8 @@ theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a
 
 grind_pattern getElem_mem => xs[i] ∈ xs
 
+
+@[grind ←]
 theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun
 
 @[simp, grind =] theorem mem_push {xs : Vector α n} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by

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]

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

src/Init/Tactics.lean

@@ -436,8 +436,8 @@ macro "rfl'" : tactic => `(tactic| set_option smartUnfolding false in with_unfol
 /--
 `ac_rfl` proves equalities up to application of an associative and commutative operator.
 ```
-instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
-instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
+instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
+instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
 
 example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by ac_rfl
 ```
@@ -1563,8 +1563,8 @@ syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
   list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
   can also be used, to signify the target of the goal.
 ```
-instance : Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
-instance : Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
+instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
+instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩
 
 example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
  ac_nf

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -101,24 +101,32 @@ instance : Literal Bool where
   getLit := getBoolLit
   mkLit := mkBoolLit
 
-private partial def getLitAux [Inhabited α] (fvarId : FVarId) (ofNat : Nat → α) (ofNatName : Name) : CompilerM (Option α) := do
+private def getLitAux (fvarId : FVarId) (ofNat : Nat → α) (ofNatName : Name) : CompilerM (Option α) := do
   let some (.const declName _ #[.fvar fvarId]) ← findLetValue? fvarId | return none
   unless declName == ofNatName do return none
   let some natLit ← getLit fvarId | return none
   return ofNat natLit
 
-def mkNatWrapperInstance [Inhabited α] (ofNat : Nat → α) (ofNatName : Name) (toNat : α → Nat) : Literal α where
+def mkNatWrapperInstance (ofNat : Nat → α) (ofNatName : Name) (toNat : α → Nat) : Literal α where
   getLit := (getLitAux · ofNat ofNatName)
   mkLit x := do
     let helperId ← mkAuxLit <| toNat x
     return .const ofNatName [] #[.fvar helperId]
 
-instance : Literal UInt8 := mkNatWrapperInstance UInt8.ofNat ``UInt8.ofNat UInt8.toNat
-instance : Literal UInt16 := mkNatWrapperInstance UInt16.ofNat ``UInt16.ofNat UInt16.toNat
-instance : Literal UInt32 := mkNatWrapperInstance UInt32.ofNat ``UInt32.ofNat UInt32.toNat
-instance : Literal UInt64 := mkNatWrapperInstance UInt64.ofNat ``UInt64.ofNat UInt64.toNat
 instance : Literal Char := mkNatWrapperInstance Char.ofNat ``Char.ofNat Char.toNat
 
+def mkUIntInstance (matchLit : LitValue → Option α) (litValueCtor : α → LitValue) : Literal α where
+  getLit fvarId := do
+    let some (.lit litVal) ← findLetValue? fvarId | return none
+    return matchLit litVal
+  mkLit x :=
+    return .lit <| litValueCtor x
+
+instance : Literal UInt8 := mkUIntInstance (fun | .uint8 x => some x | _ => none) .uint8
+instance : Literal UInt16 := mkUIntInstance (fun | .uint16 x => some x | _ => none) .uint16
+instance : Literal UInt32 := mkUIntInstance (fun | .uint32 x => some x | _ => none) .uint32
+instance : Literal UInt64 := mkUIntInstance (fun | .uint64 x => some x | _ => none) .uint64
+
 end Literals
 
 /--
@@ -386,7 +394,7 @@ def relationFolders : List (Name × Folder) := [
   (``UInt64.decLt, Folder.mkBinaryDecisionProcedure UInt64.decLt),
   (``UInt64.decLe, Folder.mkBinaryDecisionProcedure UInt64.decLe),
   (``Bool.decEq, Folder.mkBinaryDecisionProcedure Bool.decEq),
-  (``Bool.decEq, Folder.mkBinaryDecisionProcedure String.decEq)
+  (``String.decEq, Folder.mkBinaryDecisionProcedure String.decEq)
 ]
 
 def conversionFolders : List (Name × Folder) := [

src/Lean/Data/Lsp/Utf16.lean

@@ -94,6 +94,10 @@ def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
 def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
   { start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
 
+/-- Gets the LSP range of syntax `stx`. -/
+def lspRangeOfStx? (text : FileMap) (stx : Syntax) (canonicalOnly := false) : Option Lsp.Range :=
+  text.utf8RangeToLspRange <$> stx.getRange? canonicalOnly
+
 def lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : String.Range :=
   { start := text.lspPosToUtf8Pos range.start, stop := text.lspPosToUtf8Pos range.end }
 

src/Lean/Data/NameMap.lean

@@ -8,5 +8,3 @@ module
 prelude
 public import Lean.Data.NameMap.Basic
 public import Lean.Data.NameMap.AdditionalOperations
-
-public section

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"

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"

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),

src/Lean/Linter/MissingDocs.lean

@@ -126,6 +126,10 @@ def hasInheritDoc (attrs : Syntax) : Bool :=
     attr[1].isOfKind ``Parser.Attr.simple &&
     attr[1][0].getId.eraseMacroScopes == `inherit_doc
 
+def hasTacticAlt (attrs : Syntax) : Bool :=
+  attrs[0][1].getSepArgs.any fun attr =>
+    attr[1].isOfKind ``Parser.Attr.tactic_alt
+
 def declModifiersPubNoDoc (mods : Syntax) : CommandElabM Bool := do
   let isPublic := if (← getEnv).header.isModule && !(← getScope).isPublic then
     mods[2][0].getKind == ``Command.public else
@@ -201,7 +205,7 @@ def checkMixfix : SimpleHandler := fun stx => do
 
 @[builtin_missing_docs_handler «syntax»]
 def checkSyntax : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
     if stx[5].isNone then lint stx[3] "syntax"
     else lintNamed stx[5][0][3] "syntax"
 
@@ -217,13 +221,13 @@ def checkSyntaxCat : SimpleHandler := mkSimpleHandler "syntax category"
 
 @[builtin_missing_docs_handler «macro»]
 def checkMacro : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
     if stx[5].isNone then lint stx[3] "macro"
     else lintNamed stx[5][0][3] "macro"
 
 @[builtin_missing_docs_handler «elab»]
 def checkElab : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] then
+  if stx[0].isNone && stx[2][0][0].getKind != ``«local» && !hasInheritDoc stx[1] && !hasTacticAlt stx[1] then
     if stx[5].isNone then lint stx[3] "elab"
     else lintNamed stx[5][0][3] "elab"
 

src/Lean/PremiseSelection.lean

@@ -6,134 +6,5 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Lean.Elab.Command
-public import Lean.Meta.Eval
-public import Lean.Meta.CompletionName
-public import Init.Data.Random
-
-public section
-
-/-!
-# An API for premise selection algorithms.
-
-This module provides a basic API for premise selection algorithms,
-which are used to suggest identifiers that should be introduced in a proof.
-
-The core interface is the `Selector` type, which is a function from a metavariable
-and a configuration to a list of suggestions.
-
-The `Selector` is registered as an environment extension, and the trivial (no suggestions) implementation
-is `Lean.PremiseSelection.empty`.
-
-Lean does not provide a default premise selector, so this module is intended to be used in conjunction
-with a downstream package which registers a premise selector.
--/
-
-namespace Lean.PremiseSelection
-
-/--
-A `Suggestion` is essentially just an identifier and a confidence score that the identifier is relevant.
-If the premise selection request included information about the intended use (e.g. in the simplifier, in `grind`, etc.)
-the score may be adjusted for that application.
-
--/
-structure Suggestion where
-  name : Name
-  /--
-  The score of the suggestion, as a probability that this suggestion should be used.
-  -/
-  score : Float
-
-structure Config where
-  /--
-  The maximum number of suggestions to return.
-  -/
-  maxSuggestions : Option Nat := none
-  /--
-  The tactic that is calling the premise selection, e.g. `simp`, `grind`, or `aesop`.
-  This may be used to adjust the score of the suggestions
-  -/
-  caller : Option Name := none
-  /--
-  A filter on suggestions; only suggestions returning `true` should be returned.
-  (It can be better to filter on the premise selection side, to ensure that enough suggestions are returned.)
-  -/
-  filter : Name → MetaM Bool := fun _ => pure true
-  /--
-  An optional arbitrary "hint" to the premise selection algorithm.
-  There is no guarantee that the algorithm will make any use of the hint.
-
-  Potential use cases include a natural language comment provided by the user
-  (e.g. allowing use of the premise selector as a search engine)
-  or including context from the current proof and/or file.
-
-  We may later split these use cases into separate fields if necessary.
-  -/
-  hint : Option String := none
-
-abbrev Selector : Type := MVarId → Config → MetaM (Array Suggestion)
-
-/--
-The trivial premise selector, which returns no suggestions.
--/
-def empty : Selector := fun _ _ => pure #[]
-
-/-- A random premise selection algorithm, provided solely for testing purposes. -/
-def random (gen : StdGen := ⟨37, 59⟩) : Selector := fun _ cfg => do
-  IO.stdGenRef.set gen
-  let env ← getEnv
-  let max := cfg.maxSuggestions.getD 10
-  let consts := env.const2ModIdx.keysArray
-  let mut suggestions := #[]
-  while suggestions.size < max do
-    let i ← IO.rand 0 consts.size
-    let name := consts[i]!
-    if ! (`Lean).isPrefixOf name && Lean.Meta.allowCompletion env name then
-      suggestions := suggestions.push { name := name, score := 1.0 / consts.size.toFloat }
-  return suggestions
-
-initialize premiseSelectorExt : EnvExtension (Option Selector) ←
-  registerEnvExtension (pure none)
-
-/-- Generate premise suggestions for the given metavariable, using the currently registered premise selector. -/
-def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
-  let some selector := premiseSelectorExt.getState (← getEnv) |
-    throwError "No premise selector registered. \
-      (Note the Lean does not provide a default premise selector, these must be installed by a downstream library.)"
-  selector m c
-
-/-!
-Currently the registration mechanism is just global state.
-This means that if multiple modules register premise selectors,
-the behaviour will be dependent on the order of loading modules.
-
-We should replace this with a mechanism so that
-premise selectors are configured via options in the `lakefile`, and
-commands are only used to override in a single declaration or file.
--/
-
-/-- Set the current premise selector.-/
-def registerPremiseSelector (selector : Selector) : CoreM Unit := do
-  modifyEnv fun env => premiseSelectorExt.setState env (some selector)
-
-open Lean Elab Command in
-@[builtin_command_elab setPremiseSelectorCmd, inherit_doc setPremiseSelectorCmd]
-def elabSetPremiseSelector : CommandElab
-  | `(command| set_premise_selector $selector) => do
-    let selector ← liftTermElabM do
-      try
-        let selectorTerm ← Term.elabTermEnsuringType selector (some (Expr.const ``Selector []))
-        unsafe Meta.evalExpr Selector (Expr.const ``Selector []) selectorTerm
-      catch _ =>
-        throwError "Failed to elaborate {selector} as a `MVarId → Config → MetaM (Array Suggestion)`."
-    liftCoreM (registerPremiseSelector selector)
-  | _ => throwUnsupportedSyntax
-
-open Lean.Elab.Tactic in
-@[builtin_tactic Lean.Parser.Tactic.suggestPremises] def evalSuggestPremises : Tactic := fun _ =>
-  liftMetaTactic1 fun mvarId => do
-    let suggestions ← select mvarId
-    logInfo m!"Premise suggestions: {suggestions.map (·.name)}"
-    return mvarId
-
-end Lean.PremiseSelection
+import Lean.PremiseSelection.Basic
+import Lean.PremiseSelection.MePo

src/Lean/PremiseSelection/Basic.lean

@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public import Lean.Elab.Command
+public import Lean.Meta.Eval
+public import Lean.Meta.CompletionName
+public import Init.Data.Random
+
+/-!
+# An API for premise selection algorithms.
+
+This module provides a basic API for premise selection algorithms,
+which are used to suggest identifiers that should be introduced in a proof.
+
+The core interface is the `Selector` type, which is a function from a metavariable
+and a configuration to a list of suggestions.
+
+The `Selector` is registered as an environment extension, and the trivial (no suggestions) implementation
+is `Lean.PremiseSelection.empty`.
+
+Lean does not provide a default premise selector, so this module is intended to be used in conjunction
+with a downstream package which registers a premise selector.
+-/
+
+@[expose] public section
+
+namespace Lean.PremiseSelection
+
+/--
+A `Suggestion` is essentially just an identifier and a confidence score that the identifier is relevant.
+If the premise selection request included information about the intended use (e.g. in the simplifier, in `grind`, etc.)
+the score may be adjusted for that application.
+
+-/
+structure Suggestion where
+  name : Name
+  /--
+  The score of the suggestion, as a probability that this suggestion should be used.
+  -/
+  score : Float
+
+structure Config where
+  /--
+  The maximum number of suggestions to return.
+  -/
+  maxSuggestions : Option Nat := none
+  /--
+  The tactic that is calling the premise selection, e.g. `simp`, `grind`, or `aesop`.
+  This may be used to adjust the score of the suggestions
+  -/
+  caller : Option Name := none
+  /--
+  A filter on suggestions; only suggestions returning `true` should be returned.
+  (It can be better to filter on the premise selection side, to ensure that enough suggestions are returned.)
+  -/
+  filter : Name → MetaM Bool := fun _ => pure true
+  /--
+  An optional arbitrary "hint" to the premise selection algorithm.
+  There is no guarantee that the algorithm will make any use of the hint.
+
+  Potential use cases include a natural language comment provided by the user
+  (e.g. allowing use of the premise selector as a search engine)
+  or including context from the current proof and/or file.
+
+  We may later split these use cases into separate fields if necessary.
+  -/
+  hint : Option String := none
+
+abbrev Selector : Type := MVarId → Config → MetaM (Array Suggestion)
+
+section DenyList
+
+/-- Premises from a module whose name has one of the following components are not retrieved. -/
+builtin_initialize moduleDenyListExt : SimplePersistentEnvExtension String (List String) ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := (·.cons)
+    addImportedFn := mkStateFromImportedEntries (·.cons) []
+  }
+
+/-- A premise whose name has one of the following components is not retrieved. -/
+builtin_initialize nameDenyListExt : SimplePersistentEnvExtension String (List String) ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := (·.cons)
+    addImportedFn := mkStateFromImportedEntries (·.cons) []
+  }
+
+/-- A premise whose `type.getForallBody.getAppFn` is a constant that has one of these prefixes is not retrieved. -/
+builtin_initialize typePrefixDenyListExt : SimplePersistentEnvExtension Name (List Name) ←
+  registerSimplePersistentEnvExtension {
+    addEntryFn := (·.cons)
+    addImportedFn := mkStateFromImportedEntries (·.cons) []
+  }
+
+def isDeniedModule (env : Environment) (moduleName : Name) : Bool :=
+  (moduleDenyListExt.getState env).any fun p => moduleName.anyS (· == p)
+
+def isDeniedPremise (env : Environment) (name : Name) : Bool := Id.run do
+  if name == ``sorryAx then return true
+  if name.isInternalDetail then return true
+  if (nameDenyListExt.getState env).any (fun p => name.anyS (· == p)) then return true
+  if let some moduleIdx := env.getModuleIdxFor? name then
+    let moduleName := env.header.moduleNames[moduleIdx.toNat]!
+    if isDeniedModule env moduleName then
+      return true
+  let some ci := env.find? name | return true
+  if let .const fnName _ := ci.type.getForallBody.getAppFn then
+    if (typePrefixDenyListExt.getState env).any (fun p => p.isPrefixOf fnName) then return true
+  return false
+
+end DenyList
+
+/--
+The trivial premise selector, which returns no suggestions.
+-/
+def empty : Selector := fun _ _ => pure #[]
+
+/-- A random premise selection algorithm, provided solely for testing purposes. -/
+def random (gen : StdGen := ⟨37, 59⟩) : Selector := fun _ cfg => do
+  IO.stdGenRef.set gen
+  let env ← getEnv
+  let max := cfg.maxSuggestions.getD 10
+  let consts := env.const2ModIdx.keysArray
+  let mut suggestions := #[]
+  while suggestions.size < max do
+    let i ← IO.rand 0 consts.size
+    let name := consts[i]!
+    unless isDeniedPremise env name do
+      suggestions := suggestions.push { name := name, score := 1.0 / consts.size.toFloat }
+  return suggestions
+
+builtin_initialize premiseSelectorExt : EnvExtension (Option Selector) ←
+  registerEnvExtension (pure none)
+
+/-- Generate premise suggestions for the given metavariable, using the currently registered premise selector. -/
+def select (m : MVarId) (c : Config := {}) : MetaM (Array Suggestion) := do
+  let some selector := premiseSelectorExt.getState (← getEnv) |
+    throwError "No premise selector registered. \
+      (Note the Lean does not provide a default premise selector, these must be installed by a downstream library.)"
+  selector m c
+
+/-!
+Currently the registration mechanism is just global state.
+This means that if multiple modules register premise selectors,
+the behaviour will be dependent on the order of loading modules.
+
+We should replace this with a mechanism so that
+premise selectors are configured via options in the `lakefile`, and
+commands are only used to override in a single declaration or file.
+-/
+
+/-- Set the current premise selector.-/
+def registerPremiseSelector (selector : Selector) : CoreM Unit := do
+  modifyEnv fun env => premiseSelectorExt.setState env (some selector)
+
+open Lean Elab Command in
+@[builtin_command_elab setPremiseSelectorCmd, inherit_doc setPremiseSelectorCmd]
+def elabSetPremiseSelector : CommandElab
+  | `(command| set_premise_selector $selector) => do
+    let selector ← liftTermElabM do
+      try
+        let selectorTerm ← Term.elabTermEnsuringType selector (some (Expr.const ``Selector []))
+        unsafe Meta.evalExpr Selector (Expr.const ``Selector []) selectorTerm
+      catch _ =>
+        throwError "Failed to elaborate {selector} as a `MVarId → Config → MetaM (Array Suggestion)`."
+    liftCoreM (registerPremiseSelector selector)
+  | _ => throwUnsupportedSyntax
+
+open Lean.Elab.Tactic in
+@[builtin_tactic Lean.Parser.Tactic.suggestPremises] def evalSuggestPremises : Tactic := fun _ =>
+  liftMetaTactic1 fun mvarId => do
+    let suggestions ← select mvarId
+    logInfo m!"Premise suggestions: {suggestions.map (·.name)}"
+    return mvarId
+
+end Lean.PremiseSelection

src/Lean/PremiseSelection/MePo.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public import Lean.PremiseSelection.Basic
+import Lean.Util.FoldConsts
+import Lean.Meta.Basic
+
+/-!
+# MePo premise selection
+
+This is a naive implement of the MePo premise selection algorithm, from
+"Lightweight relevance filtering for machine-generated resolution problems" by Meng and Paulson.
+
+It needs to be tuned and evaluated for Lean.
+-/
+
+open Lean
+
+namespace Lean.PremiseSelection.MePo
+
+def symbolFrequency (env : Environment) : NameMap Nat := Id.run do
+  let mut map := {}
+  for (_, ci) in env.constants do
+    for n' in ci.type.getUsedConstantsAsSet do
+      map := map.alter n' fun i? => some (i?.getD 0 + 1)
+  return map
+
+def weightedScore (weight : Name → Float) (relevant candidate : NameSet) : Float :=
+  let S := candidate
+  let R := relevant ∩ S
+  let R' := S \ R
+  let M := R.foldl (fun acc n => acc + weight n) 0
+  M / (M + R'.size.toFloat)
+
+-- This function is taken from the MePo paper and needs to be tuned.
+def weightFunction (n : Nat) := 1.0 + 2.0 / (n.log2.toFloat + 1.0)
+
+def frequencyScore (frequency : Name → Nat) (relevant candidate : NameSet) : Float :=
+  weightedScore (fun n => weightFunction (frequency n)) relevant candidate
+
+def unweightedScore (relevant candidate : NameSet) : Float := weightedScore (fun _ => 1) relevant candidate
+
+def mepo (initialRelevant : NameSet) (score : NameSet → NameSet → Float) (accept : ConstantInfo → CoreM Bool) (p : Float) (c : Float) : CoreM (Array (Name × Float)) := do
+  let env ← getEnv
+  let mut p := p
+  let mut candidates := #[]
+  let mut relevant := initialRelevant
+  let mut accepted : Array (Name × Float) := {}
+  for (n, ci) in env.constants do
+    if ← accept ci then
+      candidates := candidates.push (n, ci.type.getUsedConstantsAsSet)
+  while candidates.size > 0 do
+    let (newAccepted, candidates') := candidates.map (fun (n, c) => (n, c, score relevant c)) |>.partition fun (_, _, s) => p ≤ s
+    if newAccepted.isEmpty then return accepted
+    accepted := newAccepted.foldl (fun acc (n, _, s) => acc.push (n, s)) accepted
+    candidates := candidates'.map fun (n, c, _) => (n, c)
+    relevant := newAccepted.foldl (fun acc (_, ns, _) => acc ++ ns) relevant
+    p := p + (1 - p) / c
+  return accepted
+
+open Lean Meta MVarId in
+def _root_.Lean.MVarId.getConstants (g : MVarId) : MetaM NameSet := withContext g do
+  let mut c := (← g.getType).getUsedConstantsAsSet
+  for t in (← getLocalHyps) do
+    c := c ∪ (← inferType t).getUsedConstantsAsSet
+  return c
+
+end MePo
+
+open MePo
+
+-- The values of p := 0.6 and c := 2.4 are taken from the MePo paper, and need to be tuned.
+-- When retrieving ≤32 premises for use by downstream automation, Thomas Zhu suggests that c := 0.5 is optimal.
+public def mepoSelector (useRarity : Bool) (p : Float := 0.6) (c : Float := 2.4) : Selector := fun g config => do
+  let constants ← g.getConstants
+  let env ← getEnv
+  let score := if useRarity then
+    let frequency := symbolFrequency env
+    frequencyScore (frequency.getD · 0)
+  else
+    unweightedScore
+  let accept := fun ci => return !isDeniedPremise env ci.name
+  let suggestions ← mepo constants score accept p c
+  let suggestions := suggestions
+    |>.map (fun (n, s) => { name := n, score := s })
+    |>.reverse  -- we favor constants that appear at the end of `env.constants`
+  match config.maxSuggestions with
+  | none => return suggestions
+  | some k => return suggestions.take k

src/Lean/Server/Rpc/RequestHandling.lean

@@ -36,6 +36,10 @@ private unsafe def evalRpcProcedureUnsafe (env : Environment) (opts : Options) (
 private opaque evalRpcProcedure (env : Environment) (opts : Options) (procName : Name) :
     Except String RpcProcedure
 
+/-- Checks whether a builtin RPC procedure exists with the given name. -/
+def existsBuiltinRpcProcedure (method : Name) : IO Bool := do
+  return (← builtinRpcProcedures.get).contains method
+
 open RequestM in
 def handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do
   -- The imports are finished at this point, because the handleRequest function

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

src/Lean/Util/SearchPath.lean

@@ -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)

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']

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']

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

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]

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

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 =

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 =

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⟩

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⟩

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₂.
 

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⟩

src/Std/Internal/Async/TCP.lean

@@ -118,12 +118,19 @@ Connects the client socket to the given address.
 def connect (s : Client) (addr : SocketAddress) : Async Unit :=
   Async.ofPromise <| s.native.connect addr
 
+/--
+Sends multiple data buffers through the client socket.
+-/
+@[inline]
+def sendAll (s : Client) (data : Array ByteArray) : Async Unit :=
+  Async.ofPromise <| s.native.send data
+
 /--
 Sends data through the client socket.
 -/
 @[inline]
 def send (s : Client) (data : ByteArray) : Async Unit :=
-  Async.ofPromise <| s.native.send data
+  Async.ofPromise <| s.native.send #[data]
 
 /--
 Receives data from the client socket. If data is received, it’s wrapped in .some. If EOF is reached,

src/Std/Internal/Async/UDP.lean

@@ -61,13 +61,21 @@ automatically sent to that destination.
 def connect (s : Socket) (addr : SocketAddress) : IO Unit :=
   s.native.connect addr
 
+/--
+Sends multiple data buffers through an UDP socket. The `addr` parameter specifies the destination
+address. If `addr` is `none`, the data is sent to the default peer address set by `connect`.
+-/
+@[inline]
+def sendAll (s : Socket) (data : Array ByteArray) (addr : Option SocketAddress := none) : Async Unit :=
+  Async.ofPromise <| s.native.send data addr
+
 /--
 Sends data through an UDP socket. The `addr` parameter specifies the destination address. If `addr`
 is `none`, the data is sent to the default peer address set by `connect`.
 -/
 @[inline]
 def send (s : Socket) (data : ByteArray) (addr : Option SocketAddress := none) : Async Unit :=
-  Async.ofPromise <| s.native.send data addr
+  Async.ofPromise <| s.native.send #[data] addr
 
 /--
 Receives data from an UDP socket. `size` is for the maximum bytes to receive.

src/Std/Internal/UV/TCP.lean

@@ -47,7 +47,7 @@ opaque connect (socket : @& Socket) (addr : @& SocketAddress) : IO (IO.Promise (
 Sends data through a TCP socket.
 -/
 @[extern "lean_uv_tcp_send"]
-opaque send (socket : @& Socket) (data : ByteArray) : IO (IO.Promise (Except IO.Error Unit))
+opaque send (socket : @& Socket) (data : Array ByteArray) : IO (IO.Promise (Except IO.Error Unit))
 
 /--
 Receives data from a TCP socket with a maximum size of size bytes. The promise resolves when data is

src/Std/Internal/UV/UDP.lean

@@ -55,7 +55,7 @@ Sends data through an UDP socket. The `addr` parameter specifies the destination
 is `none`, the data is sent to the default peer address set by `connect`.
 -/
 @[extern "lean_uv_udp_send"]
-opaque send (socket : @& Socket) (data : ByteArray) (addr : @& Option SocketAddress) : IO (IO.Promise (Except IO.Error Unit))
+opaque send (socket : @& Socket) (data : Array ByteArray) (addr : @& Option SocketAddress) : IO (IO.Promise (Except IO.Error Unit))
 
 /--
 Receives data from an UDP socket. `size` is for the maximum bytes to receive. The promise

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
 

src/runtime/uv/tcp.cpp

@@ -22,6 +22,7 @@ typedef struct {
     lean_object* promise;
     lean_object* data;
     lean_object* socket;
+    uv_buf_t* bufs;
 } tcp_send_data;
 
 // =======================================
@@ -164,14 +165,31 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_
     return lean_io_result_mk_ok(promise);
 }
 
-/* Std.Internal.UV.TCP.Socket.send (socket : @& Socket) (data : ByteArray) : IO (IO.Promise (Except IO.Error Unit)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data, obj_arg /* w */) {
+/* Std.Internal.UV.TCP.Socket.send (socket : @& Socket) (data : Array ByteArray) : IO (IO.Promise (Except IO.Error Unit)) */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array, obj_arg /* w */) {
     lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
 
-    size_t data_len = lean_sarray_size(data);
-    char* data_str = (char*)lean_sarray_cptr(data);
+    size_t array_len = lean_array_size(data_array);
 
-    uv_buf_t buf = uv_buf_init(data_str, data_len);
+    if (array_len == 0) {
+        lean_dec(data_array);
+
+        lean_object* promise = lean_promise_new();
+        mark_mt(promise);
+        lean_promise_resolve_with_code(0, promise);
+
+        return lean_io_result_mk_ok(promise);
+    }
+
+    // Allocate buffer array for uv_write
+    uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t));
+
+    for (size_t i = 0; i < array_len; i++) {
+        lean_object* byte_array = lean_array_get_core(data_array, i);
+        size_t data_len = lean_sarray_size(byte_array);
+        char* data_str = (char*)lean_sarray_cptr(byte_array);
+        bufs[i] = uv_buf_init(data_str, data_len);
+    }
 
     lean_object* promise = lean_promise_new();
     mark_mt(promise);
@@ -181,8 +199,9 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
 
     tcp_send_data* send_data = (tcp_send_data*)write_uv->data;
     send_data->promise = promise;
-    send_data->data = data;
+    send_data->data = data_array;
     send_data->socket = socket;
+    send_data->bufs = bufs;
 
     // These objects are going to enter the loop and be owned by it
     lean_inc(promise);
@@ -190,7 +209,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
 
     event_loop_lock(&global_ev);
 
-    int result = uv_write(write_uv, (uv_stream_t*)tcp_socket->m_uv_tcp, &buf, 1, [](uv_write_t* req, int status) {
+    int result = uv_write(write_uv, (uv_stream_t*)tcp_socket->m_uv_tcp, bufs, array_len, [](uv_write_t* req, int status) {
         tcp_send_data* tup = (tcp_send_data*) req->data;
 
         lean_promise_resolve_with_code(status, tup->promise);
@@ -199,6 +218,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
         lean_dec(tup->data);
         lean_dec(tup->socket);
 
+        free(tup->bufs);
         free(req->data);
         free(req);
     });
@@ -209,8 +229,9 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
         lean_dec(promise); // The structure does not own it.
         lean_dec(promise); // We are not going to return it.
         lean_dec(socket);
-        lean_dec(data);
-
+        lean_dec(data_array);
+        free(bufs);
+        
         free(write_uv->data);
         free(write_uv);
 
@@ -385,7 +406,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, ob
         tcp_socket->m_byte_array = nullptr;
     }
 
-    lean_dec((lean_object*)tcp_socket);
+    lean_dec(socket);
 
     event_loop_unlock(&global_ev);
     return lean_io_result_mk_ok(lean_box(0));
@@ -709,4 +730,4 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int3
 }
 
 #endif
-}
+}

src/runtime/uv/tcp.h

@@ -43,7 +43,7 @@ static inline lean_uv_tcp_socket_object* lean_to_uv_tcp_socket(lean_object* o) {
 
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array, obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket, obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, obj_arg /* w */);

src/runtime/uv/udp.cpp

@@ -16,6 +16,7 @@ typedef struct {
     lean_object *promise;
     lean_object *data;
     lean_object *socket;
+    uv_buf_t* bufs;
 } udp_send_data;
 
 void lean_uv_udp_socket_finalizer(void* ptr) {
@@ -123,14 +124,30 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_
     return lean_io_result_mk_ok(lean_box(0));
 }
 
-/* Std.Internal.UV.UDP.Socket.send (socket : @& Socket) (data : ByteArray) (addr : @& Option SocketAddress) : IO (IO.Promise (Except IO.Error Unit)) */
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data, b_obj_arg opt_addr, obj_arg /* w */) {
+/* Std.Internal.UV.UDP.Socket.send (socket : @& Socket) (data : Array ByteArray) (addr : @& Option SocketAddress) : IO (IO.Promise (Except IO.Error Unit)) */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr, obj_arg /* w */) {
     lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
 
-    size_t data_len = lean_sarray_size(data);
-    char* data_str = (char*)lean_sarray_cptr(data);
+    size_t array_len = lean_array_size(data_array);
 
-    uv_buf_t buf = uv_buf_init(data_str, data_len);
+    if (array_len == 0) {
+        lean_dec(data_array);
+
+        lean_object* promise = lean_promise_new();
+        mark_mt(promise);
+        lean_promise_resolve_with_code(0, promise);
+
+        return lean_io_result_mk_ok(promise);
+    }
+
+    uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t));
+
+    for (size_t i = 0; i < array_len; i++) {
+        lean_object* byte_array = lean_array_get_core(data_array, i);
+        size_t data_len = lean_sarray_size(byte_array);
+        char* data_str = (char*)lean_sarray_cptr(byte_array);
+        bufs[i] = uv_buf_init(data_str, data_len);
+    }
 
     lean_object* promise = lean_promise_new();
     mark_mt(promise);
@@ -140,8 +157,9 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
 
     udp_send_data* send_data = (udp_send_data*)send_uv->data;
     send_data->promise = promise;
-    send_data->data = data;
+    send_data->data = data_array;
     send_data->socket = socket;
+    send_data->bufs = bufs;
 
     // These objects are going to enter the loop and be owned by it
     lean_inc(promise);
@@ -157,7 +175,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
 
     event_loop_lock(&global_ev);
 
-    int result = uv_udp_send(send_uv, udp_socket->m_uv_udp, &buf, 1, (sockaddr*)addr_ptr, [](uv_udp_send_t* req, int status) {
+    int result = uv_udp_send(send_uv, udp_socket->m_uv_udp, bufs, array_len, (sockaddr*)addr_ptr, [](uv_udp_send_t* req, int status) {
         udp_send_data* tup = (udp_send_data*) req->data;
         lean_promise_resolve_with_code(status, tup->promise);
 
@@ -165,6 +183,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
         lean_dec(tup->socket);
         lean_dec(tup->data);
 
+        free(tup->bufs);
         free(req->data);
         free(req);
     });
@@ -179,7 +198,8 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
         lean_dec(promise); // The structure does not own it.
         lean_dec(promise); // We are not going to return it.
         lean_dec(socket); // The loop does not own the object.
-        lean_dec(data); // The data is owned.
+        lean_dec(data_array); // The data is owned.
+        free(bufs);
 
         free(send_uv->data);
         free(send_uv);
@@ -344,10 +364,12 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket,
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, obj_arg /* w */) {
     lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
 
+    lean_inc(socket);
     event_loop_lock(&global_ev);
 
     if (udp_socket->m_promise_read == nullptr) {
         event_loop_unlock(&global_ev);
+        lean_dec(socket);
         return lean_io_result_mk_ok(lean_box(0));
     }
 
@@ -358,14 +380,14 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, ob
     udp_socket->m_promise_read = nullptr;
 
     lean_object* byte_array = udp_socket->m_byte_array;
+
     if (byte_array != nullptr) {
         lean_dec(byte_array);
         udp_socket->m_byte_array = nullptr;
     }
 
-    lean_dec((lean_object*)udp_socket);
-
     event_loop_unlock(&global_ev);
+    lean_dec(socket);
 
     return lean_io_result_mk_ok(lean_box(0));
 }
@@ -601,4 +623,4 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32
 }
 
 #endif
-}
+}

src/runtime/uv/udp.h

@@ -41,7 +41,7 @@ static inline lean_uv_udp_socket_object* lean_to_uv_udp_socket(lean_object * o)
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
-extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data, b_obj_arg opt_addr, obj_arg /* w */);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr, obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket, obj_arg /* w */);
 extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, obj_arg /* w */);