diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 943a5770ba..ed9f27776b 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -119,7 +119,7 @@ have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from
         ... = pr1 (proj a)                              : (proj_ge_pr1 H)⁻¹
         ... = pr2 (flip (proj a))                       : (flip_pr2 (proj a))⁻¹,
   prod.equal H3 H4,
-or.elim le_total
+or.elim !le_total
   (assume H : pr2 a ≤ pr1 a, special a H)
   (assume H : pr1 a ≤ pr2 a,
     have H2 : pr2 (flip a) ≤ pr1 (flip a), from P_flip a H,
@@ -129,7 +129,7 @@ or.elim le_total
         ... = flip (proj a)                       : {flip_flip a})
 
 theorem proj_rel (a : ℕ × ℕ) : rel a (proj a) :=
-or.elim le_total
+or.elim !le_total
   (assume H : pr2 a ≤ pr1 a,
     calc
       pr1 a + pr2 (proj a) = pr1 a + 0 : {proj_ge_pr2 H}
@@ -148,7 +148,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from
   take a b,
   assume H2 : pr2 a ≤ pr1 a,
   assume H : rel a b,
-  have H3 : pr1 a + pr2 b ≤ pr2 a + pr1 b, from H ▸ le_refl,
+  have H3 : pr1 a + pr2 b ≤ pr2 a + pr1 b, from H ▸ !le_refl,
   have H4 : pr2 b ≤ pr1 b, from add_le_inv H3 H2,
   have H5 : pr1 (proj a) = pr1 (proj b), from
     calc
@@ -163,7 +163,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from
       pr2 (proj a) = 0 : proj_ge_pr2 H2
         ... = pr2 (proj b) : {(proj_ge_pr2 H4)⁻¹},
   prod.equal H5 H6,
-or.elim le_total
+or.elim !le_total
   (assume H2 : pr2 a ≤ pr1 a, special a b H2 H)
   (assume H2 : pr1 a ≤ pr2 a,
     have H3 : pr2 (flip a) ≤ pr1 (flip a), from P_flip a H2,
@@ -175,7 +175,7 @@ theorem proj_inj {a b : ℕ × ℕ} (H : proj a = proj b) : rel a b :=
 representative_map_equiv_inj rel_equiv proj_rel @proj_congr H
 
 theorem proj_zero_or (a : ℕ × ℕ) : pr1 (proj a) = 0 ∨ pr2 (proj a) = 0 :=
-or.elim le_total
+or.elim !le_total
   (assume H : pr2 a ≤ pr1 a, or.inr (proj_ge_pr2 H))
   (assume H : pr1 a ≤ pr2 a, or.inl (proj_le_pr1 H))
 
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index bd3a5b2e96..dd8849d4c1 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -420,7 +420,7 @@ obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H,
 Hn⁻¹ ▸ congr_arg of_nat (to_nat_of_nat n)
 
 theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
-iff.mp (iff.symm (le_of_nat _ _)) zero_le
+iff.mp (iff.symm !le_of_nat) !zero_le
 
 definition le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
 have aux : Πx, decidable (0 ≤ x), from
@@ -615,7 +615,7 @@ or.elim (em (a = 0))
         mul_cancel_right H3 H))
 
 theorem sign_idempotent (a : ℤ) : sign (sign a) = sign a :=
-have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (lt_of_nat 0 1)) succ_pos,
+have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (lt_of_nat 0 1)) !succ_pos,
     --this should be done with simp
 or.elim3 (trichotomy a 0) sorry sorry sorry
 --  (by simp)
@@ -623,7 +623,7 @@ or.elim3 (trichotomy a 0) sorry sorry sorry
 --  (by simp)
 
 theorem sign_succ (n : ℕ) : sign (succ n) = 1 :=
