diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean
index 2ed44bdd1..8ba0dc43a 100644
--- a/library/data/list/perm.lean
+++ b/library/data/list/perm.lean
@@ -237,17 +237,17 @@ definition decidable_perm_aux : ∀ (n : nat) (l₁ l₂ : list A), length l₁
   by_cases
     (assume xinl₂ : x ∈ l₂,
       let t₂ : list A := erase x l₂ in
-      have len_t₁       : length t₁ = n,                begin injection H₁ with e, exact e end,
-      assert len_t₂_aux : length t₂ = pred (length l₂), from length_erase_of_mem xinl₂,
-      assert len_t₂     : length t₂ = n,                by rewrite [len_t₂_aux, H₂],
-      match decidable_perm_aux n t₁ t₂ len_t₁ len_t₂ with
+      have len_t₁ : length t₁ = n,         begin injection H₁ with e, exact e end,
+      assert length t₂ = pred (length l₂), from length_erase_of_mem xinl₂,
+      assert length t₂ = n,                by rewrite [this, H₂],
+      match decidable_perm_aux n t₁ t₂ len_t₁ this with
       | inl p  := inl (calc
           x::t₁ ~ x::(erase x l₂) : skip x p
            ...  ~ l₂              : perm_erase xinl₂)
       | inr np := inr (λ p : x::t₁ ~ l₂,
-        assert p₁ : erase x (x::t₁) ~ erase x l₂, from erase_perm_erase_of_perm x p,
-        have p₂ : t₁ ~ erase x l₂, by rewrite [erase_cons_head at p₁]; exact p₁,
-        absurd p₂ np)
+        assert erase x (x::t₁) ~ erase x l₂, from erase_perm_erase_of_perm x p,
+        have t₁ ~ erase x l₂, by rewrite [erase_cons_head at this]; exact this,
+        absurd this np)
       end)
     (assume nxinl₂ : x ∉ l₂,
       inr (λ p : x::t₁ ~ l₂, absurd (mem_perm p !mem_cons) nxinl₂))
@@ -450,9 +450,9 @@ perm_induction_on p'
      (r₁ : ∀{a s₁ s₂}, t₁ ≈ a|s₁ → t₂≈a|s₂ → s₁ ~ s₂)
      (r₂ : ∀{a s₁ s₂}, t₂ ≈ a|s₁ → t₃≈a|s₂ → s₁ ~ s₂)
      a s₁ s₂ e₁ e₂,
