diff --git a/library/data/bool.lean b/library/data/bool.lean
index c1110a47d6..bd8e48ac0f 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -4,143 +4,142 @@
 
 import logic.core.connectives logic.classes.decidable logic.classes.inhabited
 
-open eq_ops decidable
+open eq_ops eq decidable
 
 inductive bool : Type :=
-ff : bool,
-tt : bool
-
+  ff : bool,
+  tt : bool
 namespace bool
+  definition rec_on [protected] {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b :=
+  rec H₁ H₂ b
 
-theorem cases_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
-rec H0 H1 b
+  theorem cases_on [protected] {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b :=
+  rec H₁ H₂ b
 
-theorem bool_inhabited [instance] : inhabited bool :=
-inhabited.mk ff
+  definition cond {A : Type} (b : bool) (t e : A) :=
+  rec_on b e t
 
-definition cond {A : Type} (b : bool) (t e : A) :=
-rec e t b
+  theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
+  cases_on b (or.inl rfl) (or.inr rfl)
 
-theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
-cases_on b (or.inl (eq.refl ff)) (or.inr (eq.refl tt))
+  theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
+  rfl
 
-theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
-rfl
+  theorem cond_tt {A : Type} (t e : A) : cond tt t e = t :=
+  rfl
 
-theorem cond_tt {A : Type} (t e : A) : cond tt t e = t :=
-rfl
+  theorem ff_ne_tt : ¬ ff = tt :=
+  assume H : ff = tt, absurd
+    (calc true  = cond tt true false : (cond_tt _ _)⁻¹
+            ... = cond ff true false : {H⁻¹}
+            ... = false              : cond_ff _ _)
+    true_ne_false
 
-theorem ff_ne_tt : ¬ ff = tt :=
-assume H : ff = tt, absurd
-  (calc true  = cond tt true false : (cond_tt _ _)⁻¹
-          ... = cond ff true false : {H⁻¹}
-          ... = false              : cond_ff _ _)
-  true_ne_false
+  definition bor (a b : bool) :=
+  rec_on a (rec_on b ff tt) tt
 
-theorem decidable_eq [instance] (a b : bool) : decidable (a = b) :=
-rec
-  (rec (inl (eq.refl ff)) (inr ff_ne_tt) b)
-  (rec (inr (ne.symm ff_ne_tt)) (inl (eq.refl tt)) b)
-  a
+  theorem bor_tt_left (a : bool) : bor tt a = tt :=
+  rfl
 
-definition bor (a b : bool) :=
-rec (rec ff tt b) tt a
+  infixl `||` := bor
 
-theorem bor_tt_left (a : bool) : bor tt a = tt :=
-rfl
+  theorem bor_tt_right (a : bool) : a || tt = tt :=
+  cases_on a rfl rfl
 
-infixl `||` := bor
+  theorem bor_ff_left (a : bool) : ff || a = a :=
+  cases_on a rfl rfl
 
-theorem bor_tt_right (a : bool) : a || tt = tt :=
-cases_on a (eq.refl (ff || tt)) (eq.refl (tt || tt))
+  theorem bor_ff_right (a : bool) : a || ff = a :=
+  cases_on a rfl rfl
 
-theorem bor_ff_left (a : bool) : ff || a = a :=
-cases_on a (eq.refl (ff || ff)) (eq.refl (ff || tt))
+  theorem bor_id (a : bool) : a || a = a :=
+  cases_on a rfl rfl
 
-theorem bor_ff_right (a : bool) : a || ff = a :=
-cases_on a (eq.refl (ff || ff)) (eq.refl (tt || ff))
+  theorem bor_comm (a b : bool) : a || b = b || a :=
+  cases_on a
+    (cases_on b rfl rfl)
+    (cases_on b rfl rfl)
 
-theorem bor_id (a : bool) : a || a = a :=
-cases_on a (eq.refl (ff || ff)) (eq.refl (tt || tt))
+  theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
+  cases_on a
+    (calc (ff || b) || c = b || c         : {bor_ff_left b}
+                   ...   = ff || (b || c) : bor_ff_left (b || c)⁻¹)
+    (calc (tt || b) || c = tt || c        : {bor_tt_left b}
+                   ...   = tt             : bor_tt_left c
+                   ...   = tt || (b || c) : bor_tt_left (b || c)⁻¹)
 
-theorem bor_comm (a b : bool) : a || b = b || a :=
-cases_on a
-  (cases_on b (eq.refl (ff || ff)) (eq.refl (ff || tt)))
-  (cases_on b (eq.refl (tt || ff)) (eq.refl (tt || tt)))
+  theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
+  rec_on a
+    (assume H : ff || b = tt,
+      have Hb : b = tt, from (bor_ff_left b) ▸ H,
+      or.inr Hb)
+    (assume H, or.inl rfl)
 
-theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
-cases_on a
-  (calc (ff || b) || c = b || c         : {bor_ff_left b}
-                 ...   = ff || (b || c) : bor_ff_left (b || c)⁻¹)
-  (calc (tt || b) || c = tt || c        : {bor_tt_left b}
-                 ...   = tt             : bor_tt_left c
-                 ...   = tt || (b || c) : bor_tt_left (b || c)⁻¹)
+  definition band (a b : bool) :=
+  rec_on a ff (rec_on b ff tt)
 
-theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
-rec
-  (assume H : ff || b = tt,
-    have Hb : b = tt, from (bor_ff_left b) ▸ H,
-    or.inr Hb)
-  (assume H, or.inl (eq.refl tt))
-  a
+  infixl `&&` := band
 
-definition band (a b : bool) :=
-rec ff (rec ff tt b) a
+  theorem band_ff_left (a : bool) : ff && a = ff :=
+  rfl
 
-infixl `&&` := band
+  theorem band_tt_left (a : bool) : tt && a = a :=
+  cases_on a rfl rfl
 
-theorem band_ff_left (a : bool) : ff && a = ff :=
-rfl
+  theorem band_ff_right (a : bool) : a && ff = ff :=
+  cases_on a rfl rfl
 
-theorem band_tt_left (a : bool) : tt && a = a :=
-cases_on a (eq.refl (tt && ff)) (eq.refl (tt && tt))
+  theorem band_tt_right (a : bool) : a && tt = a :=
+  cases_on a rfl rfl
 
-theorem band_ff_right (a : bool) : a && ff = ff :=
-cases_on a (eq.refl (ff && ff)) (eq.refl (tt && ff))
+  theorem band_id (a : bool) : a && a = a :=
+  cases_on a rfl rfl
 
-theorem band_tt_right (a : bool) : a && tt = a :=
-cases_on a (eq.refl (ff && tt)) (eq.refl (tt && tt))
+  theorem band_comm (a b : bool) : a && b = b && a :=
+  cases_on a
+    (cases_on b rfl rfl)
+    (cases_on b rfl rfl)
 
-theorem band_id (a : bool) : a && a = a :=
-cases_on a (eq.refl (ff && ff)) (eq.refl (tt && tt))
+  theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
+  cases_on a
+    (calc (ff && b) && c = ff && c        : {band_ff_left b}
+                    ...  = ff             : band_ff_left c
+                    ...  = ff && (b && c) : band_ff_left (b && c)⁻¹)
+    (calc (tt && b) && c = b && c         : {band_tt_left b}
+                    ...  = tt && (b && c) : band_tt_left (b && c)⁻¹)
 
-theorem band_comm (a b : bool) : a && b = b && a :=
-cases_on a
-  (cases_on b (eq.refl (ff && ff)) (eq.refl (ff && tt)))
-  (cases_on b (eq.refl (tt && ff)) (eq.refl (tt && tt)))
+  theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
+  or.elim (dichotomy a)
+    (assume H0 : a = ff,
+      absurd
+        (calc ff = ff && b : (band_ff_left _)⁻¹
+             ... = a && b  : {H0⁻¹}
+             ... = tt      : H)
+        ff_ne_tt)
+    (assume H1 : a = tt, H1)
 
-theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
-cases_on a
-  (calc (ff && b) && c = ff && c        : {band_ff_left b}
-                  ...  = ff             : band_ff_left c
-                  ...  = ff && (b && c) : band_ff_left (b && c)⁻¹)
-  (calc (tt && b) && c = b && c         : {band_tt_left b}
-                  ...  = tt && (b && c) : band_tt_left (b && c)⁻¹)
+  theorem band_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
+  band_eq_tt_elim_left (band_comm b a ⬝ H)
 
-theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
-or.elim (dichotomy a)
-  (assume H0 : a = ff,
-    absurd
-      (calc ff = ff && b : (band_ff_left _)⁻¹
-           ... = a && b  : {H0⁻¹}
-           ... = tt      : H)
-      ff_ne_tt)
-  (assume H1 : a = tt, H1)
+  definition bnot (a : bool) :=
+  rec_on a tt ff
 
-theorem band_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
-band_eq_tt_elim_left (eq.trans (band_comm b a) H)
+  notation `!` x:max := bnot x
 
-definition bnot (a : bool) := rec tt ff a
+  theorem bnot_bnot (a : bool) : !!a = a :=
+  cases_on a rfl rfl
 
-notation `!` x:max := bnot x
+  theorem bnot_false : !ff = tt :=
+  rfl
 
-theorem bnot_bnot (a : bool) : !!a = a :=
-cases_on a (eq.refl (!!ff)) (eq.refl (!!tt))
+  theorem bnot_true  : !tt = ff :=
+  rfl
 
-theorem bnot_false : !ff = tt :=
-rfl
-
-theorem bnot_true  : !tt = ff :=
-rfl
+  theorem is_inhabited [protected] [instance] : inhabited bool :=
+  inhabited.mk ff
 
+  theorem has_decidable_eq [protected] [instance] (a b : bool) : decidable (a = b) :=
+  rec_on a
+    (rec_on b (inl rfl) (inr ff_ne_tt))
+    (rec_on b (inr (ne.symm ff_ne_tt)) (inl rfl))
 end bool
diff --git a/library/data/empty.lean b/library/data/empty.lean
index 74a3a5d5b5..6b19b4e009 100644
--- a/library/data/empty.lean
+++ b/library/data/empty.lean
@@ -9,4 +9,7 @@
 
 inductive empty : Type
 
-theorem empty_elim (A : Type) (H : empty) : A := empty.rec (λe, A) H
+namespace empty
+  theorem elim [protected] (A : Type) (H : empty) : A :=
+  rec (λe, A) H
+end empty
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index c2fbc51909..7e10f7a1ef 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -118,7 +118,7 @@ have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from
         ... = pr1 a - pr2 a                             : {flip_pr1 a}
         ... = pr1 (proj a)                              : (proj_ge_pr1 H)⁻¹
         ... = pr2 (flip (proj a))                       : (flip_pr2 (proj a))⁻¹,
-  prod_eq H3 H4,
+  prod.equal H3 H4,
 or.elim le_total
   (assume H : pr2 a ≤ pr1 a, special a H)
   (assume H : pr1 a ≤ pr2 a,
@@ -162,7 +162,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from
     calc
       pr2 (proj a) = 0 : proj_ge_pr2 H2
         ... = pr2 (proj b) : {(proj_ge_pr2 H4)⁻¹},
-  prod_eq H5 H6,
+  prod.equal H5 H6,
 or.elim le_total
   (assume H2 : pr2 a ≤ pr1 a, special a b H2 H)
   (assume H2 : pr1 a ≤ pr2 a,
diff --git a/library/data/num.lean b/library/data/num.lean
index c5058ce154..51b69bde13 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -13,12 +13,14 @@ one  : pos_num,
 bit1 : pos_num → pos_num,
 bit0 : pos_num → pos_num
 
+namespace pos_num
+  theorem is_inhabited [instance] : inhabited pos_num :=
+  inhabited.mk one
+end pos_num
+
 inductive num : Type :=
 zero  : num,
 pos   : pos_num → num
 
-theorem inhabited_pos_num [instance] : inhabited pos_num :=
-inhabited.mk pos_num.one
-
 theorem num_inhabited [instance] : inhabited num :=
 inhabited.mk num.zero
diff --git a/library/data/option.lean b/library/data/option.lean
index d654eb9210..e726746345 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -6,47 +6,45 @@ import logic.core.eq logic.classes.inhabited logic.classes.decidable
 open eq_ops decidable
 
 inductive option (A : Type) : Type :=
-none {} : option A,
-some    : A → option A
+  none {} : option A,
+  some    : A → option A
 
 namespace option
+  theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A)
+    (H1 : p none) (H2 : ∀a, p (some a)) : p o :=
+  rec H1 H2 o
 
-theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A)
-  (H1 : p none) (H2 : ∀a, p (some a)) : p o :=
-rec H1 H2 o
+  definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A)
+    (H1 : C none) (H2 : ∀a, C (some a)) : C o :=
+  rec H1 H2 o
 
-definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A)
-  (H1 : C none) (H2 : ∀a, C (some a)) : C o :=
-rec H1 H2 o
+  definition is_none {A : Type} (o : option A) : Prop :=
+  rec true (λ a, false) o
 