-sign_pos (iff.elim_left (iff.symm (lt_of_nat 0 (succ n))) succ_pos)
+sign_pos (iff.elim_left (iff.symm (lt_of_nat 0 (succ n))) !succ_pos)
   --this should be done with simp
 
 theorem sign_neg (a : ℤ) : sign (-a) = - sign a :=
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 76d670b521..eb8cd0f7b4 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -73,7 +73,7 @@ let f  := rec_measure default measure rec_val in
 case_strong_induction_on m
   (take x,
     have H1 : f' 0 x = default, from rfl,
-    have H2 : ¬ measure x < 0, from not_lt_zero,
+    have H2 : ¬ measure x < 0, from !not_lt_zero,
     have H3 : restrict default measure f 0 x = default, from if_neg H2,
     show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹)
   (take m,
@@ -86,7 +86,7 @@ case_strong_induction_on m
             take z,
               assume Hzx : measure z < measure x,
               calc
-                f' m z = restrict default measure f m z : IH m le_refl z
+                f' m z = restrict default measure f m z : IH m !le_refl z
                   ... = f z : restrict_lt_eq _ _ _ _ _ (lt_le_trans Hzx (lt_succ_imp_le H1)),
           have H2 : f' (succ m) x = rec_val x f, from
             calc
@@ -105,7 +105,7 @@ case_strong_induction_on m
               restrict default measure f (succ m) x = f x : if_pos H1
                 ... = f' (succ m') x : eq.refl _
                 ... = if measure x < succ m' then rec_val x (f' m') else default : rfl
-                ... = rec_val x (f' m') : if_pos self_lt_succ
+                ... = rec_val x (f' m') : if_pos !self_lt_succ
                 ... = rec_val x f : rec_decreasing _ _ _ H3a,
           show f' (succ m) x = restrict default measure f (succ m) x,
             from H2 ⬝ H3⁻¹)
@@ -138,7 +138,7 @@ have H : ∀z, measure z < measure x → f' m z = f z, from
 calc
   f x = f' (succ m) x : rfl
     ... = if measure x < succ m then rec_val x (f' m) else default : rfl
-    ... = rec_val x (f' m) : if_pos (self_lt_succ)
+    ... = rec_val x (f' m) : if_pos !self_lt_succ
     ... = rec_val x f : rec_decreasing _ _ _ H
 
 
@@ -193,7 +193,7 @@ div_aux_spec _ _ ⬝ if_pos (or.inr H)
 -- add_rewrite div_less
 
 theorem zero_div {y : ℕ} : 0 div y = 0 :=
-case y div_zero (take y', div_less succ_pos)
+case y div_zero (take y', div_less !succ_pos)
 
 -- add_rewrite zero_div
 
@@ -202,7 +202,7 @@ have H3 : ¬ (y = 0 ∨ x < y), from
   not_intro
     (assume H4 : y = 0 ∨ x < y,
       or.elim H4
-        (assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1))
+        (assume H5 : y = 0, not_elim !lt_irrefl (H5 ▸ H1))
         (assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)),
 div_aux_spec _ _ ⬝ if_neg H3
 
@@ -269,7 +269,7 @@ mod_aux_spec _ _ ⬝ if_pos (or.inr H)
 -- add_rewrite mod_lt_eq
 
 theorem zero_mod {y : ℕ} : 0 mod y = 0 :=
-case y mod_zero (take y', mod_lt_eq succ_pos)
+case y mod_zero (take y', mod_lt_eq !succ_pos)
 
 -- add_rewrite zero_mod
 
@@ -278,7 +278,7 @@ have H3 : ¬ (y = 0 ∨ x < y), from
   not_intro
     (assume H4 : y = 0 ∨ x < y,
       or.elim H4
-        (assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1))
+        (assume H5 : y = 0, not_elim !lt_irrefl (H5 ▸ H1))
         (assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)),
 mod_aux_spec _ _ ⬝ if_neg H3
 
@@ -325,7 +325,7 @@ case_strong_induction_on x
         (assume H1 : ¬ succ x < y,
           have H2 : y ≤ succ x, from not_lt_imp_ge H1,
           have H3 : succ x mod y = (succ x - y) mod y, from mod_rec H H2,
-          have H4 : succ x - y < succ x, from sub_lt succ_pos H,
+          have H4 : succ x - y < succ x, from sub_lt !succ_pos H,
           have H5 : succ x - y ≤ x, from lt_succ_imp_le H4,
           show succ x mod y < y, from H3⁻¹ ▸ IH _ H5))
 
@@ -353,7 +353,7 @@ case_zero_pos y
                 have H2 : y ≤ succ x, from not_lt_imp_ge H1,
                 have H3 : succ x div y = succ ((succ x - y) div y), from div_rec H H2,
                 have H4 : succ x mod y = (succ x - y) mod y, from mod_rec H H2,
-                have H5 : succ x - y < succ x, from sub_lt succ_pos H,
+                have H5 : succ x - y < succ x, from sub_lt !succ_pos H,
                 have H6 : succ x - y ≤ x, from lt_succ_imp_le H5,
                 (calc
                   succ x div y * y + succ x mod y = succ ((succ x - y) div y) * y + succ x mod y :
@@ -365,7 +365,7 @@ case_zero_pos y
                     ... = succ x : add_sub_ge_left H2)⁻¹)))
 
 theorem mod_le {x y : ℕ} : x mod y ≤ x :=
-div_mod_eq⁻¹ ▸ le_add_left
+div_mod_eq⁻¹ ▸ !le_add_left
 
 --- a good example where simplifying using the context causes problems
 theorem remainder_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y) (H2 : r2 < y)
