diff --git a/tests/lean/421.lean b/tests/lean/421.lean
index 75c78a9079..43df298d41 100644
--- a/tests/lean/421.lean
+++ b/tests/lean/421.lean
@@ -7,5 +7,5 @@ inductive Conw : Con → Prop
 
 example (x : Conw Con.nil) : x = Conw.nilw := by
   cases x
-  traceState
+  trace_state
   rfl
diff --git a/tests/lean/cdotAtSimpArg.lean b/tests/lean/cdotAtSimpArg.lean
index 8d8c3f36c5..e57cb130fd 100644
--- a/tests/lean/cdotAtSimpArg.lean
+++ b/tests/lean/cdotAtSimpArg.lean
@@ -3,14 +3,14 @@ example : ¬ true = false := by
 
 example (h : y = 0) : x + y = x := by
   simp [(.+.)] -- Expands `HAdd.hAdd
-  traceState
+  trace_state
   simp [Add.add]
   simp [h, Nat.add]
   done
 
 example (h : y = 0) : x + y = x := by
   simp [.+.]
-  traceState
+  trace_state
   simp [Add.add]
   simp [h, Nat.add]
   done
diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean
index b94e7193cf..66f3166ee2 100644
--- a/tests/lean/conv1.lean
+++ b/tests/lean/conv1.lean
@@ -8,7 +8,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
     congr
     . skip
     . whnf; skip
-  traceState
+  trace_state
   rw [Nat.add_comm]
   rfl
 
@@ -17,7 +17,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
     whnf
     rhs
     whnf
-  traceState
+  trace_state
   rw [Nat.add_comm]
   rfl
 
@@ -29,7 +29,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
   conv =>
     rhs
     whnf
-  traceState
+  trace_state
   apply Nat.add_comm x y
 
 def f (x y z : Nat) : Nat :=
@@ -40,7 +40,7 @@ example (x y : Nat) : f x (x + y + 0) y = y + x := by
     lhs
     arg 2
     whnf
-  traceState
+  trace_state
   simp [f]
   apply Nat.add_comm
 
@@ -49,7 +49,7 @@ example (x y : Nat) : f x (x + y + 0) y = y + x := by
     lhs
     arg 2
     change x + y
-    traceState
+    trace_state
     rw [Nat.add_comm]
 
 example : id (fun x y => 0 + x + y) = Nat.add := by
@@ -57,9 +57,9 @@ example : id (fun x y => 0 + x + y) = Nat.add := by
     lhs
     arg 1
     ext a b
-    traceState
+    trace_state
     rw [Nat.zero_add]
-    traceState
+    trace_state
 
 example : id (fun x y => 0 + x + y) = Nat.add := by
   conv =>
@@ -71,27 +71,27 @@ example : id (fun x y => 0 + x + y) = Nat.add := by
 example : id (fun x y => 0 + x + y) = Nat.add := by
   conv =>
     enter [1, 1, a, b]
-    traceState
+    trace_state
     rw [Nat.zero_add]
 
 example (p : Nat → Prop) (h : ∀ a, p a) : ∀ a, p (id (0 + a)) := by
   conv =>
     intro x
-    traceState
+    trace_state
     arg 1
-    traceState
+    trace_state
     simp only [id]
-    traceState
+    trace_state
     rw [Nat.zero_add]
   exact h
 
 example (p : Prop) (x : Nat) : (x = x → p) → p := by
   conv =>
     congr
-    . traceState
+    . trace_state
       congr
       . simp
-  traceState
+  trace_state
   conv =>
     lhs
     simp
@@ -102,7 +102,7 @@ example : (fun x => 0 + x) = id := by
   conv =>
     lhs
     tactic => funext x
-    traceState
+    trace_state
     rw [Nat.zero_add]
 
 example (p : Prop) (x : Nat) : (x = x → p) → p := by
@@ -110,7 +110,7 @@ example (p : Prop) (x : Nat) : (x = x → p) → p := by
     apply implies_congr
     . apply implies_congr
       simp
-  traceState
+  trace_state
   conv =>
     lhs
     simp
@@ -120,11 +120,11 @@ example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat) (h₁ : ∀ z, f
   conv =>
     pattern _ + _
     apply Nat.zero_add
-  traceState
+  trace_state
   conv =>
     pattern 0 + _
     apply Nat.zero_add
-  traceState
+  trace_state
   simp [h₁, h₂]
 
 example (x y : Nat) (h : y = 0) : x + ((y + x) + x) = x + (x + x) := by
@@ -132,7 +132,7 @@ example (x y : Nat) (h : y = 0) : x + ((y + x) + x) = x + (x + x) := by
     lhs
     rhs
     lhs
-    traceState
+    trace_state
     rw [h, Nat.zero_add]
 
 example (p : Nat → Prop) (x y : Nat) (h : y = 0) : p (y + x) := by
@@ -147,7 +147,7 @@ example (p : Prop) : p := by
 example (p : Nat → Prop) (x y : Nat) (h1 : y = 0) (h2 : p x) : p (y + x) := by
   conv =>
     rhs
-    traceState
+    trace_state
     rw [h1]
     apply Nat.zero_add
   exact h2
diff --git a/tests/lean/delta.lean b/tests/lean/delta.lean
index 1aabb8a71a..7edb5dd4a8 100644
--- a/tests/lean/delta.lean
+++ b/tests/lean/delta.lean
@@ -2,7 +2,7 @@ def f (x : Nat) : Nat := x + 1
 
 example (x y : Nat) (h : f x = 0) : False := by
   delta f at h
-  traceState
+  trace_state
   contradiction
 
 example (x y : Nat) (h : f x = 0) : False := by
@@ -16,7 +16,7 @@ example (x y : Nat) (h1 : f x = 0) (h2 : 0 = 0) : False := by
 
 example (x y : Nat) (h1 : f x = 0) (h2 : 0 = 0) : False := by
   delta f at *
-  traceState
+  trace_state
   contradiction
 
 example (x y : Nat) (h2 : 0 = 0) : False := by
diff --git a/tests/lean/hidingInaccessibleNames.lean b/tests/lean/hidingInaccessibleNames.lean
index fffa3cbb52..c4028786fe 100644
--- a/tests/lean/hidingInaccessibleNames.lean
+++ b/tests/lean/hidingInaccessibleNames.lean
@@ -12,7 +12,7 @@ def f' : (xs : List Nat) → Nat → xs ≠ [] → Nat
 theorem ex1 : p ∨ q → q ∨ p := by
   intro h
   cases h
-  traceState
+  trace_state
   apply Or.inr
   assumption
   apply Or.inl
diff --git a/tests/lean/inductionGen.lean b/tests/lean/inductionGen.lean
index 37a511243e..c20f580c66 100644
--- a/tests/lean/inductionGen.lean
+++ b/tests/lean/inductionGen.lean
@@ -25,7 +25,7 @@ theorem ex1 (xs ys : Vec α (n+1)) (h : xs = ys) : xs.head = ys.head := by
 theorem ex2 (xs ys : Vec α (n+1)) (h : xs = ys) : xs.head = ys.head := by
   cases xs with
   | cons x xs =>
-    traceState -- `h` has been refined
+    trace_state -- `h` has been refined
     repeat admit
 
 inductive ExprType where
@@ -64,5 +64,5 @@ def eval : Expr α → denoteType α
 theorem ex3 (a b : Expr α) (h : a = b) : eval (constProp a) = eval b := by
   set_option trace.Meta.debug true in
   induction a
-  traceState -- b's type must have been refined, `h` too
+  trace_state -- b's type must have been refined, `h` too
   repeat admit
diff --git a/tests/lean/letFun.lean b/tests/lean/letFun.lean
index 0da44ce333..15aa199710 100644
--- a/tests/lean/letFun.lean
+++ b/tests/lean/letFun.lean
@@ -6,5 +6,5 @@
 
 example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (let_fun x := a + 1; x + x) > b := by
   simp (config := { beta := false }) [h1]
-  traceState
+  trace_state
   simp [h2]
diff --git a/tests/lean/matchOfNatIssue.lean b/tests/lean/matchOfNatIssue.lean
index c8f9f6bf2a..0ffdce3d4f 100644
--- a/tests/lean/matchOfNatIssue.lean
+++ b/tests/lean/matchOfNatIssue.lean
@@ -1,6 +1,6 @@
 example (x : Int) (h : x = 2) : Int.div 2 1 = x := by
   simp [Int.div]
-  traceState
+  trace_state
   simp [h]
 
 example (n : Nat) : Int.div (Int.ofNat n) (Int.ofNat 0) = Int.ofNat (n / 0) := by
diff --git a/tests/lean/renameI.lean b/tests/lean/renameI.lean
index e01bb20a50..70173877f6 100644
--- a/tests/lean/renameI.lean
+++ b/tests/lean/renameI.lean
@@ -1,17 +1,17 @@
 example : (m n : Nat) → m = n := by
   intro y y
-  renameI x
-  traceState
+  rename_i x
+  trace_state
   admit
 
 example : (m n : Nat) → m = n := by
   intro a.b a.b
-  renameI x
-  traceState
+  rename_i x
+  trace_state
   admit
 
 example : (m o p n: Nat) → m + p = n + o := by
   intro a.b _ _ a.b
-  renameI x _ y
-  traceState
+  rename_i x _ y
+  trace_state
   admit
diff --git a/tests/lean/revertlet.lean b/tests/lean/revertlet.lean
index 882e9a3e67..4d3de8184b 100644
--- a/tests/lean/revertlet.lean
+++ b/tests/lean/revertlet.lean
@@ -2,7 +2,7 @@ theorem ex (n : Nat) (h : n = 0) : 0 + n = 0 := by
   let m := n + 1
   let v := m + 1
   have : v = n + 2 := rfl
-  traceState
+  trace_state
   subst h
-  traceState
+  trace_state
   rfl
diff --git a/tests/lean/rewrite.lean b/tests/lean/rewrite.lean
index 5e9245a74b..d49f2b4bec 100644
--- a/tests/lean/rewrite.lean
+++ b/tests/lean/rewrite.lean
@@ -4,7 +4,7 @@ axiom reverseEq {α} (as : List α) : as.reverse.reverse = as
 
 theorem ex1 {α} (as bs : List α) : as.reverse.reverse ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs) := by
   rw [appendNil, appendNil, reverseEq];
-  traceState;
+  trace_state;
   rw [←appendAssoc];
 
 
@@ -16,7 +16,7 @@ axiom zeroAdd (x : Nat) : 0 + x = x
 
 theorem ex2 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
 rewrite [zeroAdd] at h₁ h₂;
-traceState;
+trace_state;
 subst x;
 subst y;
 exact rfl
@@ -33,7 +33,7 @@ done
 
 theorem ex5 (m n k : Nat) (h : 0 + n = m) (h : k = m) : k = n := by
 rw [zeroAdd] at *;
-traceState; -- `h` is still a name for `h : k = m`
+trace_state; -- `h` is still a name for `h : k = m`
 refine Eq.trans h ?hole;
 apply Eq.symm;
 assumption
diff --git a/tests/lean/run/387.lean b/tests/lean/run/387.lean
index 00e2947a05..24b6c66cdb 100644
--- a/tests/lean/run/387.lean
+++ b/tests/lean/run/387.lean
@@ -12,7 +12,7 @@ example : p 0 0 := by
   simp [foo 0]
 example : p 0 0 ∧ p 1 1 := by
   simp [foo 1]
-  traceState
+  trace_state
   simp [foo 0]
 
 namespace Foo
diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean
index 7309ad62d8..58074ff0cd 100644
--- a/tests/lean/run/allGoals.lean
+++ b/tests/lean/run/allGoals.lean
@@ -28,7 +28,7 @@ def Weekday.previous : Weekday -> Weekday
 
 theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d := by
   cases d
-  allGoals rfl
+  all_goals rfl
 
 theorem Weekday.nextOfPrevious' (d : Weekday) : previous (next d) = d ∧ next (previous d) = d := by
   apply And.intro
@@ -49,15 +49,15 @@ theorem idEq (a : α) : id a = a :=
 
 theorem Weekday.test (d : Weekday) : next (previous d) = id d := by
   cases d
-  traceState
-  allGoals rw [idEq]
-  traceState
-  allGoals rfl
+  trace_state
+  all_goals rw [idEq]
+  trace_state
+  all_goals rfl
 
 theorem Weekday.test2 (d : Weekday) : next (previous d) = id d := by
   cases d <;> rw [idEq]
-  traceState
-  allGoals rfl
+  trace_state
+  all_goals rfl
 
 def bug {a b c : Nat} (h₁ : a = b) (h₂ : b = c) : a = c := by
   apply Eq.trans <;> assumption
diff --git a/tests/lean/run/conv1.lean b/tests/lean/run/conv1.lean
index 09bbb55347..89da47cf5b 100644
--- a/tests/lean/run/conv1.lean
+++ b/tests/lean/run/conv1.lean
@@ -8,7 +8,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
     congr
     . skip
     . whnf; skip
-  traceState
+  trace_state
   rw [Nat.add_comm]
   rfl
 
@@ -17,7 +17,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
     whnf
     rhs
     whnf
-  traceState
+  trace_state
   rw [Nat.add_comm]
   rfl
 
@@ -29,7 +29,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
   conv =>
     rhs
     whnf
-  traceState
+  trace_state
   apply Nat.add_comm x y
 
 example (x y : Nat) : p (x + y) (0 + y + x) := by
@@ -37,7 +37,7 @@ example (x y : Nat) : p (x + y) (0 + y + x) := by
     whnf
     rhs
     rw [Nat.zero_add, Nat.add_comm]
-    traceState
+    trace_state
     skip
     done
 
@@ -89,9 +89,9 @@ example (h₁ : f x = x + 1) (h₂ : x > 0) : f x = f x := by
 
 example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat) (h₁ : ∀ z, f z z = z) (h₂ : ∀ x y, f (g x) (g y) = y) : f (g (0 + y)) (f (g x) (g (x + 0))) = x := by
   conv in _ + 0 => apply Nat.add_zero
-  traceState
+  trace_state
   conv in 0 + _ => apply Nat.zero_add
-  traceState
+  trace_state
   simp [h₁, h₂]
 
 example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat)
@@ -99,7 +99,7 @@ example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat)
         (h₃ : f (g (0 + x)) (g x) = 0)
  : g x = 0 := by
   conv at h₃ in 0 + x => apply Nat.zero_add
-  traceState
+  trace_state
   conv at h₃ => lhs; apply h₁
-  traceState
+  trace_state
   assumption
diff --git a/tests/lean/run/elab_cmd.lean b/tests/lean/run/elab_cmd.lean
index 7d598eb60d..00f2053db3 100644
--- a/tests/lean/run/elab_cmd.lean
+++ b/tests/lean/run/elab_cmd.lean
@@ -28,8 +28,8 @@ by {
   intro h1; intro h2; intro h3;
   apply @Eq.trans;
   try exact h1; -- `exact h1` fails
-  traceState;
+  trace_state;
   try exact h3;
-  traceState;
+  trace_state;
   try exact h1;
 }
diff --git a/tests/lean/run/eqThm.lean b/tests/lean/run/eqThm.lean
index cf7f211e55..7ef40eb157 100644
--- a/tests/lean/run/eqThm.lean
+++ b/tests/lean/run/eqThm.lean
@@ -10,7 +10,7 @@ macro "urfl" : tactic => `(set_option smartUnfolding false in rfl)
 
 
 theorem f_main_eq : f x b = f.match_1 (fun _ _ => Nat) x b (fun _ => 1) (fun _ => 2) (fun _ => 3) (fun _ => 4) (fun x => f x true) (fun x b => f x (not b)) := by