-definition is_none {A : Type} (o : option A) : Prop :=
-rec true (λ a, false) o
+  theorem is_none_none {A : Type} : is_none (@none A) :=
+  trivial
 
-theorem is_none_none {A : Type} : is_none (@none A) :=
-trivial
+  theorem not_is_none_some {A : Type} (a : A) : ¬ is_none (some a) :=
+  not_false_trivial
 
-theorem not_is_none_some {A : Type} (a : A) : ¬ is_none (some a) :=
-not_false_trivial
+  theorem none_ne_some {A : Type} (a : A) : none ≠ some a :=
+  assume H : none = some a, absurd
+    (H ▸ is_none_none)
+    (not_is_none_some a)
 
-theorem none_ne_some {A : Type} (a : A) : none ≠ some a :=
-assume H : none = some a, absurd
-  (H ▸ is_none_none)
-  (not_is_none_some a)
+  theorem equal [protected] {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
+  congr_arg (option.rec a₁ (λ a, a)) H
 
-theorem some_inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
-congr_arg (option.rec a₁ (λ a, a)) H
-
-theorem option_inhabited [instance] (A : Type) : inhabited (option A) :=
-inhabited.mk none
-
-theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)}
-    (o₁ o₂ : option A) : decidable (o₁ = o₂) :=
-rec_on o₁
-  (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))
-  (take a₁ : A, rec_on o₂
-    (inr (ne.symm (none_ne_some a₁)))
-    (take a₂ : A, decidable.rec_on (H a₁ a₂)
-      (assume Heq : a₁ = a₂, inl (Heq ▸ rfl))
-      (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some_inj Hn) Hne))))
+  theorem is_inhabited [protected] [instance] (A : Type) : inhabited (option A) :=
+  inhabited.mk none
 
