diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index f549ef27e..57fc5302f 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -169,20 +169,15 @@ local infix ≡ := int.equiv
 
 protected theorem equiv.refl [refl] {p : ℕ × ℕ} : p ≡ p := !add.comm
 
+local attribute int.equiv [reducible]
+
 protected theorem equiv.symm [symm] {p q : ℕ × ℕ} (H : p ≡ q) : q ≡ p :=
-calc
-  pr1 q + pr2 p = pr2 p + pr1 q : by rewrite add.comm
-    ... = pr1 p + pr2 q         : H⁻¹
-    ... = pr2 q + pr1 p         : by rewrite add.comm
+by simp
 
 protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
 add.right_cancel (calc
-   pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by rewrite add.right_comm
-    ... = pr2 p + pr1 q + pr2 r                  : {H1}
-    ... = pr2 p + (pr1 q + pr2 r)                : by rewrite add.assoc
-    ... = pr2 p + (pr2 q + pr1 r)                : {H2}
-    ... = pr2 p + pr2 q + pr1 r                  : by rewrite add.assoc
-    ... = pr2 p + pr1 r + pr2 q                  : by rewrite add.right_comm)
+   pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by simp_nohyps
+                     ... = pr2 p + pr1 r + pr2 q : by simp)
 
 protected theorem equiv_equiv : is_equivalence int.equiv :=
 is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans
@@ -239,7 +234,7 @@ or.elim (int.equiv_cases Hequiv)
            = pr1 p + pr2 q - pr2 q - pr2 p   : by rewrite nat.add_sub_cancel
        ... = pr2 p + pr1 q - pr2 q - pr2 p   : Hequiv
        ... = pr2 p + (pr1 q - pr2 q) - pr2 p : nat.add_sub_assoc Hq
-       ... = pr1 q - pr2 q + pr2 p - pr2 p   : by rewrite add.comm
+       ... = pr1 q - pr2 q + pr2 p - pr2 p   : by simp
        ... = pr1 q - pr2 q                   : by rewrite nat.add_sub_cancel,
     abstr_of_ge Hp ⬝ (H ▸ rfl) ⬝ (abstr_of_ge Hq)⁻¹))
   (and.rec (assume (Hp : pr1 p < pr2 p) (Hq : pr1 q < pr2 q),
@@ -324,20 +319,16 @@ theorem repr_add : Π (a b : ℤ), repr (add a b) ≡ padd (repr a) (repr b)
 
 theorem padd_congr {p p' q q' : ℕ × ℕ} (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' :=
 calc pr1 p + pr1 q + (pr2 p' + pr2 q')
-        = pr1 p + pr2 p' + (pr1 q + pr2 q') : add.comm4
-    ... = pr2 p + pr1 p' + (pr1 q + pr2 q') : {Ha}
-    ... = pr2 p + pr1 p' + (pr2 q + pr1 q') : {Hb}
-    ... = pr2 p + pr2 q + (pr1 p' + pr1 q') : add.comm4
+        = pr1 p + pr2 p' + (pr1 q + pr2 q') : by simp_nohyps
+    ... = pr2 p + pr1 p' + (pr2 q + pr1 q') : by simp
+    ... = pr2 p + pr2 q + (pr1 p' + pr1 q') : by simp_nohyps
 
 theorem padd_comm (p q : ℕ × ℕ) : padd p q = padd q p :=
-calc (pr1 p + pr1 q, pr2 p + pr2 q)
-        = (pr1 q + pr1 p, pr2 p + pr2 q) : by rewrite add.comm
-    ... = (pr1 q + pr1 p, pr2 q + pr2 p) : by rewrite (add.comm (pr2 p) (pr2 q))
+calc (pr1 p + pr1 q, pr2 p + pr2 q) = (pr1 q + pr1 p, pr2 q + pr2 p) : by simp
 
 theorem padd_assoc (p q r : ℕ × ℕ) : padd (padd p q) r = padd p (padd q r) :=
 calc (pr1 p + pr1 q + pr1 r, pr2 p + pr2 q + pr2 r)
-        = (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r)   : by rewrite add.assoc
-    ... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : by rewrite add.assoc
+     = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : by simp
 
 protected theorem add_comm (a b : ℤ) : a + b = b + a :=
 eq_of_repr_equiv_repr (equiv.trans !repr_add
@@ -383,13 +374,7 @@ theorem padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) :=
 show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add_comm ▸ rfl
 
 theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p :=
