diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 506c6813f4..33d8c79b97 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1379,8 +1379,6 @@ theorem filter_eq_push_iff {p : α → Bool} {l l' : Array α} {a : α} :
   · rintro ⟨⟨l₁⟩, ⟨l₂⟩, h₁, h₂, h₃, h₄⟩
     refine ⟨l₂.reverse, l₁.reverse, by simp_all⟩
 
-@[deprecated filter_map (since := "2024-06-15")] abbrev map_filter := @filter_map
-
 theorem mem_of_mem_filter {a : α} {l} (h : a ∈ filter p l) : a ∈ l :=
   (mem_filter.mp h).1
 
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 7387c02591..648e6421a3 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1294,11 +1294,6 @@ theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
     BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by
   simp [← shiftLeft_or_distrib]
 
-@[deprecated shiftLeft_add (since := "2024-06-02")]
-theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) :
-    (x <<< n) <<< m = x <<< (n + m) := by
-  rw [shiftLeft_add]
-
 /-! ### shiftLeft reductions from BitVec to Nat -/
 
 @[simp]
@@ -1946,11 +1941,6 @@ theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
     (x <<< n).msb = x.getMsbD n := by
   simp [BitVec.msb]
 
-@[deprecated shiftRight_add (since := "2024-06-02")]
-theorem shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) :
-    (x >>> n) >>> m = x >>> (n + m) := by
-  rw [shiftRight_add]
-
 /-! ### rev -/
 
 theorem getLsbD_rev (x : BitVec w) (i : Fin w) :
diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean
index a93cc7af78..3d57fc3a61 100644
--- a/src/Init/Data/Char/Lemmas.lean
+++ b/src/Init/Data/Char/Lemmas.lean
@@ -70,5 +70,3 @@ theorem utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Siz
   rfl
 
 end Char
-
-@[deprecated Char.utf8Size (since := "2024-06-04")] abbrev String.csize := Char.utf8Size
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 3b9b7efb09..5f59e19cf3 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -258,9 +258,6 @@ theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n)
     have h0 : some a = some a' := h 0
     injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]
 
-/-- Deprecated alias for `ext_get?`. The preferred extensionality theorem is now `ext_getElem?`. -/
-@[deprecated ext_get? (since := "2024-06-07")] abbrev ext := @ext_get?
-
 /-! ### getD -/
 
 /--
@@ -619,11 +616,6 @@ set_option linter.missingDocs false in
 set_option linter.missingDocs false in
 @[deprecated flatMap_cons (since := "2024-10-16")] abbrev cons_flatMap := @flatMap_cons
 
-set_option linter.missingDocs false in
-@[deprecated flatMap_nil (since := "2024-06-15")] abbrev nil_bind := @flatMap_nil
-set_option linter.missingDocs false in
-@[deprecated flatMap_cons (since := "2024-06-15")] abbrev cons_bind := @flatMap_cons
-
 /-! ### replicate -/
 
 /--
