diff --git a/library/init/core.lean b/library/init/core.lean
index 5c5fa92f5e..12ecf36a45 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -631,7 +631,7 @@ infix != := bne
 def implies (a b : Prop) := a → b
 
 theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
-assume hp, h₂ (h₁ hp)
+λ hp, h₂ (h₁ hp)
 
 def trivial : True := ⟨⟩
 
@@ -641,7 +641,7 @@ False.rec (λ _, C) h
 @[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : ¬a) : b :=
 False.elim (h₂ h₁)
 
-theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := assume ha : a, h₂ (h₁ ha)
+theorem mt {a b : Prop} (h₁ : a → b) (h₂ : ¬b) : ¬a := λ ha : a, h₂ (h₁ ha)
 
 theorem notFalse : ¬False := id
 
@@ -679,7 +679,7 @@ theorem ofEqTrue {p : Prop} (h : p = True) : p :=
 h.symm ▸ trivial
 
 theorem notOfEqFalse {p : Prop} (h : p = False) : ¬p :=
-assume hp, h ▸ hp
+λ hp, h ▸ hp
 
 @[macroInline] def cast {α β : Sort u} (h : α = β) (a : α) : β :=
 Eq.rec a h
@@ -704,15 +704,15 @@ theorem Ne.elim (h : a ≠ b) : a = b → False := h
 theorem Ne.irrefl (h : a ≠ a) : False := h rfl
 
 theorem Ne.symm (h : a ≠ b) : b ≠ a :=
-assume (h₁ : b = a), h (h₁.symm)
+λ (h₁ : b = a), h (h₁.symm)
 
 theorem falseOfNe : a ≠ a → False := Ne.irrefl
 
 theorem neFalseOfSelf : p → p ≠ False :=
-assume (hp : p) (Heq : p = False), Heq ▸ hp
+λ (hp : p) (Heq : p = False), Heq ▸ hp
 
 theorem neTrueOfNot : ¬p → p ≠ True :=
-assume (hnp : ¬p) (Heq : p = True), (Heq ▸ hnp) trivial
+λ (hnp : ¬p) (Heq : p = True), (Heq ▸ hnp) trivial
 
 theorem trueNeFalse : ¬True = False :=
 neFalseOfSelf trivial
@@ -777,7 +777,7 @@ theorem And.elim (h₁ : a ∧ b) (h₂ : a → b → c) : c :=
 And.rec h₂ h₁
 
 theorem And.swap : a ∧ b → b ∧ a :=
-assume ⟨ha, hb⟩, ⟨hb, ha⟩
+λ ⟨ha, hb⟩, ⟨hb, ha⟩
 
 def And.symm := @And.swap
 
@@ -803,15 +803,15 @@ theorem iffIffImpliesAndImplies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b 
 Iff.intro (λ h, And.intro h.mp h.mpr) (λ h, Iff.intro h.left h.right)
 
 theorem Iff.refl (a : Prop) : a ↔ a :=
-Iff.intro (assume h, h) (assume h, h)
+Iff.intro (λ h, h) (λ h, h)
 
 theorem Iff.rfl {a : Prop} : a ↔ a :=
 Iff.refl a
 
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
 Iff.intro
-  (assume ha, Iff.mp h₂ (Iff.mp h₁ ha))
-  (assume hc, Iff.mpr h₁ (Iff.mpr h₂ hc))
+  (λ ha, Iff.mp h₂ (Iff.mp h₁ ha))
+  (λ hc, Iff.mpr h₁ (Iff.mpr h₂ hc))
 
 theorem Iff.symm (h : a ↔ b) : b ↔ a :=
 Iff.intro (Iff.right h) (Iff.left h)
@@ -829,8 +829,8 @@ absurd this h₁
 
 theorem notIffNotOfIff (h₁ : a ↔ b) : ¬a ↔ ¬b :=
 Iff.intro
- (assume (hna : ¬ a) (hb : b), hna (Iff.right h₁ hb))
- (assume (hnb : ¬ b) (ha : a), hnb (Iff.left h₁ ha))
+ (λ (hna : ¬ a) (hb : b), hna (Iff.right h₁ hb))
+ (λ (hnb : ¬ b) (ha : a), hnb (Iff.left h₁ ha))
 
 theorem ofIffTrue (h : a ↔ True) : a :=
 Iff.mp (Iff.symm h) trivial
@@ -846,7 +846,7 @@ theorem iffFalseIntro (h : ¬a) : a ↔ False :=
 Iff.intro h (False.rec (λ _, a))
 
 theorem notNotIntro (ha : a) : ¬¬a :=
-assume hna : ¬a, hna ha
+λ hna : ¬a, hna ha
 
 theorem notTrue : (¬ True) ↔ False :=
 iffFalseIntro (notNotIntro trivial)
@@ -957,8 +957,8 @@ variables {p q : Prop}
 @[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∧ q) :=
 if hp : p then
   if hq : q then isTrue ⟨hp, hq⟩