-  split <;> (first | rfl | (conv => lhs; delta f; whnf; simpMatch); try urfl)
+  split <;> (first | rfl | (conv => lhs; delta f; whnf; simp_match); try urfl)
 
 #check @f_main_eq
 
@@ -22,7 +22,7 @@ def g : List Nat → List Nat → Nat
   | x::xs,      []    => g xs []
 
 theorem g_main_eq (xs ys : List Nat) : g xs ys = g.match_1 (fun _ _ => Nat) xs ys (fun y ys => y) (fun _ => 0) (fun _ _ xs ys => g xs ys) (fun _ xs y ys => g xs ys + y) (fun _ xs => g xs []) := by
-  split <;> (first | rfl | (conv => lhs; delta g; whnf; simpMatch); try urfl)
+  split <;> (first | rfl | (conv => lhs; delta g; whnf; simp_match); try urfl)
 
 #check @g_main_eq
 
diff --git a/tests/lean/run/generalizeMany.lean b/tests/lean/run/generalizeMany.lean
index 846a3d2ba7..c3afdd4924 100644
--- a/tests/lean/run/generalizeMany.lean
+++ b/tests/lean/run/generalizeMany.lean
@@ -9,5 +9,5 @@ example (p : (n : Nat) → Fin n → Prop)
         (v : Fin n)
         : p n.succ v.succ := by
   generalize h₁ : n.succ = n', h₂ : v.succ = v'
