diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean
index 0aa972cd2f27..c6d252c6a57f 100644
--- a/src/Init/Control/Lawful/Basic.lean
+++ b/src/Init/Control/Lawful/Basic.lean
@@ -170,6 +170,7 @@ theorem bind_pure_unit [Monad m] [LawfulMonad m] {x : m PUnit} : (x >>= fun _ =>
 theorem map_congr [Functor m] {x : m α} {f g : α → β} (h : ∀ a, f a = g a) : (f <$> x : m β) = g <$> x := by
   simp [funext h]
 
+@[deprecated seq_eq_bind_map (since := "2025-10-26")]
 theorem seq_eq_bind {α β : Type u} [Monad m] [LawfulMonad m] (mf : m (α → β)) (x : m α) : mf <*> x = mf >>= fun f => f <$> x := by
   rw [bind_map]
 
@@ -256,14 +257,3 @@ instance : LawfulMonad Id := by
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
 
 end Id
-
-/-! # Option -/
-
-instance : LawfulMonad Option := LawfulMonad.mk'
-  (id_map := fun x => by cases x <;> rfl)
-  (pure_bind := fun _ _ => rfl)
-  (bind_assoc := fun x _ _ => by cases x <;> rfl)
-  (bind_pure_comp := fun _ x => by cases x <;> rfl)
-
-instance : LawfulApplicative Option := inferInstance
-instance : LawfulFunctor Option := inferInstance
diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean
index 9a4aa13ed1fc..4c0914e046a8 100644
--- a/src/Init/Control/Lawful/Instances.lean
+++ b/src/Init/Control/Lawful/Instances.lean
@@ -189,12 +189,12 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (OptionT m) where
 
 @[simp] theorem run_seq [Monad m] [LawfulMonad m] (f : OptionT m (α → β)) (x : OptionT m α) :
     (f <*> x).run = Option.elimM f.run (pure none) (fun f => Option.map f <$> x.run) := by
-  simp [seq_eq_bind, Option.elimM, Option.elim]
+  simp [seq_eq_bind_map, Option.elimM, Option.elim]
 
 @[simp] theorem run_seqLeft [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
     (x <* y).run = Option.elimM x.run (pure none)
       (fun x => Option.map (Function.const β x) <$> y.run) := by
-  simp [seqLeft_eq, seq_eq_bind, Option.elimM, OptionT.run_bind]
+  simp [seqLeft_eq, seq_eq_bind_map, Option.elimM, OptionT.run_bind]
 
 @[simp] theorem run_seqRight [Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β) :
     (x *> y).run = Option.elimM x.run (pure none) (Function.const α y.run) := by
@@ -219,7 +219,7 @@ instance : LawfulMonad Option := LawfulMonad.mk'
   (id_map := fun x => by cases x <;> rfl)
   (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun a _ _ => by cases a <;> rfl)
-  (bind_pure_comp := bind_pure_comp)
+  (bind_pure_comp := fun _ x => by cases x <;> rfl)
 
 instance : LawfulApplicative Option := inferInstance
 instance : LawfulFunctor Option := inferInstance
diff --git a/src/Init/Control/Lawful/MonadLift/Lemmas.lean b/src/Init/Control/Lawful/MonadLift/Lemmas.lean
index cd617a3621c6..c0d75cbd5510 100644
--- a/src/Init/Control/Lawful/MonadLift/Lemmas.lean
+++ b/src/Init/Control/Lawful/MonadLift/Lemmas.lean
@@ -23,7 +23,7 @@ theorem monadLift_map [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α
 
 theorem monadLift_seq [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) :
     monadLift (mf <*> ma) = monadLift mf <*> (monadLift ma : n α) := by
-  simp only [seq_eq_bind, monadLift_map, monadLift_bind]
+  simp only [seq_eq_bind_map, monadLift_map, monadLift_bind]
 
 theorem monadLift_seqLeft [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
     monadLift (x <* y) = (monadLift x : n α) <* (monadLift y : n β) := by
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 118056464080..44f9d1d745aa 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1348,8 +1348,12 @@ namespace Subtype
 theorem exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x)
   | ⟨a, h⟩ => ⟨a, h⟩
 
-variable {α : Type u} {p : α → Prop}
+variable {α : Sort u} {p : α → Prop}
 
+protected theorem ext : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+@[deprecated Subtype.ext (since := "2025-10-26")]
 protected theorem eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
@@ -1364,9 +1368,9 @@ instance {α : Type u} {p : α → Prop} [BEq α] [ReflBEq α] : ReflBEq {x : α
   rfl {x} := BEq.refl x.1
 
 instance {α : Type u} {p : α → Prop} [BEq α] [LawfulBEq α] : LawfulBEq {x : α // p x} where
-  eq_of_beq h := Subtype.eq (eq_of_beq h)
+  eq_of_beq h := Subtype.ext (eq_of_beq h)
 
-instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
+instance {α : Sort u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α // p x} :=
   fun ⟨a, h₁⟩ ⟨b, h₂⟩ =>
     if h : a = b then isTrue (by subst h; exact rfl)
     else isFalse (fun h' => Subtype.noConfusion h' (fun h' => absurd h' h))
@@ -1483,20 +1487,24 @@ protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α}
 
 /-! # Universe polymorphic unit -/
 
+theorem PUnit.ext (a b : PUnit) : a = b := by
+  cases a; cases b; exact rfl
+
+@[deprecated PUnit.ext (since := "2025-10-26")]
 theorem PUnit.subsingleton (a b : PUnit) : a = b := by
   cases a; cases b; exact rfl
 
 theorem PUnit.eq_punit (a : PUnit) : a = ⟨⟩ :=
-  PUnit.subsingleton a ⟨⟩
+  PUnit.ext a ⟨⟩
 
 instance : Subsingleton PUnit :=
-  Subsingleton.intro PUnit.subsingleton
+  Subsingleton.intro PUnit.ext
 
 instance : Inhabited PUnit where
   default := ⟨⟩
 
 instance : DecidableEq PUnit :=
-  fun a b => isTrue (PUnit.subsingleton a b)
+  fun a b => isTrue (PUnit.ext a b)
 
 /-! # Setoid -/
 
diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index fb6aabc8f078..e0ba68d36b8d 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -31,7 +31,7 @@ theorem foldlM_toList.aux [Monad m]
   · cases Nat.not_le_of_gt ‹_› (Nat.zero_add _ ▸ H)
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_toList.aux (j := j+1) H]
-    rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
+    rw (occs := [2]) [← List.getElem_cons_drop ‹_›]
     simp
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; simp
 
diff --git a/src/Init/Data/Array/GetLit.lean b/src/Init/Data/Array/GetLit.lean
index 855d4f2d5816..f2d09e9db473 100644
--- a/src/Init/Data/Array/GetLit.lean
+++ b/src/Init/Data/Array/GetLit.lean
@@ -50,6 +50,6 @@ where
   getLit_eq (xs : Array α) (i : Nat) (h₁ : xs.size = n) (h₂ : i < n) : xs.getLit i h₁ h₂ = getElem xs.toList i ((id (α := xs.toList.length = n) h₁) ▸ h₂) :=
     rfl
   go (i : Nat) (hi : i ≤ xs.size) : toListLitAux xs n hsz i hi (xs.toList.drop i) = xs.toList := by
-    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop_succ_eq_drop, *]
+    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop, *]
 
 end Array
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 2a0cdbb390b7..78e8efefc80c 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -265,8 +265,6 @@ theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a
   · rintro ⟨rfl, rfl⟩
     rfl
 
-theorem push_eq_append_singleton {as : Array α} {x : α} : as.push x = as ++ #[x] := rfl
-
 theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) :
     ∃ (ys : Array α) (a : α), xs = ys.push a := by
   rcases xs with ⟨xs⟩
@@ -817,6 +815,11 @@ theorem contains_eq_true_of_mem [BEq α] [ReflBEq α] {a : α} {as : Array α} (
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     elem a xs = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
 
+@[grind =]
+theorem contains_iff_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
+    xs.contains a = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
+
+@[deprecated contains_iff_mem (since := "2025-10-26")]
 theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     xs.contains a = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
 
@@ -1139,7 +1142,7 @@ where
   aux (i bs) :
       mapM.map f xs i bs = (xs.toList.drop i).foldlM (fun bs a => bs.push <$> f a) bs := by
     unfold mapM.map; split
-    · rw [← List.getElem_cons_drop_succ_eq_drop ‹_›]
+    · rw [← List.getElem_cons_drop ‹_›]
       simp only [aux (i + 1), map_eq_pure_bind, List.foldlM_cons, bind_assoc,
         pure_bind]
       rfl
@@ -1853,6 +1856,9 @@ theorem getElem_of_append {xs ys zs : Array α} (eq : xs = ys.push a ++ zs) (h :
 
 theorem push_eq_append {a : α} {as : Array α} : as.push a = as ++ #[a] := rfl
 
+@[deprecated push_eq_append (since := "2025-10-26")]
+theorem push_eq_append_singleton {as : Array α} {x : α} : as.push x = as ++ #[x] := rfl
+
 theorem append_inj {xs₁ xs₂ ys₁ ys₂ : Array α} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) :
     xs₁ = xs₂ ∧ ys₁ = ys₂ := by
   rcases xs₁ with ⟨s₁⟩
@@ -2053,11 +2059,22 @@ theorem append_eq_map_iff {f : α → β} :
   | nil => simp
   | cons as => induction as.toList <;> simp [*]
 
-@[simp] theorem flatten_toArray_map {L : List (List α)} :
+@[simp] theorem flatten_toArray_map_toArray {L : List (List α)} :
     (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
   apply ext'
   simp [Function.comp_def]
 
+@[deprecated flatten_toArray_map_toArray (since := "2025-10-26")]
+theorem flatten_toArray_map {L : List (List α)} :
+    (L.map List.toArray).toArray.flatten = L.flatten.toArray := by
+  simp
+
+@[grind =]
+theorem flatten_map_toArray_toArray {L : List (List α)} :
+    (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
+  simp
+
+@[deprecated flatten_map_toArray_toArray (since := "2025-10-26")]
 theorem flatten_map_toArray {L : List (List α)} :
     (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   simp
@@ -2104,32 +2121,33 @@ theorem forall_mem_flatten {p : α → Prop} {xss : Array (Array α)} :
 
 theorem flatten_eq_flatMap {xss : Array (Array α)} : flatten xss = xss.flatMap id := by
   induction xss using array₂_induction
-  rw [flatten_toArray_map, List.flatten_eq_flatMap]
+  rw [flatten_toArray_map_toArray, List.flatten_eq_flatMap]
   simp [List.flatMap_map]
 
 @[simp, grind _=_] theorem map_flatten {f : α → β} {xss : Array (Array α)} :
     (flatten xss).map f = (map (map f) xss).flatten := by
   induction xss using array₂_induction with
   | of xss =>
-    simp only [flatten_toArray_map, List.map_toArray, List.map_flatten, List.map_map,
+    simp only [flatten_toArray_map_toArray, List.map_toArray, List.map_flatten, List.map_map,
       Function.comp_def]
-    rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+    rw [← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
 
 @[simp, grind =] theorem filterMap_flatten {f : α → Option β} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) :
     filterMap f (flatten xss) 0 stop = flatten (map (filterMap f) xss) := by
   subst w
   induction xss using array₂_induction
-  simp only [flatten_toArray_map, List.size_toArray, List.length_flatten, List.filterMap_toArray',
-    List.filterMap_flatten, List.map_toArray, List.map_map, Function.comp_def]
-  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+  simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
+    List.filterMap_toArray', List.filterMap_flatten, List.map_toArray, List.map_map,
+    Function.comp_def]
+  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
 
 @[simp, grind =] theorem filter_flatten {p : α → Bool} {xss : Array (Array α)} {stop : Nat} (w : stop = xss.flatten.size) :
     filter p (flatten xss) 0 stop = flatten (map (filter p) xss) := by
   subst w
   induction xss using array₂_induction
-  simp only [flatten_toArray_map, List.size_toArray, List.length_flatten, List.filter_toArray',
-    List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]
-  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map]
+  simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
+    List.filter_toArray', List.filter_flatten, List.map_toArray, List.map_map, Function.comp_def]
+  rw [← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
 
 theorem flatten_filter_not_isEmpty {xss : Array (Array α)} :
     flatten (xss.filter fun xs => !xs.isEmpty) = xss.flatten := by
@@ -2152,23 +2170,23 @@ theorem flatten_filter_ne_empty [DecidablePred fun xs : Array α => xs ≠ #[]]
   induction xss using array₂_induction
   rcases xs with ⟨l⟩
   have this : [l.toArray] = [l].map List.toArray := by simp
-  simp only [List.push_toArray, flatten_toArray_map, List.append_toArray]
-  rw [this, ← List.map_append, flatten_toArray_map]
+  simp only [List.push_toArray, flatten_toArray_map_toArray, List.append_toArray]
+  rw [this, ← List.map_append, flatten_toArray_map_toArray]
   simp
 
 theorem flatten_flatten {xss : Array (Array (Array α))} : flatten (flatten xss) = flatten (map flatten xss) := by
   induction xss using array₃_induction with
   | of xss =>
-    rw [flatten_toArray_map]
+    rw [flatten_toArray_map_toArray]
     have : (xss.map (fun xs => xs.map List.toArray)).flatten = xss.flatten.map List.toArray := by
       induction xss with
       | nil => simp
       | cons xs xss ih =>
         simp only [List.map_cons, List.flatten_cons, ih, List.map_append]
-    rw [this, flatten_toArray_map, List.flatten_flatten, ← List.map_toArray, Array.map_map,
+    rw [this, flatten_toArray_map_toArray, List.flatten_flatten, ← List.map_toArray, Array.map_map,
       ← List.map_toArray, map_map, Function.comp_def]
-    simp only [Function.comp_apply, flatten_toArray_map]
-    rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map]
+    simp only [Function.comp_apply, flatten_toArray_map_toArray]
+    rw [List.map_toArray, ← Function.comp_def, ← List.map_map, flatten_toArray_map_toArray]
 
 theorem flatten_eq_push_iff {xss : Array (Array α)} {ys : Array α} {y : α} :
     xss.flatten = ys.push y ↔
@@ -2177,13 +2195,13 @@ theorem flatten_eq_push_iff {xss : Array (Array α)} {ys : Array α} {y : α} :
   induction xss using array₂_induction with
   | of xs =>
     rcases ys with ⟨ys⟩
-    rw [flatten_toArray_map, List.push_toArray, mk.injEq, List.flatten_eq_append_iff]
+    rw [flatten_toArray_map_toArray, List.push_toArray, mk.injEq, List.flatten_eq_append_iff]
     constructor
     · rintro (⟨as, bs, rfl, rfl, h⟩ | ⟨as, bs, c, cs, ds, rfl, rfl, h⟩)
       · rw [List.singleton_eq_flatten_iff] at h
         obtain ⟨xs, ys, rfl, h₁, h₂⟩ := h
         exact ⟨((as ++ xs).map List.toArray).toArray, #[], (ys.map List.toArray).toArray, by simp,
-          by simpa using h₂, by rw [flatten_toArray_map]; simpa⟩
+          by simpa using h₂, by rw [flatten_toArray_map_toArray]; simpa⟩
       · rw [List.singleton_eq_append_iff] at h
         obtain (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩) := h
         · simp at h₁
@@ -2228,10 +2246,6 @@ theorem eq_iff_flatten_eq {xss₁ xss₂ : Array (Array α)} :
       rw [List.map_inj_right]
       simp +contextual
 
-theorem flatten_toArray_map_toArray {xss : List (List α)} :
-    (xss.map List.toArray).toArray.flatten = xss.flatten.toArray := by
-  simp
-
 /-! ### flatMap -/
 
 theorem flatMap_def {xs : Array α} {f : α → Array β} : xs.flatMap f = flatten (map f xs) := by
@@ -2535,8 +2549,8 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i
         split <;> rename_i h₃
         · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
           exact (List.getElem?_reverse' (Eq.trans (by simp +arith) h)).symm
-        simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
-          Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
+        simp only [Nat.succ_le_iff, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃),
+          Nat.lt_succ_iff.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))]
     · rw [H]; split <;> rename_i h₂
       · cases Nat.le_antisymm (Nat.not_lt.1 h₁) (Nat.le_trans h₂.1 h₂.2)
         cases Nat.le_antisymm h₂.1 h₂.2
@@ -2551,7 +2565,7 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i
     split
     · rfl
     · rename_i h
-      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := xs.size - 1), this, Nat.zero_le,
+      simp only [← show k < _ + 1 ↔ _ from Nat.lt_succ_iff (n := xs.size - 1), this, Nat.zero_le,
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (xs.toList.length_reverse ▸ ‹_›)]
 
@@ -2699,8 +2713,8 @@ theorem extract_loop_eq_aux {xs ys : Array α} {size start : Nat} :
   | zero => rw [extract_loop_zero, extract_loop_zero, append_empty]
   | succ size ih =>
     if h : start < xs.size then
-      rw [extract_loop_succ (h := h), ih, push_eq_append_singleton]
-      rw [extract_loop_succ (h := h), ih (ys := #[].push _), push_eq_append_singleton, empty_append]
+      rw [extract_loop_succ (h := h), ih, push_eq_append]
+      rw [extract_loop_succ (h := h), ih (ys := #[].push _), push_eq_append, empty_append]
       rw [append_assoc]
     else
       rw [extract_loop_of_ge (h := Nat.le_of_not_lt h)]
@@ -3622,11 +3636,6 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
 -- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
 grind_pattern contains_iff_exists_mem_beq => xs.contains a
 
-@[grind =]
-theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
-    xs.contains a ↔ a ∈ xs := by
-  simp
-
 @[simp, grind =]
 theorem contains_toList [BEq α] {xs : Array α} {x : α} :
     xs.toList.contains x = xs.contains x := by
@@ -4276,6 +4285,7 @@ theorem getElem_fin_eq_getElem_toList {xs : Array α} {i : Fin xs.size} : xs[i]
 @[simp] theorem ugetElem_eq_getElem {xs : Array α} {i : USize} (h : i.toNat < xs.size) :
   xs[i] = xs[i.toNat] := rfl
 
+@[deprecated getElem?_eq_none (since := "2025-10-26")]
 theorem getElem?_size_le {xs : Array α} {i : Nat} (h : xs.size ≤ i) : xs[i]? = none := by
   simp [getElem?_neg, h]
 
@@ -4295,6 +4305,7 @@ theorem getElem?_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
     (xs.push x)[i]? = some xs[i] := by
   rw [getElem?_pos (xs.push x) i (size_push _ ▸ Nat.lt_succ_of_lt h), getElem_push_lt]
 
+@[deprecated getElem?_push_size (since := "2025-10-26")]
 theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some x := by
   rw [getElem?_pos (xs.push x) xs.size (size_push _ ▸ Nat.lt_succ_self xs.size), getElem_push_eq]
 
@@ -4426,7 +4437,8 @@ theorem uset_toArray {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray
   apply ext'
   simp
 
-@[simp, grind =] theorem flatten_toArray {L : List (List α)} :
+@[deprecated Array.flatten_map_toArray_toArray (since := "2025-10-26")]
+theorem flatten_toArray {L : List (List α)} :
     (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   apply ext'
   simp
diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean
index aab8d6a823a3..fd39fb274dd0 100644
--- a/src/Init/Data/Array/Lex/Lemmas.lean
+++ b/src/Init/Data/Array/Lex/Lemmas.lean
@@ -34,7 +34,18 @@ grind_pattern _root_.List.le_toArray => l₁.toArray ≤ l₂.toArray
 grind_pattern lt_toList => xs.toList < ys.toList
 grind_pattern le_toList => xs.toList ≤ ys.toList
 
+@[simp]
+protected theorem not_lt [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+
+@[deprecated Array.not_lt (since := "2025-10-26")]
 protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+
+@[simp]
+protected theorem not_le [LT α] {xs ys : Array α} :
+    ¬ xs ≤ ys ↔ ys < xs :=
+  Classical.not_not
+
+@[deprecated Array.not_le (since := "2025-10-26")]
 protected theorem not_le_iff_gt [LT α] {xs ys : Array α} :
     ¬ xs ≤ ys ↔ ys < xs :=
   Classical.not_not
@@ -178,12 +189,6 @@ protected theorem le_total [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)] (xs ys : Array α) : xs ≤ ys ∨ ys ≤ xs :=
   List.le_total xs.toList ys.toList
 
-@[simp] protected theorem not_lt [LT α]
-    {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-
-@[simp] protected theorem not_le [LT α]
-    {xs ys : Array α} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
-
 protected theorem le_of_lt [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)]
     {xs ys : Array α} (h : xs < ys) : xs ≤ ys :=
diff --git a/src/Init/Data/Array/Perm.lean b/src/Init/Data/Array/Perm.lean
index 97da16c9b202..3360290a0ee5 100644
--- a/src/Init/Data/Array/Perm.lean
+++ b/src/Init/Data/Array/Perm.lean
@@ -104,7 +104,7 @@ grind_pattern Perm.append => xs ~ ys, as ~ bs, ys ++ bs
 
 theorem Perm.push (x : α) {xs ys : Array α} (p : xs ~ ys) :
     xs.push x ~ ys.push x := by
-  rw [push_eq_append_singleton]
+  rw [push_eq_append]
   exact p.append .rfl
 
 grind_pattern Perm.push => xs ~ ys, xs.push x
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index d5f022dbf8be..41c7497c7a22 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -1025,7 +1025,7 @@ theorem lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) :
     case neg.hrWidth =>
       simp only
       have hdr' : d ≤ (qr.r.shiftConcat (n.getLsbD (qr.wn - 1))) :=
-        BitVec.not_lt_iff_le.mp rltd
+        BitVec.not_lt.mp rltd
       have hr' : ((qr.r.shiftConcat (n.getLsbD (qr.wn - 1)))).toNat < 2 ^ (qr.wr + 1) := by
         apply toNat_shiftConcat_lt_of_lt <;> bv_omega
       rw [BitVec.toNat_sub_of_le hdr']
@@ -1033,7 +1033,7 @@ theorem lawful_divSubtractShift (qr : DivModState w) (h : qr.Poised args) :
     case neg.hqWidth =>
       apply toNat_shiftConcat_lt_of_lt <;> omega
     case neg.hdiv =>
-      have rltd' := (BitVec.not_lt_iff_le.mp rltd)
+      have rltd' := (BitVec.not_lt.mp rltd)
       simp only [qr.toNat_shiftRight_sub_one_eq h,
         BitVec.toNat_sub_of_le rltd',
         toNat_shiftConcat_eq_of_lt (qr.wr_lt_w h) h.hrWidth]
@@ -1407,7 +1407,7 @@ theorem eq_iff_eq_of_inv (f : α → BitVec w) (g : BitVec w → α) (h : ∀ x,
     have := congrArg g h'
     simpa [h] using this
 
-@[simp]
+@[deprecated BitVec.ne_intMin_of_msb_eq_false (since := "2025-10-26")]
 theorem ne_intMin_of_lt_of_msb_false {x : BitVec w} (hw : 0 < w) (hx : x.msb = false) :
     x ≠ intMin w := by
   have := toNat_lt_of_msb_false hx
@@ -1512,7 +1512,7 @@ theorem sdiv_ne_intMin_of_ne_intMin {x y : BitVec w} (h : x ≠ intMin w) :
   by_cases hx : x.msb <;> by_cases hy : y.msb
   <;> simp only [hx, hy, neg_ne_intMin_inj]
   <;> simp only [Bool.not_eq_true] at hx hy
-  <;> apply ne_intMin_of_lt_of_msb_false (by omega)
+  <;> apply ne_intMin_of_msb_eq_false (by omega)
   <;> rw [msb_udiv]
   <;> try simp only [hx, Bool.false_and]
   · simp [h, ne_zero_of_msb_true, hx]
@@ -1624,7 +1624,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
             · have ry := (intMin_udiv_eq_intMin_iff b).mp
               simp only [hb1, imp_false] at ry
               simp [msb_udiv, ha_intMin, hb1, ry, intMin_udiv_ne_zero_of_ne_zero, hb, hb0]
-            · have := @BitVec.ne_intMin_of_lt_of_msb_false w ((-a) / b) wpos (by simp [ha, ha0, ha_intMin])
+            · have := @BitVec.ne_intMin_of_msb_eq_false w wpos ((-a) / b) (by simp [ha, ha0, ha_intMin])
               simp [msb_neg, h', this, ha, ha_intMin]
       rw [toInt_eq_toNat_of_msb hb, toInt_eq_neg_toNat_neg_of_msb_true ha, Int.neg_tdiv,
         Int.tdiv_eq_ediv_of_nonneg (by omega), sdiv_toInt_of_msb_true_of_msb_false]
@@ -1635,7 +1635,7 @@ theorem toInt_sdiv_of_ne_or_ne (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1
         rw [toInt_udiv_of_msb ha, toInt_eq_toNat_of_msb ha]
         rw [toInt_eq_neg_toNat_neg_of_msb_true hb, Int.tdiv_neg, Int.tdiv_eq_ediv_of_nonneg (by omega)]
       · apply sdiv_ne_intMin_of_ne_intMin
-        apply ne_intMin_of_lt_of_msb_false (by omega) ha
+        apply ne_intMin_of_msb_eq_false (by omega) ha
     · rw [sdiv, Int.tdiv_cases, udiv_eq, neg_eq, if_pos (toInt_nonneg_of_msb_false ha),
         if_pos (toInt_nonneg_of_msb_false hb), ha, hb, toInt_udiv_of_msb ha,
         toInt_eq_toNat_of_msb ha, toInt_eq_toNat_of_msb hb]
@@ -1927,7 +1927,7 @@ theorem toInt_sub_neg_umod {x y : BitVec w} (hxmsb : x.msb = true) (hymsb : y.ms
       rw [Int.bmod_eq_of_le (by omega) (by omega)]
       simp only [toInt_eq_toNat_of_msb hymsb, BitVec.toInt_eq_neg_toNat_neg_of_msb_true hxmsb,
         Int.dvd_neg] at hdvd
-      simp only [hdvd, ↓reduceIte, Int.natAbs_cast]
+      simp only [hdvd, ↓reduceIte, Int.natAbs_natCast]
 
 theorem srem_zero_of_dvd {x y : BitVec w} (h : y.toInt ∣ x.toInt) :
     x.srem y = 0#w := by
diff --git a/src/Init/Data/BitVec/Folds.lean b/src/Init/Data/BitVec/Folds.lean
index f9dc9a22a4fd..2c92b04ae740 100644
--- a/src/Init/Data/BitVec/Folds.lean
+++ b/src/Init/Data/BitVec/Folds.lean
@@ -82,7 +82,7 @@ theorem iunfoldr_getLsbD' {f : Fin w → α → α × Bool} (state : Nat → α)
       intro i
       simp only [getLsbD_cons]
       have hj2 : j.val ≤ w := by simp
-      cases (Nat.lt_or_eq_of_le (Nat.lt_succ.mp i.isLt)) with
+      cases (Nat.lt_or_eq_of_le (Nat.lt_succ_iff.mp i.isLt)) with
       | inl h3 => simp [(Nat.ne_of_lt h3)]
                   exact (ih hj2).1 ⟨i.val, h3⟩
       | inr h3 => simp [h3]
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 60366e0fd71f..d396903c1e04 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -132,9 +132,6 @@ theorem two_pow_le_toNat_of_getElem_eq_true {i : Nat} {x : BitVec w}
   rw [← getElem_eq_testBit_toNat x i hi]
   exact hx
 
-@[grind =] theorem msb_eq_getMsbD (x : BitVec w) : x.msb = x.getMsbD 0 := by
-  simp [BitVec.msb]
-
 @[grind =] theorem getMsb_eq_getLsb (x : BitVec w) (i : Fin w) :
     x.getMsb i = x.getLsb ⟨w - 1 - i, by omega⟩ := by
   simp only [getMsb, getLsb]
@@ -518,6 +515,10 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
 @[grind _=_] theorem msb_eq_getMsbD_zero (x : BitVec w) : x.msb = x.getMsbD 0 := by
   cases w <;> simp [getMsbD_eq_getLsbD, msb_eq_getLsbD_last]
 
+@[deprecated msb_eq_getMsbD_zero (since := "2025-10-26")]
+theorem msb_eq_getMsbD (x : BitVec w) : x.msb = x.getMsbD 0 := by
+  simp [BitVec.msb]
+
 /-! ### cast -/
 
 @[simp, grind =] theorem toFin_cast (h : w = v) (x : BitVec w) :
@@ -1182,7 +1183,7 @@ let x' = x.extractLsb' 7 5  =   _ _ 9 8 7
 
 @[simp] theorem getLsbD_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsbD x (lo+i)) := by
-  simp [getLsbD, Nat.lt_succ]
+  simp [getLsbD, Nat.lt_succ_iff]
 
 @[simp] theorem getLsbD_extractLsb {hi lo : Nat} {x : BitVec n} {i : Nat} :
     (extractLsb hi lo x).getLsbD i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i)) := by
@@ -4057,6 +4058,7 @@ protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y :=
   simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod]
   apply Nat.mod_lt
 
+@[deprecated BitVec.not_lt (since := "2025-10-26")]
 theorem not_lt_iff_le {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by
   constructor <;>
     (intro h; simp only [lt_def, Nat.not_lt, le_def] at h ⊢; omega)
@@ -4073,7 +4075,7 @@ theorem not_lt_zero {x : BitVec w} : ¬x < 0#w := of_decide_eq_false rfl
 theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w := by
   constructor
   · intro h
-    have : x ≥ 0 := not_lt_iff_le.mp not_lt_zero
+    have : x ≥ 0 := BitVec.not_lt.mp not_lt_zero
     exact Eq.symm (BitVec.le_antisymm this h)
   · simp_all
 
@@ -4096,7 +4098,7 @@ theorem not_allOnes_lt {x : BitVec w} : ¬allOnes w < x := by
 theorem allOnes_le_iff {x : BitVec w} : allOnes w ≤ x ↔ x = allOnes w := by
   constructor
   · intro h
-    have : x ≤ allOnes w := not_lt_iff_le.mp not_allOnes_lt
+    have : x ≤ allOnes w := BitVec.not_lt.mp not_allOnes_lt
     exact Eq.symm (BitVec.le_antisymm h this)
   · simp_all
 
diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean
index ecc7c6a21e5b..868562d249c4 100644
--- a/src/Init/Data/Char/Lemmas.lean
+++ b/src/Init/Data/Char/Lemmas.lean
@@ -13,12 +13,16 @@ public section
 
 namespace Char
 
-@[ext] protected theorem ext : {a b : Char} → a.val = b.val → a = b
+@[deprecated Char.ext (since := "2025-10-26")]
+protected theorem eq_of_val_eq : {a b : Char} → a.val = b.val → a = b
   | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl
 
 theorem le_def {a b : Char} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
 theorem lt_def {a b : Char} : a < b ↔ a.1 < b.1 := .rfl
+
+@[deprecated lt_def (since := "2025-10-26")]
 theorem lt_iff_val_lt_val {a b : Char} : a < b ↔ a.val < b.val := Iff.rfl
+
 @[simp] protected theorem not_le {a b : Char} : ¬ a ≤ b ↔ b < a := UInt32.not_le
 @[simp] protected theorem not_lt {a b : Char} : ¬ a < b ↔ b ≤ a := UInt32.not_lt
 @[simp] protected theorem le_refl (a : Char) : a ≤ a := by simp [le_def]
diff --git a/src/Init/Data/Dyadic/Basic.lean b/src/Init/Data/Dyadic/Basic.lean
index 0dc70fa775c7..fa897b73b790 100644
--- a/src/Init/Data/Dyadic/Basic.lean
+++ b/src/Init/Data/Dyadic/Basic.lean
@@ -472,7 +472,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
       Rat.den_ofNat, Nat.one_pow, Nat.mul_one]
     split
     · simp_all
-    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
+    · rw [Int.ediv_ediv (Int.natCast_nonneg _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       rw [Int.natCast_dvd_natCast]
@@ -495,7 +495,7 @@ theorem toRat_toDyadic (x : Rat) (prec : Int) :
     simp only [this, Int.mul_one]
     split
     · simp_all
-    · rw [Int.ediv_ediv (Int.ofNat_zero_le _)]
+    · rw [Int.ediv_ediv (Int.natCast_nonneg _)]
       congr 1
       rw [Int.natCast_ediv, Int.mul_ediv_cancel']
       · simp
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 2ae06ac0c12f..d53fca52e83c 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -157,6 +157,7 @@ theorem le_def {a b : Fin n} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
 
 theorem lt_def {a b : Fin n} : a < b ↔ a.1 < b.1 := .rfl
 
+@[deprecated lt_def (since := "2025-10-26")]
 theorem lt_iff_val_lt_val {a b : Fin n} : a < b ↔ a.val < b.val := Iff.rfl
 
 @[simp] protected theorem not_le {a b : Fin n} : ¬ a ≤ b ↔ b < a := Nat.not_le
@@ -264,7 +265,7 @@ instance : LawfulOrderLT (Fin n) where
   rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
 
 @[simp] theorem rev_le_rev {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i := by
-  simp only [le_def, val_rev, Nat.sub_le_sub_iff_left (Nat.succ_le.2 j.is_lt)]
+  simp only [le_def, val_rev, Nat.sub_le_sub_iff_left (Nat.succ_le_iff.2 j.is_lt)]
   exact Nat.succ_le_succ_iff
 
 @[simp] theorem rev_inj {i j : Fin n} : rev i = rev j ↔ i = j :=
@@ -383,9 +384,10 @@ theorem add_one_pos (i : Fin (n + 1)) (h : i < Fin.last n) : (0 : Fin (n + 1)) <
     rw [Fin.lt_def, val_add, val_zero, val_one, Nat.mod_eq_of_lt h]
     exact Nat.zero_lt_succ _
 
+@[deprecated zero_lt_one (since := "2025-10-26")]
 theorem one_pos : (0 : Fin (n + 2)) < 1 := Nat.succ_pos 0
 
-theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt one_pos
+theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt zero_lt_one
 
 /-! ### succ and casts into larger Fin types -/
 
@@ -540,7 +542,7 @@ theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
 
 @[simp] theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
 
-@[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt.step h⟩ := rfl
+@[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt_succ_of_lt h⟩ := rfl
 
 @[simp] theorem cast_castSucc {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
     i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := rfl
@@ -754,7 +756,7 @@ theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w
   | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [Fin.ext_iff]
 
 @[simp] theorem pred_one {n : Nat} :
-    Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
+    Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt zero_lt_one)) = 0 := rfl
 
 theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
     pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
@@ -1137,6 +1139,7 @@ theorem mul_ofNat [NeZero n] (x : Fin n) (y : Nat) :
 theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 
+@[deprecated val_mul (since := "2025-10-26")]
 theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
   | ⟨_, _⟩, ⟨_, _⟩ => rfl
 
diff --git a/src/Init/Data/Int/DivMod/Bootstrap.lean b/src/Init/Data/Int/DivMod/Bootstrap.lean
index 254d65dc9919..9c834f3b4ca8 100644
--- a/src/Init/Data/Int/DivMod/Bootstrap.lean
+++ b/src/Init/Data/Int/DivMod/Bootstrap.lean
@@ -38,7 +38,7 @@ protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
   refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.natCast_mul]⟩⟩
   match Int.le_total a 0 with
   | .inl h =>
-    have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
+    have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (natCast_nonneg _) h
     rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
     apply Nat.dvd_zero
   | .inr h => match a, eq_ofNat_of_zero_le h with
@@ -206,7 +206,7 @@ theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a
 /-! ### emod -/
 
 theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b
-  | ofNat _, _, _ => ofNat_zero_le _
+  | ofNat _, _, _ => natCast_nonneg _
   | -[_+1], _, H => Int.sub_nonneg_of_le <| ofNat_le.2 <| Nat.mod_lt _ (natAbs_pos.2 H)
 
 theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
diff --git a/src/Init/Data/Int/DivMod/Lemmas.lean b/src/Init/Data/Int/DivMod/Lemmas.lean
index 5c8901e2b4f7..5b8e35ba47e7 100644
--- a/src/Init/Data/Int/DivMod/Lemmas.lean
+++ b/src/Init/Data/Int/DivMod/Lemmas.lean
@@ -73,7 +73,7 @@ protected theorem dvd_iff_dvd_of_dvd_add {a b c : Int} (H : a ∣ b + c) : a ∣
 theorem le_of_dvd {a b : Int} (bpos : 0 < b) (H : a ∣ b) : a ≤ b :=
   match a, b, eq_succ_of_zero_lt bpos, H with
   | ofNat _, _, ⟨n, rfl⟩, H => ofNat_le.2 <| Nat.le_of_dvd n.succ_pos <| ofNat_dvd.1 H
-  | -[_+1], _, ⟨_, rfl⟩, _ => Int.le_trans (Int.le_of_lt <| negSucc_lt_zero _) (ofNat_zero_le _)
+  | -[_+1], _, ⟨_, rfl⟩, _ => Int.le_trans (Int.le_of_lt <| negSucc_lt_zero _) (natCast_nonneg _)
 
 theorem natAbs_dvd {a b : Int} : (a.natAbs : Int) ∣ b ↔ a ∣ b :=
   match natAbs_eq a with
@@ -215,7 +215,7 @@ theorem tdiv_eq_ediv {a b : Int} :
   | -[a+1], 0 => simp
   | -[a+1], ofNat (succ b) =>
     simp only [tdiv, Nat.succ_eq_add_one, ofNat_eq_coe, Int.natCast_add, cast_ofNat_Int,
-      negSucc_not_nonneg, sign_of_add_one]
+      negSucc_not_nonneg, sign_natCast_add_one]
     simp only [negSucc_emod_ofNat_succ_eq_zero_iff]
     norm_cast
     simp only [Nat.succ_eq_add_one, false_or]
@@ -516,23 +516,23 @@ theorem negSucc_ediv (m : Nat) {b : Int} (H : 0 < b) : -[m+1] / b = -(ediv m b +
 
 theorem ediv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a / b :=
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_zero_le _
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => natCast_nonneg _
 
 theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b := by
   match a, b with
   | ofNat a, b =>
-    match Int.le_antisymm Ha (ofNat_zero_le a) with
+    match Int.le_antisymm Ha (natCast_nonneg a) with
     | h1 =>
       rw [h1, zero_ediv]
       exact Int.le_refl 0
   | a, ofNat b =>
-    match Int.le_antisymm Hb (ofNat_zero_le  b) with
+    match Int.le_antisymm Hb (natCast_nonneg  b) with
     | h1 =>
       rw [h1, Int.ediv_zero]
       exact Int.le_refl 0
   | negSucc a, negSucc b =>
     rw [Int.div_def, ediv]
-    exact le_add_one (ediv_nonneg (ofNat_zero_le a) (Int.le_trans (ofNat_zero_le b) (le.intro 1 rfl)))
+    exact le_add_one (ediv_nonneg (natCast_nonneg a) (Int.le_trans (natCast_nonneg b) (le.intro 1 rfl)))
 
 theorem ediv_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a / b := by
   rw [Int.div_def]
@@ -646,7 +646,7 @@ theorem sign_ediv (a b : Int) : sign (a / b) = if 0 ≤ a ∧ a < b.natAbs then
       | (a + 1 : Nat) =>
         norm_cast
         simp only [Nat.le_add_left, Nat.add_lt_add_iff_right, true_and, Int.natCast_add,
-          cast_ofNat_Int, sign_of_add_one, Int.mul_one]
+          cast_ofNat_Int, sign_natCast_add_one, Int.mul_one]
         split
         · rw [Nat.div_eq_of_lt (by omega)]
           simp
@@ -1063,7 +1063,7 @@ theorem emod_natAbs_of_neg {x : Int} (h : x < 0) {n : Nat} (w : n ≠ 0) :
   match x, h with
   | -(x + 1 : Nat), _ =>
     rw [Int.natAbs_neg]
-    rw [Int.natAbs_cast]
+    rw [Int.natAbs_natCast]
     rw [Int.neg_emod]
     simp only [Int.dvd_neg]
     simp only [Int.natCast_dvd_natCast]
@@ -1271,7 +1271,7 @@ because these statements are all incorrect, and require awkward conditional off-
 
 protected theorem tdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.tdiv b :=
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_zero_le _
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => natCast_nonneg _
 
 theorem tdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a.tdiv b := by
   rw [tdiv_eq_ediv]
@@ -1972,7 +1972,7 @@ theorem add_fdiv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b).fdiv c = a.fd
 
 theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :=
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ natCast_nonneg _
 
 theorem fdiv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a.fdiv b := by
   rw [fdiv_eq_ediv]
@@ -2021,8 +2021,8 @@ protected theorem fdiv_eq_of_eq_mul_right {a b c : Int}
     (H1 : b ≠ 0) (H2 : a = b * c) : a.fdiv b = c := by rw [H2, Int.mul_fdiv_cancel_left _ H1]
 
 protected theorem eq_fdiv_of_mul_eq_right {a b c : Int}
-    (H1 : a ≠ 0) (H2 : a * b = c) : b = c.tdiv a :=
-  (Int.tdiv_eq_of_eq_mul_right H1 H2.symm).symm
+    (H1 : a ≠ 0) (H2 : a * b = c) : b = c.fdiv a :=
+  (Int.fdiv_eq_of_eq_mul_right H1 H2.symm).symm
 
 protected theorem fdiv_eq_of_eq_mul_left {a b c : Int}
     (H1 : b ≠ 0) (H2 : a = c * b) : a.fdiv b = c :=
@@ -2904,7 +2904,7 @@ theorem ediv_nonneg_of_nonneg_of_nonneg {x y : Int} (hx : 0 ≤ x) (hy : 0 ≤ y
   obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega)
   obtain ⟨yn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := y) (by omega)
   rw [← Int.natCast_ediv]
-  exact Int.ofNat_zero_le (xn / yn)
+  exact natCast_nonneg (xn / yn)
 
 /--  When both x and y are negative we need stricter bounds on x and y
   to establish the upper bound of x/y, i.e., x / y < x.natAbs.
diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index 6e3548f6f43c..eb4b79b5afb0 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -600,6 +600,4 @@ protected theorem natCast_zero : ((0 : Nat) : Int) = (0 : Int) := rfl
 
 protected theorem natCast_one : ((1 : Nat) : Int) = (1 : Int) := rfl
 
-@[simp, norm_cast] theorem natAbs_cast (n : Nat) : natAbs ↑n = n := rfl
-
 end Int
diff --git a/src/Init/Data/Int/LemmasAux.lean b/src/Init/Data/Int/LemmasAux.lean
index a4273a288f25..2417bc3c65a1 100644
--- a/src/Init/Data/Int/LemmasAux.lean
+++ b/src/Init/Data/Int/LemmasAux.lean
@@ -27,22 +27,24 @@ namespace Int
   natCast_nonneg _
 
 @[simp] theorem neg_natCast_le_natCast (n m : Nat) : -(n : Int) ≤ (m : Int) :=
-  Int.le_trans (by simp) (ofNat_zero_le m)
+  Int.le_trans (by simp) (natCast_nonneg m)
 
 @[simp] theorem neg_natCast_le_ofNat (n m : Nat) : -(n : Int) ≤ (no_index (OfNat.ofNat m)) :=
-  Int.le_trans (by simp) (ofNat_zero_le m)
+  Int.le_trans (by simp) (natCast_nonneg m)
 
 @[simp] theorem neg_ofNat_le_ofNat (n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (no_index (OfNat.ofNat m)) :=
-  Int.le_trans (by simp) (ofNat_zero_le m)
+  Int.le_trans (by simp) (natCast_nonneg m)
 
 @[simp] theorem neg_ofNat_le_natCast (n m : Nat) : -(no_index (OfNat.ofNat n)) ≤ (m : Int) :=
-  Int.le_trans (by simp) (ofNat_zero_le m)
+  Int.le_trans (by simp) (natCast_nonneg m)
 
 theorem neg_lt_self_iff {n : Int} : -n < n ↔ 0 < n := by
   omega
 
+@[deprecated ofNat_add_ofNat (since := "2025-10-26")]
 protected theorem ofNat_add_out (m n : Nat) : ↑m + ↑n = (↑(m + n) : Int) := rfl
 
+@[deprecated ofNat_mul_ofNat (since := "2025-10-26")]
 protected theorem ofNat_mul_out (m n : Nat) : ↑m * ↑n = (↑(m * n) : Int) := rfl
 
 protected theorem ofNat_add_one_out (n : Nat) : ↑n + (1 : Int) = ↑(Nat.succ n) := rfl
@@ -62,8 +64,6 @@ theorem natCast_succ_pos (n : Nat) : 0 < (n.succ : Int) := natCast_pos.2 n.succ_
 
 @[simp high] theorem natCast_nonpos_iff {n : Nat} : (n : Int) ≤ 0 ↔ n = 0 := by omega
 
-@[simp] theorem sign_natCast_add_one (n : Nat) : sign (n + 1) = 1 := rfl
-
 @[simp, norm_cast] theorem cast_id {n : Int} : Int.cast n = n := rfl
 
 @[simp] theorem ble'_eq_true (a b : Int) : (Int.ble' a b = true) = (a ≤ b) := by
diff --git a/src/Init/Data/Int/Order.lean b/src/Init/Data/Int/Order.lean
index 5e8e75f2483d..f2ce2e47d9ab 100644
--- a/src/Init/Data/Int/Order.lean
+++ b/src/Init/Data/Int/Order.lean
@@ -62,8 +62,6 @@ protected theorem le_total (a b : Int) : a ≤ b ∨ b ≤ a :=
     let ⟨k, (hk : m + k = n)⟩ := Nat.le.dest h
     le.intro k (by rw [← hk]; rfl)⟩
 
-@[simp] theorem ofNat_zero_le (n : Nat) : 0 ≤ (↑n : Int) := ofNat_le.2 n.zero_le
-
 theorem eq_ofNat_of_zero_le {a : Int} (h : 0 ≤ a) : ∃ n : Nat, a = n := by
   have t := le.dest_sub h; rwa [Int.sub_zero] at t
 
@@ -88,8 +86,12 @@ theorem lt.dest {a b : Int} (h : a < b) : ∃ n : Nat, a + Nat.succ n = b :=
 @[deprecated natCast_pos (since := "2025-05-13"), simp high]
 theorem ofNat_pos {n : Nat} : 0 < (↑n : Int) ↔ 0 < n := ofNat_lt
 
+@[simp]
 theorem natCast_nonneg (n : Nat) : 0 ≤ (n : Int) := ⟨_⟩
 
+@[deprecated natCast_nonneg (since := "2025-10-26")]
+theorem ofNat_zero_le (n : Nat) : 0 ≤ (↑n : Int) := ofNat_le.2 n.zero_le
+
 @[deprecated natCast_nonneg (since := "2025-05-13")]
 theorem ofNat_nonneg (n : Nat) : 0 ≤ (n : Int) := ⟨_⟩
 
@@ -237,7 +239,7 @@ theorem eq_natAbs_of_nonneg {a : Int} (h : 0 ≤ a) : a = natAbs a := by
 theorem le_natAbs {a : Int} : a ≤ natAbs a :=
   match Int.le_total 0 a with
   | .inl h => by rw [eq_natAbs_of_nonneg h]; apply Int.le_refl
-  | .inr h => Int.le_trans h (ofNat_zero_le _)
+  | .inr h => Int.le_trans h (natCast_nonneg _)
 
 @[simp] theorem negSucc_lt_zero (n : Nat) : -[n+1] < 0 :=
   Int.not_le.1 fun h => let ⟨_, h⟩ := eq_ofNat_of_zero_le h; nomatch h
@@ -465,10 +467,10 @@ protected theorem max_lt {a b c : Int} : max a b < c ↔ a < c ∧ b < c := by
   simpa using Int.max_le (a := a + 1) (b := b + 1) (c := c)
 
 @[simp] theorem ofNat_max_zero (n : Nat) : (max (n : Int) 0) = n := by
-  rw [Int.max_eq_left (ofNat_zero_le n)]
+  rw [Int.max_eq_left (natCast_nonneg n)]
 
 @[simp] theorem zero_max_ofNat (n : Nat) : (max 0 (n : Int)) = n := by
-  rw [Int.max_eq_right (ofNat_zero_le n)]
+  rw [Int.max_eq_right (natCast_nonneg n)]
 
 @[simp] theorem negSucc_max_zero (n : Nat) : (max (Int.negSucc n) 0) = 0 := by
   rw [Int.max_eq_right (negSucc_le_zero _)]
@@ -551,6 +553,9 @@ protected theorem mul_le_mul_of_nonpos_left {a b c : Int}
 
 @[simp, norm_cast] theorem natAbs_natCast (n : Nat) : natAbs ↑n = n := rfl
 
+@[deprecated natAbs_natCast (since := "2025-10-26")]
+theorem natAbs_cast (n : Nat) : natAbs ↑n = n := rfl
+
 /-
 TODO: rename `natAbs_ofNat'` to `natAbs_ofNat` once the current deprecated alias
 `natAbs_ofNat := natAbs_natCast` is removed
@@ -628,7 +633,7 @@ theorem eq_zero_of_dvd_of_natAbs_lt_natAbs {d n : Int} (h : d ∣ n) (h₁ : n.n
 /-! ### toNat -/
 
 theorem toNat_eq_max : ∀ a : Int, (toNat a : Int) = max a 0
-  | (n : Nat) => (Int.max_eq_left (ofNat_zero_le n)).symm
+  | (n : Nat) => (Int.max_eq_left (natCast_nonneg n)).symm
   | -[n+1] => (Int.max_eq_right (Int.le_of_lt (negSucc_lt_zero n))).symm
 
 @[simp] theorem toNat_zero : (0 : Int).toNat = 0 := rfl
@@ -713,7 +718,7 @@ protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_t
   simp only [Int.not_lt, iff_false]; constructor
 
 theorem eq_negSucc_of_lt_zero : ∀ {a : Int}, a < 0 → ∃ n : Nat, a = -[n+1]
-  | ofNat _, h => absurd h (Int.not_lt.2 (ofNat_zero_le _))
+  | ofNat _, h => absurd h (Int.not_lt.2 (natCast_nonneg _))
   | -[n+1],  _ => ⟨n, rfl⟩
 
 protected theorem lt_of_add_lt_add_left {a b c : Int} (h : a + b < a + c) : b < c := by
@@ -781,10 +786,10 @@ theorem add_one_le_iff {a b : Int} : a + 1 ≤ b ↔ a < b := .rfl
 theorem lt_add_one_iff {a b : Int} : a < b + 1 ↔ a ≤ b := Int.add_le_add_iff_right _
 
 @[simp] theorem succ_ofNat_pos (n : Nat) : 0 < (n : Int) + 1 :=
-  lt_add_one_iff.mpr (ofNat_zero_le _)
+  lt_add_one_iff.mpr (natCast_nonneg _)
 
 theorem not_ofNat_neg (n : Nat) : ¬((n : Int) < 0) :=
-  Int.not_lt.mpr (ofNat_zero_le ..)
+  Int.not_lt.mpr (natCast_nonneg ..)
 
 theorem le_add_one {a b : Int} (h : a ≤ b) : a ≤ b + 1 :=
   Int.le_of_lt (Int.lt_add_one_iff.2 h)
@@ -1235,7 +1240,11 @@ protected theorem neg_of_mul_pos_right {a b : Int}
 @[simp] theorem sign_one : sign 1 = 1 := rfl
 theorem sign_neg_one : sign (-1) = -1 := rfl
 
-@[simp] theorem sign_of_add_one (x : Nat) : Int.sign (x + 1) = 1 := rfl
+@[simp] theorem sign_natCast_add_one (n : Nat) : sign (n + 1) = 1 := rfl
+
+@[deprecated sign_natCast_add_one (since := "2025-10-26")]
+theorem sign_of_add_one (x : Nat) : Int.sign (x + 1) = 1 := rfl
+
 @[simp] theorem sign_negSucc (x : Nat) : Int.sign (Int.negSucc x) = -1 := rfl
 
 theorem natAbs_sign (z : Int) : z.sign.natAbs = if z = 0 then 0 else 1 :=
@@ -1246,7 +1255,7 @@ theorem natAbs_sign_of_ne_zero {z : Int} (hz : z ≠ 0) : z.sign.natAbs = 1 := b
 
 theorem sign_natCast_of_ne_zero {n : Nat} (hn : n ≠ 0) : Int.sign n = 1 :=
   match n, Nat.exists_eq_succ_of_ne_zero hn with
-  | _, ⟨n, rfl⟩ => Int.sign_of_add_one n
+  | _, ⟨n, rfl⟩ => Int.sign_natCast_add_one n
 
 @[simp] theorem sign_neg (z : Int) : Int.sign (-z) = -Int.sign z := by
   match z with | 0 | succ _ | -[_+1] => rfl
diff --git a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean
index 50dce25b0922..aa1be20a8ced 100644
--- a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean
+++ b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean
@@ -55,7 +55,7 @@ theorem LawfulMonadLiftFunction.lift_map [LawfulMonad m] [LawfulMonad n]
 theorem LawfulMonadLiftFunction.lift_seq [LawfulMonad m] [LawfulMonad n]
     [LawfulMonadLiftFunction lift] (mf : m (α → β)) (ma : m α) :
     lift (mf <*> ma) = lift mf <*> (lift ma : n α) := by
-  simp only [seq_eq_bind, lift_map, lift_bind]
+  simp only [seq_eq_bind_map, lift_map, lift_bind]
 
 theorem LawfulMonadLiftFunction.lift_seqLeft [LawfulMonad m] [LawfulMonad n]
     [LawfulMonadLiftFunction lift] (x : m α) (y : m β) :
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 173eefa9a198..79b25c463eae 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -901,7 +901,8 @@ def take : (n : Nat) → (xs : List α) → List α
 
 @[simp, grind =] theorem take_nil {i : Nat} : ([] : List α).take i = [] := by cases i <;> rfl
 @[simp, grind =] theorem take_zero {l : List α} : l.take 0 = [] := rfl
-@[simp, grind =] theorem take_succ_cons {a : α} {as : List α} {i : Nat} : (a::as).take (i+1) = a :: as.take i := rfl
+@[simp, grind =] theorem take_succ_cons {a : α} {as : List α} {i : Nat} :
+    (a::as).take (i+1) = a :: as.take i := rfl
 
 /-! ### drop -/
 
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 055957633839..f3f190c2344b 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -499,6 +499,11 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
     elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
 
+@[grind =]
+theorem contains_iff_mem [BEq α] [LawfulBEq α] {a : α} {as : List α} :
+    as.contains a ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
+
+@[deprecated contains_iff_mem (since := "2025-10-26")]
 theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
     as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
 
@@ -830,6 +835,7 @@ theorem getElem_cons_length {x : α} {xs : List α} {i : Nat} (h : i = xs.length
 @[simp] theorem getLast?_singleton {a : α} : getLast? [a] = some a := rfl
 
 -- The `l : List α` argument is intentionally explicit.
+@[deprecated getLast?_eq_some_getLast (since := "2025-10-26")]
 theorem getLast?_eq_getLast : ∀ {l : List α} h, l.getLast? = some (l.getLast h)
   | [], h => nomatch h rfl
   | _ :: _, _ => rfl
@@ -837,11 +843,11 @@ theorem getLast?_eq_getLast : ∀ {l : List α} h, l.getLast? = some (l.getLast
 @[grind =] theorem getLast?_eq_getElem? : ∀ {l : List α}, l.getLast? = l[l.length - 1]?
   | [] => rfl
   | a::l => by
-    rw [getLast?_eq_getLast (l := a :: l) nofun, getLast_eq_getElem, getElem?_eq_getElem]
+    rw [getLast?_eq_some_getLast (l := a :: l) nofun, getLast_eq_getElem, getElem?_eq_getElem]
 
 theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
     xs.getLast h = a ↔ xs.getLast? = some a := by
-  rw [getLast?_eq_getLast h]
+  rw [getLast?_eq_some_getLast h]
   simp
 
 -- `getLast?_eq_none_iff`, `getLast?_eq_some_iff`, `getLast?_isSome`, and `getLast_mem`
@@ -868,7 +874,7 @@ theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
 @[simp] theorem getLast!_eq_getLast?_getD [Inhabited α] {l : List α} : getLast! l = (getLast? l).getD default := by
   cases l with
   | nil => simp [getLast!_nil]
-  | cons _ _ => simp [getLast!, getLast?_eq_getLast]
+  | cons _ _ => simp [getLast!, getLast?_eq_some_getLast]
 
 theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
   | _ :: _, rfl => rfl
@@ -892,9 +898,6 @@ set_option linter.unusedVariables false in -- See https://github.com/leanprover/
 theorem head!_of_head? [Inhabited α] : ∀ {l : List α}, head? l = some a → head! l = a
   | _ :: _, rfl => rfl
 
-theorem head?_eq_head : ∀ {l : List α} h, l.head? = some (head l h)
-  | _ :: _, _ => rfl
-
 theorem head?_eq_getElem? : ∀ {l : List α}, l.head? = l[0]?
   | [] => rfl
   | a :: l => by simp
@@ -943,6 +946,10 @@ theorem head_mem_head? : ∀ {l : List α} (h : l ≠ []), head l h ∈ head? l
 theorem head?_eq_some_head : ∀ {l : List α} (h : l ≠ []), head? l = some (head l h)
   | _ :: _, _ => rfl
 
+@[deprecated head?_eq_some_head (since := "2025-10-26")]
+theorem head?_eq_head : ∀ {l : List α} h, l.head? = some (head l h)
+  | _ :: _, _ => rfl
+
 theorem head?_concat {a : α} : (l ++ [a]).head? = some (l.head?.getD a) := by
   cases l <;> simp
 
@@ -1205,7 +1212,7 @@ theorem tailD_map {f : α → β} {l l' : List α} :
 @[simp, grind _=_] theorem getLast?_map {f : α → β} {l : List α} : (map f l).getLast? = l.getLast?.map f := by
   cases l
   · simp
-  · rw [getLast?_eq_getLast, getLast?_eq_getLast, getLast_map] <;> simp
+  · rw [getLast?_eq_some_getLast, getLast?_eq_some_getLast, getLast_map] <;> simp
 
 theorem getLastD_map {f : α → β} {l : List α} {a : α} : (map f l).getLastD (f a) = f (l.getLastD a) := by
   simp
@@ -1254,7 +1261,7 @@ theorem length_filter_eq_length_iff {l} : (filter p l).length = l.length ↔ ∀
     simp only [filter_cons, length_cons, mem_cons, forall_eq_or_imp]
     split <;> rename_i h
     · simp_all [Nat.add_one_inj] -- Why does the simproc not fire here?
-    · have := Nat.ne_of_lt (Nat.lt_succ.mpr (length_filter_le p l))
+    · have := Nat.ne_of_lt (Nat.lt_succ_iff.mpr (length_filter_le p l))
       simp_all
 
 @[simp, grind =] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
@@ -1409,7 +1416,7 @@ theorem filterMap_length_eq_length {l} :
   | cons a l ih =>
     simp only [filterMap_cons, length_cons, mem_cons, forall_eq_or_imp]
     split <;> rename_i h
-    · have := Nat.ne_of_lt (Nat.lt_succ.mpr (length_filterMap_le f l))
+    · have := Nat.ne_of_lt (Nat.lt_succ_iff.mpr (length_filterMap_le f l))
       simp_all
     · simp_all [Nat.add_one_inj] -- Why does the simproc not fire here?
 
@@ -1572,7 +1579,7 @@ theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {i : Nat}, l₁.length
 | [], _, _, _ => rfl
 | a :: l, _, i+1, h₁ => by
   rw [cons_append]
-  simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)]
+  simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ_iff.1 h₁)]
 
 @[grind =] theorem getElem?_append {l₁ l₂ : List α} {i : Nat} :
     (l₁ ++ l₂)[i]? = if i < l₁.length then l₁[i]? else l₂[i - l₁.length]? := by
@@ -2918,11 +2925,6 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
 -- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
 grind_pattern contains_iff_exists_mem_beq => l.contains a
 
-@[grind =]
-theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
-    l.contains a ↔ a ∈ l := by
-  simp
-
 @[simp, grind =]
 theorem contains_map [BEq β] {l : List α} {x : β} {f : α → β} :
     (l.map f).contains x = l.any (fun a => x == f a) := by
@@ -3324,7 +3326,7 @@ theorem head_replace {l : List α} {a b : α} (w) :
       else
         l.head  (by rintro rfl; simp_all) := by
   apply Option.some.inj
-  rw [← head?_eq_head, head?_replace, head?_eq_head]
+  rw [← head?_eq_some_head, head?_replace, head?_eq_some_head]
 
 @[grind =] theorem replace_append [LawfulBEq α] {l₁ l₂ : List α} :
     (l₁ ++ l₂).replace a b = if a ∈ l₁ then l₁.replace a b ++ l₂ else l₁ ++ l₂.replace a b := by
@@ -3470,13 +3472,13 @@ theorem head?_insert {l : List α} {a : α} :
     (l.insert a).head? = some (if h : a ∈ l then l.head (ne_nil_of_mem h) else a) := by
   simp only [insert_eq]
   split <;> rename_i h
-  · simp [head?_eq_head (ne_nil_of_mem h)]
+  · simp [head?_eq_some_head (ne_nil_of_mem h)]
   · rfl
 
 theorem head_insert {l : List α} {a : α} (w) :
     (l.insert a).head w = if h : a ∈ l then l.head (ne_nil_of_mem h) else a := by
   apply Option.some.inj
-  rw [← head?_eq_head, head?_insert]
+  rw [← head?_eq_some_head, head?_insert]
 
 @[grind =] theorem insert_append {l₁ l₂ : List α} {a : α} :
     (l₁ ++ l₂).insert a = if a ∈ l₂ then l₁ ++ l₂ else l₁.insert a ++ l₂ := by
diff --git a/src/Init/Data/List/Lex.lean b/src/Init/Data/List/Lex.lean
index a18c6d1d5a8e..28bb449a733c 100644
--- a/src/Init/Data/List/Lex.lean
+++ b/src/Init/Data/List/Lex.lean
@@ -28,7 +28,18 @@ instance [LT α] [Std.Asymm (α := List α) (· < ·)] : LawfulOrderLT (List α)
 @[simp] theorem lex_lt [LT α] {l₁ l₂ : List α} : Lex (· < ·) l₁ l₂ ↔ l₁ < l₂ := Iff.rfl
 @[simp] theorem not_lex_lt [LT α] {l₁ l₂ : List α} : ¬ Lex (· < ·) l₁ l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 
+@[simp]
+protected theorem not_lt [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+
+@[deprecated List.not_lt (since := "2025-10-26")]
 protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
+
+@[simp]
+protected theorem not_le [LT α] {l₁ l₂ : List α} :
+    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
+  Classical.not_not
+
+@[deprecated List.not_le (since := "2025-10-26")]
 protected theorem not_le_iff_gt [LT α] {l₁ l₂ : List α} :
     ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
   Classical.not_not
@@ -277,12 +288,6 @@ instance [LT α] [Std.Asymm (· < · : α → α → Prop)] :
 instance instIsLinearOrder [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α] :
     IsLinearOrder (List α) := IsLinearOrder.of_le
 
-@[simp] protected theorem not_lt [LT α]
-    {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
-
-@[simp] protected theorem not_le [LT α]
-    {l₁ l₂ : List α} : ¬ l₂ ≤ l₁ ↔ l₁ < l₂ := Classical.not_not
-
 protected theorem le_of_lt [LT α]
     [i : Std.Asymm (· < · : α → α → Prop)]
     {l₁ l₂ : List α} (h : l₁ < l₂) : l₁ ≤ l₂ := by
diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean
index 3d2ada3a405f..8c406d192cb8 100644
--- a/src/Init/Data/List/MapIdx.lean
+++ b/src/Init/Data/List/MapIdx.lean
@@ -501,7 +501,7 @@ theorem mapIdx_eq_mapIdx_iff {l : List α} :
     (mapIdx f l).getLast? = (getLast? l).map (f (l.length - 1)) := by
   cases l
   · simp
-  · rw [getLast?_eq_getLast, getLast?_eq_getLast, getLast_mapIdx] <;> simp
+  · rw [getLast?_eq_some_getLast, getLast?_eq_some_getLast, getLast_mapIdx] <;> simp
 
 @[simp, grind =] theorem mapIdx_mapIdx {l : List α} {f : Nat → α → β} {g : Nat → β → γ} :
     (l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i) := by
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 8e957cc08f2f..987d90bdc846 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -71,7 +71,7 @@ theorem head?_take {l : List α} {i : Nat} :
 theorem head_take {l : List α} {i : Nat} (h : l.take i ≠ []) :
     (l.take i).head h = l.head (by simp_all) := by
   apply Option.some_inj.1
-  rw [← head?_eq_head, ← head?_eq_head, head?_take, if_neg]
+  rw [← head?_eq_some_head, ← head?_eq_some_head, head?_take, if_neg]
   simp_all
 
 theorem getLast?_take {l : List α} : (l.take i).getLast? = if i = 0 then none else l[i - 1]?.or l.getLast? := by
@@ -290,7 +290,7 @@ theorem getLast?_drop {l : List α} : (l.drop i).getLast? = if l.length ≤ i th
     (l.drop i).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega)) := by
   simp only [ne_eq, drop_eq_nil_iff] at h
   apply Option.some_inj.1
-  simp only [← getLast?_eq_getLast, getLast?_drop, ite_eq_right_iff]
+  simp only [← getLast?_eq_some_getLast, getLast?_drop, ite_eq_right_iff]
   omega
 
 theorem drop_length_cons {l : List α} (h : l ≠ []) (a : α) :
@@ -436,10 +436,6 @@ theorem reverse_drop {l : List α} {i : Nat} :
     rw [w, take_zero, drop_of_length_le, reverse_nil]
     omega
 
-theorem take_add_one {l : List α} {i : Nat} :
-    l.take (i + 1) = l.take i ++ l[i]?.toList := by
-  simp [take_add, take_one]
-
 theorem drop_eq_getElem?_toList_append {l : List α} {i : Nat} :
     l.drop i = l[i]?.toList ++ l.drop (i + 1) := by
   induction l generalizing i with
diff --git a/src/Init/Data/List/Range.lean b/src/Init/Data/List/Range.lean
index d73ccda87689..dcfcaaf52be4 100644
--- a/src/Init/Data/List/Range.lean
+++ b/src/Init/Data/List/Range.lean
@@ -70,8 +70,8 @@ theorem mem_range' : ∀ {n}, m ∈ range' s n step ↔ ∃ i < n, m = s + step
   | 0 => by simp [range', Nat.not_lt_zero]
   | n + 1 => by
     have h (i) : i ≤ n ↔ i = 0 ∨ ∃ j, i = succ j ∧ j < n := by
-      cases i <;> simp [Nat.succ_le, Nat.succ_inj]
-    simp [range', mem_range', Nat.lt_succ, h]; simp only [← exists_and_right, and_assoc]
+      cases i <;> simp [Nat.succ_le_iff, Nat.succ_inj]
+    simp [range', mem_range', Nat.lt_succ_iff, h]; simp only [← exists_and_right, and_assoc]
     rw [exists_comm]; simp [Nat.mul_succ, Nat.add_assoc, Nat.add_comm]
 
 theorem getElem?_range' {s step} :
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index bb565cb6c580..8ff5a9295f5c 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -72,12 +72,6 @@ theorem lt_length_of_take_ne_self {l : List α} {i} (h : l.take i ≠ l) : i < l
 
 @[simp, grind =] theorem take_length {l : List α} : l.take l.length = l := take_of_length_le (Nat.le_refl _)
 
-@[simp]
-theorem getElem_cons_drop : ∀ {l : List α} {i : Nat} (h : i < l.length),
-    l[i] :: drop (i + 1) l = drop i l
-  | _::_, 0, _ => rfl
-  | _::_, _+1, h => getElem_cons_drop (Nat.add_one_lt_add_one_iff.mp h)
-
 theorem drop_eq_getElem_cons {i} {l : List α} (h : i < l.length) : drop i l = l[i] :: drop (i + 1) l :=
   (getElem_cons_drop h).symm
 
@@ -186,7 +180,7 @@ theorem set_drop {l : List α} {i j : Nat} {a : α} :
 theorem take_concat_get {l : List α} {i : Nat} (h : i < l.length) :
     (l.take i).concat l[i] = l.take (i+1) :=
   Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by
-    rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop]
+    rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop, take_append_drop]
 
 @[simp] theorem take_append_getElem {l : List α} {i : Nat} (h : i < l.length) :
     (l.take i) ++ [l[i]] = l.take (i+1) := by
@@ -227,7 +221,7 @@ theorem take_left : ∀ {l₁ l₂ : List α}, take (length l₁) (l₁ ++ l₂)
 theorem take_left' {l₁ l₂ : List α} {i} (h : length l₁ = i) : take i (l₁ ++ l₂) = l₁ := by
   rw [← h]; apply take_left
 
-theorem take_succ {l : List α} {i : Nat} : l.take (i + 1) = l.take i ++ l[i]?.toList := by
+theorem take_add_one {l : List α} {i : Nat} : l.take (i + 1) = l.take i ++ l[i]?.toList := by
   induction l generalizing i with
   | nil =>
     simp only [take_nil, Option.toList, getElem?_nil, append_nil]
@@ -236,6 +230,9 @@ theorem take_succ {l : List α} {i : Nat} : l.take (i + 1) = l.take i ++ l[i]?.t
     · simp only [take, Option.toList, getElem?_cons_zero, nil_append]
     · simp only [take, hl, getElem?_cons_succ, cons_append]
 
+@[deprecated take_add_one (since := "2025-10-26")]
+theorem take_succ {l : List α} {i : Nat} : l.take (i + 1) = l.take i ++ l[i]?.toList := take_add_one
+
 theorem dropLast_eq_take {l : List α} : l.dropLast = l.take (l.length - 1) := by
   cases l with
   | nil => simp [dropLast]
@@ -321,7 +318,7 @@ theorem head?_dropWhile_not (p : α → Bool) (l : List α) :
 -- The argument `p` is explicit, as otherwise the head of the left hand side may be a metavariable.
 theorem head_dropWhile_not (p : α → Bool) {l : List α} (w) :
     p ((l.dropWhile p).head w) = false := by
-  simpa [head?_eq_head, w] using head?_dropWhile_not p l
+  simpa [head?_eq_some_head, w] using head?_dropWhile_not p l
 
 theorem takeWhile_map {f : α → β} {p : β → Bool} {l : List α} :
     (l.map f).takeWhile p = (l.takeWhile (p ∘ f)).map f := by
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index ee8b2c215d49..4eaa5a80cdc1 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -226,7 +226,7 @@ private theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α →
   | zero => simp [Array.findSomeRevM?.find]
   | succ i ih =>
     rw [size_toArray] at h
-    rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]
+    rw [Array.findSomeRevM?.find, take_add_one, getElem?_eq_getElem (by omega)]
     simp only [ih, reverse_append]
     congr
     ext1 (_|_) <;> simp
@@ -510,7 +510,7 @@ private theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
         getElem_toArray, getElem_cons_succ, drop_succ_cons]
       split <;> rename_i h₁
       · rw [takeWhile_go_succ, ih]
-        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
+        rw [← getElem_cons_drop h₁, takeWhile_cons]
         split <;> simp_all
       · simp_all [drop_eq_nil_of_le]
 
diff --git a/src/Init/Data/List/Zip.lean b/src/Init/Data/List/Zip.lean
index dbf3589cc0f9..ba153fcd5e91 100644
--- a/src/Init/Data/List/Zip.lean
+++ b/src/Init/Data/List/Zip.lean
@@ -96,7 +96,7 @@ theorem head?_zipWith {f : α → β → γ} :
 theorem head_zipWith {f : α → β → γ} (h):
     (List.zipWith f as bs).head h = f (as.head (by rintro rfl; simp_all)) (bs.head (by rintro rfl; simp_all)) := by
   apply Option.some.inj
-  rw [← head?_eq_head, head?_zipWith, head?_eq_head, head?_eq_head]
+  rw [← head?_eq_some_head, head?_zipWith, head?_eq_some_head, head?_eq_some_head]
 
 @[simp, grind =]
 theorem zipWith_map {μ} {f : γ → δ → μ} {g : α → γ} {h : β → δ} {l₁ : List α} {l₂ : List β} :
@@ -392,7 +392,7 @@ theorem head?_zipWithAll {f : Option α → Option β → γ} :
 @[simp, grind =] theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
     (zipWithAll f as bs).head h = f as.head? bs.head? := by
   apply Option.some.inj
-  rw [← head?_eq_head, head?_zipWithAll]
+  rw [← head?_eq_some_head, head?_zipWithAll]
   split <;> simp_all
 
 @[simp, grind =] theorem tail_zipWithAll {f : Option α → Option β → γ} :
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index c5f4a5c29e34..e25128a7a164 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -255,6 +255,10 @@ protected theorem two_mul (n) : 2 * n = n + n := by rw [Nat.succ_mul, Nat.one_mu
 
 attribute [simp] Nat.le_refl
 
+@[deprecated Nat.le_succ_of_le (since := "2025-10-26")]
+theorem le_step (h : LE.le n m) : LE.le n (succ m) :=
+  Nat.le.step h
+
 theorem succ_lt_succ {n m : Nat} : n < m → succ n < succ m := succ_le_succ
 
 theorem le_of_lt_add_one {n m : Nat} : n < m + 1 → n ≤ m := le_of_succ_le_succ
@@ -310,8 +314,6 @@ instance : Trans (. ≤ . : Nat → Nat → Prop) (. < . : Nat → Nat → Prop)
 protected theorem le_of_eq {n m : Nat} (p : n = m) : n ≤ m :=
   p ▸ Nat.le_refl n
 
-theorem lt.step {n m : Nat} : n < m → n < succ m := le_step
-
 theorem le_of_succ_le {n m : Nat} (h : succ n ≤ m) : n ≤ m := Nat.le_trans (le_succ n) h
 theorem lt_of_succ_lt      {n m : Nat} : succ n < m → n < m := le_of_succ_le
 protected theorem le_of_lt {n m : Nat} : n < m → n ≤ m := le_of_succ_le
@@ -321,6 +323,8 @@ theorem lt_of_succ_lt_succ {n m : Nat} : succ n < succ m → n < m := le_of_succ
 theorem lt_of_succ_le {n m : Nat} (h : succ n ≤ m) : n < m := h
 theorem succ_le_of_lt {n m : Nat} (h : n < m) : succ n ≤ m := h
 
+theorem succ_le_iff : succ m ≤ n ↔ m < n := ⟨lt_of_succ_le, succ_le_of_lt⟩
+
 theorem eq_zero_or_pos : ∀ (n : Nat), n = 0 ∨ n > 0
   | 0   => Or.inl rfl
   | _+1 => Or.inr (succ_pos _)
@@ -331,6 +335,7 @@ theorem pos_of_neZero (n : Nat) [NeZero n] : 0 < n := Nat.pos_of_ne_zero (NeZero
 
 attribute [simp] Nat.lt_add_one
 
+@[deprecated Nat.lt_add_one (since := "2025-10-26")]
 theorem lt.base (n : Nat) : n < succ n := Nat.le_refl (succ n)
 
 protected theorem le_total (m n : Nat) : m ≤ n ∨ n ≤ m :=
@@ -606,14 +611,16 @@ attribute [simp] zero_lt_succ
 
 theorem add_one_ne_self (n) : n + 1 ≠ n := Nat.ne_of_gt (lt_succ_self n)
 
-theorem succ_le : succ n ≤ m ↔ n < m := .rfl
-
 theorem add_one_le_iff : n + 1 ≤ m ↔ n < m := .rfl
 
+@[deprecated Nat.lt_succ_iff (since := "2025-10-26")]
 theorem lt_succ : m < succ n ↔ m ≤ n := ⟨le_of_lt_succ, lt_succ_of_le⟩
 
 theorem lt_succ_of_lt (h : a < b) : a < succ b := le_succ_of_le h
 
+@[deprecated lt_succ_of_lt (since := "2025-10-26")]
+theorem lt.step {n m : Nat} : n < m → n < succ m := le_succ_of_le
+
 theorem lt_add_one_of_lt (h : a < b) : a < b + 1 := le_succ_of_le h
 
 @[simp] theorem lt_one_iff : n < 1 ↔ n = 0 := Nat.lt_succ_iff.trans <| by rw [le_zero_eq]
@@ -639,6 +646,7 @@ theorem add_one_inj : a + 1 = b + 1 ↔ a = b := succ_inj
 
 theorem ne_add_one (n : Nat) : n ≠ n + 1 := fun h => by cases h
 
+@[deprecated add_one_ne_self (since := "2025-10-26")]
 theorem add_one_ne (n : Nat) : n + 1 ≠ n := fun h => by cases h
 
 theorem add_one_le_add_one_iff : a + 1 ≤ b + 1 ↔ a ≤ b := succ_le_succ_iff
@@ -664,25 +672,35 @@ theorem pred_lt_self : ∀ {a}, 0 < a → pred a < a
 theorem pred_lt_pred : ∀ {n m}, n ≠ 0 → n < m → pred n < pred m
   | _+1, _+1, _, h => lt_of_succ_lt_succ h
 
+theorem pred_le_iff : ∀ {n m}, pred n ≤ m ↔ n ≤ succ m
+  | 0, _ => ⟨fun _ => Nat.zero_le _, fun _ => Nat.zero_le _⟩
+  | _+1, _ => Nat.succ_le_succ_iff.symm
+
+@[deprecated pred_le_iff (since := "2025-10-26")]
 theorem pred_le_iff_le_succ : ∀ {n m}, pred n ≤ m ↔ n ≤ succ m
   | 0, _ => ⟨fun _ => Nat.zero_le _, fun _ => Nat.zero_le _⟩
   | _+1, _ => Nat.succ_le_succ_iff.symm
 
-theorem le_succ_of_pred_le : pred n ≤ m → n ≤ succ m := pred_le_iff_le_succ.1
+theorem le_succ_of_pred_le : pred n ≤ m → n ≤ succ m := pred_le_iff.1
+
+theorem pred_le_of_le_succ : n ≤ succ m → pred n ≤ m := pred_le_iff.2
 
-theorem pred_le_of_le_succ : n ≤ succ m → pred n ≤ m := pred_le_iff_le_succ.2
+theorem lt_pred_iff : ∀ {n m}, n < pred m ↔ succ n < m
+  | _, 0 => ⟨nofun, nofun⟩
+  | _, _+1 => Nat.succ_lt_succ_iff.symm
 
+@[deprecated lt_pred_iff (since := "2025-10-26")]
 theorem lt_pred_iff_succ_lt : ∀ {n m}, n < pred m ↔ succ n < m
   | _, 0 => ⟨nofun, nofun⟩
   | _, _+1 => Nat.succ_lt_succ_iff.symm
 
-theorem succ_lt_of_lt_pred : n < pred m → succ n < m := lt_pred_iff_succ_lt.1
+theorem succ_lt_of_lt_pred : n < pred m → succ n < m := lt_pred_iff.1
 
-theorem lt_pred_of_succ_lt : succ n < m → n < pred m := lt_pred_iff_succ_lt.2
+theorem lt_pred_of_succ_lt : succ n < m → n < pred m := lt_pred_iff.2
 
 theorem le_pred_iff_lt : ∀ {n m}, 0 < m → (n ≤ pred m ↔ n < m)
   | 0, _+1, _ => ⟨fun _ => Nat.zero_lt_succ _, fun _ => Nat.zero_le _⟩
-  | _+1, _+1, _ => Nat.lt_pred_iff_succ_lt
+  | _+1, _+1, _ => Nat.lt_pred_iff
 
 theorem le_pred_of_lt (h : n < m) : n ≤ pred m := (le_pred_iff_lt (Nat.zero_lt_of_lt h)).2 h
 
@@ -703,6 +721,7 @@ theorem exists_eq_add_one_of_ne_zero : ∀ {n}, n ≠ 0 → Exists fun k => n =
 
 /-! # Basic theorems for comparing numerals -/
 
+@[deprecated zero_eq (since := "2025-10-26")]
 theorem ctor_eq_zero : Nat.zero = 0 :=
   rfl
 
diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean
index d131e4a6891c..7e7ccb81cb9e 100644
--- a/src/Init/Data/Nat/Div/Lemmas.lean
+++ b/src/Init/Data/Nat/Div/Lemmas.lean
@@ -44,10 +44,10 @@ theorem add_mod_eq_sub : (a + b) % c = a % c + b % c - if a % c + b % c < c then
 
 theorem lt_div_iff_mul_lt (h : 0 < k) : x < y / k ↔ x * k < y - (k - 1) := by
   have t := le_div_iff_mul_le h (x := x + 1) (y := y)
-  rw [succ_le, add_one_mul] at t
+  rw [succ_le_iff, add_one_mul] at t
   have s : k = k - 1 + 1 := by omega
   conv at t => rhs; lhs; rhs; rw [s]
-  rw [← Nat.add_assoc, succ_le, add_lt_iff_lt_sub_right] at t
+  rw [← Nat.add_assoc, succ_le_iff, add_lt_iff_lt_sub_right] at t
   exact t
 
 theorem div_le_iff_le_mul (h : 0 < k) : x / k ≤ y ↔ x ≤ y * k + k - 1 := by
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index fb85eb549012..66c35053d1aa 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -114,6 +114,7 @@ protected theorem sub_one (n) : n - 1 = pred n := rfl
 
 theorem one_add (n) : 1 + n = succ n := Nat.add_comm ..
 
+@[deprecated succ_ne_succ_iff (since := "2025-10-26")]
 theorem succ_ne_succ : succ m ≠ succ n ↔ m ≠ n :=
   ⟨mt (congrArg Nat.succ ·), mt succ.inj⟩
 
@@ -121,7 +122,8 @@ theorem one_lt_succ_succ (n : Nat) : 1 < n.succ.succ := succ_lt_succ <| succ_pos
 
 theorem not_succ_lt_self : ¬ succ n < n := Nat.not_lt_of_ge n.le_succ
 
-theorem succ_le_iff : succ m ≤ n ↔ m < n := ⟨lt_of_succ_le, succ_le_of_lt⟩
+@[deprecated succ_le_iff (since := "2025-10-26")]
+theorem succ_le : succ n ≤ m ↔ n < m := .rfl
 
 theorem le_succ_iff {m n : Nat} : m ≤ n.succ ↔ m ≤ n ∨ m = n.succ := by
   refine ⟨fun hmn ↦ (Nat.lt_or_eq_of_le hmn).imp_left le_of_lt_succ, ?_⟩
@@ -179,18 +181,10 @@ theorem sub_one_add_self (n : Nat) : (n - 1) + n = 2 * n - 1 := Nat.add_comm _ n
 theorem self_add_pred (n : Nat) : n + pred n = (2 * n).pred := self_add_sub_one n
 theorem pred_add_self (n : Nat) : pred n + n = (2 * n).pred := sub_one_add_self n
 
-theorem pred_le_iff : pred m ≤ n ↔ m ≤ succ n :=
-  ⟨le_succ_of_pred_le, by
-    cases m
-    · exact fun _ ↦ zero_le n
-    · exact le_of_succ_le_succ⟩
-
 theorem lt_of_lt_pred (h : m < n - 1) : m < n := by omega
 
 theorem le_add_pred_of_pos (a : Nat) (hb : b ≠ 0) : a ≤ b + (a - 1) := by omega
 
-theorem lt_pred_iff : a < pred b ↔ succ a < b := by simp; omega
-
 /-! ## add -/
 
 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by
@@ -203,7 +197,7 @@ theorem succ_add_eq_add_succ (a b) : succ a + b = a + succ b := Nat.succ_add ..
 protected theorem eq_zero_of_add_eq_zero_right (h : n + m = 0) : n = 0 :=
   (Nat.eq_zero_of_add_eq_zero h).1
 
-protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 :=
+@[simp high] protected theorem add_eq_zero_iff : n + m = 0 ↔ n = 0 ∧ m = 0 :=
   ⟨Nat.eq_zero_of_add_eq_zero, fun ⟨h₁, h₂⟩ => h₂.symm ▸ h₁⟩
 
 @[simp high] protected theorem add_left_cancel_iff {n : Nat} : n + m = n + k ↔ m = k :=
@@ -262,7 +256,8 @@ protected theorem add_self_ne_one : ∀ n, n + n ≠ 1
 theorem le_iff_lt_add_one : x ≤ y ↔ x < y + 1 := by
   omega
 
-@[simp high] protected theorem add_eq_zero : m + n = 0 ↔ m = 0 ∧ n = 0 := by omega
+@[deprecated Nat.add_eq_zero_iff (since := "2025-10-26")]
+protected theorem add_eq_zero : m + n = 0 ↔ m = 0 ∧ n = 0 := by omega
 
 theorem add_pos_iff_pos_or_pos : 0 < m + n ↔ 0 < m ∨ 0 < n := by omega
 
diff --git a/src/Init/Data/Order/Ord.lean b/src/Init/Data/Order/Ord.lean
index e7e6a426e218..2cfba68796c5 100644
--- a/src/Init/Data/Order/Ord.lean
+++ b/src/Init/Data/Order/Ord.lean
@@ -270,6 +270,7 @@ theorem TransCmp.gt_of_gt_of_isGE [TransCmp cmp] {a b c : α} (hab : cmp a b = .
   rw [OrientedCmp.gt_iff_lt, OrientedCmp.isGE_iff_isLE] at *
   exact TransCmp.lt_of_isLE_of_lt hbc hab
 
+@[deprecated TransCmp.gt_trans (since := "2025-10-26")]
 theorem TransCmp.gt_of_gt_of_gt [TransCmp cmp] {a b c : α} (hab : cmp a b = .gt)
     (hbc : cmp b c = .gt) : cmp a c = .gt := by
   apply gt_of_gt_of_isGE hab (Ordering.isGE_of_eq_gt hbc)
diff --git a/src/Init/Data/Range/Polymorphic/Int.lean b/src/Init/Data/Range/Polymorphic/Int.lean
index fd2a37e2b6cb..3d63036bd95e 100644
--- a/src/Init/Data/Range/Polymorphic/Int.lean
+++ b/src/Init/Data/Range/Polymorphic/Int.lean
@@ -37,7 +37,6 @@ instance : LawfulUpwardEnumerableLE Int where
       Int.sub_eq_iff_eq_add', eq_comm (a := y)]
 
 instance : LawfulUpwardEnumerableLT Int := inferInstance
-instance : LawfulUpwardEnumerableLT Int := inferInstance
 
 instance : Rxc.HasSize Int where
   size lo hi := (hi + 1 - lo).toNat
diff --git a/src/Init/Data/Range/Polymorphic/UInt.lean b/src/Init/Data/Range/Polymorphic/UInt.lean
index eb44e66620d4..086afc6cf7af 100644
--- a/src/Init/Data/Range/Polymorphic/UInt.lean
+++ b/src/Init/Data/Range/Polymorphic/UInt.lean
@@ -61,7 +61,6 @@ instance : LawfulUpwardEnumerableLE UInt8 where
       LawfulUpwardEnumerableLE.le_iff _ _
 
 instance : LawfulUpwardEnumerableLT UInt8 := inferInstance
-instance : LawfulUpwardEnumerableLT UInt8 := inferInstance
 
 instance : Rxc.HasSize UInt8 where
   size lo hi := hi.toNat + 1 - lo.toNat
@@ -157,7 +156,6 @@ instance : LawfulUpwardEnumerableLE UInt16 where
       LawfulUpwardEnumerableLE.le_iff _ _
 
 instance : LawfulUpwardEnumerableLT UInt16 := inferInstance
-instance : LawfulUpwardEnumerableLT UInt16 := inferInstance
 
 instance : Rxc.HasSize UInt16 where
   size lo hi := hi.toNat + 1 - lo.toNat
@@ -253,7 +251,6 @@ instance : LawfulUpwardEnumerableLE UInt32 where
       LawfulUpwardEnumerableLE.le_iff _ _
 
 instance : LawfulUpwardEnumerableLT UInt32 := inferInstance
-instance : LawfulUpwardEnumerableLT UInt32 := inferInstance
 
 instance : Rxc.HasSize UInt32 where
   size lo hi := hi.toNat + 1 - lo.toNat
@@ -349,7 +346,6 @@ instance : LawfulUpwardEnumerableLE UInt64 where
       LawfulUpwardEnumerableLE.le_iff _ _
 
 instance : LawfulUpwardEnumerableLT UInt64 := inferInstance
-instance : LawfulUpwardEnumerableLT UInt64 := inferInstance
 
 instance : Rxc.HasSize UInt64 where
   size lo hi := hi.toNat + 1 - lo.toNat
@@ -445,7 +441,6 @@ instance : LawfulUpwardEnumerableLE USize where
       LawfulUpwardEnumerableLE.le_iff _ _
 
 instance : LawfulUpwardEnumerableLT USize := inferInstance
-instance : LawfulUpwardEnumerableLT USize := inferInstance
 
 instance : Rxc.HasSize USize where
   size lo hi := hi.toNat + 1 - lo.toNat
diff --git a/src/Init/Data/Rat/Lemmas.lean b/src/Init/Data/Rat/Lemmas.lean
index bd9ce088411b..2cf5d5f112b5 100644
--- a/src/Init/Data/Rat/Lemmas.lean
+++ b/src/Init/Data/Rat/Lemmas.lean
@@ -231,7 +231,7 @@ theorem den_divInt (a b : Int) : (a /. b).den = if b = 0 then 1 else b.natAbs /
   rw [divInt.eq_def]
   simp only [inline, Nat.succ_eq_add_one]
   split <;> rename_i d
-  · simp only [den_mkRat, Int.ofNat_eq_coe, Int.natAbs_cast]
+  · simp only [den_mkRat, Int.ofNat_eq_coe, Int.natAbs_natCast]
     split <;> rename_i h
     · simp_all
     · simp [if_neg (by omega), Int.gcd]
@@ -650,7 +650,7 @@ protected theorem add_nonneg {a b : Rat} : 0 ≤ a → 0 ≤ b → 0 ≤ a + b :
     simp only [d₁0, d₂0, h₁, h₂, Int.mul_pos, divInt_nonneg_iff_of_pos_right, divInt_add_divInt,
       ne_eq, Int.natCast_eq_zero, not_false_eq_true]
     intro n₁0 n₂0
-    apply Int.add_nonneg <;> apply Int.mul_nonneg <;> · first | assumption | apply Int.ofNat_zero_le
+    apply Int.add_nonneg <;> apply Int.mul_nonneg <;> · first | assumption | apply Int.natCast_nonneg
 
 protected theorem mul_nonneg {a b : Rat} : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
   numDenCasesOn' a fun n₁ d₁ h₁ =>
diff --git a/src/Init/Data/SInt/Bitwise.lean b/src/Init/Data/SInt/Bitwise.lean
index f3658059c4fd..c2639858e1ae 100644
--- a/src/Init/Data/SInt/Bitwise.lean
+++ b/src/Init/Data/SInt/Bitwise.lean
@@ -717,8 +717,8 @@ theorem ISize.shiftLeft_or {a b c : ISize} : (a ||| b) <<< c = (a <<< c) ||| (b
     (-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← Int16.shiftLeft_or]
 @[simp] theorem Int32.neg_one_shiftLeft_or_shiftLeft {a b : Int32} :
     (-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← Int32.shiftLeft_or]
-@[simp] theorem Int64.neg_one_shiftLeft_or_shiftLeft {a b : Int8} :
-    (-1) <<< b ||| a <<< b = (-1) <<< b := by simp
+@[simp] theorem Int64.neg_one_shiftLeft_or_shiftLeft {a b : Int64} :
+    (-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← Int64.shiftLeft_or]
 @[simp] theorem ISize.neg_one_shiftLeft_or_shiftLeft {a b : ISize} :
     (-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← ISize.shiftLeft_or]
 
diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean
index 11514ce92fa7..58807a1bb4db 100644
--- a/src/Init/Data/SInt/Lemmas.lean
+++ b/src/Init/Data/SInt/Lemmas.lean
@@ -2160,10 +2160,10 @@ theorem Int64.ofNat_div {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
 theorem ISize.ofNat_div {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
     ISize.ofNat (a / b) = ISize.ofNat a / ISize.ofNat b := by
   rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tdiv, ofInt_tdiv]
-  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
+  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.natCast_nonneg _))
   · apply Int.le_of_lt_add_one
     simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using ha
-  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
+  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.natCast_nonneg _))
   · apply Int.le_of_lt_add_one
     simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using hb
 
@@ -2229,10 +2229,10 @@ theorem Int64.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
 theorem ISize.ofNat_le_iff_le {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
     ISize.ofNat a ≤ ISize.ofNat b ↔ a ≤ b := by
   rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ofInt_le_iff_le, Int.ofNat_le]
-  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
+  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.natCast_nonneg _))
   · apply Int.le_of_lt_add_one
     simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using ha
-  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
+  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.natCast_nonneg _))
   · apply Int.le_of_lt_add_one
     simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using hb
 
@@ -2292,10 +2292,10 @@ theorem Int64.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
 theorem ISize.ofNat_lt_iff_lt {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
     ISize.ofNat a < ISize.ofNat b ↔ a < b := by
   rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ofInt_lt_iff_lt, Int.ofNat_lt]
-  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
+  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.natCast_nonneg _))
   · apply Int.le_of_lt_add_one
     simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using ha
-  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
+  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.natCast_nonneg _))
   · apply Int.le_of_lt_add_one
     simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using hb
 
