diff --git a/tests/lean/inductionErrors.lean b/tests/lean/inductionErrors.lean
index 608c8b9681..9bc246952f 100644
--- a/tests/lean/inductionErrors.lean
+++ b/tests/lean/inductionErrors.lean
@@ -10,13 +10,13 @@ theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx with
   | lower d => apply Or.inl -- Error
   | upper d => apply Or.inr -- Error
-  | diag    => apply Or.inl; apply Nat.leRefl
+  | diag    => apply Or.inl; apply Nat.le_refl
 
 theorem ex2 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx2 with -- Error
   | lower d => apply Or.inl
   | upper d => apply Or.inr
-  | diag    => apply Or.inl; apply Nat.leRefl
+  | diag    => apply Or.inl; apply Nat.le_refl
 
 theorem ex3 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p /- Error -/ using elimEx with
@@ -28,7 +28,7 @@ theorem ex4 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p using Nat.add with -- Error
   | lower d => apply Or.inl
   | upper d => apply Or.inr
-  | diag    => apply Or.inl; apply Nat.leRefl
+  | diag    => apply Or.inl; apply Nat.le_refl
 
 theorem ex5 (x : Nat) : 0 + x = x := by
   match x with
@@ -58,19 +58,19 @@ theorem ex8 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx with
   | lower d => apply Or.inl; admit
   | upper2 /- Error -/ d => apply Or.inr
-  | diag    => apply Or.inl; apply Nat.leRefl
+  | diag    => apply Or.inl; apply Nat.le_refl
 
 theorem ex9 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx with
   | lower d => apply Or.inl; admit
   | _ => apply Or.inr; admit
-  | diag    => apply Or.inl; apply Nat.leRefl
+  | diag    => apply Or.inl; apply Nat.le_refl
 
 theorem ex10 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx with
   | lower d => apply Or.inl; admit
   | upper d => apply Or.inr; admit
-  | diag    => apply Or.inl; apply Nat.leRefl
+  | diag    => apply Or.inl; apply Nat.le_refl
   | _  /- error unused -/ => admit
 
 theorem ex11 (p q : Nat) : p ≤ q ∨ p > q := by
@@ -78,4 +78,4 @@ theorem ex11 (p q : Nat) : p ≤ q ∨ p > q := by
   | lower d => apply Or.inl; admit
   | upper d => apply Or.inr; admit
   | lower d /- error unused -/ => apply Or.inl; admit
-  | diag    => apply Or.inl; apply Nat.leRefl
+  | diag    => apply Or.inl; apply Nat.le_refl
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index 264103da1c..6b9d954e7f 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -75,9 +75,9 @@
             x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabIdent
               x : Nat @ ⟨17, 43⟩-⟨17, 44⟩
   fun x y b =>
-    ofEqTrue
+    of_eq_true
       (Eq.trans (congrFun (β := fun a => Prop) (f := Eq (x + 0)) (g := Eq x) (congrArg Eq (Nat.add_zero _)) _)
-        (eqSelf x)) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨18, 2⟩-⟨19, 8⟩ @ Lean.Elab.Term.elabFun
+        (eq_self x)) : ∀ (x y : Nat), Bool → x + 0 = x @ ⟨18, 2⟩-⟨19, 8⟩ @ Lean.Elab.Term.elabFun
     Nat : Type @ ⟨18, 6⟩†-⟨18, 7⟩† @ Lean.Elab.Term.elabHole
     x : Nat @ ⟨18, 6⟩-⟨18, 7⟩
     Nat : Type @ ⟨18, 8⟩†-⟨18, 9⟩† @ Lean.Elab.Term.elabHole
diff --git a/tests/lean/interactive/plainTermGoal.lean b/tests/lean/interactive/plainTermGoal.lean
index 096f799c5c..109a3540e0 100644
--- a/tests/lean/interactive/plainTermGoal.lean
+++ b/tests/lean/interactive/plainTermGoal.lean
@@ -1,11 +1,11 @@
-
+--
 example : 0 < 2 :=
-  Nat.ltTrans Nat.zeroLtOne (Nat.ltSuccSelf _)
-           --^ $/lean/plainTermGoal
+  Nat.lt_trans Nat.zero_lt_one (Nat.lt_succ_self _)
             --^ $/lean/plainTermGoal
              --^ $/lean/plainTermGoal