-  traceState
+  trace_state
   admit
diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
index e38f2a5aa6..3a30b1b92f 100644
--- a/tests/lean/run/induction1.lean
+++ b/tests/lean/run/induction1.lean
@@ -55,7 +55,7 @@ theorem tst11 {p q r : Prop } (h₁ : Iff2 r p q) (h₂ : p) : q := by
   | intro h _ => exact h h₂
 
 theorem tst12 {p q : Prop } (h₁ : p ∨ q) (h₂ : p ↔ q) (h₃ : p) : q := by
-  failIfSuccess induction h₁ using Iff.casesOn
+  fail_if_success induction h₁ using Iff.casesOn
   induction h₂ using Iff.casesOn with
   | intro h _ =>
     exact h h₃
@@ -88,7 +88,7 @@ def getHeads {α β} {n} (xs : Vec α (n+1)) (ys : Vec β (n+1)) : α × β := b
   cases ys
   apply Prod.mk
   repeat
-    traceState
+    trace_state
     assumption
   done
 
diff --git a/tests/lean/run/multiTargetCasesInductionIssue.lean b/tests/lean/run/multiTargetCasesInductionIssue.lean
index fa1f6147f5..507d9919bc 100644
--- a/tests/lean/run/multiTargetCasesInductionIssue.lean
+++ b/tests/lean/run/multiTargetCasesInductionIssue.lean
@@ -25,7 +25,7 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co
   induction n+2, Vec.cons a (Vec.cons a as) using Vec.casesOn
   case nil => constructor
   case cons n a as ih =>
