diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 18c13ef21c..3b614f9b3b 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -15,15 +15,6 @@ structure Subarray (α : Type u)  where
   start_le_stop : start ≤ stop
   stop_le_array_size : stop ≤ array.size
 
-@[deprecated Subarray.array (since := "2024-04-13")]
-abbrev Subarray.as (s : Subarray α) : Array α := s.array
-
-@[deprecated Subarray.start_le_stop (since := "2024-04-13")]
-theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
-
-@[deprecated Subarray.stop_le_array_size (since := "2024-04-13")]
-theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.array.size := s.stop_le_array_size
-
 namespace Subarray
 
 def size (s : Subarray α) : Nat :=
diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 43465f4612..f509f7b03a 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -29,9 +29,6 @@ section Nat
 
 instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
 
-@[deprecated isLt (since := "2024-03-12")]
-theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.isLt
-
 /-- Theorem for normalizing the bit vector literal representation. -/
 -- TODO: This needs more usage data to assess which direction the simp should go.
 @[simp, bv_toNat] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = .ofNat n i := rfl
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index f45d367251..0ea46f8ba2 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -16,10 +16,6 @@ def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[deprecated getM (since := "2024-04-17")]
--- `[Monad m]` is not needed here.
-def toMonad [Monad m] [Alternative m] : Option α → m α := getM
-
 /-- Returns `true` on `some x` and `false` on `none`. -/
 @[inline] def isSome : Option α → Bool
   | some _ => true
@@ -28,8 +24,6 @@ def toMonad [Monad m] [Alternative m] : Option α → m α := getM
 @[simp] theorem isSome_none : @isSome α none = false := rfl
 @[simp] theorem isSome_some : isSome (some a) = true := rfl
 
-@[deprecated isSome (since := "2024-04-17"), inline] def toBool : Option α → Bool := isSome
-
 /-- Returns `true` on `none` and `false` on `some x`. -/
 @[inline] def isNone : Option α → Bool
   | some _ => false
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 6851c3ef13..999dacf350 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -514,9 +514,6 @@ instance : Inhabited String := ⟨""⟩
 
 instance : Append String := ⟨String.append⟩
 
-@[deprecated push (since := "2024-04-06")]
-def str : String → Char → String := push
-
 @[inline] def pushn (s : String) (c : Char) (n : Nat) : String :=
   n.repeat (fun s => s.push c) s
 
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index 225424a5f3..056863bef1 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -254,10 +254,6 @@ Apply `And.intro` as much as possible to goal `mvarId`.
 abbrev splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
   splitAndCore mvarId
 
-@[deprecated splitAnd (since := "2024-03-17")]
-def _root_.Lean.Meta.splitAnd (mvarId : MVarId) : MetaM (List MVarId) :=
-  mvarId.splitAnd
-
 def exfalso (mvarId : MVarId) : MetaM MVarId :=
   mvarId.withContext do
     mvarId.checkNotAssigned `exfalso