+  theorem has_decidable_eq [protected] [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)}
+          (o₁ o₂ : option A) : decidable (o₁ = o₂) :=
+  rec_on o₁
+    (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))
+    (take a₁ : A, rec_on o₂
+      (inr (ne.symm (none_ne_some a₁)))
+      (take a₂ : A, decidable.rec_on (H a₁ a₂)
+        (assume Heq : a₁ = a₂, inl (Heq ▸ rfl))
+        (assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (equal Hn) Hne))))
 end option
diff --git a/library/data/prod.lean b/library/data/prod.lean
index fa74c51f00..0f96ac333d 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -1,30 +1,25 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
+import logic.classes.inhabited logic.core.eq logic.classes.decidable
 
 -- data.prod
 -- =========
 
--- The cartesian product.
-
-import logic.classes.inhabited logic.core.eq logic.classes.decidable
-
 open inhabited decidable
 
+-- The cartesian product.
 inductive prod (A B : Type) : Type :=
-mk : A → B → prod A B
+  mk : A → B → prod A B
 
 abbreviation pair := @prod.mk
-
 infixr `×` := prod
 
 -- notation for n-ary tuples
 notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
 
 namespace prod
-
 section
-
   parameters {A B : Type}
 
   abbreviation pr1 (p : prod A B) := rec (λ x y, x) p