-calc      pr1 p + pr1 q + pr2 q + pr2 p
-        = pr1 p + (pr1 q + pr2 q) + pr2 p : add.assoc
-    ... = pr1 p + (pr1 q + pr2 q + pr2 p) : add.assoc
-    ... = pr1 p + (pr2 q + pr1 q + pr2 p) : add.comm
-    ... = pr1 p + (pr2 q + pr2 p + pr1 q) : add.right_comm
-    ... = pr1 p + (pr2 p + pr2 q + pr1 q) : add.comm
-    ... = pr2 p + pr2 q + pr1 q + pr1 p   : add.comm
+by unfold [padd, pneg]; simp
 
 protected theorem add_left_inv (a : ℤ) : -a + a = 0 :=
 have H : repr (-a + a) ≡ repr 0, from
@@ -457,31 +442,19 @@ theorem repr_mul : Π (a b : ℤ), repr (a * b) = pmul (repr a) (repr b)
           (succ m * succ n, 0) = (succ m * succ n, 0 * succ n) : by rewrite zero_mul
             ... = (0 + succ m * succ n, 0 * succ n) : nat.zero_add
 
+local attribute left_distrib right_distrib [simp]
 theorem equiv_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
-  (H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm)
-: xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) :=
-nat.add_right_cancel (calc
-            xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn))
-          = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*ym+yb*xm + (xb*xn+yb*yn)) : by rewrite add.comm4
-      ... = xa*xn+ya*yn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*ym+yb*xm)) : by rewrite {xb*ym+yb*xm +_}nat.add_comm
-      ... = xa*xn+yb*xn + (ya*yn+xb*yn) + (xb*xn+xb*ym + (yb*yn+yb*xm)) : by exact !congr_arg2 !add.comm4 !add.comm4
-      ... = ya*xn+xb*xn + (xa*yn+yb*yn) + (xb*yn+xb*xm + (yb*xn+yb*ym)) : by rewrite[-+left_distrib,-+right_distrib]; exact H1 ▸ H2 ▸ rfl
-      ... = ya*xn+xa*yn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : by exact !congr_arg2 !add.comm4 !add.comm4
-      ... = xa*yn+ya*xn + (xb*xn+yb*yn) + (xb*yn+yb*xn + (xb*xm+yb*ym)) : by rewrite {xa*yn + _}nat.add_comm
-      ... = xa*yn+ya*xn + (xb*xn+yb*yn) + (yb*xn+xb*yn + (xb*xm+yb*ym)) : by rewrite {xb*yn + _}nat.add_comm
-      ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xn+yb*yn + (xb*xm+yb*ym)) : by rewrite (!add.comm4)
-      ... = xa*yn+ya*xn + (yb*xn+xb*yn) + (xb*xm+yb*ym + (xb*xn+yb*yn)) : by rewrite {xb*xn+yb*yn + _}nat.add_comm
-      ... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn)) : by rewrite add.comm4)
+  (H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm) : xa*xn+ya*yn+(xb*ym+yb*xm) = xa*yn+ya*xn+(xb*xm+yb*ym) :=
+nat.add_right_cancel (
+calc xa*xn+ya*yn + (xb*ym+yb*xm) + (yb*xn+xb*yn + (xb*xn+yb*yn))
+         = (xa + yb)*xn + (ya + xb)*yn  + (xb*(xn + ym)) + (yb*(yn + xm)) : by simp_nohyps
+     ... = (ya + xb)*xn + (xa + yb)*yn  + (xb*(yn + xm)) + (yb*(xn + ym)) : by simp
+     ... = xa*yn+ya*xn + (xb*xm+yb*ym) + (yb*xn+xb*yn + (xb*xn+yb*yn))    : by simp_nohyps)
 
 theorem pmul_congr {p p' q q' : ℕ × ℕ} : p ≡ p' → q ≡ q' → pmul p q ≡ pmul p' q' := equiv_mul_prep
 
 theorem pmul_comm (p q : ℕ × ℕ) : pmul p q = pmul q p :=