-    have aint₁ : a ∈ t₁, from mem_head_of_qeq e₁,
-    have aint₂ : a ∈ t₂, from mem_perm p₁ aint₁,
-    obtain (t₂' : list A) (e₂' : t₂≈a|t₂'), from qeq_of_mem aint₂,
+    have a ∈ t₁, from mem_head_of_qeq e₁,
+    have a ∈ t₂, from mem_perm p₁ this,
+    obtain (t₂' : list A) (e₂' : t₂≈a|t₂'), from qeq_of_mem this,
     calc s₁  ~ t₂' : r₁ e₁ e₂'
         ...  ~ s₂  : r₂ e₂' e₂)
 
@@ -688,17 +688,15 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a
 | []       (a₂::t₂) d₁ d₂ e := absurd (iff.mpr (e a₂) !mem_cons) (not_mem_nil a₂)
 | (a₁::t₁) []       d₁ d₂ e := absurd (iff.mp (e a₁) !mem_cons) (not_mem_nil a₁)
 | (a₁::t₁) (a₂::t₂) d₁ d₂ e :=
-  have a₁inl₂   : a₁ ∈ a₂::t₂, from iff.mp (e a₁) !mem_cons,
-  have dt₁      : nodup t₁, from nodup_of_nodup_cons d₁,
-  have na₁int₁  : a₁ ∉ t₁, from not_mem_of_nodup_cons d₁,
-  have ex : ∃s₁ s₂, a₂::t₂ = s₁++(a₁::s₂), from mem_split a₁inl₂,
-  obtain (s₁ s₂ : list A) (t₂_eq : a₂::t₂ = s₁++(a₁::s₂)), from ex,
+  have a₁ ∈ a₂::t₂, from iff.mp (e a₁) !mem_cons,
+  have ∃s₁ s₂, a₂::t₂ = s₁++(a₁::s₂), from mem_split this,
+  obtain (s₁ s₂ : list A) (t₂_eq : a₂::t₂ = s₁++(a₁::s₂)), from this,
   have dt₂'     : nodup (a₁::(s₁++s₂)), from nodup_head (by rewrite [t₂_eq at d₂]; exact d₂),
   have na₁s₁s₂  : a₁ ∉ s₁++s₂, from not_mem_of_nodup_cons dt₂',
   have na₁s₁    : a₁ ∉ s₁,     from not_mem_of_not_mem_append_left na₁s₁s₂,
   have na₁s₂    : a₁ ∉ s₂,     from not_mem_of_not_mem_append_right na₁s₁s₂,
   have ds₁s₂    : nodup (s₁++s₂), from nodup_of_nodup_cons dt₂',
-  have eqv     : ∀a, a ∈ t₁ ↔ a ∈ s₁++s₂, from
+  have eqv      : ∀a, a ∈ t₁ ↔ a ∈ s₁++s₂, from
     take a, iff.intro
       (λ aint₁   : a ∈ t₁,
          assert aina₂t₂ : a ∈ a₂::t₂,       from iff.mp (e a) (mem_cons_of_mem _ aint₁),
@@ -706,22 +704,25 @@ theorem perm_ext : ∀ {l₁ l₂ : list A}, nodup l₁ → nodup l₂ → (∀a
          or.elim (mem_or_mem_of_mem_append ains₁a₁s₂)
            (λ ains₁ : a ∈ s₁, mem_append_left s₂ ains₁)
            (λ aina₁s₂ : a ∈ a₁::s₂, or.elim (eq_or_mem_of_mem_cons aina₁s₂)
-             (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ aint₁) na₁int₁)
+             (λ aeqa₁ : a = a₁,
+               have a₁ ∉ t₁, from not_mem_of_nodup_cons d₁,
+               absurd (aeqa₁ ▸ aint₁) this)
              (λ ains₂ : a ∈ s₂, mem_append_right s₁ ains₂)))
       (λ ains₁s₂ : a ∈ s₁ ++ s₂, or.elim (mem_or_mem_of_mem_append ains₁s₂)
         (λ ains₁ : a ∈ s₁,
-           have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ ains₁),
-           have aina₁t₁ : a ∈ a₁::t₁, from iff.mpr (e a) aina₂t₂,
-           or.elim (eq_or_mem_of_mem_cons aina₁t₁)
+           have a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_left _ ains₁),
+           have a ∈ a₁::t₁, from iff.mpr (e a) this,
+           or.elim (eq_or_mem_of_mem_cons this)
              (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₁) na₁s₁)
              (λ aint₁ : a ∈ t₁, aint₁))
         (λ ains₂ : a ∈ s₂,
-           have aina₂t₂ : a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ ains₂)),
-           have aina₁t₁ : a ∈ a₁::t₁, from iff.mpr (e a) aina₂t₂,
-           or.elim (eq_or_mem_of_mem_cons aina₁t₁)
+           have a ∈ a₂::t₂, from by rewrite [t₂_eq]; exact (mem_append_right _ (mem_cons_of_mem _ ains₂)),
+           have a ∈ a₁::t₁, from iff.mpr (e a) this,
+           or.elim (eq_or_mem_of_mem_cons this)
              (λ aeqa₁ : a = a₁, absurd (aeqa₁ ▸ ains₂) na₁s₂)
              (λ aint₁ : a ∈ t₁, aint₁))),
-  calc a₁::t₁ ~ a₁::(s₁++s₂) : skip a₁ (perm_ext dt₁ ds₁s₂ eqv)
+  have nodup t₁, from nodup_of_nodup_cons d₁,
+  calc a₁::t₁ ~ a₁::(s₁++s₂) : skip a₁ (perm_ext this ds₁s₂ eqv)
          ...  ~ s₁++(a₁::s₂) : !perm_middle
          ...  = a₂::t₂       : by rewrite t₂_eq
 end ext
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index c3ef4904a..4de7aa535 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -157,13 +157,13 @@ nat.induction_on n
   (take H : 0 + m = 0 + k,
     !zero_add⁻¹ ⬝ H ⬝ !zero_add)
   (take (n : ℕ) (IH : n + m = n + k → m = k) (H : succ n + m = succ n + k),
-    have H2 : succ (n + m) = succ (n + k),
+    have succ (n + m) = succ (n + k),
     from calc
       succ (n + m) = succ n + m   : succ_add
                ... = succ n + k   : H
                ... = succ (n + k) : succ_add,
-    have H3 : n + m = n + k, from succ.inj H2,
-    IH H3)
+    have n + m = n + k, from succ.inj this,
+    IH this)
 
 theorem add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k :=
 have H2 : m + n = m + k, from !add.comm ⬝ H ⬝ !add.comm,
diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean
index 26ae85568..b6b714d76 100644
--- a/library/data/nat/bquant.lean
+++ b/library/data/nat/bquant.lean
@@ -123,10 +123,10 @@ namespace nat
   | 0        h := absurd (ball_zero P) h
   | (succ n) h := decidable.by_cases
     (λ hp : P n,
-      have h₁ : ¬ ball n P, from
+      have ¬ ball n P, from
         assume b : ball n P, absurd (ball_succ_of_ball b hp) h,
-      have h₂ : {i | i < n ∧ ¬ P i}, from bsub_not_of_not_ball h₁,
-      bsub_succ h₂)
+      have {i | i < n ∧ ¬ P i}, from bsub_not_of_not_ball this,
+      bsub_succ this)
     (λ hn : ¬ P n, bsub_succ_of_pred hn)
 
   theorem bex_not_of_not_ball {n : nat} (H : ¬ ball n P) : bex n (λ n, ¬ P n) :=
@@ -137,8 +137,8 @@ namespace nat
   | (succ n) h := by_cases
     (λ hp : P n, absurd (bex_succ_of_pred hp) h)
     (λ hn : ¬ P n,
-      have h₁ : ¬ bex n P, from
+      have ¬ bex n P, from
         assume b : bex n P, absurd (bex_succ b) h,
-      have h₂ : ball n (λ n, ¬ P n), from ball_not_of_not_bex h₁,
-      ball_succ_of_ball h₂ hn)
+      have ball n (λ n, ¬ P n), from ball_not_of_not_bex this,
+      ball_succ_of_ball this hn)
 end nat
diff --git a/library/data/nat/choose.lean b/library/data/nat/choose.lean
index 8100a0f15..36025adf2 100644
--- a/library/data/nat/choose.lean
+++ b/library/data/nat/choose.lean
@@ -42,12 +42,12 @@ acc.intro x (λ (y : nat) (l : y ≺ x),
 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),
-   have ygtx  : x < y,    from and.elim_left l,
    by_cases
-     (λ yeqx : y = succ x, by substvars; assumption)
-     (λ ynex : y ≠ succ x,
-        have ygtsx : succ x < y, from lt_of_le_and_ne ygtx (ne.symm ynex),
-        acc.inv h (and.intro ygtsx (and.elim_right l))))
+     (assume yeqx : y = succ x, by substvars; assumption)
+     (assume ynex : 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),
+        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 :=
 assume px ygtx,
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 37c1a0342..9af907260 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -135,14 +135,14 @@ nat.case_strong_induction_on x
     show succ x mod y < y, from
       by_cases -- (succ x < y)
         (assume H1 : succ x < y,
-          have H2 : succ x mod y = succ x, from mod_eq_of_lt H1,
-          show succ x mod y < y, from H2⁻¹ ▸ H1)
+          have succ x mod y = succ x, from mod_eq_of_lt H1,
+          show succ x mod y < y, from this⁻¹ ▸ H1)
         (assume H1 : ¬ succ x < y,
-          have H2 : y ≤ succ x, from le_of_not_gt H1,
-          have H3 : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H H2,
-          have H4 : succ x - y < succ x, from sub_lt !succ_pos H,
-          have H5 : succ x - y ≤ x, from le_of_lt_succ H4,
-          show succ x mod y < y, from H3⁻¹ ▸ IH _ H5))
+          have y ≤ succ x, from le_of_not_gt H1,
+          have h : succ x mod y = (succ x - y) mod y, from mod_eq_sub_mod H this,
+          have succ x - y < succ x, from sub_lt !succ_pos H,
+          have succ x - y ≤ x, from le_of_lt_succ this,
+          show succ x mod y < y, from h⁻¹ ▸ IH _ this))
 
 theorem mod_one (n : ℕ) : n mod 1 = 0 :=
 have H1 : n mod 1 < 1, from !mod_lt !succ_pos,
