From 0de715ae54f7466777f683d481388d73cca926d2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Jul 2015 09:10:56 -0700
Subject: [PATCH] refactor(library/data): cleanup proofs using new features

---
 library/algebra/ring.lean                     | 148 +++++++++---------
 library/data/bool.lean                        |  15 +-
 library/data/int/basic.lean                   |  30 ++--
 library/data/int/div.lean                     |  28 ++--
 library/data/int/gcd.lean                     |  62 ++++----
 library/data/int/order.lean                   | 110 ++++++-------
 library/data/nat/choose.lean                  |  28 ++--
 library/data/num.lean                         |   8 +-
 library/data/rat/basic.lean                   |  52 +++---
 library/data/stream.lean                      |   4 +-
 .../number_theory/prime_factorization.lean    |  58 +++----
 library/theories/number_theory/primes.lean    |  23 +--
 12 files changed, 284 insertions(+), 282 deletions(-)

diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index e0fa6fe62..87a1c9d6b 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -49,14 +49,14 @@ section semiring
   include s
 
   theorem ne_zero_of_mul_ne_zero_right {a b : A} (H : a * b ≠ 0) : a ≠ 0 :=
-  assume H1 : a = 0,
-  have H2 : a * b = 0, from H1⁻¹ ▸ zero_mul b,
-  H H2
+  suppose a = 0,
+  have a * b = 0, from this⁻¹ ▸ zero_mul b,
+  H this
 
   theorem ne_zero_of_mul_ne_zero_left {a b : A} (H : a * b ≠ 0) : b ≠ 0 :=
-  assume H1 : b = 0,
-  have H2 : a * b = 0, from H1⁻¹ ▸ mul_zero a,
-  H H2
+  suppose b = 0,
+  have a * b = 0, from this⁻¹ ▸ mul_zero a,
+  H this
 
   theorem distrib_three_right (a b c d : A) : (a + b + c) * d = a * d + b * d + c * d :=
     by rewrite *right_distrib
@@ -116,21 +116,21 @@ section comm_semiring
   theorem dvd_mul_of_dvd_left {a b : A} (H : a ∣ b) (c : A) : a ∣ b * c :=
   dvd.elim H
     (take d,
-      assume H₁ : b = a * d,
+      suppose b = a * d,
       dvd.intro
-        (show a * (d * c) = b * c, from by rewrite [-mul.assoc, H₁]))
+        (show a * (d * c) = b * c, from by rewrite [-mul.assoc]; substvars))
 
   theorem dvd_mul_of_dvd_right {a b : A} (H : a ∣ b) (c : A) : a ∣ c * b :=
   !mul.comm ▸ (dvd_mul_of_dvd_left H _)
 
   theorem mul_dvd_mul {a b c d : A} (dvd_ab : a ∣ b) (dvd_cd : c ∣ d) : a * c ∣ b * d :=
   dvd.elim dvd_ab
-    (take e, assume Haeb : b = a * e,
+    (take e, suppose b = a * e,
       dvd.elim dvd_cd
-        (take f, assume Hcfd : d = c * f,
+        (take f, suppose d = c * f,
           dvd.intro
             (show a * c * (e * f) = b * d,
-             by rewrite [mul.assoc, {c*_}mul.left_comm, -mul.assoc, Haeb, Hcfd])))
+             by rewrite [mul.assoc, {c*_}mul.left_comm, -mul.assoc]; substvars)))
 
   theorem dvd_of_mul_right_dvd {a b c : A} (H : a * b ∣ c) : a ∣ c :=
   dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc⁻¹))
@@ -140,11 +140,11 @@ section comm_semiring
 
   theorem dvd_add {a b c : A} (Hab : a ∣ b) (Hac : a ∣ c) : a ∣ b + c :=
   dvd.elim Hab
-    (take d, assume Hadb : b = a * d,
+    (take d, suppose b = a * d,
       dvd.elim Hac
-        (take e, assume Haec : c = a * e,
+        (take e, suppose c = a * e,
           dvd.intro (show a * (d + e) = b + c,
-                     by rewrite [left_distrib, -Hadb, -Haec])))
+                     by rewrite [left_distrib]; substvars)))
 end comm_semiring
 
 /- ring -/
@@ -152,18 +152,18 @@ end comm_semiring
 structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A
 
 theorem ring.mul_zero [s : ring A] (a : A) : a * 0 = 0 :=
-have H : a * 0 + 0 = a * 0 + a * 0, from calc
+have a * 0 + 0 = a * 0 + a * 0, from calc
   a * 0 + 0 = a * 0         : by rewrite add_zero
         ... = a * (0 + 0)   : by rewrite add_zero
         ... = a * 0 + a * 0 : by rewrite {a*_}ring.left_distrib,
-show a * 0 = 0, from (add.left_cancel H)⁻¹
+show a * 0 = 0, from (add.left_cancel this)⁻¹
 
 theorem ring.zero_mul [s : ring A] (a : A) : 0 * a = 0 :=
-have H : 0 * a + 0 = 0 * a + 0 * a, from calc
+have 0 * a + 0 = 0 * a + 0 * a, from calc
   0 * a + 0 = 0 * a         : by rewrite add_zero
         ... = (0 + 0) * a   : by rewrite add_zero
         ... = 0 * a + 0 * a : by rewrite {_*a}ring.right_distrib,
-show 0 * a = 0, from  (add.left_cancel H)⁻¹
+show 0 * a = 0, from  (add.left_cancel this)⁻¹
 
 definition ring.to_semiring [trans-instance] [coercion] [reducible] [s : ring A] : semiring A :=
 ⦃ semiring, s,
@@ -223,23 +223,23 @@ section
       ... ↔ (a - b) * e + c = d   : by rewrite mul_sub_right_distrib
 
   theorem mul_neg_one_eq_neg : a * (-1) = -a :=
-    have H : a + a * -1 = 0, from calc
+    have a + a * -1 = 0, from calc
       a + a * -1 = a * 1 + a * -1 : mul_one
              ... = a * (1 + -1)   : left_distrib
              ... = a * 0          : add.right_inv
              ... = 0              : mul_zero,
-    symm (neg_eq_of_add_eq_zero H)
+    symm (neg_eq_of_add_eq_zero this)
 
   theorem ne_zero_and_ne_zero_of_mul_ne_zero {a b : A} (H : a * b ≠ 0) : a ≠ 0 ∧ b ≠ 0 :=
-    have Ha : a ≠ 0, from
-      (assume Ha1 : a = 0,
-        have H1 : a * b = 0, by rewrite [Ha1, zero_mul],
-        absurd H1 H),
-    have Hb : b ≠ 0, from
-      (assume Hb1 : b = 0,
-        have H1 : a * b = 0, by rewrite [Hb1, mul_zero],
-        absurd H1 H),
-    and.intro Ha Hb
+    have a ≠ 0, from
+      (suppose a = 0,
+        have a * b = 0, by rewrite [this, zero_mul],
+        absurd this H),
+    have b ≠ 0, from
+      (suppose b = 0,
+        have a * b = 0, by rewrite [this, mul_zero],
+        absurd this H),
+    and.intro `a ≠ 0` `b ≠ 0`
 end
 
 structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
@@ -265,31 +265,31 @@ section
 
   theorem dvd_neg_iff_dvd : (a ∣ -b) ↔ (a ∣ b) :=
   iff.intro