-                           --^ $/lean/plainTermGoal
-                                          --^ $/lean/plainTermGoal
+              --^ $/lean/plainTermGoal
+                             --^ $/lean/plainTermGoal
+                                              --^ $/lean/plainTermGoal
 
 example : OptionM Unit := do
   let y : Int ← none
@@ -14,14 +14,14 @@ example : OptionM Unit := do
   return ()
 
 example (m n : Nat) : m < n :=
-  Nat.ltTrans _ _
-              --^ $/lean/plainTermGoal
+  Nat.lt_trans _ _
+               --^ $/lean/plainTermGoal
 
 example : True := sorry
                 --^ $/lean/plainTermGoal
 
 example : ∀ n, n < n + 42 :=
-  fun n => Nat.ltOfLeOfLt (Nat.leAddRight n 41) (Nat.ltSuccSelf _)
+  fun n => Nat.lt_of_le_of_lt (Nat.le_add_right n 41) (Nat.lt_succ_self _)
 --^ $/lean/plainTermGoal
     --^ $/lean/plainTermGoal
 
@@ -29,7 +29,7 @@ example : ∀ n, n < 1 + n := by
   intro n
   rw [Nat.add_comm]
     --^ $/lean/plainTermGoal
-  exact Nat.ltSuccSelf _
+  exact Nat.lt_succ_self _
       --^ $/lean/plainTermGoal
 
 #check fun (n m : Nat) => m
diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out
index df77cd0568..d761e97d4b 100644
--- a/tests/lean/interactive/plainTermGoal.lean.expected.out
+++ b/tests/lean/interactive/plainTermGoal.lean.expected.out
@@ -1,37 +1,37 @@
-{"textDocument": {"uri": "file://plainTermGoal.lean"},
- "position": {"line": 2, "character": 13}}
-{"range":
- {"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 46}},
- "goal": "⊢ 0 < 2"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 2, "character": 14}}
 {"range":
- {"start": {"line": 2, "character": 14}, "end": {"line": 2, "character": 27}},
- "goal": "⊢ 0 < 1"}
+ {"start": {"line": 2, "character": 2}, "end": {"line": 2, "character": 51}},
+ "goal": "⊢ 0 < 2"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 2, "character": 15}}
 {"range":
- {"start": {"line": 2, "character": 14}, "end": {"line": 2, "character": 27}},
+ {"start": {"line": 2, "character": 15}, "end": {"line": 2, "character": 30}},
  "goal": "⊢ 0 < 1"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
- "position": {"line": 2, "character": 29}}
+ "position": {"line": 2, "character": 16}}
 {"range":
- {"start": {"line": 2, "character": 29}, "end": {"line": 2, "character": 45}},
+ {"start": {"line": 2, "character": 15}, "end": {"line": 2, "character": 30}},
+ "goal": "⊢ 0 < 1"}
+{"textDocument": {"uri": "file://plainTermGoal.lean"},
+ "position": {"line": 2, "character": 31}}
+{"range":
+ {"start": {"line": 2, "character": 31}, "end": {"line": 2, "character": 51}},
  "goal": "⊢ 1 < 2"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
- "position": {"line": 2, "character": 44}}
+ "position": {"line": 2, "character": 48}}
 {"range":
- {"start": {"line": 2, "character": 44}, "end": {"line": 2, "character": 45}},
- "goal": "⊢ Nat"}
+ {"start": {"line": 2, "character": 32}, "end": {"line": 2, "character": 50}},
+ "goal": "⊢ 1 < 2"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 11, "character": 10}}
 {"range":
  {"start": {"line": 11, "character": 10}, "end": {"line": 11, "character": 18}},
  "goal": "y : Int\n⊢ OptionM Nat"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
- "position": {"line": 16, "character": 16}}
+ "position": {"line": 16, "character": 17}}
 {"range":
- {"start": {"line": 16, "character": 16}, "end": {"line": 16, "character": 17}},
+ {"start": {"line": 16, "character": 17}, "end": {"line": 16, "character": 18}},
  "goal": "m n : Nat\n⊢ ?m m n < n"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 19, "character": 18}}
@@ -41,7 +41,7 @@
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 23, "character": 2}}
 {"range":
- {"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 66}},
+ {"start": {"line": 23, "character": 2}, "end": {"line": 23, "character": 74}},
  "goal": "⊢ ∀ (n : Nat), n < n + 42"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 23, "character": 6}}