@@ -382,7 +382,7 @@ theorem quotient_unique {y : ℕ} (H : y > 0) {q1 r1 q2 r2 : ℕ} (H1 : r1 < y)
   (H3 : q1 * y + r1 = q2 * y + r2) : q1 = q2 :=
 have H4 : q1 * y + r2 = q2 * y + r2, from (remainder_unique H H1 H2 H3) ▸ H3,
 have H5 : q1 * y = q2 * y, from add.cancel_right H4,
-have H6 : y > 0, from le_lt_trans zero_le H1,
+have H6 : y > 0, from le_lt_trans !zero_le H1,
 show q1 = q2, from mul_cancel_right H6 H5
 
 theorem div_mul_mul {z x y : ℕ} (zpos : z > 0) : (z * x) div (z * y) = x div y :=
@@ -418,7 +418,7 @@ by_cases -- (y = 0)
           ... = (x div y) * (z * y) + z * (x mod y) : {!mul.left_comm}))
 
 theorem mod_one {x : ℕ} : x mod 1 = 0 :=
-have H1 : x mod 1 < 1, from mod_lt succ_pos,
+have H1 : x mod 1 < 1, from mod_lt !succ_pos,
 le_zero (lt_succ_imp_le H1)
 
 -- add_rewrite mod_one
@@ -427,7 +427,7 @@ theorem mod_self {n : ℕ} : n mod n = 0 :=
 case n (by simp)
   (take n,
     have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
-      from mod_mul_mul succ_pos,
+      from mod_mul_mul !succ_pos,
     (by simp) ▸ H)
 
 -- add_rewrite mod_self
@@ -651,9 +651,9 @@ have aux : ∀m, P m n, from
     (take n,
       assume IH : ∀k, k ≤ n → ∀m, P m k,
       take m,
-      have H2 : m mod succ n ≤ n, from lt_succ_imp_le (mod_lt succ_pos),
+      have H2 : m mod succ n ≤ n, from lt_succ_imp_le (mod_lt !succ_pos),
       have H3 : P (succ n) (m mod succ n), from IH _ H2 _,
-      show P m (succ n), from H1 _ _ succ_pos H3),
+      show P m (succ n), from H1 _ _ !succ_pos H3),
 aux m
 
 theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) :=
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 1173f9f1de..a5fe4128ea 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -34,17 +34,17 @@ irreducible le
 
 -- ### partial order (totality is part of less than)
 
-theorem le_refl {n : ℕ} : n ≤ n :=
+theorem le_refl (n : ℕ) : n ≤ n :=
 le_intro !add.zero_right
 
-theorem zero_le {n : ℕ} : 0 ≤ n :=
+theorem zero_le (n : ℕ) : 0 ≤ n :=
 le_intro !add.zero_left
 
 theorem le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
 obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
 add.eq_zero_left Hk
 