-    (assume H : (a ∣ -b),
-      dvd.elim H
-        (take c, assume H' : -b = a * c,
+    (suppose a ∣ -b,
+      dvd.elim this
+        (take c, suppose -b = a * c,
           dvd.intro
             (show a * -c = b,
-             by rewrite [-neg_mul_eq_mul_neg, -H', neg_neg])))
-    (assume H : (a ∣ b),
-      dvd.elim H
-        (take c, assume H' : b = a * c,
+             by rewrite [-neg_mul_eq_mul_neg, -this, neg_neg])))
+    (suppose a ∣ b,
+      dvd.elim this
+        (take c, suppose b = a * c,
           dvd.intro
             (show a * -c = -b,
-             by rewrite [-neg_mul_eq_mul_neg, -H'])))
+             by rewrite [-neg_mul_eq_mul_neg, -this])))
 
   theorem neg_dvd_iff_dvd : (-a ∣ b) ↔ (a ∣ b) :=
   iff.intro
-    (assume H : (-a ∣ b),
-      dvd.elim H
-        (take c, assume H' : b = -a * c,
+    (suppose -a ∣ b,
+      dvd.elim this
+        (take c, suppose b = -a * c,
           dvd.intro
-            (show a * -c = b, by rewrite [-neg_mul_comm, H'])))
-    (assume H : (a ∣ b),
-      dvd.elim H
-        (take c, assume H' : b = a * c,
+            (show a * -c = b, by rewrite [-neg_mul_comm, this])))
+    (suppose a ∣ b,
+      dvd.elim this
+        (take c, suppose b = a * c,
           dvd.intro
-            (show -a * -c = b, by rewrite [neg_mul_neg, H'])))
+            (show -a * -c = b, by rewrite [neg_mul_neg, this])))
 
   theorem dvd_sub (H₁ : (a ∣ b)) (H₂ : (a ∣ c)) : (a ∣ b - c) :=
   dvd_add H₁ (iff.elim_right !dvd_neg_iff_dvd H₂)
@@ -311,56 +311,56 @@ section
   include s
 
   theorem mul_ne_zero {a b : A} (H1 : a ≠ 0) (H2 : b ≠ 0) : a * b ≠ 0 :=
-  assume H : a * b = 0,
-    or.elim (eq_zero_or_eq_zero_of_mul_eq_zero H) (assume H3, H1 H3) (assume H4, H2 H4)
+  suppose a * b = 0,
+    or.elim (eq_zero_or_eq_zero_of_mul_eq_zero this) (assume H3, H1 H3) (assume H4, H2 H4)
 
   theorem eq_of_mul_eq_mul_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
-  have H1  : b * a - c * a = 0, from iff.mp !eq_iff_sub_eq_zero H,
-  have H2 : (b - c) * a = 0, using H1, by rewrite [mul_sub_right_distrib, H1],
-  have H3 : b - c = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
-  iff.elim_right !eq_iff_sub_eq_zero H3
+  have b * a - c * a = 0, from iff.mp !eq_iff_sub_eq_zero H,
+  have (b - c) * a = 0, using this, by rewrite [mul_sub_right_distrib, this],
+  have b - c = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero this) Ha,
+  iff.elim_right !eq_iff_sub_eq_zero this
 
   theorem eq_of_mul_eq_mul_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
-  have H1 : a * b - a * c = 0, from iff.mp !eq_iff_sub_eq_zero H,
-  have H2 : a * (b - c) = 0, using H1, by rewrite [mul_sub_left_distrib, H1],
-  have H3 : b - c = 0, from or_resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
-  iff.elim_right !eq_iff_sub_eq_zero H3
+  have a * b - a * c = 0, from iff.mp !eq_iff_sub_eq_zero H,
+  have a * (b - c) = 0, using this, by rewrite [mul_sub_left_distrib, this],
+  have b - c = 0, from or_resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero this) Ha,
+  iff.elim_right !eq_iff_sub_eq_zero this
 
   -- TODO: do we want the iff versions?
 
   theorem mul_self_eq_mul_self_iff (a b : A) : a * a = b * b ↔ a = b ∨ a = -b :=
   iff.intro
-    (λ H : a * a = b * b,
-      have aux₁ : (a - b) * (a + b) = 0,
-        by rewrite [mul.comm, -mul_self_sub_mul_self_eq, H, sub_self],
-      assert aux₂ : a - b = 0 ∨ a + b = 0, from !eq_zero_or_eq_zero_of_mul_eq_zero aux₁,
-      or.elim aux₂
-        (λ H : a - b = 0, or.inl (eq_of_sub_eq_zero H))
-        (λ H : a + b = 0, or.inr (eq_neg_of_add_eq_zero H)))
-    (λ H : a = b ∨ a = -b, or.elim H
-      (λ a_eq_b,  by rewrite a_eq_b)
-      (λ a_eq_mb, by rewrite [a_eq_mb, neg_mul_neg]))
+    (suppose a * a = b * b,
+      have (a - b) * (a + b) = 0,
+        by rewrite [mul.comm, -mul_self_sub_mul_self_eq, this, sub_self],
+      assert a - b = 0 ∨ a + b = 0, from !eq_zero_or_eq_zero_of_mul_eq_zero this,
+      or.elim this
+        (suppose a - b = 0, or.inl (eq_of_sub_eq_zero this))
+        (suppose a + b = 0, or.inr (eq_neg_of_add_eq_zero this)))
+    (suppose a = b ∨ a = -b, or.elim this
+      (suppose a = b,  by rewrite this)
+      (suppose a = -b, by rewrite [this, neg_mul_neg]))
 
   theorem mul_self_eq_one_iff (a : A) : a * a = 1 ↔ a = 1 ∨ a = -1 :=
-  assert aux : a * a = 1 * 1 ↔ a = 1 ∨ a = -1, from mul_self_eq_mul_self_iff a 1,
-  by rewrite mul_one at aux; exact aux
+  assert a * a = 1 * 1 ↔ a = 1 ∨ a = -1, from mul_self_eq_mul_self_iff a 1,
+  by rewrite mul_one at this; exact this
 
   -- TODO: c - b * c → c = 0 ∨ b = 1 and variants
 
   theorem dvd_of_mul_dvd_mul_left {a b c : A} (Ha : a ≠ 0) (Hdvd : (a * b ∣ a * c)) : (b ∣ c) :=
   dvd.elim Hdvd
     (take d,
-      assume H : a * c = a * b * d,
-      have H1 : b * d = c, from eq_of_mul_eq_mul_left Ha (mul.assoc a b d ▸ H⁻¹),
-      dvd.intro H1)
+      suppose a * c = a * b * d,
+      have b * d = c, from eq_of_mul_eq_mul_left Ha (mul.assoc a b d ▸ this⁻¹),
+      dvd.intro this)
 
   theorem dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : (b * a ∣ c * a)) : (b ∣ c) :=
   dvd.elim Hdvd
     (take d,
-      assume H : c * a = b * a * d,
-      have H1 : b * d * a = c * a, from by rewrite [mul.right_comm, -H],
-      have H2 : b * d = c, from eq_of_mul_eq_mul_right Ha H1,
-      dvd.intro H2)
+      suppose c * a = b * a * d,
+      have b * d * a = c * a, from by rewrite [mul.right_comm, -this],
+      have b * d = c, from eq_of_mul_eq_mul_right Ha this,
+      dvd.intro this)
 end
 
 end algebra
diff --git a/library/data/bool.lean b/library/data/bool.lean
index 65a43a79f..6f2b434c9 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -59,10 +59,11 @@ namespace bool
 
   theorem or_of_bor_eq {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
   bool.rec_on a
-    (assume H : ff || b = tt,
-      have Hb : b = tt, from !ff_bor ▸ H,
-      or.inr Hb)
-    (assume H, or.inl rfl)
+    (suppose ff || b = tt,
+      have b = tt, from !ff_bor ▸ this,
+      or.inr this)
+    (suppose tt || b = tt,
+      or.inl rfl)
 
   theorem bor_inl {a b : bool} (H : a = tt) : a || b = tt :=
   by rewrite H
@@ -98,13 +99,13 @@ namespace bool
 
   theorem band_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
   or.elim (dichotomy a)
-    (assume H0 : a = ff,
+    (suppose a = ff,
       absurd
         (calc ff = ff && b : ff_band
-             ... = a && b  : H0
+             ... = a && b  : this
              ... = tt      : H)
         ff_ne_tt)
-    (assume H1 : a = tt, H1)
+    (suppose a = tt, this)
 
   theorem band_intro {a b : bool} (H₁ : a = tt) (H₂ : b = tt) : a && b = tt :=
   by rewrite [H₁, H₂]
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index b9da0a1b5..edf7015c0 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -149,8 +149,8 @@ theorem nat_abs_of_nat (n : ℕ) : nat_abs (of_nat n) = n := rfl
 
 theorem nat_abs_eq_zero {a : ℤ} : nat_abs a = 0 → a = 0 :=
 int.cases_on a
-  (take m, assume H : nat_abs (of_nat m) = 0, congr_arg of_nat H)
-  (take m', assume H : nat_abs (neg_succ_of_nat m') = 0, absurd H (succ_ne_zero _))
+  (take m,  suppose nat_abs (of_nat m) = 0, congr_arg of_nat this)
+  (take m', suppose nat_abs (neg_succ_of_nat m') = 0, absurd this (succ_ne_zero _))
 
 /- int is a quotient of ordered pairs of natural numbers -/
 
@@ -182,12 +182,12 @@ is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans
 protected theorem equiv_cases {p q : ℕ × ℕ} (H : int.equiv p q) :
     (pr1 p ≥ pr2 p ∧ pr1 q ≥ pr2 q) ∨ (pr1 p < pr2 p ∧ pr1 q < pr2 q) :=
 or.elim (@le_or_gt (pr2 p) (pr1 p))
-  (assume H1: pr1 p ≥ pr2 p,
-    have H2 : pr2 p + pr1 q ≥ pr2 p + pr2 q, from H ▸ add_le_add_right H1 (pr2 q),
-    or.inl (and.intro H1 (le_of_add_le_add_left H2)))
-  (assume H1: pr1 p < pr2 p,
-    have H2 : pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right H1 (pr2 q),
-    or.inr (and.intro H1 (lt_of_add_lt_add_left H2)))
+  (suppose pr1 p ≥ pr2 p,
+    have pr2 p + pr1 q ≥ pr2 p + pr2 q, from H ▸ add_le_add_right this (pr2 q),
+    or.inl (and.intro `pr1 p ≥ pr2 p` (le_of_add_le_add_left this)))
+  (suppose pr1 p < pr2 p,
+    have pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right this (pr2 q),
+    or.inr (and.intro `pr1 p < pr2 p` (lt_of_add_lt_add_left this)))
 
 protected theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv.refl
 
@@ -209,15 +209,15 @@ int.cases_on a (take m, (sub_nat_nat_of_ge (zero_le m))) (take m, rfl)
 
 theorem repr_sub_nat_nat (m n : ℕ) : repr (sub_nat_nat m n) ≡ (m, n) :=
 or.elim (@le_or_gt n m)
-  (take H : m ≥ n,
-    have H1 : repr (sub_nat_nat m n) = (m - n, 0), from sub_nat_nat_of_ge H ▸ rfl,
-    H1⁻¹ ▸
+  (suppose m ≥ n,
+    have repr (sub_nat_nat m n) = (m - n, 0), from sub_nat_nat_of_ge this ▸ rfl,
+    this⁻¹ ▸
       (calc
-        m - n + n = m : sub_add_cancel H
+        m - n + n = m : sub_add_cancel `m ≥ n`
           ... = 0 + m : zero_add))
-  (take H : m < n,
-    have H1 : repr (sub_nat_nat m n) = (0, succ (pred (n - m))), from sub_nat_nat_of_lt H ▸ rfl,
-    H1⁻¹ ▸
+  (suppose H : m < n,
+    have repr (sub_nat_nat m n) = (0, succ (pred (n - m))), from sub_nat_nat_of_lt H ▸ rfl,
+    this⁻¹ ▸
       (calc
         0 + n = n : zero_add
           ... = n - m + m : sub_add_cancel (le_of_lt H)
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index 0ce97ca31..e63f469b1 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -66,11 +66,11 @@ calc
       ... ≤ 0           : neg_nonpos_of_nonneg (div_nonneg Ha (neg_nonneg_of_nonpos Hb))
 
 theorem div_neg' {a b : ℤ} (Ha : a < 0) (Hb : b > 0) : a div b < 0 :=
-have H1 : -a - 1 ≥ 0, from le_sub_one_of_lt (neg_pos_of_neg Ha),
-have H2 : (-a - 1) div b + 1 > 0, from lt_add_one_of_le (div_nonneg H1 (le_of_lt Hb)),
+have -a - 1 ≥ 0, from le_sub_one_of_lt (neg_pos_of_neg Ha),
+have (-a - 1) div b + 1 > 0, from lt_add_one_of_le (div_nonneg this (le_of_lt Hb)),
 calc
   a div b = -((-a - 1) div b + 1) : div_of_neg_of_pos Ha Hb
-      ... < 0                     : neg_neg_of_pos H2
+      ... < 0                     : neg_neg_of_pos this
 
 set_option pp.coercions true
 
@@ -84,10 +84,10 @@ theorem div_zero (a : ℤ) : a div 0 = 0 :=
 by rewrite [↑divide, sign_zero, zero_mul]
 
 theorem div_one (a : ℤ) :a div 1 = a :=
-assert H : 1 > 0, from dec_trivial,
+assert 1 > 0, from dec_trivial,
 int.cases_on a
   (take m, by rewrite [-of_nat_div, nat.div_one])
-  (take m, by rewrite [!neg_succ_of_nat_div H, -of_nat_div, nat.div_one])
+  (take m, by rewrite [!neg_succ_of_nat_div this, -of_nat_div, nat.div_one])
 
 theorem eq_div_mul_add_mod (a b : ℤ) : a = a div b * b + a mod b :=
 !add.comm ▸ eq_add_of_sub_eq rfl
@@ -107,20 +107,20 @@ int.cases_on a
         absurd H H1))
   (take m,
     assume H : 0 ≤ -[1+m],
-    have H1 : ¬ (0 ≤ -[1+m]), from dec_trivial,
-    absurd H H1)
+    have ¬ (0 ≤ -[1+m]), from dec_trivial,
+    absurd H this)
 
 theorem div_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < abs b) : a div b = 0 :=
 lt.by_cases
-  (assume H : b < 0,
-    assert H3 : a < -b, from abs_of_neg H ▸ H2,
+  (suppose b < 0,
+    assert a < -b, from abs_of_neg this ▸ H2,
     calc
       a div b = - (a div -b) : by rewrite [div_neg, neg_neg]
-          ... = 0            : by rewrite [div_eq_zero_of_lt H1 H3, neg_zero])
-  (assume H : b = 0, H⁻¹ ▸ !div_zero)
-  (assume H : b > 0,
-    have H3 : a < b, from abs_of_pos H ▸ H2,
-    div_eq_zero_of_lt H1 H3)
+          ... = 0            : by rewrite [div_eq_zero_of_lt H1 this, neg_zero])
+  (suppose b = 0, this⁻¹ ▸ !div_zero)
+  (suppose b > 0,
+    have a < b, from abs_of_pos this ▸ H2,
+    div_eq_zero_of_lt H1 this)
 
 private theorem add_mul_div_self_aux1 {a : ℤ} {k : ℕ} (n : ℕ)
     (H1 : a ≥ 0) (H2 : #nat k > 0) :
diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean
index 22527bee7..e9ae3449f 100644
--- a/library/data/int/gcd.lean
+++ b/library/data/int/gcd.lean
@@ -42,12 +42,12 @@ theorem gcd_abs_abs (a b : ℤ) : gcd (abs a) (abs b) = gcd a b :=
 by rewrite [↑gcd, *nat_abs_abs]
 
 theorem gcd_of_ne_zero (a : ℤ) {b : ℤ} (H : b ≠ 0) : gcd a b = gcd b (abs a mod abs b) :=
-have H1 : nat_abs b ≠ nat.zero, from assume H', H (nat_abs_eq_zero H'),
-have H2 : (#nat nat_abs b > nat.zero), from nat.pos_of_ne_zero H1,
-assert H3 : nat.gcd (nat_abs a) (nat_abs b) = (#nat nat.gcd (nat_abs b) (nat_abs a mod nat_abs b)),
-  from @nat.gcd_of_pos (nat_abs a) (nat_abs b) H2,
+have nat_abs b ≠ nat.zero,        from assume H', H (nat_abs_eq_zero H'),
+have (#nat nat_abs b > nat.zero), from nat.pos_of_ne_zero this,
+assert nat.gcd (nat_abs a) (nat_abs b) = (#nat nat.gcd (nat_abs b) (nat_abs a mod nat_abs b)),
+  from @nat.gcd_of_pos (nat_abs a) (nat_abs b) this,
 calc
- gcd a b = nat.gcd (nat_abs b) (#nat nat_abs a mod nat_abs b) : by rewrite [↑gcd, H3]
+ gcd a b = nat.gcd (nat_abs b) (#nat nat_abs a mod nat_abs b) : by rewrite [↑gcd, this]
      ... = gcd (abs b) (abs a mod abs b)                      :
                by rewrite [↑gcd, -*of_nat_nat_abs, of_nat_mod]
      ... = gcd b (abs a mod abs b)                            : by rewrite [↑gcd, *nat_abs_abs]
@@ -62,9 +62,9 @@ theorem gcd_self (a : ℤ) : gcd a a = abs a :=
 by rewrite [↑gcd, nat.gcd_self, of_nat_nat_abs]
 
 theorem gcd_dvd_left (a b : ℤ) : gcd a b ∣ a :=
-have H : gcd a b ∣ abs a,
+have gcd a b ∣ abs a,
   by rewrite [↑gcd, -of_nat_nat_abs, of_nat_dvd_of_nat]; apply nat.gcd_dvd_left,
-iff.mp !dvd_abs_iff H
+iff.mp !dvd_abs_iff this
 
 theorem gcd_dvd_right (a b : ℤ) : gcd a b ∣ b :=
 by rewrite gcd.comm; apply gcd_dvd_left
@@ -92,20 +92,20 @@ theorem gcd_mul_right (a b c : ℤ) : gcd (a * b) (c * b) = gcd a c * abs b :=
 by rewrite [mul.comm a, mul.comm c, mul.comm (gcd a c), gcd_mul_left]
 
 theorem gcd_pos_of_ne_zero_left {a : ℤ} (b : ℤ) (H : a ≠ 0) : gcd a b > 0 :=
-have H1 : gcd a b ≠ 0, from
-  assume H2 : gcd a b = 0,
-  have H3: 0 ∣ a, from H2 ▸ gcd_dvd_left a b,
-  show false, from H (eq_zero_of_zero_dvd H3),
-lt_of_le_of_ne (gcd_nonneg a b) (ne.symm H1)
+have gcd a b ≠ 0, from
+  suppose gcd a b = 0,
+  have 0 ∣ a,    from this ▸ gcd_dvd_left a b,
+  show false,    from H (eq_zero_of_zero_dvd this),
+lt_of_le_of_ne (gcd_nonneg a b) (ne.symm this)
 
 theorem gcd_pos_of_ne_zero_right (a : ℤ) {b : ℤ} (H : b ≠ 0) : gcd a b > 0 :=
 by rewrite gcd.comm; apply !gcd_pos_of_ne_zero_left H
 
 theorem eq_zero_of_gcd_eq_zero_left {a b : ℤ} (H : gcd a b = 0) : a = 0 :=
 decidable.by_contradiction
-  (assume H1 : a ≠ 0,
-    have H2 : gcd a b > 0, from !gcd_pos_of_ne_zero_left H1,
-    ne_of_lt H2 H⁻¹)
+  (suppose a ≠ 0,
+    have gcd a b > 0, from !gcd_pos_of_ne_zero_left this,
+    ne_of_lt this H⁻¹)
 
 theorem eq_zero_of_gcd_eq_zero_right {a b : ℤ} (H : gcd a b = 0) : b = 0 :=
 by rewrite gcd.comm at H; apply !eq_zero_of_gcd_eq_zero_left H
@@ -113,15 +113,15 @@ by rewrite gcd.comm at H; apply !eq_zero_of_gcd_eq_zero_left H
 theorem gcd_div {a b c : ℤ} (H1 : c ∣ a) (H2 : c ∣ b) :
   gcd (a div c) (b div c) = gcd a b div (abs c) :=
 decidable.by_cases
-  (assume H3 : c = 0,
+  (suppose c = 0,
     calc
       gcd (a div c) (b div c) = gcd 0 0             : by subst c; rewrite *div_zero
                           ... = 0                   : gcd_zero_left
                           ... = gcd a b div 0       : div_zero
                           ... = gcd a b div (abs c) : by subst c)
-  (assume H3 : c ≠ 0,
-    have H4 : abs c ≠ 0, from assume H', H3 (eq_zero_of_abs_eq_zero H'),
-    eq.symm (div_eq_of_eq_mul_left H4
+  (suppose c ≠ 0,
+    have abs c ≠ 0, from assume H', this (eq_zero_of_abs_eq_zero H'),
+    eq.symm (div_eq_of_eq_mul_left this
       (eq.symm (calc
         gcd (a div c) (b div c) * abs c = gcd (a div c * c) (b div c * c) : gcd_mul_right
                                 ... = gcd a (b div c * c)                 : div_mul_cancel H1
@@ -314,25 +314,25 @@ coprime_of_coprime_mul_left_right (!mul.comm ▸ H)
 theorem exists_eq_prod_and_dvd_and_dvd {a b c} (H : c ∣ a * b) :
   ∃ a' b', c = a' * b' ∧ a' ∣ a ∧ b' ∣ b :=
 decidable.by_cases
- (assume H1 : gcd c a = 0,
-    have H2 : c = 0, from eq_zero_of_gcd_eq_zero_left H1,
-    have H3 : a = 0, from eq_zero_of_gcd_eq_zero_right H1,
-    have H4 : c = 0 * b, from H2 ⬝ !zero_mul⁻¹,
-    have H5 : 0 ∣ a, from H3⁻¹ ▸ !dvd.refl,
-    have H6 : b ∣ b, from !dvd.refl,
-    exists.intro _ (exists.intro _ (and.intro H4 (and.intro H5 H6))))
-  (assume H1 : gcd c a ≠ 0,
-    have H2 : gcd c a ∣ c, from !gcd_dvd_left,
-    have H3 : c div gcd c a ∣ (a * b) div gcd c a, from div_dvd_div H2 H,
+ (suppose gcd c a = 0,
+    have c = 0, from eq_zero_of_gcd_eq_zero_left `gcd c a = 0`,
+    have a = 0, from eq_zero_of_gcd_eq_zero_right `gcd c a = 0`,
+    have c = 0 * b, from `c = 0` ⬝ !zero_mul⁻¹,
+    have 0 ∣ a, from `a = 0`⁻¹ ▸ !dvd.refl,
+    have b ∣ b, from !dvd.refl,
+    exists.intro _ (exists.intro _ (and.intro `c = 0 * b` (and.intro `0 ∣ a` `b ∣ b`))))
+  (suppose gcd c a ≠ 0,
+    have gcd c a ∣ c, from !gcd_dvd_left,
+    have H3 : c div gcd c a ∣ (a * b) div gcd c a, from div_dvd_div this H,
     have H4 : (a * b) div gcd c a = (a div gcd c a) * b, from
       calc
         a * b div gcd c a = b * a div gcd c a   : mul.comm
                       ... = b * (a div gcd c a) : !mul_div_assoc !gcd_dvd_right
                       ... = a div gcd c a * b   : mul.comm,
     have H5 : c div gcd c a ∣ (a div gcd c a) * b, from H4 ▸ H3,
-    have H6 : coprime (c div gcd c a) (a div gcd c a), from coprime_div_gcd_div_gcd H1,
+    have H6 : coprime (c div gcd c a) (a div gcd c a), from coprime_div_gcd_div_gcd `gcd c a ≠ 0`,
     have H7 : c div gcd c a ∣ b, from dvd_of_coprime_of_dvd_mul_left H6 H5,
-    have H8 : c = gcd c a * (c div gcd c a), from (mul_div_cancel' H2)⁻¹,
+    have H8 : c = gcd c a * (c div gcd c a), from (mul_div_cancel' `gcd c a ∣ c`)⁻¹,
     exists.intro _ (exists.intro _ (and.intro H8 (and.intro !gcd_dvd_right H7))))
 
 end int
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 1f82124cb..188cc3436 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -34,9 +34,9 @@ private theorem nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) :=
 int.cases_on a (take n, or.inl trivial) (take n, or.inr trivial)
 
 theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
-have H1 : b - a = n, from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹,
-have H2 : nonneg n, from true.intro,
-show nonneg (b - a), from H1⁻¹ ▸ H2
+have b - a = n,      from (eq_add_neg_of_add_eq (!add.comm ▸ H))⁻¹,
+have nonneg n,       from true.intro,
+show nonneg (b - a), from `b - a = n`⁻¹ ▸ this
 
 theorem le.elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
 obtain (n : ℕ) (H1 : b - a = n), from nonneg.elim H,
@@ -46,9 +46,9 @@ theorem le.total (a b : ℤ) : a ≤ b ∨ b ≤ a :=
 or.elim (nonneg_or_nonneg_neg (b - a))
   (assume H, or.inl H)
   (assume H : nonneg (-(b - a)),
-    have H0 : -(b - a) = a - b, from neg_sub b a,
-    have H1 : nonneg (a - b), from H0 ▸ H,    -- too bad: can't do it in one step
-    or.inr H1)
+    have -(b - a) = a - b, from neg_sub b a,
+    have nonneg (a - b), from this ▸ H,
+    or.inr this)
 
 theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : #nat m ≤ n) : of_nat m ≤ of_nat n :=
 obtain (k : ℕ) (Hk : m + k = n), from nat.le.elim H,
@@ -56,8 +56,8 @@ le.intro (Hk ▸ (of_nat_add m k)⁻¹)
 
 theorem le_of_of_nat_le_of_nat {m n : ℕ} (H : of_nat m ≤ of_nat n) : (#nat m ≤ n) :=
 obtain (k : ℕ) (Hk : of_nat m + of_nat k = of_nat n), from le.elim H,
-have H1 : m + k = n, from of_nat.inj (of_nat_add m k ⬝ Hk),
-nat.le.intro H1
+have m + k = n, from of_nat.inj (of_nat_add m k ⬝ Hk),
+nat.le.intro this
 
 theorem of_nat_le_of_nat (m n : ℕ) : of_nat m ≤ of_nat n ↔ m ≤ n :=
 iff.intro le_of_of_nat_le_of_nat of_nat_le_of_nat_of_le
@@ -74,11 +74,11 @@ H ▸ lt_add_succ a n
 
 theorem lt.elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b :=
 obtain (n : ℕ) (Hn : a + 1 + n = b), from le.elim H,
-have H2 : a + succ n = b, from
+have a + succ n = b, from
   calc
     a + succ n = a + 1 + n : by simp
       ... = b : Hn,
-exists.intro n H2
+exists.intro n this
 
 theorem of_nat_lt_of_nat (n m : ℕ) : of_nat n < of_nat m ↔ n < m :=
 calc
@@ -101,47 +101,47 @@ le.intro (add_zero a)
 theorem le.trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c :=
 obtain (n : ℕ) (Hn : a + n = b), from le.elim H1,
 obtain (m : ℕ) (Hm : b + m = c), from le.elim H2,
-have H3 : a + of_nat (n + m) = c, from
+have a + of_nat (n + m) = c, from
   calc
     a + of_nat (n + m) = a + (of_nat n + m) : {of_nat_add n m}
       ... = a + n + m : (add.assoc a n m)⁻¹
       ... = b + m : {Hn}
       ... = c : Hm,
-le.intro H3
+le.intro this
 
 theorem le.antisymm : ∀ {a b : ℤ}, a ≤ b → b ≤ a → a = b :=
 take a b : ℤ, assume (H₁ : a ≤ b) (H₂ : b ≤ a),
 obtain (n : ℕ) (Hn : a + n = b), from le.elim H₁,
 obtain (m : ℕ) (Hm : b + m = a), from le.elim H₂,
-have H₃ : a + of_nat (n + m) = a + 0, from
+have a + of_nat (n + m) = a + 0, from
   calc
     a + of_nat (n + m) = a + (of_nat n + m) : of_nat_add
       ... = a + n + m                       : add.assoc
       ... = b + m                           : Hn
       ... = a                               : Hm
       ... = a + 0                           : add_zero,
-have H₄ : of_nat (n + m) = of_nat 0, from add.left_cancel H₃,
-have H₅ : n + m = 0, from of_nat.inj H₄,
-have H₆ : n = 0, from nat.eq_zero_of_add_eq_zero_right H₅,
+have of_nat (n + m) = of_nat 0, from add.left_cancel this,
+have n + m = 0,                 from of_nat.inj this,
+have n = 0,                     from nat.eq_zero_of_add_eq_zero_right this,
 show a = b, from
   calc
     a = a + 0        : add_zero
-      ... = a + n    : H₆
+      ... = a + n    : this
       ... = b        : Hn
 
 theorem lt.irrefl (a : ℤ) : ¬ a < a :=
-(assume H : a < a,
-  obtain (n : ℕ) (Hn : a + succ n = a), from lt.elim H,
-  have H2 : a + succ n = a + 0, from
+(suppose a < a,
+  obtain (n : ℕ) (Hn : a + succ n = a), from lt.elim this,
+  have a + succ n = a + 0, from
     calc
       a + succ n = a : Hn
         ... = a + 0 : by simp,
-  have H3 : nat.succ n = 0, from add.left_cancel H2,
-  have H4 : nat.succ n = 0, from of_nat.inj H3,
-  absurd H4 !succ_ne_zero)
+  have nat.succ n = 0, from add.left_cancel this,
+  have nat.succ n = 0, from of_nat.inj this,
+  absurd this !succ_ne_zero)
 
 theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b :=
-(assume H2 : a = b, absurd (H2 ▸ H) (lt.irrefl b))
+(suppose a = b, absurd (this ▸ H) (lt.irrefl b))
 
 theorem le_of_lt {a b : ℤ} (H : a < b) : a ≤ b :=
 obtain (n : ℕ) (Hn : a + succ n = b), from lt.elim H,
@@ -151,22 +151,22 @@ theorem lt_iff_le_and_ne (a b : ℤ) : a < b ↔ (a ≤ b ∧ a ≠ b) :=
 iff.intro
   (assume H, and.intro (le_of_lt H) (ne_of_lt H))
   (assume H,
-    have H1 : a ≤ b, from and.elim_left H,
-    have H2 : a ≠ b, from and.elim_right H,
-    obtain (n : ℕ) (Hn : a + n = b), from le.elim H1,
-    have H3 : n ≠ 0, from (assume H' : n = 0, H2 (!add_zero ▸ H' ▸ Hn)),
-    obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero H3,
+    have a ≤ b, from and.elim_left H,
+    have a ≠ b, from and.elim_right H,
+    obtain (n : ℕ) (Hn : a + n = b), from le.elim `a ≤ b`,
+    have n ≠ 0, from (assume H' : n = 0, `a ≠ b` (!add_zero ▸ H' ▸ Hn)),
+    obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero this,
     lt.intro (Hk ▸ Hn))
 
 theorem le_iff_lt_or_eq (a b : ℤ) : a ≤ b ↔ (a < b ∨ a = b) :=
 iff.intro
   (assume H,
     by_cases
-      (assume H1 : a = b, or.inr H1)
-      (assume H1 : a ≠ b,
+      (suppose a = b, or.inr this)
+      (suppose a ≠ b,
         obtain (n : ℕ) (Hn : a + n = b), from le.elim H,
-        have H2 : n ≠ 0, from (assume H' : n = 0, H1 (!add_zero ▸ H' ▸ Hn)),
-        obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero H2,
+        have n ≠ 0, from (assume H' : n = 0, `a ≠ b` (!add_zero ▸ H' ▸ Hn)),
+        obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero this,
         or.inl (lt.intro (Hk ▸ Hn))))
   (assume H,
     or.elim H
@@ -208,8 +208,8 @@ obtain (m : ℕ) (Hm : 0 + nat.succ m = b), from lt.elim Hb,
 lt.intro
   (eq.symm
     (calc
-      a * b = (0 + nat.succ n) * b                 : Hn
-        ... = nat.succ n * b                       : nat.zero_add
+      a * b = (0 + nat.succ n) * b                     : Hn
+        ... = nat.succ n * b                           : nat.zero_add
         ... = nat.succ n * (0 + nat.succ m)            : {Hm⁻¹}
         ... = nat.succ n * nat.succ m                  : nat.zero_add
         ... = of_nat (nat.succ n * nat.succ m)         : of_nat_mul
@@ -308,8 +308,8 @@ obtain (n : ℕ) (H1 : 0 + of_nat n = a), from le.elim H,
 exists.intro n (!zero_add ▸ (H1⁻¹))
 
 theorem exists_eq_neg_of_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -(of_nat n) :=
-have H2 : -a ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos H,
-obtain (n : ℕ) (Hn : -a = of_nat n), from exists_eq_of_nat H2,
+have -a ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos H,
+obtain (n : ℕ) (Hn : -a = of_nat n), from exists_eq_of_nat this,
 exists.intro n (eq_neg_of_eq_neg (Hn⁻¹))
 
 theorem of_nat_nat_abs_of_nonneg {a : ℤ} (H : a ≥ 0) : of_nat (nat_abs a) = a :=
@@ -317,10 +317,10 @@ obtain (n : ℕ) (Hn : a = of_nat n), from exists_eq_of_nat H,
 Hn⁻¹ ▸ congr_arg of_nat (nat_abs_of_nat n)
 
 theorem of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) : of_nat (nat_abs a) = -a :=
-have H1 : (-a) ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos H,
+have -a ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos H,
 calc
   of_nat (nat_abs a) = of_nat (nat_abs (-a)) : nat_abs_neg
-                 ... = -a                    : of_nat_nat_abs_of_nonneg H1
+                 ... = -a                    : of_nat_nat_abs_of_nonneg this
 
 theorem of_nat_nat_abs (b : ℤ) : nat_abs b = abs b :=
 or.elim (le.total 0 b)
@@ -332,13 +332,13 @@ abs.by_cases rfl !nat_abs_neg
 
 theorem lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) : a < b :=
 obtain n (H1 : a + 1 + n = b), from le.elim H,
-have H2 : a + succ n = b, by rewrite [-H1, add.assoc, add.comm 1],
-lt.intro H2
+have a + succ n = b, by rewrite [-H1, add.assoc, add.comm 1],
+lt.intro this
 
 theorem add_one_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b :=
 obtain n (H1 : a + succ n = b), from lt.elim H,
-have H2 : a + 1 + n = b, by rewrite [-H1, add.assoc, add.comm 1],
-le.intro H2
+have a + 1 + n = b, by rewrite [-H1, add.assoc, add.comm 1],
+le.intro this
 
 theorem lt_add_one_of_le {a b : ℤ} (H : a ≤ b) : a < b + 1 :=
 lt_add_of_le_of_pos H trivial
@@ -368,17 +368,17 @@ int.cases_on a
   (take m H, exists.intro m rfl)
 
 theorem eq_one_of_mul_eq_one_right {a b : ℤ} (H : a ≥ 0) (H' : a * b = 1) : a = 1 :=
-have H2 : a * b > 0, by rewrite H'; apply trivial,
-have H3 : b > 0, from pos_of_mul_pos_left H2 H,
-have H4 : a > 0, from pos_of_mul_pos_right H2 (le_of_lt H3),
+have a * b > 0, by rewrite H'; apply trivial,
+have b > 0, from pos_of_mul_pos_left this H,
+have a > 0, from pos_of_mul_pos_right `a * b > 0` (le_of_lt `b > 0`),
 or.elim (le_or_gt a 1)
-  (assume H5 : a ≤ 1,
-    show a = 1, from le.antisymm H5 (add_one_le_of_lt H4))
-  (assume H5 : a > 1,
-    assert H6 : a * b ≥ 2 * 1,
-      from mul_le_mul (add_one_le_of_lt H5) (add_one_le_of_lt H3) trivial H,
-    have H7 : false, by rewrite [H' at H6]; apply H6,
-    false.elim H7)
+  (suppose a ≤ 1,
+    show a = 1, from le.antisymm this (add_one_le_of_lt `a > 0`))
+  (suppose a > 1,
+    assert a * b ≥ 2 * 1,
+      from mul_le_mul (add_one_le_of_lt `a > 1`) (add_one_le_of_lt `b > 0`) trivial H,
+    have false, by rewrite [H' at this]; exact this,
+    false.elim this)
 
 theorem eq_one_of_mul_eq_one_left {a b : ℤ} (H : b ≥ 0) (H' : a * b = 1) : b = 1 :=
 eq_one_of_mul_eq_one_right H (!mul.comm ▸ H')
@@ -392,7 +392,7 @@ eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H)
 theorem eq_one_of_dvd_one {a : ℤ} (H : a ≥ 0) (H' : a ∣ 1) : a = 1 :=
 dvd.elim H'
   (take b,
-    assume H1 : 1 = a * b,
-    eq_one_of_mul_eq_one_right H H1⁻¹)
+    suppose 1 = a * b,
+    eq_one_of_mul_eq_one_right H this⁻¹)
 
 end int
diff --git a/library/data/nat/choose.lean b/library/data/nat/choose.lean
index e6e8738e8..f1bdc0906 100644
--- a/library/data/nat/choose.lean
+++ b/library/data/nat/choose.lean
@@ -25,8 +25,8 @@ private lemma lbp_zero : lbp 0 :=
 private lemma lbp_succ {x : nat} : lbp x → ¬ p x → lbp (succ x) :=
 λ lx npx y yltsx,
   or.elim (eq_or_lt_of_le (le_of_succ_le_succ yltsx))
-    (λ yeqx, by substvars; assumption)
-    (λ yltx, lx y yltx)
+    (suppose y = x, by substvars; assumption)
+    (suppose y < x, lx y this)
 
 private definition gtb (a b : nat) : Prop :=
 a > b ∧ lbp a
@@ -43,10 +43,10 @@ private lemma acc_of_acc_succ {x : nat} : acc gtb (succ x) → acc gtb x :=
 assume h,
 acc.intro x (λ (y : nat) (l : y ≺ x),
    by_cases
-     (assume yeqx : y = succ x, by substvars; assumption)
-     (assume ynex : y ≠ succ x,
+     (suppose y = succ x, by substvars; assumption)
+     (suppose y ≠ succ x,
         have x < y,      from and.elim_left l,
-        have succ x < y, from lt_of_le_and_ne this (ne.symm ynex),
+        have succ x < y, from lt_of_le_and_ne this (ne.symm `y ≠ succ x`),
         acc.inv h (and.intro this (and.elim_right l))))
 
 private lemma acc_of_px_of_gt {x y : nat} : p x → y > x → acc gtb y :=
@@ -58,10 +58,10 @@ acc.intro y (λ (z : nat) (l : z ≺ y),
 private lemma acc_of_acc_of_lt : ∀ {x y : nat}, acc gtb x → y < x → acc gtb y
 | 0        y a0  ylt0  := absurd ylt0 !not_lt_zero
 | (succ x) y asx yltsx :=
-  assert ax : acc gtb x, from acc_of_acc_succ asx,
+  assert acc gtb x, from acc_of_acc_succ asx,
   by_cases
      (suppose y = x, by substvars; assumption)
-     (suppose y ≠ x, acc_of_acc_of_lt ax (lt_of_le_and_ne (le_of_lt_succ yltsx) this))
+     (suppose y ≠ x, acc_of_acc_of_lt `acc gtb x` (lt_of_le_and_ne (le_of_lt_succ yltsx) this))
 
 parameter (ex : ∃ a, p a)
 parameter [dp : decidable_pred p]
@@ -81,14 +81,14 @@ private definition find.F (x : nat) : (Π x₁, x₁ ≺ x → lbp x₁ → {a :
 match x with
 | 0 := λ f l0, by_cases
   (λ p0 : p 0,    tag 0 p0)
-  (λ np0 : ¬ p 0,
-    have l₁ : lbp 1, from lbp_succ l0 np0,
-    have 1 ≺ 0, from and.intro (lt.base 0) l₁,
-    f 1 this l₁)
+  (suppose ¬ p 0,
+    have lbp 1, from lbp_succ l0 this,
+    have 1 ≺ 0, from and.intro (lt.base 0) `lbp 1`,
+    f 1 `1 ≺ 0` `lbp 1`)
 | (succ n) := λ f lsn, by_cases
-  (λ psn : p (succ n), tag (succ n) psn)
-  (λ npsn : ¬ p (succ n),
-    have lss : lbp (succ (succ n)), from lbp_succ lsn npsn,
+  (suppose p (succ n), tag (succ n) this)
+  (suppose ¬ p (succ n),
+    have lss : lbp (succ (succ n)), from lbp_succ lsn this,
     have succ (succ n) ≺ succ n, from and.intro (lt.base (succ n)) lss,
     f (succ (succ n)) this lss)
 end
diff --git a/library/data/num.lean b/library/data/num.lean
index 98bb11655..1723b5c62 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -15,12 +15,12 @@ namespace pos_num
   theorem succ_bit0 (a : pos_num) : succ (bit0 a) = bit1 a
 
   theorem ne_of_bit0_ne_bit0 {a b : pos_num} (H₁ : bit0 a ≠ bit0 b) : a ≠ b :=
-  assume H : a = b,
-  absurd rfl (H ▸ H₁)
+  suppose a = b,
+  absurd rfl (this ▸ H₁)
 
   theorem ne_of_bit1_ne_bit1 {a b : pos_num} (H₁ : bit1 a ≠ bit1 b) : a ≠ b :=
-  assume H : a = b,
-  absurd rfl (H ▸ H₁)
+  suppose a = b,
+  absurd rfl (this ▸ H₁)
 
   theorem pred_succ : ∀ (a : pos_num), pred (succ a) = a
   | one      := rfl
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index 409f874de..bb1e584d5 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -29,32 +29,32 @@ theorem equiv.refl [refl] (a : prerat) : a ≡ a := rfl
 theorem equiv.symm [symm] {a b : prerat} (H : a ≡ b) : b ≡ a := !eq.symm H
 
 theorem num_eq_zero_of_equiv {a b : prerat} (H : a ≡ b) (na_zero : num a = 0) : num b = 0 :=
-have H1 : num a * denom b = 0, from !zero_mul ▸ na_zero ▸ rfl,
-have H2 : num b * denom a = 0, from H ▸ H1,
-show num b = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H2) (ne_of_gt (denom_pos a))
+have num a * denom b = 0, from !zero_mul ▸ na_zero ▸ rfl,
+have num b * denom a = 0, from H ▸ this,
+show num b = 0, from or_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero this) (ne_of_gt (denom_pos a))
 
 theorem num_pos_of_equiv {a b : prerat} (H : a ≡ b) (na_pos : num a > 0) : num b > 0 :=
-have H1 : num a * denom b > 0, from mul_pos na_pos (denom_pos b),
-have H2 : num b * denom a > 0, from H ▸ H1,
-show num b > 0, from pos_of_mul_pos_right H2 (le_of_lt (denom_pos a))
+have num a * denom b > 0, from mul_pos na_pos (denom_pos b),
+have num b * denom a > 0, from H ▸ this,
+show num b > 0, from pos_of_mul_pos_right this (le_of_lt (denom_pos a))
 
 theorem num_neg_of_equiv {a b : prerat} (H : a ≡ b) (na_neg : num a < 0) : num b < 0 :=
-have H1 : num a * denom b < 0, from mul_neg_of_neg_of_pos na_neg (denom_pos b),
-have H2 : -(-num b * denom a) < 0, from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_neg⁻¹ ▸ H ▸ H1,
-have H3 : -num b > 0, from pos_of_mul_pos_right (pos_of_neg_neg H2) (le_of_lt (denom_pos a)),
-neg_of_neg_pos H3
+have num a * denom b < 0, from mul_neg_of_neg_of_pos na_neg (denom_pos b),
+have -(-num b * denom a) < 0, from !neg_mul_eq_neg_mul⁻¹ ▸ !neg_neg⁻¹ ▸ H ▸ this,
+have -num b > 0, from pos_of_mul_pos_right (pos_of_neg_neg this) (le_of_lt (denom_pos a)),
+neg_of_neg_pos this
 
 theorem equiv_of_num_eq_zero {a b : prerat} (H1 : num a = 0) (H2 : num b = 0) : a ≡ b :=
 by rewrite [↑equiv, H1, H2, *zero_mul]
 
 theorem equiv.trans [trans] {a b c : prerat} (H1 : a ≡ b) (H2 : b ≡ c) : a ≡ c :=
 decidable.by_cases
-  (assume b0 : num b = 0,
-    have a0 : num a = 0, from num_eq_zero_of_equiv (equiv.symm H1) b0,
-    have c0 : num c = 0, from num_eq_zero_of_equiv H2 b0,
-    equiv_of_num_eq_zero a0 c0)
-  (assume bn0 : num b ≠ 0,
-    have H3 : num b * denom b ≠ 0, from mul_ne_zero bn0 (ne_of_gt (denom_pos b)),
+  (suppose num b = 0,
+    have num a = 0, from num_eq_zero_of_equiv (equiv.symm H1) `num b = 0`,
+    have num c = 0, from num_eq_zero_of_equiv H2 `num b = 0`,
+    equiv_of_num_eq_zero `num a = 0` `num c = 0`)
+  (suppose num b ≠ 0,
+    have H3 : num b * denom b ≠ 0, from mul_ne_zero this (ne_of_gt (denom_pos b)),
     have H4 : (num b * denom b) * (num a * denom c) = (num b * denom b) * (num c * denom a),
       from calc
         (num b * denom b) * (num a * denom c) = (num a * denom b) * (num b * denom c) :
@@ -122,17 +122,17 @@ theorem inv_zero' : inv zero = zero := inv_zero (of_nat_succ_pos nat.zero)
 
 theorem inv_of_pos {n d : int} (np : n > 0) (dp : d > 0) : inv (mk n d dp) ≡ mk d n np :=
 obtain (n' : nat) (Hn' : n = of_nat n'), from exists_eq_of_nat (le_of_lt np),
-have H1 : (#nat n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
-obtain (k : nat) (Hk : n' = nat.succ k), from nat.exists_eq_succ_of_lt H1,
-have H2 : d * n = d * nat.succ k, by rewrite [Hn', Hk],
-Hn'⁻¹ ▸ (Hk⁻¹ ▸ H2)
+have (#nat n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
+obtain (k : nat) (Hk : n' = nat.succ k), from nat.exists_eq_succ_of_lt this,
+have d * n = d * nat.succ k, by rewrite [Hn', Hk],
+Hn'⁻¹ ▸ (Hk⁻¹ ▸ this)
 
 theorem inv_neg {n d : int} (np : n > 0) (dp : d > 0) : inv (mk (-n) d dp) ≡ mk (-d) n np :=
 obtain (n' : nat) (Hn' : n = of_nat n'), from exists_eq_of_nat (le_of_lt np),
-have H1 : (#nat n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
-obtain (k : nat) (Hk : n' = nat.succ k), from nat.exists_eq_succ_of_lt H1,
-have H2 : -d * n = -d * nat.succ k, by rewrite [Hn', Hk],
-have H3 : inv (mk -[1+k] d dp) ≡ mk (-d) n np, from H2,
+have (#nat n' > nat.zero), from lt_of_of_nat_lt_of_nat (Hn' ▸ np),
+obtain (k : nat) (Hk : n' = nat.succ k), from nat.exists_eq_succ_of_lt this,
+have -d * n = -d * nat.succ k, by rewrite [Hn', Hk],
+have H3 : inv (mk -[1+k] d dp) ≡ mk (-d) n np, from this,
 have H4 : -[1+k] = -n, from calc
   -[1+k] = -(nat.succ k) : rfl
       ... = -n            : by rewrite [Hk⁻¹, Hn'],
@@ -140,9 +140,9 @@ H4 ▸ H3
 
 theorem inv_of_neg {n d : int} (nn : n < 0) (dp : d > 0) :
   inv (mk n d dp) ≡ mk (-d) (-n) (neg_pos_of_neg nn) :=
-have H : inv (mk (-(-n)) d dp) ≡ mk (-d) (-n) (neg_pos_of_neg nn),
+have inv (mk (-(-n)) d dp) ≡ mk (-d) (-n) (neg_pos_of_neg nn),
   from inv_neg (neg_pos_of_neg nn) dp,
-!neg_neg ▸ H
+!neg_neg ▸ this
 
 /- operations respect equiv -/
 
diff --git a/library/data/stream.lean b/library/data/stream.lean
index 40d07827e..0091bb758 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -650,10 +650,10 @@ lt.by_cases
           exact !he₂ jlti₁
     end)
   (λ i₂lti₁ : i₂ < i₁,
-    assert aux : nth i₂ s₁ = nth i₂ s₂, from he₁ _ i₂lti₁,
+    assert nth i₂ s₁ = nth i₂ s₂, from he₁ _ i₂lti₁,
     begin
       existsi i₂, split,
-       {rewrite aux, exact hlt₂},
+       {rewrite this, exact hlt₂},
        {intro j jlti₂, transitivity nth j s₂,
          exact !he₁ (lt.trans jlti₂ i₂lti₁),
          exact !he₂ jlti₂}
diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean
index d4f993f88..9bc2aaccb 100644
--- a/library/theories/number_theory/prime_factorization.lean
+++ b/library/theories/number_theory/prime_factorization.lean
@@ -30,8 +30,8 @@ definition mult (p n : ℕ) : ℕ := fix (mult.F p) n
 
 theorem mult_rec {p n : ℕ} (pgt1 : p > 1) (ngt0 : n > 0) (pdivn : p ∣ n) :
   mult p n = succ (mult p (n div p)) :=
-have H : (p > 1 ∧ n > 0) ∧ p ∣ n, from and.intro (and.intro pgt1 ngt0) pdivn,
-eq.trans (well_founded.fix_eq (mult.F p) n) (dif_pos H)
+have (p > 1 ∧ n > 0) ∧ p ∣ n, from and.intro (and.intro pgt1 ngt0) pdivn,
+eq.trans (well_founded.fix_eq (mult.F p) n) (dif_pos this)
 
 private theorem mult_base {p n : ℕ} (H : ¬ ((p > 1 ∧ n > 0) ∧ p ∣ n)) :
   mult p n = 0 :=
@@ -57,11 +57,11 @@ by rewrite (mult_rec pgt1 npos pdvdn); apply succ_pos
 
 theorem not_dvd_of_mult_eq_zero {p n : ℕ} (pgt1 : p > 1) (npos : n > 0) (H : mult p n = 0) :
   ¬ p ∣ n :=
-assume pdvdn : p ∣ n,
-ne_of_gt (mult_pos_of_dvd pgt1 npos pdvdn) H
+suppose p ∣ n,
+ne_of_gt (mult_pos_of_dvd pgt1 npos this) H
 
 theorem dvd_of_mult_pos {p n : ℕ} (H : mult p n > 0) : p ∣ n :=
-by_contradiction (assume npdvdn : ¬ p ∣ n, ne_of_gt H (mult_eq_zero_of_not_dvd npdvdn))
+by_contradiction (suppose ¬ p ∣ n, ne_of_gt H (mult_eq_zero_of_not_dvd this))
 
 /- properties of mult -/
 
@@ -76,28 +76,28 @@ begin
     {rewrite [mult_eq_zero_of_not_dvd pndvdn, pow_zero], apply one_dvd},
   show p ^ (mult p n) ∣ n, from dvd.elim pdvdn
     (take n',
-      assume Hn' : n = p * n',
-      have ppos : p > 0, from lt.trans zero_lt_one pgt1,
-      assert ndivpeq : n div p = n', from !div_eq_of_eq_mul_right ppos Hn',
-      assert ndivplt : n' < n,
-        by rewrite -ndivpeq; apply mult_rec_decreasing pgt1 npos,
+      suppose n = p * n',
+      have p > 0, from lt.trans zero_lt_one pgt1,
+      assert n div p = n', from !div_eq_of_eq_mul_right this `n = p * n'`,
+      assert n' < n,
+        by rewrite -this; apply mult_rec_decreasing pgt1 npos,
       begin
-        rewrite [mult_rec pgt1 npos pdvdn, ndivpeq, pow_succ', Hn'],
+        rewrite [mult_rec pgt1 npos pdvdn, `n div p = n'`, pow_succ'], subst n,
         apply mul_dvd_mul !dvd.refl,
-        apply ih _ ndivplt
+        apply ih _ this
       end)
 end
 
 theorem mult_one_right (p : ℕ) : mult p 1 = 0:=
 assert H : p^(mult p 1) = 1, from eq_one_of_dvd_one !pow_mult_dvd,
 or.elim (le_or_gt p 1)
-  (assume H1 : p ≤ 1, by rewrite [!mult_eq_zero_of_le_one H1])
-  (assume H1 : p > 1,
+  (suppose p ≤ 1, by rewrite [!mult_eq_zero_of_le_one this])
+  (suppose p > 1,
     by_contradiction
-      assume H2 : mult p 1 ≠ 0,
-      have H3 : mult p 1 > 0, from pos_of_ne_zero H2,
-      assert H4 : p^(mult p 1) > 1, from pow_gt_one H1 H3,
-      show false, by rewrite H at H4; apply !lt.irrefl H4)
+      (suppose mult p 1 ≠ 0,
+       have mult p 1 > 0,       from pos_of_ne_zero this,
+       assert p^(mult p 1) > 1, from pow_gt_one `p > 1` this,
+       show false,              by rewrite H at this; apply !lt.irrefl this))
 
 private theorem mult_pow_mul {p n : ℕ} (i : ℕ) (pgt1 : p > 1) (npos : n > 0) :
   mult p (p^i * n) = i + mult p n :=
@@ -117,31 +117,31 @@ by rewrite [-(mul_one (p^i)), mult_pow_mul i pgt1 zero_lt_one, mult_one_right]
 theorem le_mult {p i n : ℕ} (pgt1 : p > 1) (npos : n > 0) (pidvd : p^i ∣ n) : i ≤ mult p n :=
 dvd.elim pidvd
   (take m,
-    assume neq : n = p^i * m,
-    assert mpos : m > 0, from pos_of_mul_pos_left (neq ▸ npos),
-    by rewrite [neq, mult_pow_mul i pgt1 mpos]; apply le_add_right)
+    suppose n = p^i * m,
+    assert m > 0, from pos_of_mul_pos_left (this ▸ npos),
+    by subst n; rewrite [mult_pow_mul i pgt1 this]; apply le_add_right)
 
 theorem not_dvd_div_pow_mult {p n : ℕ} (pgt1 : p > 1) (npos : n > 0) : ¬ p ∣ n div p^(mult p n) :=
 assume pdvd : p ∣ n div p^(mult p n),
 obtain m (H : n div p^(mult p n) = p * m), from exists_eq_mul_right_of_dvd pdvd,
-assert neq : n = p^(succ (mult p n)) * m, from
+assert n = p^(succ (mult p n)) * m, from
   calc
     n     = p^mult p n * (n div p^mult p n) : by rewrite (mul_div_cancel' !pow_mult_dvd)
       ... = p^(succ (mult p n)) * m         : by rewrite [H, pow_succ, mul.assoc],
-have H1 : p^(succ (mult p n)) ∣ n, by rewrite neq at {2}; apply dvd_mul_right,
-have H2 : succ (mult p n) ≤ mult p n, from le_mult pgt1 npos H1,
-show false, from !not_succ_le_self H2
+have p^(succ (mult p n)) ∣ n,    by rewrite this at {2}; apply dvd_mul_right,
+have succ (mult p n) ≤ mult p n, from le_mult pgt1 npos this,
+show false,                      from !not_succ_le_self this
 
 theorem mult_mul {p m n : ℕ} (primep : prime p) (mpos : m > 0) (npos : n > 0) :
   mult p (m * n) = mult p m + mult p n :=
 let m' := m div p^mult p m, n' := n div p^mult p n in
-assert pgt1 : p > 1, from gt_one_of_prime primep,
+assert p > 1, from gt_one_of_prime primep,
 assert meq : m = p^mult p m * m', by rewrite (mul_div_cancel' !pow_mult_dvd),
 assert neq : n = p^mult p n * n', by rewrite (mul_div_cancel' !pow_mult_dvd),
 have m'pos : m' > 0, from pos_of_mul_pos_left (meq ▸ mpos),
 have n'pos : n' > 0, from pos_of_mul_pos_left (neq ▸ npos),
-have npdvdm' : ¬ p ∣ m', from !not_dvd_div_pow_mult pgt1 mpos,
-have npdvdn' : ¬ p ∣ n', from !not_dvd_div_pow_mult pgt1 npos,
+have npdvdm' : ¬ p ∣ m', from !not_dvd_div_pow_mult `p > 1` mpos,
+have npdvdn' : ¬ p ∣ n', from !not_dvd_div_pow_mult `p > 1` npos,
 assert npdvdm'n' : ¬ p ∣ m' * n', from not_dvd_mul_of_prime primep npdvdm' npdvdn',
 assert m'n'pos : m' * n' > 0, from mul_pos m'pos n'pos,
 assert multm'n' : mult p (m' * n') = 0, from mult_eq_zero_of_not_dvd npdvdm'n',
@@ -150,7 +150,7 @@ calc
                      by rewrite [pow_add, mul.right_comm, -mul.assoc, -meq, mul.assoc,
                                  mul.comm (n div _), -neq]
              ... = mult p m + mult p n                          :
-                     by rewrite [!mult_pow_mul pgt1 m'n'pos, multm'n']
+                     by rewrite [!mult_pow_mul `p > 1` m'n'pos, multm'n']
 
 theorem dvd_of_forall_prime_mult_le {m n : ℕ} (mpos : m > 0)
     (H : ∀ {p}, prime p → mult p m ≤ mult p n) :
diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean
index 77bdc10af..d1416373c 100644
--- a/library/theories/number_theory/primes.lean
+++ b/library/theories/number_theory/primes.lean
@@ -66,7 +66,7 @@ assume h d, obtain h₁ h₂, from h, h₂ m d
 lemma gt_one_of_pos_of_prime_dvd {i p : nat} : prime p → 0 < i → i mod p = 0 → 1 < i :=
 assume ipp pos h,
 have p ≥ 2,  from ge_two_of_prime ipp,
-have p ∣ i,   from dvd_of_mod_eq_zero h,
+have p ∣ i,  from dvd_of_mod_eq_zero h,
 have p ≤ i,  from le_of_dvd pos this,
 lt_of_succ_le (le.trans `2 ≤ p` this)
 
@@ -88,14 +88,15 @@ assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime h₁ h₂)
 
 definition sub_dvd_of_not_prime2 {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≥ 2 ∧ m < n} :=
 assume h₁ h₂,
-have n_ne_0 : n ≠ 0, from assume h, begin subst n, exact absurd h₁ dec_trivial end,
+have n ≠ 0, from assume h, begin subst n, exact absurd h₁ dec_trivial end,
 obtain m m_dvd_n m_ne_1 m_ne_n, from sub_dvd_of_not_prime h₁ h₂,
-assert m_ne_0 : m ≠ 0, from assume h, begin subst m, exact absurd (eq_zero_of_zero_dvd m_dvd_n) n_ne_0 end,
+assert m_ne_0 : m ≠ 0, from assume h, begin subst m, exact absurd (eq_zero_of_zero_dvd m_dvd_n) `n ≠ 0` end,
 begin
   existsi m, split, assumption,
   split,
-    {cases m with m, exact absurd rfl m_ne_0, cases m with m, exact absurd rfl m_ne_1, exact succ_le_succ (succ_le_succ (zero_le _))},
-    {have m_le_n : m ≤ n, from le_of_dvd (pos_of_ne_zero n_ne_0) m_dvd_n,
+    {cases m with m, exact absurd rfl m_ne_0,
+    cases m with m, exact absurd rfl m_ne_1, exact succ_le_succ (succ_le_succ (zero_le _))},
+    {have m_le_n : m ≤ n, from le_of_dvd (pos_of_ne_zero `n ≠ 0`) m_dvd_n,
      exact lt_of_le_and_ne m_le_n m_ne_n}
 end
 
@@ -106,14 +107,14 @@ definition sub_prime_and_dvd {n : nat} : n ≥ 2 → {p | prime p ∧ p ∣ n} :
 nat.strong_rec_on n
   (take n,
    assume ih : ∀ m, m < n → m ≥ 2 → {p | prime p ∧ p ∣ m},
-   assume n_ge_2 : n ≥ 2,
+   suppose n ≥ 2,
    by_cases
-    (λ h : prime n, subtype.tag n (and.intro h (dvd.refl n)))
-    (λ h : ¬ prime n,
-      obtain m m_dvd_n m_ge_2 m_lt_n, from sub_dvd_of_not_prime2 n_ge_2 h,
+    (suppose prime n, subtype.tag n (and.intro this (dvd.refl n)))
+    (suppose ¬ prime n,
+      obtain m m_dvd_n m_ge_2 m_lt_n, from sub_dvd_of_not_prime2 `n ≥ 2` this,
       obtain p (hp : prime p) (p_dvd_m : p ∣ m), from ih m m_lt_n m_ge_2,
-      have p_dvd_n : p ∣ n, from dvd.trans p_dvd_m m_dvd_n,
-      subtype.tag p (and.intro hp p_dvd_n)))
+      have p ∣ n, from dvd.trans p_dvd_m m_dvd_n,
+      subtype.tag p (and.intro hp this)))
 
 lemma ex_prime_and_dvd {n : nat} : n ≥ 2 → ∃ p, prime p ∧ p ∣ n :=
 assume h, ex_of_sub (sub_prime_and_dvd h)