@@ -56,7 +56,7 @@
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 31, "character": 8}}
 {"range":
- {"start": {"line": 31, "character": 8}, "end": {"line": 31, "character": 24}},
+ {"start": {"line": 31, "character": 8}, "end": {"line": 31, "character": 26}},
  "goal": "n : Nat\n⊢ n < n + 1"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 34, "character": 14}}
diff --git a/tests/lean/modBug.lean b/tests/lean/modBug.lean
index 5e664c22c7..61b5357d23 100644
--- a/tests/lean/modBug.lean
+++ b/tests/lean/modBug.lean
@@ -1 +1 @@
-theorem proofOfFalse : False := Nat.zeroNeOne (Nat.mod_zero 1)
+theorem proofOfFalse : False := Nat.zero_ne_one (Nat.mod_zero 1)
diff --git a/tests/lean/modBug.lean.expected.out b/tests/lean/modBug.lean.expected.out
index ee4f0d2636..8be39d4ea7 100644
--- a/tests/lean/modBug.lean.expected.out
+++ b/tests/lean/modBug.lean.expected.out
@@ -1,5 +1,5 @@
-modBug.lean:1:32-1:62: error: application type mismatch
-  Nat.zeroNeOne (Nat.mod_zero _)
+modBug.lean:1:32-1:64: error: application type mismatch
+  Nat.zero_ne_one (Nat.mod_zero _)
 argument
   Nat.mod_zero _
 has type
diff --git a/tests/lean/run/394.lean b/tests/lean/run/394.lean
index 1d0e284aca..7b09bfb15b 100644
--- a/tests/lean/run/394.lean
+++ b/tests/lean/run/394.lean
@@ -1,7 +1,7 @@
 def casesTFOn {motive : Prop → Sort _} (P) [inst : Decidable P] : (T : motive True) → (F : motive False) → motive P :=
   λ ht hf => match inst with
-  | isTrue H => eqTrue H ▸ ht
-  | isFalse H => eqFalse H ▸ hf
+  | isTrue H => eq_true H ▸ ht
+  | isFalse H => eq_false H ▸ hf
 
 example (P) [Decidable P] : ¬¬P → P := by
   induction P using casesTFOn
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 27513be5d0..7b2caf87a7 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -312,7 +312,6 @@ def typeAs (α : Type u) (a : α) := ()
 #testDelabN instInhabitedPUnit
 #testDelabN Lean.Syntax.getOptionalIdent?
 #testDelabN Lean.Meta.ppExpr
-#testDelabN Eq.mprProp
 #testDelabN MonadLift.noConfusion
 #testDelabN MonadLift.noConfusionType
 #testDelabN MonadExcept.noConfusion
@@ -327,7 +326,7 @@ def typeAs (α : Type u) (a : α) := ()
 
 -- TODO: for some reason this *only* works when trusting subst
 set_option pp.analyze.trustSubst true in
-#testDelabN Lean.Simp.and_false
+#testDelabN and_false
 
 -- TODO: this one prints out a structure instance with keyword field `end`
 set_option pp.structureInstances false in
diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean
index 2406ab4a90..b7c2f2cc01 100644
--- a/tests/lean/run/bigop.lean
+++ b/tests/lean/run/bigop.lean
@@ -28,11 +28,11 @@ instance : Enumerable Bool :=
 
 partial def finElemsAux (n : Nat) : (i : Nat) → i < n → List (Fin n)
 | 0,   h => [⟨0, h⟩]
-| i+1, h => ⟨i+1, h⟩ :: finElemsAux n i (Nat.ltOfSuccLt h)
+| i+1, h => ⟨i+1, h⟩ :: finElemsAux n i (Nat.lt_of_succ_lt h)
 
 partial def finElems : (n : Nat) → List (Fin n)
 | 0     => []
-| (n+1) => finElemsAux (n+1) n (Nat.ltSuccSelf n)
+| (n+1) => finElemsAux (n+1) n (Nat.lt_succ_self n)
 
 instance {n} : Enumerable (Fin n) :=
 { elems := (finElems n).reverse }
diff --git a/tests/lean/run/casesUsing.lean b/tests/lean/run/casesUsing.lean
index 9f26b0ca4a..0dbe9edda3 100644
--- a/tests/lean/run/casesUsing.lean
+++ b/tests/lean/run/casesUsing.lean
@@ -13,7 +13,7 @@ axiom elimEx (motive : Nat → Nat → Sort u) (x y : Nat)
 
 theorem ex1 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx with
