diff --git a/library/init/classical.lean b/library/init/classical.lean
index afad3988d1..426712d73d 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -11,7 +11,7 @@ universe variables u v
 /- the axiom -/
 
 -- In the presence of classical logic, we could prove this from a weaker statement:
--- axiom indefinite_description {A : Type u} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
+-- axiom indefinite_description {A : Type u} {P : A->Prop} (H : ∃ x, P x) : {x : A, P x}
 axiom strong_indefinite_description {A : Type u} (P : A → Prop) (H : nonempty A) :
   { x \ (∃ y : A, P y) → P x}
 
@@ -19,7 +19,7 @@ theorem exists_true_of_nonempty {A : Type u} (H : nonempty A) : ∃ x : A, true
 nonempty.elim H (take x, ⟨x, trivial⟩)
 
 noncomputable definition inhabited_of_nonempty {A : Type u} (H : nonempty A) : inhabited A :=
-⟨elt_of (strong_indefinite_description (λa, true) H)⟩
+⟨elt_of (strong_indefinite_description (λ a, true) H)⟩
 
 noncomputable definition inhabited_of_exists {A : Type u} {P : A → Prop} (H : ∃ x, P x) : inhabited A :=
 inhabited_of_nonempty (exists.elim H (λ w Hw, ⟨w⟩))
@@ -59,7 +59,7 @@ theorem skolem {A : Type u} {B : A → Type 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)),
+    take x, exists.elim H (λ (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)),
       ⟨fw x, Hw x⟩))
 /-
 Prove excluded middle using Hilbert's choice
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 3bf1a3ca6b..d52d10b2e8 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -83,7 +83,7 @@ inductive pos_num : Type
 
 namespace pos_num
   definition succ (a : pos_num) : pos_num :=
-  pos_num.rec_on a (bit0 one) (λn r, bit0 r) (λn r, bit1 n)
+  pos_num.rec_on a (bit0 one) (λ n r, bit0 r) (λ n r, bit1 n)
 end pos_num
 
 inductive num : Type
@@ -93,7 +93,7 @@ inductive num : Type
 namespace num
   open pos_num
   definition succ (a : num) : num :=
-  num.rec_on a (pos one) (λp, pos (succ p))
+  num.rec_on a (pos one) (λ p, pos (succ p))
 end num
 
 inductive bool : Type
@@ -170,25 +170,25 @@ definition pos_num_has_one : has_one pos_num :=
 
 namespace pos_num
   definition is_one (a : pos_num) : bool :=
-  pos_num.rec_on a tt (λn r, ff) (λn r, ff)
+  pos_num.rec_on a tt (λ n r, ff) (λ n r, ff)
 
   definition pred (a : pos_num) : pos_num :=
-  pos_num.rec_on a one (λn r, bit0 n) (λn r, bool.rec_on (is_one n) (bit1 r) one)
+  pos_num.rec_on a one (λ n r, bit0 n) (λ n r, bool.rec_on (is_one n) (bit1 r) one)
 
   definition size (a : pos_num) : pos_num :=
-  pos_num.rec_on a one (λn r, succ r) (λn r, succ r)
+  pos_num.rec_on a one (λ n r, succ r) (λ n r, succ r)
 
   definition add (a b : pos_num) : pos_num :=
   pos_num.rec_on a
     succ
-    (λn f b, pos_num.rec_on b
+    (λ n f b, pos_num.rec_on b
       (succ (bit1 n))
-      (λm r, succ (bit1 (f m)))
-      (λm r, bit1 (f m)))
-    (λn f b, pos_num.rec_on b
+      (λ m r, succ (bit1 (f m)))
+      (λ m r, bit1 (f m)))
+    (λ n f b, pos_num.rec_on b
       (bit1 n)
-      (λm r, bit1 (f m))
-      (λm r, bit0 (f m)))
+      (λ m r, bit1 (f m))
+      (λ m r, bit0 (f m)))
     b
 end pos_num
 
@@ -200,7 +200,7 @@ namespace num
   open pos_num
 
   definition add (a b : num) : num :=
-  num.rec_on a b (λpa, num.rec_on b (pos pa) (λpb, pos (pos_num.add pa pb)))
+  num.rec_on a b (λ pa, num.rec_on b (pos pa) (λ pb, pos (pos_num.add pa pb)))
 end num
 
 attribute [instance]