-show (_,_) = (_,_),
-begin
-  congruence,
-    { congruence, repeat rewrite mul.comm },
-    { rewrite add.comm, congruence, repeat rewrite mul.comm }
-end
+by unfold pmul; simp
 
 protected theorem mul_comm (a b : ℤ) : a * b = b * a :=
 eq_of_repr_equiv_repr
@@ -493,13 +466,7 @@ eq_of_repr_equiv_repr
 private theorem pmul_assoc_prep {p1 p2 q1 q2 r1 r2 : ℕ} :
   ((p1*q1+p2*q2)*r1+(p1*q2+p2*q1)*r2, (p1*q1+p2*q2)*r2+(p1*q2+p2*q1)*r1) =
    (p1*(q1*r1+q2*r2)+p2*(q1*r2+q2*r1), p1*(q1*r2+q2*r1)+p2*(q1*r1+q2*r2)) :=
-begin
-   rewrite [+left_distrib, +right_distrib, *mul.assoc],
-   rewrite (add.comm4 (p1 * (q1 * r1)) (p2 * (q2 * r1)) (p1 * (q2 * r2)) (p2 * (q1 * r2))),
-   rewrite (add.comm (p2 * (q2 * r1)) (p2 * (q1 * r2))),
-   rewrite (add.comm4 (p1 * (q1 * r2)) (p2 * (q2 * r2)) (p1 * (q2 * r1)) (p2 * (q1 * r1))),
-   rewrite (add.comm (p2 * (q2 * r2)) (p2 * (q1 * r1)))
-end
+by simp
 
 theorem pmul_assoc (p q r: ℕ × ℕ) : pmul (pmul p q) r = pmul p (pmul q r) := pmul_assoc_prep
 
@@ -522,11 +489,7 @@ int.mul_comm a 1 ▸ int.mul_one a
 private theorem mul_distrib_prep {a1 a2 b1 b2 c1 c2 : ℕ} :
  ((a1+b1)*c1+(a2+b2)*c2,     (a1+b1)*c2+(a2+b2)*c1) =
  (a1*c1+a2*c2+(b1*c1+b2*c2), a1*c2+a2*c1+(b1*c2+b2*c1)) :=
-begin
-  rewrite +right_distrib, congruence,
-    {rewrite add.comm4},
-    {rewrite add.comm4}
-end
+by simp
 
 protected theorem right_distrib (a b c : ℤ) : (a + b) * c = a * c + b * c :=
 eq_of_repr_equiv_repr
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 45bc25180..acabd6664 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -255,8 +255,6 @@ protected definition comm_semiring [reducible] [trans_instance] : comm_semiring
  mul_zero       := nat.mul_zero,
  mul_comm       := nat.mul_comm⦄
 
-attribute succ_eq_add_one [simp]
-
 end nat
 
 section
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 90bae70bf..f3ce9d2e6 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -12,144 +12,86 @@ namespace nat
 
 /- subtraction -/
 
-protected theorem sub_zero (n : ℕ) : n - 0 = n :=
+protected theorem sub_zero [simp] (n : ℕ) : n - 0 = n :=
 rfl
 
-theorem sub_succ (n m : ℕ) : n - succ m = pred (n - m) :=
+theorem sub_succ [simp] (n m : ℕ) : n - succ m = pred (n - m) :=
 rfl
 
-protected theorem zero_sub (n : ℕ) : 0 - n = 0 :=
-nat.induction_on n !nat.sub_zero
-  (take k : nat,
-    assume IH : 0 - k = 0,
-    calc
-      0 - succ k = pred (0 - k) : sub_succ
-             ... = pred 0       : IH
-             ... = 0            : pred_zero)
+protected theorem zero_sub [simp] (n : ℕ) : 0 - n = 0 :=
+nat.induction_on n (by simp) (by simp)
 
-theorem succ_sub_succ (n m : ℕ) : succ n - succ m = n - m :=
+theorem succ_sub_succ [simp] (n m : ℕ) : succ n - succ m = n - m :=
 succ_sub_succ_eq_sub n m
 
-protected theorem sub_self (n : ℕ) : n - n = 0 :=
-nat.induction_on n !nat.sub_zero (take k IH, !succ_sub_succ ⬝ IH)
+protected theorem sub_self [simp] (n : ℕ) : n - n = 0 :=
+nat.induction_on n (by simp) (by simp)
 