@@ -3240,20 +3240,20 @@ theorem ISize.toUSize_le {a b : ISize} (ha : 0 ≤ a) (hab : a ≤ b) : a.toUSiz
 
 theorem Int8.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 7) : 0 ≤ Int8.ofNat a := by
   rw [le_iff_toInt_le, toInt_ofNat_of_lt ha, Int8.toInt_zero]
-  exact Int.ofNat_zero_le _
+  exact Int.natCast_nonneg _
 theorem Int16.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 15) : 0 ≤ Int16.ofNat a := by
   rw [le_iff_toInt_le, toInt_ofNat_of_lt ha, Int16.toInt_zero]
-  exact Int.ofNat_zero_le _
+  exact Int.natCast_nonneg _
 theorem Int32.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 31) : 0 ≤ Int32.ofNat a := by
   rw [le_iff_toInt_le, toInt_ofNat_of_lt ha, Int32.toInt_zero]
-  exact Int.ofNat_zero_le _
+  exact Int.natCast_nonneg _
 theorem Int64.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ 63) : 0 ≤ Int64.ofNat a := by
   rw [le_iff_toInt_le, toInt_ofNat_of_lt ha, Int64.toInt_zero]
-  exact Int.ofNat_zero_le _
+  exact Int.natCast_nonneg _
 theorem ISize.zero_le_ofNat_of_lt {a : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) :
     0 ≤ ISize.ofNat a := by
   rw [le_iff_toInt_le, toInt_ofNat_of_lt_two_pow_numBits ha, ISize.toInt_zero]
