diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index 396f0ce967..12c646b255 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -23,7 +23,7 @@ rfl
 protected lemma add_zero (n : ℕ) : n + 0 = n :=
 rfl
 
-lemma add_one_eq_succ (n : ℕ) : n + 1 = succ n :=
+lemma add_one (n : ℕ) : n + 1 = succ n :=
 rfl
 
 lemma succ_eq_add_one (n : ℕ) : succ n = n + 1 :=
@@ -74,7 +74,7 @@ lemma eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ}, n + m = 0 → n = 0
 | (n+1) m := λ h,
   begin
     exfalso,
-    rw [add_one_eq_succ, succ_add] at h,
+    rw [add_one, succ_add] at h,
     apply succ_ne_zero _ h
   end
 
@@ -432,7 +432,7 @@ protected lemma bit0_inj : ∀ {n m : ℕ}, bit0 n = bit0 m → n = m
 | (n+1) 0     h := by contradiction
 | (n+1) (m+1) h :=
   have succ (succ (n + n)) = succ (succ (m + m)),
-  begin unfold bit0 at h, simp [add_one_eq_succ, add_succ, succ_add] at h, exact h end,
+  begin unfold bit0 at h, simp [add_one, add_succ, succ_add] at h, exact h end,
   have n + n = m + m, by repeat {injection this with this},
   have n = m, from bit0_inj this,
   by rw this
@@ -847,10 +847,10 @@ begin
     { simp [zero_mul, zero_le] },
     { have Hlt : y - k < y,
       { apply sub_lt_of_pos_le ; assumption },
-      rw [ ← add_one_eq_succ
+      rw [ ← add_one
          , nat.add_le_add_iff_le_right
          , IH (y - k) Hlt x
-         , add_one_eq_succ
+         , add_one
          , succ_mul, add_le_to_le_sub _ h ]
      } }
 end
diff --git a/tests/lean/run/smt_ematch3.lean b/tests/lean/run/smt_ematch3.lean
index d169e10981..db2bdf69e1 100644
--- a/tests/lean/run/smt_ematch3.lean
+++ b/tests/lean/run/smt_ematch3.lean
@@ -39,7 +39,7 @@ begin
   intros,
   induction v₁,
   {[smt] repeat {ematch_using [app, rev, zero_add, add_zero, add_comm, app_nil_right]}},
-  {[smt] repeat {ematch_using [app, rev, zero_add, add_zero, add_comm, app_assoc, add_one_eq_succ]} }
+  {[smt] repeat {ematch_using [app, rev, zero_add, add_zero, add_comm, app_assoc, add_one]} }
 end
 
 end vector
diff --git a/tests/lean/run/smt_tests3.lean b/tests/lean/run/smt_tests3.lean
index 61ef65195c..791c6b7624 100644
--- a/tests/lean/run/smt_tests3.lean
+++ b/tests/lean/run/smt_tests3.lean
@@ -15,7 +15,7 @@ lemma ex2  (a : nat) : f a ≠ 0 :=
 begin [smt]
   induction a,
   { intros, ematch_using [f] },
-  { repeat {ematch_using [f, nat.add_one_eq_succ, nat.succ_ne_zero]}}
+  { repeat {ematch_using [f, nat.add_one, nat.succ_ne_zero]}}
 end
 
 lemma ex3 (a : nat) : f (a+1) = f a + 1 :=
diff --git a/tests/lean/run/term_app2.lean b/tests/lean/run/term_app2.lean
index 6a8db61e9e..299c0230e2 100644
--- a/tests/lean/run/term_app2.lean
+++ b/tests/lean/run/term_app2.lean
@@ -10,7 +10,7 @@ lemma nat.lt_one_add_of_lt {a b : nat} : a < b → a < 1 + b :=
 begin
   intro h,
   have aux := lt.trans h (nat.lt_succ_self _),
-  rwa [<- nat.add_one_eq_succ, add_comm] at aux
+  rwa [<- nat.add_one, add_comm] at aux
 end
 
 namespace list