-theorem not_succ_zero_le {n : ℕ} : ¬ succ n ≤ 0 :=
+theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0 :=
 not_intro
   (assume H : succ n ≤ 0,
     have H2 : succ n = 0, from le_zero H,
@@ -77,10 +77,10 @@ calc
 
 -- ### interaction with addition
 
-theorem le_add_right {n m : ℕ} : n ≤ n + m :=
+theorem le_add_right (n m : ℕ) : n ≤ n + m :=
 le_intro rfl
 
-theorem le_add_left {n m : ℕ} : n ≤ m + n :=
+theorem le_add_left (n m : ℕ): n ≤ m + n :=
 le_intro !add.comm
 
 theorem add_le_left {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m :=
@@ -111,7 +111,7 @@ theorem add_le_inv {n m k l : ℕ} (H1 : n + m ≤ k + l) (H2 : k ≤ n) : m ≤
 obtain (a : ℕ) (Ha : k + a = n), from le_elim H2,
 have H3 : k + (a + m) ≤ k + l, from !add.assoc ▸ Ha⁻¹ ▸ H1,
 have H4 : a + m ≤ l, from add_le_cancel_left H3,
-show m ≤ l, from le_trans le_add_left H4
+show m ≤ l, from le_trans !le_add_left H4
 
 -- add_rewrite le_add_right le_add_left
 
@@ -123,11 +123,11 @@ theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m :=
 theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) :  n ≤ m :=
 add_le_cancel_right (!add.one⁻¹ ▸ !add.one⁻¹ ▸ H)
 
-theorem self_le_succ {n : ℕ} : n ≤ succ n :=
+theorem self_le_succ (n : ℕ) : n ≤ succ n :=
 le_intro !add.one
 
 theorem le_imp_le_succ {n m : ℕ} (H : n ≤ m) : n ≤ succ m :=
-le_trans H self_le_succ
+le_trans H !self_le_succ
 
 theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m :=
 obtain (k : ℕ) (Hk : n + k = m), from (le_elim H),
@@ -166,13 +166,13 @@ obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H),
     show n ≤ m, from le_intro H3)
   (assume H3 : n = m,
       have H4 : succ n ≤ n, from H3⁻¹ ▸ H,
-      have H5 : succ n = n, from le_antisym H4 self_le_succ,
+      have H5 : succ n = n, from le_antisym H4 !self_le_succ,
       show false, from absurd H5 succ.ne_self)
 
-theorem le_pred_self {n : ℕ} : pred n ≤ n :=
+theorem le_pred_self (n : ℕ) : pred n ≤ n :=
 case n
-  (pred.zero⁻¹ ▸ le_refl)
-  (take k : ℕ, !pred.succ⁻¹ ▸ self_le_succ)
+  (pred.zero⁻¹ ▸ !le_refl)
+  (take k : ℕ, !pred.succ⁻¹ ▸ !self_le_succ)
 
 theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m :=
 discriminate
@@ -181,7 +181,7 @@ discriminate
       from calc
         pred n = pred 0 : {Hn}
            ... = 0 : pred.zero,
-    H2⁻¹ ▸ zero_le)
+    H2⁻¹ ▸ !zero_le)
   (take k : ℕ,
     assume Hn : n = succ k,
     obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
@@ -198,7 +198,7 @@ discriminate
 theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m :=
 discriminate
   (take Hn : n = 0,
-    or.inl (Hn⁻¹ ▸ zero_le))
+    or.inl (Hn⁻¹ ▸ !zero_le))
   (take k : ℕ,
     assume Hn : n = succ k,
     have H2 : pred n = k,
@@ -235,11 +235,11 @@ have general : ∀n, decidable (n ≤ m), from
   rec_on m
     (take n,
       rec_on n
-        (decidable.inl le_refl)
-        (take m iH, decidable.inr not_succ_zero_le))
+        (decidable.inl !le_refl)
+        (take m iH, decidable.inr !not_succ_zero_le))
     (take (m' : ℕ) (iH1 : ∀n, decidable (n ≤ m')) (n : ℕ),
       rec_on n