@@ -47,20 +42,18 @@ section
   theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) :=
   H1 ▸ H2 ▸ rfl
 
-  theorem prod_eq {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
+  theorem equal [protected] {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
   destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
 
-  theorem prod_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
+  theorem is_inhabited [protected] [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
   inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b)))
 
-  theorem prod_eq_decidable [instance] (u v : A × B) (H1 : decidable (pr1 u = pr1 v))
+  theorem has_decidable_eq [protected] [instance] (u v : A × B) (H1 : decidable (pr1 u = pr1 v))
       (H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) :=
     have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
       iff.intro
         (assume H, H ▸ and.intro rfl rfl)
-        (assume H, and.elim H (assume H4 H5, prod_eq H4 H5)),
+        (assume H, and.elim H (assume H4 H5, equal H4 H5)),
     decidable_iff_equiv _ (iff.symm H3)
-
 end
-
 end prod
diff --git a/library/data/quotient/aux.lean b/library/data/quotient/aux.lean
index e2c32022b3..9abb1697bb 100644
--- a/library/data/quotient/aux.lean
+++ b/library/data/quotient/aux.lean
@@ -150,7 +150,7 @@ have Hy : pr2 (map_pair2 f v (pair e e)) = pr2 v, from
     pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by simp
       ... = f (pr2 v) e : by simp
       ... = pr2 v : Hid (pr2 v)),