-  exact Int.ofNat_zero_le _
+  exact Int.natCast_nonneg _
 
 protected theorem Int8.sub_nonneg_of_le {a b : Int8} (hb : 0 ≤ b) (hab : b ≤ a) : 0 ≤ a - b := by
   rw [← ofNat_toNatClampNeg _ hb, ← ofNat_toNatClampNeg _ (Int8.le_trans hb hab),
@@ -3477,9 +3477,9 @@ theorem Int64.ofNat_mod {a b : Nat} (ha : a < 2 ^ 63) (hb : b < 2 ^ 63) :
 theorem ISize.ofNat_mod {a b : Nat} (ha : a < 2 ^ (System.Platform.numBits - 1)) (hb : b < 2 ^ (System.Platform.numBits - 1)) :
     ISize.ofNat (a % b) = ISize.ofNat a % ISize.ofNat b := by
   rw [← ofInt_eq_ofNat, ← ofInt_eq_ofNat, ← ofInt_eq_ofNat, Int.ofNat_tmod, ofInt_tmod]
-  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
+  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.natCast_nonneg _))
   · apply Int.le_of_lt_add_one
     simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using ha
-  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.ofNat_zero_le _))
+  · exact Int.le_of_lt (Int.lt_of_lt_of_le ISize.toInt_minValue_lt_zero (Int.natCast_nonneg _))
   · apply Int.le_of_lt_add_one
     simpa only [toInt_maxValue_add_one, ← Int.ofNat_lt, Int.natCast_pow] using hb
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 868250e8de3b..036883f6d404 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -1574,7 +1574,7 @@ private theorem Slice.le_offset_findNextPosGo {s : Slice} {o : String.Pos.Raw} (
   | case2 x h₁ h₂ ih =>
     refine Pos.Raw.le_of_lt (Pos.Raw.lt_of_lt_of_le Pos.Raw.lt_inc (ih ?_))
     rw [Pos.Raw.le_iff, Pos.Raw.byteIdx_inc]
-    exact Nat.succ_le.2 h₁
+    exact Nat.succ_le_iff.2 h₁
   | case3 x h => exact h
 
 theorem Slice.lt_offset_findNextPos {s : Slice} {o : String.Pos.Raw} (h) : o < (s.findNextPos o h).offset :=
diff --git a/src/Init/Data/String/PosRaw.lean b/src/Init/Data/String/PosRaw.lean
index 292602c27c0e..a3723c44dd12 100644
--- a/src/Init/Data/String/PosRaw.lean
+++ b/src/Init/Data/String/PosRaw.lean
@@ -239,7 +239,7 @@ theorem Pos.Raw.lt_inc {p : Pos.Raw} : p < p.inc := by simp [lt_iff]
 
 theorem Pos.Raw.le_of_lt {p q : Pos.Raw} : p < q → p ≤ q := by simpa [lt_iff, le_iff] using Nat.le_of_lt
 
-theorem Pos.Raw.inc_le {p q : Pos.Raw} : p.inc ≤ q ↔ p < q := by simpa [lt_iff, le_iff] using Nat.succ_le
+theorem Pos.Raw.inc_le {p q : Pos.Raw} : p.inc ≤ q ↔ p < q := by simpa [lt_iff, le_iff] using Nat.succ_le_iff
 
 theorem Pos.Raw.lt_of_le_of_lt {a b c : Pos.Raw} : a ≤ b → b < c → a < c := by
   simpa [le_iff, lt_iff] using Nat.lt_of_le_of_lt
diff --git a/src/Init/Data/Subtype/Basic.lean b/src/Init/Data/Subtype/Basic.lean
index 07e06f1ac827..b01fb56cf424 100644
--- a/src/Init/Data/Subtype/Basic.lean
+++ b/src/Init/Data/Subtype/Basic.lean
@@ -15,10 +15,6 @@ namespace Subtype
 universe u
 variable {α : Sort u} {p q : α → Prop}
 
-@[ext]
-protected theorem ext : ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2
-  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
-
 @[simp]
 protected theorem «forall» {q : { a // p a } → Prop} : (∀ x, q x) ↔ ∀ a b, q ⟨a, b⟩ :=
   ⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩
diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean
index 55ff82962488..5030aaf6a909 100644
--- a/src/Init/Data/UInt/Bitwise.lean
+++ b/src/Init/Data/UInt/Bitwise.lean
@@ -1231,8 +1231,8 @@ theorem USize.shiftLeft_add {a b c : USize} (hb : b < USize.ofNat System.Platfor
     (-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← UInt16.shiftLeft_or]
 @[simp] theorem UInt32.neg_one_shiftLeft_or_shiftLeft {a b : UInt32} :
     (-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← UInt32.shiftLeft_or]
-@[simp] theorem UInt64.neg_one_shiftLeft_or_shiftLeft {a b : UInt8} :
-    (-1) <<< b ||| a <<< b = (-1) <<< b := by simp
+@[simp] theorem UInt64.neg_one_shiftLeft_or_shiftLeft {a b : UInt64} :
+    (-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← UInt64.shiftLeft_or]
 @[simp] theorem USize.neg_one_shiftLeft_or_shiftLeft {a b : USize} :
     (-1) <<< b ||| a <<< b = (-1) <<< b := by simp [← USize.shiftLeft_or]
 
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index 2f59ad28b35f..544fb83ae0f2 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -1445,7 +1445,7 @@ theorem UInt64.toUSize_div_of_toNat_lt (a b : UInt64) (ha : a.toNat < USize.size
   USize.toNat.inj (by simpa using Nat.div_mod_eq_mod_div_mod ha hb)
 
 @[simp] protected theorem UInt8.toFin_mod (a b : UInt8) : (a % b).toFin = a.toFin % b.toFin := (rfl)
-@[simp] protected theorem UInt16.toFin_mod (a b : UInt8) : (a % b).toFin = a.toFin % b.toFin := (rfl)
+@[simp] protected theorem UInt16.toFin_mod (a b : UInt16) : (a % b).toFin = a.toFin % b.toFin := (rfl)
 @[simp] protected theorem UInt32.toFin_mod (a b : UInt32) : (a % b).toFin = a.toFin % b.toFin := (rfl)
 @[simp] protected theorem UInt64.toFin_mod (a b : UInt64) : (a % b).toFin = a.toFin % b.toFin := (rfl)
 @[simp] protected theorem USize.toFin_mod (a b : USize) : (a % b).toFin = a.toFin % b.toFin := (rfl)
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 2539fd187bea..db30ee2e4113 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -556,12 +556,12 @@ and simplifies these to the function directly taking the value.
   simp
   rw [Array.findSome?_subtype hf]
 
-@[simp] theorem find?_subtype {p : α → Prop} {xs : Array { x // p x }}
+@[simp] theorem find?_subtype {p : α → Prop} {xs : Vector { x // p x } n}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (xs.find? f).map Subtype.val = xs.unattach.find? g := by
-  rcases xs with ⟨l, rfl⟩
+  rcases xs with ⟨xs, rfl⟩
+  rw [find?_mk, Array.find?_subtype hf]
   simp
-  rw [Array.find?_subtype hf]
 
 @[simp] theorem all_subtype {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool}
     (hf : ∀ x h, f ⟨x, h⟩ = g x) :
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 1785d12d1bbb..529703c7c8b1 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -1188,17 +1188,22 @@ theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α
   simp only [mem_mk] at h
   simp [h]
 
+@[grind =]
+theorem contains_iff_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
+    as.contains a ↔ a ∈ as := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
+
+@[deprecated contains_iff_mem (since := "2025-10-26")]
 theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
     as.contains a = true ↔ a ∈ as := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
 
 instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈ as) :=
-  decidable_of_decidable_of_iff contains_iff
+  decidable_of_decidable_of_iff contains_iff_mem
 
 @[grind =] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := by simp
 
 @[simp, grind =] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
     as.contains a = decide (a ∈ as) := by
-  rw [Bool.eq_iff_iff, contains_iff, decide_eq_true_iff]
+  rw [Bool.eq_iff_iff, contains_iff_mem, decide_eq_true_iff]
 
 @[simp] theorem any_push {as : Vector α n} {a : α} {p : α → Bool} :
     (as.push a).any p = (as.any p || p a) := by
@@ -2588,11 +2593,6 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Vector α n} {a : α} :
 -- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
 grind_pattern contains_iff_exists_mem_beq => xs.contains a
 
-@[grind =]
-theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
-    xs.contains a ↔ a ∈ xs := by
-  simp
-
 @[simp, grind =]
 theorem contains_toList [BEq α] {xs : Vector α n} {x : α} :
     xs.toList.contains x = xs.contains x := by
diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean
index d8cc151c52ad..5b08a6f5d0bc 100644
--- a/src/Init/Data/Vector/Lex.lean
+++ b/src/Init/Data/Vector/Lex.lean
@@ -32,7 +32,18 @@ grind_pattern le_toArray => xs.toArray ≤ ys.toArray
 @[simp] theorem lt_toList [LT α] {xs ys : Vector α n} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
 @[simp] theorem le_toList [LT α] {xs ys : Vector α n} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
+@[simp]
+protected theorem not_lt [LT α] {xs ys : Vector α n} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+
+@[deprecated Vector.not_lt (since := "2025-10-26")]
 protected theorem not_lt_iff_ge [LT α] {xs ys : Vector α n} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+
+@[simp]
+protected theorem not_le [LT α] {xs ys : Vector α n} :
+    ¬ xs ≤ ys ↔ ys < xs :=
+  Classical.not_not
+
+@[deprecated Vector.not_le (since := "2025-10-26")]
 protected theorem not_le_iff_gt [LT α] {xs ys : Vector α n} :
     ¬ xs ≤ ys ↔ ys < xs :=
   Classical.not_not
@@ -157,12 +168,6 @@ instance [LT α] [LE α] [IsLinearOrder α] [LawfulOrderLT α] :
   case le_total => constructor; apply Vector.le_total
   case le_trans => constructor; apply Vector.le_trans
 
-@[simp] protected theorem not_lt [LT α]
-    {xs ys : Vector α n} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
-
-@[simp] protected theorem not_le [LT α]
-    {xs ys : Vector α n} : ¬ ys ≤ xs ↔ xs < ys := Classical.not_not
-
 instance [LT α] [Std.Asymm (· < · : α → α → Prop)] : LawfulOrderLT (Vector α n) where
   lt_iff _ _ := by
     open Classical in
diff --git a/src/Init/Ext.lean b/src/Init/Ext.lean
index be3834235c10..d3a6685a43f9 100644
--- a/src/Init/Ext.lean
+++ b/src/Init/Ext.lean
@@ -82,11 +82,14 @@ end Elab.Tactic.Ext
 end Lean
 
 attribute [ext] Prod PProd Sigma PSigma
-attribute [ext] funext propext Subtype.eq Array.ext
+attribute [ext] funext propext Subtype.ext Array.ext Char.ext
+
+@[deprecated Subtype.ext_iff (since := "2025-10-26")]
+protected def Subtype.eq_iff := @Subtype.ext_iff
 
 attribute [grind ext] funext Array.ext
 
-@[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
+attribute [ext] PUnit.ext
 protected theorem Unit.ext (x y : Unit) : x = y := rfl
 
 @[ext] protected theorem Thunk.ext : {a b : Thunk α} → a.get = b.get → a = b
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index c2256fefc1ef..f27bd84bc289 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -300,11 +300,16 @@ theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: a
 
 grind_pattern getElem_mem => l[n]'h ∈ l
 
-theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
+@[simp]
+theorem getElem_cons_drop {as : List α} {i : Nat} (h : i < as.length) :
     as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with
   | _::_, 0   => rfl
-  | _::_, i+1 => getElem_cons_drop_succ_eq_drop (i := i) (Nat.add_one_lt_add_one_iff.mp h)
+  | _::_, i+1 => getElem_cons_drop (i := i) (Nat.add_one_lt_add_one_iff.mp h)
+
+@[deprecated getElem_cons_drop (since := "2025-10-26")]
+theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
+    as[i] :: as.drop (i+1) = as.drop i := getElem_cons_drop h
 
 /-! ### getElem? -/
 
diff --git a/src/Init/Grind/Ring/CommSemiringAdapter.lean b/src/Init/Grind/Ring/CommSemiringAdapter.lean
index 2fd1e3064ce0..009915fc0ab8 100644
--- a/src/Init/Grind/Ring/CommSemiringAdapter.lean
+++ b/src/Init/Grind/Ring/CommSemiringAdapter.lean
@@ -485,7 +485,7 @@ theorem Expr.toPolyS_NonnegCoeffs {e : Expr} : e.toPolyS.NonnegCoeffs := by
   next => constructor; apply Int.pow_nonneg; apply Int.natCast_nonneg
   next => constructor; decide; constructor; decide
   next => apply Poly.pow_NonnegCoeffs; assumption
-  next => constructor; apply Int.ofNat_zero_le
+  next => constructor; apply Int.natCast_nonneg
   all_goals exact Poly.num_zero_NonnegCoeffs
 
 attribute [local simp] Expr.toPolyS_NonnegCoeffs
@@ -499,7 +499,7 @@ theorem Expr.toPolyS_nc_NonnegCoeffs {e : Expr} : e.toPolyS_nc.NonnegCoeffs := b
   next => constructor; apply Int.pow_nonneg; apply Int.natCast_nonneg
   next => constructor; decide; constructor; decide
   next => apply Poly.pow_nc_NonnegCoeffs; assumption
-  next => constructor; apply Int.ofNat_zero_le
+  next => constructor; apply Int.natCast_nonneg
   all_goals exact Poly.num_zero_NonnegCoeffs
 
 attribute [local simp] Expr.toPolyS_nc_NonnegCoeffs
diff --git a/src/Init/GrindInstances/ToInt.lean b/src/Init/GrindInstances/ToInt.lean
index 0fa9c053316e..e48d1fd2c11b 100644
--- a/src/Init/GrindInstances/ToInt.lean
+++ b/src/Init/GrindInstances/ToInt.lean
@@ -280,7 +280,7 @@ instance : ToInt USize (.uint System.Platform.numBits) where
   toInt x := (x.toNat : Int)
   toInt_inj x y w := USize.toNat_inj.mp (Int.ofNat_inj.mp w)
   toInt_mem x := by
-    simp only [IntInterval.mem_co, Int.ofNat_zero_le, true_and]
+    simp only [IntInterval.mem_co, Int.natCast_nonneg, true_and]
     rw [show (2 : Int) ^ System.Platform.numBits = (2 ^ System.Platform.numBits : Nat) by simp,
       Int.ofNat_lt]
     exact USize.toNat_lt_two_pow_numBits x
diff --git a/src/Init/Omega/Int.lean b/src/Init/Omega/Int.lean
index e858c229c253..db10c434803f 100644
--- a/src/Init/Omega/Int.lean
+++ b/src/Init/Omega/Int.lean
@@ -54,7 +54,7 @@ theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) /
   simp only [Nat.shiftRight_eq_div_pow, Int.natCast_ediv]
 
 theorem emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ (x : Int) % y :=
-  Int.ofNat_zero_le _
+  Int.natCast_nonneg _
 
 -- FIXME these are insane:
 theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
@@ -88,7 +88,7 @@ theorem le_of_ge {x y : Int} (h : x ≥ y) : y ≤ x := ge_iff_le.mp h
 
 theorem ofNat_mul_nonneg {a b : Nat} : 0 ≤ (a : Int) * b := by
   rw [← Int.natCast_mul]
-  exact Int.ofNat_zero_le (a * b)
+  exact Int.natCast_nonneg (a * b)
 
 theorem ofNat_sub_eq_zero {b a : Nat} (h : ¬ b ≤ a) : ((a - b : Nat) : Int) = 0 :=
   Int.ofNat_eq_zero.mpr (Nat.sub_eq_zero_of_le (Nat.le_of_lt (Nat.not_le.mp h)))
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 393ceafc3393..d1dab605bf02 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1876,7 +1876,7 @@ theorem Nat.succ_le_succ : LE.le n m → LE.le (succ n) (succ m)
 theorem Nat.zero_lt_succ (n : Nat) : LT.lt 0 (succ n) :=
   succ_le_succ (zero_le n)
 
-theorem Nat.le_step (h : LE.le n m) : LE.le n (succ m) :=
+theorem Nat.le_succ_of_le (h : LE.le n m) : LE.le n (succ m) :=
   Nat.le.step h
 
 protected theorem Nat.le_trans {n m k : Nat} : LE.le n m → LE.le m k → LE.le n k
@@ -1887,14 +1887,11 @@ protected theorem Nat.lt_of_lt_of_le {n m k : Nat} : LT.lt n m → LE.le m k →
   Nat.le_trans
 
 protected theorem Nat.lt_trans {n m k : Nat} (h₁ : LT.lt n m) : LT.lt m k → LT.lt n k :=
-  Nat.le_trans (le_step h₁)
+  Nat.le_trans (le_succ_of_le h₁)
 
 theorem Nat.le_succ (n : Nat) : LE.le n (succ n) :=
   Nat.le.step Nat.le.refl
 
-theorem Nat.le_succ_of_le {n m : Nat} (h : LE.le n m) : LE.le n (succ m) :=
-  Nat.le_trans h (le_succ m)
-
 protected theorem Nat.le_refl (n : Nat) : LE.le n n :=
   Nat.le.refl
 
@@ -2812,7 +2809,7 @@ def Char.ofNat (n : Nat) : Char :=
     (fun h => Char.ofNatAux n h)
     (fun _ => { val := ⟨BitVec.ofNatLT 0 (of_decide_eq_true rfl)⟩, valid := Or.inl (of_decide_eq_true rfl) })
 
-theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
+theorem Char.ext : ∀ {c d : Char}, Eq c.val d.val → Eq c d
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
 theorem Char.val_eq_of_eq : ∀ {c d : Char}, Eq c d → Eq c.val d.val
@@ -2822,12 +2819,12 @@ theorem Char.ne_of_val_ne {c d : Char} (h : Not (Eq c.val d.val)) : Not (Eq c d)
   fun h' => absurd (val_eq_of_eq h') h
 
 theorem Char.val_ne_of_ne {c d : Char} (h : Not (Eq c d)) : Not (Eq c.val d.val) :=
-  fun h' => absurd (eq_of_val_eq h') h
+  fun h' => absurd (ext h') h
 
 instance : DecidableEq Char :=
   fun c d =>
     match decEq c.val d.val with
-    | isTrue h  => isTrue (Char.eq_of_val_eq h)
+    | isTrue h  => isTrue (Char.ext h)
     | isFalse h => isFalse (Char.ne_of_val_ne h)
 
 /-- Returns the number of bytes required to encode this `Char` in UTF-8. -/
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index d291e2946a34..7b730bb70295 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -961,7 +961,7 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
 @[simp]
 theorem mem_keys [LawfulBEq α] (h : m.1.WF) {k : α} :
     k ∈ m.1.keys ↔ m.contains k := by
-  rw [← List.contains_iff]
+  rw [← List.contains_iff_mem]
   simp_to_model [contains, keys]
   rw [List.containsKey_eq_keys_contains]
 
diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index 3ad64d2c080a..5b5a351accf5 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -1599,7 +1599,7 @@ theorem contains_keys [BEq α] [beqOrd : LawfulBEqOrd α] [TransOrd α] {k : α}
 
 theorem mem_keys [LawfulEqOrd α] [TransOrd α] {k : α} (h : t.WF) :
     k ∈ t.keys ↔ k ∈ t := by
-  simpa only [mem_iff_contains, ← List.contains_iff, ← Bool.eq_iff_iff] using contains_keys h
+  simpa only [mem_iff_contains, ← List.contains_iff_mem, ← Bool.eq_iff_iff] using contains_keys h
 
 theorem mem_of_mem_keys [TransOrd α] (h : t.WF) {k : α}
     (h' : k ∈ t.keys) : k ∈ t :=
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index 6bc4cfcc7b76..f57645efa6a7 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -6766,7 +6766,7 @@ theorem minKey_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [LawfulB
 theorem minKey_eq_head_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) {he} :
     minKey l he = (keys l).head (by simp_all [keys_eq_map, List.isEmpty_eq_false_iff]) := by
-  simp [minKey_eq_get_minKey?, Option.get_eq_iff_eq_some, ← List.head?_eq_head,
+  simp [minKey_eq_get_minKey?, Option.get_eq_iff_eq_some, ← List.head?_eq_some_head,
     minKey?_eq_head?_keys ho]
 
 theorem minKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f}
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean
index 1f07f256d035..4fd1df154607 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Clz.lean
@@ -60,7 +60,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG α)
         · simp [hx]
         · simp [Ref.hgate]
       · intro idx hidx
-        simp only [Nat.add_eq_zero, Nat.succ_ne_self, and_false, reduceIte,
+        simp only [Nat.add_eq_zero_iff, Nat.succ_ne_self, and_false, reduceIte,
           Nat.add_one_sub_one]
         rw [RefVec.denote_ite]
         split
diff --git a/src/Std/Time/Internal/Bounded.lean b/src/Std/Time/Internal/Bounded.lean
index edea6338e221..00395c2d5fc2 100644
--- a/src/Std/Time/Internal/Bounded.lean
+++ b/src/Std/Time/Internal/Bounded.lean
@@ -119,12 +119,12 @@ def ofNatWrapping { lo hi : Int } (val : Int) (h : lo ≤ hi) : Bounded.LE lo hi
 
 instance {k : Nat} : OfNat (Bounded.LE lo (lo + k)) n where
   ofNat :=
-    let h : lo ≤ lo + k := Int.le_add_of_nonneg_right (Int.ofNat_zero_le k)
+    let h : lo ≤ lo + k := Int.le_add_of_nonneg_right (Int.natCast_nonneg k)
     ofNatWrapping n h
 
 instance {k : Nat} : Inhabited (Bounded.LE lo (lo + k)) where
   default :=
-    let h : lo ≤ lo + k := Int.le_add_of_nonneg_right (Int.ofNat_zero_le k)
+    let h : lo ≤ lo + k := Int.le_add_of_nonneg_right (Int.natCast_nonneg k)
     ofNatWrapping lo h
 
 /--
@@ -155,7 +155,7 @@ Convert a `Nat` to a `Bounded.LE`.
 -/
 @[inline]
 def ofNat (val : Nat) (h : val ≤ hi) : Bounded.LE 0 hi :=
-  Bounded.mk val (And.intro (Int.ofNat_zero_le val) (Int.ofNat_le.mpr h))
+  Bounded.mk val (And.intro (Int.natCast_nonneg val) (Int.ofNat_le.mpr h))
 
 /--
 Convert a `Nat` to a `Bounded.LE` if it checks.
diff --git a/tests/lean/run/simp4.lean b/tests/lean/run/simp4.lean
index dc7773a204e3..cce6c8cdf784 100644
--- a/tests/lean/run/simp4.lean
+++ b/tests/lean/run/simp4.lean
@@ -49,7 +49,7 @@ theorem ex8 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
   simp (config := { contextual := true })
 
 theorem ex9 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
-  fail_if_success simp [-Nat.add_eq_zero]
+  fail_if_success simp [-Nat.add_eq_zero_iff]
   intro h₁ h₂
   simp [h₁] at h₂
   simp [h₂]
diff --git a/tests/lean/run/simpStar.lean b/tests/lean/run/simpStar.lean
index 6e4fb528801e..53ba8e74fc3e 100644
--- a/tests/lean/run/simpStar.lean
+++ b/tests/lean/run/simpStar.lean
@@ -20,7 +20,7 @@ h₂ : g x < 5
 -/
 #guard_msgs in
 theorem ex3 (x y : Nat) (h₁ : f x x = g x) (h₂ : f x x < 5) : f x x + f x x = 0 := by
-  simp [*, -Nat.add_eq_zero] at *
+  simp [*, -Nat.add_eq_zero_iff] at *
   trace_state
   have aux₁ : f x x = g x := h₁
   have aux₂ : g x < 5     := h₂