-        (decidable.inl zero_le)
+        (decidable.inl !zero_le)
         (take (n' : ℕ) (iH2 : decidable (n' ≤ succ m')),
           decidable.by_cases
             (assume Hp : n' ≤ m', decidable.inl (succ_le Hp))
@@ -283,18 +283,18 @@ lt_intro !add.move_succ
 theorem lt_imp_ne {n m : ℕ} (H : n < m) : n ≠ m :=
 and.elim_right (succ_le_imp_le_and_ne H)
 
-theorem lt_irrefl {n : ℕ} : ¬ n < n :=
+theorem lt_irrefl (n : ℕ) : ¬ n < n :=
 not_intro (assume H : n < n, absurd rfl (lt_imp_ne H))
 
-theorem succ_pos {n : ℕ} : 0 < succ n :=
-succ_le zero_le
+theorem succ_pos (n : ℕ) : 0 < succ n :=
+succ_le !zero_le
 
-theorem not_lt_zero {n : ℕ} : ¬ n < 0 :=
-not_succ_zero_le
+theorem not_lt_zero (n : ℕ) : ¬ n < 0 :=
+!not_succ_zero_le
 
 theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
 discriminate
-  (take (Hm : m = 0), absurd (Hm ▸ H) not_lt_zero)
+  (take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
   (take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
 
 -- ### interaction with le
@@ -305,8 +305,8 @@ H
 theorem le_succ_imp_lt {n m : ℕ} (H : succ n ≤ m) : n < m :=
 H
 
-theorem self_lt_succ {n : ℕ} : n < succ n :=
-le_refl
+theorem self_lt_succ (n : ℕ) : n < succ n :=
+!le_refl
 
 theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m :=
 and.elim_left (succ_le_imp_le_and_ne H)
@@ -335,10 +335,10 @@ theorem lt_trans {n m k : ℕ} (H1 : n < m) (H2 : m < k) : n < k :=
 lt_le_trans H1 (lt_imp_le H2)
 
 theorem le_imp_not_gt {n m : ℕ} (H : n ≤ m) : ¬ n > m :=
-not_intro (assume H2 : m < n, absurd (le_lt_trans H H2) lt_irrefl)
+not_intro (assume H2 : m < n, absurd (le_lt_trans H H2) !lt_irrefl)
 
 theorem lt_imp_not_ge {n m : ℕ} (H : n < m) : ¬ n ≥ m :=
-not_intro (assume H2 : m ≤ n, absurd (lt_le_trans H H2) lt_irrefl)
+not_intro (assume H2 : m ≤ n, absurd (lt_le_trans H H2) !lt_irrefl)
 
 theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n :=
 le_imp_not_gt (lt_imp_le H)
@@ -375,13 +375,13 @@ theorem succ_lt_cancel {n m : ℕ} (H : succ n < succ m) :  n < m :=
 add_lt_cancel_right (!add.one⁻¹ ▸ !add.one⁻¹ ▸ H)
 
 theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m
-:= lt_trans H self_lt_succ
+:= lt_trans H !self_lt_succ
 
 -- ### totality of lt and le
 
 theorem le_or_gt {n m : ℕ} : n ≤ m ∨ n > m :=
 induction_on n
-  (or.inl zero_le)
+  (or.inl !zero_le)
   (take (k : ℕ),
     assume IH : k ≤ m ∨ m < k,
     or.elim IH
@@ -394,7 +394,7 @@ induction_on n
                 m = k + l     : Hl⁻¹
                   ... = k + 0 : {H2}
                   ... = k     : !add.zero_right,
-            have H4 : m < succ k, from H3 ▸ self_lt_succ,
+            have H4 : m < succ k, from H3 ▸ !self_lt_succ,
             or.inr H4)
           (take l2 : ℕ,
             assume H2 : l = succ l2,
@@ -406,13 +406,13 @@ induction_on n
             or.inl (le_intro H3)))
       (assume H : m < k, or.inr (lt_imp_lt_succ H)))
 
-theorem trichotomy_alt {n m : ℕ} : (n < m ∨ n = m) ∨ n > m :=
+theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ n > m :=
 or.imp_or_left le_or_gt (assume H : n ≤ m, le_imp_lt_or_eq H)
 
-theorem trichotomy {n m : ℕ} : n < m ∨ n = m ∨ n > m :=
-iff.elim_left or.assoc trichotomy_alt
+theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ n > m :=
+iff.elim_left or.assoc !trichotomy_alt
 
-theorem le_total {n m : ℕ} : n ≤ m ∨ m ≤ n :=
+theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n :=
 or.imp_or_right le_or_gt (assume H : m < n, lt_imp_le H)
 
 theorem not_lt_imp_ge {n m : ℕ} (H : ¬ n < m) : n ≥ m :=
@@ -434,7 +434,7 @@ protected theorem strong_induction_on {P : nat → Prop} (n : ℕ) (H : ∀n, (
 have H1 : ∀ {n m : nat}, m < n → P m, from
   take n,
   induction_on n
-    (show ∀m, m < 0 → P m, from take m H, absurd H not_lt_zero)
+    (show ∀m, m < 0 → P m, from take m H, absurd H !not_lt_zero)
     (take n',
       assume IH : ∀ {m : nat}, m < n' → P m,
       have H2: P n', from H n' @IH,
@@ -444,7 +444,7 @@ have H1 : ∀ {n m : nat}, m < n → P m, from
         or.elim (le_imp_lt_or_eq (lt_succ_imp_le H3))
           (assume H4: m < n', IH H4)
           (assume H4: m = n', H4⁻¹ ▸ H2)),
-H1 self_lt_succ
+H1 !self_lt_succ
 
 protected theorem case_strong_induction_on {P : nat → Prop} (a : nat) (H0 : P 0)
   (Hind : ∀(n : nat), (∀m, m ≤ n → P m) → P (succ n)) : P a :=
@@ -466,15 +466,15 @@ strong_induction_on a (
 -- ### basic
 
 theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat}, y > 0 → P y) : P y :=
-case y H0 (take y, H1 succ_pos)
+case y H0 (take y, H1 !succ_pos)
 
 theorem zero_or_pos {n : ℕ} : n = 0 ∨ n > 0 :=
 or.imp_or_left
-  (or.swap (le_imp_lt_or_eq zero_le))
+  (or.swap (le_imp_lt_or_eq !zero_le))
   (take H : 0 = n, H⁻¹)
 
 theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 :=
-H⁻¹ ▸ succ_pos
+H⁻¹ ▸ !succ_pos
 
 theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
 or.elim zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
@@ -510,10 +510,10 @@ discriminate
         n * m = 0 * m : {H2}
           ... = 0     : !mul.zero_left,
     have H4 : 0 > 0, from H3 ▸ H,
-    absurd H4 lt_irrefl)
+    absurd H4 !lt_irrefl)
   (take l : nat,
     assume Hl : n = succ l,
-    Hl⁻¹ ▸ succ_pos)
+    Hl⁻¹ ▸ !succ_pos)
 
 theorem mul_pos_imp_pos_right {m n : ℕ} (H : n * m > 0) : m > 0 :=
 mul_pos_imp_pos_left (!mul.comm ▸ H)
@@ -536,7 +536,7 @@ le_lt_trans (mul_le_left H2 n) (mul_lt_right Hl H1)
 
 theorem mul_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n * m < k * l :=
 have H3 : n * m ≤ k * m, from mul_le_right (lt_imp_le H1) m,
-have H4 : k * m < k * l, from mul_lt_left (le_lt_trans zero_le H1) H2,
+have H4 : k * m < k * l, from mul_lt_left (le_lt_trans !zero_le H1) H2,
 le_lt_trans H3 H4
 
 theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m :=
@@ -559,8 +559,8 @@ theorem mul_le_cancel_right {n k m : ℕ} (Hm : m > 0) (H : n * m ≤ k * m) : n
 mul_le_cancel_left Hm (!mul.comm ▸ !mul.comm ▸ H)
 
 theorem mul_cancel_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
-have H2 : n * m ≤ n * k, from H ▸ le_refl,
-have H3 : n * k ≤ n * m, from H ▸ le_refl,
+have H2 : n * m ≤ n * k, from H ▸ !le_refl,
+have H3 : n * k ≤ n * m, from H ▸ !le_refl,
 have H4 : m ≤ k, from mul_le_cancel_left Hn H2,
 have H5 : k ≤ m, from mul_le_cancel_left Hn H3,
 le_antisym H4 H5
@@ -576,7 +576,7 @@ theorem mul_cancel_right_or  {n m k : ℕ} (H : n * m = k * m) : m = 0 ∨ n = k
 mul_cancel_left_or (!mul.comm ▸ !mul.comm ▸ H)
 
 theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 :=
-have H2 : n * m > 0, from H⁻¹ ▸ succ_pos,
+have H2 : n * m > 0, from H⁻¹ ▸ !succ_pos,
 have H3 : n > 0, from mul_pos_imp_pos_left H2,
 have H4 : m > 0, from mul_pos_imp_pos_right H2,
 or.elim le_or_gt
@@ -585,7 +585,7 @@ or.elim le_or_gt
   (assume H5 : n > 1,
     have H6 : n * m ≥ 2 * 1, from mul_le H5 H4,
     have H7 : 1 ≥ 2, from !mul.one_right ▸ H ▸ H6,
-    absurd self_lt_succ (le_imp_not_gt H7))
+    absurd !self_lt_succ (le_imp_not_gt H7))
 
 theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
 mul_eq_one_left (!mul.comm ▸ H)
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 2cb65c98e9..8b7de383b2 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -180,7 +180,7 @@ sub_induction n m
              ... = succ (k - 0) : {sub_zero_right⁻¹})
   (take k,
     assume H : succ k ≤ 0,
-    absurd H not_succ_zero_le)
+    absurd H !not_succ_zero_le)
   (take k l,
     assume IH : k ≤ l → succ l - k = succ (l - k),
     take H : succ k ≤ succ l,
@@ -199,7 +199,7 @@ sub_induction n m
     calc
       0 + (k - 0) = k - 0 : !add.zero_left
               ... = k     : sub_zero_right)
