diff --git a/Batteries/Classes/Order.lean b/Batteries/Classes/Order.lean
index 422025b746..90d966cf80 100644
--- a/Batteries/Classes/Order.lean
+++ b/Batteries/Classes/Order.lean
@@ -37,7 +37,7 @@ theorem cmp_refl [OrientedCmp cmp] : cmp x x = .eq :=
 end OrientedCmp
 
 /-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/
-class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class TransCmp (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- The comparator operation is transitive. -/
   le_trans : cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt
 
@@ -99,7 +99,7 @@ theorem BEqCmp.cmp_iff_eq [BEq α] [LawfulBEq α] [BEqCmp (α := α) cmp] : cmp
   simp [BEqCmp.cmp_iff_beq]
 
 /-- `LTCmp cmp` asserts that `cmp x y = .lt` and `x < y` coincide. -/
-class LTCmp [LT α] (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class LTCmp [LT α] (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- `cmp x y = .lt` holds iff `x < y` is true. -/
   cmp_iff_lt : cmp x y = .lt ↔ x < y
 
@@ -107,7 +107,7 @@ theorem LTCmp.cmp_iff_gt [LT α] [LTCmp (α := α) cmp] : cmp x y = .gt ↔ y <
   rw [OrientedCmp.cmp_eq_gt, LTCmp.cmp_iff_lt]
 
 /-- `LECmp cmp` asserts that `cmp x y ≠ .gt` and `x ≤ y` coincide. -/
-class LECmp [LE α] (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class LECmp [LE α] (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- `cmp x y ≠ .gt` holds iff `x ≤ y` is true. -/
   cmp_iff_le : cmp x y ≠ .gt ↔ x ≤ y
 
@@ -116,8 +116,8 @@ theorem LECmp.cmp_iff_ge [LE α] [LECmp (α := α) cmp] : cmp x y ≠ .lt ↔ y
 
 /-- `LawfulCmp cmp` asserts that the `LE`, `LT`, `BEq` instances are all coherent with each other
 and with `cmp`, describing a strict weak order (a linear order except for antisymmetry). -/
-class LawfulCmp [LE α] [LT α] [BEq α] (cmp : α → α → Ordering) extends
-  TransCmp cmp, BEqCmp cmp, LTCmp cmp, LECmp cmp : Prop
+class LawfulCmp [LE α] [LT α] [BEq α] (cmp : α → α → Ordering) : Prop extends
+  TransCmp cmp, BEqCmp cmp, LTCmp cmp, LECmp cmp
 
 /-- `OrientedOrd α` asserts that the `Ord` instance satisfies `OrientedCmp`. -/
 abbrev OrientedOrd (α) [Ord α] := OrientedCmp (α := α) compare
diff --git a/Batteries/CodeAction/Misc.lean b/Batteries/CodeAction/Misc.lean
index 1ff2505a76..d49cac1fcf 100644
--- a/Batteries/CodeAction/Misc.lean
+++ b/Batteries/CodeAction/Misc.lean
@@ -290,7 +290,7 @@ def casesExpand : TacticCodeAction := fun _ snap ctx _ node => do
   let (targets, induction, using_, alts) ← match info.stx with
     | `(tactic| cases $[$[$_ :]? $targets],* $[using $u]? $(alts)?) =>
       pure (targets, false, u, alts)
-    | `(tactic| induction $[$targets],* $[using $u]? $[generalizing $_*]? $(alts)?) =>
+    | `(tactic| induction $[$[$_ :]? $targets],* $[using $u]? $[generalizing $_*]? $(alts)?) =>
       pure (targets, true, u, alts)
     | _ => return #[]
   let some discrInfos := targets.mapM (findTermInfo? node) | return #[]
diff --git a/Batteries/Control/Monad.lean b/Batteries/Control/Monad.lean
index 6ecf117be7..0a425a65f1 100644
--- a/Batteries/Control/Monad.lean
+++ b/Batteries/Control/Monad.lean
@@ -3,35 +3,9 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Batteries.Tactic.Alias
 
--- Note: this will be replaced by `_root_.map_inj_right_of_nonempty` in nightly-2025-02-07
-theorem _root_.LawfulFunctor.map_inj_right_of_nonempty [Functor f] [LawfulFunctor f] [Nonempty α]
-    {g : α → β} (h : ∀ {x y : α}, g x = g y → x = y) {x y : f α} :
-    g <$> x = g <$> y ↔ x = y := by
-  constructor
-  · open Classical in
-    let g' a := if h : ∃ b, g b = a then h.choose else Classical.ofNonempty
-    have g'g a : g' (g a) = a := by
-      simp only [exists_apply_eq_apply, ↓reduceDIte, g']
-      exact h (_ : ∃ b, g b = g a).choose_spec
-    intro h'
-    simpa only [Functor.map_map, g'g, id_map'] using congrArg (g' <$> ·) h'
-  · intro h'
-    rw [h']
-
--- Note: this will be replaced by `_root_.map_inj_right` in nightly-2025-02-07
-theorem _root_.LawfulMonad.map_inj_right [Monad m] [LawfulMonad m]
-    {f : α → β} (h : ∀ {x y : α}, f x = f y → x = y) {x y : m α} :
-    f <$> x = f <$> y ↔ x = y := by
-  by_cases hempty : Nonempty α
-  · exact LawfulFunctor.map_inj_right_of_nonempty h
-  · constructor
-    · intro h'
-      have (z : m α) : z = (do let a ← z; let b ← pure (f a); x) := by
-        conv => lhs; rw [← bind_pure z]
-        congr; funext a
-        exact (hempty ⟨a⟩).elim
-      rw [this x, this y]
-      rw [← bind_assoc, ← map_eq_pure_bind, h', map_eq_pure_bind, bind_assoc]
-    · intro h'
-      rw [h']
+@[deprecated (since := "2025-02-09")] alias LawfulFunctor.map_inj_right_of_nonempty :=
+map_inj_right_of_nonempty
+@[deprecated (since := "2025-02-09")] alias LawfulMonad.map_inj_right :=
+map_inj_right
diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean
index a93a0e2fd1..119a89cb4e 100644
--- a/Batteries/Data/Array/Lemmas.lean
+++ b/Batteries/Data/Array/Lemmas.lean
@@ -43,8 +43,8 @@ theorem idxOf?_toList [BEq α] {a : α} {l : Array α} :
 
 /-! ### erase -/
 
-@[deprecated (since := "2025-02-03")] alias eraseP_toArray := List.eraseP_toArray
-@[deprecated (since := "2025-02-03")] alias erase_toArray := List.erase_toArray
+@[deprecated (since := "2025-02-06")] alias eraseP_toArray := List.eraseP_toArray
+@[deprecated (since := "2025-02-06")] alias erase_toArray := List.erase_toArray
 
 @[simp] theorem toList_erase [BEq α] (l : Array α) (a : α) :
     (l.erase a).toList = l.toList.erase a := by
@@ -65,137 +65,11 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp
 
 /-! ### insertAt -/
 
-@[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) :
-    (insertIdx.loop i as j).size = as.size := by
-  unfold insertIdx.loop
-  split
-  · rw [size_insertIdx_loop, size_swap]
-  · rfl
-
-@[simp] theorem size_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
-    (as.insertIdx i v).size = as.size + 1 := by
-  rw [insertIdx, size_insertIdx_loop, size_push]
-
-@[deprecated size_insertIdx (since := "2024-11-20")] alias size_insertAt := size_insertIdx
-
-theorem getElem_insertIdx_loop_lt {as : Array α} {i : Nat} {j : Fin as.size} {k : Nat} {h}
-    (w : k < i) :
-    (insertIdx.loop i as j)[k] = as[k]'(by simpa using h) := by
-  unfold insertIdx.loop
-  split <;> rename_i h₁
-  · simp only
-    rw [getElem_insertIdx_loop_lt w]
-    rw [getElem_swap]
-    split <;> rename_i h₂
-    · simp_all
-      omega
-    · split <;> rename_i h₃
-      · omega
-      · simp_all
-  · rfl
-
-theorem getElem_insertIdx_loop_eq {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {h} :
-    (insertIdx.loop i as ⟨j, hj⟩)[i] = if i ≤ j then as[j] else as[i]'(by simpa using h) := by
-  unfold insertIdx.loop
-  split <;> rename_i h₁
-  · simp at h₁
-    have : j - 1 < j := by omega
-    rw [getElem_insertIdx_loop_eq]
-    rw [getElem_swap]
-    simp
-    split <;> rename_i h₂
-    · rw [if_pos (by omega)]
-    · omega
-  · simp at h₁
-    by_cases h' : i = j
-    · simp [h']
-    · have t : ¬ i ≤ j := by omega
-      simp [t]
-
-theorem getElem_insertIdx_loop_gt {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size}
-    {k : Nat} {h} (w : i < k) :
-    (insertIdx.loop i as ⟨j, hj⟩)[k] =
-      if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
-  unfold insertIdx.loop
-  split <;> rename_i h₁
-  · simp only
-    simp only at h₁
-    have : j - 1 < j := by omega
-    rw [getElem_insertIdx_loop_gt w]
-    rw [getElem_swap]
-    split <;> rename_i h₂
-    · rw [if_neg (by omega), if_neg (by omega)]
-      have t : k ≤ j := by omega
-      simp [t]
-    · rw [getElem_swap]
-      rw [if_neg (by omega)]
-      split <;> rename_i h₃
-      · simp [h₃]
-      · have t : ¬ k ≤ j := by omega
-        simp [t]
-  · simp only at h₁
-    have t : ¬ k ≤ j := by omega
-    simp [t]
-
-theorem getElem_insertIdx_loop {as : Array α} {i : Nat} {j : Nat} {hj : j < as.size} {k : Nat} {h} :
-    (insertIdx.loop i as ⟨j, hj⟩)[k] =
-      if h₁ : k < i then
-        as[k]'(by simpa using h)
-      else
-        if h₂ : k = i then
-          if i ≤ j then as[j] else as[i]'(by simpa [h₂] using h)
-        else
-          if k ≤ j then as[k-1]'(by simp at h; omega) else as[k]'(by simpa using h) := by
-  split <;> rename_i h₁
-  · rw [getElem_insertIdx_loop_lt h₁]
-  · split <;> rename_i h₂
-    · subst h₂
-      rw [getElem_insertIdx_loop_eq]
-    · rw [getElem_insertIdx_loop_gt (by omega)]
-
-theorem getElem_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
-    (k) (h' : k < (as.insertIdx i v).size) :
-    (as.insertIdx i v)[k] =
-      if h₁ : k < i then
-        as[k]'(by omega)
-      else
-        if h₂ : k = i then
-          v
-        else
-          as[k - 1]'(by simp at h'; omega) := by
-  unfold insertIdx
-  rw [getElem_insertIdx_loop]
-  simp only [size_insertIdx] at h'
-  replace h' : k ≤ as.size := by omega
-  simp only [getElem_push, h, ↓reduceIte, Nat.lt_irrefl, ↓reduceDIte, h', dite_eq_ite]
-  split <;> rename_i h₁
-  · rw [dif_pos (by omega)]
-  · split <;> rename_i h₂
-    · simp [h₂]
-    · split <;> rename_i h₃
-      · rfl
-      · omega
-
-theorem getElem_insertIdx_lt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
-    (k) (h' : k < (as.insertIdx i v).size) (h : k < i) :
-    (as.insertIdx i v)[k] = as[k] := by
-  simp [getElem_insertIdx, h]
-
-@[deprecated getElem_insertIdx_lt (since := "2024-11-20")] alias getElem_insertAt_lt :=
-getElem_insertIdx_lt
-
-theorem getElem_insertIdx_eq (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
-    (as.insertIdx i v)[i]'(by simp; omega) = v := by
-  simp [getElem_insertIdx, h]
-
-@[deprecated getElem_insertIdx_eq (since := "2024-11-20")] alias getElem_insertAt_eq :=
-getElem_insertIdx_eq
-
-theorem getElem_insertIdx_gt (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α)
-    (k) (h' : k < (as.insertIdx i v).size) (h : i < k) :
-    (as.insertIdx i v)[k] = as[k-1]'(by simp at h'; omega) := by
-  rw [getElem_insertIdx]
-  rw [dif_neg (by omega), dif_neg (by omega)]
-
-@[deprecated getElem_insertIdx_gt (since := "2024-11-20")] alias getElem_insertAt_gt :=
-getElem_insertIdx_gt
+@[deprecated (since := "2024-11-20")] alias size_insertAt := size_insertIdx
+@[deprecated (since := "2024-11-20")] alias getElem_insertAt_lt := getElem_insertIdx_of_lt
+@[deprecated (since := "2024-11-20")] alias getElem_insertAt_eq := getElem_insertIdx_self
+@[deprecated (since := "2024-11-20")] alias getElem_insertAt_gt := getElem_insertIdx_of_gt
+
+@[deprecated (since := "2025-02-06")] alias getElem_insertIdx_lt := getElem_insertIdx_of_lt
+@[deprecated (since := "2025-02-06")] alias getElem_insertIdx_eq := getElem_insertIdx_self
+@[deprecated (since := "2025-02-06")] alias getElem_insertIdx_gt := getElem_insertIdx_of_gt
diff --git a/Batteries/Data/Array/Monadic.lean b/Batteries/Data/Array/Monadic.lean
index 74855f57c4..36cc22abcb 100644
--- a/Batteries/Data/Array/Monadic.lean
+++ b/Batteries/Data/Array/Monadic.lean
@@ -182,122 +182,3 @@ theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α
   · exact .pure rfl
 
 end Array
-
-namespace List
-
-theorem filterM_toArray [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) :
-    l.toArray.filterM p = toArray <$> l.filterM p := by
-  simp only [Array.filterM, filterM, foldlM_toArray, bind_pure_comp, Functor.map_map]
-  conv => lhs; rw [← reverse_nil]
-  generalize [] = acc
-  induction l generalizing acc with simp
-  | cons x xs ih =>
-    congr; funext b
-    cases b
-    · simp only [Bool.false_eq_true, ↓reduceIte, pure_bind, cond_false]
-      exact ih acc
-    · simp only [↓reduceIte, ← reverse_cons, pure_bind, cond_true]
-      exact ih (x :: acc)
-
-theorem filterRevM_toArray [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) :
-    l.toArray.filterRevM p = toArray <$> l.filterRevM p := by
-  simp [Array.filterRevM, filterRevM]
-  rw [← foldlM_reverse, ← foldlM_toArray, ← Array.filterM, filterM_toArray]
-  simp only [filterM, bind_pure_comp, Functor.map_map, reverse_toArray, reverse_reverse]
-
-theorem filterMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Option β)) :
-    l.toArray.filterMapM f = toArray <$> l.filterMapM f := by
-  simp [Array.filterMapM, filterMapM]
-  conv => lhs; rw [← reverse_nil]
-  generalize [] = acc
-  induction l generalizing acc with simp [filterMapM.loop]
-  | cons x xs ih =>
-    congr; funext o
-    cases o
-    · simp only [pure_bind]; exact ih acc
-    · simp only [pure_bind]; rw [← List.reverse_cons]; exact ih _
-
-theorem flatMapM_toArray [Monad m] [LawfulMonad m] (l : List α) (f : α → m (Array β)) :
-    l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a) := by
-  simp only [Array.flatMapM, bind_pure_comp, foldlM_toArray, flatMapM]
-  conv => lhs; arg 2; change [].reverse.flatten.toArray
-  generalize [] = acc
-  induction l generalizing acc with
-  | nil => simp only [foldlM_nil, flatMapM.loop, map_pure]
-  | cons x xs ih =>
-    simp only [foldlM_cons, bind_map_left, flatMapM.loop, _root_.map_bind]
-    congr; funext a
-    conv => lhs; rw [Array.toArray_append, ← flatten_concat, ← reverse_cons]
-    exact ih _
-
-theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
-    (f : (i : Nat) → α → (h : i < l.length) → m β) :
-    l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f := by
-  let rec go (i : Nat) (acc : Array β) (inv : i + acc.size = l.length) :
-      Array.mapFinIdxM.map l.toArray f i acc.size inv acc
-      = toArray <$> mapFinIdxM.go l f (l.drop acc.size) acc
-        (by simp [Nat.sub_add_cancel (Nat.le.intro (Nat.add_comm _ _ ▸ inv))]) := by
-    match i with
-    | 0 =>
-      rw [Nat.zero_add] at inv
-      simp only [Array.mapFinIdxM.map, inv, drop_length, mapFinIdxM.go, map_pure]
-    | k + 1 =>
-      conv => enter [2, 2, 3]; rw [← getElem_cons_drop l acc.size (by omega)]
-      simp only [Array.mapFinIdxM.map, mapFinIdxM.go, _root_.map_bind]
-      congr; funext x
-      conv => enter [1, 4]; rw [← Array.size_push _ x]
-      conv => enter [2, 2, 3]; rw [← Array.size_push _ x]
-      refine go k (acc.push x) _
-  simp only [Array.mapFinIdxM, mapFinIdxM]
-  exact go _ #[] _
-
-theorem mapIdxM_toArray [Monad m] [LawfulMonad m] (l : List α)
-    (f : Nat → α → m β) :
-    l.toArray.mapIdxM f = toArray <$> l.mapIdxM f := by
-  let rec go (bs : List α) (acc : Array β) (inv : bs.length + acc.size = l.length) :
-      mapFinIdxM.go l (fun i a h => f i a) bs acc inv = mapIdxM.go f bs acc := by
-    match bs with
-    | [] => simp only [mapFinIdxM.go, mapIdxM.go]
-    | x :: xs => simp only [mapFinIdxM.go, mapIdxM.go, go]
-  unfold Array.mapIdxM
-  rw [mapFinIdxM_toArray]
-  simp only [mapFinIdxM, mapIdxM]
-  rw [go]
-
-end List
-
-namespace Array
-
-theorem toList_filterM [Monad m] [LawfulMonad m] (a : Array α) (p : α → m Bool) :
-    toList <$> a.filterM p = a.toList.filterM p := by
-  rw [List.filterM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_filterRevM [Monad m] [LawfulMonad m] (a : Array α) (p : α → m Bool) :
-    toList <$> a.filterRevM p = a.toList.filterRevM p := by
-  rw [List.filterRevM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_filterMapM [Monad m] [LawfulMonad m] (a : Array α) (f : α → m (Option β)) :
-    toList <$> a.filterMapM f = a.toList.filterMapM f := by
-  rw [List.filterMapM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_flatMapM [Monad m] [LawfulMonad m] (a : Array α) (f : α → m (Array β)) :
-    toList <$> a.flatMapM f = a.toList.flatMapM (fun a => toList <$> f a) := by
-  rw [List.flatMapM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_mapFinIdxM [Monad m] [LawfulMonad m] (l : Array α)
-    (f : (i : Nat) → α → (h : i < l.size) → m β) :
-    toList <$> l.mapFinIdxM f = l.toList.mapFinIdxM f := by
-  rw [List.mapFinIdxM_toArray]
-  simp only [Functor.map_map, id_map']
-
-theorem toList_mapIdxM [Monad m] [LawfulMonad m] (l : Array α)
-    (f : Nat → α → m β) :
-    toList <$> l.mapIdxM f = l.toList.mapIdxM f := by
-  rw [List.mapIdxM_toArray]
-  simp only [Functor.map_map, id_map']
-
-end Array
diff --git a/Batteries/Data/Array/Pairwise.lean b/Batteries/Data/Array/Pairwise.lean
index 498c070540..bc4b7db952 100644
--- a/Batteries/Data/Array/Pairwise.lean
+++ b/Batteries/Data/Array/Pairwise.lean
@@ -19,14 +19,12 @@ that `as` is strictly sorted and `as.Pairwise (· ≤ ·)` asserts that `as` is
 -/
 def Pairwise (R : α → α → Prop) (as : Array α) : Prop := as.toList.Pairwise R
 
-theorem pairwise_iff_get {as : Array α} : as.Pairwise R ↔
-    ∀ (i j : Fin as.size), i < j → R (as.get i i.2) (as.get j j.2) := by
-  unfold Pairwise; simp [List.pairwise_iff_get, getElem_fin_eq_getElem_toList]
-
 theorem pairwise_iff_getElem {as : Array α} : as.Pairwise R ↔
     ∀ (i j : Nat) (_ : i < as.size) (_ : j < as.size), i < j → R as[i] as[j] := by
   unfold Pairwise; simp [List.pairwise_iff_getElem, length_toList]
 
+@[deprecated (since := "2025-02-19")] alias pairwise_iff_get := pairwise_iff_getElem
+
 instance (R : α → α → Prop) [DecidableRel R] (as) : Decidable (Pairwise R as) :=
   have : (∀ (j : Fin as.size) (i : Fin j.val), R as[i.val] (as[j.val])) ↔ Pairwise R as := by
     rw [pairwise_iff_getElem]
diff --git a/Batteries/Data/BinaryHeap.lean b/Batteries/Data/BinaryHeap.lean
index 4795be8352..6da9617579 100644
--- a/Batteries/Data/BinaryHeap.lean
+++ b/Batteries/Data/BinaryHeap.lean
@@ -40,8 +40,8 @@ def heapifyDown (lt : α → α → Bool) (a : Vector α sz) (i : Fin sz) :
       simp only [maxChild] at h
       split at h
       · split at h
-        · split at h <;> (cases h; simp_arith)
-        · cases h; simp_arith
+        · split at h <;> (cases h; simp +arith)
+        · cases h; simp +arith
       · contradiction
     if lt a[i] a[j] then
       heapifyDown lt (a.swap i j) j
@@ -117,8 +117,8 @@ def popMax (self : BinaryHeap α lt) : BinaryHeap α lt :=
     self.popMax.size = self.size - 1 := by
   simp only [popMax, size]
   split
-  · simp_arith [*]
-  · split <;> simp_arith [*]
+  · simp +arith [*]
+  · split <;> simp +arith
 
 /-- `O(log n)`. Return and remove the maximum element from a `BinaryHeap`. -/
 def extractMax (self : BinaryHeap α lt) : Option α × BinaryHeap α lt :=
diff --git a/Batteries/Data/BinomialHeap/Basic.lean b/Batteries/Data/BinomialHeap/Basic.lean
index 5c0aa90fde..3258fcf2db 100644
--- a/Batteries/Data/BinomialHeap/Basic.lean
+++ b/Batteries/Data/BinomialHeap/Basic.lean
@@ -62,7 +62,7 @@ def HeapNode.rank : HeapNode α → Nat
 where
   go {α} : ∀ s n, @rankTR.go α s n = rank s + n
   | .nil, _ => (Nat.zero_add ..).symm
-  | .node .., _ => by simp_arith only [rankTR.go, go, rank]
+  | .node .., _ => by simp +arith only [rankTR.go, go, rank]
 
 /--
 A `Heap` is the top level structure in a binomial heap.
@@ -277,7 +277,7 @@ by repeatedly pulling the minimum element out of the heap.
   match eq : s.deleteMin le with
   | none => pure init
   | some (hd, tl) => do
-    have : tl.realSize < s.realSize := by simp_arith [Heap.realSize_deleteMin eq]
+    have : tl.realSize < s.realSize := by simp +arith [Heap.realSize_deleteMin eq]
     foldM le tl (← f init hd) f
 termination_by s.realSize
 
diff --git a/Batteries/Data/ByteArray.lean b/Batteries/Data/ByteArray.lean
index 5669e2147a..57d398d650 100644
--- a/Batteries/Data/ByteArray.lean
+++ b/Batteries/Data/ByteArray.lean
@@ -55,11 +55,11 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
   Array.size_set ..
 
 @[simp] theorem get_set_eq (a : ByteArray) (i : Fin a.size) (v : UInt8) : (a.set i v)[i.val] = v :=
-  Array.getElem_set_self _ _ _ _ (eq := rfl) _
+  Array.getElem_set_self _ _ _ _
 
 theorem get_set_ne (a : ByteArray) (i : Fin a.size) (v : UInt8) (hj : j < a.size) (h : i.val ≠ j) :
     (a.set i v)[j]'(a.size_set .. ▸ hj) = a[j] :=
-  Array.get_set_ne (h:=h) ..
+  Array.getElem_set_ne (h := h) ..
 
 theorem set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) :
     (a.set i v).set i v' = a.set i v' :=
diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean
index af33401646..6966e68c86 100644
--- a/Batteries/Data/HashMap/WF.lean
+++ b/Batteries/Data/HashMap/WF.lean
@@ -98,12 +98,11 @@ where
     · next H =>
       refine (go (i+1) _ _ fun j hj => ?a).trans ?b
       · case a =>
-        simp only [Array.length_toList, Array.toList_set]
-        simp [List.getD_eq_getElem?_getD, List.getElem?_set, Option.map_eq_map]; split
+        simp only [Array.toList_set, List.getElem?_set, Array.length_toList]; split
         · cases source.toList[j]? <;> rfl
         · next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H))
       · case b =>
-        simp only [Array.length_toList, Array.toList_set, Array.get_eq_getElem, AssocList.foldl_eq]
+        simp only [Array.length_toList, Array.toList_set, AssocList.foldl_eq]
         refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set H; eq ▸ ?_
         rw [h₁]
         simp only [Buckets.size_eq, List.map_append, List.map_cons, AssocList.toList,
@@ -180,7 +179,7 @@ where
         · exact hs₂ _ (by simp_all)
       · let rank (k : α) := ((hash k).toUSize % USize.ofNat source.size).toNat
         have := expand_WF.foldl rank ?_ (hs₂ _ H) ht.1 (fun _ h₁ _ h₂ => ?_)
-        · simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.size_set]
+        · simp only [AssocList.foldl_eq, Array.size_set]
           exact ⟨this.1, fun _ h₁ _ h₂ => Nat.lt_succ_of_le (this.2 _ h₁ _ h₂)⟩
         · exact hs₁ _ (Array.getElem_mem_toList ..)
         · have := ht.2 _ h₁ _ h₂
@@ -371,7 +370,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable
     have := H.out.2.1 _ h
     rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢
     exact this.sublist (H3 l.toList)
-  · simp only [Array.size_toArray, List.length_map, Array.length_toList, ← Array.getElem_toList,
+  · simp only [List.size_toArray, List.length_map, Array.length_toList, ← Array.getElem_toList,
       List.getElem_map] at h ⊢
     have := H.out.2.2 _ h
     simp only [AssocList.All, List.toList_toAssocList, List.mem_reverse, List.mem_filterMap,
diff --git a/Batteries/Data/List/EraseIdx.lean b/Batteries/Data/List/EraseIdx.lean
index 42b4bfacd1..b2b7676f1b 100644
--- a/Batteries/Data/List/EraseIdx.lean
+++ b/Batteries/Data/List/EraseIdx.lean
@@ -27,6 +27,7 @@ theorem mem_eraseIdx_iff_get {x : α} {l} {k} :
   · rintro ⟨i, h, rfl⟩
     exact ⟨i.1, h, i.2, rfl⟩
 
+set_option linter.deprecated false in
 @[deprecated mem_eraseIdx_iff_getElem? (since := "2024-06-12")]
 theorem mem_eraseIdx_iff_get? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l.get? i = x := by
   simp [mem_eraseIdx_iff_getElem?]
diff --git a/Batteries/Data/List/Lemmas.lean b/Batteries/Data/List/Lemmas.lean
index 4f7bb3fb78..6cd61d0b4a 100644
--- a/Batteries/Data/List/Lemmas.lean
+++ b/Batteries/Data/List/Lemmas.lean
@@ -47,28 +47,34 @@ theorem set_eq_take_cons_drop (a : α) {n l} (h : n < length l) :
     set l n a = take n l ++ a :: drop (n + 1) l := by
   rw [set_eq_modify, modify_eq_take_cons_drop h]
 
-theorem modify_eq_set_get? (f : α → α) :
-    ∀ n (l : List α), l.modify f n = ((fun a => l.set n (f a)) <$> l.get? n).getD l
-  | 0, l => by cases l <;> rfl
+theorem modify_eq_set_getElem? (f : α → α) :
+    ∀ n (l : List α), l.modify f n = ((fun a => l.set n (f a)) <$> l[n]?).getD l
+  | 0, l => by cases l <;> simp
   | _+1, [] => rfl
   | n+1, b :: l =>
-    (congrArg (cons _) (modify_eq_set_get? ..)).trans <| by cases h : l[n]? <;> simp [h]
+    (congrArg (cons _) (modify_eq_set_getElem? ..)).trans <| by cases h : l[n]? <;> simp [h]
+
+@[deprecated (since := "2025-02-15")] alias modify_eq_set_get? := modify_eq_set_getElem?
 
 theorem modify_eq_set_get (f : α → α) {n} {l : List α} (h) :
     l.modify f n = l.set n (f (l.get ⟨n, h⟩)) := by
-  rw [modify_eq_set_get?, get?_eq_get h]; rfl
+  rw [modify_eq_set_getElem?, getElem?_eq_getElem h]; rfl
 
 theorem getElem?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) :
     (set l n a)[n]? = some a := by rw [getElem?_set_self', getElem?_eq_getElem h]; rfl
 
-theorem get?_set_of_lt (a : α) {m n} (l : List α) (h : n < length l) :
-    (set l m a).get? n = if m = n then some a else l.get? n := by
+theorem getElem?_set_of_lt (a : α) {m n} (l : List α) (h : n < length l) :
+    (set l m a)[n]? = if m = n then some a else l[n]? := by
   simp [getElem?_set', getElem?_eq_getElem h]
 
-theorem get?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
-    (set l m a).get? n = if m = n then some a else l.get? n := by
+@[deprecated (since := "2025-02-15")] alias get?_set_of_lt := getElem?_set_of_lt
+
+theorem getElem?_set_of_lt' (a : α) {m n} (l : List α) (h : m < length l) :
+    (set l m a)[n]? = if m = n then some a else l[n]? := by
   simp [getElem?_set]; split <;> subst_vars <;> simp [*, getElem?_eq_getElem h]
 
+@[deprecated (since := "2025-02-15")] alias get?_set_of_lt' := getElem?_set_of_lt'
+
 /-! ### tail -/
 
 theorem length_tail_add_one (l : List α) (h : 0 < length l) : (length (tail l)) + 1 = length l := by
@@ -391,6 +397,7 @@ theorem chain_lt_range' (s n : Nat) {step} (h : 0 < step) :
     Chain (· < ·) s (range' (s + step) n step) :=
   (chain_succ_range' s n step).imp fun _ _ e => e.symm ▸ Nat.lt_add_of_pos_right h
 
+set_option linter.deprecated false in
 @[deprecated getElem?_range' (since := "2024-06-12")]
 theorem get?_range' (s step) {m n : Nat} (h : m < n) :
     get? (range' s n step) m = some (s + step * m) := by
@@ -401,6 +408,7 @@ theorem get_range' {n m step} (i) (H : i < (range' n m step).length) :
     get (range' n m step) ⟨i, H⟩ = n + step * i := by
   simp
 
+set_option linter.deprecated false in
 @[deprecated getElem?_range (since := "2024-06-12")]
 theorem get?_range {m n : Nat} (h : m < n) : get? (range n) m = some m := by
   simp [getElem?_range, h]
@@ -562,7 +570,7 @@ theorem dropInfix?_go_eq_some_iff [BEq α] {i l acc p s : List α} :
         (∀ p'' i'' s'', l = p'' ++ i'' ++ s'' → i'' == i → p''.length ≥ p'.length) := by
   unfold dropInfix?.go
   split
-  · simp only [isEmpty_eq_true, ite_none_right_eq_some, some.injEq, Prod.mk.injEq, nil_eq,
+  · simp only [isEmpty_iff, ite_none_right_eq_some, some.injEq, Prod.mk.injEq, nil_eq,
       append_assoc, append_eq_nil_iff, ge_iff_le, and_imp]
     constructor
     · rintro ⟨rfl, rfl, rfl⟩
@@ -587,7 +595,7 @@ theorem dropInfix?_go_eq_some_iff [BEq α] {i l acc p s : List α} :
         rw [cons_eq_append_iff] at h₁
         simp at h₁
         obtain (⟨⟨rfl, rfl⟩, rfl⟩ | ⟨a', h₁, rfl⟩) := h₁
-        · simp only [nil_beq_iff, isEmpty_eq_true] at h₂
+        · simp only [nil_beq_iff, isEmpty_iff] at h₂
           simp only [h₂] at h
           simp at h
         · rw [append_eq_cons_iff] at h₁
@@ -676,24 +684,32 @@ theorem append_eq_of_isSuffixOf?_eq_some [BEq α] [LawfulBEq α] {xs ys zs : Lis
 /-! ### deprecations -/
 
 @[deprecated (since := "2024-08-15")] alias isEmpty_iff_eq_nil := isEmpty_iff
+
+set_option linter.deprecated false in
 @[deprecated getElem_eq_iff (since := "2024-06-12")]
 theorem get_eq_iff : List.get l n = x ↔ l.get? n.1 = some x := by
   simp
+
+set_option linter.deprecated false in
 @[deprecated getElem?_inj (since := "2024-06-12")]
 theorem get?_inj
     (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs.get? i = xs.get? j) : i = j := by
   apply getElem?_inj h₀ h₁
   simp_all
+
 @[deprecated (since := "2024-10-21")] alias modifyNth_nil := modify_nil
 @[deprecated (since := "2024-10-21")] alias modifyNth_zero_cons := modify_zero_cons
 @[deprecated (since := "2024-10-21")] alias modifyNth_succ_cons := modify_succ_cons
 @[deprecated (since := "2024-10-21")] alias modifyNthTail_id := modifyTailIdx_id
 @[deprecated (since := "2024-10-21")] alias eraseIdx_eq_modifyNthTail := eraseIdx_eq_modifyTailIdx
 @[deprecated (since := "2024-10-21")] alias getElem?_modifyNth := getElem?_modify
+
+set_option linter.deprecated false in
 @[deprecated getElem?_modify (since := "2024-06-12")]
 theorem get?_modifyNth (f : α → α) (n) (l : List α) (m) :
     (modify f n l).get? m = (fun a => if n = m then f a else a) <$> l.get? m := by
   simp [getElem?_modify]
+
 @[deprecated (since := "2024-10-21")] alias length_modifyNthTail := length_modifyTailIdx
 @[deprecated (since := "2024-06-07")] alias modifyNthTail_length := length_modifyTailIdx
 @[deprecated (since := "2024-10-21")] alias modifyNthTail_add := modifyTailIdx_add
@@ -701,15 +717,21 @@ theorem get?_modifyNth (f : α → α) (n) (l : List α) (m) :
 @[deprecated (since := "2024-10-21")] alias length_modifyNth := length_modify
 @[deprecated (since := "2024-06-07")] alias modifyNth_get?_length := length_modify
 @[deprecated (since := "2024-10-21")] alias getElem?_modifyNth_eq := getElem?_modify_eq
+
+set_option linter.deprecated false in
 @[deprecated getElem?_modify_eq (since := "2024-06-12")]
 theorem get?_modifyNth_eq (f : α → α) (n) (l : List α) :
     (modify f n l).get? n = f <$> l.get? n := by
   simp [getElem?_modify_eq]
+
 @[deprecated (since := "2024-06-12")] alias getElem?_modifyNth_ne := getElem?_modify_ne
+
+set_option linter.deprecated false in
 @[deprecated getElem?_modify_ne (since := "2024-06-12")]
 theorem get?_modifyNth_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
     (modify f m l).get? n = l.get? n := by
   simp [h]
+
 @[deprecated (since := "2024-10-21")] alias exists_of_modifyNth := exists_of_modify
 @[deprecated (since := "2024-10-21")] alias modifyNthTail_eq_take_drop := modifyTailIdx_eq_take_drop
 @[deprecated (since := "2024-10-21")] alias modifyNth_eq_take_drop := modify_eq_take_drop
@@ -723,17 +745,25 @@ theorem get?_modifyNth_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
 theorem exists_of_set' {l : List α} (h : n < l.length) :
     ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ l.set n a' = l₁ ++ a' :: l₂ := by
   rw [set_eq_modify]; exact exists_of_modify _ h
+
+set_option linter.deprecated false in
 @[deprecated getElem?_set_self' (since := "2024-06-12")]
 theorem get?_set_eq (a : α) (n) (l : List α) : (set l n a).get? n = (fun _ => a) <$> l.get? n := by
   simp only [get?_eq_getElem?, getElem?_set_self', Option.map_eq_map]
   rfl
+
+set_option linter.deprecated false in
 @[deprecated getElem?_set_eq_of_lt (since := "2024-06-12")]
 theorem get?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) :
     (set l n a).get? n = some a := by
   rw [get?_eq_getElem?, getElem?_set_self', getElem?_eq_getElem h]; rfl
+
+set_option linter.deprecated false in
 @[deprecated getElem?_set_ne (since := "2024-06-12")]
 theorem get?_set_ne (a : α) {m n} (l : List α) (h : m ≠ n) : (set l m a).get? n = l.get? n := by
   simp [h]
+
+set_option linter.deprecated false in
 @[deprecated getElem?_set (since := "2024-06-12")]
 theorem get?_set (a : α) {m n} (l : List α) :
     (set l m a).get? n = if m = n then (fun _ => a) <$> l.get? n else l.get? n := by
diff --git a/Batteries/Data/List/Perm.lean b/Batteries/Data/List/Perm.lean
index b0c155e0c7..2be98a0281 100644
--- a/Batteries/Data/List/Perm.lean
+++ b/Batteries/Data/List/Perm.lean
@@ -70,7 +70,7 @@ theorem Subperm.filter (p : α → Bool) ⦃l l' : List α⦄ (h : l <+~ l') :
   exact ⟨_, hp.filter p, h.filter p⟩
 
 @[simp] theorem subperm_nil : l <+~ [] ↔ l = [] :=
-  ⟨fun h => length_eq_zero.1 $ Nat.le_zero.1 h.length_le, by rintro rfl; rfl⟩
+  ⟨fun h => length_eq_zero_iff.1 $ Nat.le_zero.1 h.length_le, by rintro rfl; rfl⟩
 
 @[simp] theorem singleton_subperm_iff {α} {l : List α} {a : α} : [a] <+~ l ↔ a ∈ l := by
   refine ⟨fun ⟨s, hla, h⟩ => ?_, fun h => ⟨[a], .rfl, singleton_sublist.mpr h⟩⟩
diff --git a/Batteries/Data/Nat/Bisect.lean b/Batteries/Data/Nat/Bisect.lean
index f692675944..a93c7cbeb1 100644
--- a/Batteries/Data/Nat/Bisect.lean
+++ b/Batteries/Data/Nat/Bisect.lean
@@ -15,10 +15,10 @@ theorem avg_comm (a b : Nat) : avg a b = avg b a := by
   rw [avg, Nat.add_comm]
 
 theorem avg_le_left (h : b ≤ a) : avg a b ≤ a := by
-  apply Nat.div_le_of_le_mul; simp_arith [*]
+  apply Nat.div_le_of_le_mul; simp +arith [*]
 
 theorem avg_le_right (h : a ≤ b) : avg a b ≤ b := by
-  apply Nat.div_le_of_le_mul; simp_arith [*]
+  apply Nat.div_le_of_le_mul; simp +arith [*]
 
 theorem avg_lt_left (h : b < a) : avg a b < a := by
   apply Nat.div_lt_of_lt_mul; omega
@@ -27,10 +27,10 @@ theorem avg_lt_right (h : a < b) : avg a b < b := by
   apply Nat.div_lt_of_lt_mul; omega
 
 theorem le_avg_left (h : a ≤ b) : a ≤ avg a b := by
-  apply (Nat.le_div_iff_mul_le Nat.zero_lt_two).mpr; simp_arith [*]
+  apply (Nat.le_div_iff_mul_le Nat.zero_lt_two).mpr; simp +arith [*]
 
 theorem le_avg_right (h : b ≤ a) : b ≤ avg a b := by
-  apply (Nat.le_div_iff_mul_le Nat.zero_lt_two).mpr; simp_arith [*]
+  apply (Nat.le_div_iff_mul_le Nat.zero_lt_two).mpr; simp +arith [*]
 
 theorem le_add_one_of_avg_eq_left (h : avg a b = a) : b ≤ a + 1 := by
   cases Nat.lt_or_ge b (a+2) with
diff --git a/Batteries/Data/Nat/Lemmas.lean b/Batteries/Data/Nat/Lemmas.lean
index 944c473d33..07419788b3 100644
--- a/Batteries/Data/Nat/Lemmas.lean
+++ b/Batteries/Data/Nat/Lemmas.lean
@@ -197,7 +197,7 @@ theorem ofBits_lt_two_pow (f : Fin n → Bool) : ofBits f < 2 ^ n := by
   apply testBit_lt_two_pow
   apply Nat.lt_of_lt_of_le
   · exact ofBits_lt_two_pow f
-  · exact pow_le_pow_of_le_right Nat.zero_lt_two h
+  · exact pow_le_pow_right Nat.zero_lt_two h
 
 theorem testBit_ofBits (f : Fin n → Bool) :
     (ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false := by
diff --git a/Batteries/Data/PairingHeap.lean b/Batteries/Data/PairingHeap.lean
index 658af68055..6d1912de4d 100644
--- a/Batteries/Data/PairingHeap.lean
+++ b/Batteries/Data/PairingHeap.lean
@@ -118,13 +118,13 @@ theorem Heap.noSibling_tail (le) (s : Heap α) : (s.tail le).NoSibling := by
 
 theorem Heap.size_merge_node (le) (a₁ : α) (c₁ s₁ : Heap α) (a₂ : α) (c₂ s₂ : Heap α) :
     (merge le (.node a₁ c₁ s₁) (.node a₂ c₂ s₂)).size = c₁.size + c₂.size + 2 := by
-  unfold merge; dsimp; split <;> simp_arith [size]
+  unfold merge; dsimp; split <;> simp +arith [size]
 
 theorem Heap.size_merge (le) {s₁ s₂ : Heap α} (h₁ : s₁.NoSibling) (h₂ : s₂.NoSibling) :
     (merge le s₁ s₂).size = s₁.size + s₂.size := by
   match h₁, h₂ with
   | .nil, .nil | .nil, .node _ _ | .node _ _, .nil => simp [merge, size]
-  | .node _ _, .node _ _ => unfold merge; dsimp; split <;> simp_arith [size]
+  | .node _ _, .node _ _ => unfold merge; dsimp; split <;> simp +arith [size]
 
 theorem Heap.size_combine (le) (s : Heap α) :
     (s.combine le).size = s.size := by
@@ -132,7 +132,7 @@ theorem Heap.size_combine (le) (s : Heap α) :
   · rename_i a₁ c₁ a₂ c₂ s
     rw [size_merge le (noSibling_merge _ _ _) (noSibling_combine _ _),
       size_merge_node, size_combine le s]
-    simp_arith [size]
+    simp +arith [size]
   · rfl
 
 theorem Heap.size_deleteMin {s : Heap α} (h : s.NoSibling) (eq : s.deleteMin le = some (a, s')) :
@@ -153,7 +153,7 @@ theorem Heap.size_tail (le) {s : Heap α} (h : s.NoSibling) : (s.tail le).size =
 
 theorem Heap.size_deleteMin_lt {s : Heap α} (eq : s.deleteMin le = some (a, s')) :
     s'.size < s.size := by
-  cases s with cases eq | node a c => simp_arith [size_combine, size]
+  cases s with cases eq | node a c => simp +arith [size_combine, size]
 
 theorem Heap.size_tail?_lt {s : Heap α} : s.tail? le = some s' →
     s'.size < s.size := by
@@ -170,7 +170,7 @@ by repeatedly pulling the minimum element out of the heap.
   match eq : s.deleteMin le with
   | none => pure init
   | some (hd, tl) =>
-    have : tl.size < s.size := by simp_arith [Heap.size_deleteMin_lt eq]
+    have : tl.size < s.size := by simp +arith [Heap.size_deleteMin_lt eq]
     do foldM le tl (← f init hd) f
 termination_by s.size
 
diff --git a/Batteries/Data/RBMap/Depth.lean b/Batteries/Data/RBMap/Depth.lean
index 4e37318816..d9768f74f8 100644
--- a/Batteries/Data/RBMap/Depth.lean
+++ b/Batteries/Data/RBMap/Depth.lean
@@ -26,8 +26,8 @@ theorem size_lt_depth : ∀ t : RBNode α, t.size < 2 ^ t.depth
     rw [size, depth, Nat.add_right_comm, Nat.pow_succ, Nat.mul_two]
     refine Nat.add_le_add
       (Nat.lt_of_lt_of_le a.size_lt_depth ?_) (Nat.lt_of_lt_of_le b.size_lt_depth ?_)
-    · exact Nat.pow_le_pow_of_le_right (by decide) (Nat.le_max_left ..)
-    · exact Nat.pow_le_pow_of_le_right (by decide) (Nat.le_max_right ..)
+    · exact Nat.pow_le_pow_right (by decide) (Nat.le_max_left ..)
+    · exact Nat.pow_le_pow_right (by decide) (Nat.le_max_right ..)
 
 /--
 `depthLB c n` is the best upper bound on the depth of any balanced red-black tree
@@ -71,7 +71,7 @@ theorem Balanced.le_size : @Balanced α t c n → 2 ^ depthLB c n ≤ t.size + 1
   | .black hl hr => by
     rw [size, Nat.add_right_comm (size _), Nat.add_assoc, depthLB, Nat.pow_succ, Nat.mul_two]
     refine Nat.add_le_add (Nat.le_trans ?_ hl.le_size) (Nat.le_trans ?_ hr.le_size) <;>
-      exact Nat.pow_le_pow_of_le_right (by decide) (depthLB_le ..)
+      exact Nat.pow_le_pow_right (by decide) (depthLB_le ..)
 
 theorem Balanced.depth_bound (h : @Balanced α t c n) : t.depth ≤ 2 * (t.size + 1).log2 :=
   Nat.le_trans h.depth_le <| Nat.le_trans (depthUB_le_two_depthLB ..) <|
diff --git a/Batteries/Data/RBMap/Lemmas.lean b/Batteries/Data/RBMap/Lemmas.lean
index b32beaf675..f3989b7c78 100644
--- a/Batteries/Data/RBMap/Lemmas.lean
+++ b/Batteries/Data/RBMap/Lemmas.lean
@@ -111,7 +111,7 @@ instance (cmp cut) [@IsCut α cmp cut] : IsCut (flip cmp) (cut · |>.swap) where
 `IsStrictCut` upgrades the `IsCut` property to ensure that at most one element of the tree
 can match the cut, and hence `find?` will return the unique such element if one exists.
 -/
-class IsStrictCut (cmp : α → α → Ordering) (cut : α → Ordering) extends IsCut cmp cut : Prop where
+class IsStrictCut (cmp : α → α → Ordering) (cut : α → Ordering) : Prop extends IsCut cmp cut where
   /-- If `cut = x`, then `cut` and `x` have compare the same with respect to other elements. -/
   exact [TransCmp cmp] : cut x = .eq → cmp x y = cut y
 
diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean
index 37951fbec6..99f101db5e 100644
--- a/Batteries/Data/Rat/Basic.lean
+++ b/Batteries/Data/Rat/Basic.lean
@@ -107,7 +107,7 @@ def divInt : Int → Int → Rat
 `Rat.ofScientific_true_def`, or `Rat.ofScientific_false_def` instead.) -/
 @[irreducible] protected def ofScientific (m : Nat) (s : Bool) (e : Nat) : Rat :=
   if s then
-    Rat.normalize m (10 ^ e) <| Nat.ne_of_gt <| Nat.pos_pow_of_pos _ (by decide)
+    Rat.normalize m (10 ^ e) <| Nat.ne_of_gt <| Nat.pow_pos (by decide)
   else
     (m * 10 ^ e : Nat)
 
diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean
index 007a57d75d..0aeea51a36 100644
--- a/Batteries/Data/UInt.lean
+++ b/Batteries/Data/UInt.lean
@@ -10,8 +10,6 @@ import Batteries.Classes.Order
 @[ext] theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
-
 @[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat := rfl
 
 @[simp] theorem UInt8.toUInt32_toNat (x : UInt8) : x.toUInt32.toNat = x.toNat := rfl
@@ -26,8 +24,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
 @[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
-
 @[simp] theorem UInt16.toUInt8_toNat (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
 
 @[simp] theorem UInt16.toUInt32_toNat (x : UInt16) : x.toUInt32.toNat = x.toNat := rfl
@@ -42,8 +38,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
 @[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
-
 @[simp] theorem UInt32.toUInt8_toNat (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
 
 @[simp] theorem UInt32.toUInt16_toNat (x : UInt32) : x.toUInt16.toNat = x.toNat % 2 ^ 16 := rfl
@@ -58,8 +52,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
 @[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
-
 @[simp] theorem UInt64.toUInt8_toNat (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
 
 @[simp] theorem UInt64.toUInt16_toNat (x : UInt64) : x.toUInt16.toNat = x.toNat % 2 ^ 16 := rfl
@@ -74,22 +66,6 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
 @[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
-  rw [USize.size]
-
-theorem USize.le_size : 2 ^ 32 ≤ USize.size := by
-  rw [size_eq]
-  apply Nat.pow_le_pow_of_le_right (by decide)
-  cases System.Platform.numBits_eq <;> simp_arith [*]
-
-theorem USize.size_le : USize.size ≤ 2 ^ 64 := by
-  rw [size_eq]
-  apply Nat.pow_le_pow_of_le_right (by decide)
-  cases System.Platform.numBits_eq <;> simp_arith [*]
-
-theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by
-  rw [←USize.size_eq]; exact x.val.isLt
-
 @[simp] theorem USize.toUInt64_toNat (x : USize) : x.toUInt64.toNat = x.toNat := by
   simp only [USize.toUInt64, UInt64.toNat]; rfl
 
diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean
index fc093a0f16..9d337664c5 100644
--- a/Batteries/Data/UnionFind/Basic.lean
+++ b/Batteries/Data/UnionFind/Basic.lean
@@ -43,14 +43,14 @@ theorem lt_of_parentD : parentD arr i ≠ i → i < arr.size :=
 
 theorem parentD_set {arr : Array UFNode} {x v i h} :
     parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
-  rw [parentD]; simp only [Array.size_set, Array.get_eq_getElem, parentD]
+  rw [parentD]; simp only [Array.size_set, parentD]
   split
   · split <;> simp_all
   · split <;> [(subst i; cases ‹¬_› h); rfl]
 
 theorem rankD_set {arr : Array UFNode} {x v i h} :
     rankD (arr.set x v h) i = if x = i then v.rank else rankD arr i := by
-  rw [rankD]; simp only [Array.size_set, Array.get_eq_getElem, rankD]
+  rw [rankD]; simp only [Array.size_set, rankD]
   split
   · split <;> simp_all
   · split <;> [(subst i; cases ‹¬_› h); rfl]
@@ -145,7 +145,7 @@ theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank <
   let rec go : ∀ {l} {x : UFNode}, x ∈ l → x.rank ≤ List.foldr (max ·.rank) 0 l
     | a::l, _, List.Mem.head _ => by dsimp; apply Nat.le_max_left
     | a::l, _, .tail _ h => by dsimp; exact Nat.le_trans (go h) (Nat.le_max_right ..)
-  simp only [Array.get_eq_getElem, rankMax, ← Array.foldr_toList]
+  simp only [rankMax, ← Array.foldr_toList]
   exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem _)
 
 theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
@@ -155,11 +155,11 @@ theorem rankD_lt_rankMax (self : UnionFind) (i : Nat) :
 theorem lt_rankMax (self : UnionFind) (i : Nat) : self.rank i < self.rankMax := rankD_lt_rankMax ..
 
 theorem push_rankD (arr : Array UFNode) : rankD (arr.push ⟨arr.size, 0⟩) i = rankD arr i := by
-  simp only [rankD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
+  simp only [rankD, Array.size_push, Array.getElem_push, dite_eq_ite]
   split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
 
 theorem push_parentD (arr : Array UFNode) : parentD (arr.push ⟨arr.size, 0⟩) i = parentD arr i := by
-  simp only [parentD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]
+  simp only [parentD, Array.size_push, Array.getElem_push, dite_eq_ite]
   split <;> split <;> try simp
   · exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)
   · cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
@@ -168,7 +168,7 @@ theorem push_parentD (arr : Array UFNode) : parentD (arr.push ⟨arr.size, 0⟩)
 def push (self : UnionFind) : UnionFind where
   arr := self.arr.push ⟨self.arr.size, 0⟩
   parentD_lt {i} := by
-    simp only [Array.size_push, push_parentD]; simp only [parentD, Array.get_eq_getElem]
+    simp only [Array.size_push, push_parentD]; simp only [parentD]
     split <;> [exact fun _ => Nat.lt_succ_of_lt (self.parent'_lt ..); exact id]
   rankD_lt := by simp only [push_parentD, ne_eq, push_rankD]; exact self.rank_lt
 
@@ -206,7 +206,7 @@ theorem parent_rootD (self : UnionFind) (x : Nat) :
     self.parent (self.rootD x) = self.rootD x := by
   rw [rootD]
   split
-  · simp [parentD, parent_root, -Array.get_eq_getElem]
+  · simp [parentD, parent_root]
   · simp [parentD_of_not_lt, *]
 
 @[nolint unusedHavesSuffices]
@@ -278,7 +278,7 @@ termination_by self.rankMax - self.rank x
 theorem findAux_root {self : UnionFind} {x : Fin self.size} :
     (findAux self x).root = self.root x := by
   rw [findAux, root]
-  simp only [Array.length_toList, Array.get_eq_getElem, dite_eq_ite]
+  simp only [Array.length_toList, dite_eq_ite]
   split <;> simp only
   have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)
   exact findAux_root
@@ -292,7 +292,7 @@ theorem findAux_s {self : UnionFind} {x : Fin self.size} :
   rw [show self.rootD _ = (self.findAux ⟨_, self.parent'_lt x x.2⟩).root from _]
   · rw [findAux]; split <;> rfl
   · rw [← rootD_parent, parent, parentD_eq]
-    simp only [rootD, Array.get_eq_getElem, Array.length_toList, findAux_root]
+    simp only [rootD, Array.length_toList, findAux_root]
     apply dif_pos
     exact parent'_lt ..
 
@@ -304,9 +304,9 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} :
     have := lt_of_parentD (by rwa [parentD_eq])
     rw [rankD_eq (by simp [FindAux.size_eq, h]), Array.getElem_modify]
     split <;>
-      simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem]
+      simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩)]
   else
-    simp only [rankD, Array.length_toList, Array.get_eq_getElem, rank]
+    simp only [rankD, Array.length_toList, rank]
     rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h]
 termination_by self.rankMax - self.rank x
 
@@ -314,13 +314,13 @@ theorem parentD_findAux {self : UnionFind} {x : Fin self.size} :
     parentD (findAux self x).s i =
     if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt _ x.2⟩).s i := by
   rw [findAux_s]; split <;> [split; skip]
-  · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *, -Array.get_eq_getElem]
-  · rw [findAux_s]; simp [*, -Array.get_eq_getElem]
+  · subst i; rw [rootD_eq_self.2 _] <;> simp [parentD_eq, *]
+  · rw [findAux_s]; simp [*]
   · next h =>
     rw [parentD]; split <;> rename_i h'
     · rw [Array.getElem_modify (by simpa using h')]
       simp only [Array.length_toList, @eq_comm _ i]
-      split <;> simp [← parentD_eq, -Array.get_eq_getElem]
+      split <;> simp [← parentD_eq]
     · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')]
       rw [parentD, dif_neg]; simpa using h'
 
@@ -462,10 +462,10 @@ theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
         arr[y.1].rank + 1
       else rankD arr i) :
     ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i) := by
-  simp [hP, hR, -Array.get_eq_getElem] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
+  simp [hP, hR] at *; split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
     split <;> rename_i h₂ <;> intro h
   · simp [h₂] at h
-  · simp only [rankD_eq, x.2, y.2, Array.get_eq_getElem]
+  · simp only [rankD_eq, x.2, y.2]
     split <;> rename_i h₃
     · rw [← h₃]; apply Nat.lt_succ_self
     · exact Nat.lt_of_le_of_ne H h₃
@@ -483,10 +483,10 @@ theorem setParent_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
     let arr' := arr.set x ⟨y, arr[x].rank⟩
     parentD arr' i ≠ i → rankD arr' i < rankD arr' (parentD arr' i) :=
   setParentBump_rankD_lt (.inl h) (Nat.le_of_lt h) rankD_lt parentD_set
-    (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq, -Array.get_eq_getElem])
+    (by simp [rankD_set, Nat.ne_of_lt h, rankD_eq])
 
 @[simp] theorem linkAux_size : (linkAux self x y).size = self.size := by
-  simp only [linkAux, Array.get_eq_getElem]
+  simp only [linkAux]
   split <;> [rfl; split] <;> [skip; split] <;> simp
 
 /-- Link a union-find node to a root node. -/
@@ -494,7 +494,7 @@ def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) :
   arr := linkAux self.arr x y
   parentD_lt h := by
     simp only [Array.length_toList, linkAux_size] at *
-    simp only [linkAux, Array.get_eq_getElem]
+    simp only [linkAux]
     split <;> [skip; split <;> [skip; split]]
     · exact self.parentD_lt h
     · rw [parentD_set]; split <;> [exact x.2; exact self.parentD_lt h]
@@ -504,7 +504,7 @@ def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) :
     · rw [parentD_set]; split <;> [exact y.2; exact self.parentD_lt h]
   rankD_lt := by
     rw [parent, parentD_eq] at yroot
-    simp only [linkAux, Array.get_eq_getElem, ne_eq]
+    simp only [linkAux, ne_eq]
     split <;> [skip; split <;> [skip; split]]
     · exact self.rankD_lt
     · exact setParent_rankD_lt ‹_› self.rankD_lt
@@ -512,10 +512,10 @@ def link (self : UnionFind) (x y : Fin self.size) (yroot : self.parent y = y) :
         simp only [parentD_set, ite_eq_right_iff]
         rintro rfl
         simp [*, parentD_eq]) fun {i} => ?_
-      simp only [rankD_set, Fin.eta, Array.get_eq_getElem]
+      simp only [rankD_set, Fin.eta]
       split
       · simp_all
-      · simp_all only [Array.get_eq_getElem, Array.length_toList, Nat.lt_irrefl, not_false_eq_true,
+      · simp_all only [Array.length_toList, Nat.lt_irrefl, not_false_eq_true,
           and_true, ite_false, ite_eq_right_iff]
         rintro rfl
         simp [rankD_eq, *]
diff --git a/Batteries/Data/Vector/Monadic.lean b/Batteries/Data/Vector/Monadic.lean
index e80f35c854..b51a1f1a87 100644
--- a/Batteries/Data/Vector/Monadic.lean
+++ b/Batteries/Data/Vector/Monadic.lean
@@ -4,44 +4,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Batteries.Classes.SatisfiesM
-import Batteries.Control.Monad
 import Batteries.Data.Array.Monadic
 
 namespace Vector
 
-theorem toArray_mapFinIdxM [Monad m] [LawfulMonad m]
-    (a : Vector α n) (f : (i : Nat) → α → (h : i < n) → m β) :
-    toArray <$> a.mapFinIdxM f = a.toArray.mapFinIdxM
-      (fun i x h => f i x (size_toArray a ▸ h)) := by
-  let rec go (i j : Nat) (inv : i + j = n) (bs : Vector β (n - i)) :
-      toArray <$> mapFinIdxM.map a f i j inv bs
-      = Array.mapFinIdxM.map a.toArray (fun i x h => f i x (size_toArray a ▸ h))
-        i j (size_toArray _ ▸ inv) bs.toArray := by
-    match i with
-    | 0 => simp only [mapFinIdxM.map, map_pure, Array.mapFinIdxM.map, Nat.sub_zero]
-    | k + 1 =>
-      simp only [mapFinIdxM.map, map_bind, Array.mapFinIdxM.map, getElem_toArray]
-      conv => lhs; arg 2; intro; rw [go]
-      rfl
-  simp only [mapFinIdxM, Array.mapFinIdxM, size_toArray]
-  exact go _ _ _ _
-
-theorem toArray_mapIdxM [Monad m] [LawfulMonad m] (a : Vector α n) (f : Nat → α → m β) :
-    toArray <$> a.mapIdxM f = a.toArray.mapIdxM f := by
-  exact toArray_mapFinIdxM _ _
-
 theorem mapM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
     (a : Array α) (h : a.size = n) (f : α → m β) :
     (Vector.mk a h).mapM f =
       (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying (Array.size_mapM f a) := by
-  rw [← LawfulMonad.map_inj_right Vector.toArray_inj.mp]
+  rw [← _root_.map_inj_right Vector.toArray_inj.mp]
   simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapM]
 
 theorem mapIdxM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
     (a : Array α) (h : a.size = n) (f : Nat → α → m β) :
     (Vector.mk a h).mapIdxM f =
       (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying (Array.size_mapIdxM a f) := by
-  rw [← LawfulMonad.map_inj_right Vector.toArray_inj.mp]
+  rw [← _root_.map_inj_right Vector.toArray_inj.mp]
   simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapIdxM]
 
 theorem mapFinIdxM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
@@ -49,5 +27,5 @@ theorem mapFinIdxM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
     (Vector.mk a h).mapFinIdxM f =
       (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying
         (Array.size_mapFinIdxM a (fun i a h' => f i a (h ▸ h'))) := by
-  rw [← LawfulMonad.map_inj_right Vector.toArray_inj.mp]
+  rw [← _root_.map_inj_right Vector.toArray_inj.mp]
   simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapFinIdxM]
diff --git a/BatteriesTest/array.lean b/BatteriesTest/array.lean
index e94478ddb6..82e4473088 100644
--- a/BatteriesTest/array.lean
+++ b/BatteriesTest/array.lean
@@ -9,8 +9,8 @@ variable (v d : α)
 variable (g : i < (a.set! i v).size)
 variable (j_lt : j < (a.set! i v).size)
 
-#check_simp (a.set! i v).get i g ~> v
-#check_simp (a.set! i v).get! i ~> (a.setIfInBounds i v)[i]!
+#check_simp (a.set! i v)[i] ~> v
+#check_simp (a.set! i v)[i]! ~> (a.setIfInBounds i v)[i]!
 #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d
 #check_simp (a.set! i v)[i] ~> v
 
diff --git a/BatteriesTest/float.lean b/BatteriesTest/float.lean
index 7d8e7363e1..c1440fdf20 100644
--- a/BatteriesTest/float.lean
+++ b/BatteriesTest/float.lean
@@ -50,8 +50,8 @@ import Batteries.Lean.Float
 #guard Nat.divFloat 2 3 == (2 / 3 : Float)
 #guard Nat.divFloat 100 17 == (100 / 17 : Float)
 #guard Nat.divFloat 5000000000000000 1 == (5000000000000000 : Float)
-#guard [0,0,0,1,1,1,2,2,2,2,2,3,3,3,4,4,4].enum.all fun p =>
-  Nat.divFloat (5000000000000000*4+p.1) 4 == (5000000000000000+p.2).toFloat
+#guard [0,0,0,1,1,1,2,2,2,2,2,3,3,3,4,4,4].zipIdx.all fun p =>
+  Nat.divFloat (5000000000000000*4+p.2) 4 == (5000000000000000+p.1).toFloat
 #guard Nat.divFloat ((2^53-1)*(2^(1024-53))) 1 == ((2^53-1)*(2^(1024-53)))
 #guard Nat.divFloat (((2^53-1)*4+1)*(2^(1024-53))) 4 == ((2^53-1)*(2^(1024-53)))
 #guard Nat.divFloat (((2^53-1)*4+2)*(2^(1024-53))) 4 == Float.inf
diff --git a/BatteriesTest/nondet.lean b/BatteriesTest/nondet.lean
index 1669c8109f..4ed586f334 100644
--- a/BatteriesTest/nondet.lean
+++ b/BatteriesTest/nondet.lean
@@ -17,7 +17,7 @@ def record (n : Nat) : M Unit := do
   discard <| restoreState (n :: (← saveState))
 
 def iotaM [Monad m] [Alternative m] [MonadBacktrack σ m] (n : Nat) : Nondet m Nat :=
-  Nondet.ofList (List.iota n)
+  Nondet.ofList (List.range' 1 n).reverse
 
 /-- info: (52, []) -/
 #guard_msgs in
@@ -39,7 +39,7 @@ def x : Nondet M Nat :=
 #guard_msgs in
 #eval show MetaM (Nat × List Nat) from StateT.run x.head []
 
-def divisors (n : Nat) : List Nat := List.iota (n - 1) |>.filter fun m => n % m = 0
+def divisors (n : Nat) : List Nat := List.range' 1 (n - 1) |>.reverse.filter fun m => n % m = 0
 example : divisors 52 = [26, 13, 4, 2, 1] := rfl
 
 def divisorsM [Monad m] [MonadBacktrack σ m] (n : Nat) : Nondet m Nat :=
diff --git a/lean-toolchain b/lean-toolchain
index 5499a2460c..62e3298fa6 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0-rc1