-    traceState
+    trace_state
     constructor
 
 #print "-----"
@@ -34,7 +34,7 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co
   cases n+2, Vec.cons a (Vec.cons a as) using Vec.casesOn
   case nil => constructor
   case cons n a as ih =>
-    traceState
+    trace_state
     constructor
 
 #print "-----"
@@ -43,5 +43,5 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co
   cases h₁ : n+2, h₂ : Vec.cons a (Vec.cons a as) using Vec.casesOn
   case nil => constructor
   case cons n' a' as' ih =>
-    traceState
+    trace_state
     constructor
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index e0c1a6e7f2..b118ccc847 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -108,7 +108,7 @@ case pre => exact h3
 
 theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z := by
 intros h1 _ h3
-traceState
+trace_state
 focus
   refine' Eq.trans ?pre ?post
   first
@@ -120,7 +120,7 @@ focus
 
 theorem simple9b (x y z : Nat) : y = z → x = x → x = y → x = z := by
 intros h1 _ h3
-traceState
+trace_state
 focus
   refine' Eq.trans ?pre ?post
   first
@@ -168,7 +168,7 @@ theorem simple11 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro h2; intro h3;
   apply @Eq.trans;
-  traceState;
+  trace_state;
   exact h3;
   assumption
 }
@@ -178,26 +178,26 @@ by {
   intro h1; intro h2; intro h3;
   apply @Eq.trans;
   try exact h1; -- `exact h1` fails
-  traceState;
+  trace_state;
   try exact h3;
-  traceState;
+  trace_state;
   try exact h1;
 }
 
 theorem simple13 (x y z : Nat) : y = z → x = x → x = y → x = z := by
 intros h1 h2 h3
