From 05fe436bda1489bc96ab7cab2325a71d79977e26 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 4 Sep 2024 17:56:25 +1000
Subject: [PATCH] chore: don't use simp_arith when simp will do (#5256)

---
 src/Init/Data/Array/BasicAux.lean | 2 +-
 src/Init/Data/List/BasicAux.lean  | 8 ++++----
 src/Init/Data/Nat/Log2.lean       | 4 ++--
 src/Init/SizeOfLemmas.lean        | 2 +-
 src/Lean/Util/Diff.lean           | 4 ++--
 5 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean
index b4fd9b671d..c6221d620e 100644
--- a/src/Init/Data/Array/BasicAux.lean
+++ b/src/Init/Data/Array/BasicAux.lean
@@ -38,7 +38,7 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra
   · intro h; rw [h]
 
 def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } :=
-  go 0 ⟨mkEmpty as.size, rfl⟩ (by simp_arith)
+  go 0 ⟨mkEmpty as.size, rfl⟩ (by simp)
 where
   go (i : Nat) (acc : { bs : Array β // bs.size = i }) (hle : i ≤ as.size) : m { bs : Array β // bs.size = as.size } := do
     if h : i = as.size then
diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean
index b33b57495d..90892b72c6 100644
--- a/src/Init/Data/List/BasicAux.lean
+++ b/src/Init/Data/List/BasicAux.lean
@@ -167,8 +167,8 @@ theorem getElem_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} :
   induction as generalizing i with
   | nil => trivial
   | cons a as ih =>
-    cases i with simp [get, Nat.succ_sub_succ] <;> simp_arith [Nat.succ_sub_succ] at h
-    | succ i => apply ih; simp_arith [h]
+    cases i with simp [get, Nat.succ_sub_succ] <;> simp [Nat.succ_sub_succ] at h
+    | succ i => apply ih; simp [h]
 
 theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.length) : (as ++ [a] : List _).get i = a := by
   cases i; rename_i i h'
@@ -177,8 +177,8 @@ theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.
     | zero => simp [List.get]
     | succ => simp_arith at h'
   | cons a as ih =>
-    cases i with simp_arith at h
-    | succ i => apply ih; simp_arith [h]
+    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
diff --git a/src/Init/Data/Nat/Log2.lean b/src/Init/Data/Nat/Log2.lean
index a9335074cc..ff85ddb6f0 100644
--- a/src/Init/Data/Nat/Log2.lean
+++ b/src/Init/Data/Nat/Log2.lean
@@ -14,8 +14,8 @@ theorem log2_terminates : ∀ n, n ≥ 2 → n / 2 < n
   | n+4, _ => by
     rw [div_eq, if_pos]
     refine succ_lt_succ (Nat.lt_trans ?_ (lt_succ_self _))
-    exact log2_terminates (n+2) (by simp_arith)
-    simp_arith
+    exact log2_terminates (n+2) (by simp)
+    simp
 
 /--
 Computes `⌊max 0 (log₂ n)⌋`.
diff --git a/src/Init/SizeOfLemmas.lean b/src/Init/SizeOfLemmas.lean
index 4fbda63e56..dd75ee0b67 100644
--- a/src/Init/SizeOfLemmas.lean
+++ b/src/Init/SizeOfLemmas.lean
@@ -30,4 +30,4 @@ import Init.Data.Nat.Linear
   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_arith
+  cases s; simp
diff --git a/src/Lean/Util/Diff.lean b/src/Lean/Util/Diff.lean
index 24d3982491..77575819a2 100644
--- a/src/Lean/Util/Diff.lean
+++ b/src/Lean/Util/Diff.lean
@@ -150,8 +150,8 @@ partial def lcs (left right : Subarray α) : Array α := Id.run do
   let some (_, v, li, ri) := best
     | return pref ++ suff
 
-  let lefts := left.split ⟨li.val, by cases li; simp_arith; omega⟩
-  let rights := right.split ⟨ri.val, by cases ri; simp_arith; omega⟩
+  let lefts := left.split ⟨li.val, by cases li; omega⟩
+  let rights := right.split ⟨ri.val, by cases ri; omega⟩
 
   pref ++ lcs lefts.1 rights.1 ++ #[v] ++ lcs (lefts.2.drop 1) (rights.2.drop 1) ++ suff