-protected theorem add_sub_add_right (n k m : ℕ) : (n + k) - (m + k) = n - m :=
-nat.induction_on k
-  (calc
-    (n + 0) - (m + 0) = n - (m + 0) : {!add_zero}
-                  ... = n - m       : {!add_zero})
-  (take l : nat,
-    assume IH : (n + l) - (m + l) = n - m,
-    calc
-      (n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {!add_succ}
-                              ... = succ (n + l) - succ (m + l) : {!add_succ}
-                              ... = (n + l) - (m + l)           : !succ_sub_succ
-                              ... =  n - m                      : IH)
-protected theorem add_sub_add_left (k n m : ℕ) : (k + n) - (k + m) = n - m :=
-add.comm n k ▸ add.comm m k ▸ nat.add_sub_add_right n k m
+local attribute nat.add_succ [simp]
 
-protected theorem add_sub_cancel (n m : ℕ) : n + m - m = n :=
-nat.induction_on m
-  (begin rewrite add_zero end)
-  (take k : ℕ,
-    assume IH : n + k - k = n,
-    calc
-      n + succ k - succ k = succ (n + k) - succ k : add_succ
-                      ... = n + k - k             : succ_sub_succ
-                      ... = n                     : IH)
+protected theorem add_sub_add_right [simp] (n k m : ℕ) : (n + k) - (m + k) = n - m :=
+nat.induction_on k (by simp) (by simp)
 
-protected theorem add_sub_cancel_left (n m : ℕ) : n + m - n = m :=
-!add.comm ▸ !nat.add_sub_cancel
+protected theorem add_sub_add_left [simp] (k n m : ℕ) : (k + n) - (k + m) = n - m :=
+nat.induction_on k (by simp) (by simp)
 
-protected theorem sub_sub (n m k : ℕ) : n - m - k = n - (m + k) :=
-nat.induction_on k
-  (calc
-    n - m - 0 = n - m        : nat.sub_zero
-          ... =  n - (m + 0) : add_zero)
-  (take l : nat,
-    assume IH : n - m - l = n - (m + l),
-    calc
-      n - m - succ l = pred (n - m - l)   : !sub_succ
-                 ... = pred (n - (m + l)) : IH
-                 ... = n - succ (m + l)   : sub_succ
-                 ... = n - (m + succ l)   : by rewrite add_succ)
+protected theorem add_sub_cancel [simp] (n m : ℕ) : n + m - m = n :=
+nat.induction_on m (by simp) (by simp)
 
-theorem succ_sub_sub_succ (n m k : ℕ) : succ n - m - succ k = n - m - k :=
+protected theorem add_sub_cancel_left [simp] (n m : ℕ) : n + m - n = m :=
+nat.induction_on n (by simp) (by simp)
+
+protected theorem sub_sub [simp] (n m k : ℕ) : n - m - k = n - (m + k) :=
+nat.induction_on k (by simp) (by simp)
+
+theorem succ_sub_sub_succ [simp] (n m k : ℕ) : succ n - m - succ k = n - m - k :=
+by simp
+
+theorem sub_self_add [simp] (n m : ℕ) : n - (n + m) = 0 :=
 calc
-  succ n - m - succ k = succ n - (m + succ k) : nat.sub_sub
-                  ... = succ n - succ (m + k) : add_succ
-                  ... = n - (m + k)           : succ_sub_succ
-                  ... = n - m - k             : nat.sub_sub
-
-theorem sub_self_add (n m : ℕ) : n - (n + m) = 0 :=
-calc
-  n - (n + m) = n - n - m : nat.sub_sub
-          ... = 0 - m     : nat.sub_self
-          ... = 0         : nat.zero_sub
+  n - (n + m) = n - n - m : by topdown_simp
+          ... = 0         : by simp
 
 protected theorem sub.right_comm (m n k : ℕ) : m - n - k = m - k - n :=
-calc
-  m - n - k = m - (n + k) : !nat.sub_sub
-        ... = m - (k + n) : {!add.comm}
-        ... = m - k - n   : !nat.sub_sub⁻¹
+by simp
 
 theorem sub_one (n : ℕ) : n - 1 = pred n :=
 rfl
 
-theorem succ_sub_one (n : ℕ) : succ n - 1 = n :=
+theorem succ_sub_one [simp] (n : ℕ) : succ n - 1 = n :=
 rfl
 
+local attribute nat.succ_mul nat.mul_succ [simp]
+
 /- interaction with multiplication -/
 
 theorem mul_pred_left (n m : ℕ) : pred n * m = n * m - m :=
-nat.induction_on n
-  (calc
-    pred 0 * m = 0 * m     : pred_zero
-           ... = 0         : zero_mul
-           ... = 0 - m     : nat.zero_sub
-           ... = 0 * m - m : zero_mul)
-  (take k : nat,
-    assume IH : pred k * m = k * m - m,
-    calc
-      pred (succ k) * m = k * m          : pred_succ
-                    ... = k * m + m - m  : nat.add_sub_cancel
-                    ... = succ k * m - m : succ_mul)
+nat.induction_on n (by simp) (by simp)
 
 theorem mul_pred_right (n m : ℕ) : n * pred m = n * m - n :=
 calc
-  n * pred m = pred m * n : mul.comm
+  n * pred m = pred m * n : by simp
          ... = m * n - n  : mul_pred_left
-         ... = n * m - n  : mul.comm
+         ... = n * m - n  : by simp
 
-protected theorem mul_sub_right_distrib (n m k : ℕ) : (n - m) * k = n * k - m * k :=
-nat.induction_on m
-  (calc
-    (n - 0) * k = n * k         : nat.sub_zero
-            ... = n * k - 0     : nat.sub_zero
-            ... = n * k - 0 * k : zero_mul)
-  (take l : nat,
-    assume IH : (n - l) * k = n * k - l * k,
-    calc
-      (n - succ l) * k = pred (n - l) * k     : sub_succ
-                   ... = (n - l) * k - k      : mul_pred_left
-                   ... = n * k - l * k - k    : IH
-                   ... = n * k - (l * k + k)  : nat.sub_sub
-                   ... = n * k - (succ l * k) : succ_mul)
+attribute mul_pred_left mul_pred_right [simp]
 
-protected theorem mul_sub_left_distrib (n m k : ℕ) : n * (m - k) = n * m - n * k :=
+protected theorem mul_sub_right_distrib [simp] (n m k : ℕ) : (n - m) * k = n * k - m * k :=
+nat.induction_on m (by simp) (by simp)
+
+protected theorem mul_sub_left_distrib [simp] (n m k : ℕ) : n * (m - k) = n * m - n * k :=
 calc
-  n * (m - k) = (m - k) * n   : !mul.comm
-          ... = m * n - k * n : !nat.mul_sub_right_distrib
-          ... = n * m - k * n : {!mul.comm}
-          ... = n * m - n * k : {!mul.comm}
+  n * (m - k) = (m - k) * n   : by rewrite mul.comm
+          ... = n * m - n * k : by simp
 
 protected theorem mul_self_sub_mul_self_eq (a b : nat) : a * a - b * b = (a + b) * (a - b) :=
 by rewrite [nat.mul_sub_left_distrib, *right_distrib, mul.comm b a, add.comm (a*a) (a*b),
             nat.add_sub_add_left]
 
+local attribute succ_eq_add_one right_distrib left_distrib [simp]
+
 theorem succ_mul_succ_eq (a : nat) : succ a * succ a = a*a + a + a + 1 :=
-calc succ a * succ a = (a+1)*(a+1)     : by rewrite [add_one]
-                ...  = a*a + a + a + 1 : by rewrite [right_distrib, left_distrib, one_mul, mul_one]
+by simp
 
 /- interaction with inequalities -/
 
@@ -213,11 +155,7 @@ exists.intro k
 protected theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) :=
 have l1 : k ≤ m → n + m - k = n + (m - k), from
   sub_induction k m