-prod_eq Hx Hy
+prod.equal Hx Hy
 
 theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a : A, f e a = a)
   (v : A × A) : map_pair2 f (pair e e) v = v :=
@@ -164,7 +164,7 @@ have Hy : pr2 (map_pair2 f (pair e e) v) = pr2 v, from
     pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by simp
       ... = f e (pr2 v) : by simp
       ... = pr2 v : Hid (pr2 v),
-prod_eq Hx Hy
+prod.equal Hx Hy
 
 opaque_hint (hiding flip map_pair map_pair2)
 
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 0ff1008c5a..28559bf873 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -294,7 +294,7 @@ intro
           ... = f (f a) : {Ha⁻¹}
           ... = f a : representative_map_idempotent H1 H2 a
           ... = elt_of u : Ha,
-    show abs (elt_of u) = u, from subtype_eq H)
+    show abs (elt_of u) = u, from subtype.equal H)
   (take u : image f,
     show R (elt_of u) (elt_of u), from
       obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u,
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 3d7b7e0eaa..19726b653a 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -42,13 +42,12 @@ section
               ... = dpair a1 b2' : {H2'}) H1)
   b2 H1 H2
 
-  theorem sigma_eq {p1 p2 : Σx : A, B x} :
+  theorem equal [protected] {p1 p2 : Σx : A, B x} :
     ∀(H1 : dpr1 p1 = dpr1 p2) (H2 : eq.rec_on H1 (dpr2 p1) = (dpr2 p2)), p1 = p2 :=
   sigma_destruct p1 (take a1 b1, sigma_destruct p2 (take a2 b2 H1 H2, dpair_eq H1 H2))
 
-  theorem sigma_inhabited [instance] (H1 : inhabited A) (H2 : inhabited (B (default A))) :
+  theorem is_inhabited [protected] [instance] (H1 : inhabited A) (H2 : inhabited (B (default A))) :
     inhabited (sigma B) :=
    inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (dpair (default A) b)))
-
 end
 end sigma
diff --git a/library/data/string.lean b/library/data/string.lean
index 64261555df..6f91b363e4 100644
--- a/library/data/string.lean
+++ b/library/data/string.lean
@@ -7,14 +7,18 @@ import data.bool
 open bool inhabited
 
 inductive char : Type :=
-mk : bool → bool → bool → bool → bool → bool → bool → bool → char
+  mk : bool → bool → bool → bool → bool → bool → bool → bool → char
+
+namespace char
+  theorem is_inhabited [protected] [instance] : inhabited char :=
+  inhabited.mk (mk ff ff ff ff ff ff ff ff)
+end char
 
 inductive string : Type :=
-empty : string,
-str   : char → string → string
+  empty : string,
+  str   : char → string → string
 