-  | diag    => apply Or.inl; apply Nat.leRefl
+  | diag    => apply Or.inl; apply Nat.le_refl
   | lower d => apply Or.inl; show p ≤ p + d.succ; admit
   | upper d => apply Or.inr; show q + d.succ > q; admit
 
@@ -21,7 +21,7 @@ theorem ex2 (p q : Nat) : p ≤ q ∨ p > q := by
   cases p, q using elimEx
   case lower => admit
   case upper => admit
-  case diag  => apply Or.inl; apply Nat.leRefl
+  case diag  => apply Or.inl; apply Nat.le_refl
 
 axiom Nat.parityElim (motive : Nat → Sort u)
   (even : (n : Nat) → motive (2*n))
@@ -93,10 +93,10 @@ theorem modLt (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
     rw [Nat.mod_eq_sub_mod h₁.2]
     exact ih h
   | base x y h₁ =>
-    match Iff.mp (Decidable.notAndIffOrNot ..) h₁ with
+    match Iff.mp (Decidable.not_and_iff_or_not ..) h₁ with
     | Or.inl h₁ => contradiction
     | Or.inr h₁ =>
-      have hgt := Nat.gtOfNotLe h₁
+      have hgt := Nat.gt_of_not_le h₁
       have heq := Nat.mod_eq_of_lt hgt
       rw [← heq] at hgt
       assumption
@@ -120,7 +120,7 @@ theorem ex13 (p q : Nat) : p ≤ q ∨ p > q := by
   | diag    => ?hdiag
   | lower d => ?hlower
   | upper d => ?hupper
-  case hdiag  => apply Or.inl; apply Nat.leRefl
+  case hdiag  => apply Or.inl; apply Nat.le_refl
   case hlower => apply Or.inl; show p ≤ p + d.succ; admit
   case hupper => apply Or.inr; show q + d.succ > q; admit
 
@@ -129,7 +129,7 @@ theorem ex14 (p q : Nat) : p ≤ q ∨ p > q := by
   | diag    => ?hdiag
   | lower d => _
   | upper d => ?hupper
-  case hdiag  => apply Or.inl; apply Nat.leRefl
+  case hdiag  => apply Or.inl; apply Nat.le_refl
   case lower => apply Or.inl; show p ≤ p + d.succ; admit
   case hupper => apply Or.inr; show q + d.succ > q; admit
 
@@ -138,7 +138,7 @@ theorem ex15 (p q : Nat) : p ≤ q ∨ p > q := by
   | diag    => ?hdiag
   | lower d => _
   | upper d => ?hupper
-  { apply Or.inl; apply Nat.leRefl }
+  { apply Or.inl; apply Nat.le_refl }
   { apply Or.inr; show q + d.succ > q; admit }
   { apply Or.inl; show p ≤ p + d.succ; admit }
 
diff --git a/tests/lean/run/decClassical.lean b/tests/lean/run/decClassical.lean
index ed2d59fd99..81e1ae08bb 100644
--- a/tests/lean/run/decClassical.lean
+++ b/tests/lean/run/decClassical.lean
@@ -5,7 +5,7 @@ theorem ex : if (fun x => x + 1) = (fun x => x + 2) then False else True := by
     intro h
     have : 1 = 2 := congrFun h 0
     contradiction
-  rw [ifNeg this]
+  rw [if_neg this]
   exact True.intro
 
 def tst (x : Nat) : Bool :=
diff --git a/tests/lean/run/def13.lean b/tests/lean/run/def13.lean
index fd23a4565a..f1d185b7b9 100644
--- a/tests/lean/run/def13.lean
+++ b/tests/lean/run/def13.lean
@@ -12,8 +12,8 @@ rfl
 
 theorem filter_cons_of_pos {a : α} (as : List α) (h : p a) : filter p (a :: as) = a :: filter p as := by
 rw [filter_cons];
-rw [ifPos h]
+rw [if_pos h]
 
 theorem filter_cons_of_neg {a : α} (as : List α) (h : ¬ p a) : filter p (a :: as) = filter p as := by
 rw [filter_cons];
-rw [ifNeg h]
+rw [if_neg h]
diff --git a/tests/lean/run/doNotation3.lean b/tests/lean/run/doNotation3.lean
index d19e3095ec..f64703dcc7 100644
--- a/tests/lean/run/doNotation3.lean
+++ b/tests/lean/run/doNotation3.lean
@@ -1,19 +1,19 @@
-theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
+theorem zero_lt_of_lt : {a b : Nat} → a < b → 0 < b
 | 0,   _, h => h
 | a+1, b, h =>
-  have : a < b := Nat.ltTrans (Nat.ltSuccSelf _) h
-  zeroLtOfLt this
+  have : a < b := Nat.lt_trans (Nat.lt_succ_self _) h
+  zero_lt_of_lt this
 
 def fold {m α β} [Monad m] (as : Array α) (b : β) (f : α → β → m β) : m β := do
 let rec loop : (i : Nat) → i ≤ as.size → β → m β
   | 0,   h, b => b
   | i+1, h, b => do
-    have h' : i < as.size          := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
-    have : as.size - 1 < as.size     := Nat.subLt (zeroLtOfLt h') (by decide)
-    have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
+    have h' : i < as.size          := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
+    have : as.size - 1 < as.size     := Nat.sub_lt (zero_lt_of_lt h') (by decide)
+    have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
     let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
-    loop i (Nat.leOfLt h') b
-loop as.size (Nat.leRefl _) b
+    loop i (Nat.le_of_lt h') b
+loop as.size (Nat.le_refl _) b
 
 #eval Id.run $ fold #[1, 2, 3, 4] 0 (pure $ · + ·)
 
@@ -25,12 +25,12 @@ let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
   match i, h with
   | 0,   h => return b
   | i+1, h =>
-    have h' : i < as.size          := Nat.ltOfLtOfLe (Nat.ltSuccSelf i) h
-    have : as.size - 1 < as.size     := Nat.subLt (zeroLtOfLt h') (by decide)
-    have : as.size - 1 - i < as.size := Nat.ltOfLeOfLt (Nat.subLe (as.size - 1) i) this
+    have h' : i < as.size          := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
+    have : as.size - 1 < as.size     := Nat.sub_lt (zero_lt_of_lt h') (by decide)
+    have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
     let b ← f (as.get ⟨as.size - 1 - i, this⟩) b
-    loop i (Nat.leOfLt h') b
-loop as.size (Nat.leRefl _) b
+    loop i (Nat.le_of_lt h') b
+loop as.size (Nat.le_refl _) b
 
 def f (x : Nat) (ref : IO.Ref Nat) : IO Nat := do
 let mut x := x
diff --git a/tests/lean/run/lean3_zulip_issues_1.lean b/tests/lean/run/lean3_zulip_issues_1.lean
index 497f9030bc..9e9cad5693 100644
--- a/tests/lean/run/lean3_zulip_issues_1.lean
+++ b/tests/lean/run/lean3_zulip_issues_1.lean
@@ -29,11 +29,11 @@ def f : wrap → Nat
   | _ => 1
 
 example (a : Nat) : True := by
-  have : ∀ n, n ≥ 0 → a ≤ a := fun _ _ => Nat.leRefl ..
+  have : ∀ n, n ≥ 0 → a ≤ a := fun _ _ => Nat.le_refl ..
   exact True.intro
 
 example (ᾰ : Nat) : True := by
-  have : ∀ n, n ≥ 0 → ᾰ ≤ ᾰ := fun _ _ => Nat.leRefl ..
+  have : ∀ n, n ≥ 0 → ᾰ ≤ ᾰ := fun _ _ => Nat.le_refl ..
   exact True.intro
 
 inductive Vec.{u} (α : Type u) : Nat → Type u
diff --git a/tests/lean/run/matchArrayLit.lean b/tests/lean/run/matchArrayLit.lean
index d0430ea3ec..fa820d6db9 100644
--- a/tests/lean/run/matchArrayLit.lean
+++ b/tests/lean/run/matchArrayLit.lean
@@ -1,17 +1,17 @@
 universe u v
 
 theorem eqLitOfSize0 {α : Type u} (a : Array α) (hsz : a.size = 0) : a = #[] :=
-a.toArrayLitEq 0 hsz
+a.toArrayLit_eq 0 hsz
 
-theorem eqLitOfSize1 {α : Type u} (a : Array α) (hsz : a.size = 1) : a = #[a.getLit 0 hsz (ofDecideEqTrue rfl)] :=
-a.toArrayLitEq 1 hsz
+theorem eqLitOfSize1 {α : Type u} (a : Array α) (hsz : a.size = 1) : a = #[a.getLit 0 hsz (of_decide_eq_true rfl)] :=
+a.toArrayLit_eq 1 hsz
 
-theorem eqLitOfSize2 {α : Type u} (a : Array α) (hsz : a.size = 2) : a = #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl)] :=
-a.toArrayLitEq 2 hsz
+theorem eqLitOfSize2 {α : Type u} (a : Array α) (hsz : a.size = 2) : a = #[a.getLit 0 hsz (of_decide_eq_true rfl), a.getLit 1 hsz (of_decide_eq_true rfl)] :=
+a.toArrayLit_eq 2 hsz
 
 theorem eqLitOfSize3 {α : Type u} (a : Array α) (hsz : a.size = 3) :
-  a = #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl), a.getLit 2 hsz (ofDecideEqTrue rfl)] :=
-a.toArrayLitEq 3 hsz
+  a = #[a.getLit 0 hsz (of_decide_eq_true rfl), a.getLit 1 hsz (of_decide_eq_true rfl), a.getLit 2 hsz (of_decide_eq_true rfl)] :=
+a.toArrayLit_eq 3 hsz
 
 /-
 Matcher for the following patterns
@@ -28,11 +28,11 @@ def matchArrayLit {α : Type u} (C : Array α → Sort v) (a : Array α)
     (h₄ : ∀ a,        C a)
     : C a :=
 if h : a.size = 0 then
-  @Eq.rec _ _ (fun x _ => C x) (h₁ ()) _ (a.toArrayLitEq 0 h).symm
+  @Eq.rec _ _ (fun x _ => C x) (h₁ ()) _ (a.toArrayLit_eq 0 h).symm
 else if h : a.size = 1 then
-  @Eq.rec _ _ (fun x _ => C x) (h₂ (a.getLit 0 h (ofDecideEqTrue rfl))) _ (a.toArrayLitEq 1 h).symm
+  @Eq.rec _ _ (fun x _ => C x) (h₂ (a.getLit 0 h (of_decide_eq_true rfl))) _ (a.toArrayLit_eq 1 h).symm
 else if h : a.size = 3 then
-  @Eq.rec _ _ (fun x _ => C x) (h₃ (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) (a.getLit 2 h (ofDecideEqTrue rfl))) _ (a.toArrayLitEq 3 h).symm
+  @Eq.rec _ _ (fun x _ => C x) (h₃ (a.getLit 0 h (of_decide_eq_true rfl)) (a.getLit 1 h (of_decide_eq_true rfl)) (a.getLit 2 h (of_decide_eq_true rfl))) _ (a.toArrayLit_eq 3 h).symm
 else
   h₄ a
 
diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean
index 325ffc9467..5ef07aca86 100644
--- a/tests/lean/run/matrix.lean
+++ b/tests/lean/run/matrix.lean
@@ -33,14 +33,14 @@ macro_rules
   | `($x[$i, $j]) => `($x $i $j)
 
 def dotProduct [Mul α] [Add α] [Zero α] (u v : Fin m → α) : α :=
-  loop m (Nat.leRefl ..) Zero.zero
+  loop m (Nat.le_refl ..) Zero.zero
 where
   loop (i : Nat) (h : i ≤ m) (acc : α) : α :=
     match i, h with
     | 0, h   => acc
     | i+1, h =>
-      have : i < m := Nat.ltOfLtOfLe (Nat.ltSuccSelf _) h
-      loop i (Nat.leOfLt this) (acc + u ⟨i, this⟩ * v ⟨i, this⟩)
+      have : i < m := Nat.lt_of_lt_of_le (Nat.lt_succ_self _) h
+      loop i (Nat.le_of_lt this) (acc + u ⟨i, this⟩ * v ⟨i, this⟩)
 
 instance [Zero α] : Zero (Matrix m n α) where
   zero _ _ := 0
diff --git a/tests/lean/run/newfrontend3.lean b/tests/lean/run/newfrontend3.lean
index 61bd2481b0..d2a80068b3 100644
--- a/tests/lean/run/newfrontend3.lean
+++ b/tests/lean/run/newfrontend3.lean
@@ -17,7 +17,7 @@ by {
 
 def g (i j k : Nat) (a : Array Nat) (h₁ : i < k) (h₂ : k < j) (h₃ : j < a.size) : Nat :=
   let vj := a.get ⟨j, h₃⟩;
-  let vi := a.get ⟨i, Nat.ltTrans h₁ (Nat.ltTrans h₂ h₃)⟩;
+  let vi := a.get ⟨i, Nat.lt_trans h₁ (Nat.lt_trans h₂ h₃)⟩;
   vi + vj
 
 set_option pp.all true in
diff --git a/tests/lean/run/noindexAnnotation.lean b/tests/lean/run/noindexAnnotation.lean
index 17a5632827..f6578f118e 100644
--- a/tests/lean/run/noindexAnnotation.lean
+++ b/tests/lean/run/noindexAnnotation.lean
@@ -3,7 +3,7 @@ structure Fin2 (n : Nat) :=
   (isLt : val < n)
 
 protected def Fin2.ofNat {n : Nat} (a : Nat) : Fin2 (Nat.succ n) :=
-  ⟨a % Nat.succ n, Nat.mod_lt _ (Nat.zeroLtSucc _)⟩
+  ⟨a % Nat.succ n, Nat.mod_lt _ (Nat.zero_lt_succ _)⟩
 
 instance : OfNat (Fin2 (no_index (n+1))) i where
   ofNat := Fin2.ofNat i
diff --git a/tests/lean/run/reduce1.lean b/tests/lean/run/reduce1.lean
index 342ac55419..773cab96f2 100644
--- a/tests/lean/run/reduce1.lean
+++ b/tests/lean/run/reduce1.lean
@@ -23,7 +23,7 @@ theorem tst5 : 10000000000000000 < 200000000000000000000 :=
 theorem tst6 : 10000000000000000 < 200000000000000000000 :=
   let h₁ : 10000000000000000 < 10000000000000010 := by nativeDecide
   let h₂ : 10000000000000010 < 200000000000000000000 := by nativeDecide
-  Nat.ltTrans h₁ h₂
+  Nat.lt_trans h₁ h₂
 
 theorem tst7 : 10000000000000000 < 200000000000000000000 :=
   by decide
@@ -31,7 +31,7 @@ theorem tst7 : 10000000000000000 < 200000000000000000000 :=
 theorem tst8 : 10000000000000000 < 200000000000000000000 :=
   let h₁ : 10000000000000000 < 10000000000000010 := by decide
   let h₂ : 10000000000000010 < 200000000000000000000 := by decide
-  Nat.ltTrans h₁ h₂
+  Nat.lt_trans h₁ h₂
 
 theorem tst9 : 10000000000000000 < 200000000000000000000 :=
   by decide
diff --git a/tests/lean/run/reduce3.lean b/tests/lean/run/reduce3.lean
index 8971820bab..edf914f497 100644
--- a/tests/lean/run/reduce3.lean
+++ b/tests/lean/run/reduce3.lean
@@ -20,7 +20,7 @@ theorem tst4 : fact 10 = 3628800 :=
 rfl
 
 theorem tst5 : 100000000001 < 300000000000 :=
-ofDecideEqTrue rfl
+of_decide_eq_true rfl
 
 theorem tst6 : "hello".length = 5 :=
 rfl
diff --git a/tests/lean/run/simp7.lean b/tests/lean/run/simp7.lean
index 9da55f24ad..8e10267936 100644
--- a/tests/lean/run/simp7.lean
+++ b/tests/lean/run/simp7.lean
@@ -10,7 +10,7 @@ def length : List α → Nat
 theorem ex2 (a b c : α) (as : List α) : length (a :: b :: as) > length as := by
   simp [length]
   apply Nat.lt.step
-  apply Nat.ltSuccSelf
+  apply Nat.lt_succ_self
 
 def fact : Nat → Nat
   | 0 => 1
@@ -21,8 +21,8 @@ theorem ex3 : fact x > 0 := by
   | zero => rfl
   | succ x ih =>
     simp [fact]
-    apply Nat.mulPos
-    apply Nat.zeroLtSucc
+    apply Nat.mul_pos
+    apply Nat.zero_lt_succ
     apply ih
 
 def head [Inhabited α] : List α → α
diff --git a/tests/lean/run/subst.lean b/tests/lean/run/subst.lean
index 85179ffdf7..8555968b7e 100644
--- a/tests/lean/run/subst.lean
+++ b/tests/lean/run/subst.lean
@@ -52,7 +52,7 @@ theorem ex12 {α : Type u} {n : Nat}
 Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ hi₂ => h i (hsz₁ ▸ hi₁)
 
 def toArrayLit {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
-List.toArray $ Array.toListLitAux a n hsz n (hsz ▸ Nat.leRefl _) []
+List.toArray $ Array.toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
 
 partial def isEqvAux {α} (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
   if h : i < a.size then
diff --git a/tests/lean/run/synthPending1.lean b/tests/lean/run/synthPending1.lean
index d7231a21c0..90cd25f408 100644
--- a/tests/lean/run/synthPending1.lean
+++ b/tests/lean/run/synthPending1.lean
@@ -1,4 +1,4 @@
-
+--
 
 theorem ex : Not (1 = 2) :=
-ofDecideEqFalse rfl
+of_decide_eq_false rfl
diff --git a/tests/lean/run/trans.lean b/tests/lean/run/trans.lean
index 4514745b72..90913f80fb 100644
--- a/tests/lean/run/trans.lean
+++ b/tests/lean/run/trans.lean
@@ -4,7 +4,7 @@ class Trans (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α
 export Trans (trans)
 
 instance : Trans (α := Nat) (β := Nat) (γ := Nat) (.≤.) (.≤.) (.≤.) where
-  trans := Nat.leTrans
+  trans := Nat.le_trans
 
 instance : Trans (α := Int) (β := Int) (γ := Int) (.≤.) (.≤.) (.≤.) where
   trans := sorry
diff --git a/tests/lean/simpArgTypeMismatch.lean b/tests/lean/simpArgTypeMismatch.lean
index 5a3f8ee731..70d5241db2 100644
--- a/tests/lean/simpArgTypeMismatch.lean
+++ b/tests/lean/simpArgTypeMismatch.lean
@@ -1,3 +1,3 @@
 example (p : Prop) [Decidable p] (hnp : ¬ p) :
     if decide p then 0 = 1 else 1 = 1 := by
-  simp [hnp, decideEqFalse Unit]
+  simp [hnp, decide_eq_false Unit]
diff --git a/tests/lean/simpArgTypeMismatch.lean.expected.out b/tests/lean/simpArgTypeMismatch.lean.expected.out
index dab7b20ba4..bad66bda4b 100644
--- a/tests/lean/simpArgTypeMismatch.lean.expected.out
+++ b/tests/lean/simpArgTypeMismatch.lean.expected.out
@@ -1,5 +1,5 @@
-simpArgTypeMismatch.lean:3:13-3:31: error: application type mismatch
-  decideEqFalse Unit
+simpArgTypeMismatch.lean:3:13-3:33: error: application type mismatch
+  decide_eq_false Unit
 argument
   Unit
 has type
diff --git a/tests/lean/uintCtors.lean b/tests/lean/uintCtors.lean
index b19594c36a..dc4ddf7407 100644
--- a/tests/lean/uintCtors.lean
+++ b/tests/lean/uintCtors.lean
@@ -18,7 +18,7 @@ def UInt64.ofNatCore' (n : Nat) (h : n < UInt64.size) : UInt64 := {
 #eval (3 : UInt32).val
 #eval toString $ { val := { val := 3, isLt := (by decide) } : UInt64 }
 #eval (3 : UInt64).val
-#eval toString $ { val := { val := 3, isLt := (match USize.size, usizeSzEq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
+#eval toString $ { val := { val := 3, isLt := (match USize.size, usize_size_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
 #eval (3 : USize).val
 
 
@@ -30,5 +30,5 @@ def UInt64.ofNatCore' (n : Nat) (h : n < UInt64.size) : UInt64 := {
 #eval (4 : UInt32).val
 #eval toString $ { val := { val := 4, isLt := (by decide) } : UInt64 }
 #eval (4 : UInt64).val
-#eval toString $ { val := { val := 4, isLt := (match USize.size, usizeSzEq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
+#eval toString $ { val := { val := 4, isLt := (match USize.size, usize_size_eq with | _, Or.inl rfl => (by decide) | _, Or.inr rfl => (by decide)) } : USize }
 #eval (4 : USize).val