@@ -368,10 +368,10 @@ by_cases_zero_pos n
     assume H2 : n ∣ m,
     obtain k (Hk : n = m * k), from exists_eq_mul_right_of_dvd H1,
     obtain l (Hl : m = n * l), from exists_eq_mul_right_of_dvd H2,
-    have H3 : n * (l * k) = n, from !mul.assoc ▸ Hl ▸ Hk⁻¹,
-    have H4 : l * k = 1, from eq_one_of_mul_eq_self_right Hpos H3,
-    have H5 : k = 1, from eq_one_of_mul_eq_one_left H4,
-    show m = n, from (mul_one m)⁻¹ ⬝ (H5 ▸ Hk⁻¹))
+    have n * (l * k) = n, from !mul.assoc ▸ Hl ▸ Hk⁻¹,
+    have l * k = 1,       from eq_one_of_mul_eq_self_right Hpos this,
+    have k = 1,           from eq_one_of_mul_eq_one_left this,
+    show m = n,           from (mul_one m)⁻¹ ⬝ (this ▸ Hk⁻¹))
 
 theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : k ∣ n) : m * n div k = m * (n div k) :=
 or.elim (eq_zero_or_pos k)
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 9162e42d7..19f2d4250 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -392,11 +392,11 @@ have H4 : k * m < k * l, from mul_lt_mul_of_pos_left H2 (lt_of_le_of_lt !zero_le
 lt_of_le_of_lt H3 H4
 
 theorem eq_of_mul_eq_mul_left {m k n : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k :=
-have H2 : n * m ≤ n * k, by rewrite H,
-have H3 : n * k ≤ n * m, by rewrite H,
-have H4 : m ≤ k, from le_of_mul_le_mul_left H2 Hn,
-have H5 : k ≤ m, from le_of_mul_le_mul_left H3 Hn,
-le.antisymm H4 H5
+have n * m ≤ n * k, by rewrite H,
+have h : m ≤ k, from le_of_mul_le_mul_left this Hn,
+have n * k ≤ n * m, by rewrite H,
+have k ≤ m, from le_of_mul_le_mul_left this Hn,
+le.antisymm h this
 
 theorem eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k :=
 eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
@@ -410,15 +410,15 @@ eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H)
 
 theorem eq_one_of_mul_eq_one_right {n m : ℕ} (H : n * m = 1) : n = 1 :=
 have H2 : n * m > 0, by rewrite H; apply succ_pos,
-have H3 : n > 0, from pos_of_mul_pos_right H2,
-have H4 : m > 0, from pos_of_mul_pos_left H2,
 or.elim (le_or_gt n 1)
   (assume H5 : n ≤ 1,
-    show n = 1, from le.antisymm H5 (succ_le_of_lt H3))
+    have n > 0, from pos_of_mul_pos_right H2,
+    show n = 1, from le.antisymm H5 (succ_le_of_lt this))
   (assume H5 : n > 1,
-    have H6 : n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt H4),
-    have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6,
-    absurd !lt_succ_self (not_lt_of_ge H7))
+    have m > 0, from pos_of_mul_pos_left H2,
+    have n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt this),
+    have 1 ≥ 2, from !mul_one ▸ H ▸ this,
+    absurd !lt_succ_self (not_lt_of_ge this))
 
 theorem eq_one_of_mul_eq_one_left {n m : ℕ} (H : n * m = 1) : m = 1 :=
 eq_one_of_mul_eq_one_right (!mul.comm ▸ H)
diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean
index 9671f9105..385d41291 100644
--- a/library/theories/number_theory/primes.lean
+++ b/library/theories/number_theory/primes.lean
@@ -64,23 +64,23 @@ 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 h₁ : p ∣ i, from dvd_of_mod_eq_zero h,
-have h₂ : p ≥ 2, from ge_two_of_prime ipp,
-have h₃ : p ≤ i, from le_of_dvd pos h₁,
-lt_of_succ_le (le.trans h₂ h₃)
+have h₁ : p ≥ 2, from ge_two_of_prime ipp,
+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 h₁ this)
 
 definition sub_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → {m | m ∣ n ∧ m ≠ 1 ∧ m ≠ n} :=
 assume h₁ h₂,