diff --git a/library/init/function.lean b/library/init/function.lean
index e43ee743f7..5cac2399c3 100644
--- a/library/init/function.lean
+++ b/library/init/function.lean
@@ -13,12 +13,12 @@ variables {A : Type u_a} {B : Type u_b} {C : Type u_c} {D : Type u_d} {E : Type
 
 attribute [inline, reducible]
 definition function.comp (f : B → C) (g : A → B) : A → C :=
-λx, f (g x)
+λ x, f (g x)
 
 attribute [inline, reducible]
 definition function.dcomp {B : A → Type u_b} {C : Π {x : A}, B x → Type u_c}
-  (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
-λx, f (g x)
+  (f : Π {x : A} (y : B x), C y) (g : Π x, B x) : Π x, C (g x) :=
+λ x, f (g x)
 
 infixr  ` ∘ `      := function.comp
 infixr  ` ∘' `:80  := function.dcomp
@@ -35,23 +35,23 @@ definition comp_left (f : B → B → B) (g : A → B) : A → B → B :=
 
 attribute [reducible]
 definition on_fun (f : B → B → C) (g : A → B) : A → A → C :=
-λx y, f (g x) (g y)
+λ x y, f (g x) (g y)
 
 attribute [reducible]
 definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D)
   : A → B → E :=
-λx y, op (f x y) (g x y)
+λ x y, op (f x y) (g x y)
 
 attribute [reducible]
 definition const (B : Type u_b) (a : A) : B → A :=
-λx, a
+λ x, a
 
 attribute [reducible]
-definition swap {C : A → B → Type u_c} (f : Πx y, C x y) : Πy x, C x y :=
-λy x, f x y
+definition swap {C : A → B → Type u_c} (f : Π x y, C x y) : Π y x, C x y :=
+λ y x, f x y
 
 attribute [reducible]
-definition app {B : A → Type u_b} (f : Πx, B x) (x : A) : B x :=
+definition app {B : A → Type u_b} (f : Π x, B x) (x : A) : B x :=
 f x
 
 attribute [reducible]
@@ -106,7 +106,7 @@ and.elim Hg (λ Hginj Hgsurj, and.elim Hf (λ Hfinj Hfsurj,
   ⟨injective_comp Hginj Hfinj, surjective_comp Hgsurj Hfsurj⟩))
 
 -- g is a left inverse to f
-definition left_inverse (g : B → A) (f : A → B) : Prop := ∀x, g (f x) = x
+definition left_inverse (g : B → A) (f : A → B) : Prop := ∀ x, g (f x) = x
 
 definition id_of_left_inverse {g : B → A} {f : A → B} : left_inverse g f → g ∘ f = id :=
 assume h, funext h
diff --git a/library/init/funext.lean b/library/init/funext.lean
index d487d4a4d3..b5e7563d9f 100644
--- a/library/init/funext.lean
+++ b/library/init/funext.lean
@@ -34,7 +34,7 @@ section
   variables {A : Type u} {B : A → Type v}
 
   attribute [instance]
-  private definition fun_setoid (A : Type u) (B : A → Type v) : setoid (Πx : A, B x) :=
+  private definition fun_setoid (A : Type u) (B : A → Type v) : setoid (Π x : A, B x) :=
   setoid.mk (@function.equiv A B) (function.equiv.is_equivalence A B)
 
   private definition extfun (A : Type u) (B : A → Type v) : Type (imax u v) :=
diff --git a/library/init/logic.lean b/library/init/logic.lean
index f18301750d..ac6eefbade 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -349,16 +349,16 @@ iff.intro
 
 theorem imp_congr (h₁ : a ↔ c) (h₂ : b ↔ d) : (a → b) ↔ (c → d) :=
 iff.intro
-  (λhab hc, iff.mp h₂ (hab (iff.mpr h₁ hc)))
-  (λhcd ha, iff.mpr h₂ (hcd (iff.mp h₁ ha)))
+  (λ hab hc, iff.mp h₂ (hab (iff.mpr h₁ hc)))
+  (λ hcd ha, iff.mpr h₂ (hcd (iff.mp h₁ ha)))
 
 theorem imp_congr_ctx (h₁ : a ↔ c) (h₂ : c → (b ↔ d)) : (a → b) ↔ (c → d) :=
 iff.intro
-  (λhab hc, have ha : a, from iff.mpr h₁ hc,
-            have hb : b, from hab ha,
-            iff.mp (h₂ hc) hb)
-  (λhcd ha, have hc : c, from iff.mp h₁ ha,
-            have hd : d, from hcd hc,
+  (λ hab hc, have ha : a, from iff.mpr h₁ hc,
+             have hb : b, from hab ha,
+             iff.mp (h₂ hc) hb)
+  (λ hcd ha, have hc : c, from iff.mp h₁ ha,
+             have hd : d, from hcd hc,
 iff.mpr (h₂ hc) hd)
 
 theorem imp_congr_right (h : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
@@ -583,24 +583,24 @@ notation `∃` binders `, ` r:(scoped P, Exists P) := r
 attribute Exists.rec [elim]
 
 theorem exists.elim {A : Type u} {p : A → Prop} {b : Prop}
-  (h₁ : ∃x, p x) (h₂ : ∀ (a : A), p a → b) : b :=
+  (h₁ : ∃ x, p x) (h₂ : ∀ (a : A), p a → b) : b :=
 Exists.rec h₂ h₁
 
 /- exists unique -/
 
 definition exists_unique {A : Type u} (p : A → Prop) :=
-∃x, p x ∧ ∀y, p y → y = x
+∃ x, p x ∧ ∀ y, p y → y = x
 
 notation `∃!` binders `, ` r:(scoped P, exists_unique P) := r
 
 attribute [intro]
-theorem exists_unique.intro {A : Type u} {p : A → Prop} (w : A) (h₁ : p w) (h₂ : ∀y, p y → y = w) :
-  ∃!x, p x :=
+theorem exists_unique.intro {A : Type u} {p : A → Prop} (w : A) (h₁ : p w) (h₂ : ∀ y, p y → y = w) :
+  ∃! x, p x :=
 exists.intro w ⟨h₁, h₂⟩
 
 attribute [recursor 4, elim]
 theorem exists_unique.elim {A : Type u} {p : A → Prop} {b : Prop}
-    (h₂ : ∃!x, p x) (h₁ : ∀x, p x → (∀y, p y → y = x) → b) : b :=
+    (h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b :=
 exists.elim h₂ (λ w hw, h₁ w (and.left hw) (and.right hw))
 
 theorem exists_unique_of_exists_of_unique {A : Type u} {p : A → Prop}
@@ -628,12 +628,12 @@ exists.elim p (λ a hp, ⟨a, h a hp⟩)
 attribute [congr]
 theorem exists_congr {A : Type u} {p q : A → Prop} (h : ∀ a, (p a ↔ q a)) : (Exists p) ↔ ∃ a, q a :=
 iff.intro
-  (exists_imp_exists (λa, iff.mp (h a)))
-  (exists_imp_exists (λa, iff.mpr (h a)))
+  (exists_imp_exists (λ a, iff.mp (h a)))
+  (exists_imp_exists (λ a, iff.mpr (h a)))
 
 attribute [congr]
 theorem exists_unique_congr {A : Type u} {p₁ p₂ : A → Prop} (h : ∀ x, p₁ x ↔ p₂ x) : (exists_unique p₁) ↔ (∃! x, p₂ x) := --
-exists_congr (λ x, and_congr (h x) (forall_congr (λy, imp_congr (h y) iff.rfl)))
+exists_congr (λ x, and_congr (h x) (forall_congr (λ y, imp_congr (h y) iff.rfl)))
 
 /- decidable -/
 
@@ -668,11 +668,11 @@ namespace decidable
 
   definition rec_on_true [h : decidable p] {h₁ : p → Type u} {h₂ : ¬p → Type u} (h₃ : p) (h₄ : h₁ h₃)
       : decidable.rec_on h h₂ h₁ :=
-  decidable.rec_on h (λh, false.rec _ (h h₃)) (λh, h₄)
+  decidable.rec_on h (λ h, false.rec _ (h h₃)) (λ h, h₄)
 
   definition rec_on_false [h : decidable p] {h₁ : p → Type u} {h₂ : ¬p → Type u} (h₃ : ¬p) (h₄ : h₂ h₃)
       : decidable.rec_on h h₂ h₁ :=
-  decidable.rec_on h (λh, h₄) (λh, false.rec _ (h₃ h))
+  decidable.rec_on h (λ h, h₄) (λ h, false.rec _ (h₃ h))
 
   definition by_cases {q : Type u} [C : decidable p] : (p → q) → (¬p → q) → q := dite _
 
@@ -752,7 +752,7 @@ definition is_dec_refl {A : Type u} (p : A → A → bool) : Prop := ∀ x, p x
 
 open decidable
 attribute [instance]
-protected definition bool.has_decidable_eq : ∀a b : bool, decidable (a = b)
+protected definition bool.has_decidable_eq : ∀ a b : bool, decidable (a = b)
 | ff ff := is_true rfl
 | ff tt := is_false bool.ff_ne_tt
 | tt ff := is_false (ne.symm bool.ff_ne_tt)
@@ -806,8 +806,8 @@ definition inhabited_fun (A : Type u) {B : Type v} [h : inhabited B] : inhabited
 inhabited.rec_on h (λ b, ⟨λ a, b⟩)
 
 attribute [instance]
-definition inhabited_Pi (A : Type u) {B : A → Type v} [Πx, inhabited (B x)] :
-  inhabited (Πx, B x) :=
+definition inhabited_Pi (A : Type u) {B : A → Type v} [Π x, inhabited (B x)] :
+  inhabited (Π x, B x) :=
 ⟨λ a, default (B a)⟩
 
 attribute [inline, instance]
@@ -868,7 +868,7 @@ subsingleton.intro (λ d₁,
 
 protected theorem rec_subsingleton {p : Prop} [h : decidable p]
     {h₁ : p → Type u} {h₂ : ¬p → Type u}
-    [h₃ : Π(h : p), subsingleton (h₁ h)] [h₄ : Π(h : ¬p), subsingleton (h₂ h)]
+    [h₃ : Π (h : p), subsingleton (h₁ h)] [h₄ : Π (h : ¬p), subsingleton (h₂ h)]
   : subsingleton (decidable.rec_on h h₂ h₁) :=
 match h with
 | (is_true h)  := h₃ h
@@ -998,7 +998,7 @@ theorem dif_ctx_simp_congr {A : Type u} {b c : Prop} [dec_b : decidable b]
 @dif_ctx_congr A b c dec_b (decidable_of_decidable_of_iff dec_b h_c) x u y v h_c h_t h_e
 
 -- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
-theorem dite_ite_eq (c : Prop) [h : decidable c] {A : Type u} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
+theorem dite_ite_eq (c : Prop) [h : decidable c] {A : Type u} (t : A) (e : A) : dite c (λ h, t) (λ h, e) = ite c t e :=
 match h with
 | (is_true hc)   := rfl
 | (is_false hnc) := rfl
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 3888f8aa16..a261dd2351 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -150,29 +150,29 @@ namespace nat
   theorem pred_le_iff_true (n : ℕ) : pred n ≤ n ↔ true :=
   iff_true_intro (pred_le n)
 
-  protected theorem le_trans {n m k : ℕ} (H1 : n ≤ m) : m ≤ k → n ≤ k :=
-  le.rec H1 (λp H2, le.step)
+  protected theorem le_trans {n m k : ℕ} (h1 : n ≤ m) : m ≤ k → n ≤ k :=
+  le.rec h1 (λ p h2, le.step)
 
-  theorem le_succ_of_le {n m : ℕ} (H : n ≤ m) : n ≤ succ m :=
-  nat.le_trans H (le_succ m)
+  theorem le_succ_of_le {n m : ℕ} (h : n ≤ m) : n ≤ succ m :=
+  nat.le_trans h (le_succ m)
 
-  theorem le_of_succ_le {n m : ℕ} (H : succ n ≤ m) : n ≤ m :=
-  nat.le_trans (le_succ n) H
+  theorem le_of_succ_le {n m : ℕ} (h : succ n ≤ m) : n ≤ m :=
+  nat.le_trans (le_succ n) h
 
-  protected theorem le_of_lt {n m : ℕ} (H : n < m) : n ≤ m :=
-  le_of_succ_le H
+  protected theorem le_of_lt {n m : ℕ} (h : n < m) : n ≤ m :=
+  le_of_succ_le h
 
   theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
-  λ H, le.rec (nat.le_refl (succ n)) (λ a b, le.step) H
+  λ h, le.rec (nat.le_refl (succ n)) (λ a b, le.step) h
 
   theorem pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
-  λ H, le.rec (nat.le_refl (pred n)) (λ n, nat.rec (λ a b, b) (λ a b c, le.step) n) H
+  λ h, le.rec (nat.le_refl (pred n)) (λ n, nat.rec (λ a b, b) (λ a b c, le.step) n) h
 
   theorem le_of_succ_le_succ {n m : ℕ} : succ n ≤ succ m → n ≤ m :=
   pred_le_pred
 
   theorem le_succ_of_pred_le {n m : ℕ} : pred n ≤ m → n ≤ succ m :=
-  nat.cases_on n le.step (λa, succ_le_succ)
+  nat.cases_on n le.step (λ a, succ_le_succ)
 
   theorem not_succ_le_zero : ∀ (n : ℕ), succ n ≤ 0 → false
   .
@@ -181,7 +181,7 @@ namespace nat
   iff_false_intro (not_succ_le_zero n)
 
   theorem not_succ_le_self : ∀ n : ℕ, ¬succ n ≤ n :=
-  λ n, nat.rec (not_succ_le_zero 0) (λa b c, b (le_of_succ_le_succ c)) n
+  λ n, nat.rec (not_succ_le_zero 0) (λ a b c, b (le_of_succ_le_succ c)) n
 
   attribute [simp]
   theorem succ_le_self_iff_false (n : ℕ) : succ n ≤ n ↔ false :=
@@ -215,11 +215,11 @@ namespace nat
   theorem zero_lt_succ_iff_true (n : ℕ) : 0 < succ n ↔ true :=
   iff_true_intro (zero_lt_succ n)
 
-  protected theorem lt_trans {n m k : ℕ} (H1 : n < m) : m < k → n < k :=
-  nat.le_trans (le.step H1)
+  protected theorem lt_trans {n m k : ℕ} (h₁ : n < m) : m < k → n < k :=
+  nat.le_trans (le.step h₁)
 
-  protected theorem lt_of_le_of_lt {n m k : ℕ} (H1 : n ≤ m) : m < k → n < k :=
-  nat.le_trans (succ_le_succ H1)
+  protected theorem lt_of_le_of_lt {n m k : ℕ} (h₁ : n ≤ m) : m < k → n < k :=
+  nat.le_trans (succ_le_succ h₁)
 
   protected theorem lt_of_lt_of_le {n m k : ℕ} : n < m → m ≤ k → n < k := nat.le_trans
 
@@ -227,7 +227,7 @@ namespace nat
   not_succ_le_self n
 
   theorem lt_self_iff_false (n : ℕ) : n < n ↔ false :=
-  iff_false_intro (λ H, absurd H (nat.lt_irrefl n))
+  iff_false_intro (λ h, absurd h (nat.lt_irrefl n))
 
   theorem self_lt_succ (n : ℕ) : n < succ n := nat.le_refl (succ n)
 
@@ -237,17 +237,17 @@ namespace nat
 
   definition lt.base (n : ℕ) : n < succ n := nat.le_refl (succ n)
 
-  theorem le_lt_antisymm {n m : ℕ} (H1 : n ≤ m) (H2 : m < n) : false :=
-  nat.lt_irrefl n (nat.lt_of_le_of_lt H1 H2)
+  theorem le_lt_antisymm {n m : ℕ} (h₁ : n ≤ m) (h₂ : m < n) : false :=
+  nat.lt_irrefl n (nat.lt_of_le_of_lt h₁ h₂)
 
-  protected theorem le_antisymm {n m : ℕ} (H1 : n ≤ m) : m ≤ n → n = m :=
-  le.cases_on H1 (λa, rfl) (λa b c, absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n))
+  protected theorem le_antisymm {n m : ℕ} (h₁ : n ≤ m) : m ≤ n → n = m :=
+  le.cases_on h₁ (λ a, rfl) (λ a b c, absurd (nat.lt_of_le_of_lt b c) (nat.lt_irrefl n))
 
-  theorem lt_le_antisymm {n m : ℕ} (H1 : n < m) (H2 : m ≤ n) : false :=
-  le_lt_antisymm H2 H1
+  theorem lt_le_antisymm {n m : ℕ} (h₁ : n < m) (h₂ : m ≤ n) : false :=
+  le_lt_antisymm h₂ h₁
 
-  protected theorem nat.lt_asymm {n m : ℕ} (H1 : n < m) : ¬ m < n :=
-  le_lt_antisymm (nat.le_of_lt H1)
+  protected theorem nat.lt_asymm {n m : ℕ} (h₁ : n < m) : ¬ m < n :=
+  le_lt_antisymm (nat.le_of_lt h₁)
 
   theorem not_lt_zero (a : ℕ) : ¬ a < 0 := not_succ_le_zero a
 
@@ -255,11 +255,11 @@ namespace nat
   theorem lt_zero_iff_false (a : ℕ) : a < 0 ↔ false :=
   iff_false_intro (not_lt_zero a)
 
-  protected theorem eq_or_lt_of_le {a b : ℕ} (H : a ≤ b) : a = b ∨ a < b :=
-  le.cases_on H (or.inl rfl) (λn h, or.inr (succ_le_succ h))
+  protected theorem eq_or_lt_of_le {a b : ℕ} (h : a ≤ b) : a = b ∨ a < b :=
+  le.cases_on h (or.inl rfl) (λ n h, or.inr (succ_le_succ h))
 
-  protected theorem le_of_eq_or_lt {a b : ℕ} (H : a = b ∨ a < b) : a ≤ b :=
-  or.elim H nat.le_of_eq nat.le_of_lt
+  protected theorem le_of_eq_or_lt {a b : ℕ} (h : a = b ∨ a < b) : a ≤ b :=
+  or.elim h nat.le_of_eq nat.le_of_lt
 
   theorem succ_lt_succ {a b : ℕ} : a < b → succ a < succ b :=
   succ_le_succ
@@ -271,17 +271,17 @@ namespace nat
   le_of_succ_le_succ
 
   attribute [instance, priority nat.prio]
-  protected definition decidable_le : ∀ a b : nat, decidable (a ≤ b)
+  protected definition decidable_le : ∀ a b : ℕ, decidable (a ≤ b)
   | 0     b     := is_true (zero_le b)
   | (a+1) 0     := is_false (not_succ_le_zero a)
   | (a+1) (b+1) :=
     match decidable_le a b with
-    | is_true H  := is_true (succ_le_succ H)
-    | is_false H := is_false (λa, H (le_of_succ_le_succ a))
+    | is_true h  := is_true (succ_le_succ h)
+    | is_false h := is_false (λ a, h (le_of_succ_le_succ a))
     end
 
   attribute [instance, priority nat.prio]
-  protected definition decidable_lt : ∀ a b : nat, decidable (a < b) :=
+  protected definition decidable_lt : ∀ a b : ℕ, decidable (a < b) :=
   λ a b, nat.decidable_le (succ a) b
 
   protected theorem lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b
@@ -296,16 +296,16 @@ namespace nat
       end
     end
 
-  protected definition {u} lt_ge_by_cases {a b : ℕ} {P : Type u} (H1 : a < b → P) (H2 : a ≥ b → P) : P :=
-  decidable.by_cases H1 (λh, H2 (or.elim (nat.lt_or_ge a b) (λa, absurd a h) (λa, a)))
+  protected definition {u} lt_ge_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a ≥ b → C) : C :=
+  decidable.by_cases h₁ (λ h, h₂ (or.elim (nat.lt_or_ge a b) (λ a, absurd a h) (λ a, a)))
 
-  protected definition {u} lt_by_cases {a b : ℕ} {P : Type u} (H1 : a < b → P) (H2 : a = b → P)
-    (H3 : b < a → P) : P :=
-  nat.lt_ge_by_cases H1 (λh₁,
-    nat.lt_ge_by_cases H3 (λh₂, H2 (nat.le_antisymm h₂ h₁)))
+  protected definition {u} lt_by_cases {a b : ℕ} {C : Type u} (h₁ : a < b → C) (h₂ : a = b → C)
+    (h₃ : b < a → C) : C :=
+  nat.lt_ge_by_cases h₁ (λ h₁,
+    nat.lt_ge_by_cases h₃ (λ h, h₂ (nat.le_antisymm h h₁)))
 
   protected theorem lt_trichotomy (a b : ℕ) : a < b ∨ a = b ∨ b < a :=
-  nat.lt_by_cases (λH, or.inl H) (λH, or.inr (or.inl H)) (λH, or.inr (or.inr H))
+  nat.lt_by_cases (λ h, or.inl h) (λ h, or.inr (or.inl h)) (λ h, or.inr (or.inr h))
 
   protected theorem eq_or_lt_of_not_lt {a b : ℕ} (hnlt : ¬ a < b) : a = b ∨ b < a :=
   or.elim (nat.lt_trichotomy a b)
@@ -365,11 +365,11 @@ namespace nat
   theorem le_add_left (n m : ℕ): n ≤ m + n :=
   nat.add_comm n m ▸ le_add_right n m
 
-  definition {u} repeat {A : Type u} (f : nat → A → A) : nat → A → A
+  definition {u} repeat {A : Type u} (f : ℕ → A → A) : ℕ → A → A
   | 0         a := a
   | (succ n)  a := f n (repeat n a)
 
   attribute [instance]
-  protected definition is_inhabited : inhabited nat :=
+  protected definition is_inhabited : inhabited ℕ :=
   ⟨nat.zero⟩
 end nat
diff --git a/library/init/num.lean b/library/init/num.lean
index a13fc16b28..9a9194cb04 100644
--- a/library/init/num.lean
+++ b/library/init/num.lean
@@ -10,23 +10,23 @@ namespace pos_num
   protected definition mul (a b : pos_num) : pos_num :=
   pos_num.rec_on a
     b
-    (λn r, bit0 r + b)
-    (λn r, bit0 r)
+    (λ n r, bit0 r + b)
+    (λ n r, bit0 r)
 
   definition lt (a b : pos_num) : bool :=
   pos_num.rec_on a
     (λ b, pos_num.cases_on b
       ff
-      (λm, tt)
-      (λm, tt))
-    (λn f b, pos_num.cases_on b
+      (λ m, tt)
+      (λ m, tt))
+    (λ n f b, pos_num.cases_on b
       ff
-      (λm, f m)
-      (λm, f m))
-    (λn f b, pos_num.cases_on b
+      (λ m, f m)
+      (λ m, f m))
+    (λ n f b, pos_num.cases_on b
       ff
-      (λm, f (succ m))
-      (λm, f m))
+      (λ m, f (succ m))
+      (λ m, f m))
     b
 
   definition le (a b : pos_num) : bool :=
@@ -41,13 +41,13 @@ namespace num
   open pos_num
 
   definition pred (a : num) : num :=
-  num.rec_on a zero (λp, bool.cond (is_one p) zero (pos (pred p)))
+  num.rec_on a zero (λ p, bool.cond (is_one p) zero (pos (pred p)))
 
   definition size (a : num) : num :=
-  num.rec_on a (pos pos_num.one) (λp, pos (size p))
+  num.rec_on a (pos pos_num.one) (λ p, pos (size p))
 
   protected definition mul (a b : num) : num :=
-  num.rec_on a zero (λpa, num.rec_on b zero (λpb, pos (pos_num.mul pa pb)))
+  num.rec_on a zero (λ pa, num.rec_on b zero (λ pb, pos (pos_num.mul pa pb)))
 end num
 
 attribute [instance]
@@ -56,29 +56,29 @@ definition num_has_mul : has_mul num :=
 
 namespace num
   protected definition le (a b : num) : bool :=
-  num.rec_on a tt (λpa, num.rec_on b ff (λpb, pos_num.le pa pb))
+  num.rec_on a tt (λ pa, num.rec_on b ff (λ pb, pos_num.le pa pb))
 
   private definition psub (a b : pos_num) : num :=
   pos_num.rec_on a
-    (λb, zero)
-    (λn f b,
+    (λ b, zero)
+    (λ n f b,
       bool.cond (pos_num.le (bit1 n) b)
         zero
         (pos_num.cases_on b
            (pos (bit0 n))
-           (λm, 2 * f m)
-           (λm, 2 * f m + 1)))
-    (λn f b,
+           (λ m, 2 * f m)
+           (λ m, 2 * f m + 1)))
+    (λ n f b,
       bool.cond (pos_num.le (bit0 n) b)
         zero
         (pos_num.cases_on b
            (pos (pos_num.pred (bit0 n)))
-           (λm, pred (2 * f m))
-           (λm, 2 * f m)))
+           (λ m, pred (2 * f m))
+           (λ m, 2 * f m)))
     b
 
   protected definition sub (a b : num) : num :=