-theorem char_inhabited [instance] : inhabited char :=
-inhabited.mk (char.mk ff ff ff ff ff ff ff ff)
-
-theorem string_inhabited [instance] : inhabited string :=
-inhabited.mk string.empty
+namespace string
+  theorem is_inhabited [protected] [instance] : inhabited string :=
+  inhabited.mk empty
+end string
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index 0eebdd1c3d..6dcd20f39e 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -7,12 +7,11 @@ import logic.classes.inhabited logic.core.eq logic.classes.decidable
 open decidable
 
 inductive subtype {A : Type} (P : A → Prop) : Type :=
-tag : Πx : A, P x → subtype P
+  tag : Πx : A, P x → subtype P
 
 notation `{` binders `,` r:(scoped P, subtype P) `}` := r
 
 namespace subtype
-
 section
   parameter {A : Type}
   parameter {P : A → Prop}
@@ -36,18 +35,16 @@ section
   theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
   eq.subst H3 (take H2, tag_irrelevant H1 H2) H2
 
-  theorem subtype_eq {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
+  theorem equal [protected] {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
   destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H))
 
-  theorem subtype_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
+  theorem is_inhabited [protected] [instance] {a : A} (H : P a) : inhabited {x, P x} :=
   inhabited.mk (tag a H)
 
-  theorem eq_decidable [protected] [instance] (a1 a2 : {x, P x})
+  theorem has_decidable_eq [protected] [instance] (a1 a2 : {x, P x})
     (H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) :=
   have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
-    iff.intro (assume H, eq.subst H rfl) (assume H, subtype_eq H),
+    iff.intro (assume H, eq.subst H rfl) (assume H, equal H),
   decidable_iff_equiv _ (iff.symm H1)
-
 end
-
 end subtype
diff --git a/library/data/sum.lean b/library/data/sum.lean
index fc645ba13b..cbba4744a6 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -1,83 +1,76 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
-
+import logic.core.prop logic.classes.inhabited logic.classes.decidable
+open inhabited decidable eq_ops
 -- data.sum
 -- ========
-
 -- The sum type, aka disjoint union.
 
-import logic.core.prop logic.classes.inhabited logic.classes.decidable
-
-open inhabited decidable eq_ops
-
--- TODO: take this outside the namespace when the inductive package handles it better
 inductive sum (A B : Type) : Type :=
-inl : A → sum A B,
-inr : B → sum A B
+  inl : A → sum A B,
+  inr : B → sum A B
 
 namespace sum
-infixr `⊎` := sum
+  infixr `⊎` := sum
+  namespace extra_notation
+    infixr `+`:25 := sum    -- conflicts with notation for addition
+  end extra_notation
 