-have h₃ : ¬ prime_ext n, from iff.mpr (not_iff_not_of_iff !prime_ext_iff_prime) h₂,
-have h₄ : ¬ n ≥ 2 ∨ ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from iff.mp !not_and_iff_not_or_not h₃,
-have h₅ : ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from or_resolve_right h₄ (not_not_intro h₁),
-have h₆ : ¬ (∀ m, m < succ n → m ∣ n → m = 1 ∨ m = n), from
-  assume h, absurd (λ m hl hd, h m (lt_succ_of_le hl) hd) h₅,
-have h₇ : {m | m < succ n ∧ ¬(m ∣ n → m = 1 ∨ m = n)}, from bsub_not_of_not_ball h₆,
-obtain m hlt (h₈ : ¬(m ∣ n → m = 1 ∨ m = n)), from h₇,
-obtain (h₈ : m ∣ n) (h₉ : ¬ (m = 1 ∨ m = n)), from iff.mp !not_implies_iff_and_not h₈,
-have h₁₀ : ¬ m = 1 ∧ ¬ m = n, from iff.mp !not_or_iff_not_and_not h₉,
-subtype.tag m (and.intro h₈ h₁₀)
+have ¬ prime_ext n, from iff.mpr (not_iff_not_of_iff !prime_ext_iff_prime) h₂,
+have ¬ n ≥ 2 ∨ ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from iff.mp !not_and_iff_not_or_not this,
+have ¬ (∀ m, m ≤ n → m ∣ n → m = 1 ∨ m = n), from or_resolve_right this (not_not_intro h₁),
+have ¬ (∀ m, m < succ n → m ∣ n → m = 1 ∨ m = n), from
+  assume h, absurd (λ m hl hd, h m (lt_succ_of_le hl) hd) this,
+have {m | m < succ n ∧ ¬(m ∣ n → m = 1 ∨ m = n)}, from bsub_not_of_not_ball this,
+obtain m hlt (h₃ : ¬(m ∣ n → m = 1 ∨ m = n)), from this,
+obtain (h₄ : m ∣ n) (h₅ : ¬ (m = 1 ∨ m = n)), from iff.mp !not_implies_iff_and_not h₃,
+have ¬ m = 1 ∧ ¬ m = n,  from iff.mp !not_or_iff_not_and_not h₅,
+subtype.tag m (and.intro h₄ this)
 
 theorem ex_dvd_of_not_prime {n : nat} : n ≥ 2 → ¬ prime n → ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
 assume h₁ h₂, ex_of_sub (sub_dvd_of_not_prime h₁ h₂)
@@ -121,20 +121,20 @@ open eq.ops
 
 definition infinite_primes (n : nat) : {p | p ≥ n ∧ prime p} :=
 let m := fact (n + 1) in
-have m_ge_1 : m ≥ 1,  from le_of_lt_succ (succ_lt_succ (fact_pos _)),
-have m1_ge_2 : m + 1 ≥ 2, from succ_le_succ m_ge_1,
-obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd m1_ge_2,
+have m ≥ 1,     from le_of_lt_succ (succ_lt_succ (fact_pos _)),
+have m + 1 ≥ 2, from succ_le_succ this,
+obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from sub_prime_and_dvd this,
 have p_ge_2 : p ≥ 2, from ge_two_of_prime prime_p,
 have p_gt_0 : p > 0, from lt_of_succ_lt (lt_of_succ_le p_ge_2),