-    (take m : ℕ,
-      assume H : 0 ≤ m,
-      calc
-        n + m - 0 = n + m       : nat.sub_zero
-              ... = n + (m - 0) : nat.sub_zero)
+    (by simp)
     (take k : ℕ, assume H : succ k ≤ 0, absurd H !not_succ_le_zero)
     (take k m,
       assume IH : k ≤ m → n + m - k = n + (m - k),
@@ -267,10 +205,9 @@ or.elim !le.total
   (assume H2 : k ≤ n,
     have H3 : n - k + l = m - k, from
       calc
-        n - k + l = l + (n - k) : add.comm
+        n - k + l = l + (n - k) : by simp
               ... = l + n - k   : nat.add_sub_assoc H2 l
-              ... = n + l - k   : add.comm
-              ... = m - k       : Hl,
+              ... = m - k       : by simp,
     le.intro H3)
 
 protected theorem sub_le_sub_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k - m ≤ k - n :=
@@ -280,14 +217,7 @@ sub.cases
   (take m' : ℕ,
     assume Hm : m + m' = k,
     have H3 : n ≤ k, from le.trans H (le.intro Hm),
-    have H4 : m' + l + n = k - n + n, from
-      calc
-        m' + l + n = n + (m' + l) : add.comm
-               ... = n + (l + m') : add.comm
-               ... = n + l + m'   : add.assoc
-               ... = m + m'       : Hl
-               ... = k            : Hm
-               ... = k - n + n    : nat.sub_add_cancel H3,
+    have H4 : m' + l + n = k - n + n, by simp,
     le.intro (add.right_cancel H4))
 
 protected theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 :=
@@ -327,8 +257,7 @@ sub.cases
         assume Hkm : k + km = m,
         have H : k + (mn + km) = n, from
           calc
-            k + (mn + km) = k + (km + mn): add.comm
-                      ... = k + km + mn  : add.assoc
+            k + (mn + km) = k + km + mn  : by simp
                       ... = m + mn       : Hkm
                       ... = n            : Hmn,
         have H2 : n - k = mn + km, from nat.sub_eq_of_add_eq H,
@@ -366,13 +295,10 @@ lt_of_succ_le this
 definition dist [reducible] (n m : ℕ) := (n - m) + (m - n)
 
 theorem dist.comm (n m : ℕ) : dist n m = dist m n :=
-!add.comm
+by simp
 
 theorem dist_self (n : ℕ) : dist n n = 0 :=
-calc
-  (n - n) + (n - n) = 0 + (n - n) : nat.sub_self
-                ... = 0 + 0       : nat.sub_self
-                ... = 0           : rfl
+by simp
 
 theorem eq_of_dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m :=
 have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H,
@@ -433,10 +359,9 @@ theorem dist_sub_eq_dist_add_left {n m : ℕ} (H : n ≥ m) (k : ℕ) :
   dist (n - m) k = dist n (k + m) :=
 have H2 : n - m + (k + m) = k + n, from
   calc
-    n - m + (k + m) = n - m + (m + k) : add.comm
-                ... = n - m + m + k   : add.assoc
+    n - m + (k + m) = n - m + m + k   : by simp
                 ... = n + k           : nat.sub_add_cancel H
-                ... = k + n           : add.comm,
+                ... = k + n           : by simp,
 dist_eq_intro H2
 
 theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) :