@@ -713,11 +705,6 @@ def elem [BEq α] (a : α) : List α → Bool
 theorem elem_cons [BEq α] {a : α} :
     (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl
 
-/-- `notElem a l` is `!(elem a l)`. -/
-@[deprecated "Use `!(elem a l)` instead."(since := "2024-06-15")]
-def notElem [BEq α] (a : α) (as : List α) : Bool :=
-  !(as.elem a)
-
 /-! ### contains -/
 
 @[inherit_doc elem] abbrev contains [BEq α] (as : List α) (a : α) : Bool :=
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 410effcfa1..354fd801cd 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -813,11 +813,6 @@ theorem getElem_cons_length (x : α) (xs : List α) (i : Nat) (h : i = xs.length
     (x :: xs)[i]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by
   rw [getLast_eq_getElem]; cases h; rfl
 
-@[deprecated getElem_cons_length (since := "2024-06-12")]
-theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :
-    (x :: xs).get ⟨n, by simp [h]⟩ = (x :: xs).getLast (cons_ne_nil x xs) := by
-  simp [getElem_cons_length, h]
-
 /-! ### getLast? -/
 
 @[simp] theorem getLast?_singleton (a : α) : getLast? [a] = a := rfl
@@ -1026,21 +1021,10 @@ theorem getLast?_tail (l : List α) : (tail l).getLast? = if l.length = 1 then n
   | _ :: _, 0 => by simp
   | _ :: l, i+1 => by simp [getElem?_map f l i]
 
-@[deprecated getElem?_map (since := "2024-06-12")]
-theorem get?_map (f : α → β) : ∀ l i, (map f l).get? i = (l.get? i).map f
-  | [], _ => rfl
-  | _ :: _, 0 => rfl
-  | _ :: l, i+1 => get?_map f l i
-
 @[simp] theorem getElem_map (f : α → β) {l} {i : Nat} {h : i < (map f l).length} :
     (map f l)[i] = f (l[i]'(length_map l f ▸ h)) :=
   Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl
 
-@[deprecated getElem_map (since := "2024-06-12")]
-theorem get_map (f : α → β) {l i} :
-    get (map f l) i = f (get l ⟨i, length_map l f ▸ i.2⟩) := by
-  simp
-
 @[simp] theorem map_id_fun : map (id : α → α) = id := by
   funext l
   induction l <;> simp_all
@@ -1286,8 +1270,6 @@ theorem filter_map (f : β → α) (l : List β) : filter p (map f l) = map f (f
   | nil => rfl
   | cons a l IH => by_cases h : p (f a) <;> simp [*]
 
-@[deprecated filter_map (since := "2024-06-15")] abbrev map_filter := @filter_map
-
 theorem map_filter_eq_foldr (f : α → β) (p : α → Bool) (as : List α) :
     map f (filter p as) = foldr (fun a bs => bif p a then f a :: bs else bs) [] as := by
   induction as with
@@ -1332,8 +1314,6 @@ theorem filter_congr {p q : α → Bool} :
     · simp [pa, h.1 ▸ pa, filter_congr h.2]
     · simp [pa, h.1 ▸ pa, filter_congr h.2]
 
-@[deprecated filter_congr (since := "2024-06-20")] abbrev filter_congr' := @filter_congr
-
 theorem head_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (l.head w)) :
     (filter p l).head ((ne_nil_of_mem (mem_filter.2 ⟨head_mem w, h⟩))) = l.head w := by
   cases l with
@@ -1561,11 +1541,6 @@ theorem getElem?_append {l₁ l₂ : List α} {i : Nat} :
   · exact getElem?_append_left h
   · exact getElem?_append_right (by simpa using h)
 
-@[deprecated getElem?_append_right (since := "2024-06-12")]
-theorem get?_append_right {l₁ l₂ : List α} {i : Nat} (h : l₁.length ≤ i) :
-    (l₁ ++ l₂).get? i = l₂.get? (i - l₁.length) := by
-  simp [getElem?_append_right, h]
-
 /-- Variant of `getElem_append_left` useful for rewriting from the small list to the big list. -/
 theorem getElem_append_left' (l₂ : List α) {l₁ : List α} {i : Nat} (hi : i < l₁.length) :
     l₁[i] = (l₁ ++ l₂)[i]'(by simpa using Nat.lt_add_right l₂.length hi) := by
@@ -1576,33 +1551,11 @@ theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi :
     l₂[i] = (l₁ ++ l₂)[i + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _) := by
   rw [getElem_append_right] <;> simp [*, le_add_left]
 
-@[deprecated "Deprecated without replacement." (since := "2024-06-12")]
-theorem get_append_right_aux {l₁ l₂ : List α} {i : Nat}
-  (h₁ : l₁.length ≤ i) (h₂ : i < (l₁ ++ l₂).length) : i - l₁.length < l₂.length := by
-  rw [length_append] at h₂
-  exact Nat.sub_lt_left_of_lt_add h₁ h₂
-
-set_option linter.deprecated false in
-@[deprecated getElem_append_right (since := "2024-06-12")]
-theorem get_append_right' {l₁ l₂ : List α} {i : Nat} (h₁ : l₁.length ≤ i) (h₂) :
-    (l₁ ++ l₂).get ⟨i, h₂⟩ = l₂.get ⟨i - l₁.length, get_append_right_aux h₁ h₂⟩ :=
-  Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁]
-
 theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
     l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
   rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h]
   simp
 
-@[deprecated "Deprecated without replacement." (since := "2024-06-12")]
-theorem get_of_append_proof {l : List α}
-    (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) : i < length l := eq ▸ h ▸ by simp_arith
-
-set_option linter.deprecated false in
-@[deprecated getElem_of_append (since := "2024-06-12")]
-theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
-    l.get ⟨i, get_of_append_proof eq h⟩ = a := Option.some.inj <| by
-  rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl
-
 @[simp 1100] theorem singleton_append : [x] ++ l = x :: l := rfl
 
 theorem append_inj :
@@ -1653,26 +1606,6 @@ theorem getLast_concat {a : α} : ∀ (l : List α), getLast (l ++ [a]) (by simp
   | a::t => by
     simp [getLast_cons _, getLast_concat t]
 
-@[deprecated getElem_append (since := "2024-06-12")]
-theorem get_append {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length) :
-    (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩ := by
-  simp [getElem_append, h]
-
-@[deprecated getElem_append_left (since := "2024-06-12")]
-theorem get_append_left (as bs : List α) (h : i < as.length) {h'} :
-    (as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩ := by
-  simp [getElem_append_left, h, h']
-
-@[deprecated getElem_append_right (since := "2024-06-12")]
-theorem get_append_right (as bs : List α) (h : as.length ≤ i) {h' h''} :
-    (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by
-  simp [getElem_append_right, h, h', h'']
-
-@[deprecated getElem?_append_left (since := "2024-06-12")]
-theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) :
-    (l₁ ++ l₂).get? n = l₁.get? n := by
-  simp [getElem?_append_left hn]
-
 @[simp] theorem append_eq_nil_iff : p ++ q = [] ↔ p = [] ∧ q = [] := by
   cases p <;> simp
 
@@ -2199,10 +2132,6 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
     (replicate n a)[m] = a :=
   eq_of_mem_replicate (getElem_mem _)
 
-@[deprecated getElem_replicate (since := "2024-06-12")]
-theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by
-  simp
-
 theorem getElem?_replicate : (replicate n a)[m]? = if m < n then some a else none := by
   by_cases h : m < n
   · rw [getElem?_eq_getElem (by simpa), getElem_replicate, if_pos h]
@@ -2438,10 +2367,6 @@ theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
     rw [getElem?_append_left, getElem?_reverse' _ _ this]
     rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _)
 
-@[deprecated getElem?_reverse' (since := "2024-06-12")]
-theorem get?_reverse' {l : List α} (i j) (h : i + j + 1 = length l) : get? l.reverse i = get? l j := by
-  simp [getElem?_reverse' _ _ h]
-
 @[simp]
 theorem getElem?_reverse {l : List α} {i} (h : i < length l) :
     l.reverse[i]? = l[l.length - 1 - i]? :=
@@ -2456,11 +2381,6 @@ theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) :
   rw [← getElem?_eq_getElem, ← getElem?_eq_getElem]
   rw [getElem?_reverse (by simpa using h)]
 
-@[deprecated getElem?_reverse (since := "2024-06-12")]
-theorem get?_reverse {l : List α} {i} (h : i < length l) :
-    get? l.reverse i = get? l (l.length - 1 - i) := by
-  simp [getElem?_reverse h]
-
 theorem reverseAux_reverseAux_nil (as bs : List α) : reverseAux (reverseAux as bs) [] = reverseAux bs as := by
   induction as generalizing bs with
   | nil => rfl
@@ -2501,10 +2421,6 @@ theorem mem_of_mem_getLast? {l : List α} {a : α} (h : a ∈ getLast? l) : a 
 @[simp] theorem map_reverse (f : α → β) (l : List α) : l.reverse.map f = (l.map f).reverse := by
   induction l <;> simp [*]
 
-@[deprecated map_reverse (since := "2024-06-20")]
-theorem reverse_map (f : α → β) (l : List α) : (l.map f).reverse = l.reverse.map f := by
-  simp
-
 @[simp] theorem filter_reverse (p : α → Bool) (l : List α) : (l.reverse.filter p) = (l.filter p).reverse := by
   induction l with
   | nil => simp
@@ -2968,11 +2884,6 @@ are often used for theorems about `Array.pop`.
   | _::_::_, 0, _ => rfl
   | _::_::_, i+1, h => getElem_dropLast _ i (Nat.add_one_lt_add_one_iff.mp h)
 
-@[deprecated getElem_dropLast (since := "2024-06-12")]
-theorem get_dropLast (xs : List α) (i : Fin xs.dropLast.length) :
-    xs.dropLast.get i = xs.get ⟨i, Nat.lt_of_lt_of_le i.isLt (length_dropLast .. ▸ Nat.pred_le _)⟩ := by
-  simp
-
 theorem getElem?_dropLast (xs : List α) (i : Nat) :
     xs.dropLast[i]? = if i < xs.length - 1 then xs[i]? else none := by
   split
@@ -3510,29 +3421,6 @@ theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a :=
 
 /-! ### Deprecations -/
 
-@[deprecated getD_eq_getElem?_getD (since := "2024-06-12")]
-theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp
-@[deprecated getElem_singleton (since := "2024-06-12")]
-theorem get_singleton (a : α) (n : Fin 1) : get [a] n = a := by simp
-@[deprecated getElem?_concat_length (since := "2024-06-12")]
-theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp
-@[deprecated getElem_set_self (since := "2024-06-12")]
-theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
-    (l.set i a).get ⟨i, h⟩ = a := by
-  simp
-@[deprecated getElem_set_ne (since := "2024-06-12")]
-theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α}
-    (hj : j < (l.set i a).length) :
-    (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by
-  simp [h]
-@[deprecated getElem_set (since := "2024-06-12")]
-theorem get_set {l : List α} {m n} {a : α} (h) :
-    (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by
-  simp [getElem_set]
-@[deprecated cons_inj_right (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right
-@[deprecated ne_nil_of_length_eq_add_one (since := "2024-06-16")]
-abbrev ne_nil_of_length_eq_succ := @ne_nil_of_length_eq_add_one
-
 @[deprecated "Deprecated without replacement." (since := "2024-07-09")]
 theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl
 
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 1fdc1fe60f..b5af5ae6b2 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -47,41 +47,16 @@ length `> i`. Version designed to rewrite from the small list to the big list. -
     L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by
   rw [length_take, Nat.lt_min] at h; rw [getElem_take' L _ h.1]
 
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the big list to the small list. -/
-@[deprecated getElem_take' (since := "2024-06-12")]
-theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) :
-    get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by
-  simp
-
-/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of
-length `> i`. Version designed to rewrite from the small list to the big list. -/
-@[deprecated getElem_take (since := "2024-06-12")]
-theorem get_take' (L : List α) {j i} :
-    get (L.take j) i =
-    get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by
-  simp [getElem_take]
-
 theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
     (l.take n)[m]? = none :=
   getElem?_eq_none <| Nat.le_trans (length_take_le _ _) h
 
-@[deprecated getElem?_take_eq_none (since := "2024-06-12")]
-theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) :
-    (l.take n).get? m = none := by
-  simp [getElem?_take_eq_none h]
-
 theorem getElem?_take {l : List α} {n m : Nat} :
     (l.take n)[m]? = if m < n then l[m]? else none := by
   split
   · next h => exact getElem?_take_of_lt h
   · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h)
 
-@[deprecated getElem?_take (since := "2024-06-12")]
-theorem get?_take_eq_if {l : List α} {n m : Nat} :
-    (l.take n).get? m = if m < n then l.get? m else none := by
-  simp [getElem?_take]
-
 theorem head?_take {l : List α} {n : Nat} :
     (l.take n).head? = if n = 0 then none else l.head? := by
   simp [head?_eq_getElem?, getElem?_take]
@@ -226,13 +201,6 @@ theorem getElem_drop' (L : List α) {i j : Nat} (h : i + j < L.length) :
   · simp [Nat.min_eq_left this, Nat.add_sub_cancel_left]
   · simp [Nat.min_eq_left this, Nat.le_add_right]
 
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/
-@[deprecated getElem_drop' (since := "2024-06-12")]
-theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) :
-    get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by
-  simp [getElem_drop']
-
 /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
 dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
 @[simp] theorem getElem_drop (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).length} :
@@ -241,15 +209,6 @@ dropping the first `i` elements. Version designed to rewrite from the small list
       exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h)) := by
   rw [getElem_drop']
 
-/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
-dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/
-@[deprecated getElem_drop' (since := "2024-06-12")]
-theorem get_drop' (L : List α) {i j} :
-    get (L.drop i) j = get L ⟨i + j, by
-      rw [Nat.add_comm]
-      exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by
-  simp
-
 @[simp]
 theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := by
   ext
@@ -261,10 +220,6 @@ theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? :=
     rw [Nat.add_comm] at h
     apply Nat.lt_sub_of_add_lt h
 
-@[deprecated getElem?_drop (since := "2024-06-12")]
-theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by
-  simp
-
 theorem mem_take_iff_getElem {l : List α} {a : α} :
     a ∈ l.take n ↔ ∃ (i : Nat) (hm : i < min n l.length), l[i] = a := by
   rw [mem_iff_getElem]
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 5f9ca842d1..335ecb9dca 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -67,17 +67,9 @@ theorem getElem_cons_drop : ∀ (l : List α) (i : Nat) (h : i < l.length),
   | _::_, 0, _ => rfl
   | _::_, i+1, h => getElem_cons_drop _ i (Nat.add_one_lt_add_one_iff.mp h)
 
-@[deprecated getElem_cons_drop (since := "2024-06-12")]
-theorem get_cons_drop (l : List α) (i) : get l i :: drop (i + 1) l = drop i l := by
-  simp
-
 theorem drop_eq_getElem_cons {n} {l : List α} (h : n < l.length) : drop n l = l[n] :: drop (n + 1) l :=
   (getElem_cons_drop _ n h).symm
 
-@[deprecated drop_eq_getElem_cons (since := "2024-06-12")]
-theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l := by
-  simp [drop_eq_getElem_cons]
-
 @[simp]
 theorem getElem?_take_of_lt {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l[m]? := by
   induction n generalizing l m with
@@ -91,10 +83,6 @@ theorem getElem?_take_of_lt {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m
       · simp
       · simpa using hn (Nat.lt_of_succ_lt_succ h)
 
-@[deprecated getElem?_take_of_lt (since := "2024-06-12")]
-theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by
-  simp [getElem?_take_of_lt, h]
-
 theorem getElem?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := by simp
 
 @[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (m + n) l
@@ -111,10 +99,6 @@ theorem take_drop : ∀ (m n : Nat) (l : List α), take n (drop m l) = drop m (t
   | _, _, [] => by simp
   | _+1, _, _ :: _ => by simpa [Nat.succ_add, take_succ_cons, drop_succ_cons] using take_drop ..
 
-@[deprecated drop_drop (since := "2024-06-15")]
-theorem drop_add (m n) (l : List α) : drop (m + n) l = drop n (drop m l) := by
-  simp [drop_drop]
-
 @[simp]
 theorem tail_drop (l : List α) (n : Nat) : (l.drop n).tail = l.drop (n + 1) := by
   induction l generalizing n with
diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean
index 4ffb4b08d3..79685a004d 100644
--- a/src/Init/Data/List/Zip.lean
+++ b/src/Init/Data/List/Zip.lean
@@ -76,15 +76,6 @@ theorem getElem?_zip_eq_some {l₁ : List α} {l₂ : List β} {z : α × β} {i
   · rintro ⟨h₀, h₁⟩
     exact ⟨_, _, h₀, h₁, rfl⟩
 
-@[deprecated getElem?_zipWith (since := "2024-06-12")]
-theorem get?_zipWith {f : α → β → γ} :
-    (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with
-      | some a, some b => some (f a b) | _, _ => none := by
-  simp [getElem?_zipWith]
-
-set_option linter.deprecated false in
-@[deprecated getElem?_zipWith (since := "2024-06-07")] abbrev zipWith_get? := @get?_zipWith
-
 theorem head?_zipWith {f : α → β → γ} :
     (List.zipWith f as bs).head? = match as.head?, bs.head? with
       | some a, some b => some (f a b) | _, _ => none := by
@@ -369,15 +360,6 @@ theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
       cases i <;> simp_all
     | cons b bs => cases i <;> simp_all
 
-@[deprecated getElem?_zipWithAll (since := "2024-06-12")]
-theorem get?_zipWithAll {f : Option α → Option β → γ} :
-    (zipWithAll f as bs).get? i = match as.get? i, bs.get? i with
-      | none, none => .none | a?, b? => some (f a? b?) := by
-  simp [getElem?_zipWithAll]
-
-set_option linter.deprecated false in
-@[deprecated getElem?_zipWithAll (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll
-
 theorem head?_zipWithAll {f : Option α → Option β → γ} :
     (zipWithAll f as bs).head? = match as.head?, bs.head? with
       | none, none => .none | a?, b? => some (f a? b?) := by
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index e046df9b9a..9e2d85fab1 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -788,9 +788,6 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by
 theorem pred_lt_of_lt {n m : Nat} (h : m < n) : pred n < n :=
   pred_lt (not_eq_zero_of_lt h)
 
-set_option linter.missingDocs false in
-@[deprecated pred_lt_of_lt (since := "2024-06-01")] abbrev pred_lt' := @pred_lt_of_lt
-
 theorem sub_one_lt_of_lt {n m : Nat} (h : m < n) : n - 1 < n :=
   sub_one_lt (not_eq_zero_of_lt h)
 
@@ -1074,9 +1071,6 @@ theorem pred_mul (n m : Nat) : pred n * m = n * m - m := by
   | zero   => simp
   | succ n => rw [Nat.pred_succ, succ_mul, Nat.add_sub_cancel]
 
-set_option linter.missingDocs false in
-@[deprecated pred_mul (since := "2024-06-01")] abbrev mul_pred_left := @pred_mul
-
 protected theorem sub_one_mul  (n m : Nat) : (n - 1) * m = n * m - m := by
   cases n with
   | zero   => simp
@@ -1086,9 +1080,6 @@ protected theorem sub_one_mul  (n m : Nat) : (n - 1) * m = n * m - m := by
 theorem mul_pred (n m : Nat) : n * pred m = n * m - n := by
   rw [Nat.mul_comm, pred_mul, Nat.mul_comm]
 
-set_option linter.missingDocs false in
-@[deprecated mul_pred (since := "2024-06-01")] abbrev mul_pred_right := @mul_pred
-
 theorem mul_sub_one (n m : Nat) : n * (m - 1) = n * m - n := by
   rw [Nat.mul_comm, Nat.sub_one_mul , Nat.mul_comm]
 
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 6cd491d64b..50c161fb8a 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -1003,11 +1003,6 @@ theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k
   | 0 => rfl
   | k + 1 => by simp [← Nat.add_assoc, shiftLeft_add _ _ k, shiftLeft_succ]
 
-@[deprecated shiftLeft_add (since := "2024-06-02")]
-theorem shiftLeft_shiftLeft (m n : Nat) : ∀ k, (m <<< n) <<< k = m <<< (n + k)
-  | 0 => rfl
-  | k + 1 => by simp [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
-
 @[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
   rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
 
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index f6ff06f5a3..f0658f142a 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -234,23 +234,3 @@ theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNa
 
 theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
   simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
-
-@[deprecated UInt8.toNat_zero (since := "2024-06-23")] protected abbrev UInt8.zero_toNat := @UInt8.toNat_zero
-@[deprecated UInt8.toNat_div (since := "2024-06-23")] protected abbrev UInt8.div_toNat := @UInt8.toNat_div
-@[deprecated UInt8.toNat_mod (since := "2024-06-23")] protected abbrev UInt8.mod_toNat := @UInt8.toNat_mod
-
-@[deprecated UInt16.toNat_zero (since := "2024-06-23")] protected abbrev UInt16.zero_toNat := @UInt16.toNat_zero
-@[deprecated UInt16.toNat_div (since := "2024-06-23")] protected abbrev UInt16.div_toNat := @UInt16.toNat_div
-@[deprecated UInt16.toNat_mod (since := "2024-06-23")] protected abbrev UInt16.mod_toNat := @UInt16.toNat_mod
-
-@[deprecated UInt32.toNat_zero (since := "2024-06-23")] protected abbrev UInt32.zero_toNat := @UInt32.toNat_zero
-@[deprecated UInt32.toNat_div (since := "2024-06-23")] protected abbrev UInt32.div_toNat := @UInt32.toNat_div
-@[deprecated UInt32.toNat_mod (since := "2024-06-23")] protected abbrev UInt32.mod_toNat := @UInt32.toNat_mod
-
-@[deprecated UInt64.toNat_zero (since := "2024-06-23")] protected abbrev UInt64.zero_toNat := @UInt64.toNat_zero
-@[deprecated UInt64.toNat_div (since := "2024-06-23")] protected abbrev UInt64.div_toNat := @UInt64.toNat_div
-@[deprecated UInt64.toNat_mod (since := "2024-06-23")] protected abbrev UInt64.mod_toNat := @UInt64.toNat_mod
-
-@[deprecated USize.toNat_zero (since := "2024-06-23")] protected abbrev USize.zero_toNat := @USize.toNat_zero
-@[deprecated USize.toNat_div (since := "2024-06-23")] protected abbrev USize.div_toNat := @USize.toNat_div
-@[deprecated USize.toNat_mod (since := "2024-06-23")] protected abbrev USize.mod_toNat := @USize.toNat_mod