-have p_ge_n : p ≥ n, from by_contradiction
+have p ≥ n, from by_contradiction
   (assume h₁ : ¬ p ≥ n,
-    have h₂ : p < n, from lt_of_not_ge h₁,
-    have h₃ : p ≤ n + 1, from le_of_lt (lt.step h₂),
-    have h₄ : p ∣ m, from dvd_fact p_gt_0 h₃,
-    have h₅ : p ∣ 1, from dvd_of_dvd_add_right (!add.comm ▸ p_dvd_m1) h₄,
-    have h₆ : p ≤ 1, from le_of_dvd zero_lt_one h₅,
-    absurd (le.trans p_ge_2 h₆) dec_trivial),
-subtype.tag p (and.intro p_ge_n prime_p)
+    have p < n,     from lt_of_not_ge h₁,
+    have p ≤ n + 1, from le_of_lt (lt.step this),
+    have p ∣ m,      from dvd_fact p_gt_0 this,
+    have p ∣ 1,      from dvd_of_dvd_add_right (!add.comm ▸ p_dvd_m1) this,
+    have p ≤ 1,     from le_of_dvd zero_lt_one this,
+    absurd (le.trans p_ge_2 this) dec_trivial),
+subtype.tag p (and.intro this prime_p)
 
 lemma ex_infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p :=
 ex_of_sub (infinite_primes n)
@@ -158,10 +158,10 @@ by_contradiction (assume nc : ¬ coprime p n, npdvdn (dvd_of_prime_of_not_coprim
 
 theorem not_dvd_of_prime_of_coprime {p n : ℕ} (primep : prime p) (cop : coprime p n) : ¬ p ∣ n :=
 assume pdvdn : p ∣ n,
-have H1 : p ∣ gcd p n, from dvd_gcd !dvd.refl pdvdn,
-have H2 : p ≤ gcd p n, from le_of_dvd (!gcd_pos_of_pos_left (pos_of_prime primep)) H1,
-have H3 : 2 ≤ 1, from le.trans (ge_two_of_prime primep) (cop ▸ H2),
-show false, from !not_succ_le_self H3
+have p ∣ gcd p n,  from dvd_gcd !dvd.refl pdvdn,
+have p ≤ gcd p n, from le_of_dvd (!gcd_pos_of_pos_left (pos_of_prime primep)) this,
+have 2 ≤ 1,       from le.trans (ge_two_of_prime primep) (cop ▸ this),
+show false,       from !not_succ_le_self this
 
 theorem not_coprime_of_prime_dvd {p n : ℕ} (primep : prime p) (pdvdn : p ∣ n) : ¬ coprime p n :=
 assume cop, not_dvd_of_prime_of_coprime primep cop pdvdn
@@ -169,8 +169,8 @@ assume cop, not_dvd_of_prime_of_coprime primep cop pdvdn
 theorem dvd_of_prime_of_dvd_mul_left {p m n : ℕ} (primep : prime p)
     (Hmn : p ∣ m * n) (Hm : ¬ p ∣ m) :
   p ∣ n :=
-have copm : coprime p m, from coprime_of_prime_of_not_dvd primep Hm,
-show p ∣ n, from dvd_of_coprime_of_dvd_mul_left copm Hmn
+have coprime p m, from coprime_of_prime_of_not_dvd primep Hm,
+show p ∣ n, from dvd_of_coprime_of_dvd_mul_left this Hmn
 
 theorem dvd_of_prime_of_dvd_mul_right {p m n : ℕ} (primep : prime p)
     (Hmn : p ∣ m * n) (Hn : ¬ p ∣ n) :
@@ -188,12 +188,12 @@ lemma dvd_or_dvd_of_prime_of_dvd_mul {p m n : nat} : prime p → p ∣ m * n →
 
 lemma dvd_of_prime_of_dvd_pow {p m : nat} : ∀ {n}, prime p → p ∣ m^n → p ∣ m
 | 0 hp hd :=
-  assert peq1 : p = 1, from eq_one_of_dvd_one hd,
-  have h₂ : 1 ≥ 2, by rewrite -peq1; apply ge_two_of_prime hp,
-  absurd h₂ dec_trivial
+  assert p = 1, from eq_one_of_dvd_one hd,
+  have   1 ≥ 2, by rewrite -this; apply ge_two_of_prime hp,
+  absurd this dec_trivial
 | (succ n) hp hd :=
-  have hd₁ : p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd,
-  or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp hd₁)
+  have p ∣ (m^n)*m, by rewrite [pow_succ at hd]; exact hd,
+  or.elim (dvd_or_dvd_of_prime_of_dvd_mul hp this)
     (λ h : p ∣ m^n, dvd_of_prime_of_dvd_pow hp h)
     (λ h : p ∣ m, h)
 
@@ -202,13 +202,13 @@ lemma coprime_pow_of_prime_of_not_dvd {p m a : nat} : prime p → ¬ p ∣ a →
 
 lemma coprime_primes {p q : nat} : prime p → prime q → p ≠ q → coprime p q :=
 λ hp hq hn,
-  assert d₁ : gcd p q ∣ p, from !gcd_dvd_left,
-  assert d₂ : gcd p q ∣ q, from !gcd_dvd_right,
-  or.elim (eq_one_or_eq_self_of_prime_of_dvd hp d₁)
+  assert gcd p q ∣ p, from !gcd_dvd_left,
+  or.elim (eq_one_or_eq_self_of_prime_of_dvd hp this)
     (λ h : gcd p q = 1, h)
     (λ h : gcd p q = p,
-      have d₃ : p ∣ q, by rewrite -h; exact d₂,
-      or.elim (eq_one_or_eq_self_of_prime_of_dvd hq d₃)
+      assert gcd p q ∣ q, from !gcd_dvd_right,
+      have   p ∣ q, by rewrite -h; exact this,
+      or.elim (eq_one_or_eq_self_of_prime_of_dvd hq this)
         (λ h₁ : p = 1, by subst p; exact absurd hp not_prime_one)
         (λ he : p = q, by contradiction))
 
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index c5eae4ab8..fce21c492 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -16,7 +16,7 @@
     "alias" "help" "environment" "options" "precedence" "reserve"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"
     "tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix"
-    "eval" "check" "end" "reveal"
+    "eval" "check" "end" "reveal" "this"
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes"
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing")
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 5c1fcb78a..9109b6a57 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -369,7 +369,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
     if (p.curr_is_token(get_visible_tk())) {
         p.next();
         is_visible    = true;
-        id            = p.mk_fresh_name();
+        id            = get_this_tk();
         prop          = p.parse_expr();
     } else if (p.curr_is_identifier()) {
         id = p.get_name_val();
@@ -384,11 +384,15 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
             prop      = p.parse_expr();
         } else {
             expr left = p.id_to_expr(id, id_pos);
-            id        = p.mk_fresh_name();
-            prop      = p.parse_led(left);
+            id        = get_this_tk();
+            unsigned rbp = 0;
+            while (rbp < p.curr_expr_lbp()) {
+                left = p.parse_led(left);
+            }
+            prop      = left;
         }
     } else {
-        id            = p.mk_fresh_name();
+        id            = get_this_tk();
         prop          = p.parse_expr();
     }
     expr proof;
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 3c603a01c..808145c17 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -141,6 +141,7 @@ static name const * g_fields_tk = nullptr;
 static name const * g_trust_tk = nullptr;
 static name const * g_metaclasses_tk = nullptr;
 static name const * g_inductive_tk = nullptr;