-  (take k, assume H : succ k ≤ 0, absurd H not_succ_zero_le)
+  (take k, assume H : succ k ≤ 0, absurd H !not_succ_zero_le)
   (take k l,
     assume IH : k ≤ l → k + (l - k) = l,
     take H : succ k ≤ succ l,
@@ -209,7 +209,7 @@ sub_induction n m
                              ... = succ l             : {IH (succ_le_cancel H)})
 
 theorem add_sub_ge_left {n m : ℕ} : n ≥ m → n - m + m = n :=
-!add.comm ▸ add_sub_le
+!add.comm ▸ !add_sub_le
 
 theorem add_sub_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n :=
 calc
@@ -220,24 +220,24 @@ theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m :=
 !add.comm ▸ add_sub_ge
 
 theorem le_add_sub_left {n m : ℕ} : n ≤ n + (m - n) :=
-or.elim le_total
+or.elim !le_total
   (assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ H)
-  (assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ le_refl)
+  (assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ !le_refl)
 
 theorem le_add_sub_right {n m : ℕ} : m ≤ n + (m - n) :=
-or.elim le_total
-  (assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ le_refl)
+or.elim !le_total
+  (assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ !le_refl)
   (assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ H)
 
 theorem sub_split {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k)
   : P (n - m) :=
