diff --git a/library/data/dlist.lean b/library/data/dlist.lean
index 99533ea3de..21064c40cc 100644
--- a/library/data/dlist.lean
+++ b/library/data/dlist.lean
@@ -95,7 +95,7 @@ protected def rel_dlist_list (d : dlist α) (l : list α) : Prop :=
 to_list d = l
 
 instance bi_total_rel_dlist_list : @relator.bi_total (dlist α) (list α) dlist.rel_dlist_list :=
-⟨take d, ⟨to_list d, rfl⟩, take l, ⟨of_list l, to_list_of_list l⟩⟩
+⟨assume d, ⟨to_list d, rfl⟩, assume l, ⟨of_list l, to_list_of_list l⟩⟩
 
 protected lemma rel_eq :
   (dlist.rel_dlist_list ⇒ dlist.rel_dlist_list ⇒ iff) (@eq (dlist α)) eq
diff --git a/library/data/list/set.lean b/library/data/list/set.lean
index 76df0eddcb..52818d16ab 100644
--- a/library/data/list/set.lean
+++ b/library/data/list/set.lean
@@ -117,7 +117,7 @@ theorem disjoint_of_nodup_append : ∀ {l₁ l₂ : list α}, nodup (l₁++l₂)
   have nodup (x::(xs++l₂)),    from d,
   have x ∉ xs++l₂,             from not_mem_of_nodup_cons this,
   have nxinl₂ : x ∉ l₂,        from not_mem_of_not_mem_append_right this,
