diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean
index 5323de51d7..ae7e8328f0 100644
--- a/library/data/bitvec.lean
+++ b/library/data/bitvec.lean
@@ -42,9 +42,9 @@ section shift
   bitvec.cong
     begin
       by_cases (i ≤ n),
-      { note h₁ := sub_le n i,
+      { have h₁ := sub_le n i,
         rw [min_eq_right h], rw [min_eq_left h₁, -nat.add_sub_assoc h, add_comm, nat.add_sub_cancel] },
-      { note h₁ := le_of_not_ge h,
+      { have h₁ := le_of_not_ge h,
         rw [min_eq_left h₁, sub_eq_zero_of_le h₁, min_zero_left, add_zero] }
     end $
     repeat fill (min n i) ++ₜ taken (n-i) x
@@ -165,7 +165,7 @@ section conversion
     simp [bits_to_nat_to_list], clear P,
     unfold bits_to_nat list.foldl,
       -- the next 4 lines generalize the accumulator of foldl
-    define x := 0,
+    let x := 0,
     change _ = add_lsb x b + _,
     generalize 0 y,
     revert x, simp,
@@ -192,7 +192,7 @@ section conversion
     revert n,
     induction k with k ; intro n,
     { unfold pow, simp [nat.mod_one], refl },
-    { note h : 0 < 2, { apply le_succ },
+    { have h : 0 < 2, { apply le_succ },
       rw [ of_nat_succ
          , to_nat_append
          , ih_1
diff --git a/library/data/dlist.lean b/library/data/dlist.lean
index 5a3d26588e..99533ea3de 100644
--- a/library/data/dlist.lean
+++ b/library/data/dlist.lean
@@ -68,7 +68,7 @@ by cases l; simp
 lemma of_list_to_list (l : dlist α) : of_list (to_list l) = l :=
 begin
    cases l with xs,
-   note h : append (xs []) = xs,
+   have h : append (xs []) = xs,
    {intros, apply funext, intros x, simp [invariant x]},
    simp [h]
 end
diff --git a/library/data/hash_map.lean b/library/data/hash_map.lean
index 203b749bb1..b59532a435 100644
--- a/library/data/hash_map.lean
+++ b/library/data/hash_map.lean
@@ -41,7 +41,7 @@ begin
   intros,
   induction j with j IH,
   exact ⟨false.elim, λ⟨i, h, _⟩, absurd h (nat.not_lt_zero _)⟩,
-  note IH := IH (le_of_lt h),
+  have IH := IH (le_of_lt h),
   simp[array.iterate_aux],
   exact ⟨λo, or.elim o
     (λm, ⟨⟨j, h⟩, nat.le_refl _, m⟩)
@@ -165,10 +165,10 @@ have h1 : list.length (array.to_list bkts) - 1 - i < list.length (list.reverse (
 have sigma.mk a b ∈ list.nth_le (array.to_list bkts) i (by simph[array.to_list_length]), by {rw array.to_list_nth, exact el},
 begin
   rw -list.nth_le_reverse at this,
-  note v : valid_aux (λa, (mk_idx n (hash_fn a)).1) (array.to_list bkts).reverse sz,
+  have v : valid_aux (λa, (mk_idx n (hash_fn a)).1) (array.to_list bkts).reverse sz,
   rw array.to_list_reverse,
   exact v,
-  note mm := @_root_.hash_map.valid_aux.eq _ _ _ _ _ _ v -- TODO (Mario): Why is explicit namespacing needed here?
+  have mm := @_root_.hash_map.valid_aux.eq _ _ _ _ _ _ v -- TODO (Mario): Why is explicit namespacing needed here?
     (list.length (array.to_list bkts) - 1 - i) h1 a b this,
   rwa [list.length_reverse, array.to_list_length, nat.sub_sub_self (show i ≤ n.1 - 1, from nat.pred_le_pred h)] at mm
 end
@@ -190,7 +190,7 @@ begin
     let ⟨⟨a', b⟩, m1, e1⟩ := list.exists_of_mem_map m1 in
     let ⟨⟨a'', b'⟩, m2, e2⟩ := list.exists_of_mem_map m2 in
     match a', a'', b, b', m1, m2, e1, e2 with ._, ._, b, b', m1, m2, rfl, rfl :=
-      by {note hlt := al _ m1, rw v.eq _ m2 at hlt, exact lt_irrefl _ hlt}
+      by {have hlt := al _ m1, rw v.eq _ m2 at hlt, exact lt_irrefl _ hlt}
     end,
   λ⟨a, b⟩ m, or.elim m
     (λm2, by rw v.eq _ m2; exact nat.le_refl _)
@@ -200,7 +200,7 @@ end
 theorem valid.as_list_length {n} {bkts : bucket_array α β n} {sz : nat} (v : valid bkts sz) : bkts.as_list.length = sz :=
 have ∀l sz, valid_aux (λ (a : α), (mk_idx n (hash_fn a)).val) l sz → ∀t, (l.foldr (λbkt r, r ++ bkt) t).length = sz + t.length,
 by {intros, induction a, simp[list.foldr], simp[list.foldr, ih_1]},
-by note h := this _ _ v []; rwa -array.foldl_eq at h
+by have h := this _ _ v []; rwa -array.foldl_eq at h
 
 theorem valid.mk (n : ℕ+) : @valid n (mk_array n.1 []) 0 :=
 let bkts : bucket_array α β n := mk_array n.1 [] in
@@ -321,10 +321,10 @@ section
           have nd' : ((u ++ v2 ++ w).map sigma.fst).nodup, begin
             rw [list.map_append, list.map_append] at nd,
             rw [list.map_append, list.map_append],
-            note ndu : (u.map sigma.fst).nodup := list.nodup_of_nodup_append_left (list.nodup_of_nodup_append_left nd),
-            note ndv1 : (v1.map sigma.fst).nodup := list.nodup_of_nodup_append_right (list.nodup_of_nodup_append_left nd),
-            note ndw : (w.map sigma.fst).nodup := list.nodup_of_nodup_append_right nd,
-            note djuw : (u.map sigma.fst).disjoint (w.map sigma.fst) :=
+            have ndu : (u.map sigma.fst).nodup := list.nodup_of_nodup_append_left (list.nodup_of_nodup_append_left nd),
+            have ndv1 : (v1.map sigma.fst).nodup := list.nodup_of_nodup_append_right (list.nodup_of_nodup_append_left nd),
+            have ndw : (w.map sigma.fst).nodup := list.nodup_of_nodup_append_right nd,
+            have djuw : (u.map sigma.fst).disjoint (w.map sigma.fst) :=
               list.disjoint_of_disjoint_append_left_left (list.disjoint_of_nodup_append nd),
             exact list.nodup_append_of_nodup_of_nodup_of_disjoint
               (list.nodup_append_of_nodup_of_nodup_of_disjoint ndu hvnd djuv)
@@ -487,7 +487,7 @@ suffices ∀ (l : list Σ a, β a),
   ∀ (t : bucket_array α β n') sz, valid hash_fn t sz → ((l ++ t.as_list).map sigma.fst).nodup →
     valid hash_fn (l.foldl (λr (a : Σ a, β a), reinsert_aux hash_fn r a.1 a.2) t) (sz + l.length),
 begin
-  note p := this bkts.as_list _ _ (valid.mk _ _),
+  have p := this bkts.as_list _ _ (valid.mk _ _),
   rw [mk_as_list hash_fn, list.append_nil, zero_add, v.as_list_length _] at p,
   rw bucket_array.foldl_eq,
   exact p (v.as_list_nodup _),
@@ -498,13 +498,13 @@ end,
   intros t sz v nd,
   rw (show sz + (c :: l).length = sz + 1 + l.length, by simp),
   simp at nd,
-  note nc := list.not_mem_of_nodup_cons nd,
-  note v' := v.insert _ _ c.2
+  have nc := list.not_mem_of_nodup_cons nd,
+  have v' := v.insert _ _ c.2
     (λHc, nc $ list.mem_append_right _ $
       (v.contains_aux_iff _ c.1).1 Hc),
   apply IH _ _ v',
   simp,
-  note nd' := list.nodup_of_nodup_cons nd,
+  have nd' := list.nodup_of_nodup_cons nd,
   apply list.nodup_append_of_nodup_of_nodup_of_disjoint
     (list.nodup_of_nodup_append_left nd')
     (v'.as_list_nodup _),
@@ -576,7 +576,7 @@ if h : a = a' then by simp[h]; exact
       have bkts.as_list.map sigma.fst = u.map sigma.fst ++ w.map sigma.fst, by simp [hl],
       by rw this at na; exact na
     | ._, or.inr ⟨b'', rfl⟩, hl := by {
-      note nd' := v.as_list_nodup _,
+      have nd' := v.as_list_nodup _,
       rw hl at nd', simp at nd',
       exact list.not_mem_of_nodup_cons (list.nodup_head nd') }
     end,
@@ -681,7 +681,7 @@ match (by apply_instance : decidable (contains_aux a bkt)) with
   | ._, ._, ⟨u, w, rfl, rfl⟩, nd' := by simp; simp at nd'; exact
     ⟨λhm, ⟨λe, match a', e, b', hm with ._, rfl, b', hm := by {
       rw -list.mem_append_iff at hm;
-      note hm := list.mem_map sigma.fst hm;
+      have hm := list.mem_map sigma.fst hm;
       rw list.map_append at hm;
       exact list.not_mem_of_nodup_cons (list.nodup_head nd') hm }
     end, or.inr hm⟩,
diff --git a/library/data/stream.lean b/library/data/stream.lean
index 848059bd93..4a39389c46 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -482,8 +482,8 @@ lemma take_lemma (s₁ s₂ : stream α) : (∀ (n : nat), approx n s₁ = appro
 begin
   intro h, apply stream.ext, intro n,
   induction n with n ih,
-  { note aux := h 1, unfold approx at aux, injection aux },
-  { note h₁ : some (nth (succ n) s₁) = some (nth (succ n) s₂),
+  { have aux := h 1, unfold approx at aux, injection aux },
+  { have h₁ : some (nth (succ n) s₁) = some (nth (succ n) s₂),
     { rw [-nth_approx, -nth_approx, h (succ (succ n))] },
     injection h₁ }
 end
diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean
index 62d8cc14c0..2402ee38c1 100644
--- a/library/init/algebra/functions.lean
+++ b/library/init/algebra/functions.lean
@@ -299,14 +299,14 @@ or.elim (le_total b 0)
     assume h4 : a < 0,
     have h5 : a + b < 0,
       begin
-        note aux := add_lt_add_of_lt_of_le h4 h2,
+        have aux := add_lt_add_of_lt_of_le h4 h2,
         rwa [add_zero] at aux
       end,
     not_lt_of_ge h1 h5,
   aux1 h1 (le_of_not_gt h3))
  (assume h2 : 0 ≤ b,
   begin
-    note h3 : abs (b + a) ≤ abs b + abs a,
+    have h3 : abs (b + a) ≤ abs b + abs a,
     begin
       rw add_comm at h1,
       exact aux1 h1 h2
diff --git a/library/init/algebra/norm_num.lean b/library/init/algebra/norm_num.lean
index d09d82f19d..85d2689048 100644
--- a/library/init/algebra/norm_num.lean
+++ b/library/init/algebra/norm_num.lean
@@ -113,7 +113,7 @@ by rw [-h, mul_div_assoc]
 lemma nonzero_of_div_helper [field α] (a b : α) (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 :=
 begin
   intro hab,
-  note habb : (a / b) * b = 0, rw [hab, zero_mul],
+  have habb : (a / b) * b = 0, rw [hab, zero_mul],
   rw [div_mul_cancel _ hb] at habb,
   exact ha habb
 end
diff --git a/library/init/algebra/ordered_field.lean b/library/init/algebra/ordered_field.lean
index f4bbb2fba6..df40f8aaf4 100644
--- a/library/init/algebra/ordered_field.lean
+++ b/library/init/algebra/ordered_field.lean
@@ -329,8 +329,8 @@ calc
 lemma div_mul_le_div_mul_of_div_le_div_pos {a b c d e : α} (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b ≤ c / d)
       (he : e > 0) : a / (b * e) ≤ c / (d * e) :=
 begin
-  note h₁ := field.div_mul_eq_div_mul_one_div a hb (ne_of_gt he),
-  note h₂ := field.div_mul_eq_div_mul_one_div c hd (ne_of_gt he),
+  have h₁ := field.div_mul_eq_div_mul_one_div a hb (ne_of_gt he),
+  have h₂ := field.div_mul_eq_div_mul_one_div c hd (ne_of_gt he),
   rw [h₁, h₂],
   apply mul_le_mul_of_nonneg_right h,
   apply le_of_lt,
@@ -341,13 +341,13 @@ lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a
 begin
   apply exists.intro ((a - b) / (1 + 1)),
   split,
-  {note h2 : a + a > (b + b) + (a - b),
+  {have h2 : a + a > (b + b) + (a - b),
     calc
       a + a > b + a             : add_lt_add_right h _
         ... = b + a + b - b     : by rw add_sub_cancel
         ... = b + b + a - b     : by simp
         ... = (b + b) + (a - b) : by rw add_sub,
-   note h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
+   have h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
      exact div_lt_div_of_lt_of_pos h2 two_pos,
    rw [one_add_one_eq_two, sub_eq_add_neg],
    rw [add_self_div_two, -div_add_div_same, add_self_div_two, sub_eq_add_neg] at h3,
@@ -360,7 +360,7 @@ begin
   apply le_of_not_gt,
   intro hb,
   cases exists_add_lt_and_pos_of_lt hb with c hc,
-  note  hc' := h c (and.right hc),
+  have  hc' := h c (and.right hc),
   apply (not_le_of_gt (and.left hc)) (le_add_of_sub_right_le hc')
 end
 
diff --git a/library/init/algebra/ordered_group.lean b/library/init/algebra/ordered_group.lean
index 601450fdca..49763175e7 100644
--- a/library/init/algebra/ordered_group.lean
+++ b/library/init/algebra/ordered_group.lean
@@ -262,145 +262,145 @@ by rwa neg_zero at this
 
 lemma le_neg_of_le_neg {a b : α} (h : a ≤ -b) : b ≤ -a :=
 begin
-  note h := neg_le_neg h,
+  have h := neg_le_neg h,
   rwa neg_neg at h
 end
 
 lemma neg_le_of_neg_le {a b : α} (h : -a ≤ b) : -b ≤ a :=
 begin
-  note h := neg_le_neg h,
+  have h := neg_le_neg h,
   rwa neg_neg at h
 end
 
 lemma lt_neg_of_lt_neg {a b : α} (h : a < -b) : b < -a :=
 begin
-  note h := neg_lt_neg h,
+  have h := neg_lt_neg h,
   rwa neg_neg at h
 end
 
 lemma neg_lt_of_neg_lt {a b : α} (h : -a < b) : -b < a :=
 begin
-  note h := neg_lt_neg h,
+  have h := neg_lt_neg h,
   rwa neg_neg at h
 end
 
 lemma sub_nonneg_of_le {a b : α} (h : b ≤ a) : 0 ≤ a - b :=
 begin
-  note h := add_le_add_right h (-b),
+  have h := add_le_add_right h (-b),
   rwa add_right_neg at h
 end
 
 lemma le_of_sub_nonneg {a b : α} (h : 0 ≤ a - b) : b ≤ a :=
 begin
-  note h := add_le_add_right h b,
+  have h := add_le_add_right h b,
   rwa [sub_add_cancel, zero_add] at h
 end
 
 lemma sub_nonpos_of_le {a b : α} (h : a ≤ b) : a - b ≤ 0 :=
 begin
-  note h := add_le_add_right h (-b),
+  have h := add_le_add_right h (-b),
   rwa add_right_neg at h
 end
 
 lemma le_of_sub_nonpos {a b : α} (h : a - b ≤ 0) : a ≤ b :=
 begin
-  note h := add_le_add_right h b,
+  have h := add_le_add_right h b,
   rwa [sub_add_cancel, zero_add] at h
 end
 
 lemma sub_pos_of_lt {a b : α} (h : b < a) : 0 < a - b :=
 begin
-  note h := add_lt_add_right h (-b),
+  have h := add_lt_add_right h (-b),
   rwa add_right_neg at h
 end
 
 lemma lt_of_sub_pos {a b : α} (h : 0 < a - b) : b < a :=
 begin
-  note h := add_lt_add_right h b,
+  have h := add_lt_add_right h b,
   rwa [sub_add_cancel, zero_add] at h
 end
 
 lemma sub_neg_of_lt {a b : α} (h : a < b) : a - b < 0 :=
 begin
-  note h := add_lt_add_right h (-b),
+  have h := add_lt_add_right h (-b),
   rwa add_right_neg at h
 end
 
 lemma lt_of_sub_neg {a b : α} (h : a - b < 0) : a < b :=
 begin
-  note h := add_lt_add_right h b,
+  have h := add_lt_add_right h b,
   rwa [sub_add_cancel, zero_add] at h
 end
 
 lemma add_le_of_le_neg_add {a b c : α} (h : b ≤ -a + c) : a + b ≤ c :=
 begin
-  note h := add_le_add_left h a,
+  have h := add_le_add_left h a,
   rwa add_neg_cancel_left at h
 end
 
 lemma le_neg_add_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ -a + c :=
 begin
-  note h := add_le_add_left h (-a),
+  have h := add_le_add_left h (-a),
   rwa neg_add_cancel_left at h
 end
 
 lemma add_le_of_le_sub_left {a b c : α} (h : b ≤ c - a) : a + b ≤ c :=
 begin
-  note h := add_le_add_left h a,
+  have h := add_le_add_left h a,
   rwa [-add_sub_assoc, add_comm a c, add_sub_cancel] at h
 end
 
 lemma le_sub_left_of_add_le {a b c : α} (h : a + b ≤ c) : b ≤ c - a :=
 begin
-  note h := add_le_add_right h (-a),
+  have h := add_le_add_right h (-a),
   rwa [add_comm a b, add_neg_cancel_right] at h
 end
 
 lemma add_le_of_le_sub_right {a b c : α} (h : a ≤ c - b) : a + b ≤ c :=
 begin
-  note h := add_le_add_right h b,
+  have h := add_le_add_right h b,
   rwa sub_add_cancel at h
 end
 
 lemma le_sub_right_of_add_le {a b c : α} (h : a + b ≤ c) : a ≤ c - b :=
 begin
-  note h := add_le_add_right h (-b),
+  have h := add_le_add_right h (-b),
   rwa add_neg_cancel_right at h
 end
 
 lemma le_add_of_neg_add_le {a b c : α} (h : -b + a ≤ c) : a ≤ b + c :=
 begin
-  note h := add_le_add_left h b,
+  have h := add_le_add_left h b,
   rwa add_neg_cancel_left at h
 end
 
 lemma neg_add_le_of_le_add {a b c : α} (h : a ≤ b + c) : -b + a ≤ c :=
 begin
-  note h := add_le_add_left h (-b),
+  have h := add_le_add_left h (-b),
   rwa neg_add_cancel_left at h
 end
 
 lemma le_add_of_sub_left_le {a b c : α} (h : a - b ≤ c) : a ≤ b + c :=
 begin
-  note h := add_le_add_right h b,
+  have h := add_le_add_right h b,
   rwa [sub_add_cancel, add_comm] at h
 end
 
 lemma sub_left_le_of_le_add {a b c : α} (h : a ≤ b + c) : a - b ≤ c :=
 begin
-  note h := add_le_add_right h (-b),
+  have h := add_le_add_right h (-b),
   rwa [add_comm b c, add_neg_cancel_right] at h
 end
 
 lemma le_add_of_sub_right_le {a b c : α} (h : a - c ≤ b) : a ≤ b + c :=
 begin
-  note h := add_le_add_right h c,
+  have h := add_le_add_right h c,
   rwa sub_add_cancel at h
 end
 
 lemma sub_right_le_of_le_add {a b c : α} (h : a ≤ b + c) : a - c ≤ b :=
 begin
-  note h := add_le_add_right h (-c),
+  have h := add_le_add_right h (-c),
   rwa add_neg_cancel_right at h
 end
 
@@ -433,7 +433,7 @@ le_add_of_neg_add_le_left (add_le_of_le_sub_right h)
 
 lemma neg_le_sub_left_of_le_add {a b c : α} (h : c ≤ a + b) : -a ≤ b - c :=
 begin
-  note h := le_neg_add_of_add_le (sub_left_le_of_le_add h),
+  have h := le_neg_add_of_add_le (sub_left_le_of_le_add h),
   rwa add_comm at h
 end
 
@@ -457,73 +457,73 @@ add_le_add hab (neg_le_neg hcd)
 
 lemma add_lt_of_lt_neg_add {a b c : α} (h : b < -a + c) : a + b < c :=
 begin
-  note h := add_lt_add_left h a,
+  have h := add_lt_add_left h a,
   rwa add_neg_cancel_left at h
 end
 
 lemma lt_neg_add_of_add_lt {a b c : α} (h : a + b < c) : b < -a + c :=
 begin
-  note h := add_lt_add_left h (-a),
+  have h := add_lt_add_left h (-a),
   rwa neg_add_cancel_left at h
 end
 
 lemma add_lt_of_lt_sub_left {a b c : α} (h : b < c - a) : a + b < c :=
 begin
-  note h := add_lt_add_left h a,
+  have h := add_lt_add_left h a,
   rwa [-add_sub_assoc, add_comm a c, add_sub_cancel] at h
 end
 
 lemma lt_sub_left_of_add_lt {a b c : α} (h : a + b < c) : b < c - a :=
 begin
-  note h := add_lt_add_right h (-a),
+  have h := add_lt_add_right h (-a),
   rwa [add_comm a b, add_neg_cancel_right] at h
 end
 
 lemma add_lt_of_lt_sub_right {a b c : α} (h : a < c - b) : a + b < c :=
 begin
-  note h := add_lt_add_right h b,
+  have h := add_lt_add_right h b,
   rwa sub_add_cancel at h
 end
 
 lemma lt_sub_right_of_add_lt {a b c : α} (h : a + b < c) : a < c - b :=
 begin
-  note h := add_lt_add_right h (-b),
+  have h := add_lt_add_right h (-b),
   rwa add_neg_cancel_right at h
 end
 
 lemma lt_add_of_neg_add_lt {a b c : α} (h : -b + a < c) : a < b + c :=
 begin
-  note h := add_lt_add_left h b,
+  have h := add_lt_add_left h b,
   rwa add_neg_cancel_left at h
 end
 
 lemma neg_add_lt_of_lt_add {a b c : α} (h : a < b + c) : -b + a < c :=
 begin
-  note h := add_lt_add_left h (-b),
+  have h := add_lt_add_left h (-b),
   rwa neg_add_cancel_left at h
 end
 
 lemma lt_add_of_sub_left_lt {a b c : α} (h : a - b < c) : a < b + c :=
 begin
-  note h := add_lt_add_right h b,
+  have h := add_lt_add_right h b,
   rwa [sub_add_cancel, add_comm] at h
 end
 
 lemma sub_left_lt_of_lt_add {a b c : α} (h : a < b + c) : a - b < c :=
 begin
-  note h := add_lt_add_right h (-b),
+  have h := add_lt_add_right h (-b),
   rwa [add_comm b c, add_neg_cancel_right] at h
 end
 
 lemma lt_add_of_sub_right_lt {a b c : α} (h : a - c < b) : a < b + c :=
 begin
-  note h := add_lt_add_right h c,
+  have h := add_lt_add_right h c,
   rwa sub_add_cancel at h
 end
 
 lemma sub_right_lt_of_lt_add {a b c : α} (h : a < b + c) : a - c < b :=
 begin
-  note h := add_lt_add_right h (-c),
+  have h := add_lt_add_right h (-c),
   rwa add_neg_cancel_right at h
 end
 
@@ -556,7 +556,7 @@ lt_add_of_neg_add_lt_left (add_lt_of_lt_sub_right h)
 
 lemma neg_lt_sub_left_of_lt_add {a b c : α} (h : c < a + b) : -a < b - c :=
 begin
-  note h := lt_neg_add_of_add_lt (sub_left_lt_of_lt_add h),
+  have h := lt_neg_add_of_add_lt (sub_left_lt_of_lt_add h),
   rwa add_comm at h
 end
 
diff --git a/library/init/algebra/ordered_ring.lean b/library/init/algebra/ordered_ring.lean
index e620304e2a..8ea58dd681 100644
--- a/library/init/algebra/ordered_ring.lean
+++ b/library/init/algebra/ordered_ring.lean
@@ -313,7 +313,7 @@ lt_of_mul_lt_mul_left h3 nhc
 
 lemma zero_gt_neg_one : -1 < (0:α) :=
 begin
-  note this := neg_lt_neg (@zero_lt_one α _),
+  have this := neg_lt_neg (@zero_lt_one α _),
   rwa neg_zero at this
 end
 
diff --git a/library/init/category/state.lean b/library/init/category/state.lean
index a2949fcace..0d87965522 100644
--- a/library/init/category/state.lean
+++ b/library/init/category/state.lean
@@ -69,7 +69,7 @@ instance (σ : Type u) (m : Type u → Type v) [monad m] : monad (state_t σ m)
  id_map := begin
    intros, apply funext, intro,
    simp [state_t_bind, state_t_return, function.comp, return],
-   note h : state_t_bind._match_1 (λ (x : α) (s : σ), @pure m _ _ (x, s)) = pure,
+   have h : state_t_bind._match_1 (λ (x : α) (s : σ), @pure m _ _ (x, s)) = pure,
    { apply funext, intro s, cases s, apply rfl },
    { rw h, apply @monad.bind_pure _ σ },
  end,
diff --git a/library/init/data/array/lemmas.lean b/library/init/data/array/lemmas.lean
index f36494f82d..d66689e25c 100644
--- a/library/init/data/array/lemmas.lean
+++ b/library/init/data/array/lemmas.lean
@@ -55,7 +55,7 @@ theorem mem_iff_rev_list_mem_core (a : array α n) (v : α) : Π i (h : i ≤ n)
 | (i+1) h := let IH := mem_iff_rev_list_mem_core i (le_of_lt h) in
   ⟨λ⟨j, ji1, e⟩, or.elim (lt_or_eq_of_le $ nat.le_of_succ_le_succ ji1)
     (λji, list.mem_cons_of_mem _ $ IH.1 ⟨j, ji, e⟩)
-    (λje, by simp[iterate_aux]; apply or.inl; note H : j = ⟨i, h⟩ := fin.eq_of_veq je; rwa [-H, e]),
+    (λje, by simp[iterate_aux]; apply or.inl; have H : j = ⟨i, h⟩ := fin.eq_of_veq je; rwa [-H, e]),
   λm, begin
     simp[iterate_aux, list.mem] at m,
     cases m with e m',
diff --git a/library/init/data/char/lemmas.lean b/library/init/data/char/lemmas.lean
index 818cd5201b..44495791ca 100644
--- a/library/init/data/char/lemmas.lean
+++ b/library/init/data/char/lemmas.lean
@@ -18,7 +18,7 @@ begin
   unfold of_nat,
   cases (nat.decidable_lt n char_sz),
   {reflexivity},
-  {note h' := not_lt_of_ge h, contradiction}
+  {have h' := not_lt_of_ge h, contradiction}
 end
 
 lemma of_nat_eq_of_ge {n : nat} : n ≥ char_sz → of_nat n = of_nat 0 :=
diff --git a/library/init/data/fin/ops.lean b/library/init/data/fin/ops.lean
index 8b99db91cf..f193384c26 100644
--- a/library/init/data/fin/ops.lean
+++ b/library/init/data/fin/ops.lean
@@ -38,7 +38,7 @@ private lemma modlt {a b n : nat} (h₁ : a < n) (h₂ : b < n) : a % b < n :=
 begin
   cases b with b,
   {simp [mod_zero], assumption},
-  {note h : a % (succ b) < succ b,
+  {have h : a % (succ b) < succ b,
    apply nat.mod_lt _ (nat.zero_lt_succ _),
    exact lt.trans h h₂}
 end
@@ -110,8 +110,8 @@ lemma val_zero : (0 : fin (succ n)).val = 0 := rfl
 def pred {n : nat} : ∀ i : fin (succ n), i ≠ 0 → fin n
 | ⟨a, h₁⟩ h₂ := ⟨a.pred,
   begin
-    note this : a ≠ 0,
-    { note aux₁ := vne_of_ne h₂,
+    have this : a ≠ 0,
+    { have aux₁ := vne_of_ne h₂,
       dsimp at aux₁, rw val_zero at aux₁, exact aux₁ },
     exact nat.pred_lt_pred this (nat.succ_ne_zero n) h₁
   end⟩
diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean
index 996292aff4..2d69c3757a 100644
--- a/library/init/data/int/basic.lean
+++ b/library/init/data/int/basic.lean
@@ -130,14 +130,14 @@ lemma sub_nat_nat_elim (m n : ℕ) (P : ℕ → ℕ → ℤ → Prop)
   (hn : ∀i m, P m (m + i + 1) (-[1+ i])) :
   P m n (sub_nat_nat m n) :=
 begin
-  note H : ∀k, n - m = k → P m n (nat.cases_on k (of_nat (m - n)) (λa, -[1+ a])),
+  have H : ∀k, n - m = k → P m n (nat.cases_on k (of_nat (m - n)) (λa, -[1+ a])),
   { intro k, cases k,
     { intro e,
       cases (nat.le.dest (nat.le_of_sub_eq_zero e)) with k h,
       rw [h.symm, nat.add_sub_cancel_left],
       apply hp },
     { intro heq,
-      note h : m ≤ n,
+      have h : m ≤ n,
       { exact nat.le_of_lt (nat.lt_of_sub_eq_succ heq) },
       rw [nat.sub_eq_iff_eq_add h] at heq,
       rw [heq, add_comm],
diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean
index 49b35c2ca4..6f6c74a753 100644
--- a/library/init/data/int/order.lean
+++ b/library/init/data/int/order.lean
@@ -75,7 +75,7 @@ lemma coe_zero_le (n : ℕ) : 0 ≤ (↑n : ℤ) :=
 coe_nat_le_coe_nat_of_le n.zero_le
 
 lemma eq_coe_of_zero_le {a : ℤ} (h : 0 ≤ a) : ∃ n : ℕ, a = n :=
-by note t := le.dest_sub h; simp at t; exact t
+by have t := le.dest_sub h; simp at t; exact t
 
 lemma lt_add_succ (a : ℤ) (n : ℕ) : a < a + ↑(nat.succ n) :=
 le.intro (show a + 1 + n = a + nat.succ n, begin simp [int.coe_nat_eq], reflexivity end)
diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean
index 328792eb1a..4b51ef669b 100644
--- a/library/init/data/list/lemmas.lean
+++ b/library/init/data/list/lemmas.lean
@@ -146,9 +146,9 @@ theorem nth_ge_len : Π (l : list α) (n), n ≥ length l → nth l n = none
 
 theorem ext : Π {l₁ l₂ : list α}, (∀n, nth l₁ n = nth l₂ n) → l₁ = l₂
 | []      []       h := rfl
-| (a::l₁) []       h := by note h0 := h 0; contradiction
-| []      (a'::l₂) h := by note h0 := h 0; contradiction
-| (a::l₁) (a'::l₂) h := by note h0 : some a = some a' := h 0; injection h0 with aa; simph[ext $ λn, h (n+1)]
+| (a::l₁) []       h := by have h0 := h 0; contradiction
+| []      (a'::l₂) h := by have h0 := h 0; contradiction
+| (a::l₁) (a'::l₂) h := by have h0 : some a = some a' := h 0; injection h0 with aa; simph[ext $ λn, h (n+1)]
 
 theorem ext_le {l₁ l₂ : list α} (hl : length l₁ = length l₂) (h : ∀n h₁ h₂, nth_le l₁ n h₁ = nth_le l₂ n h₂) : l₁ = l₂ :=
 ext $ λn, if h₁ : n < length l₁
@@ -243,13 +243,13 @@ lemma nth_le_reverse_aux2 : Π (l r : list α) (i : nat) (h1) (h2),
   nth_le (reverse_core l r) (length l - 1 - i) h1 = nth_le l i h2
 | []       r i     h1 h2 := absurd h2 (not_lt_zero _)
 | (a :: l) r 0     h1 h2 := begin
-    note aux := nth_le_reverse_aux1 l (a :: r) 0,
+    have aux := nth_le_reverse_aux1 l (a :: r) 0,
     rw zero_add at aux,
     exact aux _ (zero_lt_succ _)
   end
 | (a :: l) r (i+1) h1 h2 := begin
-    note aux := nth_le_reverse_aux2 l (a :: r) i,
-    note heq := calc length (a :: l) - 1 - (i + 1)
+    have aux := nth_le_reverse_aux2 l (a :: r) i,
+    have heq := calc length (a :: l) - 1 - (i + 1)
           = length l - (1 + i) : by rw add_comm; refl
       ... = length l - 1 - i   : by rw nat.sub_sub,
     rw -heq at aux,
@@ -270,7 +270,7 @@ by {induction l; intros, contradiction, simph, reflexivity}
 @[simp] lemma last_append {a : α} (l : list α) (h : l ++ [a] ≠ []) : last (l ++ [a]) h = a :=
 begin
   induction l with hd tl ih; rsimp,
-  note haux : tl ++ [a] ≠ [],
+  have haux : tl ++ [a] ≠ [],
     {apply append_ne_nil_of_ne_nil_right, contradiction},
   simph
 end
@@ -735,7 +735,7 @@ by simp [sublists]; exact
       (sublist_of_cons_sublist sl) _ hs
   end,
 λsl, begin
-  note this : ∀ {a : α} {y t}, y ∈ t → y ∈ foldr (λ ys r, ys :: (a :: ys) :: r) nil t
+  have this : ∀ {a : α} {y t}, y ∈ t → y ∈ foldr (λ ys r, ys :: (a :: ys) :: r) nil t
                                   ∧ a :: y ∈ foldr (λ ys r, ys :: (a :: ys) :: r) nil t,
   { intros a y t yt, induction t with x t IH, exact absurd yt (not_mem_nil _),
     simp, simp at yt, cases yt with yx yt,
diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean
index dd25ea4b2e..d9c9d77096 100644
--- a/library/init/data/nat/bitwise.lean
+++ b/library/init/data/nat/bitwise.lean
@@ -94,7 +94,7 @@ namespace nat
   def binary_rec {C : nat → Sort u} (f : ∀ b n, C n → C (bit b n)) (z : C 0) : Π n, C n
   | n := if n0 : n = 0 then by rw n0; exact z else let n' := shiftr n 1 in
     have n' < n, from (div_lt_iff_lt_mul _ _ dec_trivial).2 $
-    by note := nat.mul_lt_mul_of_pos_left (dec_trivial : 1 < 2)
+    by have := nat.mul_lt_mul_of_pos_left (dec_trivial : 1 < 2)
          (lt_of_le_of_ne (zero_le _) (ne.symm n0));
        rwa mul_one at this,
     by rw [-show bit (bodd n) n' = n, from bit_decomp n]; exact 
@@ -126,7 +126,7 @@ namespace nat
     { generalize (binary_rec._main._pack._proof_2 (bit b n)) e,
       rw [bodd_bit, shiftr1_bit], intro e, refl },
     { generalize (binary_rec._main._pack._proof_1 (bit b n) b0) e,
-      note bf := bodd_bit b n, note n0 := shiftr1_bit b n,
+      have bf := bodd_bit b n, have n0 := shiftr1_bit b n,
       rw b0 at bf n0, rw [-show ff = b, from bf, -show 0 = n, from n0], intro e,
       exact h.symm },
   end
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index 3d9c53dbc3..cb97b0a50d 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -879,12 +879,12 @@ nat.strong_induction_on a $ λ n,
 
 /- mod -/
 lemma mod_def (x y : nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
-by note h := mod_def_aux x y; rwa [dif_eq_if] at h
+by have h := mod_def_aux x y; rwa [dif_eq_if] at h
 
 lemma mod_zero (a : nat) : a % 0 = a :=
 begin
   rw mod_def,
-  note h : ¬ (0 < 0 ∧ 0 ≤ a),
+  have h : ¬ (0 < 0 ∧ 0 ≤ a),
   simp [lt_irrefl],
   simp [if_neg, h]
 end
@@ -892,7 +892,7 @@ end
 lemma mod_eq_of_lt {a b : nat} (h : a < b) : a % b = a :=
 begin
   rw mod_def,
-  note h' : ¬(0 < b ∧ b ≤ a),
+  have h' : ¬(0 < b ∧ b ≤ a),
   simp [not_le_of_gt h],
   simp [if_neg, h']
 end
@@ -900,7 +900,7 @@ end
 @[simp] lemma zero_mod (b : nat) : 0 % b = 0 :=
 begin
   rw mod_def,
-  note h : ¬(0 < b ∧ b ≤ 0),
+  have h : ¬(0 < b ∧ b ≤ 0),
   {intro hn, cases hn with l r, exact absurd (lt_of_lt_of_le l r) (lt_irrefl 0)},
   simp [if_neg, h]
 end
@@ -917,9 +917,9 @@ begin
   {apply or.elim (decidable.em (succ x < y)),
     {intro h₁, rwa [mod_eq_of_lt h₁]},
     {intro h₁,
-      note h₁ : succ x % y = (succ x - y) % y, {exact mod_eq_sub_mod (le_of_not_gt h₁)},
-      note this : succ x - y ≤ x, {exact le_of_lt_succ (sub_lt (succ_pos x) h)},
-      note h₂ : (succ x - y) % y < y, {exact ih _ this},
+      have h₁ : succ x % y = (succ x - y) % y, {exact mod_eq_sub_mod (le_of_not_gt h₁)},
+      have this : succ x - y ≤ x, {exact le_of_lt_succ (sub_lt (succ_pos x) h)},
+      have h₂ : (succ x - y) % y < y, {exact ih _ this},
       rwa -h₁ at h₂}}
 end
 
@@ -977,7 +977,7 @@ by rw [mul_comm x z, mul_comm y z, mul_comm (x % y) z]; apply mul_mod_mul_left
 lemma mod_two_eq_zero_or_one (n : ℕ)
 : n % 2 = 0 ∨ n % 2 = 1 :=
 begin
-  note h : ((n % 2 < 1) ∨ (n % 2 = 1)),
+  have h : ((n % 2 < 1) ∨ (n % 2 = 1)),
   { apply lt_or_eq_of_le,
     apply nat.le_of_succ_le_succ,
     apply @nat.mod_lt n 2 (nat.le_succ _) },
@@ -1004,11 +1004,11 @@ lemma sub_mul_mod (x k n : ℕ) (h₁ : n*k ≤ x) : (x - n*k) % n = x % n :=
 begin
   induction k with k,
   { simp },
-  { note h₂ : n * k ≤ x,
+  { have h₂ : n * k ≤ x,
     { rw [mul_succ] at h₁,
       apply nat.le_trans _ h₁,
       apply le_add_right _ n },
-    note h₄ : x - n * k ≥ n,
+    have h₄ : x - n * k ≥ n,
     { apply @nat.le_of_add_le_add_right (n*k),
       rw [nat.sub_add_cancel h₂],
       simp [mul_succ] at h₁, simp [h₁] },
@@ -1017,7 +1017,7 @@ end
 
 /- div & mod -/
 lemma div_def (x y : nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
-by note h := div_def_aux x y; rwa dif_eq_if at h
+by have h := div_def_aux x y; rwa dif_eq_if at h
 
 lemma mod_add_div (m k : ℕ)
 : m % k + k * (m / k) = m :=
@@ -1027,7 +1027,7 @@ begin
   intros m IH,
   cases decidable.em (0 < k ∧ k ≤ m) with h h',
   -- 0 < k ∧ k ≤ m
-  { note h' : m - k < m,
+  { have h' : m - k < m,
     { apply nat.sub_lt _ h.left,
       apply lt_of_lt_of_le h.left h.right },
     rw [div_def, mod_def, if_pos h, if_pos h],
@@ -1078,11 +1078,11 @@ begin
   { rw [h₀, nat.div_zero, nat.div_zero, nat.zero_sub] },
   { induction p with p,
     { simp },
-    { note h₂ : n*p ≤ x,
+    { have h₂ : n*p ≤ x,
       { transitivity,
         { apply nat.mul_le_mul_left, apply le_succ },
         { apply h₁ } },
-      note h₃ : x - n * p ≥ n,
+      have h₃ : x - n * p ≥ n,
       { apply le_of_add_le_add_right,
         rw [nat.sub_add_cancel h₂, add_comm],
         rw [mul_succ] at h₁,
@@ -1130,7 +1130,7 @@ begin
   { rw [div_eq_sub_div Hk h],
     cases x with x,
     { simp [zero_mul, zero_le_iff_true] },
-    { note Hlt : y - k < y,
+    { have Hlt : y - k < y,
       { apply sub_lt_of_pos_le ; assumption },
       rw [ -add_one_eq_succ
          , nat.add_le_add_iff_le_right
@@ -1232,7 +1232,7 @@ end
 
 theorem pow_lt_pow_of_lt_right {x : ℕ} (H : x > 1) {i j} (h : i < j) : x^i < x^j :=
 begin
-  note xpos := lt_of_succ_lt H,
+  have xpos := lt_of_succ_lt H,
   refine lt_of_lt_of_le _ (pow_le_pow_of_le_right xpos h),
   rw [-mul_one (x^i), pow_succ],
   exact nat.mul_lt_mul_of_pos_left H (pos_pow_of_pos _ xpos)
@@ -1248,7 +1248,7 @@ begin
   intros p IH,
   cases lt_or_ge p (b^succ w) with h₁ h₁,
   -- base case: p < b^succ w
-  { note h₂ : p / b < b^w,
+  { have h₂ : p / b < b^w,
     { rw [div_lt_iff_lt_mul p _ b_pos],
       simp [pow_succ] at h₁,
       simp [h₁] },
@@ -1256,7 +1256,7 @@ begin
     simp [mod_add_div] },
   -- step: p ≥ b^succ w
   { -- Generate condiition for induction principal
-    note h₂ : p - b^succ w < p,
+    have h₂ : p - b^succ w < p,
     { apply sub_lt_of_pos_le _ _ (pos_pow_of_pos _ b_pos) h₁ },
 
     -- Apply induction
@@ -1267,7 +1267,7 @@ begin
     -- Pull subtraction outside mod and div
     rw [sub_mul_mod _ _ _ h₁, sub_mul_div _ _ _ h₁],
     -- Cancel subtraction inside mod b^w
-    note p_b_ge :  b^w ≤ p / b,
+    have p_b_ge :  b^w ≤ p / b,
     { rw [le_div_iff_mul_le _ _ b_pos],
       simp [h₁] },
     rw [eq.symm (mod_eq_sub_mod p_b_ge)] }
diff --git a/library/init/data/option_t.lean b/library/init/data/option_t.lean
index 5d57ee55d4..58829bf8ec 100644
--- a/library/init/data/option_t.lean
+++ b/library/init/data/option_t.lean
@@ -29,7 +29,7 @@ instance {m : Type u → Type v} [monad m] : monad (option_t m) :=
  id_map := begin
    intros,
    simp [option_t_bind, function.comp],
-   note h : option_t_bind._match_1 option_t_return = @pure m _ (option α),
+   have h : option_t_bind._match_1 option_t_return = @pure m _ (option α),
    { apply funext, intro s, cases s, refl, refl },
    { simp [h], apply @monad.bind_pure _ (option α) m },
  end,
diff --git a/library/init/data/sigma/lex.lean b/library/init/data/sigma/lex.lean
index 6a75220db3..7daa175c84 100644
--- a/library/init/data/sigma/lex.lean
+++ b/library/init/data/sigma/lex.lean
@@ -40,7 +40,7 @@ section
                 (λ (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb),
                   begin
                     subst eq₂,
-                    note new_eq₃ := eq_of_heq eq₃,
+                    have new_eq₃ := eq_of_heq eq₃,
                     subst new_eq₃,
                     exact ihb b₁ h
                   end),
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index dd12bfc000..d9098f9ad7 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -448,11 +448,14 @@ tactic.focus [tac]
 
 /--
 This tactic applies to any goal.
-- `note h : T := p` adds a new hypothesis of name `h` and type `T` to the current goal if `p` a term of type `T`.
-- `note h : T` adds a new hypothesis of name `h` and type `T` to the current goal and opens a new subgoal with target `T`.
-The new subgoal becomes the main goal.
+- `have h : T := p` adds the hypothesis `h : T` to the current goal if `p` a term of type `T`.
+If `T` is omitted, it will be inferred.
+- `have h : T` adds the hypothesis `h : T` to the current goal and opens a new subgoal with target `T`.
+The new subgoal becomes the main goal. If `T` is omitted, it will be replaced by a fresh meta variable.
+
+If `h` is omitted, it defaults to `this`.
 -/
-meta def note (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
+meta def have_tac (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
 let h := h.get_or_else `this in
 match q₁, q₂ with
 | some e, some p := do
@@ -469,7 +472,16 @@ match q₁, q₂ with
   tactic.assert h e
 end >> skip
 
-meta def define (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
+/--
+This tactic applies to any goal.
+- `let h : T := p` adds the hypothesis `h : T := p` to the current goal if `p` a term of type `T`.
+If `T` is omitted, it will be inferred.
+- `let h : T` adds the hypothesis `h : T := ?M` to the current goal and opens a new subgoal `?M : T`.
+The new subgoal becomes the main goal. If `T` is omitted, it will be replaced by a fresh meta variable.
+
+If `h` is omitted, it defaults to `this`.
+-/
+meta def let_tac (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : tactic unit :=
 let h := h.get_or_else `this in
 match q₁, q₂ with
 | some e, some p := do
@@ -849,16 +861,16 @@ tactic.by_contradiction >> return ()
 meta def done : tactic unit :=
 tactic.done
 
-private meta def show_goal_aux (p : pexpr) : list expr → list expr → tactic unit
-| []      r := fail "show_goal tactic failed"
+private meta def show_tac_aux (p : pexpr) : list expr → list expr → tactic unit
+| []      r := fail "show tactic failed"
 | (g::gs) r := do
   do {set_goals [g], g_ty ← target, ty ← i_to_expr p, unify g_ty ty, set_goals (g :: r.reverse ++ gs), tactic.change ty}
   <|>
-  show_goal_aux gs (g::r)
+  show_tac_aux gs (g::r)
 
-meta def show_goal (q : parse texpr) : tactic unit :=
+meta def show_tac (q : parse texpr) : tactic unit :=
 do gs ← get_goals,
-   show_goal_aux q gs []
+   show_tac_aux q gs []
 
 end interactive
 end tactic
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index c3a184f4f2..b6535d4bc8 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -77,7 +77,7 @@ tactic.interactive.change q none (loc.ns [])
 meta def exact (q : parse texpr) : smt_tactic unit :=
 tactic.interactive.exact q
 
-meta def note (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
+meta def have_tac (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
 let h := h.get_or_else `this in
 match q₁, q₂ with
 | some e, some p := do
@@ -94,7 +94,7 @@ match q₁, q₂ with
   smt_tactic.assert h e
 end >> return ()
 
-meta def define (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
+meta def let_tac (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) (q₂ : parse $ (tk ":=" *> texpr)?) : smt_tactic unit :=
 let h := h.get_or_else `this in
 match q₁, q₂ with
 | some e, some p := do
diff --git a/library/init/native/result.lean b/library/init/native/result.lean
index a46b20fba7..0f9e058262 100644
--- a/library/init/native/result.lean
+++ b/library/init/native/result.lean
@@ -50,7 +50,7 @@ section resultT
    id_map := begin
      intros, cases x,
      dsimp [resultT.and_then],
-     note h : @resultT.and_then._match_1 _ m E α _ resultT.pure = pure,
+     have h : @resultT.and_then._match_1 _ m E α _ resultT.pure = pure,
      { apply funext, intro x,
        cases x; simp [resultT.and_then, resultT.pure, resultT.and_then] },
      { rw [h, @monad.bind_pure _ (result E α) _] },
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index 57299fd2da..1584536e01 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -115,9 +115,36 @@ name get_interactive_tactic_full_name(name const & tac_class, name const & tac)
     return name(tac_class, "interactive") + tac;
 }
 
+static bool is_curr_exact_shortcut(parser & p) {
+    return
+            p.curr_is_token(get_assume_tk()) ||
+            p.curr_is_token(get_calc_tk()) ||
+            p.curr_is_token(get_suppose_tk());
+}
+
+static bool is_keyword_tactic(parser & p) {
+    return
+            p.curr_is_token(get_let_tk()) ||
+            p.curr_is_token(get_have_tk()) ||
+            p.curr_is_token(get_show_tk());
+}
+
 static optional<name> is_interactive_tactic(parser & p, name const & tac_class) {
-    if (!p.curr_is_identifier()) return optional<name>();
-    name id = get_interactive_tactic_full_name(tac_class, p.get_name_val());
+    name id;
+    switch (p.curr()) {
+        case token_kind::Identifier:
+            id = p.get_name_val();
+            break;
+        case token_kind::Keyword:
+            if (is_keyword_tactic(p)) {
+                id = p.get_token_info().value().append_after("_tac");
+                break;
+            }
+            /* fall through */
+        default:
+            return {};
+    }
+    id = get_interactive_tactic_full_name(tac_class, id);
     if (p.env().find(id))
         return optional<name>(id);
     else
@@ -178,14 +205,6 @@ static expr parse_interactive_tactic(parser & p, name const & decl_name, name co
     return mk_tactic_step(p, r, pos, pos, tac_class, use_istep);
 }
 
-static bool is_curr_exact_shortcut(parser & p) {
-    return
-        p.curr_is_token(get_have_tk()) ||
-        p.curr_is_token(get_assume_tk()) ||
-        p.curr_is_token(get_calc_tk()) ||
-        p.curr_is_token(get_suppose_tk());
-}
-
 static expr mk_tactic_unit(name const & tac_class) {
     return mk_app(mk_constant(tac_class), mk_constant(get_unit_name()));
 }
@@ -246,11 +265,6 @@ struct parse_tactic_fn {
                 }
                 throw;
             }
-        } else if (m_p.curr_is_token(get_show_tk())) {
-            m_p.next();
-            expr arg = parse_qexpr();
-            r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "show_goal")), pos), arg, pos);
-            if (m_use_istep) r = mk_tactic_istep(m_p, r, pos, pos, m_tac_class);
         } else if (is_curr_exact_shortcut(m_p)) {
             expr arg = parse_qexpr();
             r = m_p.mk_app(m_p.save_pos(mk_constant(get_interactive_tactic_full_name(m_tac_class, "exact")), pos), arg, pos);
diff --git a/tests/lean/1207.lean b/tests/lean/1207.lean
index ec1305b458..01957fa371 100644
--- a/tests/lean/1207.lean
+++ b/tests/lean/1207.lean
@@ -1,12 +1,12 @@
 example : true :=
 begin
-  note H : true := (by trivial),
+  have H : true := (by trivial),
   exact H
 end
 
 example : true :=
 begin
-  note H : true := (by tactic.triv),
+  have H : true := (by tactic.triv),
   exact H
 end
 
@@ -18,13 +18,13 @@ end
 
 example : false :=
 begin
-  note H : true := (by foo), -- ERROR
+  have H : true := (by foo), -- ERROR
   exact sorry
 end
 
 constant P : Prop
 example (p : P) : true :=
 begin
-  note H : P := by do { p ← tactic.get_local `p, tactic.exact p },
+  have H : P := by do { p ← tactic.get_local `p, tactic.exact p },
   trivial
 end
diff --git a/tests/lean/1467.lean b/tests/lean/1467.lean
index aedd2a448b..d3be6badbe 100644
--- a/tests/lean/1467.lean
+++ b/tests/lean/1467.lean
@@ -3,8 +3,8 @@ axiom H_f_g : ∀ n, f (g n) = n
 
 example (m : ℕ) : h m = h m :=
 begin
-define n : ℕ := g m,
-note H : f n = m := begin dsimp, rw H_f_g end,
+let n : ℕ := g m,
+have H : f n = m := begin dsimp, rw H_f_g end,
 subst H, -- Error here
 end
 
@@ -12,16 +12,16 @@ set_option pp.instantiate_mvars false
 
 example (m : ℕ) : h m = h m :=
 begin
-define n : ℕ, -- add metavar
+let n : ℕ, -- add metavar
 exact g m,
-note H : f n = m := begin dsimp, rw H_f_g end,
+have H : f n = m := begin dsimp, rw H_f_g end,
 subst H, -- Error here
 end
 
 example (m : ℕ) : h m = h m :=
 begin
-define n : ℕ := g m,
-note H : f n = m := begin dsimp, rw H_f_g end,
+let n : ℕ := g m,
+have H : f n = m := begin dsimp, rw H_f_g end,
 subst m, -- Error here
 end
 
@@ -29,15 +29,15 @@ set_option pp.instantiate_mvars false
 
 example (m : ℕ) : h m = h m :=
 begin
-define n : ℕ, -- add metavar
+let n : ℕ, -- add metavar
 exact g m,
-note H : f n = m := begin dsimp, rw H_f_g end,
+have H : f n = m := begin dsimp, rw H_f_g end,
 subst m, -- Error here
 end
 
 example (m p: ℕ) : h m = h m :=
 begin
-define a : ℕ := g p,
-define n : ℕ := g a,
+let a : ℕ := g p,
+let n : ℕ := g a,
 clear p -- Error here
 end
diff --git a/tests/lean/auto_quote_error2.lean b/tests/lean/auto_quote_error2.lean
index 9cfd358ca4..c177715843 100644
--- a/tests/lean/auto_quote_error2.lean
+++ b/tests/lean/auto_quote_error2.lean
@@ -48,6 +48,6 @@ end
 
 example : true :=
 begin
-  { note h' := eq.refl _ },
+  { have h' := eq.refl _ },
                        --^ error should be at `}`
-end
\ No newline at end of file
+end
diff --git a/tests/lean/run/assert_tac1.lean b/tests/lean/run/assert_tac1.lean
index 991d4499b5..b49179aad1 100644
--- a/tests/lean/run/assert_tac1.lean
+++ b/tests/lean/run/assert_tac1.lean
@@ -28,7 +28,7 @@ by do
 
 definition tst3 (a : nat) : a = a :=
 begin
-  define x : nat,
+  let x : nat,
   exact a,
   revert x,
   intro y,
diff --git a/tests/lean/run/assert_tac3.lean b/tests/lean/run/assert_tac3.lean
index 3584f8497c..46caddb67b 100644
--- a/tests/lean/run/assert_tac3.lean
+++ b/tests/lean/run/assert_tac3.lean
@@ -26,7 +26,7 @@ by do
 
 definition tst4 (a : nat) : a = a :=
 begin
-  note x : nat,
+  have x : nat,
   rotate 1,
   exact eq.refl a,
   exact a
@@ -34,14 +34,14 @@ end
 
 definition tst5 (a : nat) : a = a :=
 begin
-  define x : nat := a,
+  let x : nat := a,
   trace_state,
   exact eq.refl x
 end
 
 definition tst6 (a : nat) : a = a :=
 begin
-  define x := a,
+  let x := a,
   trace_state,
   exact eq.refl x
 end
diff --git a/tests/lean/run/cases_nested.lean b/tests/lean/run/cases_nested.lean
index 67e28b55fc..5be973ce0d 100644
--- a/tests/lean/run/cases_nested.lean
+++ b/tests/lean/run/cases_nested.lean
@@ -18,7 +18,7 @@ lemma ex (t : term) (h : cidx t = 2) : term.app (tid t) (to_list t) = t :=
 begin
   cases t,
   {simp [cidx] at h,
-   note h : 1 ≠ 2, tactic.comp_val,
+   have h : 1 ≠ 2, tactic.comp_val,
    contradiction},
   {simp [tid, to_list]}
 end
diff --git a/tests/lean/run/cc_constructors.lean b/tests/lean/run/cc_constructors.lean
index 38b6e83701..a1f370febc 100644
--- a/tests/lean/run/cc_constructors.lean
+++ b/tests/lean/run/cc_constructors.lean
@@ -25,7 +25,7 @@ begin
      constructor applications. So, the following one should fail. -/
   try {cc},
   /- Complete it manually. TODO(Leo): we can automate it for inhabited types. -/
-  note h := congr_fun h1 [],
+  have h := congr_fun h1 [],
   cc
 end
 
@@ -39,7 +39,7 @@ begin
   /- In the current implementation, cc does not "complete" partially applied
      constructor applications. So, the following one should fail. -/
   try {cc},
-  note h := congr_fun h1 0,
+  have h := congr_fun h1 0,
   cc
 end
 
diff --git a/tests/lean/run/destruct.lean b/tests/lean/run/destruct.lean
index 1763337ec3..7360c9cadf 100644
--- a/tests/lean/run/destruct.lean
+++ b/tests/lean/run/destruct.lean
@@ -16,8 +16,8 @@ axiom fax2 {α : Type u} {n : nat} (v : Vec α (nat.succ n)) : f v = 1
 example {α : Type u} {n : nat} (v : Vec α n) : f v ≠ 2 :=
 begin
   destruct v,
-  {intros, intro, note h := fax1 α, cc},
-  intros n1 h t, intros, intro, note h := fax2 (Vec.cons h t), cc
+  {intros, intro, have h := fax1 α, cc},
+  intros n1 h t, intros, intro, have h := fax2 (Vec.cons h t), cc
 end
 
 open nat
@@ -25,6 +25,6 @@ example : ∀ n, 0 < n → succ (pred n) = n :=
 begin
   intro n,
   destruct n,
-   {dsimp, intros, note h := lt_irrefl 0, cc},
+   {dsimp, intros, have h := lt_irrefl 0, cc},
    {intros, subst n, dsimp, reflexivity}
 end
diff --git a/tests/lean/run/doc_string4.lean b/tests/lean/run/doc_string4.lean
index e46d5057b9..8f643043af 100644
--- a/tests/lean/run/doc_string4.lean
+++ b/tests/lean/run/doc_string4.lean
@@ -123,8 +123,8 @@ lemma aval_asimp_const₃ : ∀ (a : aexp) (s : state), aval (asimp_const a) s =
 | (var x) s := rfl
 | (plus a₁ a₂) s :=
   begin
-   note h₁ := aval_asimp_const₃ a₁ s,
-   note h₂ := aval_asimp_const₃ a₂ s,
+   have h₁ := aval_asimp_const₃ a₁ s,
+   have h₂ := aval_asimp_const₃ a₂ s,
    unfold asimp_const aval,
    rewrite [-h₁, -h₂],
    cases (asimp_const a₁); cases (asimp_const a₂); repeat {reflexivity}
diff --git a/tests/lean/run/overload2.lean b/tests/lean/run/overload2.lean
index f6a2031a03..221d25091c 100644
--- a/tests/lean/run/overload2.lean
+++ b/tests/lean/run/overload2.lean
@@ -22,39 +22,39 @@ open F2 nat
 
 example :  true :=
 begin
- note H : (1 : nat) + (1 : nat) = 2,
+ have H : (1 : nat) + (1 : nat) = 2,
  reflexivity,
  constructor
 end
 
 example :  true :=
 begin
- note H : 1 + 1 = 2,
+ have H : 1 + 1 = 2,
  reflexivity,
  constructor
 end
 
 example :  true :=
 begin
- note H : (1:nat) + 1 = 2,
+ have H : (1:nat) + 1 = 2,
  reflexivity,
  constructor
 end
 
 example :  true :=
 begin
- note H : I + O = I,
+ have H : I + O = I,
  reflexivity,
  constructor
 end
 
 example :  true :=
 begin
- note H1 : I + O = I,
+ have H1 : I + O = I,
  reflexivity,
- note H2 : 1 + 0 = 1,
+ have H2 : 1 + 0 = 1,
  reflexivity,
- note H3 : (1:int) + 0 = 1,
+ have H3 : (1:int) + 0 = 1,
  reflexivity,
  constructor
 end
diff --git a/tests/lean/run/show_goal.lean b/tests/lean/run/show_goal.lean
index 551cb5b4b7..6480a347a8 100644
--- a/tests/lean/run/show_goal.lean
+++ b/tests/lean/run/show_goal.lean
@@ -1,14 +1,6 @@
 open tactic
 
 lemma ex1 (a b c : nat) : a + 0 = 0 + a ∧ 0 + b = b ∧ c + b = b + c :=
-begin
-  repeat {any_goals {constructor}},
-  show_goal c + b = b + c, { apply add_comm },
-  show_goal a + 0 = 0 + a, { simp },
-  show_goal 0 + b = b,     { rw [zero_add] }
-end
-
-lemma ex2 (a b c : nat) : a + 0 = 0 + a ∧ 0 + b = b ∧ c + b = b + c :=
 begin
   repeat {any_goals {constructor}},
   show c + b = b + c, { apply add_comm },
diff --git a/tests/lean/run/simp_univ_metavars.lean b/tests/lean/run/simp_univ_metavars.lean
index c6b738808c..74aa45569e 100644
--- a/tests/lean/run/simp_univ_metavars.lean
+++ b/tests/lean/run/simp_univ_metavars.lean
@@ -38,8 +38,8 @@ lemma NaturalTransformations_componentwise_equal
   begin
     induction α with αc,
     induction β with βc,
-    have hc : αc = βc, from funext w,
-    by subst hc
+    have hc : αc = βc := funext w,
+    subst hc
   end
 
 @[simp]
diff --git a/tests/lean/run/smt_assert_define.lean b/tests/lean/run/smt_assert_define.lean
index 675ae56b75..f24446b574 100644
--- a/tests/lean/run/smt_assert_define.lean
+++ b/tests/lean/run/smt_assert_define.lean
@@ -35,6 +35,6 @@ end
 lemma ex4 (a b c : nat) : a = b → p (f a) (f b) → p a b :=
 begin [smt]
   intros,
-  note h : p (f a) (f a),
+  have h : p (f a) (f a),
   add_fact (pf _ h)
 end
diff --git a/tests/lean/run/smt_destruct.lean b/tests/lean/run/smt_destruct.lean
index d7455dc520..1a118e10a3 100644
--- a/tests/lean/run/smt_destruct.lean
+++ b/tests/lean/run/smt_destruct.lean
@@ -11,7 +11,7 @@ by using_smt $ do
 lemma ex2 (p q : Prop) : p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → false :=
 begin [smt]
    intros,
-   note h : p ∨ q,
+   have h : p ∨ q,
    destruct h
 end
 
diff --git a/tests/lean/run/smt_ematch1.lean b/tests/lean/run/smt_ematch1.lean
index 0ac8bb12e8..7046a0d2fa 100644
--- a/tests/lean/run/smt_ematch1.lean
+++ b/tests/lean/run/smt_ematch1.lean
@@ -44,7 +44,7 @@ end
 lemma ex6 (a b c d e : nat) : (∀ x, g x (f x) = 0) → a = f b → g b a + 0 = f 0 :=
 begin [smt]
    intros,
-   note h : ∀ x, g x (f x) = 0,
+   have h : ∀ x, g x (f x) = 0,
    add_lemma [h, fax, add_zero],
    ematch
 end
@@ -52,7 +52,7 @@ end
 lemma ex7 (a b c d e : nat) : (∀ x, g x (f x) = 0) → a = f b → g b a + 0 = f 0 :=
 begin [smt]
    intros,
-   note h : ∀ x, g x (f x) = 0,
+   have h : ∀ x, g x (f x) = 0,
    ematch_using [h, fax, add_zero]
 end
 
diff --git a/tests/lean/run/tactic_mode_scope_bug.lean b/tests/lean/run/tactic_mode_scope_bug.lean
index 7f9c19205e..a4c33e8717 100644
--- a/tests/lean/run/tactic_mode_scope_bug.lean
+++ b/tests/lean/run/tactic_mode_scope_bug.lean
@@ -1,15 +1,15 @@
 example (p q : Prop) : p ∧ q → q ∧ p :=
 begin
   intro h,
-  have hp : p, from h^.left,
-  have hq : q, from h^.right,
-  ⟨hq, hp⟩
+  have hp : p := h^.left,
+  have hq : q := h^.right,
+  exact ⟨hq, hp⟩
 end
 
 example (p q : Prop) (hp : q) (hq : p) : p ∧ q → q ∧ p :=
 begin
   intro h,
-  have hp : p, from h^.left,
-  have hq : q, from h^.right,
-  ⟨hq, hp⟩
+  have hp : p := h^.left,
+  have hq : q := h^.right,
+  exact ⟨hq, hp⟩
 end
diff --git a/tests/lean/run/term_app2.lean b/tests/lean/run/term_app2.lean
index 45922f8d09..488cee002c 100644
--- a/tests/lean/run/term_app2.lean
+++ b/tests/lean/run/term_app2.lean
@@ -1,15 +1,15 @@
 lemma nat.lt_add_of_lt {a b c : nat} : a < b → a < c + b :=
 begin
   intro h,
-  note aux₁ := nat.le_add_right b c,
-  note aux₂ := lt_of_lt_of_le h aux₁,
+  have aux₁ := nat.le_add_right b c,
+  have aux₂ := lt_of_lt_of_le h aux₁,
   rwa [add_comm] at aux₂
 end
 
 lemma nat.lt_one_add_of_lt {a b : nat} : a < b → a < 1 + b :=
 begin
   intro h,
-  note aux := lt.trans h (nat.lt_succ_self _),
+  have aux := lt.trans h (nat.lt_succ_self _),
   rwa [-nat.add_one_eq_succ, add_comm] at aux
 end
 
@@ -31,7 +31,7 @@ lemma sizeof_lt_sizeof_of_mem {α} [has_sizeof α] {a : α} : ∀ {l : list α},
     cases eq_or_mem_of_mem_cons h with h_1 h_2,
     subst h_1,
     {unfold_sizeof, cancel_nat_add_lt, trivial_nat_lt},
-    {note aux₁ := sizeof_lt_sizeof_of_mem h_2,
+    {have aux₁ := sizeof_lt_sizeof_of_mem h_2,
      unfold_sizeof,
      exact nat.lt_one_add_of_lt (nat.lt_add_of_lt aux₁)}
   end
diff --git a/tests/lean/smt_begin_end1.lean b/tests/lean/smt_begin_end1.lean
index a9c8d0ba3e..9db40378ed 100644
--- a/tests/lean/smt_begin_end1.lean
+++ b/tests/lean/smt_begin_end1.lean
@@ -5,7 +5,7 @@ axiom pf (a : nat) : p (f a) (f a) → p a a
 example (a b c : nat) : a = b → p (f a) (f b) → p a b :=
 begin [smt]
   intros,
-  note h : p (f a) (f a),
+  have h : p (f a) (f a),
   trace_state,
   add_fact (pf _ h)
 end
@@ -21,7 +21,7 @@ begin
   subst h,
   begin [smt]
     intros,
-    note h₁ : p (f a) (f a),
+    have h₁ : p (f a) (f a),
     trace_state,
     add_fact (pf _ h₁)
   end
diff --git a/tests/lean/tactic_state_pp.lean b/tests/lean/tactic_state_pp.lean
index f2ee7bbd6f..7a3323895a 100644
--- a/tests/lean/tactic_state_pp.lean
+++ b/tests/lean/tactic_state_pp.lean
@@ -26,8 +26,8 @@ meta instance i2 : has_to_format tactic_state :=
 example {α : Type u} {n : nat} (v : Vec α n) : f v ≠ 2 :=
 begin
   destruct v,
-  intros, intro, note h := fax1 α, cc,
-  -- intros n1 h t, intros, intro, note h := fax2 (Vec.cons h t), cc
+  intros, intro, have h := fax1 α, cc,
+  -- intros n1 h t, intros, intro, have h := fax2 (Vec.cons h t), cc
 end
 
 open nat
@@ -35,5 +35,5 @@ example : ∀ n, 0 < n → succ (pred n) = n :=
 begin
   intro n,
   destruct n,
-   dsimp, intros, note h := lt_irrefl 0, cc,
+   dsimp, intros, have h := lt_irrefl 0, cc,
 end