-or.elim le_total
+or.elim !le_total
   (assume H3 : n ≤ m, (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 H3))
   (assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3))
 
 theorem sub_le_self {n m : ℕ} : n - m ≤ n :=
 sub_split
-  (assume H : n ≤ m, zero_le)
+  (assume H : n ≤ m, !zero_le)
   (take k : ℕ, assume H : m + k = n, le_intro (!add.comm ▸ H))
 
 theorem le_elim_sub {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
@@ -255,7 +255,7 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
       calc
         n + m - 0 = n + m       : sub_zero_right
               ... = n + (m - 0) : {sub_zero_right⁻¹})
-    (take k : ℕ, assume H : succ k ≤ 0, absurd H not_succ_zero_le)
+    (take k : ℕ, assume H : succ k ≤ 0, absurd H !not_succ_zero_le)
     (take k m,
       assume IH : k ≤ m → n + m - k = n + (m - k),
       take H : succ k ≤ succ m,
@@ -273,11 +273,11 @@ sub_split
     assume H1 : m + k = n,
     assume H2 : k = 0,
     have H3 : n = m, from !add.zero_right ▸ H2 ▸ H1⁻¹,
-    H3 ▸ le_refl)
+    H3 ▸ !le_refl)
 
 theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0)
   (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) :=
-or.elim le_total
+or.elim !le_total
   (assume H3 : n ≤ m,
     le_imp_sub_eq_zero H3⁻¹ ▸  (H2 (m - n) (add_sub_le H3⁻¹)))
   (assume H3 : m ≤ n,
@@ -300,13 +300,13 @@ obtain (x' : ℕ) (xeq : x = succ x'), from pos_imp_eq_succ xpos,
        ... = succ x' - succ y' : {yeq}
        ... = x' - y'           : sub_succ_succ,
  have H1 : x' - y' ≤ x', from sub_le_self,
- have H2 : x' < succ x', from self_lt_succ,
+ have H2 : x' < succ x', from !self_lt_succ,
  show x - y < x, from xeq⁻¹ ▸ xsuby_eq⁻¹ ▸ le_lt_trans H1 H2
 
 theorem sub_le_right {n m : ℕ} (H : n ≤ m) (k : nat) : n - k ≤ m - k :=
 obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
-or.elim le_total
-  (assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ zero_le)
+or.elim !le_total
+  (assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ !zero_le)
   (assume H2 : k ≤ n,
     have H3 : n - k + l = m - k, from
       calc
@@ -319,7 +319,7 @@ or.elim le_total
 theorem sub_le_left {n m : ℕ} (H : n ≤ m) (k : nat) : k - m ≤ k - n :=
 obtain (l : ℕ) (Hl : n + l = m), from le_elim H,
 sub_split
-  (assume H2 : k ≤ m, zero_le)
+  (assume H2 : k ≤ m, !zero_le)
   (take m' : ℕ,
     assume Hm : m + m' = k,
     have H3 : n ≤ k, from le_trans H (le_intro Hm),
@@ -357,7 +357,7 @@ sub_split
                       ... = m + mn      : {Hkm}
                       ... = n           : Hmn,
         have H2 : n - k = mn + km, from sub_intro H,
-        H2 ▸ le_refl))
+        H2 ▸ !le_refl))
 
 
 -- add_rewrite sub_self mul_sub_distr_left mul_sub_distr_right