-  take a, suppose a ∈ x::xs,
+  assume a, suppose a ∈ x::xs,
     or.elim (eq_or_mem_of_mem_cons this)
       (suppose a = x, eq.symm this ▸ nxinl₂)
       (suppose ainxs : a ∈ xs,
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index fcdb5ebc40..5c52782d22 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -8,12 +8,12 @@ universes u
 variable {α : Type u}
 
 lemma ext {a b : set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
-funext (take x, propext (h x))
+funext (assume x, propext (h x))
 
-lemma subset.refl (a : set α) : a ⊆ a := take x, assume H, H
+lemma subset.refl (a : set α) : a ⊆ a := assume x, assume H, H
 
 lemma subset.trans {a b c : set α} (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c :=
-take x, assume ax, subbc (subab ax)
+assume x, assume ax, subbc (subab ax)
 
 lemma subset.antisymm {a b : set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
 ext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb))
@@ -32,7 +32,7 @@ lemma mem_empty_eq (x : α) : x ∈ (∅ : set α) = false :=
 rfl
 
 lemma eq_empty_of_forall_not_mem {s : set α} (h : ∀ x, x ∉ s) : s = ∅ :=
-ext (take x, iff.intro
+ext (assume x, iff.intro
   (assume xs, absurd xs (h x))
   (assume xe, absurd xe (not_mem_empty _)))
 
@@ -40,16 +40,16 @@ lemma ne_empty_of_mem {s : set α} {x : α} (h : x ∈ s) : s ≠ ∅ :=
   begin intro hs, rewrite hs at h, apply not_mem_empty _ h end
 
 lemma empty_subset (s : set α) : ∅ ⊆ s :=
-take x, assume h, false.elim h
+assume x, assume h, false.elim h
 
 lemma eq_empty_of_subset_empty {s : set α} (h : s ⊆ ∅) : s = ∅ :=
 subset.antisymm h (empty_subset s)
 
 lemma union_comm (a b : set α) : a ∪ b = b ∪ a :=
-ext (take x, or.comm)
+ext (assume x, or.comm)
 
 lemma union_assoc (a b c : set α) : (a ∪ b) ∪ c = a ∪ (b ∪ c) :=
-ext (take x, or.assoc)
+ext (assume x, or.assoc)
 
 instance union_is_assoc : is_associative (set α) (∪) :=
 ⟨union_assoc⟩
@@ -58,19 +58,19 @@ instance union_is_comm : is_commutative (set α) (∪) :=
 ⟨union_comm⟩
 
 lemma union_self (a : set α) : a ∪ a = a :=
-ext (take x, or_self _)
+ext (assume x, or_self _)
 
 lemma union_empty (a : set α) : a ∪ ∅ = a :=
-ext (take x, or_false _)
+ext (assume x, or_false _)
 
 lemma empty_union (a : set α) : ∅ ∪ a = a :=
-ext (take x, false_or _)
+ext (assume x, false_or _)
 
 lemma inter_comm (a b : set α) : a ∩ b = b ∩ a :=
-ext (take x, and.comm)
+ext (assume x, and.comm)
 
 lemma inter_assoc (a b c : set α) : (a ∩ b) ∩ c = a ∩ (b ∩ c) :=
-ext (take x, and.assoc)
+ext (assume x, and.assoc)
 
 instance inter_is_assoc : is_associative (set α) (∩) :=
 ⟨inter_assoc⟩
@@ -79,12 +79,12 @@ instance inter_is_comm : is_commutative (set α) (∩) :=
 ⟨inter_comm⟩
 
 lemma inter_self (a : set α) : a ∩ a = a :=
-ext (take x, and_self _)
+ext (assume x, and_self _)
 
 lemma inter_empty (a : set α) : a ∩ ∅ = ∅ :=
-ext (take x, and_false _)
+ext (assume x, and_false _)
 
 lemma empty_inter (a : set α) : ∅ ∩ a = ∅ :=
-ext (take x, false_and _)
+ext (assume x, false_and _)
 
 end set
diff --git a/library/init/algebra/functions.lean b/library/init/algebra/functions.lean
index 37199c78f2..5df97c46fb 100644
--- a/library/init/algebra/functions.lean
+++ b/library/init/algebra/functions.lean
@@ -137,7 +137,7 @@ lemma min_add_add_left (a b c : α) : min (a + b) (a + c) = a + min b c :=
 eq.symm (eq_min
   (show a + min b c ≤ a + b, from add_le_add_left (min_le_left _ _)  _)
   (show a + min b c ≤ a + c, from add_le_add_left (min_le_right _ _)  _)
-  (take d,
+  (assume d,
     suppose d ≤ a + b,
     suppose d ≤ a + c,
     decidable.by_cases
@@ -151,7 +151,7 @@ lemma max_add_add_left (a b c : α) : max (a + b) (a + c) = a + max b c :=
 eq.symm (eq_max
   (add_le_add_left (le_max_left _ _)  _)
   (add_le_add_left (le_max_right _ _) _)
-  (take d,
+  (assume d,
     suppose a + b ≤ d,
     suppose a + c ≤ d,
     decidable.by_cases
@@ -169,7 +169,7 @@ lemma max_neg_neg (a b : α) : max (-a) (-b) = - min a b  :=
 eq.symm (eq_max
   (show -a ≤ -(min a b), from neg_le_neg $ min_le_left a b)
   (show -b ≤ -(min a b), from neg_le_neg $ min_le_right a b)
-  (take d,
+  (assume d,
     assume H₁ : -a ≤ d,
     assume H₂ : -b ≤ d,
     have H : -d ≤ min a b,
diff --git a/library/init/algebra/ring.lean b/library/init/algebra/ring.lean
index 11dde51f19..a578339dde 100644
--- a/library/init/algebra/ring.lean
+++ b/library/init/algebra/ring.lean
@@ -49,7 +49,7 @@ lemma zero_ne_one [s: zero_ne_one_class α] : 0 ≠ (1:α) :=
 
 @[simp]
 lemma one_ne_zero [s: zero_ne_one_class α] : (1:α) ≠ 0 :=
-take h, @zero_ne_one_class.zero_ne_one α s h.symm
+assume h, @zero_ne_one_class.zero_ne_one α s h.symm
 
 /- semiring -/
 
@@ -104,10 +104,10 @@ section comm_semiring
   exists.elim H₁ H₂
 
   theorem exists_eq_mul_left_of_dvd {a b : α} (h : a ∣ b) : ∃ c, b = c * a :=
-  dvd.elim h (take c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul_comm a c)))
+  dvd.elim h (assume c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul_comm a c)))
 
   theorem dvd.elim_left {P : Prop} {a b : α} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P :=
-  exists.elim (exists_eq_mul_left_of_dvd h₁) (take c, assume h₃ : b = c * a, h₂ c h₃)
+  exists.elim (exists_eq_mul_left_of_dvd h₁) (assume c, assume h₃ : b = c * a, h₂ c h₃)
 
   @[simp] theorem dvd_refl : a ∣ a :=
   dvd.intro 1 (by simp)
@@ -121,7 +121,7 @@ section comm_semiring
   def dvd.trans := @dvd_trans
 
   theorem eq_zero_of_zero_dvd {a : α} (h : 0 ∣ a) : a = 0 :=
-  dvd.elim h (take c, assume H' : a = 0 * c, eq.trans H' (zero_mul c))
+  dvd.elim h (assume c, assume H' : a = 0 * c, eq.trans H' (zero_mul c))
 
   @[simp] theorem dvd_zero : a ∣ 0 := dvd.intro 0 (by simp)
 
@@ -236,7 +236,7 @@ section comm_ring
 
   theorem dvd_neg_of_dvd {a b : α} (h : a ∣ b) : (a ∣ -b) :=
   dvd.elim h
-    (take c, suppose b = a * c,
+    (assume c, suppose b = a * c,
       dvd.intro (-c) (by simp [this]))
 
   theorem dvd_of_dvd_neg {a b : α} (h : a ∣ -b) : (a ∣ b) :=
@@ -247,7 +247,7 @@ section comm_ring
 
   theorem neg_dvd_of_dvd {a b : α} (h : a ∣ b) : -a ∣ b :=
   dvd.elim h
-    (take c, suppose b = a * c,
+    (assume c, suppose b = a * c,
       dvd.intro (-c) (by simp [this]))
 
   theorem dvd_of_neg_dvd {a b : α} (h : -a ∣ b) : a ∣ b :=
diff --git a/library/init/category/transformers.lean b/library/init/category/transformers.lean
index f4c273cb5d..842d9cd553 100644
--- a/library/init/category/transformers.lean
+++ b/library/init/category/transformers.lean
@@ -40,7 +40,7 @@ end monad
 namespace state_t
 
 def state_t_monad_lift (S) (m) [monad m] (α) (f : m α) : state_t S m α :=
-take state, do res ← f, return (res, state)
+assume state, do res ← f, return (res, state)
 
 instance (S) : monad.monad_transformer (state_t S) :=
 ⟨ state_t.monad S, state_t_monad_lift S ⟩
diff --git a/library/init/classical.lean b/library/init/classical.lean
index fdecb44206..d3647e46a0 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -55,7 +55,7 @@ or.elim u_def
 private lemma p_implies_uv : p → u = v :=
 assume hp : p,
 have hpred : U = V, from
-  funext (take x : Prop,
+  funext (assume x : Prop,
     have hl : (x = true ∨ p) → (x = false ∨ p), from
       assume a, or.inr hp,
     have hr : (x = false ∨ p) → (x = true ∨ p), from
@@ -75,7 +75,7 @@ have h : ¬(u = v) → ¬p, from mt p_implies_uv,
 end diaconescu
 
 theorem exists_true_of_nonempty {α : Sort u} (h : nonempty α) : ∃ x : α, true :=
-nonempty.elim h (take x, ⟨x, trivial⟩)
+nonempty.elim h (assume x, ⟨x, trivial⟩)
 
 noncomputable def inhabited_of_nonempty {α : Sort u} (h : nonempty α) : inhabited α :=
 ⟨(indefinite_description _ (exists_true_of_nonempty h)).val⟩
@@ -135,7 +135,7 @@ theorem epsilon_singleton {α : Sort u} (x : α) : @epsilon α ⟨x⟩ (λ y, y
 
 theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
   ∃ (f : Π x, β x), ∀ x, r x (f x) :=
-have h : ∀ x, r x (some (h x)), from take x, some_spec (h x),
+have h : ∀ x, r x (some (h x)), from assume x, some_spec (h x),
 ⟨_, h⟩
 
 theorem skolem {α : Sort u} {b : α → Sort v} {p : Π x, b x → Prop} :
@@ -143,7 +143,7 @@ theorem skolem {α : Sort u} {b : α → Sort v} {p : Π x, b x → Prop} :
 iff.intro
   (assume h : (∀ x, ∃ y, p x y), axiom_of_choice h)
   (assume h : (∃ (f : Π x, b x), (∀ x, p x (f x))),
-    take x, exists.elim h (λ (fw : ∀ x, b x) (hw : ∀ x, p x (fw x)),
+    assume x, exists.elim h (λ (fw : ∀ x, b x) (hw : ∀ x, p x (fw x)),
       ⟨fw x, hw x⟩))
 
 theorem prop_complete (a : Prop) : a = true ∨ a = false :=
diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean
index 047f4a2151..fdd29a98b0 100644
--- a/library/init/data/int/basic.lean
+++ b/library/init/data/int/basic.lean
@@ -119,7 +119,7 @@ lemma neg_succ_of_nat_inj {m n : ℕ} (h : neg_succ_of_nat m = neg_succ_of_nat n
 int.no_confusion h id
 
 lemma neg_succ_of_nat_inj_iff {m n : ℕ} : neg_succ_of_nat m = neg_succ_of_nat n ↔ m = n :=
-⟨neg_succ_of_nat_inj, take H, by simp [H]⟩
+⟨neg_succ_of_nat_inj, assume H, by simp [H]⟩
 
 lemma neg_succ_of_nat_eq (n : ℕ) : -[1+ n] = -(n + 1) := rfl
 
@@ -164,9 +164,9 @@ calc sub_nat_nat._match_1 m (m + n + 1) (m + n + 1 - m) =
 
 private lemma sub_nat_nat_add_add (m n k : ℕ) : sub_nat_nat (m + k) (n + k) = sub_nat_nat m n :=
 sub_nat_nat_elim m n (λm n i, sub_nat_nat (m + k) (n + k) = i)
-  (take i n, have n + i + k = (n + k) + i, by simp,
+  (assume i n, have n + i + k = (n + k) + i, by simp,
     begin rw [this], exact sub_nat_nat_add_left end)
-  (take i m, have m + i + 1 + k = (m + k) + i + 1, by simp,
+  (assume i m, have m + i + 1 + k = (m + k) + i + 1, by simp,
     begin rw [this], exact sub_nat_nat_add_right end)
 
 /- nat_abs -/
@@ -273,7 +273,7 @@ inductive rel_int_nat_nat : ℤ → ℕ × ℕ → Prop
 
 protected lemma rel_sub_nat_nat {a b : ℕ} : rel_int_nat_nat (sub_nat_nat a b) (a, b) :=
 sub_nat_nat_elim a b (λa b i, rel_int_nat_nat i (a, b))
-  (take i n, rel_int_nat_nat.pos) (take i n, rel_int_nat_nat.neg)
+  (assume i n, rel_int_nat_nat.pos) (assume i n, rel_int_nat_nat.neg)
 
 instance right_total_rel_int_nat_nat : relator.right_total rel_int_nat_nat
 | (n, m) := ⟨_, int.rel_sub_nat_nat⟩
diff --git a/library/init/data/int/lemmas.lean b/library/init/data/int/lemmas.lean
index bce0c60b68..8dd7642d5d 100644
--- a/library/init/data/int/lemmas.lean
+++ b/library/init/data/int/lemmas.lean
@@ -339,7 +339,7 @@ theorem dvd_iff_mod_eq_zero (a b : ℤ) : a ∣ b ↔ b % a = 0 :=
 ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩
 
 instance decidable_dvd : @decidable_rel ℤ (∣) :=
-take a n, decidable_of_decidable_of_iff (by apply_instance) (dvd_iff_mod_eq_zero _ _).symm
+assume a n, decidable_of_decidable_of_iff (by apply_instance) (dvd_iff_mod_eq_zero _ _).symm
 
 protected theorem div_mul_cancel {a b : ℤ} (H : b ∣ a) : a / b * b = a :=
 div_mul_cancel_of_mod_eq_zero (mod_eq_zero_of_dvd H)
diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean
index 65e60111f6..551cfba613 100644
--- a/library/init/data/int/order.lean
+++ b/library/init/data/int/order.lean
@@ -10,7 +10,7 @@ import init.data.int.basic init.data.nat.find
 
 namespace int
 
-private def nonneg (a : ℤ) : Prop := int.cases_on a (take n, true) (take n, false)
+private def nonneg (a : ℤ) : Prop := int.cases_on a (assume n, true) (assume n, false)
 
 protected def le (a b : ℤ) : Prop := nonneg (b - a)
 
@@ -21,7 +21,7 @@ protected def lt (a b : ℤ) : Prop := (a + 1) ≤ b
 instance : has_lt int := ⟨int.lt⟩
 
 private def decidable_nonneg (a : ℤ) : decidable (nonneg a) :=
-int.cases_on a (take a, decidable.true) (take a, decidable.false)
+int.cases_on a (assume a, decidable.true) (assume a, decidable.false)
 
 instance decidable_le (a b : ℤ) : decidable (a ≤ b) := decidable_nonneg _
 
@@ -30,10 +30,10 @@ instance decidable_lt (a b : ℤ) : decidable (a < b) := decidable_nonneg _
 lemma lt_iff_add_one_le (a b : ℤ) : a < b ↔ a + 1 ≤ b := iff.refl _
 
 private lemma nonneg.elim {a : ℤ} : nonneg a → ∃ n : ℕ, a = n :=
-int.cases_on a (take n H, exists.intro n rfl) (take n', false.elim)
+int.cases_on a (assume n H, exists.intro n rfl) (assume n', false.elim)
 
 private lemma nonneg_or_nonneg_neg (a : ℤ) : nonneg a ∨ nonneg (-a) :=
-int.cases_on a (take n, or.inl trivial) (take n, or.inr trivial)
+int.cases_on a (assume n, or.inl trivial) (assume n, or.inr trivial)
 
 lemma le.intro_sub {a b : ℤ} {n : ℕ} (h : b - a = n) : a ≤ b :=
 show nonneg (b - a), by rw h; trivial
@@ -64,7 +64,7 @@ match nat.le.dest h with
 end
 
 lemma le_of_coe_nat_le_coe_nat {m n : ℕ} (h : (↑m : ℤ) ≤ ↑n) : m ≤ n :=
-le.elim h (take k, assume hk : ↑m + ↑k = ↑n,
+le.elim h (assume k, assume hk : ↑m + ↑k = ↑n,
   have m + k = n, from int.coe_nat_inj ((int.coe_nat_add m k).trans hk),
   nat.le.intro this)
 
@@ -88,7 +88,7 @@ lemma lt.intro {a b : ℤ} {n : ℕ} (h : a + nat.succ n = b) : a < b :=
 h ▸ lt_add_succ a n
 
 lemma lt.dest {a b : ℤ} (h : a < b) : ∃ n : ℕ, a + ↑(nat.succ n) = b :=
-le.elim h (take n, assume hn : a + 1 + n = b,
+le.elim h (assume n, assume hn : a + 1 + n = b,
     exists.intro n begin rw [-hn, add_assoc, add_comm (1 : int)], reflexivity end)
 
 lemma lt.elim {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ n : ℕ, a + ↑(nat.succ n) = b → P) : P :=
@@ -109,13 +109,13 @@ protected lemma le_refl (a : ℤ) : a ≤ a :=
 le.intro (add_zero a)
 
 protected lemma le_trans {a b c : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
-le.elim h₁ (take n, assume hn : a + n = b,
-le.elim h₂ (take m, assume hm : b + m = c,
+le.elim h₁ (assume n, assume hn : a + n = b,
+le.elim h₂ (assume m, assume hm : b + m = c,
 begin apply le.intro, rw [-hm, -hn, add_assoc], reflexivity end))
 
 protected lemma le_antisymm {a b : ℤ} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b :=
-le.elim h₁ (take n, assume hn : a + n = b,
-le.elim h₂ (take m, assume hm : b + m = a,
+le.elim h₁ (assume n, assume hn : a + n = b,
+le.elim h₂ (assume m, assume hm : b + m = a,
   have a + ↑(n + m) = a + 0, by rw [int.coe_nat_add, -add_assoc, hn, hm, add_zero a],
   have (↑(n + m) : ℤ) = 0, from add_left_cancel this,
   have n + m = 0, from int.coe_nat_inj this,
@@ -124,7 +124,7 @@ le.elim h₂ (take m, assume hm : b + m = a,
 
 protected lemma lt_irrefl (a : ℤ) : ¬ a < a :=
 suppose a < a,
-lt.elim this (take n, assume hn : a + nat.succ n = a,
+lt.elim this (assume n, assume hn : a + nat.succ n = a,
   have a + nat.succ n = a + 0, by rw [hn, add_zero],
   have nat.succ n = 0, from int.coe_nat_inj (add_left_cancel this),
   show false, from nat.succ_ne_zero _ this)
@@ -133,13 +133,13 @@ protected lemma ne_of_lt {a b : ℤ} (h : a < b) : a ≠ b :=
 (suppose a = b, absurd (begin rewrite this at h, exact h end) (int.lt_irrefl b))
 
 lemma le_of_lt {a b : ℤ} (h : a < b) : a ≤ b :=
-lt.elim h (take n, assume hn : a + nat.succ n = b, le.intro hn)
+lt.elim h (assume n, assume hn : a + nat.succ n = b, le.intro hn)
 
 protected lemma lt_iff_le_and_ne (a b : ℤ) : a < b ↔ (a ≤ b ∧ a ≠ b) :=
 iff.intro
   (assume h, ⟨le_of_lt h, int.ne_of_lt h⟩)
   (assume ⟨aleb, aneb⟩,
-    le.elim aleb (take n, assume hn : a + n = b,
+    le.elim aleb (assume n, assume hn : a + n = b,
       have n ≠ 0,
         from (suppose n = 0, aneb begin rw [-hn, this, int.coe_nat_zero, add_zero] end),
       have n = nat.succ (nat.pred n),
@@ -152,7 +152,7 @@ iff.intro
     decidable.by_cases
       (suppose a = b, or.inr this)
       (suppose a ≠ b,
-        le.elim h (take n, assume hn : a + n = b,
+        le.elim h (assume n, assume hn : a + n = b,
           have n ≠ 0, from
             (suppose n = 0, ‹a ≠ b› begin rw [-hn, this, int.coe_nat_zero, add_zero] end),
           have n = nat.succ (nat.pred n),
@@ -167,23 +167,23 @@ lemma lt_succ (a : ℤ) : a < a + 1 :=
 int.le_refl (a + 1)
 
 protected lemma add_le_add_left {a b : ℤ} (h : a ≤ b) (c : ℤ) : c + a ≤ c + b :=
-le.elim h (take n, assume hn : a + n = b,
+le.elim h (assume n, assume hn : a + n = b,
   le.intro (show c + a + n = c + b, begin rw [add_assoc, hn] end))
 
 protected lemma add_lt_add_left {a b : ℤ} (h : a < b) (c : ℤ) : c + a < c + b :=
 iff.mpr (int.lt_iff_le_and_ne _ _)
   (and.intro
     (int.add_le_add_left (le_of_lt h) _)
-    (take heq, int.lt_irrefl b begin rw add_left_cancel heq at h, exact h end))
+    (assume heq, int.lt_irrefl b begin rw add_left_cancel heq at h, exact h end))
 
 protected lemma mul_nonneg {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b :=
-le.elim ha (take n, assume hn,
-le.elim hb (take m, assume hm,
+le.elim ha (assume n, assume hn,
+le.elim hb (assume m, assume hm,
   le.intro (show 0 + ↑n * ↑m = a * b, begin rw [-hn, -hm], repeat {rw zero_add} end)))
 
 protected lemma mul_pos {a b : ℤ} (ha : 0 < a) (hb : 0 < b) : 0 < a * b :=
-lt.elim ha (take n, assume hn,
-lt.elim hb (take m, assume hm,
+lt.elim ha (assume n, assume hn,
+lt.elim hb (assume m, assume hm,
   lt.intro (show 0 + ↑(nat.succ (nat.succ n * m + n)) = a * b,
     begin rw [-hn, -hm], repeat {rw int.coe_nat_zero}, simp,
           rw [-int.coe_nat_mul], simp [nat.mul_succ, nat.succ_add] end)))
diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean
index f9898da9bf..88a2986242 100644
--- a/library/init/data/list/lemmas.lean
+++ b/library/init/data/list/lemmas.lean
@@ -341,8 +341,8 @@ lemma mem_or_mem_of_mem_append {a : α} : ∀ {s t : list α}, a ∈ s ++ t →
 
 lemma mem_append_of_mem_or_mem {a : α} {s t : list α} : a ∈ s ∨ a ∈ t → a ∈ s ++ t :=
 list.rec_on s
-  (take h, or.elim h false.elim id)
-  (take b s,
+  (assume h, or.elim h false.elim id)
+  (assume b s,
     assume ih : a ∈ s ∨ a ∈ t → a ∈ s ++ t,
     suppose a ∈ b::s ∨ a ∈ t,
       or.elim this
@@ -376,7 +376,7 @@ lemma length_pos_of_mem {a : α} : ∀ {l : list α}, a ∈ l → 0 < length l
 lemma mem_split {a : α} {l : list α} : a ∈ l → ∃ s t : list α, l = s ++ (a::t) :=
 list.rec_on l
   (suppose a ∈ [], begin simp at this, contradiction end)
-  (take b l,
+  (assume b l,
     assume ih : a ∈ l → ∃ s t : list α, l = s ++ (a::t),
     suppose a ∈ b::l,
     or.elim (eq_or_mem_of_mem_cons this)
@@ -510,14 +510,14 @@ lemma subset_app_of_subset_right (l l₁ l₂ : list α) : l ⊆ l₂ → l ⊆
 
 lemma cons_subset_of_subset_of_mem {a : α} {l m : list α} (ainm : a ∈ m) (lsubm : l ⊆ m) :
   a::l ⊆ m :=
-take b, suppose b ∈ a::l,
+assume b, suppose b ∈ a::l,
 or.elim (eq_or_mem_of_mem_cons this)
   (suppose b = a, begin subst b, exact ainm end)
   (suppose b ∈ l, lsubm this)
 
 lemma app_subset_of_subset_of_subset {l₁ l₂ l : list α} (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) :
   l₁ ++ l₂ ⊆ l :=
-take a, suppose a ∈ l₁ ++ l₂,
+assume a, suppose a ∈ l₁ ++ l₂,
 or.elim (mem_or_mem_of_mem_append this)
   (suppose a ∈ l₁, l₁subl this)
   (suppose a ∈ l₂, l₂subl this)
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index 29241856e6..84e61e8fa8 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -339,7 +339,7 @@ begin
 end
 
 protected lemma add_le_add_iff_le_right (k n m : ℕ) : n + k ≤ m + k ↔ n ≤ m :=
-  ⟨ nat.le_of_add_le_add_right , take h, nat.add_le_add_right h _ ⟩
+  ⟨ nat.le_of_add_le_add_right , assume h, nat.add_le_add_right h _ ⟩
 
 protected lemma lt_of_le_and_ne {m n : ℕ} (h1 : m ≤ n) : m ≠ n → m < n :=
 or.resolve_right (or.swap (nat.eq_or_lt_of_le h1))
@@ -415,8 +415,8 @@ instance : decidable_linear_ordered_semiring nat :=
   add_le_add_left            := @nat.add_le_add_left,
   le_of_add_le_add_left      := @nat.le_of_add_le_add_left,
   zero_lt_one                := zero_lt_succ 0,
-  mul_le_mul_of_nonneg_left  := (take a b c h₁ h₂, nat.mul_le_mul_left c h₁),
-  mul_le_mul_of_nonneg_right := (take a b c h₁ h₂, nat.mul_le_mul_right c h₁),
+  mul_le_mul_of_nonneg_left  := (assume a b c h₁ h₂, nat.mul_le_mul_left c h₁),
+  mul_le_mul_of_nonneg_right := (assume a b c h₁ h₂, nat.mul_le_mul_right c h₁),
   mul_lt_mul_of_pos_left     := @nat.mul_lt_mul_of_pos_left,
   mul_lt_mul_of_pos_right    := @nat.mul_lt_mul_of_pos_right,
   decidable_lt               := nat.decidable_lt,
@@ -761,7 +761,7 @@ begin rw [-add_one_eq_succ, -add_one_eq_succ], simp [right_distrib, left_distrib
 
 theorem sub_eq_zero_of_le {n m : ℕ} (h : n ≤ m) : n - m = 0 :=
 exists.elim (nat.le.dest h)
-  (take k, assume hk : n + k = m, by rw [-hk, sub_self_add])
+  (assume k, assume hk : n + k = m, by rw [-hk, sub_self_add])
 
 protected theorem le_of_sub_eq_zero : ∀{n m : ℕ}, n - m = 0 → n ≤ m
 | n 0 H := begin rw [nat.sub_zero] at H, simp [H] end
@@ -774,12 +774,12 @@ protected theorem sub_eq_zero_iff_le {n m : ℕ} : n - m = 0 ↔ n ≤ m :=
 
 theorem succ_sub {m n : ℕ} (h : m ≥ n) : succ m - n  = succ (m - n) :=
 exists.elim (nat.le.dest h)
-  (take k, assume hk : n + k = m,
+  (assume k, assume hk : n + k = m,
     by rw [-hk, nat.add_sub_cancel_left, -add_succ, nat.add_sub_cancel_left])
 
 theorem add_sub_of_le {n m : ℕ} (h : n ≤ m) : n + (m - n) = m :=
 exists.elim (nat.le.dest h)
-  (take k, assume hk : n + k = m,
+  (assume k, assume hk : n + k = m,
     by rw [-hk, nat.add_sub_cancel_left])
 
 protected theorem sub_add_cancel {n m : ℕ} (h : n ≥ m) : n - m + m = n :=
@@ -791,12 +791,12 @@ lt_of_add_lt_add_right this
 
 protected theorem add_sub_assoc {m k : ℕ} (h : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) :=
 exists.elim (nat.le.dest h)
-  (take l, assume hl : k + l = m,
+  (assume l, assume hl : k + l = m,
     by rw [-hl, nat.add_sub_cancel_left, add_comm k, -add_assoc, nat.add_sub_cancel])
 
 protected lemma sub_eq_iff_eq_add {a b c : ℕ} (ab : b ≤ a) : a - b = c ↔ a = c + b :=
-⟨take c_eq, begin rw [c_eq.symm, nat.sub_add_cancel ab] end,
-  take a_eq, begin rw [a_eq, nat.add_sub_cancel] end⟩
+⟨assume c_eq, begin rw [c_eq.symm, nat.sub_add_cancel ab] end,
+  assume a_eq, begin rw [a_eq, nat.add_sub_cancel] end⟩
 
 protected theorem sub_sub_self {n m : ℕ} (h : m ≤ n) : n - (n - m) = m :=
 (nat.sub_eq_iff_eq_add (nat.sub_le _ _)).2 (eq.symm (add_sub_of_le h))
@@ -807,7 +807,7 @@ protected theorem sub_add_comm {n m k : ℕ} (h : k ≤ n) : n + m - k = n - k +
 
 protected lemma lt_of_sub_eq_succ {m n l : ℕ} (H : m - n = nat.succ l) : n < m :=
 lt_of_not_ge
-  (take (H' : n ≥ m), begin simp [nat.sub_eq_zero_of_le H'] at H, contradiction end)
+  (assume (H' : n ≥ m), begin simp [nat.sub_eq_zero_of_le H'] at H, contradiction end)
 
 lemma sub_one_sub_lt {n i} (h : i < n) : n - 1 - i < n := begin
   rw nat.sub_sub,
diff --git a/library/init/function.lean b/library/init/function.lean
index 985ed189ca..abcd06a6c2 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -62,7 +62,7 @@ lemma comp_const_right (f : β → φ) (b : β) : f ∘ (const α b) = const α
 @[reducible] def injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
 
 lemma injective_comp {g : β → φ} {f : α → β} (hg : injective g) (hf : injective f) : injective (g ∘ f) :=
-take a₁ a₂, assume h, hf (hg h)
+assume a₁ a₂, assume h, hf (hg h)
 
 @[reducible] def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
 
@@ -86,7 +86,7 @@ def right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g
 def has_right_inverse (f : α → β) : Prop := ∃ finv : β → α, right_inverse finv f
 
 lemma injective_of_left_inverse {g : β → α} {f : α → β} : left_inverse g f → injective f :=
-assume h, take a b, assume faeqfb,
+assume h, assume a b, assume faeqfb,
 have h₁ : a = g (f a),       from eq.symm (h a),
 have h₂ : g (f b) = b,       from h b,
 have h₃ : g (f a) = g (f b), from congr_arg g faeqfb,
@@ -98,7 +98,7 @@ assume h, exists.elim h (λ finv inv, injective_of_left_inverse inv)
 lemma right_inverse_of_injective_of_left_inverse {f : α → β} {g : β → α}
     (injf : injective f) (lfg : left_inverse f g) :
   right_inverse f g :=
-take x,
+assume x,
 have h : f (g (f x)) = f x, from lfg (f x),
 injf h
 
@@ -108,14 +108,14 @@ lemma surjective_of_has_right_inverse {f : α → β} : has_right_inverse f →
 lemma left_inverse_of_surjective_of_right_inverse {f : α → β} {g : β → α}
     (surjf : surjective f) (rfg : right_inverse f g) :
   left_inverse f g :=
-take y, exists.elim (surjf y) (λ x hx, calc
+assume y, exists.elim (surjf y) (λ x hx, calc
   f (g y) = f (g (f x)) : hx ▸ rfl
       ... = f x         : eq.symm (rfg x) ▸ rfl
       ... = y           : hx)
 
-lemma injective_id : injective (@id α) := take a₁ a₂ h, h
+lemma injective_id : injective (@id α) := assume a₁ a₂ h, h
 
-lemma surjective_id : surjective (@id α) := take a, ⟨a, rfl⟩
+lemma surjective_id : surjective (@id α) := assume a, ⟨a, rfl⟩
 
 lemma bijective_id : bijective (@id α) := ⟨injective_id, surjective_id⟩
 
diff --git a/library/init/funext.lean b/library/init/funext.lean
index 98e784b90b..33081544a9 100644
--- a/library/init/funext.lean
+++ b/library/init/funext.lean
@@ -17,7 +17,7 @@ protected def equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂
 
 local infix `~` := function.equiv
 
-protected theorem equiv.refl (f : Π x : α, β x) : f ~ f := take x, rfl
+protected theorem equiv.refl (f : Π x : α, β x) : f ~ f := assume x, rfl
 
 protected theorem equiv.symm {f₁ f₂ : Π x: α, β x} : f₁ ~ f₂ → f₂ ~ f₁ :=
 λ h x, eq.symm (h x)
@@ -43,7 +43,7 @@ quotient (fun_setoid α β)
 private def fun_to_extfun (f : Π x : α, β x) : extfun α β :=
 ⟦f⟧
 private def extfun_app (f : extfun α β) : Π x : α, β x :=
-take x,
+assume x,
 quot.lift_on f
   (λ f : Π x : α, β x, f x)
   (λ f₁ f₂ h, h x)
diff --git a/library/init/logic.lean b/library/init/logic.lean
index d2f49347d3..ec3466ea17 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -316,8 +316,8 @@ iff.mpr (h₂ hc) hd)
 
 lemma imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
 iff.intro
-  (take hab ha, iff.elim_left (h ha) (hab ha))
-  (take hab ha, iff.elim_right (h ha) (hab ha))
+  (assume hab ha, iff.elim_left (h ha) (hab ha))
+  (assume hab ha, iff.elim_right (h ha) (hab ha))
 
 lemma not_not_intro (ha : a) : ¬¬a :=
 assume hna : ¬a, hna ha
@@ -562,7 +562,7 @@ exists.elim h₂ (λ w hw, h₁ w (and.left hw) (and.right hw))
 
 lemma exists_unique_of_exists_of_unique {α : Type u} {p : α → Prop}
     (hex : ∃ x, p x) (hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) :  ∃! x, p x :=
-exists.elim hex (λ x px, exists_unique.intro x px (take y, suppose p y, hunique y x this px))
+exists.elim hex (λ x px, exists_unique.intro x px (assume y, suppose p y, hunique y x this px))
 
 lemma exists_of_exists_unique {α : Sort u} {p : α → Prop} (h : ∃! x, p x) : ∃ x, p x :=
 exists.elim h (λ x hx, ⟨x, and.left hx⟩)
@@ -570,7 +570,7 @@ exists.elim h (λ x hx, ⟨x, and.left hx⟩)
 lemma unique_of_exists_unique {α : Sort u} {p : α → Prop}
     (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ :=
 exists_unique.elim h
-  (take x, suppose p x,
+  (assume x, suppose p x,
     assume unique : ∀ y, p y → y = x,
     show y₁ = y₂, from eq.trans (unique _ py₁) (eq.symm (unique _ py₂)))
 
@@ -707,7 +707,7 @@ instance : decidable_eq bool
 | tt tt := is_true rfl
 
 def decidable_eq_of_bool_pred {α : Sort u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α :=
-take x y : α,
+assume x y : α,
  if hp : p x y = tt then is_true (h₁ hp)
  else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z, ¬p z y = tt) _ hxy hp))
 
@@ -1054,13 +1054,13 @@ def right_commutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a
 def left_commutative  (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
 
 lemma left_comm : commutative f → associative f → left_commutative f :=
-assume hcomm hassoc, take a b c, calc
+assume hcomm hassoc, assume a b c, calc
   a*(b*c) = (a*b)*c  : eq.symm (hassoc a b c)
     ...   = (b*a)*c  : hcomm a b ▸ rfl
     ...   = b*(a*c)  : hassoc b a c
 
 lemma right_comm : commutative f → associative f → right_commutative f :=
-assume hcomm hassoc, take a b c, calc
+assume hcomm hassoc, assume a b c, calc
   (a*b)*c = a*(b*c) : hassoc a b c
     ...   = a*(c*b) : hcomm b c ▸ rfl
     ...   = (a*c)*b : eq.symm (hassoc a c b)
diff --git a/library/init/meta/coinductive_predicates.lean b/library/init/meta/coinductive_predicates.lean
index 1a8c4a309a..ca40c6a583 100644
--- a/library/init/meta/coinductive_predicates.lean
+++ b/library/init/meta/coinductive_predicates.lean
@@ -119,17 +119,17 @@ def monotonicity := { user_attribute . name := `monotonicity, descr := "Monotoni
 
 lemma monotonicity.pi {α : Sort u} {p q : α → Prop} (h : ∀a, implies (p a) (q a)) :
   implies (Πa, p a) (Πa, q a) :=
-take h' a, h a (h' a)
+assume h' a, h a (h' a)
 
 lemma monotonicity.imp {p p' q q' : Prop} (h₁ : implies p' q') (h₂ : implies q p) :
   implies (p → p') (q → q') :=
-take h, h₁ ∘ h ∘ h₂
+assume h, h₁ ∘ h ∘ h₂
 
 @[monotonicity]
 lemma monotonicity.const (p : Prop) : implies p p := id
 
 @[monotonicity]
-lemma monotonicity.true (p : Prop) : implies p true := take _, trivial
+lemma monotonicity.true (p : Prop) : implies p true := assume _, trivial
 
 @[monotonicity]
 lemma monotonicity.false (p : Prop) : implies false p := false.elim
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 0dedfdad08..8e3399c34f 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -217,7 +217,7 @@ do fmt ← pp a,
    return $ _root_.trace_fmt fmt (λ u, ())
 
 meta def trace_call_stack : tactic unit :=
-take state, _root_.trace_call_stack (success () state)
+assume state, _root_.trace_call_stack (success () state)
 
 meta def timetac {α : Type u} (desc : string) (t : thunk (tactic α)) : tactic α :=
 λ s, timeit desc (t () s)
diff --git a/library/init/relator.lean b/library/init/relator.lean
index 540dc801db..f1d8bb20e5 100644
--- a/library/init/relator.lean
+++ b/library/init/relator.lean
@@ -49,20 +49,20 @@ variables {α : Type u₁} {β : Type u₂} (R : α → β → Prop)
 @[class] def right_unique := ∀{a b c}, R a b → R a c → b = c
 
 lemma rel_forall_of_right_total [t : right_total R] : ((R ⇒ implies) ⇒ implies) (λp, ∀i, p i) (λq, ∀i, q i) :=
-take p q Hrel H b, exists.elim (t b) (take a Rab, Hrel Rab (H _))
+assume p q Hrel H b, exists.elim (t b) (assume a Rab, Hrel Rab (H _))
 
 lemma rel_exists_of_left_total [t : left_total R] : ((R ⇒ implies) ⇒ implies) (λp, ∃i, p i) (λq, ∃i, q i) :=
-take p q Hrel ⟨a, pa⟩, let ⟨b, Rab⟩ := t a in ⟨b, Hrel Rab pa⟩
+assume p q Hrel ⟨a, pa⟩, let ⟨b, Rab⟩ := t a in ⟨b, Hrel Rab pa⟩
 
 lemma rel_forall_of_total [t : bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∀i, p i) (λq, ∀i, q i) :=
-take p q Hrel,
-  ⟨take H b, exists.elim (t.right b) (take a Rab, (Hrel Rab).mp (H _)),
-    take H a, exists.elim (t.left a) (take b Rab, (Hrel Rab).mpr (H _))⟩
+assume p q Hrel,
+  ⟨assume H b, exists.elim (t.right b) (assume a Rab, (Hrel Rab).mp (H _)),
+    assume H a, exists.elim (t.left a) (assume b Rab, (Hrel Rab).mpr (H _))⟩
 
 lemma rel_exists_of_total [t : bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∃i, p i) (λq, ∃i, q i) :=
-take p q Hrel,
-  ⟨take ⟨a, pa⟩, let ⟨b, Rab⟩ := t.left a in ⟨b, (Hrel Rab).1 pa⟩,
-    take ⟨b, qb⟩, let ⟨a, Rab⟩ := t.right b in ⟨a, (Hrel Rab).2 qb⟩⟩
+assume p q Hrel,
+  ⟨assume ⟨a, pa⟩, let ⟨b, Rab⟩ := t.left a in ⟨b, (Hrel Rab).1 pa⟩,
+    assume ⟨b, qb⟩, let ⟨a, Rab⟩ := t.right b in ⟨a, (Hrel Rab).2 qb⟩⟩
 
 lemma left_unique_of_rel_eq {eq' : β → β → Prop} (he : (R ⇒ (R ⇒ iff)) eq eq') : left_unique R
 | a b c (ab : R a b) (cb : R c b) :=
@@ -73,12 +73,12 @@ iff.mpr (he ab cb) this
 end
 
 lemma rel_imp : (iff ⇒ (iff  ⇒ iff)) implies implies :=
-take p q h r s l, imp_congr h l
+assume p q h r s l, imp_congr h l
 
 lemma rel_not : (iff ⇒ iff) not not :=
-take p q h, not_congr h
+assume p q h, not_congr h
 
 instance bi_total_eq {α : Type u₁} : relator.bi_total (@eq α) :=
-⟨take a, ⟨a, rfl⟩, take a, ⟨a, rfl⟩⟩
+⟨assume a, ⟨a, rfl⟩, assume a, ⟨a, rfl⟩⟩
 
 end relator
diff --git a/library/init/wf.lean b/library/init/wf.lean
index 6fb26fef5b..6e38098717 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -27,7 +27,7 @@ class has_well_founded (α : Sort u) : Type u :=
 
 namespace well_founded
 def apply {α : Sort u} {r : α → α → Prop} (wf : well_founded r) : ∀ a, acc r a :=
-take a, well_founded.rec_on wf (λ p, p) a
+assume a, well_founded.rec_on wf (λ p, p) a
 
 section
 parameters {α : Sort u} {r : α → α → Prop}
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 00112787b7..ed96eca3cd 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -114,7 +114,7 @@ void init_token_table(token_table & t) {
          "#compile", "#unify", nullptr};
 
     pair<char const *, char const *> aliases[] =
-        {{"λ", "fun"}, {"take", "fun"}, {"forall", "Pi"},
+        {{"λ", "fun"}, {"forall", "Pi"},
          {"∀", "Pi"}, {"Π", "Pi"}, {"(|", "⟨"}, {"|)", "⟩"}, {nullptr, nullptr}};
 
     pair<char const *, char const *> cmd_aliases[] =
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 74a7bc16e9..6aab4e298d 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -52,7 +52,6 @@ static name const * g_show_tk = nullptr;
 static name const * g_have_tk = nullptr;
 static name const * g_assume_tk = nullptr;
 static name const * g_suppose_tk = nullptr;
-static name const * g_take_tk = nullptr;
 static name const * g_fun_tk = nullptr;
 static name const * g_match_tk = nullptr;
 static name const * g_ellipsis_tk = nullptr;
@@ -178,7 +177,6 @@ void initialize_tokens() {
     g_have_tk = new name{"have"};
     g_assume_tk = new name{"assume"};
     g_suppose_tk = new name{"suppose"};
-    g_take_tk = new name{"take"};
     g_fun_tk = new name{"fun"};
     g_match_tk = new name{"match"};
     g_ellipsis_tk = new name{"..."};
@@ -305,7 +303,6 @@ void finalize_tokens() {
     delete g_have_tk;
     delete g_assume_tk;
     delete g_suppose_tk;
-    delete g_take_tk;
     delete g_fun_tk;
     delete g_match_tk;
     delete g_ellipsis_tk;
@@ -431,7 +428,6 @@ name const & get_show_tk() { return *g_show_tk; }
 name const & get_have_tk() { return *g_have_tk; }
 name const & get_assume_tk() { return *g_assume_tk; }
 name const & get_suppose_tk() { return *g_suppose_tk; }
-name const & get_take_tk() { return *g_take_tk; }
 name const & get_fun_tk() { return *g_fun_tk; }
 name const & get_match_tk() { return *g_match_tk; }
 name const & get_ellipsis_tk() { return *g_ellipsis_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index b2a8b95963..80d3eb316f 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -54,7 +54,6 @@ name const & get_show_tk();
 name const & get_have_tk();
 name const & get_assume_tk();
 name const & get_suppose_tk();
-name const & get_take_tk();
 name const & get_fun_tk();
 name const & get_match_tk();
 name const & get_ellipsis_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index 3b1bbd5e18..954966e500 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -47,7 +47,6 @@ show         show
 have         have
 assume       assume
 suppose      suppose
-take         take
 fun          fun
 match        match
 ellipsis     ...
diff --git a/tests/lean/anc1.lean b/tests/lean/anc1.lean
index 37ac99282a..8cb093a896 100644
--- a/tests/lean/anc1.lean
+++ b/tests/lean/anc1.lean
@@ -33,16 +33,16 @@ universe variables u v
   ⟨⟨⟨Hb, ⟨⟩⟩, Ha⟩, ⟨Hc, Ha⟩⟩
 
 #check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
-  take (a : A), assume (H1 : P a) (H2 : Q a),
+  assume (a : A), assume (H1 : P a) (H2 : Q a),
   show ∃ x, P x ∧ Q x, from
   ⟨a, ⟨H1, H2⟩⟩
 
 #check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
-  take (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
+  assume (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
   show ∃ x y, P x ∧ Q y, from
   ⟨a, ⟨b, ⟨H1, H2⟩⟩⟩
 
 #check λ (A : Type u) (P : A → Prop) (Q : A → Prop),
-  take (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
+  assume (a : A) (b : A), assume (H1 : P a) (H2 : Q b),
   show ∃ x y, P x ∧ Q y, from
   ⟨a, b, H1, H2⟩
diff --git a/tests/lean/elab12.lean b/tests/lean/elab12.lean
index 39b7bd1087..c7ed5d7321 100644
--- a/tests/lean/elab12.lean
+++ b/tests/lean/elab12.lean
@@ -1,14 +1,14 @@
-#check (take a : nat, have H : 0, from rfl a,
+#check (assume a : nat, have H : 0, from rfl a,
  (H a a) : ∀ a : nat, a = a)
 
-#check (take a : nat, have H : a = a, from rfl a,
+#check (assume a : nat, have H : a = a, from rfl a,
  (H a a) : ∀ a : nat, a = a)
 
-#check (take a : nat, have H : a = a, from a + 0,
+#check (assume a : nat, have H : a = a, from a + 0,
  (H a a) : ∀ a : nat, a = a)
 
-#check (take a : nat, have H : a = a, from rfl,
+#check (assume a : nat, have H : a = a, from rfl,
  (H a) : ∀ a : nat, a = a)
 
-#check (take a : nat, have H : a = a, from rfl,
+#check (assume a : nat, have H : a = a, from rfl,
  H : ∀ a : nat, a = a)
diff --git a/tests/lean/elab12.lean.expected.out b/tests/lean/elab12.lean.expected.out
index 9f4632c385..9a96c06ddb 100644
--- a/tests/lean/elab12.lean.expected.out
+++ b/tests/lean/elab12.lean.expected.out
@@ -1,22 +1,22 @@
-elab12.lean:1:31: error: type expected at
+elab12.lean:1:33: error: type expected at
   0
-elab12.lean:1:39: error: function expected at
+elab12.lean:1:41: error: function expected at
   rfl
 Additional information:
-elab12.lean:1:39: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
+elab12.lean:1:41: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
   too many arguments
 elab12.lean:2:2: error: function expected at
   H
 λ (a : ℕ), have H : ⁇, from ⁇, ⁇ : ∀ (a : ℕ), a = a
-elab12.lean:4:43: error: function expected at
+elab12.lean:4:45: error: function expected at
   rfl
 Additional information:
-elab12.lean:4:43: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
+elab12.lean:4:45: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
   too many arguments
 elab12.lean:5:2: error: function expected at
   H
 λ (a : ℕ), have H : a = a, from ⁇, ⁇ : ∀ (a : ℕ), a = a
-elab12.lean:7:45: error: invalid have-expression, expression
+elab12.lean:7:47: error: invalid have-expression, expression
   a + 0
 has type
   ℕ
diff --git a/tests/lean/elab13.lean b/tests/lean/elab13.lean
index 521ab6dd73..810d83813a 100644
--- a/tests/lean/elab13.lean
+++ b/tests/lean/elab13.lean
@@ -1,7 +1,7 @@
 open tactic list
 
 #check
-take c : name,
+assume c : name,
 (
 do {
    env  ← get_env,
diff --git a/tests/lean/run/1718.lean b/tests/lean/run/1718.lean
index 30a075d90b..075edba5ce 100644
--- a/tests/lean/run/1718.lean
+++ b/tests/lean/run/1718.lean
@@ -1,11 +1,11 @@
 theorem my_theorem : ∀ (a b c d : ℕ),
   d = c → a = b * c → a = b * d :=
-take a b c d,
+assume a b c d,
 assume h₀ : d = c,
 assume h₁ : a = b * c,
 eq.substr h₀ h₁
 
 example : ∀ (a b c d : ℕ),
   d = c → a = b * c → a = b * d :=
-take a b c d, assume h₀ : d = c, assume h₁ : a = b * c,
+assume a b c d, assume h₀ : d = c, assume h₁ : a = b * c,
 h₀.substr h₁
diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean
index 281f9732bd..83f19bf0c8 100644
--- a/tests/lean/run/nat_bug.lean
+++ b/tests/lean/run/nat_bug.lean
@@ -13,13 +13,13 @@ theorem pred_succ (n : nat) : pred (succ n) = n := refl _
 theorem zero_or_succ (n : nat) : n = zero ∨ n = succ (pred n)
 := nat.rec_on n
     (or.intro_left _ (refl zero))
-    (take m IH, or.intro_right _
+    (assume m IH, or.intro_right _
       (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m))))
 
 theorem zero_or_succ2 (n : nat) : n = zero ∨ n = succ (pred n)
 := nat.rec_on n
     (or.intro_left _ (refl zero))
-    (take m IH, or.intro_right _
+    (assume m IH, or.intro_right _
       (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m))))
 end nat
 end experiment
diff --git a/tests/lean/run/sec_var.lean b/tests/lean/run/sec_var.lean
index a292628e0e..d4ab3b30e4 100644
--- a/tests/lean/run/sec_var.lean
+++ b/tests/lean/run/sec_var.lean
@@ -1,7 +1,7 @@
 section
   parameter A : Type
   definition foo : ∀ ⦃ a b : A ⦄, a = b → a = b :=
-  take a b H, H
+  assume a b H, H
 
   variable a : A
   set_option pp.implicit true
@@ -15,7 +15,7 @@ end
 section
   variable A : Type
   definition foo2 : ∀ ⦃ a b : A ⦄, a = b → a = b :=
-  take a b H, H
+  assume a b H, H
 
   variable a : A
   set_option pp.implicit true