-  num.rec_on a zero (λpa, num.rec_on b a (λpb, psub pa pb))
+  num.rec_on a zero (λ pa, num.rec_on b a (λ pb, psub pa pb))
 end num
 
 attribute [instance]
diff --git a/library/init/relation.lean b/library/init/relation.lean
index 1ff0e56e90..8a4e7ba4a2 100644
--- a/library/init/relation.lean
+++ b/library/init/relation.lean
@@ -45,5 +45,5 @@ theorem inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive (i
 λ (a : A) (H₁ : inv_image R f a a), H (f a) H₁
 
 inductive tc {A : Type u} (R : A → A → Prop) : A → A → Prop
-| base  : ∀a b, R a b → tc a b
-| trans : ∀a b c, tc a b → tc b c → tc a c
+| base  : ∀ a b, R a b → tc a b
+| trans : ∀ a b c, tc a b → tc b c → tc a c
diff --git a/library/init/sigma_lex.lean b/library/init/sigma_lex.lean
index f57189ccee..545ca81015 100644
--- a/library/init/sigma_lex.lean
+++ b/library/init/sigma_lex.lean
@@ -25,16 +25,16 @@ section
   parameters {Ra  : A → A → Prop} {Rb : Π a : A, B a → B a → Prop}
   local infix `≺`:50 := lex Ra Rb
 
-  definition lex_accessible {a} (aca : acc Ra a) (acb : ∀a, well_founded (Rb a))
+  definition lex_accessible {a} (aca : acc Ra a) (acb : ∀ a, well_founded (Rb a))
              : ∀ (b : B a), acc (lex Ra Rb) (sigma.mk a b) :=
   acc.rec_on aca
-    (λxa aca (iHa : ∀y, Ra y xa → ∀b : B y, acc (lex Ra Rb) (sigma.mk y b)),
-      λb : B xa, acc.rec_on (well_founded.apply (acb xa) b)
-        (λxb acb
+    (λ xa aca (iHa : ∀ y, Ra y xa → ∀ b : B y, acc (lex Ra Rb) (sigma.mk y b)),
+      λ b : B xa, acc.rec_on (well_founded.apply (acb xa) b)
+        (λ xb acb
           (iHb : ∀ (y : B xa), Rb xa y xb → acc (lex Ra Rb) (sigma.mk xa y)),
-          acc.intro (sigma.mk xa xb) (λp (lt : p ≺ (sigma.mk xa xb)),
+          acc.intro (sigma.mk xa xb) (λ p (lt : p ≺ (sigma.mk xa xb)),
             have aux : xa = xa → xb == xb → acc (lex Ra Rb) p, from
-              @sigma.lex.rec_on A B Ra Rb (λp₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex Ra Rb) p₁)
+              @sigma.lex.rec_on A B Ra Rb (λ p₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex Ra Rb) p₁)
                                 p (sigma.mk xa xb) lt
                 (λ (a₁ : A) (b₁ : B a₁) (a₂ : A) (b₂ : B a₂) (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
                   by do
@@ -50,7 +50,7 @@ section
 
   -- The lexicographical order of well founded relations is well-founded
   definition lex_wf (Ha : well_founded Ra) (Hb : ∀ x, well_founded (Rb x)) : well_founded (lex Ra Rb) :=
-  well_founded.intro (λp, destruct p (λa b, lex_accessible (well_founded.apply Ha a) Hb b))
+  well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply Ha a) Hb b))
 end
 
 section
@@ -61,7 +61,7 @@ section
 
   definition lex_ndep_wf {Ra  : A → A → Prop} {Rb : B → B → Prop} (Ha : well_founded Ra) (Hb : well_founded Rb)
                          : well_founded (lex_ndep Ra Rb) :=
-  well_founded.intro (λp, destruct p (λa b, lex_accessible (well_founded.apply Ha a) (λ x, Hb) b))
+  well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply Ha a) (λ x, Hb) b))
 end
 
 section
@@ -81,14 +81,14 @@ section
   parameters {Ra  : A → A → Prop} {Rb : B → B → Prop}
   local infix `≺`:50 := rev_lex Ra Rb
 
-  definition rev_lex_accessible {b} (acb : acc Rb b) (aca : ∀a, acc Ra a): ∀a, acc (rev_lex Ra Rb) (sigma.mk a b) :=
+  definition rev_lex_accessible {b} (acb : acc Rb b) (aca : ∀ a, acc Ra a): ∀ a, acc (rev_lex Ra Rb) (sigma.mk a b) :=
   acc.rec_on acb
-    (λxb acb (iHb : ∀y, Rb y xb → ∀a, acc (rev_lex Ra Rb) (sigma.mk a y)),
-      λa, acc.rec_on (aca a)
-        (λxa aca (iHa : ∀ y, Ra y xa → acc (rev_lex Ra Rb) (mk y xb)),
-          acc.intro (sigma.mk xa xb) (λp (lt : p ≺ (sigma.mk xa xb)),
+    (λ xb acb (iHb : ∀ y, Rb y xb → ∀ a, acc (rev_lex Ra Rb) (sigma.mk a y)),
+      λ a, acc.rec_on (aca a)
+        (λ xa aca (iHa : ∀ y, Ra y xa → acc (rev_lex Ra Rb) (mk y xb)),
+          acc.intro (sigma.mk xa xb) (λ p (lt : p ≺ (sigma.mk xa xb)),
             have aux : xa = xa → xb = xb → acc (rev_lex Ra Rb) p, from
-              @rev_lex.rec_on A B Ra Rb (λp₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (rev_lex Ra Rb) p₁)
+              @rev_lex.rec_on A B Ra Rb (λ p₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (rev_lex Ra Rb) p₁)
                               p (sigma.mk xa xb) lt
                (λ a₁ a₂ b (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b = xb),
                  show acc (rev_lex Ra Rb) (sigma.mk a₁ b), from
@@ -102,7 +102,7 @@ section
             aux rfl rfl)))
 
   definition rev_lex_wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rev_lex Ra Rb) :=
-  well_founded.intro (λp, destruct p (λa b, rev_lex_accessible (apply Hb b) (well_founded.apply Ha) a))
+  well_founded.intro (λ p, destruct p (λ a b, rev_lex_accessible (apply Hb b) (well_founded.apply Ha) a))
 end
 
 section
diff --git a/library/init/wf.lean b/library/init/wf.lean
index 6f2dfd6b4b..7ec120af0d 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -9,7 +9,7 @@ import init.relation init.nat init.prod
 universe variables u v
 
 inductive acc {A : Type u} (R : A → A → Prop) : A → Prop
-| intro : ∀x, (∀ y, R y x → acc y) → acc x
+| intro : ∀ x, (∀ y, R y x → acc y) → acc x
 
 namespace acc
   variables {A : Type u} {R : A → A → Prop}
@@ -35,8 +35,8 @@ inductive well_founded {A : Type u} (R : A → A → Prop) : Prop
 | intro : (∀ a, acc R a) → well_founded
 
 namespace well_founded
-  definition apply {A : Type u} {R : A → A → Prop} (wf : well_founded R) : ∀a, acc R a :=
-  take a, well_founded.rec_on wf (λp, p) a
+  definition apply {A : Type u} {R : A → A → Prop} (wf : well_founded R) : ∀ a, acc R a :=
+  take a, well_founded.rec_on wf (λ p, p) a
 
   section
   parameters {A : Type u} {R : A → A → Prop}
@@ -44,14 +44,14 @@ namespace well_founded
 
   hypothesis Hwf : well_founded R
 
-  theorem recursion {C : A → Type v} (a : A) (H : Πx, (Πy, y ≺ x → C y) → C x) : C a :=
+  theorem recursion {C : A → Type v} (a : A) (H : Π x, (Π y, y ≺ x → C y) → C x) : C a :=
   acc.rec_on (apply Hwf a) (λ x₁ ac₁ iH, H x₁ iH)
 
-  theorem induction {C : A → Prop} (a : A) (H : ∀x, (∀y, y ≺ x → C y) → C x) : C a :=
+  theorem induction {C : A → Prop} (a : A) (H : ∀ x, (∀ y, y ≺ x → C y) → C x) : C a :=
   recursion a H
 
   variable {C : A → Type v}
-  variable F : Πx, (Πy, y ≺ x → C y) → C x
+  variable F : Π x, (Π y, y ≺ x → C y) → C x
 
   definition fix_F (x : A) (a : acc R x) : C x :=
   acc.rec_on a (λ x₁ ac₁ iH, F x₁ iH)
@@ -64,12 +64,12 @@ namespace well_founded
   variables {A : Type u} {C : A → Type v} {R : A → A → Prop}
 
   -- Well-founded fixpoint
-  definition fix (Hwf : well_founded R) (F : Πx, (Πy, R y x → C y) → C x) (x : A) : C x :=
+  definition fix (Hwf : well_founded R) (F : Π x, (Π y, R y x → C y) → C x) (x : A) : C x :=
   fix_F F x (apply Hwf x)
 
   -- Well-founded fixpoint satisfies fixpoint equation
-  theorem fix_eq (Hwf : well_founded R) (F : Πx, (Πy, R y x → C y) → C x) (x : A) :
-    fix Hwf F x = F x (λy h, fix Hwf F y) :=
+  theorem fix_eq (Hwf : well_founded R) (F : Π x, (Π y, R y x → C y) → C x) (x : A) :
+    fix Hwf F x = F x (λ y h, fix Hwf F y) :=
   fix_F_eq F x (apply Hwf x)
 end well_founded
 
@@ -168,10 +168,10 @@ end tc
 -- less-than is well-founded
 definition nat.lt_wf : well_founded nat.lt :=
 well_founded.intro (nat.rec
-  (acc.intro 0 (λn H, absurd H (nat.not_lt_zero n)))
-  (λn IH, acc.intro (nat.succ n) (λm H,
+  (acc.intro 0 (λ n H, absurd H (nat.not_lt_zero n)))
+  (λ n IH, acc.intro (nat.succ n) (λ m H,
      or.elim (nat.eq_or_lt_of_le (nat.le_of_succ_le_succ H))
-        (λe, eq.substr e IH) (acc.inv IH))))
+        (λ e, eq.substr e IH) (acc.inv IH))))
 
 definition measure {A : Type u} : (A → ℕ) → A → A → Prop :=
 inv_image lt
@@ -189,12 +189,12 @@ namespace prod
 
   -- Lexicographical order based on Ra and Rb
   inductive lex : A × B → A × B → Prop
-  | left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
-  | right : ∀a {b₁ b₂},     Rb b₁ b₂ → lex (a, b₁)  (a, b₂)
+  | left  : ∀ {a₁ b₁} a₂ b₂, Ra a₁ a₂ → lex (a₁, b₁) (a₂, b₂)
+  | right : ∀ a {b₁ b₂},     Rb b₁ b₂ → lex (a, b₁)  (a, b₂)
 
   -- Relational product based on Ra and Rb
   inductive rprod : A × B → A × B → Prop
-  | intro : ∀{a₁ b₁ a₂ b₂}, Ra a₁ a₂ → Rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂)
+  | intro : ∀ {a₁ b₁ a₂ b₂}, Ra a₁ a₂ → Rb b₁ b₂ → rprod (a₁, b₁) (a₂, b₂)
   end
 
   section
@@ -202,21 +202,21 @@ namespace prod
   parameters {Ra  : A → A → Prop} {Rb  : B → B → Prop}
   local infix `≺`:50 := lex Ra Rb
 
-  definition lex_accessible {a} (aca : acc Ra a) (acb : ∀b, acc Rb b): ∀b, acc (lex Ra Rb) (a, b) :=
+  definition lex_accessible {a} (aca : acc Ra a) (acb : ∀ b, acc Rb b): ∀ b, acc (lex Ra Rb) (a, b) :=
   acc.rec_on aca
-    (λxa aca (iHa : ∀y, Ra y xa → ∀b, acc (lex Ra Rb) (y, b)),
-      λb, acc.rec_on (acb b)
-        (λxb acb
-          (iHb : ∀y, Rb y xb → acc (lex Ra Rb) (xa, y)),
-          acc.intro (xa, xb) (λp (lt : p ≺ (xa, xb)),
+    (λ xa aca (iHa : ∀ y, Ra y xa → ∀ b, acc (lex Ra Rb) (y, b)),
+      λ b, acc.rec_on (acb b)
+        (λ xb acb
+          (iHb : ∀ y, Rb y xb → acc (lex Ra Rb) (xa, y)),
+          acc.intro (xa, xb) (λ p (lt : p ≺ (xa, xb)),
             have aux : xa = xa → xb = xb → acc (lex Ra Rb) p, from
-              @prod.lex.rec_on A B Ra Rb (λp₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁)
+              @prod.lex.rec_on A B Ra Rb (λ p₁ p₂, pr₁ p₂ = xa → pr₂ p₂ = xb → acc (lex Ra Rb) p₁)
                                p (xa, xb) lt
-                (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb),
+                (λ a₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ = xb),
                   show acc (lex Ra Rb) (a₁, b₁), from
                   have Ra₁  : Ra a₁ xa, from eq.rec_on eq₂ H,
                   iHa a₁ Ra₁ b₁)
-                (λa b₁ b₂ (H : Rb b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ = xb),
+                (λ a b₁ b₂ (H : Rb b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ = xb),
                   show acc (lex Ra Rb) (a, b₁), from
                   have Rb₁  : Rb b₁ xb, from eq.rec_on eq₃ H,
                   have eq₂' : xa = a, from eq.rec_on eq₂ rfl,
@@ -225,11 +225,11 @@ namespace prod
 
   -- The lexicographical order of well founded relations is well-founded
   definition lex_wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (lex Ra Rb) :=
-  well_founded.intro (λp, destruct p (λa b, lex_accessible (apply Ha a) (well_founded.apply Hb) b))
+  well_founded.intro (λ p, destruct p (λ a b, lex_accessible (apply Ha a) (well_founded.apply Hb) b))
 
   -- Relational product is a subrelation of the lex
   definition rprod_sub_lex : ∀ a b, rprod Ra Rb a b → lex Ra Rb a b :=
-  λa b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁)
+  λ a b H, prod.rprod.rec_on H (λ a₁ b₁ a₂ b₂ H₁ H₂, lex.left Rb a₂ b₂ H₁)
 
   -- The relational product of well founded relations is well-founded
   definition rprod_wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) :=
diff --git a/library/init/wf_k.lean b/library/init/wf_k.lean
index 90807ab87d..482e41fba2 100644
--- a/library/init/wf_k.lean
+++ b/library/init/wf_k.lean
@@ -12,6 +12,6 @@ namespace well_founded
   well_founded.intro
   (nat.rec_on k
      (λ n : A, well_founded.apply Hwf n)
-     (λ (k' : nat) (f : Πa, acc R a), (λ n : A, acc.intro n (λ y H, f y))))
+     (λ (k' : nat) (f : Π a, acc R a), (λ n : A, acc.intro n (λ y H, f y))))
 
 end well_founded