diff --git a/tests/lean/allFieldForConstants.lean b/tests/lean/allFieldForConstants.lean
index b89e333f41930..d0605b565e9a3 100644
--- a/tests/lean/allFieldForConstants.lean
+++ b/tests/lean/allFieldForConstants.lean
@@ -105,7 +105,7 @@ mutual
 
   theorem listStringLen_flatList (cs : List Foo) : listStringLen (flatList cs) = textLengthList cs := by
     match cs with
-    | [] => simp
+    | [] => simp [listStringLen]
     | f :: fs => simp [listStringLen_append, listStringLen_flatList fs, listStringLen_flat f]
 end
 
diff --git a/tests/lean/letFun.lean b/tests/lean/letFun.lean
index 15aa199710426..796f572f31219 100644
--- a/tests/lean/letFun.lean
+++ b/tests/lean/letFun.lean
@@ -7,4 +7,4 @@
 example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (let_fun x := a + 1; x + x) > b := by
   simp (config := { beta := false }) [h1]
   trace_state
-  simp [h2]
+  simp (config := { decide := true }) [h2]
diff --git a/tests/lean/matchOfNatIssue.lean b/tests/lean/matchOfNatIssue.lean
index 0ffdce3d4fcbc..7619026464ec2 100644
--- a/tests/lean/matchOfNatIssue.lean
+++ b/tests/lean/matchOfNatIssue.lean
@@ -1,7 +1,7 @@
 example (x : Int) (h : x = 2) : Int.div 2 1 = x := by
   simp [Int.div]
   trace_state
-  simp [h]
+  simp (config := { decide := true }) [h]
 
 example (n : Nat) : Int.div (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n / 0) := by
   simp [Int.div]