-  else isFalse (assume h : p ∧ q, hq (And.right h))
-else isFalse (assume h : p ∧ q, hp (And.left h))
+  else isFalse (λ h : p ∧ q, hq (And.right h))
+else isFalse (λ h : p ∧ q, hp (And.left h))
 
 @[macroInline] instance [Decidable p] [Decidable q] : Decidable (p ∨ q) :=
 if hp : p then isTrue (Or.inl hp) else
@@ -970,9 +970,9 @@ if hp : p then isFalse (absurd hp) else isTrue hp
 
 @[macroInline] instance implies.Decidable [Decidable p] [Decidable q] : Decidable (p → q) :=
 if hp : p then
-  if hq : q then isTrue (assume h, hq)
-  else isFalse (assume h : p → q, absurd (h hp) hq)
-else isTrue (assume h, absurd h hp)
+  if hq : q then isTrue (λ h, hq)
+  else isFalse (λ h : p → q, absurd (h hp) hq)
+else isTrue (λ h, absurd h hp)
 
 instance [Decidable p] [Decidable q] : Decidable (p ↔ q) :=
 if hp : p then
@@ -1202,11 +1202,11 @@ def RightCommutative (h : β → α → β) := ∀ b a₁ a₂, h (h b a₁) a
 def LeftCommutative  (h : α → β → β) := ∀ a₁ a₂ b, h a₁ (h a₂ b) = h a₂ (h a₁ b)
 
 theorem leftComm : Commutative f → Associative f → LeftCommutative f :=
-assume hcomm hassoc, assume a b c,
+λ hcomm hassoc, λ a b c,
 ((Eq.symm (hassoc a b c)).trans (hcomm a b ▸ rfl : f (f a b) c = f (f b a) c)).trans (hassoc b a c)
 
 theorem rightComm : Commutative f → Associative f → RightCommutative f :=
-assume hcomm hassoc, assume a b c,
+λ hcomm hassoc, λ a b c,
 ((hassoc a b c).trans (hcomm b c ▸ rfl : f a (f b c) = f a (f c b))).trans (Eq.symm (hassoc a c b))
 
 end Binary