-namespace sum_plus_notation
-infixr `+`:25 := sum    -- conflicts with notation for addition
-end sum_plus_notation
+  abbreviation rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
+    (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
+  rec H1 H2 s
 
-abbreviation rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
-  (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
-rec H1 H2 s
+  abbreviation cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
+    (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
+  rec H1 H2 s
 
-abbreviation cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
-  (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
-rec H1 H2 s
+  -- Here is the trick for the theorems that follow:
+  -- Fixing a1, "f s" is a recursive description of "inl B a1 = s".
+  -- When s is (inl B a1), it reduces to a1 = a1.
+  -- When s is (inl B a2), it reduces to a1 = a2.
+  -- When s is (inr A b), it reduces to false.
 
--- Here is the trick for the theorems that follow:
--- Fixing a1, "f s" is a recursive description of "inl B a1 = s".
--- When s is (inl B a1), it reduces to a1 = a1.
--- When s is (inl B a2), it reduces to a1 = a2.
--- When s is (inr A b), it reduces to false.
+  theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
+  let f := λs, rec_on s (λa, a1 = a) (λb, false) in
+  have H1 : f (inl B a1), from rfl,
+  have H2 : f (inl B a2), from H ▸ H1,
+  H2
 
-theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
-let f := λs, rec_on s (λa, a1 = a) (λb, false) in
-have H1 : f (inl B a1), from rfl,
-have H2 : f (inl B a2), from H ▸ H1,
-H2
+  theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
+  let f := λs, rec_on s (λa', a = a') (λb, false) in
+  have H1 : f (inl B a), from rfl,
+  have H2 : f (inr A b), from H ▸ H1,
+  H2
 
-theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
-let f := λs, rec_on s (λa', a = a') (λb, false) in
-have H1 : f (inl B a), from rfl,
-have H2 : f (inr A b), from H ▸ H1,
-H2
+  theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 :=
+  let f := λs, rec_on s (λa, false) (λb, b1 = b) in
+  have H1 : f (inr A b1), from rfl,
+  have H2 : f (inr A b2), from H ▸ H1,
+  H2
 
-theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 :=
-let f := λs, rec_on s (λa, false) (λb, b1 = b) in
-have H1 : f (inr A b1), from rfl,
-have H2 : f (inr A b2), from H ▸ H1,
-H2
+  theorem is_inhabited_left [protected] [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) :=
+  inhabited.mk (inl B (default A))
 
-theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) :=
-inhabited.mk (inl B (default A))
-
-theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
-inhabited.mk (inr A (default B))
-
-theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A ⊎ B)
-  (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2))
-  (H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
-rec_on s1
-  (take a1, show decidable (inl B a1 = s2), from
-    rec_on s2
-      (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
-      (take b2,
-        have H3 : (inl B a1 = inr A b2) ↔ false,
-          from iff.intro inl_neq_inr (assume H4, false_elim H4),
-        show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3)))
-  (take b1, show decidable (inr A b1 = s2), from
-    rec_on s2
-      (take a2,
-        have H3 : (inr A b1 = inl B a2) ↔ false,
-          from iff.intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4),
-        show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3))
-      (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
+  theorem is_inhabited_right [protected] [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
+  inhabited.mk (inr A (default B))
 
+  theorem has_eq_decidable [protected] [instance] {A B : Type} (s1 s2 : A ⊎ B)
+    (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2))
+    (H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
+  rec_on s1
+    (take a1, show decidable (inl B a1 = s2), from
+      rec_on s2
+        (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
+        (take b2,
+          have H3 : (inl B a1 = inr A b2) ↔ false,
+            from iff.intro inl_neq_inr (assume H4, false_elim H4),
+          show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3)))
+    (take b1, show decidable (inr A b1 = s2), from
+      rec_on s2
+        (take a2,
+          have H3 : (inr A b1 = inl B a2) ↔ false,
+            from iff.intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4),
+          show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3))
+        (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 end sum
diff --git a/library/data/unit.lean b/library/data/unit.lean
index 412db7f0dd..d629c79de0 100644
--- a/library/data/unit.lean
+++ b/library/data/unit.lean
@@ -2,26 +2,22 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 import logic.classes.decidable logic.classes.inhabited
-
 open decidable
 
 inductive unit : Type :=
-star : unit
-
+  star : unit
 namespace unit
+  notation `⋆`:max := star
 
-notation `⋆`:max := star
+  theorem equal [protected] (a b : unit) : a = b :=
+  rec (rec rfl b) a
 
-theorem at_most_one (a b : unit) : a = b :=
-rec (rec rfl b) a
+  theorem eq_star (a : unit) : a = star :=
+  equal a star
 
-theorem eq_star (a : unit) : a = star :=
-at_most_one a star
-
-theorem unit_inhabited [instance] : inhabited unit :=
-inhabited.mk ⋆
-
-theorem decidable_eq [instance] (a b : unit) : decidable (a = b) :=
-inl (at_most_one a b)
+  theorem is_inhabited [protected] [instance] : inhabited unit :=
+  inhabited.mk ⋆
 
+  theorem has_decidable_eq [protected] [instance] (a b : unit) : decidable (a = b) :=
+  inl (equal a b)
 end unit
diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out
index 94d8939ec8..d6862512f6 100644
--- a/tests/lean/empty.lean.expected.out
+++ b/tests/lean/empty.lean.expected.out
@@ -1,7 +1,7 @@
 empty.lean:6:25: error: type error in placeholder assigned to
-  char_inhabited
+  num_inhabited
 placeholder has type
-  inhabited char
+  inhabited num
 but is expected to have type
   inhabited ?M_1
 the assignment was attempted when trying to solve