+static name const * g_this_tk = nullptr;
 void initialize_tokens() {
     g_period_tk = new name{"."};
     g_placeholder_tk = new name{"_"};
@@ -280,6 +281,7 @@ void initialize_tokens() {
     g_trust_tk = new name{"trust"};
     g_metaclasses_tk = new name{"metaclasses"};
     g_inductive_tk = new name{"inductive"};
+    g_this_tk = new name{"this"};
 }
 void finalize_tokens() {
     delete g_period_tk;
@@ -420,6 +422,7 @@ void finalize_tokens() {
     delete g_trust_tk;
     delete g_metaclasses_tk;
     delete g_inductive_tk;
+    delete g_this_tk;
 }
 name const & get_period_tk() { return *g_period_tk; }
 name const & get_placeholder_tk() { return *g_placeholder_tk; }
@@ -559,4 +562,5 @@ name const & get_fields_tk() { return *g_fields_tk; }
 name const & get_trust_tk() { return *g_trust_tk; }
 name const & get_metaclasses_tk() { return *g_metaclasses_tk; }
 name const & get_inductive_tk() { return *g_inductive_tk; }
+name const & get_this_tk() { return *g_this_tk; }
 }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 323195b8e..621dc6daa 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -143,4 +143,5 @@ name const & get_fields_tk();
 name const & get_trust_tk();
 name const & get_metaclasses_tk();
 name const & get_inductive_tk();
+name const & get_this_tk();
 }
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index a76230e5e..a00f8abc4 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -136,3 +136,4 @@ fields       fields
 trust        trust
 metaclasses  metaclasses
 inductive    inductive
+this         this