@@ -1275,8 +1275,8 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
   | (isTrue e₁) :=
     (match (decEq b b') with
      | (isTrue e₂)  := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
-     | (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂)))
-  | (isFalse n₁) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₁' n₁))}
+     | (isFalse n₂) := isFalse (λ h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂)))
+  | (isFalse n₁) := isFalse (λ h, Prod.noConfusion h (λ e₁' e₂', absurd e₁' n₁))}
 
 instance [HasLess α] [HasLess β] : HasLess (α × β) :=
 ⟨λ s t, s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩
@@ -1560,10 +1560,10 @@ private theorem rel.refl [s : Setoid α] : ∀ q : Quotient s, rel q q :=
 λ q, Quot.inductionOn q (λ a, Setoid.refl a)
 
 private theorem eqImpRel [s : Setoid α] {q₁ q₂ : Quotient s} : q₁ = q₂ → rel q₁ q₂ :=
-assume h, Eq.ndrecOn h (rel.refl q₁)
+λ h, Eq.ndrecOn h (rel.refl q₁)
 
 theorem exact [s : Setoid α] {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
-assume h, eqImpRel h
+λ h, eqImpRel h
 end Exact
 
 section
@@ -1624,7 +1624,7 @@ variables {α : Sort u} {β : α → Sort v}
 
 def Equiv (f₁ f₂ : Π x : α, β x) : Prop := ∀ x, f₁ x = f₂ x
 
-protected theorem Equiv.refl (f : Π x : α, β x) : Equiv f f := assume x, rfl
+protected theorem Equiv.refl (f : Π x : α, β x) : Equiv f f := λ x, rfl
 
 protected theorem Equiv.symm {f₁ f₂ : Π x: α, β x} : Equiv f₁ f₂ → Equiv f₂ f₁ :=
 λ h x, Eq.symm (h x)
@@ -1645,7 +1645,7 @@ private def funSetoid (α : Sort u) (β : α → Sort v) : Setoid (Π x : α, β
 Setoid.mk (@Function.Equiv α β) (Function.Equiv.isEquivalence α β)
 
 private def extfunApp (f : Quotient $ funSetoid α β) : Π x : α, β x :=
-assume x,
+λ x,
 Quot.liftOn f
   (λ f : Π x : α, β x, f x)
   (λ f₁ f₂ h, h x)
@@ -1711,28 +1711,28 @@ have uDef : U u, from chooseSpec exU,
 have vDef : V v, from chooseSpec exV,
 have notUvOrP : u ≠ v ∨ p, from
   Or.elim uDef
-    (assume hut : u = True,
+    (λ hut : u = True,
       Or.elim vDef
-        (assume hvf : v = False,
+        (λ hvf : v = False,
           have hne : u ≠ v, from hvf.symm ▸ hut.symm ▸ trueNeFalse,
           Or.inl hne)
         Or.inr)
     Or.inr,
 have pImpliesUv : p → u = v, from
-  assume hp : p,
+  λ hp : p,
   have hpred : U = V, from
-    funext $ assume x : Prop,
+    funext $ λ x : Prop,
       have hl : (x = True ∨ p) → (x = False ∨ p), from
-        assume a, Or.inr hp,
+        λ a, Or.inr hp,
       have hr : (x = False ∨ p) → (x = True ∨ p), from
-        assume a, Or.inr hp,
+        λ a, Or.inr hp,
       show (x = True ∨ p) = (x = False ∨ p), from
         propext (Iff.intro hl hr),
   have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV, from
     hpred ▸ λ exU exV, rfl,
   show u = v, from h₀ _ _,
 Or.elim notUvOrP
-  (assume hne : u ≠ v, Or.inr (mt pImpliesUv hne))
+  (λ hne : u ≠ v, Or.inr (mt pImpliesUv hne))
   Or.inl
 
 theorem existsTrueOfNonempty {α : Sort u} : Nonempty α → Exists (λ x : α, True)
@@ -1748,8 +1748,8 @@ inhabitedOfNonempty (Exists.elim h (λ w hw, ⟨w⟩))
 /- all propositions are Decidable -/
 noncomputable def propDecidable (a : Prop) : Decidable a :=
 choice $ Or.elim (em a)
-  (assume ha, ⟨isTrue ha⟩)
-  (assume hna, ⟨isFalse hna⟩)
+  (λ ha, ⟨isTrue ha⟩)
+  (λ hna, ⟨isFalse hna⟩)
 
 noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
 ⟨propDecidable a⟩
diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index 7683e52ba2..fbe9a3cdc5 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -492,13 +492,13 @@ theorem natZeroEqZero : Nat.zero = 0 :=
 rfl
 
 protected theorem oneNeZero : 1 ≠ (0 : Nat) :=
-assume h, Nat.noConfusion h
+λ h, Nat.noConfusion h
 
 protected theorem zeroNeOne : 0 ≠ (1 : Nat) :=
-assume h, Nat.noConfusion h
+λ h, Nat.noConfusion h
 
 theorem succNeZero (n : Nat) : succ n ≠ 0 :=
-assume h, Nat.noConfusion h
+λ h, Nat.noConfusion h
 
 protected theorem bit0SuccEq (n : Nat) : bit0 (succ n) = succ (succ (bit0 n)) :=
 show succ (succ n + n) = succ (succ (n + n)), from
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 49674ac597..dc89759ca3 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -27,6 +27,7 @@ namespace Term
 @[builtinTermParser] def type := parser! symbol "Type" maxPrec
 @[builtinTermParser] def sort := parser! symbol "Sort" maxPrec
 @[builtinTermParser] def hole := parser! symbol "_" maxPrec
+@[builtinTermParser] def cdot := parser! symbol "·" maxPrec
 @[inline] def parenSpecial : Parser := optional (", " >> sepBy termParser ", " <|> " : " >> termParser)
 @[builtinTermParser] def paren := parser! symbol "(" maxPrec >> optional (termParser >> parenSpecial) >> ")"
 
diff --git a/library/init/wf.lean b/library/init/wf.lean
index 07d78029db..fd0dc6067d 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -42,7 +42,7 @@ class HasWellFounded (α : Sort u) : Type u :=
 
 namespace WellFounded
 def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) : ∀ a, Acc r a :=
-assume a, WellFounded.recOn wf (λ p, p) a
+λ a, WellFounded.recOn wf (λ p, p) a
 
 section
 variables {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index dd8f6037ea..a12c61f46a 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -703,22 +703,6 @@ static expr parse_lambda(parser & p, unsigned, expr const *, pos_info const & po
     return parse_lambda_core(p, pos);
 }
 
-static expr parse_assume(parser & p, unsigned, expr const *, pos_info const & pos) {
-    if (p.curr_is_token(get_colon_tk())) {
-        // anonymous `assume`
-        p.next();
-        expr prop = p.parse_expr();
-        p.check_token_next(get_comma_tk(), "invalid 'assume', ',' expected");
-        parser::local_scope scope(p);
-        expr l = p.save_pos(mk_local(get_this_tk(), prop), pos);
-        p.add_local(l);
-        expr body = p.parse_expr();
-        return p.save_pos(Fun(l, body, p), pos);
-    } else {
-        return parse_lambda_core(p, pos);
-    }
-}
-
 static expr parse_list(parser & p, unsigned, expr const *, pos_info const & pos) {
     buffer<expr> elems;
     if (!p.curr_is_token(get_rbracket_tk())) {
@@ -851,7 +835,6 @@ parse_table init_nud_table() {
     expr x0 = mk_bvar(0);
     parse_table r;
     r = r.add({transition("have", mk_ext_action(parse_have))}, x0);
-    r = r.add({transition("assume", mk_ext_action(parse_assume))}, x0);
     r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
     r = r.add({transition("suffices", mk_ext_action(parse_suffices))}, x0);
     r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);