diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 10d6fbe31..d771f2e34 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -16,29 +16,31 @@ variable {A : Type}
 
 /- semigroup -/
 
+attribute inv [light 3]
+attribute neg [light 3]
+
 structure semigroup [class] (A : Type) extends has_mul A :=
 (mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))
 
-theorem mul.assoc [semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
+theorem mul.assoc [simp] [semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
 !semigroup.mul_assoc
 
 structure comm_semigroup [class] (A : Type) extends semigroup A :=
 (mul_comm : ∀a b, mul a b = mul b a)
 
-theorem mul.comm [comm_semigroup A] (a b : A) : a * b = b * a :=
+theorem mul.comm [simp] [comm_semigroup A] (a b : A) : a * b = b * a :=
 !comm_semigroup.mul_comm
 
-theorem mul.left_comm [comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
+theorem mul.left_comm [simp] [comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
 binary.left_comm (@mul.comm A _) (@mul.assoc A _) a b c
 
 theorem mul.right_comm [comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b :=
-binary.right_comm (@mul.comm A _) (@mul.assoc A _) a b c
+by simp
 
 structure left_cancel_semigroup [class] (A : Type) extends semigroup A :=
 (mul_left_cancel : ∀a b c, mul a b = mul a c → b = c)
 
-theorem mul.left_cancel [left_cancel_semigroup A] {a b c : A} :
-  a * b = a * c → b = c :=
+theorem mul.left_cancel [left_cancel_semigroup A] {a b c : A} : a * b = a * c → b = c :=
 !left_cancel_semigroup.mul_left_cancel
 
 abbreviation eq_of_mul_eq_mul_left' := @mul.left_cancel
@@ -46,8 +48,7 @@ abbreviation eq_of_mul_eq_mul_left' := @mul.left_cancel
 structure right_cancel_semigroup [class] (A : Type) extends semigroup A :=
 (mul_right_cancel : ∀a b c, mul a b = mul c b → a = c)
 
-theorem mul.right_cancel [right_cancel_semigroup A] {a b c : A} :
-  a * b = c * b → a = c :=
+theorem mul.right_cancel [right_cancel_semigroup A] {a b c : A} : a * b = c * b → a = c :=
 !right_cancel_semigroup.mul_right_cancel
 
 abbreviation eq_of_mul_eq_mul_right' := @mul.right_cancel
@@ -57,27 +58,25 @@ abbreviation eq_of_mul_eq_mul_right' := @mul.right_cancel
 structure add_semigroup [class] (A : Type) extends has_add A :=
 (add_assoc : ∀a b c, add (add a b) c = add a (add b c))
 
-theorem add.assoc [add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
+theorem add.assoc [simp] [add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
 !add_semigroup.add_assoc
 
 structure add_comm_semigroup [class] (A : Type) extends add_semigroup A :=
 (add_comm : ∀a b, add a b = add b a)
 
-theorem add.comm [add_comm_semigroup A] (a b : A) : a + b = b + a :=
+theorem add.comm [simp] [add_comm_semigroup A] (a b : A) : a + b = b + a :=
 !add_comm_semigroup.add_comm
 
-theorem add.left_comm [add_comm_semigroup A] (a b c : A) :
-  a + (b + c) = b + (a + c) :=
+theorem add.left_comm [simp] [add_comm_semigroup A] (a b c : A) : a + (b + c) = b + (a + c) :=
 binary.left_comm (@add.comm A _) (@add.assoc A _) a b c
 
 theorem add.right_comm [add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b :=
-binary.right_comm (@add.comm A _) (@add.assoc A _) a b c
+by simp
 
 structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
 (add_left_cancel : ∀a b c, add a b = add a c → b = c)
 
-theorem add.left_cancel [add_left_cancel_semigroup A] {a b c : A} :
-  a + b = a + c → b = c :=
+theorem add.left_cancel [add_left_cancel_semigroup A] {a b c : A} : a + b = a + c → b = c :=
 !add_left_cancel_semigroup.add_left_cancel
 
 abbreviation eq_of_add_eq_add_left := @add.left_cancel
@@ -85,8 +84,7 @@ abbreviation eq_of_add_eq_add_left := @add.left_cancel
 structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
 (add_right_cancel : ∀a b c, add a b = add c b → a = c)
 
-theorem add.right_cancel [add_right_cancel_semigroup A] {a b c : A} :
-  a + b = c + b → a = c :=
+theorem add.right_cancel [add_right_cancel_semigroup A] {a b c : A} : a + b = c + b → a = c :=
 !add_right_cancel_semigroup.add_right_cancel
 
 abbreviation eq_of_add_eq_add_right := @add.right_cancel
@@ -96,9 +94,9 @@ abbreviation eq_of_add_eq_add_right := @add.right_cancel
 structure monoid [class] (A : Type) extends semigroup A, has_one A :=
 (one_mul : ∀a, mul one a = a) (mul_one : ∀a, mul a one = a)
 
-theorem one_mul [monoid A] (a : A) : 1 * a = a := !monoid.one_mul
+theorem one_mul [simp] [monoid A] (a : A) : 1 * a = a := !monoid.one_mul
 
-theorem mul_one [monoid A] (a : A) : a * 1 = a := !monoid.mul_one
+theorem mul_one [simp] [monoid A] (a : A) : a * 1 = a := !monoid.mul_one
 
 structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
 
@@ -107,9 +105,9 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
 structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
 (zero_add : ∀a, add zero a = a) (add_zero : ∀a, add a zero = a)
 
-theorem zero_add [add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add
+theorem zero_add [simp] [add_monoid A] (a : A) : 0 + a = a := !add_monoid.zero_add
 
-theorem add_zero [add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
+theorem add_zero [simp] [add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
 
 structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
 
@@ -132,10 +130,10 @@ section add_comm_monoid
   variables [add_comm_monoid A]
 
   theorem add_comm_three  (a b c : A) : a + b + c = c + b + a :=
-    by rewrite [{a + _}add.comm, {_ + c}add.comm, -*add.assoc]
+  by simp
 
   theorem add.comm4 : ∀ (n m k l : A), n + m + (k + l) = n + k + (m + l) :=
-  comm4 add.comm add.assoc
+  by simp
 end add_comm_monoid
 
 /- group -/
@@ -148,35 +146,39 @@ structure group [class] (A : Type) extends monoid A, has_inv A :=
 section group
   variable [group A]
 
-  theorem mul.left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
+  theorem mul.left_inv [simp] (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
 
-  theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
+  theorem inv_mul_cancel_left [simp] (a b : A) : a⁻¹ * (a * b) = b :=
   by rewrite [-mul.assoc, mul.left_inv, one_mul]
 
-  theorem inv_mul_cancel_right (a b : A) : a * b⁻¹ * b = a :=
-  by rewrite [mul.assoc, mul.left_inv, mul_one]
+  theorem inv_mul_cancel_right [simp] (a b : A) : a * b⁻¹ * b = a :=
+  by simp
 
   theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b :=
-  by rewrite [-mul_one a⁻¹, -H, inv_mul_cancel_left]
+  calc a⁻¹ = a⁻¹ * 1       : by simp
+       ... = a⁻¹ * (a * b) : by simp
+       ... = b             : by simp_nohyps
 
-  theorem one_inv : 1⁻¹ = (1 : A) := inv_eq_of_mul_eq_one (one_mul 1)
+  theorem one_inv [simp] : 1⁻¹ = (1 : A) :=
+  inv_eq_of_mul_eq_one (one_mul 1)
 
-  theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a)
+  theorem inv_inv [simp] (a : A) : (a⁻¹)⁻¹ = a :=
+  inv_eq_of_mul_eq_one (mul.left_inv a)
 
   theorem inv.inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
   by rewrite [-inv_inv a, H, inv_inv b]
 
   theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
-  iff.intro (assume H, inv.inj H) (assume H, congr_arg _ H)
+  iff.intro (assume H, inv.inj H) (by simp)
 
   theorem inv_eq_one_iff_eq_one (a : A) : a⁻¹ = 1 ↔ a = 1 :=
   one_inv ▸ inv_eq_inv_iff_eq a 1
 
   theorem eq_one_of_inv_eq_one (a : A) : a⁻¹ = 1 → a = 1 :=
-    iff.mp !inv_eq_one_iff_eq_one
+  iff.mp !inv_eq_one_iff_eq_one
 
   theorem eq_inv_of_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ :=
-  by rewrite [H, inv_inv]
+  by simp
 
   theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
   iff.intro !eq_inv_of_eq_inv !eq_inv_of_eq_inv
@@ -184,59 +186,58 @@ section group
   theorem eq_inv_of_mul_eq_one {a b : A} (H : a * b = 1) : a = b⁻¹ :=
   begin apply eq_inv_of_eq_inv, symmetry, exact inv_eq_of_mul_eq_one H end
 
-  theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
+  theorem mul.right_inv [simp] (a : A) : a * a⁻¹ = 1 :=
   calc
-    a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv
+    a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : by simp
         ... = 1             : mul.left_inv
 
-  theorem mul_inv_cancel_left (a b : A) : a * (a⁻¹ * b) = b :=
+  theorem mul_inv_cancel_left [simp] (a b : A) : a * (a⁻¹ * b) = b :=
   calc
     a * (a⁻¹ * b) = a * a⁻¹ * b : by rewrite mul.assoc
-      ... = 1 * b               : mul.right_inv
-      ... = b                   : one_mul
+      ... = 1 * b               : by simp
+      ... = b                   : by simp
 
-  theorem mul_inv_cancel_right (a b : A) : a * b * b⁻¹ = a :=
+  theorem mul_inv_cancel_right [simp] (a b : A) : a * b * b⁻¹ = a :=
   calc
-    a * b * b⁻¹ = a * (b * b⁻¹) : mul.assoc
-      ... = a * 1 : mul.right_inv
-      ... = a : mul_one
+    a * b * b⁻¹ = a * (b * b⁻¹) : by simp
+      ... = a * 1               : by simp
+      ... = a                   : by simp
 
-  theorem mul_inv (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
+  theorem mul_inv [simp] (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
   inv_eq_of_mul_eq_one
     (calc
-      a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : mul.assoc
-        ... = a * a⁻¹                             : mul_inv_cancel_left
-        ... = 1                                   : mul.right_inv)
+      a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : by simp
+        ... = a * a⁻¹                             : by simp
+        ... = 1                                   : by simp)
 
   theorem eq_of_mul_inv_eq_one {a b : A} (H : a * b⁻¹ = 1) : a = b :=
   calc
-    a = a * b⁻¹ * b : by rewrite inv_mul_cancel_right
-      ... = 1 * b   : H
-      ... = b       : one_mul
+    a = a * b⁻¹ * b : by simp_nohyps
+      ... = b       : by simp
 
   theorem eq_mul_inv_of_mul_eq {a b c : A} (H : a * c = b) : a = b * c⁻¹ :=
-  by rewrite [-H, mul_inv_cancel_right]
+  by simp
 
   theorem eq_inv_mul_of_mul_eq {a b c : A} (H : b * a = c) : a = b⁻¹ * c :=
-  by rewrite [-H, inv_mul_cancel_left]
+  by simp
 
   theorem inv_mul_eq_of_eq_mul {a b c : A} (H : b = a * c) : a⁻¹ * b = c :=
-  by rewrite [H, inv_mul_cancel_left]
+  by simp
 
   theorem mul_inv_eq_of_eq_mul {a b c : A} (H : a = c * b) : a * b⁻¹ = c :=
-  by rewrite [H, mul_inv_cancel_right]
+  by simp
 
   theorem eq_mul_of_mul_inv_eq {a b c : A} (H : a * c⁻¹ = b) : a = b * c :=
-  !inv_inv ▸ (eq_mul_inv_of_mul_eq H)
+  by simp
 
   theorem eq_mul_of_inv_mul_eq {a b c : A} (H : b⁻¹ * a = c) : a = b * c :=
-  !inv_inv ▸ (eq_inv_mul_of_mul_eq H)
+  by simp
 
   theorem mul_eq_of_eq_inv_mul {a b c : A} (H : b = a⁻¹ * c) : a * b = c :=
-  !inv_inv ▸ (inv_mul_eq_of_eq_mul H)
+  by simp
 
   theorem mul_eq_of_eq_mul_inv {a b c : A} (H : a = c * b⁻¹) : a * b = c :=
-  !inv_inv ▸ (mul_inv_eq_of_eq_mul H)
+  by simp
 
   theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
   iff.intro eq_inv_mul_of_mul_eq mul_eq_of_eq_inv_mul
@@ -262,47 +263,45 @@ section group
   local infixl ` ~ ` := is_conjugate
   local infixr ` ∘c `:55 := conj_by
 
-  lemma conj_compose (f g a : A) : f ∘c g ∘c a = f*g ∘c a :=
-      calc f ∘c g ∘c a = f * (g * a * g⁻¹) * f⁻¹ : rfl
-      ... = f * (g * a) * g⁻¹ * f⁻¹ : mul.assoc
-      ... = f * g * a * g⁻¹ * f⁻¹ : mul.assoc
-      ... = f * g * a * (g⁻¹ * f⁻¹) : mul.assoc
-      ... = f * g * a * (f * g)⁻¹ : mul_inv
-  lemma conj_id (a : A) : 1 ∘c a = a :=
-      calc 1 * a * 1⁻¹ = a * 1⁻¹ : one_mul
-      ... = a * 1 : one_inv
-      ... = a : mul_one
-  lemma conj_one (g : A) : g ∘c 1 = 1 :=
-      calc g * 1 * g⁻¹ = g * g⁻¹ : mul_one
-      ... = 1 : mul.right_inv
-  lemma conj_inv_cancel (g : A) : ∀ a, g⁻¹ ∘c g ∘c a = a :=
-      assume a, calc
-      g⁻¹ ∘c g ∘c a = g⁻¹*g ∘c a : conj_compose
-      ... = 1 ∘c a : mul.left_inv
-      ... = a : conj_id
+  lemma conj_compose [simp] (f g a : A) : f ∘c g ∘c a = f*g ∘c a :=
+  calc f ∘c g ∘c a = f * (g * a * g⁻¹) * f⁻¹ : rfl
+               ... = f * g * a * (f * g)⁻¹   : by simp
 
-  lemma conj_inv (g : A) : ∀ a, (g ∘c a)⁻¹ = g ∘c a⁻¹ :=
-    take a, calc
-    (g * a * g⁻¹)⁻¹ = g⁻¹⁻¹ * (g * a)⁻¹   : mul_inv
-                ... = g⁻¹⁻¹ * (a⁻¹ * g⁻¹) : mul_inv
-                ... = g⁻¹⁻¹ * a⁻¹ * g⁻¹   : mul.assoc
-                ... = g * a⁻¹ * g⁻¹       : inv_inv
+  lemma conj_id [simp] (a : A) : 1 ∘c a = a :=
+  calc 1 * a * 1⁻¹ = a * 1⁻¹ : by simp
+               ... = a       : by simp
+
+  lemma conj_one [simp] (g : A) : g ∘c 1 = 1 :=
+  calc g * 1 * g⁻¹ = g * g⁻¹ : by simp
+               ... = 1       : by simp
+
+  lemma conj_inv_cancel [simp] (g : A) : ∀ a, g⁻¹ ∘c g ∘c a = a :=
+  assume a, calc
+      g⁻¹ ∘c g ∘c a = g⁻¹*g ∘c a : by simp
+                ... = a          : by simp
+
+  lemma conj_inv [simp] (g : A) : ∀ a, (g ∘c a)⁻¹ = g ∘c a⁻¹ :=
+  take a, calc
+    (g * a * g⁻¹)⁻¹ = g⁻¹⁻¹ * (g * a)⁻¹   : by simp
+                ... = g⁻¹⁻¹ * (a⁻¹ * g⁻¹) : by simp
+                ... = g⁻¹⁻¹ * a⁻¹ * g⁻¹   : by simp
+                ... = g * a⁻¹ * g⁻¹       : by simp
 
   lemma is_conj.refl (a : A) : a ~ a := exists.intro 1 (conj_id a)
 
   lemma is_conj.symm (a b : A) : a ~ b → b ~ a :=
-      assume Pab, obtain x (Pconj : x ∘c b = a), from Pab,
-      assert Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a,   begin congruence, assumption end,
-      exists.intro x⁻¹ (eq.symm (conj_inv_cancel x b ▸ Pxinv))
+  assume Pab, obtain x (Pconj : x ∘c b = a), from Pab,
+  assert Pxinv : x⁻¹ ∘c x ∘c b = x⁻¹ ∘c a,   by simp,
+  exists.intro x⁻¹ (by simp)
 
   lemma is_conj.trans (a b c : A) : a ~ b → b ~ c → a ~ c :=
-      assume Pab, assume Pbc,
-      obtain x (Px : x ∘c b = a), from Pab,
-      obtain y (Py : y ∘c c = b), from Pbc,
-      exists.intro (x*y) (calc
-      x*y ∘c c = x ∘c y ∘c c : conj_compose
-      ... = x ∘c b : Py
-      ... = a : Px)
+  assume Pab, assume Pbc,
+  obtain x (Px : x ∘c b = a), from Pab,
+  obtain y (Py : y ∘c c = b), from Pbc,
+  exists.intro (x*y) (calc
+      x*y ∘c c = x ∘c y ∘c c : by simp
+           ... = x ∘c b      : Py
+           ... = a           : Px)
 end group
 
 definition group.to_left_cancel_semigroup [trans_instance] [reducible] [s : group A] :
@@ -331,88 +330,87 @@ section add_group
   variables [s : add_group A]
   include s
 
-  theorem add.left_inv (a : A) : -a + a = 0 := !add_group.add_left_inv
+  theorem add.left_inv [simp] (a : A) : -a + a = 0 := !add_group.add_left_inv
 
-  theorem neg_add_cancel_left (a b : A) : -a + (a + b) = b :=
-  by rewrite [-add.assoc, add.left_inv, zero_add]
+  theorem neg_add_cancel_left [simp] (a b : A) : -a + (a + b) = b :=
+  calc -a + (a + b) = (-a + a) + b : by rewrite add.assoc
+               ...  = b            : by simp
 
-  theorem neg_add_cancel_right (a b : A) : a + -b + b = a :=
-  by rewrite [add.assoc, add.left_inv, add_zero]
+  theorem neg_add_cancel_right [simp] (a b : A) : a + -b + b = a :=
+  by simp
 
   theorem neg_eq_of_add_eq_zero {a b : A} (H : a + b = 0) : -a = b :=
   by rewrite [-add_zero, -H, neg_add_cancel_left]
 
-  theorem neg_zero : -0 = (0 : A) := neg_eq_of_add_eq_zero (zero_add 0)
+  theorem neg_zero [simp] : -0 = (0 : A) := neg_eq_of_add_eq_zero (zero_add 0)
 
-  theorem neg_neg (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a)
+  theorem neg_neg [simp] (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a)
 
   theorem eq_neg_of_add_eq_zero {a b : A} (H : a + b = 0) : a = -b :=
   by rewrite [-neg_eq_of_add_eq_zero H, neg_neg]
 
   theorem neg.inj {a b : A} (H : -a = -b) : a = b :=
   calc
-    a = -(-a) : neg_neg
-      ... = b : neg_eq_of_add_eq_zero (H⁻¹ ▸ (add.left_inv _))
+    a = -(-a) : by simp_nohyps
+      ... = b : begin apply neg_eq_of_add_eq_zero, simp end
 
   theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
-  iff.intro (assume H, neg.inj H) (assume H, congr_arg _ H)
+  iff.intro (assume H, neg.inj H) (by simp)
 
   theorem eq_of_neg_eq_neg {a b : A} : -a = -b → a = b :=
-    iff.mp !neg_eq_neg_iff_eq
+  iff.mp !neg_eq_neg_iff_eq
 
   theorem neg_eq_zero_iff_eq_zero (a : A) : -a = 0 ↔ a = 0 :=
   neg_zero ▸ !neg_eq_neg_iff_eq
 
   theorem eq_zero_of_neg_eq_zero {a : A} : -a = 0 → a = 0 :=
-    iff.mp !neg_eq_zero_iff_eq_zero
+  iff.mp !neg_eq_zero_iff_eq_zero
 
   theorem eq_neg_of_eq_neg {a b : A} (H : a = -b) : b = -a :=
-  H⁻¹ ▸ (neg_neg b)⁻¹
+  by simp
 
   theorem eq_neg_iff_eq_neg (a b : A) : a = -b ↔ b = -a :=
   iff.intro !eq_neg_of_eq_neg !eq_neg_of_eq_neg
 
-  theorem add.right_inv (a : A) : a + -a = 0 :=
+  theorem add.right_inv [simp] (a : A) : a + -a = 0 :=
   calc
-    a + -a = -(-a) + -a : neg_neg
-      ... = 0 : add.left_inv
+    a + -a = -(-a) + -a : by simp
+      ... = 0           : add.left_inv
 
-  theorem add_neg_cancel_left (a b : A) : a + (-a + b) = b :=
-  by rewrite [-add.assoc, add.right_inv, zero_add]
+  theorem add_neg_cancel_left [simp] (a b : A) : a + (-a + b) = b :=
+  calc a + (-a + b) = (a + -a) + b : by rewrite add.assoc
+             ...    = b            : by simp
 
-  theorem add_neg_cancel_right (a b : A) : a + b + -b = a :=
-  by rewrite [add.assoc, add.right_inv, add_zero]
+  theorem add_neg_cancel_right [simp] (a b : A) : a + b + -b = a :=
+  by simp
 
-  theorem neg_add_rev (a b : A) : -(a + b) = -b + -a :=
-  neg_eq_of_add_eq_zero
-    begin
-      rewrite [add.assoc, add_neg_cancel_left, add.right_inv]
-    end
+  theorem neg_add_rev [simp] (a b : A) : -(a + b) = -b + -a :=
+  neg_eq_of_add_eq_zero (by simp)
 
   -- TODO: delete these in favor of sub rules?
   theorem eq_add_neg_of_add_eq {a b c : A} (H : a + c = b) : a = b + -c :=
-  H ▸ !add_neg_cancel_right⁻¹
+  by simp
 
   theorem eq_neg_add_of_add_eq {a b c : A} (H : b + a = c) : a = -b + c :=
-  H ▸ !neg_add_cancel_left⁻¹
+  by simp
 
   theorem neg_add_eq_of_eq_add {a b c : A} (H : b = a + c) : -a + b = c :=
-  H⁻¹ ▸ !neg_add_cancel_left
+  by simp
 
   theorem add_neg_eq_of_eq_add {a b c : A} (H : a = c + b) : a + -b = c :=
-  H⁻¹ ▸ !add_neg_cancel_right
+  by simp
 
   theorem eq_add_of_add_neg_eq {a b c : A} (H : a + -c = b) : a = b + c :=
-  !neg_neg ▸ (eq_add_neg_of_add_eq H)
+  by simp
 
   theorem eq_add_of_neg_add_eq {a b c : A} (H : -b + a = c) : a = b + c :=
-  !neg_neg ▸ (eq_neg_add_of_add_eq H)
+  by simp
 
   theorem add_eq_of_eq_neg_add {a b c : A} (H : b = -a + c) : a + b = c :=
-  !neg_neg ▸ (neg_add_eq_of_eq_add H)
+  by simp
 
   theorem add_eq_of_eq_add_neg {a b c : A} (H : a = c + -b) : a + b = c :=
-  !neg_neg ▸ (add_neg_eq_of_eq_add H)
+  by simp
 
   theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
   iff.intro eq_neg_add_of_add_eq add_eq_of_eq_neg_add
@@ -421,14 +419,14 @@ section add_group
   iff.intro eq_add_neg_of_add_eq add_eq_of_eq_add_neg
 
   theorem add_left_cancel {a b c : A} (H : a + b = a + c) : b = c :=
-  calc b = -a + (a + b) : !neg_add_cancel_left⁻¹
-     ... = -a + (a + c) : H
-     ... = c : neg_add_cancel_left
+  calc b = -a + (a + b) : by simp_nohyps
+     ... = -a + (a + c) : by simp
+     ... = c            : by simp
 
   theorem add_right_cancel {a b c : A} (H : a + b = c + b) : a = c :=
-  calc a = (a + b) + -b : !add_neg_cancel_right⁻¹
-     ... = (c + b) + -b : H
-     ... = c : add_neg_cancel_right
+  calc a = (a + b) + -b : by simp_nohyps
+     ... = (c + b) + -b : by simp
+     ... = c            : by simp
 
   definition add_group.to_left_cancel_semigroup [trans_instance] [reducible] :
     add_left_cancel_semigroup A :=
@@ -441,7 +439,7 @@ section add_group
     add_right_cancel := @add_right_cancel A s ⦄
 
   theorem add_neg_eq_neg_add_rev {a b : A} : a + -b = -(b + -a) :=
-  by rewrite [neg_add_rev, neg_neg]
+  by simp
 
   /- sub -/
 
@@ -451,7 +449,7 @@ section add_group
   definition add_group_has_sub [reducible] [instance] : has_sub A :=
   has_sub.mk algebra.sub
 
-  theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl
+  theorem sub_eq_add_neg [simp] (a b : A) : a - b = a + -b := rfl
 
   theorem sub_self (a : A) : a - a = 0 := !add.right_inv
 
@@ -461,9 +459,9 @@ section add_group
 
   theorem eq_of_sub_eq_zero {a b : A} (H : a - b = 0) : a = b :=
   calc
-    a = (a - b) + b : !sub_add_cancel⁻¹
-      ... = 0 + b : H
-      ... = b : zero_add
+    a = (a - b) + b : by simp_nohyps
+      ... = 0 + b   : H
+      ... = b       : by simp
 
   theorem eq_iff_sub_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
   iff.intro (assume H, H ▸ !sub_self) (assume H, eq_of_sub_eq_zero H)
@@ -471,24 +469,24 @@ section add_group
   theorem zero_sub (a : A) : 0 - a = -a := !zero_add
 
   theorem sub_zero (a : A) : a - 0 = a :=
-  by rewrite [sub_eq_add_neg, neg_zero, add_zero]
+  by simp
 
   theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b :=
-  by change a + -(-b) = a + b; rewrite neg_neg
+  by simp
 
   theorem neg_sub (a b : A) : -(a - b) = b - a :=
   neg_eq_of_add_eq_zero
     (calc
-      a - b + (b - a) = a - b + b - a : by krewrite -add.assoc
-        ... = a - a                   : sub_add_cancel
-        ... = 0                       : sub_self)
+      a - b + (b - a) = a - b + b - a : by simp
+        ... = a - a                   : by simp
+        ... = 0                       : by simp)
 
   theorem add_sub (a b c : A) : a + (b - c) = a + b - c := !add.assoc⁻¹
 
   theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b :=
   calc
-    a - (b + c) = a + (-c - b) : by rewrite [sub_eq_add_neg, neg_add_rev]
-            ... = a - c - b    : by krewrite -add.assoc
+    a - (b + c) = a + (-c - b) : by simp
+            ... = a - c - b    : by simp
 
   theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
   iff.intro (assume H, eq_add_of_add_neg_eq H) (assume H, add_neg_eq_of_eq_add H)
@@ -503,16 +501,16 @@ section add_group
       ... ↔ c = d       : iff.symm (eq_iff_sub_eq_zero c d)
 
   theorem eq_sub_of_add_eq {a b c : A} (H : a + c = b) : a = b - c :=
-  !eq_add_neg_of_add_eq H
+  by simp
 
   theorem sub_eq_of_eq_add {a b c : A} (H : a = c + b) : a - b = c :=
-  !add_neg_eq_of_eq_add H
+  by simp
 
   theorem eq_add_of_sub_eq {a b c : A} (H : a - c = b) : a = b + c :=
-  eq_add_of_add_neg_eq H
+  by simp
 
   theorem add_eq_of_eq_sub {a b c : A} (H : a = c - b) : a + b = c :=
-  add_eq_of_eq_add_neg H
+  by simp
 
 end add_group
 
@@ -523,43 +521,47 @@ section add_comm_group
   include s
 
   theorem sub_add_eq_sub_sub (a b c : A) : a - (b + c) = a - b - c :=
-  !add.comm ▸ !sub_add_eq_sub_sub_swap
+  by simp
 
-  theorem neg_add_eq_sub (a b : A) : -a + b = b - a := !add.comm
+  theorem neg_add_eq_sub (a b : A) : -a + b = b - a :=
+  by simp
 
-  theorem neg_add (a b : A) : -(a + b) = -a + -b := add.comm (-b) (-a) ▸ neg_add_rev a b
+  theorem neg_add (a b : A) : -(a + b) = -a + -b :=
+  by simp
 
-  theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b := !add.right_comm
+  theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b :=
+  by simp
 
   theorem sub_sub (a b c : A) : a - b - c = a - (b + c) :=
-  by rewrite [▸ a + -b + -c = _, add.assoc, -neg_add]
+  by simp
 
   theorem add_sub_add_left_eq_sub (a b c : A) : (c + a) - (c + b) = a - b :=
-  by rewrite [sub_add_eq_sub_sub, (add.comm c a), add_sub_cancel]
+  by simp
 
   theorem eq_sub_of_add_eq' {a b c : A} (H : c + a = b) : a = b - c :=
-  !eq_sub_of_add_eq (!add.comm ▸ H)
+  by simp
 
   theorem sub_eq_of_eq_add' {a b c : A} (H : a = b + c) : a - b = c :=
-  !sub_eq_of_eq_add (!add.comm ▸ H)
+  by simp
 
   theorem eq_add_of_sub_eq' {a b c : A} (H : a - b = c) : a = b + c :=
-  !add.comm ▸ eq_add_of_sub_eq H
+  by simp
 
   theorem add_eq_of_eq_sub' {a b c : A} (H : b = c - a) : a + b = c :=
-  !add.comm ▸ add_eq_of_eq_sub H
+  by simp
 
   theorem sub_sub_self (a b : A) : a - (a - b) = b :=
-  by rewrite [sub_eq_add_neg, neg_sub, add.comm, sub_add_cancel]
+  by simp
 
   theorem add_sub_comm (a b c d : A) : a + b - (c + d) = (a - c) + (b - d) :=
-    by rewrite [sub_add_eq_sub_sub, -sub_add_eq_add_sub a c b, add_sub]
+  by simp
 
   theorem sub_eq_sub_add_sub (a b c : A) : a - b = c - b + (a - c) :=
-    by rewrite [add_sub, sub_add_cancel] ⬝ !add.comm
+  by simp
 
   theorem neg_neg_sub_neg (a b : A) : - (-a - -b) = a - b :=
-    by rewrite [neg_sub, sub_neg_eq_add, neg_add_eq_sub]
+  by simp
+
 end add_comm_group
 
 definition group_of_add_group (A : Type) [G : add_group A] : group A :=
@@ -577,105 +579,99 @@ reveal add.assoc
 
 definition add1 [has_add A] [has_one A] (a : A) : A := add a one
 
+local attribute add1 bit0 bit1 [reducible]
+
 theorem add_comm_four [add_comm_semigroup A] (a b : A) : a + a + (b + b) = (a + b) + (a + b) :=
-  by rewrite [-add.assoc at {1}, add.comm, {a + b}add.comm at {1}, *add.assoc]
+by simp
 
 theorem add_comm_middle [add_comm_semigroup A] (a b c : A) : a + b + c = a + c + b :=
-  by rewrite [add.assoc, add.comm b, -add.assoc]
+by simp
 
 theorem bit0_add_bit0 [add_comm_semigroup A] (a b : A) : bit0 a + bit0 b = bit0 (a + b) :=
-  !add_comm_four
+by simp
 
 theorem bit0_add_bit0_helper [add_comm_semigroup A] (a b t : A) (H : a + b = t) :
         bit0 a + bit0 b = bit0 t :=
-  by rewrite -H; apply bit0_add_bit0
+by rewrite -H; simp
 
 theorem bit1_add_bit0 [add_comm_semigroup A] [has_one A] (a b : A) :
         bit1 a + bit0 b = bit1 (a + b) :=
-  begin
-    rewrite [↑bit0, ↑bit1, add_comm_middle], congruence, apply add_comm_four
-  end
+by simp
 
 theorem bit1_add_bit0_helper [add_comm_semigroup A] [has_one A] (a b t : A)
         (H : a + b = t) : bit1 a + bit0 b = bit1 t :=
-  by rewrite -H; apply bit1_add_bit0
+by rewrite -H; simp
 
 theorem bit0_add_bit1 [add_comm_semigroup A] [has_one A] (a b : A) :
         bit0 a + bit1 b = bit1 (a + b) :=
-  by rewrite [{bit0 a + bit1 b}add.comm,{a + b}add.comm]; exact bit1_add_bit0 b a
+by simp
 
 theorem bit0_add_bit1_helper [add_comm_semigroup A] [has_one A] (a b t : A)
         (H : a + b = t) : bit0 a + bit1 b = bit1 t :=
-  by rewrite -H; apply bit0_add_bit1
+by rewrite -H; simp
 
 theorem bit1_add_bit1 [add_comm_semigroup A] [has_one A] (a b : A) :
         bit1 a + bit1 b = bit0 (add1 (a + b)) :=
-  begin
-    rewrite ↑[bit0, bit1, add1],
-    rewrite [*add.assoc, {_ + (b + 1)}add.comm, {_ + (b + 1 + _)}add.comm,
-      {_ + (b + 1 + _ + _)}add.comm, *add.assoc, {1 + a}add.comm, -{b + (a + 1)}add.assoc,
-      {b + a}add.comm, *add.assoc]
-  end
+by simp
 
 theorem bit1_add_bit1_helper [add_comm_semigroup A] [has_one A] (a b t s: A)
         (H : (a + b) = t) (H2 : add1 t = s) : bit1 a + bit1 b = bit0 s :=
-  begin rewrite [-H2, -H], apply bit1_add_bit1 end
+calc bit1 a + bit1 b = bit0 (add1 (a + b)) : by simp_nohyps
+           ...       = bit0 (add1 t)       : by simp
+           ...       = bit0 s              : by simp
 
-theorem bin_add_zero [add_monoid A] (a : A) : a + zero = a := !add_zero
+theorem bin_add_zero [add_monoid A] (a : A) : a + zero = a :=
+by simp
 
-theorem bin_zero_add [add_monoid A] (a : A) : zero + a = a := !zero_add
+theorem bin_zero_add [add_monoid A] (a : A) : zero + a = a :=
+by simp
 
 theorem one_add_bit0 [add_comm_semigroup A] [has_one A] (a : A) : one + bit0 a = bit1 a :=
-  begin rewrite ↑[bit0, bit1], rewrite add.comm end
+by simp
 
 theorem bit0_add_one [has_add A] [has_one A] (a : A) : bit0 a + one = bit1 a :=
-  rfl
+rfl
 
 theorem bit1_add_one [has_add A] [has_one A] (a : A) : bit1 a + one = add1 (bit1 a) :=
-  rfl
+rfl
 
 theorem bit1_add_one_helper [has_add A] [has_one A] (a t : A) (H : add1 (bit1 a) = t) :
         bit1 a + one = t :=
-  by rewrite -H
+by rewrite -H
 
-theorem one_add_bit1 [add_comm_semigroup A] [has_one A] (a : A) :
-        one + bit1 a = add1 (bit1 a) := !add.comm
+theorem one_add_bit1 [add_comm_semigroup A] [has_one A] (a : A) : one + bit1 a = add1 (bit1 a) :=
+by simp
 
 theorem one_add_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A)
         (H : add1 (bit1 a) = t) : one + bit1 a = t :=
-  by rewrite -H; apply one_add_bit1
+by rewrite -H; simp
 
 theorem add1_bit0 [has_add A] [has_one A] (a : A) : add1 (bit0 a) = bit1 a :=
-  rfl
+rfl
 
 theorem add1_bit1 [add_comm_semigroup A] [has_one A] (a : A) :
         add1 (bit1 a) = bit0 (add1 a) :=
-  begin
-    rewrite ↑[add1, bit1, bit0],
-    rewrite [add.assoc, add_comm_four]
-  end
+by simp
 
 theorem add1_bit1_helper [add_comm_semigroup A] [has_one A] (a t : A) (H : add1 a = t) :
         add1 (bit1 a) = bit0 t :=
-  by rewrite -H; apply add1_bit1
+by rewrite -H; simp
 
 theorem add1_one [has_add A] [has_one A] : add1 (one : A) = bit0 one :=
-  rfl
+rfl
 
 theorem add1_zero [add_monoid A] [has_one A] : add1 (zero : A) = one :=
-  begin
-    rewrite [↑add1, zero_add]
-  end
+by simp
 
 theorem one_add_one [has_add A] [has_one A] : (one : A) + one = bit0 one :=
-  rfl
+rfl
 
 theorem subst_into_sum [has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
         (prt : tl + tr = t) : l + r = t :=
-   by rewrite [prl, prr, prt]
+by simp
 
 theorem neg_zero_helper [add_group A] (a : A) (H : a = 0) : - a = 0 :=
-  by rewrite [H, neg_zero]
+by simp
 
 end norm_num
 
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index de2147b60..c65478c82 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -69,7 +69,7 @@
     "apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at"
     "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
     "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite"
-    "xrewrite" "krewrite" "blast" "simp" "esimp" "unfold" "change" "check_expr" "contradiction"
+    "xrewrite" "krewrite" "blast" "simp" "simp_nohyps" "esimp" "unfold" "change" "check_expr" "contradiction"
     "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity"
     "symmetry" "transitivity" "state" "induction" "induction_using" "fail" "append"
     "substvars" "now" "with_options" "with_attributes" "with_attrs" "note")