diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean
index 1b2de5f1b6..e3c70c0706 100644
--- a/doc/examples/bintree.lean
+++ b/doc/examples/bintree.lean
@@ -179,7 +179,7 @@ local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
   `(tactic|
     (have h : $lhs = $rhs :=
        -- TODO: replace with linarith
-       by simp_arith at *; apply Nat.le_antisymm <;> assumption
+       by simp +arith at *; apply Nat.le_antisymm <;> assumption
      try subst $lhs))
 
 /-!
diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean
index e98b054cb2..dc5ffbada8 100644
--- a/src/Init/Data/Array/BasicAux.lean
+++ b/src/Init/Data/Array/BasicAux.lean
@@ -17,13 +17,13 @@ theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : a
 private theorem List.size_toArrayAux (as : List α) (bs : Array α) : (as.toArrayAux bs).size = as.length + bs.size := by
   induction as generalizing bs with
   | nil => simp [toArrayAux]
-  | cons a as ih => simp_arith [toArrayAux, *]
+  | cons a as ih => simp +arith [toArrayAux, *]
 
 private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Array α} (h : as.toArrayAux cs = bs.toArrayAux ds) (hlen : cs.size = ds.size) : as = bs ∧ cs = ds := by
   match as, bs with
   | [], []    => simp [toArrayAux] at h; simp [h]
-  | a::as, [] => simp [toArrayAux] at h; rw [← h] at hlen; simp_arith [size_toArrayAux] at hlen
-  | [], b::bs => simp [toArrayAux] at h; rw [h] at hlen; simp_arith [size_toArrayAux] at hlen
+  | a::as, [] => simp [toArrayAux] at h; rw [← h] at hlen; simp +arith [size_toArrayAux] at hlen
+  | [], b::bs => simp [toArrayAux] at h; rw [h] at hlen; simp +arith [size_toArrayAux] at hlen
   | a::as, b::bs =>
     simp [toArrayAux] at h
     have : (cs.push a).size = (ds.push b).size := by simp [*]
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 894e91ccca..978a5e38ed 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1675,7 +1675,7 @@ theorem getElem_append_right' (l₁ : Array α) {l₂ : Array α} {i : Nat} (hi
   rw [getElem_append_right] <;> simp [*, Nat.le_add_left]
 
 theorem getElem_of_append {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂) (h : l₁.size = i) :
-    l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
+    l[i]'(eq ▸ h ▸ by simp +arith) = a := Option.some.inj <| by
   rw [← getElem?_eq_getElem, eq, getElem?_append_left (by simp; omega), ← h]
   simp
 
@@ -2337,10 +2337,10 @@ theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j
           ← getElem?_toList]
         split <;> rename_i h₂
         · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false]
-          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_reverse' (j+1) i (Eq.trans (by simp +arith) h)).symm
         split <;> rename_i h₃
         · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and]
-          exact (List.getElem?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm
+          exact (List.getElem?_reverse' i (j+1) (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₂)))]
     · rw [H]; split <;> rename_i h₂
diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean
index 284b03e58c..14a1412643 100644
--- a/src/Init/Data/Array/Mem.lean
+++ b/src/Init/Data/Array/Mem.lean
@@ -12,11 +12,11 @@ namespace Array
 
 theorem sizeOf_lt_of_mem [SizeOf α] {as : Array α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   cases as with | _ as =>
-  exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp_arith)
+  exact Nat.lt_trans (List.sizeOf_lt_of_mem h.val) (by simp +arith)
 
 theorem sizeOf_get [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) : sizeOf (as.get i h) < sizeOf as := by
   cases as with | _ as =>
-  simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp_arith)
+  simpa using Nat.lt_trans (List.sizeOf_get _ ⟨i, h⟩) (by simp +arith)
 
 @[simp] theorem sizeOf_getElem [SizeOf α] (as : Array α) (i : Nat) (h : i < as.size) :
   sizeOf (as[i]'h) < sizeOf as := sizeOf_get _ _ h
@@ -29,8 +29,8 @@ macro "array_get_dec" : tactic =>
     -- subsumed by simp
     -- | with_reducible apply sizeOf_get
     -- | with_reducible apply sizeOf_getElem
-    | (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_get ..)); simp_arith
-    | (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_getElem ..)); simp_arith
+    | (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_get ..)); simp +arith
+    | (with_reducible apply Nat.lt_of_lt_of_le (sizeOf_getElem ..)); simp +arith
     )
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_get_dec)
@@ -45,7 +45,7 @@ macro "array_mem_dec" : tactic =>
     | with_reducible
         apply Nat.lt_of_lt_of_le (Array.sizeOf_lt_of_mem ?h)
         case' h => assumption
-      simp_arith)
+      simp +arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| array_mem_dec)
 
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index e9c81df360..d2db35e9ae 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -178,15 +178,15 @@ theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.
   induction as generalizing i with
   | nil => cases i with
     | zero => simp [List.get]
-    | succ => simp_arith at h'
+    | succ => simp +arith at h'
   | cons a as ih =>
     cases i with simp at h
     | succ i => apply ih; simp [h]
 
 theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < sizeOf as := by
   induction h with
-  | head => simp_arith
-  | tail _ _ ih => exact Nat.lt_trans ih (by simp_arith)
+  | head => simp +arith
+  | tail _ _ ih => exact Nat.lt_trans ih (by simp +arith)
 
 /-- This tactic, added to the `decreasing_trivial` toolbox, proves that
 `sizeOf a < sizeOf as` when `a ∈ as`, which is useful for well founded recursions
@@ -197,7 +197,7 @@ macro "sizeOf_list_dec" : tactic =>
     | with_reducible
         apply Nat.lt_of_lt_of_le (sizeOf_lt_of_mem ?h)
         case' h => assumption
-      simp_arith)
+      simp +arith)
 
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| sizeOf_list_dec)
 
@@ -211,8 +211,8 @@ theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs =
 theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs := by
   match as, cs with
   | [], []       => rfl
-  | [], c::cs    => have aux := congrArg length h; simp_arith at aux
-  | a::as, []    => have aux := congrArg length h; simp_arith at aux
+  | [], c::cs    => have aux := congrArg length h; simp +arith at aux
+  | a::as, []    => have aux := congrArg length h; simp +arith at aux
   | a::as, c::cs => injection h with h₁ h₂; subst h₁; rw [append_cancel_right h₂]
 
 @[simp] theorem append_cancel_left_eq (as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs) := by
@@ -227,11 +227,11 @@ theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as
 
 theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as := by
   match as, i with
-  | a::as, ⟨0, _⟩  => simp_arith [get]
+  | a::as, ⟨0, _⟩  => simp +arith [get]
   | a::as, ⟨i+1, h⟩ =>
     have ih := sizeOf_get as ⟨i, Nat.le_of_succ_le_succ h⟩
     apply Nat.lt_trans ih
-    simp_arith
+    simp +arith
 
 theorem not_lex_antisymm [DecidableEq α] {r : α → α → Prop} [DecidableRel r]
     (antisymm : ∀ x y : α, ¬ r x y → ¬ r y x → x = y)
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index a627bb4bb7..ff3296e6a9 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1563,7 +1563,7 @@ theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi :
   rw [getElem_append_right] <;> simp [*, le_add_left]
 
 theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = i) :
-    l[i]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by
+    l[i]'(eq ▸ h ▸ by simp +arith) = a := Option.some.inj <| by
   rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h]
   simp
 
diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean
index 5bbd70c983..1b7028735c 100644
--- a/src/Init/Data/List/Sort/Lemmas.lean
+++ b/src/Init/Data/List/Sort/Lemmas.lean
@@ -152,8 +152,8 @@ theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
   | a::l, b::r =>
     rw [cons_merge_cons]
     split
-    · simp_arith [length_merge s l (b::r)]
-    · simp_arith [length_merge s (a::l) r]
+    · simp +arith [length_merge s l (b::r)]
+    · simp +arith [length_merge s (a::l) r]
 
 /--
 The elements of `merge le xs ys` are exactly the elements of `xs` and `ys`.
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 50c161fb8a..529202a824 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -1011,7 +1011,7 @@ theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x
   | 0 => simp
   | x + 1 =>
     rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]
-    simp_arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
+    simp +arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
 
 theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   match x with
diff --git a/src/Init/Data/Nat/Power2.lean b/src/Init/Data/Nat/Power2.lean
index 46b1b29599..cf777a2097 100644
--- a/src/Init/Data/Nat/Power2.lean
+++ b/src/Init/Data/Nat/Power2.lean
@@ -9,7 +9,7 @@ import Init.Data.Nat.Linear
 namespace Nat
 
 theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
-  have : power * 2 = power + power := by simp_arith
+  have : power * 2 = power + power := by simp +arith
   rw [this, Nat.sub_add_eq]
   exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁
 
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 03cb47b39f..69d0e79537 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -1509,25 +1509,35 @@ This will rewrite with all equation lemmas, which can be used to
 partially evaluate many definitions. -/
 declare_simp_like_tactic simpAutoUnfold "simp! " (autoUnfold := true)
 
-/-- `simp_arith` is shorthand for `simp` with `arith := true` and `decide := true`.
-This enables the use of normalization by linear arithmetic. -/
-declare_simp_like_tactic simpArith "simp_arith " (arith := true) (decide := true)
+/--
+`simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`.
+Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
+-/
+syntax (name := simpArith) "simp_arith " optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
-/-- `simp_arith!` is shorthand for `simp_arith` with `autoUnfold := true`.
-This will rewrite with all equation lemmas, which can be used to
-partially evaluate many definitions. -/
-declare_simp_like_tactic simpArithAutoUnfold "simp_arith! " (arith := true) (autoUnfold := true) (decide := true)
+/--
+`simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`.
+Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
+-/
+syntax (name := simpArithBang) "simp_arith! " optConfig (discharger)? (&" only")? (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
 /-- `simp_all!` is shorthand for `simp_all` with `autoUnfold := true`.
 This will rewrite with all equation lemmas, which can be used to
 partially evaluate many definitions. -/
 declare_simp_like_tactic (all := true) simpAllAutoUnfold "simp_all! " (autoUnfold := true)
 
-/-- `simp_all_arith` combines the effects of `simp_all` and `simp_arith`. -/
-declare_simp_like_tactic (all := true) simpAllArith "simp_all_arith " (arith := true) (decide := true)
+/--
+`simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`.
+Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
+-/
+syntax (name := simpAllArith) "simp_all_arith" optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic
+
+/--
+`simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`.
+Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
+-/
+syntax (name := simpAllArithBang) "simp_all_arith!" optConfig (discharger)? (&" only")? (" [" (simpErase <|> simpLemma),* "]")? : tactic
 
-/-- `simp_all_arith!` combines the effects of `simp_all`, `simp_arith` and `simp!`. -/
-declare_simp_like_tactic (all := true) simpAllArithAutoUnfold "simp_all_arith! " (arith := true) (autoUnfold := true) (decide := true)
 
 /-- `dsimp!` is shorthand for `dsimp` with `autoUnfold := true`.
 This will rewrite with all equation lemmas, which can be used to
diff --git a/src/Init/SizeOfLemmas.lean b/src/Init/SizeOfLemmas.lean
index ce0d077d3f..516f1a1f56 100644
--- a/src/Init/SizeOfLemmas.lean
+++ b/src/Init/SizeOfLemmas.lean
@@ -9,28 +9,28 @@ import Init.SizeOf
 import Init.Data.Nat.Linear
 
 @[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
-  cases a; simp_arith
+  cases a; simp +arith
 
 @[simp] protected theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1 := by
-  cases a; simp_arith
+  cases a; simp +arith
 
 @[simp] protected theorem UInt8.sizeOf (a : UInt8) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [UInt8.toNat, BitVec.toNat]
+  cases a; simp +arith [UInt8.toNat, BitVec.toNat]
 
 @[simp] protected theorem UInt16.sizeOf (a : UInt16) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [UInt16.toNat, BitVec.toNat]
+  cases a; simp +arith [UInt16.toNat, BitVec.toNat]
 
 @[simp] protected theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [UInt32.toNat, BitVec.toNat]
+  cases a; simp +arith [UInt32.toNat, BitVec.toNat]
 
 @[simp] protected theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [UInt64.toNat, BitVec.toNat]
+  cases a; simp +arith [UInt64.toNat, BitVec.toNat]
 
 @[simp] protected theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3 := by
-  cases a; simp_arith [USize.toNat, BitVec.toNat]
+  cases a; simp +arith [USize.toNat, BitVec.toNat]
 
 @[simp] protected theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4 := by
-  cases a; simp_arith [Char.toNat]
+  cases a; simp +arith [Char.toNat]
 
 @[simp] protected theorem Subtype.sizeOf {α : Sort u_1} {p : α → Prop} (s : Subtype p) : sizeOf s = sizeOf s.val + 1 := by
   cases s; simp
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 2524a50044..97159e7fc6 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1797,7 +1797,7 @@ macro_rules | `(‹$type›) => `((by assumption : $type))
 by the notation `arr[i]` to prove any side conditions that arise when
 constructing the term (e.g. the index is in bounds of the array).
 The default behavior is to just try `trivial` (which handles the case
-where `i < arr.size` is in the context) and `simp_arith` and `omega`
+where `i < arr.size` is in the context) and `simp +arith` and `omega`
 (for doing linear arithmetic in the index).
 -/
 syntax "get_elem_tactic_trivial" : tactic
diff --git a/src/Lean/Compiler/LCNF/AlphaEqv.lean b/src/Lean/Compiler/LCNF/AlphaEqv.lean
index 73e2d67150..cc907ca015 100644
--- a/src/Lean/Compiler/LCNF/AlphaEqv.lean
+++ b/src/Lean/Compiler/LCNF/AlphaEqv.lean
@@ -69,7 +69,7 @@ def eqvLetValue (e₁ e₂ : LetValue) : EqvM Bool := do
     let rec @[specialize] go (i : Nat) : EqvM Bool := do
       if h : i < params₁.size then
         let p₁ := params₁[i]
-        have : i < params₂.size := by simp_all_arith
+        have : i < params₂.size := by simp_all +arith
         let p₂ := params₂[i]
         unless (← eqvType p₁.type p₂.type) do return false
         withFVar p₁.fvarId p₂.fvarId do
diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean
index 11e86446a4..37461bc4eb 100644
--- a/src/Lean/Compiler/LCNF/PassManager.lean
+++ b/src/Lean/Compiler/LCNF/PassManager.lean
@@ -47,7 +47,7 @@ structure Pass where
   Resulting phase.
   -/
   phaseOut : Phase := phase
-  phaseInv : phaseOut ≥ phase := by simp_arith
+  phaseInv : phaseOut ≥ phase := by simp +arith +decide
   /--
   The name of the `Pass`
   -/
diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean
index b2659ca662..0a383c4204 100644
--- a/src/Lean/Elab/Tactic.lean
+++ b/src/Lean/Elab/Tactic.lean
@@ -50,3 +50,4 @@ import Lean.Elab.Tactic.Try
 import Lean.Elab.Tactic.AsAuxLemma
 import Lean.Elab.Tactic.TreeTacAttr
 import Lean.Elab.Tactic.ExposeNames
+import Lean.Elab.Tactic.SimpArith
diff --git a/src/Lean/Elab/Tactic/SimpArith.lean b/src/Lean/Elab/Tactic/SimpArith.lean
new file mode 100644
index 0000000000..393d68968e
--- /dev/null
+++ b/src/Lean/Elab/Tactic/SimpArith.lean
@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Elab.Tactic.Simp
+import Lean.Meta.Tactic.TryThis
+
+namespace Lean.Elab.Tactic
+
+private def addConfigItem (stx : Syntax) (item : Syntax) : Syntax :=
+  let optConfig := stx[1]
+  let optConfig := optConfig.modifyArg 0 fun arg => mkNullNode (#[item] ++ arg.getArgs)
+  stx.setArg 1 optConfig
+
+set_option hygiene false in
+private def addArith (stx : Syntax) : CoreM Syntax :=
+  return addConfigItem stx (← `(Lean.Parser.Tactic.configItem| +arith))
+
+set_option hygiene false in
+private def addDecide (stx : Syntax) : CoreM Syntax :=
+  return addConfigItem stx (← `(Lean.Parser.Tactic.configItem| +decide))
+
+private def setKind (stx : Syntax) (str : String) (kind : SyntaxNodeKind) : Syntax :=
+  let stx := stx.setKind kind
+  stx.setArg 0 (mkAtom str)
+
+private def addSuggestions (stx : Syntax) (tokenNew : String) (kindNew : SyntaxNodeKind) : MetaM Unit := do
+  let stx' := setKind stx tokenNew kindNew
+  let stx' := stx'.unsetTrailing
+  let s₁ : TSyntax `tactic := ⟨← addArith stx'⟩
+  let s₂ : TSyntax `tactic := ⟨← addArith (← addDecide stx')⟩
+  Meta.Tactic.TryThis.addSuggestions stx[0] #[s₁, s₂] (origSpan? := (← getRef))
+
+@[builtin_tactic Lean.Parser.Tactic.simpArith] def evalSimpArith : Tactic := fun stx => do
+  addSuggestions stx "simp" ``Parser.Tactic.simp
+  throwError "`simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
+
+@[builtin_tactic Lean.Parser.Tactic.simpArithBang] def evalSimpArithBang : Tactic := fun stx => do
+  addSuggestions stx "simp!" ``Parser.Tactic.simpAutoUnfold
+  throwError "`simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
+
+@[builtin_tactic Lean.Parser.Tactic.simpAllArith] def evalSimpAllArith : Tactic := fun stx => do
+  addSuggestions stx "simp_all" ``Parser.Tactic.simpAll
+  throwError "`simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
+
+@[builtin_tactic Lean.Parser.Tactic.simpAllArithBang] def evalSimpAllArithBang : Tactic := fun stx => do
+  addSuggestions stx "simp_all!" ``Parser.Tactic.simpAllAutoUnfold
+  throwError "`simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented."
+
+
+end Lean.Elab.Tactic
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index 9c4f4becf1..0273eb99cc 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -80,7 +80,7 @@ structure Context where
   we don't miss simplification opportunities. For example, consider the following:
   ```
   example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
-    simp_arith only
+    simp +arith only
     ...
   ```
   If we don't set `Result.cache := false` for the first `x + x`, then we get
diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean
index e213960d47..311ad2a982 100644
--- a/src/Std/Sat/AIG/CachedLemmas.lean
+++ b/src/Std/Sat/AIG/CachedLemmas.lean
@@ -73,7 +73,7 @@ theorem mkAtomCached_le_size (aig : AIG α) (var : α) :
   dsimp only [mkAtomCached]
   split
   · simp
-  · simp_arith
+  · simp +arith
 
 instance : LawfulOperator α (fun _ => α) mkAtomCached where
   le_size := mkAtomCached_le_size
@@ -147,7 +147,7 @@ theorem mkConstCached_le_size (aig : AIG α) (val : Bool) :
   dsimp only [mkConstCached]
   split
   · simp
-  · simp_arith
+  · simp +arith
 
 instance : LawfulOperator α (fun _ => Bool) mkConstCached where
   le_size := mkConstCached_le_size
@@ -189,18 +189,10 @@ theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
   dsimp only [go]
   split
   · simp
-  · split
-    · simp_arith [mkConstCached_le_size]
-    · simp_arith [mkConstCached_le_size]
-    · simp_arith [mkConstCached_le_size]
-    · simp_arith [mkConstCached_le_size]
-    · simp_arith
-    · simp_arith
-    · simp_arith
-    · simp_arith
-    · split
-      · simp_arith
-      · split <;> simp_arith [mkConstCached_le_size]
+  · split <;> try simp +arith [mkConstCached_le_size]
+    split
+    · simp +arith
+    · split <;> simp +arith [mkConstCached_le_size]
 
 /--
 `AIG.mkGateCached` never shrinks the underlying AIG.
diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean
index 0519407f2b..81d6ac58d2 100644
--- a/src/Std/Sat/AIG/Lemmas.lean
+++ b/src/Std/Sat/AIG/Lemmas.lean
@@ -70,7 +70,7 @@ theorem denote_projected_entry' {entry : Entrypoint α} :
 -/
 theorem mkGate_le_size (aig : AIG α) (input : GateInput aig) :
     aig.decls.size ≤ (aig.mkGate input).aig.decls.size := by
-  simp_arith [mkGate]
+  simp +arith [mkGate]
 
 /--
 The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that are valid for both.
@@ -125,7 +125,7 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
 -/
 theorem mkAtom_le_size (aig : AIG α) (var : α) :
     aig.decls.size ≤ (aig.mkAtom var).aig.decls.size := by
-  simp_arith [mkAtom]
+  simp +arith [mkAtom]
 
 /--
 The AIG produced by `AIG.mkAtom` agrees with the input AIG on all indices that are valid for both.
@@ -164,7 +164,7 @@ theorem denote_mkAtom {aig : AIG α} :
 -/
 theorem mkConst_le_size (aig : AIG α) (val : Bool) :
     aig.decls.size ≤ (aig.mkConst val).aig.decls.size := by
-  simp_arith [mkConst]
+  simp +arith [mkConst]
 
 /--
 The AIG produced by `AIG.mkConst` agrees with the input AIG on all indices that are valid for both.
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
index 33b4adf98a..693e54ffe9 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
@@ -43,7 +43,7 @@ theorem denote_blastShiftConcat (aig : AIG α) (target : ShiftConcatInput aig w)
   intro idx hidx
   unfold blastShiftConcat
   have hidx_lt : idx < 1 + w := by omega
-  by_cases hidx_eq : idx = 0 <;> simp_arith [hidx_lt, hidx_eq, RefVec.get_append]
+  by_cases hidx_eq : idx = 0 <;> simp +arith [hidx_lt, hidx_eq, RefVec.get_append]
 
 theorem denote_blastShiftConcat_eq_shiftConcat (aig : AIG α) (target : ShiftConcatInput aig w)
   (x : BitVec w) (b : Bool) (assign : α → Bool)
diff --git a/tests/lean/1081.lean b/tests/lean/1081.lean
index 26856a067b..184e70b9ba 100644
--- a/tests/lean/1081.lean
+++ b/tests/lean/1081.lean
@@ -22,10 +22,10 @@ namespace Vector'
   theorem insert_at_0_eq_cons1 (a: α) (v: Vector' α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v :=
     rfl -- Error, it does not hold by reflexivity because the recursion is on v
 
-  example (a : α) :  nil.insert a ⟨0, by simp_arith⟩ = cons a nil :=
+  example (a : α) :  nil.insert a ⟨0, by simp +arith⟩ = cons a nil :=
     rfl
 
-  example (a : α) (b : α) (bs : Vector' α n) :  (cons b bs).insert a ⟨0, by simp_arith⟩ = cons a (cons b bs) :=
+  example (a : α) (b : α) (bs : Vector' α n) :  (cons b bs).insert a ⟨0, by simp +arith⟩ = cons a (cons b bs) :=
     rfl
 
   theorem insert_at_0_eq_cons2 (a: α) (v: Vector' α n):  v.insert a ⟨0, Nat.zero_lt_succ n⟩ = cons a v := by
diff --git a/tests/lean/allFieldForConstants.lean b/tests/lean/allFieldForConstants.lean
index a2dc876be8..6d749b7b08 100644
--- a/tests/lean/allFieldForConstants.lean
+++ b/tests/lean/allFieldForConstants.lean
@@ -89,13 +89,13 @@ attribute [simp] List.foldl
 theorem foldl_init (s : Nat) (xs : List String) :  (xs.foldl (init := s) fun sum s => sum + s.length) = s + (xs.foldl (init := 0) fun sum s => sum + s.length) := by
   induction xs generalizing s with
   | nil => simp
-  | cons x xs ih => simp_arith [ih x.length, ih (s + x.length)]
+  | cons x xs ih => simp +arith [ih x.length, ih (s + x.length)]
 
 theorem listStringLen_append (xs ys : List String) : listStringLen (xs ++ ys) = listStringLen xs + listStringLen ys := by
   simp [listStringLen]
   induction xs with
   | nil => simp
-  | cons x xs ih => simp_arith [foldl_init x.length, foldl_init (_ + _), ih]
+  | cons x xs ih => simp +arith [foldl_init x.length, foldl_init (_ + _), ih]
 
 mutual
   theorem listStringLen_flat (f : Foo) : listStringLen (flat f) = textLength f := by
diff --git a/tests/lean/run/1228.lean b/tests/lean/run/1228.lean
index 356e4a54ba..c8def2d6f7 100644
--- a/tests/lean/run/1228.lean
+++ b/tests/lean/run/1228.lean
@@ -20,7 +20,7 @@ namespace Foo
     match s' with
     | foo s' =>
       have: Bar s' := sorry
-      have hterm: sizeOf s' < sizeOf s := by simp_all_arith
+      have hterm: sizeOf s' < sizeOf s := by simp_all +arith
       exact ex₂ this
   termination_by sizeOf s
 
diff --git a/tests/lean/run/1236.lean b/tests/lean/run/1236.lean
index 3d6001f94b..3b2a81ceab 100644
--- a/tests/lean/run/1236.lean
+++ b/tests/lean/run/1236.lean
@@ -1 +1 @@
-example: x ≤ x * 2 := by simp_arith
+example: x ≤ x * 2 := by simp +arith
diff --git a/tests/lean/run/1302.lean b/tests/lean/run/1302.lean
index 49026a8127..baab71aece 100644
--- a/tests/lean/run/1302.lean
+++ b/tests/lean/run/1302.lean
@@ -3,10 +3,10 @@
 example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
   simp
 
-example (a : Bool) : (a :: as).get ⟨0, by simp_arith⟩ = a := by
+example (a : Bool) : (a :: as).get ⟨0, by simp +arith⟩ = a := by
   simp
 
-example (a : Bool) : (a :: as).get ⟨0, by simp_arith⟩ = a := by
+example (a : Bool) : (a :: as).get ⟨0, by simp +arith⟩ = a := by
   simp
 
 example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
diff --git a/tests/lean/run/2042.lean b/tests/lean/run/2042.lean
index 9a90bd73f5..7e850b3dff 100644
--- a/tests/lean/run/2042.lean
+++ b/tests/lean/run/2042.lean
@@ -13,7 +13,7 @@ by
   funext x
   simp -- unfolds `foo`
   trace_state
-  simp_arith
+  simp +arith
 
 @[simp] def boo : Nat → Nat
   | a => 2 * a
@@ -30,4 +30,4 @@ by
   funext x
   simp -- unfolds `boo`
   trace_state
-  simp_arith
+  simp +arith
diff --git a/tests/lean/run/2615.lean b/tests/lean/run/2615.lean
index 44dac29caf..ee71a32dee 100644
--- a/tests/lean/run/2615.lean
+++ b/tests/lean/run/2615.lean
@@ -1,2 +1,2 @@
 -- `simp +arith` supports integers now
-theorem huh (x : Int) : x + 1 = 1 + x := by simp_arith
+theorem huh (x : Int) : x + 1 = 1 + x := by simp +arith
diff --git a/tests/lean/run/addDecorationsWithoutPartial.lean b/tests/lean/run/addDecorationsWithoutPartial.lean
index 3fce9f0fb9..6925f24caa 100644
--- a/tests/lean/run/addDecorationsWithoutPartial.lean
+++ b/tests/lean/run/addDecorationsWithoutPartial.lean
@@ -46,7 +46,7 @@ unsafe def replaceUnsafe (e : Expr) (f? : (e' : Expr) → sizeOf e' ≤ sizeOf e
 end ReplaceImpl'
 
 
-local macro "dec " h:ident : term => `(by apply Nat.le_trans _ $h; simp_arith)
+local macro "dec " h:ident : term => `(by apply Nat.le_trans _ $h; simp +arith)
 
 @[implemented_by ReplaceImpl'.replaceUnsafe]
 def replace' (e0 : Expr) (f? : (e : Expr) → sizeOf e ≤ sizeOf e0 → Option Expr) : Expr :=
@@ -77,4 +77,4 @@ def addDecorations (e : Expr) : Expr :=
       let rest := Expr.forallE name newType newBody data
       some <| mkApp2 (mkConst `SlimCheck.NamedBinder) (mkStrLit n) rest
     | _ => none
-decreasing_by all_goals exact Nat.le_trans (by simp_arith) h
+decreasing_by all_goals exact Nat.le_trans (by simp +arith) h
diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean
index 60f11a64e4..7ecd652728 100644
--- a/tests/lean/run/bigop.lean
+++ b/tests/lean/run/bigop.lean
@@ -28,7 +28,7 @@ instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) where
 def finElems (n : Nat) : List (Fin n) :=
   match n with
   | 0   => []
-  | n+1 => go (n+1) n (by simp_arith)
+  | n+1 => go (n+1) n (by simp +arith)
 where
   go (n : Nat) (i : Nat) (h : i < n) : List (Fin n) :=
    match i with
diff --git a/tests/lean/run/binrec.lean b/tests/lean/run/binrec.lean
index 39ec6687c9..6e066bc96c 100644
--- a/tests/lean/run/binrec.lean
+++ b/tests/lean/run/binrec.lean
@@ -29,8 +29,8 @@ theorem Nat.div2_lt (h : n ≠ 0) : n / 2 < n := by
   | n+4 =>
     rw [div_eq, if_pos]
     refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
-    exact @div2_lt (n+2) (by simp_arith)
-    simp_arith
+    exact @div2_lt (n+2) (by simp +arith)
+    simp +arith
 
 @[specialize]
 def Nat.binrec
diff --git a/tests/lean/run/caseTacInMacros.lean b/tests/lean/run/caseTacInMacros.lean
index 2743033e43..bd9822b419 100644
--- a/tests/lean/run/caseTacInMacros.lean
+++ b/tests/lean/run/caseTacInMacros.lean
@@ -4,7 +4,7 @@ macro "mymacro1 " h:ident : tactic =>
   `(tactic| {
       cases $h:ident with
       | zero => decide
-      | succ => simp_arith [f]
+      | succ => simp +arith [f]
   })
 
 example : f n > 0 := by
@@ -14,7 +14,7 @@ macro "mymacro2 " h:ident : tactic =>
   `(tactic| {
       cases $h:ident
       case zero => decide
-      case succ => simp_arith [f]
+      case succ => simp +arith [f]
   })
 
 example : f n > 0 := by
diff --git a/tests/lean/run/combinatorsAndWF.lean b/tests/lean/run/combinatorsAndWF.lean
index c69ce2016c..9265a06f42 100644
--- a/tests/lean/run/combinatorsAndWF.lean
+++ b/tests/lean/run/combinatorsAndWF.lean
@@ -5,12 +5,12 @@ where
     match cs with
     | [] => a
     | c :: cs =>
-      have : sizeOf c < sizeOf (c :: cs) := by simp_arith
+      have : sizeOf c < sizeOf (c :: cs) := by simp +arith
       -- TODO: simplify using linarith
       have h₁ : sizeOf c < sizeOf bs := Nat.lt_of_lt_of_le this h
-      have : sizeOf cs + (sizeOf c + 1) = sizeOf c + sizeOf cs + 1 := by simp_arith
+      have : sizeOf cs + (sizeOf c + 1) = sizeOf c + sizeOf cs + 1 := by simp +arith
       have : sizeOf cs ≤ sizeOf c + sizeOf cs + 1 := by rw [← this]; apply Nat.le_add_right
-      have h₂ : sizeOf cs ≤ sizeOf bs := by simp_arith at h; apply Nat.le_trans this h
+      have h₂ : sizeOf cs ≤ sizeOf bs := by simp +arith at h; apply Nat.le_trans this h
       go (f a c h₁) cs h₂
 
 theorem List.foldl_wf_eq [SizeOf β] (bs : List β) (init : α) (f : α → β → α) : bs.foldl_wf init (fun a b _ => f a b) = bs.foldl f init := by
@@ -56,12 +56,12 @@ where
     match cs with
     | [] => []
     | c :: cs =>
-      have : sizeOf c < sizeOf (c :: cs) := by simp_arith
+      have : sizeOf c < sizeOf (c :: cs) := by simp +arith
       -- TODO: simplify using linarith
       have h₁ : sizeOf c < sizeOf as := Nat.lt_of_lt_of_le this h
-      have : sizeOf cs + (sizeOf c + 1) = sizeOf c + sizeOf cs + 1 := by simp_arith
+      have : sizeOf cs + (sizeOf c + 1) = sizeOf c + sizeOf cs + 1 := by simp +arith
       have : sizeOf cs ≤ sizeOf c + sizeOf cs + 1 := by rw [← this]; apply Nat.le_add_right
-      have h₂ : sizeOf cs ≤ sizeOf as := by simp_arith at h; apply Nat.le_trans this h
+      have h₂ : sizeOf cs ≤ sizeOf as := by simp +arith at h; apply Nat.le_trans this h
       f c h₁ :: go cs h₂
 
 theorem List.map_wf_eq [SizeOf α] (as : List α) (f : α → β) : as.map_wf (fun a _ => f a) = as.map f := by
diff --git a/tests/lean/run/congrTactic.lean b/tests/lean/run/congrTactic.lean
index 07e90a52ba..fe21da83d1 100644
--- a/tests/lean/run/congrTactic.lean
+++ b/tests/lean/run/congrTactic.lean
@@ -12,11 +12,11 @@ def f (p : Prop) (a : Nat) (h : a > 0) [Decidable p] : Nat :=
   else
     a + 1
 
-example (h : a = b) : f True (a + 1) (by simp_arith) = f (0 = 0) (b + 1) (by simp_arith) := by
+example (h : a = b) : f True (a + 1) (by simp +arith) = f (0 = 0) (b + 1) (by simp +arith) := by
   congr
   decide
 
-example (h : a = b) : f True (a + 1) (by simp_arith) = f (0 = 0) (b + 1) (by simp_arith) := by
+example (h : a = b) : f True (a + 1) (by simp +arith) = f (0 = 0) (b + 1) (by simp +arith) := by
   congr 1
   · decide
   · show a + 1 = b + 1
diff --git a/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean
index 6f9a534d47..ac05c95df9 100644
--- a/tests/lean/run/constProp.lean
+++ b/tests/lean/run/constProp.lean
@@ -419,11 +419,11 @@ def State.length_erase_le (σ : State) (x : Var) : (σ.erase x).length ≤ σ.le
   | [] => simp
   | (y, v) :: σ =>
     by_cases hxy : x = y <;> simp [hxy]
-    next => exact Nat.le_trans (length_erase_le σ y) (by simp_arith)
-    next => simp_arith [length_erase_le σ x]
+    next => exact Nat.le_trans (length_erase_le σ y) (by simp +arith)
+    next => simp +arith [length_erase_le σ x]
 
 def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.length.succ :=
-  Nat.lt_of_le_of_lt (length_erase_le ..) (by simp_arith)
+  Nat.lt_of_le_of_lt (length_erase_le ..) (by simp +arith)
 
 @[simp] def State.join (σ₁ σ₂ : State) : State :=
   match σ₁ with
diff --git a/tests/lean/run/conv2.lean b/tests/lean/run/conv2.lean
index 3ac14f786c..41ed753485 100644
--- a/tests/lean/run/conv2.lean
+++ b/tests/lean/run/conv2.lean
@@ -1,12 +1,12 @@
 opaque f (a : Nat) (h : a > 0) : Nat
 
-example (h : a = b) : f (a + 1) (by simp_arith) = f (1 + b) (by simp_arith) := by
+example (h : a = b) : f (a + 1) (by simp +arith) = f (1 + b) (by simp +arith) := by
   conv => lhs; congr; rw [h]
   conv => lhs; congr; rw [Nat.add_comm]
 
 opaque g (p : Prop) [Decidable p] (a : Nat) (h : a > 0) : Nat
 
-example (h : a = b) : g True (a + 1) (by simp_arith) = g (1+1=2) (1 + b) (by simp_arith) := by
+example (h : a = b) : g True (a + 1) (by simp +arith) = g (1+1=2) (1 + b) (by simp +arith) := by
   conv =>
     lhs
     congr
diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean
index 7814dae89b..1dde93ae5d 100644
--- a/tests/lean/run/elabAsElim.lean
+++ b/tests/lean/run/elabAsElim.lean
@@ -34,10 +34,10 @@ def f3' (x : Nat) : (Nat → Nat) → Nat → Nat :=
   x.casesOn
 
 def f4 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
-  xs.casesOn (by intros; contradiction) (by intros; simp_arith)
+  xs.casesOn (by intros; contradiction) (by intros; simp +arith)
 
 def f5 (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
-  xs.casesOn (by intros; contradiction) (by intros; simp_arith) h
+  xs.casesOn (by intros; contradiction) (by intros; simp +arith) h
 
 def f6 (x : Nat) :=
   2 * x.casesOn 0 id
@@ -50,7 +50,7 @@ def f7 (xs : Vec α n) : Nat :=
   xs.casesOn (a := 10) 0
 
 def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
-  @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith)
+  @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp +arith)
 
 def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
   xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index 87baa3cc3f..a85155e34c 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -228,7 +228,7 @@ example (P Q : Prop) : (¬P → ¬Q) ↔ (Q → P) := by
 
 example {α} (a b c : α) [LE α] :
   ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b := by
-  simp_arith -- should not fail
+  simp +arith -- should not fail
   sorry
 
 example {α} (a b c : α) [LE α] :
diff --git a/tests/lean/run/inductionLetIssue.lean b/tests/lean/run/inductionLetIssue.lean
index a2c5a539f5..609ddb7cf6 100644
--- a/tests/lean/run/inductionLetIssue.lean
+++ b/tests/lean/run/inductionLetIssue.lean
@@ -13,7 +13,7 @@ def f (x? : Option Nat) (hp : P x?) : { r? : Option Nat // P r? } :=
     have : x > 0 := by
       cases h₂ : x with
       | zero => have := aux x? hp h₁; simp [x] at h₂; simp [h₂] at this; done
-      | succ x' => simp_arith
+      | succ x' => simp +arith
     ⟨some x, .somePos this⟩
   else
     ⟨none, .none⟩
diff --git a/tests/lean/run/issue5384.lean b/tests/lean/run/issue5384.lean
index 01a7b00bd3..46c98a4d5f 100644
--- a/tests/lean/run/issue5384.lean
+++ b/tests/lean/run/issue5384.lean
@@ -3,11 +3,11 @@ def bad (n : Nat) : Nat :=
   if h : n = 0 then 0 else bad (n / 2)
 termination_by n
 
-theorem foo : 2 * bad 42000 = bad 42000 + bad 42000 := by simp_arith
+theorem foo : 2 * bad 42000 = bad 42000 + bad 42000 := by simp +arith
 
-theorem foo2 (h : 2 * bad 42000 = bad 42000 + bad 42000 + 1) : False := by simp_arith at h
+theorem foo2 (h : 2 * bad 42000 = bad 42000 + bad 42000 + 1) : False := by simp +arith at h
 
-theorem foo3 (h : bad 42000 + bad 42000 = x) : (2 * bad 42000 = x) := by simp_arith at h; assumption
+theorem foo3 (h : bad 42000 + bad 42000 = x) : (2 * bad 42000 = x) := by simp +arith at h; assumption
 
 @[irreducible] def f : Nat → Nat := fun x => x
 
diff --git a/tests/lean/run/lazyListRotateUnfoldProof.lean b/tests/lean/run/lazyListRotateUnfoldProof.lean
index b09a971709..2a7e4d0c93 100644
--- a/tests/lean/run/lazyListRotateUnfoldProof.lean
+++ b/tests/lean/run/lazyListRotateUnfoldProof.lean
@@ -18,7 +18,7 @@ end LazyList
 def rotate (f : LazyList τ) (r : List τ) (a : LazyList τ)
   (h : f.length + 1 = r.length) : LazyList τ :=
   match r with
-  | List.nil => False.elim (by simp_arith [LazyList.length] at h)
+  | List.nil => False.elim (by simp +arith [LazyList.length] at h)
   | y::r' =>
   match f.force with
   | none =>  LazyList.cons y a
diff --git a/tests/lean/run/mergeSortCPDT.lean b/tests/lean/run/mergeSortCPDT.lean
index 271f29fdb0..4d834932fc 100644
--- a/tests/lean/run/mergeSortCPDT.lean
+++ b/tests/lean/run/mergeSortCPDT.lean
@@ -30,11 +30,11 @@ theorem List.length_split_of_atLeast2 {as : List α} (h : as.atLeast2) : as.spli
   | [_, _, _] => simp (config := { decide := true }) [split]
   | a::b::c::d::as =>
     -- TODO: simplify using linear arith and more automation
-    have : (c::d::as).atLeast2 := by simp_arith
+    have : (c::d::as).atLeast2 := by simp +arith
     have ih := length_split_of_atLeast2 this
-    simp_arith [split] at ih |-
+    simp +arith [split] at ih |-
     have ⟨ih₁, ih₂⟩ := ih
-    exact ⟨Nat.le_trans ih₁ (by simp_arith), Nat.le_trans ih₂ (by simp_arith)⟩
+    exact ⟨Nat.le_trans ih₁ (by simp +arith), Nat.le_trans ih₂ (by simp +arith)⟩
 
 def List.mergeSort' (p : α → α → Bool) (as : List α) : List α :=
   if h : as.atLeast2 then
diff --git a/tests/lean/run/mutualDefThms.lean b/tests/lean/run/mutualDefThms.lean
index f32b05b792..0deb8ce74e 100644
--- a/tests/lean/run/mutualDefThms.lean
+++ b/tests/lean/run/mutualDefThms.lean
@@ -38,13 +38,13 @@ attribute [simp] List.foldl
 theorem foldl_init (s : Nat) (xs : List String) :  (xs.foldl (init := s) fun sum s => sum + s.length) = s + (xs.foldl (init := 0) fun sum s => sum + s.length) := by
   induction xs generalizing s with
   | nil => simp
-  | cons x xs ih => simp_arith [ih x.length, ih (s + x.length)]
+  | cons x xs ih => simp +arith [ih x.length, ih (s + x.length)]
 
 theorem listStringLen_append (xs ys : List String) : listStringLen (xs ++ ys) = listStringLen xs + listStringLen ys := by
   simp [listStringLen]
   induction xs with
   | nil => simp
-  | cons x xs ih => simp_arith [foldl_init x.length, foldl_init (_ + _), ih]
+  | cons x xs ih => simp +arith [foldl_init x.length, foldl_init (_ + _), ih]
 
 mutual
   theorem listStringLen_flat (f : Foo) : listStringLen (flat f) = textLength f := by
diff --git a/tests/lean/run/no_grind_constProp.lean b/tests/lean/run/no_grind_constProp.lean
index df1035475e..29ada64734 100644
--- a/tests/lean/run/no_grind_constProp.lean
+++ b/tests/lean/run/no_grind_constProp.lean
@@ -290,11 +290,11 @@ def State.length_erase_le (σ : State) (x : Var) : (σ.erase x).length ≤ σ.le
   | [] => simp
   | (y, v) :: σ =>
     by_cases hxy : x = y <;> simp [hxy]
-    next => exact Nat.le_trans (length_erase_le σ y) (by simp_arith)
-    next => simp_arith [length_erase_le σ x]
+    next => exact Nat.le_trans (length_erase_le σ y) (by simp +arith)
+    next => simp +arith [length_erase_le σ x]
 
 def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.length.succ :=
-  Nat.lt_of_le_of_lt (length_erase_le ..) (by simp_arith)
+  Nat.lt_of_le_of_lt (length_erase_le ..) (by simp +arith)
 
 @[simp] def State.join (σ₁ σ₂ : State) : State :=
   match σ₁ with
diff --git a/tests/lean/run/posView.lean b/tests/lean/run/posView.lean
index c0da5b96ca..b0a8bf09c1 100644
--- a/tests/lean/run/posView.lean
+++ b/tests/lean/run/posView.lean
@@ -29,8 +29,8 @@ inductive PosView where
   and it will be applied automatically for us. -/
 theorem sizeof_lt_of_view_eq (h : Pos.view p₁ = PosView.succ p₂) : sizeOf p₂ < sizeOf p₁ := by
   match p₁, p₂ with
-  | { pred := Nat.succ n }, { pred := Nat.succ m } => simp [Pos.view] at h; simp_arith [h]
-  | { pred := Nat.succ n }, { pred := 0 }          => simp [Pos.view] at h; simp_arith [h]
+  | { pred := Nat.succ n }, { pred := Nat.succ m } => simp [Pos.view] at h; simp +arith [h]
+  | { pred := Nat.succ n }, { pred := 0 }          => simp [Pos.view] at h; simp +arith [h]
   | { pred := 0 },          _                      => simp [Pos.view] at h
 
 /-- `1` as notation for `PosView.one` -/
diff --git a/tests/lean/run/seval1.lean b/tests/lean/run/seval1.lean
index bd9db9c46c..db7dfc77ce 100644
--- a/tests/lean/run/seval1.lean
+++ b/tests/lean/run/seval1.lean
@@ -9,7 +9,7 @@ example (h : y = 2) : f x = x + y := by
 def g (x : Nat) := x + x
 
 @[seval] theorem g_eq : g x = 2 * x := by
-  simp_arith [g]
+  simp +arith [g]
 
 example (h : y = 2) : g x + 2 = 2 * x + y := by
   fail_if_success simp
diff --git a/tests/lean/run/shrinkFn.lean b/tests/lean/run/shrinkFn.lean
index 4459161ffc..b351c16f9b 100644
--- a/tests/lean/run/shrinkFn.lean
+++ b/tests/lean/run/shrinkFn.lean
@@ -4,6 +4,6 @@ class Sampleable (α : Type u) [SizeOf α] where
   shrink : shrinkFn α := fun _ => []
 
 def Prod.shrink [SizeOf α] [SizeOf β] (shrA : shrinkFn α) (shrB : shrinkFn β) : shrinkFn (α × β) := fun (fst, snd) =>
-  let shrink1 := shrA fst |>.map fun ⟨x, _⟩ => ⟨(x, snd), by simp_all_arith⟩
-  let shrink2 := shrB snd |>.map fun ⟨x, _⟩ => ⟨(fst, x), by simp_all_arith⟩
+  let shrink1 := shrA fst |>.map fun ⟨x, _⟩ => ⟨(x, snd), by simp_all +arith⟩
+  let shrink2 := shrB snd |>.map fun ⟨x, _⟩ => ⟨(fst, x), by simp_all +arith⟩
   shrink1 ++ shrink2
diff --git a/tests/lean/run/simpArith1.lean b/tests/lean/run/simpArith1.lean
index 4d2a15ec5c..5dc81090f7 100644
--- a/tests/lean/run/simpArith1.lean
+++ b/tests/lean/run/simpArith1.lean
@@ -2,18 +2,18 @@ theorem ex1 : a + b < b + 1 + a + c := by
   simp (config := { arith := true })
 
 theorem ex2 : a + b < b + 1 + a + c := by
-  simp_arith
+  simp +arith
 
 theorem ex3 : a + (fun x => x) b < b + 1 + a + c := by
-  simp_arith
+  simp +arith
 
 theorem ex5 (h : a + d + b > b + 1 + (a + (c + c) + d)) : False := by
-  simp_arith at h
+  simp +arith at h
 
 #print ex5
 
 theorem ex6 (p : Nat → Prop) (h : p (a + 1 + a + 2 + b)) : p (2*a + b + 3) := by
-  simp_arith at h
+  simp +arith at h
   assumption
 
 #print ex6
diff --git a/tests/lean/run/simpArithCacheIssue.lean b/tests/lean/run/simpArithCacheIssue.lean
index 0f1935d718..21f426497a 100644
--- a/tests/lean/run/simpArithCacheIssue.lean
+++ b/tests/lean/run/simpArithCacheIssue.lean
@@ -5,7 +5,7 @@ h : y = 0
 -/
 #guard_msgs in
 example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
-  simp_arith only
+  simp +arith only
   /-
   This is a test for a `simp` cache issue where the following incorrect goal was being
   produced.
@@ -21,5 +21,5 @@ example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
   simp [h]
 
 example (x y : Nat) (h : y = 0) : id (x + x) = id ((x + x) + y) := by
-  simp_arith only
+  simp +arith only
   simp [h]
diff --git a/tests/lean/run/simpAutoUnfold.lean b/tests/lean/run/simpAutoUnfold.lean
index 999a1fa8ba..072ec742dd 100644
--- a/tests/lean/run/simpAutoUnfold.lean
+++ b/tests/lean/run/simpAutoUnfold.lean
@@ -20,18 +20,18 @@ def g : Nat → Nat
   | n+1 => n + 2
 
 example (a : Nat) : g a > 0 := by
-  cases a <;> simp_arith!
+  cases a <;> simp! +arith
 
 example (a : Nat) : g a > 0 := by
-  cases a <;> simp_arith!
+  cases a <;> simp! +arith
 
 example (a : Nat) : g a > 0 := by
-  cases a <;> simp_arith! [-g]
-  simp_arith!
+  cases a <;> simp! +arith +decide [-g]
+  simp! +arith
 
 example (a : Nat) (h : b + 2 = 2) : g a > b := by
-  cases a <;> simp_all_arith!
+  cases a <;> simp_all! +arith
 
 example (a : Nat) (h : b + 2 = 2) : g a > b := by
-  cases a <;> simp_all_arith! [-g]
-  simp_arith!
+  cases a <;> simp_all! +arith +decide [-g]
+  simp! +arith +decide
diff --git a/tests/lean/run/simp_arith_deprecated.lean b/tests/lean/run/simp_arith_deprecated.lean
new file mode 100644
index 0000000000..0feb2a661c
--- /dev/null
+++ b/tests/lean/run/simp_arith_deprecated.lean
@@ -0,0 +1,55 @@
+/--
+info: Try these:
+• simp +arith
+• simp +arith +decide
+---
+error: `simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
+-/
+#guard_msgs in
+example : x + 2 = 1 + 1 + x := by
+  simp_arith
+
+/--
+info: Try these:
+• simp +arith [h, id] at h₂
+• simp +arith +decide [h, id] at h₂
+---
+error: `simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
+-/
+#guard_msgs in
+example (h : x = y) (h₂ : y + 2 = 1 + 1 + x) : True := by
+  simp_arith [h, id] at h₂
+
+/--
+info: Try these:
+• simp! +arith [h, id] at h₂
+• simp! +arith +decide [h, id] at h₂
+---
+error: `simp_arith!` has been deprecated. It was a shorthand for `simp! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
+-/
+#guard_msgs in
+example (h : x = y) (h₂ : y + 2 = 1 + 1 + x) : True := by
+  simp_arith! [h, id] at h₂
+
+
+/--
+info: Try these:
+• simp_all +arith
+• simp_all +arith +decide
+---
+error: `simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
+-/
+#guard_msgs in
+example (h : x = y) (h₂ : y + 2 = 1 + 1 + x) : True := by
+  simp_all_arith
+
+/--
+info: Try these:
+• simp_all! +arith
+• simp_all! +arith +decide
+---
+error: `simp_all_arith!` has been deprecated. It was a shorthand for `simp_all! +arith +decide`, but most of the time, `+decide` was redundant since simprocs have been implemented.
+-/
+#guard_msgs in
+example (h : x = y) (h₂ : y + 2 = 1 + 1 + x) : True := by
+  simp_all_arith!
diff --git a/tests/lean/run/simproc1.lean b/tests/lean/run/simproc1.lean
index 653605daa2..e8ceb4f33e 100644
--- a/tests/lean/run/simproc1.lean
+++ b/tests/lean/run/simproc1.lean
@@ -17,21 +17,21 @@ run_meta do
 
 example : x + foo 2 = 12 + x := by
   set_option simprocs false in fail_if_success simp
-  simp_arith
+  simp +arith
 
 example : x + foo 2 = 12 + x := by
   -- `simp only` must not use the default simproc set
   fail_if_success simp only
-  simp_arith
+  simp +arith
 
 example : x + foo 2 = 12 + x := by
   -- `simp only` does not use the default simproc set, but we can provide simprocs as arguments
   simp only [reduceFoo]
-  simp_arith
+  simp +arith
 
 example : x + foo 2 = 12 + x := by
   -- We can use `-` to disable `simproc`s
   fail_if_success simp [-reduceFoo]
-  simp_arith
+  simp +arith
 
 example (x : Nat) (h : x < 86) : ¬100 ≤ x + 14 := by simp; exact h
diff --git a/tests/lean/run/splitList.lean b/tests/lean/run/splitList.lean
index 71b55047f2..0e50f740ae 100644
--- a/tests/lean/run/splitList.lean
+++ b/tests/lean/run/splitList.lean
@@ -15,7 +15,7 @@ def splitList : (l : List α) → ListSplit l
 theorem splitList_length (as : List α) (h₁ : as.length > 1) (h₂ : as = bs) : (splitList as).left.length < bs.length ∧ (splitList as).right.length < bs.length := by
   match as with
   | [] => contradiction
-  | a :: as => simp_arith [← h₂, splitList]; simp_arith at h₁; assumption
+  | a :: as => simp +arith [← h₂, splitList]; simp +arith at h₁; assumption
 
 def len : List α → Nat
   | []      => 0
@@ -27,10 +27,10 @@ def len : List α → Nat
     | ListSplit.split fst snd =>
       -- Remark: `match` refined `h₁`s type to `h₁ : fst ++ snd = a :: b :: as`
       -- h₂ : HEq (splitList l) (ListSplit.split fst snd)
-      have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
+      have := splitList_length (fst ++ snd) (by simp +arith [h₁]) h₁
       -- The following two proofs ase used to justify the recursive applications `len fst` and `len snd`
-      have dec₁ : fst.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
-      have dec₂ : snd.length < as.length + 2 := by subst l; simp_arith [eq_of_heq h₂] at this |- ; simp [this]
+      have dec₁ : fst.length < as.length + 2 := by subst l; simp +arith [eq_of_heq h₂] at this |- ; simp [this]
+      have dec₂ : snd.length < as.length + 2 := by subst l; simp +arith [eq_of_heq h₂] at this |- ; simp [this]
       len fst + len snd
 termination_by xs => xs.length
 
@@ -78,9 +78,9 @@ def len : List α → Nat
 termination_by xs => xs.length
 decreasing_by
   all_goals
-    have := splitList_length (fst ++ snd) (by simp_arith [h₁]) h₁
+    have := splitList_length (fst ++ snd) (by simp +arith [h₁]) h₁
     subst h₂
-    simp_arith [eq_of_heq h₃] at this |- ; simp [this]
+    simp +arith [eq_of_heq h₃] at this |- ; simp [this]
 
 -- The equational theorems are
 #check @len.eq_1
diff --git a/tests/lean/run/treeNode.lean b/tests/lean/run/treeNode.lean
index e78a1e51b1..0174a8a47d 100644
--- a/tests/lean/run/treeNode.lean
+++ b/tests/lean/run/treeNode.lean
@@ -9,7 +9,7 @@ def treeToList (t : TreeNode) : List String :=
    let mut r := [name]
    for h : child in children do
      -- We will not this the following `have` in the future
-     have : sizeOf child < 1 + sizeOf name + sizeOf children := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp_arith)
+     have : sizeOf child < 1 + sizeOf name + sizeOf children := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp +arith)
      r := r ++ treeToList child
    return r
 
@@ -28,7 +28,7 @@ end
 theorem length_treeToList_eq_numNames (t : TreeNode) : (treeToList t).length = numNames t := by
   match t with
   | .mkLeaf .. => simp [treeToList, numNames]
-  | .mkNode _ cs => simp_arith [numNames, helper cs]
+  | .mkNode _ cs => simp +arith [numNames, helper cs]
 where
   helper (cs : List TreeNode) : (cs.map treeToList).flatten.length = numNamesLst cs := by
     match cs with
diff --git a/tests/lean/run/unfoldMany.lean b/tests/lean/run/unfoldMany.lean
index d821ecd4d4..65c8e23333 100644
--- a/tests/lean/run/unfoldMany.lean
+++ b/tests/lean/run/unfoldMany.lean
@@ -4,4 +4,4 @@ def g (x : Nat) := f x + f x
 
 example : g x > 0 := by
   unfold g f
-  simp_arith
+  simp +arith
diff --git a/tests/lean/run/wfForIn.lean b/tests/lean/run/wfForIn.lean
index 054d6630cf..5bb74ac7bf 100644
--- a/tests/lean/run/wfForIn.lean
+++ b/tests/lean/run/wfForIn.lean
@@ -5,5 +5,5 @@ def printFns : Term → IO Unit
   | Term.app f args => do
      IO.println f
      for h : arg in args do
-       have : sizeOf arg < 1 + sizeOf f + sizeOf args := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp_arith)
+       have : sizeOf arg < 1 + sizeOf f + sizeOf args := Nat.lt_trans (List.sizeOf_lt_of_mem h) (by simp +arith)
        printFns arg
diff --git a/tests/lean/run/zetaDSimpIssue.lean b/tests/lean/run/zetaDSimpIssue.lean
index baab4277bb..937e051ff9 100644
--- a/tests/lean/run/zetaDSimpIssue.lean
+++ b/tests/lean/run/zetaDSimpIssue.lean
@@ -5,4 +5,4 @@ def f (x : Nat) :=
 example : f x = 2*x + 2 := by
   dsimp [f]
   guard_target =ₛ x + 1 + (x + 1) = 2*x + 2
-  simp_arith
+  simp +arith
diff --git a/tests/lean/splitIssue.lean b/tests/lean/splitIssue.lean
index 68d3eee2d6..80ac1ec33d 100644
--- a/tests/lean/splitIssue.lean
+++ b/tests/lean/splitIssue.lean
@@ -8,7 +8,7 @@ def f (x : Nat) : Nat :=
 example : f x = 2*x + 1 := by
   unfold f
   split
-  next h => simp_arith [g] at h
+  next h => simp +arith [g] at h
   next y h =>
     trace_state
     -- split tactic should *not* rewrite `g x` to `Nat.succ y`
diff --git a/tests/lean/wildcardAlt.lean b/tests/lean/wildcardAlt.lean
index 1b47d2ffbd..a714cee8ae 100644
--- a/tests/lean/wildcardAlt.lean
+++ b/tests/lean/wildcardAlt.lean
@@ -17,10 +17,10 @@ example (x : Foo) : bla x > 0 := by
 
 example (x : Foo) : bla x > 0 := by
   cases x with
-  | c1 x => simp_arith [bla]
+  | c1 x => simp +arith [bla]
   | _    => decide
 
 example (x : Foo) : bla x > 0 := by
   induction x with
-  | c1 x => simp_arith [bla]
+  | c1 x => simp +arith [bla]
   | _    => decide
diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean
index c374a7c5c0..60e603dd4d 100644
--- a/tests/pkg/user_attr/UserAttr/Tst.lean
+++ b/tests/pkg/user_attr/UserAttr/Tst.lean
@@ -26,11 +26,11 @@ def getFooAttrInfo? (declName : Name) : CoreM (Option (Nat × Bool)) :=
 @[my_simp] theorem g_eq : g x = x + 1 := rfl
 
 example : f x + g x = 2*x + 3 := by
-  fail_if_success simp_arith -- does not apply f_eq and g_eq
-  simp_arith [f, g]
+  fail_if_success simp +arith -- does not apply f_eq and g_eq
+  simp +arith [f, g]
 
 example : f x + g x = 2*x + 3 := by
-  simp_arith [my_simp]
+  simp +arith [my_simp]
 
 example : f x = id (x + 2) := by
   simp