-traceState
+trace_state
 apply @Eq.trans
 case b => exact y
-traceState
+trace_state
 repeat assumption
 
 theorem simple13b (x y z : Nat) : y = z → x = x → x = y → x = z := by {
 intros h1 h2 h3;
-traceState;
+trace_state;
 apply @Eq.trans;
 case b => exact y;
-traceState;
+trace_state;
 repeat assumption
 }
 
@@ -222,7 +222,7 @@ by {
   intros h1 h2 h3;
   try clear x; -- should fail
   clear h2;
-  traceState;
+  trace_state;
   apply Eq.trans;
   exact h3;
   exact h1
@@ -372,7 +372,7 @@ theorem simple20 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by intros h1 h2 h3;
    try clear x; -- should fail
    clear h2;
-   traceState;
+   trace_state;
    apply Eq.trans;
    exact h3;
    exact h1
diff --git a/tests/lean/run/renameI.lean b/tests/lean/run/renameI.lean
index b2961a5c2c..6dde569c2f 100644
--- a/tests/lean/run/renameI.lean
+++ b/tests/lean/run/renameI.lean
@@ -1,6 +1,6 @@
 example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := by
   intros
-  renameI h1 _ h2
+  rename_i h1 _ h2
   apply Eq.trans
   apply Eq.symm
   exact h2
diff --git a/tests/lean/run/simpStar.lean b/tests/lean/run/simpStar.lean
index aa03034180..c44dc2783d 100644
--- a/tests/lean/run/simpStar.lean
+++ b/tests/lean/run/simpStar.lean
@@ -12,7 +12,7 @@ axiom g_ax (x : Nat) : g x = 0
 
 theorem ex3 (x y : Nat) (h₁ : f x x = g x) (h₂ : f x x < 5) : f x x + f x x = 0 := by
   simp [*] at *
-  traceState
+  trace_state
   have aux₁ : f x x = g x := h₁
   have aux₂ : g x < 5     := h₂
   simp [g_ax]
diff --git a/tests/lean/run/split3.lean b/tests/lean/run/split3.lean
index f7137ff10a..1fc0342a95 100644
--- a/tests/lean/run/split3.lean
+++ b/tests/lean/run/split3.lean
@@ -6,8 +6,8 @@ def g (xs ys : List Nat) : Nat :=
 
 example (a b : Bool) (x y z : Nat) (xs : List Nat) (h1 : (if a then x else y) = 0) (h2 : xs.head! = 0) : g [x] xs = 1 := by
   simp [g]
-  repeat anyGoals (split at *)
-  anyGoals (first | decide | contradiction | injections)
+  repeat any_goals (split at *)
+  any_goals (first | decide | contradiction | injections)
   next b c _ _ _ =>
     show Nat.succ b = 1
     subst xs; simp [List.head!] at h2; simp [h2]
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index d03c295fd3..694b771188 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -3,7 +3,7 @@ import Lean.CoreM
 open Lean
 
 structure MyState :=
-(traceState : TraceState := {})
+(trace_state : TraceState := {})
 (s          : Nat := 0)
 
 abbrev M := CoreM
diff --git a/tests/lean/rwWithoutOffsetCnstrs.lean b/tests/lean/rwWithoutOffsetCnstrs.lean
index 9c4947d052..2db3af5eea 100644
--- a/tests/lean/rwWithoutOffsetCnstrs.lean
+++ b/tests/lean/rwWithoutOffsetCnstrs.lean
@@ -4,5 +4,5 @@ macro "rw0" s:rwRuleSeq : tactic =>
 
 example (m n : Nat) : Nat.ble (n+1) (n+0) = false := by
   rw0 [Nat.add_zero]
-  traceState
+  trace_state
   admit
diff --git a/tests/lean/simpDisch.lean b/tests/lean/simpDisch.lean
index 9fce860d85..fd3df0c13c 100644
--- a/tests/lean/simpDisch.lean
+++ b/tests/lean/simpDisch.lean
@@ -2,10 +2,10 @@ constant f : Nat → Nat
 @[simp] axiom fEq (x : Nat) (h : x ≠ 0) : f x = x
 
 example (x : Nat) (h : x ≠ 0) : f x = x + 0 := by
-  simp (discharger := traceState; exact (fun h' => h') h)
+  simp (discharger := trace_state; exact (fun h' => h') h)
 
 example (x y : Nat) (h1 : x ≠ 0) (h2 : y ≠ 0) (h3 : x = y) : f x = f y + 0 := by
-  simp (discharger := traceState; assumption)
+  simp (discharger := trace_state; assumption)
   assumption
 
 example (x y : Nat) (h1 : x ≠ 0) (h2 : y ≠ 0) (h3 : x = y) : f x = f y + 0 := by
@@ -18,7 +18,7 @@ example (x y : Nat) (h1 : x ≠ 0) (h2 : y ≠ 0) (h3 : x = y) : f x = f y + 0 :
 
 example (x y : Nat) (h1 : x ≠ 0) (h2 : y ≠ 0) (h3 : x = y) : f x = f y + 0 := by
   conv => lhs; simp (disch := assumption)
-  traceState
+  trace_state
   conv => rhs; simp (disch := assumption)
-  traceState
+  trace_state
   assumption
diff --git a/tests/lean/simpPrefixIssue.lean b/tests/lean/simpPrefixIssue.lean
index 315e03f00e..3cea894032 100644
--- a/tests/lean/simpPrefixIssue.lean
+++ b/tests/lean/simpPrefixIssue.lean
@@ -4,5 +4,5 @@ axiom f_eq {α : Sort u} (a : α) : f a = a
 
 example (a : Nat) : f id a = a := by
   simp only [f_eq]
-  traceState
+  trace_state
   rfl
diff --git a/tests/lean/simpZetaFalse.lean b/tests/lean/simpZetaFalse.lean
index da973bcc5f..8e26af76e6 100644
--- a/tests/lean/simpZetaFalse.lean
+++ b/tests/lean/simpZetaFalse.lean
@@ -3,26 +3,26 @@ axiom f_eq (x : Nat) : f (f x) = x
 
 theorem ex1 (x : Nat) (h : f (f x) = x) : (let y := x*x; if f (f x) = x then 1 else y + 1) = 1 := by
   simp (config := { zeta := false }) only [h]
-  traceState
+  trace_state
   simp
 
 #print ex1 -- uses let_congr
 
 theorem ex2 (x z : Nat) (h : f (f x) = x) (h' : z = x) : (let y := f (f x); y) = z := by
   simp (config := { zeta := false }) only [h]
-  traceState
+  trace_state
   simp [h']
 
 #print ex2 -- uses let_val_congr
 
 theorem ex3 (x z : Nat) : (let α := Nat; (fun x : α => 0 + x)) = id := by
   simp (config := { zeta := false })
-  traceState -- should not simplify let body since `fun α : Nat => fun x : α => 0 + x` is not type correct
+  trace_state -- should not simplify let body since `fun α : Nat => fun x : α => 0 + x` is not type correct
   simp [id]
 
 theorem ex4 (p : Prop) (h : p) : (let n := 10; fun x : { z : Nat // z < n } => x = x) = fun z => p := by
   simp (config := { zeta := false })
-  traceState
+  trace_state
   simp [h]
 
 #print ex4 -- uses let_body_congr
diff --git a/tests/lean/simpcfg.lean b/tests/lean/simpcfg.lean
index e0803ad9ed..16c6019c2b 100644
--- a/tests/lean/simpcfg.lean
+++ b/tests/lean/simpcfg.lean
@@ -1,6 +1,6 @@
 theorem ex6 (f : Nat → Nat) (x y z : Nat) (h : (x, z).1 = (fun x => x) y) : f x = f y := by
   simp (config := { beta := false }) at h
-  traceState
+  trace_state
   simp at h
-  traceState
+  trace_state
   simp [h]
diff --git a/tests/lean/smartUnfolding.lean b/tests/lean/smartUnfolding.lean
index 1c62670e82..243a863d2d 100644
--- a/tests/lean/smartUnfolding.lean
+++ b/tests/lean/smartUnfolding.lean
@@ -1,6 +1,6 @@
 theorem ex1 (x y : Nat) (h : x + 2 = y + 2) : x = y := by
   injection h with h
-  traceState -- without smart unfolding the state would be a mess
+  trace_state -- without smart unfolding the state would be a mess
   injection h with h
-  traceState -- without smart unfolding the state would be a mess
+  trace_state -- without smart unfolding the state would be a mess
   assumption
diff --git a/tests/lean/substlet.lean b/tests/lean/substlet.lean
index 3a90761d2d..aa903ba537 100644
--- a/tests/lean/substlet.lean
+++ b/tests/lean/substlet.lean
@@ -3,9 +3,9 @@ theorem ex1 (n : Nat) : 0 + n = n := by
   have h : ∃ k, id k = m := ⟨m, rfl⟩
   cases h with
   | intro a e =>
-    traceState
+    trace_state
     subst e
-    traceState
+    trace_state
     apply Nat.zero_add
 
 theorem ex2 (n : Nat) : 0 + n = n := by
@@ -13,9 +13,9 @@ theorem ex2 (n : Nat) : 0 + n = n := by
   have h : ∃ k, m = id k := ⟨m, rfl⟩
   cases h with
   | intro a e =>
-    traceState
+    trace_state
     subst e
-    traceState
+    trace_state
     apply Nat.zero_add
 
 theorem ex3 (n : Nat) (h : n = 0) : 0 + n = 0 := by