@@ -444,10 +369,7 @@ theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) :
 dist.comm (k - m) n ▸ dist.comm k (n + m) ▸ dist_sub_eq_dist_add_left H n
 
 theorem dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
-have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
-begin rewrite [add.comm (k - m) (m - n),
-               {n - m + _ + _}add.assoc,
-               {m - k + _}add.left_comm, -add.assoc] end,
+have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)), by simp,
 this ▸ add_le_add !nat.sub_lt_sub_add_sub !nat.sub_lt_sub_add_sub
 
 theorem dist_add_add_le_add_dist_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l :=
diff --git a/library/init/tactic.lean b/library/init/tactic.lean
index 5271777f6..47a9a7626 100644
--- a/library/init/tactic.lean
+++ b/library/init/tactic.lean
@@ -107,8 +107,9 @@ definition with_options_tac (o : expr) (t : tactic) : tactic := builtin
 -- with_options_tac is just a marker for the builtin 'with_attributes' notation
 definition with_attributes_tac (o : expr) (n : identifier_list) (t : tactic) : tactic := builtin
 
-definition simp        : tactic := #tactic with_options [blast.strategy "simp"] blast
-definition simp_nohyps : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
+definition simp         : tactic := #tactic with_options [blast.strategy "simp"] blast
+definition simp_nohyps  : tactic := #tactic with_options [blast.strategy "simp_nohyps"] blast
+definition topdown_simp : tactic := #tactic with_options [blast.strategy "simp", simplify.top_down true] blast
 
 definition cases (h : expr) (ids : opt_identifier_list) : tactic := builtin