diff --git a/tests/lean/run/1293.lean b/tests/lean/run/1293.lean
index ee798f7413400..6834e8df70199 100644
--- a/tests/lean/run/1293.lean
+++ b/tests/lean/run/1293.lean
@@ -15,7 +15,7 @@ instance {arr : Array String} {f : String → String} {n : Nat} : Coe (Array (Id
 
 def store1 : Store := {
   arr := #["a", "b", "c", "d", "e"]
-  ids := #[⟨2, by simp⟩]
+  ids := #[⟨2, by decide⟩]
 }
 
 def tryCoeStore := {
diff --git a/tests/lean/run/1302.lean b/tests/lean/run/1302.lean
index 0861b351d76fd..0cc9fa7d65279 100644
--- a/tests/lean/run/1302.lean
+++ b/tests/lean/run/1302.lean
@@ -1,6 +1,6 @@
 @[simp] theorem get_cons_zero {as : List α} : (a :: as).get ⟨0, Nat.zero_lt_succ _⟩ = a := rfl
 
-example (a b c : α) : [a, b, c].get ⟨0, by simp⟩ = a := by
+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
@@ -9,5 +9,5 @@ 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⟩ = a := by
+example (a b c : α) : [a, b, c].get ⟨0, by simp (config := { decide := true })⟩ = a := by
   rw [get_cons_zero]
diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean
index d5816d8a6c3e3..248837b8551a8 100644
--- a/tests/lean/run/1380.lean
+++ b/tests/lean/run/1380.lean
@@ -4,6 +4,6 @@ theorem Nat.lt_succ_iff {m n : Nat} : m < succ n ↔ m ≤ n := sorry
 variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1)
 theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial
 set_option trace.Meta.Tactic.simp true in
-example (hv: v₁ < v₂) : True := foo n v₁ v₂ ‹_› ‹_› (by simp only[hv, Fin.mk.injEq, Nat.ne_of_gt, Nat.lt_succ_iff])
+example (hv: v₁ < v₂) : True := foo n v₁ v₂ ‹_› ‹_› (by simp (config := { decide := true }) only [hv, Fin.mk.injEq, Nat.ne_of_gt, Nat.lt_succ_iff])
 
 #check Fin.mk.injEq
diff --git a/tests/lean/run/1921.lean b/tests/lean/run/1921.lean
index 7d9868de93c29..ab288d1478a1f 100644
--- a/tests/lean/run/1921.lean
+++ b/tests/lean/run/1921.lean
@@ -1,9 +1,9 @@
 @[simp] theorem Array.size_singleton : #[a].size = 1 := rfl
-@[simp] theorem USize.not_size_le_one : ¬ USize.size ≤ 1 := by cases usize_size_eq <;> simp_all
+@[simp] theorem USize.not_size_le_one : ¬ USize.size ≤ 1 := by cases usize_size_eq <;> simp_all (config := { decide := true })
 
 def f := #[true].any id 0 USize.size
 
 -- `native_decide` used to prove `false` here, due to a bug in `Array.anyMUnsafe`.
 example : f = true := by native_decide
 
-example : f = true := by simp [f, Array.any, Array.anyM]
+example : f = true := by simp (config := { decide := true }) [f, Array.any, Array.anyM]
diff --git a/tests/lean/run/891.lean b/tests/lean/run/891.lean
index 26d3008713346..81bc91ca45380 100644
--- a/tests/lean/run/891.lean
+++ b/tests/lean/run/891.lean
@@ -44,7 +44,7 @@ example : f 'b' n = 2 := by
   simp[f]
 
 example : f 'c' n = 3 := by
-  simp[f]
+  simp (config := { decide := true }) [f]
 
 def g : String → Nat → Nat
  | "hello", _ => 1
@@ -58,7 +58,7 @@ example : g "world" n = 2 := by
   simp[g]
 
 example : g "abc" n = 3 := by
-  simp[g]
+  simp (config := { decide := true }) [g]
 
 def fn : Fin 8 → Nat → Nat
  | 2, _ => 1
diff --git a/tests/lean/run/def10.lean b/tests/lean/run/def10.lean
index 874119b304ae3..e1335b9c60711 100644
--- a/tests/lean/run/def10.lean
+++ b/tests/lean/run/def10.lean
@@ -27,4 +27,4 @@ theorem ex6 : g x y z > 0 := by
   split
   next => decide
   next => decide
-  next a b c h₁ h₂ => simp [f_eq h₁]
+  next a b c h₁ h₂ => simp (config := { decide := true }) [f_eq h₁]
diff --git a/tests/lean/run/defaultEliminator.lean b/tests/lean/run/defaultEliminator.lean
index fa67666a91889..bcd279164f069 100644
--- a/tests/lean/run/defaultEliminator.lean
+++ b/tests/lean/run/defaultEliminator.lean
@@ -28,4 +28,4 @@ example (x y : Nat) : f x y > 0 := by
   | succ_succ x y ih => simp [f, ih]
 
 example (x y : Nat) : f x y > 0 := by
-  induction x, y <;> simp [f, *]
+  induction x, y <;> simp (config := { decide := true }) [f, *]
diff --git a/tests/lean/run/eqnsAtSimp.lean b/tests/lean/run/eqnsAtSimp.lean
index ba691658cd726..a296c5f0f7784 100644
--- a/tests/lean/run/eqnsAtSimp.lean
+++ b/tests/lean/run/eqnsAtSimp.lean
@@ -15,5 +15,5 @@ decreasing_by
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
-  | zero => simp
+  | zero => simp [isEven]
   | succ x ih => simp [Nat.mul_succ, Nat.add_succ, isEven, isOdd, ih]
diff --git a/tests/lean/run/maze.lean b/tests/lean/run/maze.lean
index a55d9eb6e0bf8..431aaecdc5d2e 100644
--- a/tests/lean/run/maze.lean
+++ b/tests/lean/run/maze.lean
@@ -292,5 +292,5 @@ def maze1 := ┌───┐
 def foo : can_escape maze1 := by
   apply step_west
   set_option trace.Meta.debug true in
-  simp
+  simp (config := { decide := true })
   out
diff --git a/tests/lean/run/mergeSortCPDT.lean b/tests/lean/run/mergeSortCPDT.lean
index d7a7ccca4a91f..92bf11914dc65 100644
--- a/tests/lean/run/mergeSortCPDT.lean
+++ b/tests/lean/run/mergeSortCPDT.lean
@@ -26,8 +26,8 @@ theorem List.length_split_of_atLeast2 {as : List α} (h : as.atLeast2) : as.spli
   match as with
   | []  => simp at h
   | [_] => simp at h
-  | [_, _] => simp [split]
-  | [_, _, _] => simp [split]
+  | [_, _] => simp (config := { decide := true }) [split]
+  | [_, _, _] => 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
diff --git a/tests/lean/run/mutualDefThms.lean b/tests/lean/run/mutualDefThms.lean
index 5b62402c1136a..a20fee4ffcc4e 100644
--- a/tests/lean/run/mutualDefThms.lean
+++ b/tests/lean/run/mutualDefThms.lean
@@ -54,7 +54,7 @@ mutual
 
   theorem listStringLen_flatList (cs : List Foo) : listStringLen (flatList cs) = textLengthList cs := by
     match cs with
-    | [] => simp
+    | [] => simp [listStringLen]
     | f :: fs => simp [listStringLen_append, listStringLen_flatList fs, listStringLen_flat f]
 end
 
diff --git a/tests/lean/run/set.lean b/tests/lean/run/set.lean
index 82c24a9b0c1c3..c1238693617a3 100644
--- a/tests/lean/run/set.lean
+++ b/tests/lean/run/set.lean
@@ -8,7 +8,7 @@ def Set.pred (p : α → Prop) : Set α := p
 notation "{" a "|" p "}" => Set.pred (fun a => p)
 
 theorem ex1 : (1, 3) ∈ { (n, m) | n < 2 ∧ m < 5 } := by
-  simp [Set.in, Set.pred]
+  simp (config := { decide := true }) [Set.in, Set.pred]
 
 def Set.union (s₁ s₂ : Set α) : Set α :=
   { a | a ∈ s₁ ∨ a ∈ s₂ }
diff --git a/tests/lean/run/simp6.lean b/tests/lean/run/simp6.lean
index 64f36a558c05a..c9006bab76950 100644
--- a/tests/lean/run/simp6.lean
+++ b/tests/lean/run/simp6.lean
@@ -16,13 +16,13 @@ theorem ex5 : (10 = 20) = False :=
 #print ex5
 
 theorem ex6 : (if "hello" = "world" then 1 else 2) = 2 :=
-  by simp
+  by simp (config := { decide := true })
 
 #print ex6
 
 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by
   fail_if_success simp (config := { decide := false })
-  simp
+  simp (config := { decide := true })
 
 theorem ex8 : (10 + 2000 = 20) = False :=
   by simp
@@ -32,4 +32,4 @@ def fact : Nat → Nat
   | x+1 => (x+1) * fact x
 
 theorem ex9 : (if fact 100 > 10 then true else false) = true :=
-  by simp
+  by simp (config := { decide := true })
diff --git a/tests/lean/run/simp_all.lean b/tests/lean/run/simp_all.lean
index 60054b2fda9a4..c9dac3d7e2b9d 100644
--- a/tests/lean/run/simp_all.lean
+++ b/tests/lean/run/simp_all.lean
@@ -13,7 +13,7 @@ theorem ex3 (h₁ : a = 0) (h₂ : a + b = 0) : f (b + c) = c := by
   simp [h₂]
 
 theorem ex4 (h₁ : a = f a) (h₂ : b + 0 = 0) : f b = 0 := by
-  simp_all [-h₁]
+  simp_all (config := { decide := true }) [-h₁]
 
 theorem ex5 (h₁ : a = f a) (h₂ : b + 0 = 0) : f (b + a) = a := by
   simp_all [-h₁, f]
diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean
index 702ee1ee886d0..6a77120289f35 100644
--- a/tests/lean/unfold1.lean
+++ b/tests/lean/unfold1.lean
@@ -11,7 +11,7 @@ decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
   induction x with
-  | zero => simp
+  | zero => simp [isEven]
   | succ x ih =>
     unfold isEven
     trace_state