@@ -407,10 +407,10 @@ theorem dist_ge {n m : ℕ} (H : n ≥ m) : dist n m = n - m :=
 dist_comm ▸ dist_le H
 
 theorem dist_zero_right {n : ℕ} : dist n 0 = n :=
-dist_ge zero_le ⬝ sub_zero_right
+dist_ge !zero_le ⬝ sub_zero_right
 
 theorem dist_zero_left {n : ℕ} : dist 0 n = n :=
-dist_le zero_le ⬝ sub_zero_right
+dist_le !zero_le ⬝ sub_zero_right
 
 theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m :=
 calc
@@ -479,7 +479,7 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l
   take k l : ℕ,
   assume H : k ≥ l,
   have H2 : m * k ≥ m * l, from mul_le_left H m,
-  have H3 : n * l + m * k ≥ m * l, from le_trans H2 le_add_left,
+  have H3 : n * l + m * k ≥ m * l, from le_trans H2 !le_add_left,
   calc
     dist n m * dist k l = dist n m * (k - l)       : {dist_ge H}
       ... = dist (n * (k - l)) (m * (k - l))       : dist_mul_right⁻¹
@@ -488,7 +488,7 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l
       ... = dist (n * k) (n * l + (m * k - m * l)) : {!add.comm}
       ... = dist (n * k) (n * l + m * k - m * l)   : {(add_sub_assoc H2 (n * l))⁻¹}
       ... = dist (n * k + m * l) (n * l + m * k)   : dist_sub_move_add' H3 _,
-or.elim le_total
+or.elim !le_total
   (assume H : k ≤ l, dist_comm ▸ dist_comm ▸ aux l k H)
   (assume H : l ≤ k, aux k l H)
 
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index 90f2ac8fd1..53d5baeb36 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -63,7 +63,7 @@ let f  := rec_measure default measure rec_val in
 case_strong_induction_on m
   (take x,
     have H1 : f' 0 x = default, from rfl,
-    have H2 : ¬ measure x < 0, from not_lt_zero,
+    have H2 : ¬ measure x < 0, from !not_lt_zero,
     have H3 : restrict default measure f 0 x = default, from if_neg H2,
     show f' 0 x = restrict default measure f 0 x, from H1 ⬝ H3⁻¹)
   (take m,
@@ -77,8 +77,8 @@ case_strong_induction_on m
             take z,
               assume Hzx : measure z < measure x,
               calc
-                f' m z = restrict default measure f m z : IH m le_refl z
-                  ... = f z : restrict_lt_eq _ _ _ _ _ (lt_le_trans Hzx (lt_succ_imp_le H1))
+                f' m z = restrict default measure f m z : IH m !le_refl z
+                  ... = f z : !restrict_lt_eq (lt_le_trans Hzx (lt_succ_imp_le H1))
           ∎,
           have H2 : f' (succ m) x = rec_val x f,
           proof
@@ -94,15 +94,15 @@ case_strong_induction_on m
               assume Hzx : measure z < measure x,
               calc
                 f' m' z = restrict default measure f m' z : IH _ (lt_succ_imp_le H1) _
-                  ... = f z : restrict_lt_eq _ _ _ _ _ Hzx
+                  ... = f z : !restrict_lt_eq Hzx
           qed,
           have H3 : restrict default measure f (succ m) x = rec_val x f,
           proof
             calc
               restrict default measure f (succ m) x = f x : if_pos H1
-                ... = f' (succ m') x : eq.refl _
+                ... = f' (succ m') x : !eq.refl
                 ... = if measure x < succ m' then rec_val x (f' m') else default : rfl
-                ... = rec_val x (f' m') : if_pos self_lt_succ
+                ... = rec_val x (f' m') : if_pos !self_lt_succ
                 ... = rec_val x f : rec_decreasing _ _ _ H3a
           qed,
           show f' (succ m) x = restrict default measure f (succ m) x,