diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean
index 93534f2c18..23b89133bf 100644
--- a/hott/algebra/category/constructions/functor.hlean
+++ b/hott/algebra/category/constructions/functor.hlean
@@ -12,7 +12,7 @@ open eq category is_trunc nat_trans iso is_equiv category.hom
 
 namespace functor
 
-  definition precategory_functor [instance] [reducible] [constructor] (D C : Precategory)
+  definition precategory_functor [instance] [constructor] (D C : Precategory)
     : precategory (functor C D) :=
   precategory.mk (λa b, nat_trans a b)
                  (λ a b c g f, nat_trans.compose g f)
diff --git a/hott/algebra/category/constructions/product.hlean b/hott/algebra/category/constructions/product.hlean
index cef0b99111..777488013d 100644
--- a/hott/algebra/category/constructions/product.hlean
+++ b/hott/algebra/category/constructions/product.hlean
@@ -11,7 +11,7 @@ import ..category ..nat_trans hit.trunc
 open eq prod is_trunc functor sigma trunc iso prod.ops nat_trans
 
 namespace category
-  definition precategory_prod [constructor] [reducible] [instance] (obC obD : Type)
+  definition precategory_prod [constructor] [instance] (obC obD : Type)
     [C : precategory obC] [D : precategory obD] : precategory (obC × obD) :=
   precategory.mk' (λ a b, hom a.1 b.1 × hom a.2 b.2)
                   (λ a b c g f, (g.1 ∘ f.1, g.2 ∘ f.2))
diff --git a/hott/algebra/category/constructions/set.hlean b/hott/algebra/category/constructions/set.hlean
index 0e5a2fadca..c5372003c1 100644
--- a/hott/algebra/category/constructions/set.hlean
+++ b/hott/algebra/category/constructions/set.hlean
@@ -82,7 +82,7 @@ namespace category
     end
   end set
 
-  definition category_Set [instance] [constructor] [reducible] : category Set :=
+  definition category_Set [instance] [constructor] : category Set :=
   category.mk precategory_Set set.is_univalent_Set
 
   definition Category_Set [reducible] [constructor] : Category :=
diff --git a/hott/algebra/category/functor/attributes.hlean b/hott/algebra/category/functor/attributes.hlean
index 81abebc987..2e26e25a5a 100644
--- a/hott/algebra/category/functor/attributes.hlean
+++ b/hott/algebra/category/functor/attributes.hlean
@@ -23,7 +23,7 @@ namespace category
   definition is_weak_equivalence [class] (F : C ⇒ D) :=
   fully_faithful F × essentially_surjective F
 
-  definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D)
+  definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D)
     [H : fully_faithful F] (c c' : C) : is_equiv (@(to_fun_hom F) c c') :=
   !H
 
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index 7c52c9f522..59d975a57a 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -39,11 +39,11 @@ namespace iso
   variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
   include C
 
-  definition split_mono_of_is_iso [constructor] [instance] [priority 300] [reducible]
+  definition split_mono_of_is_iso [constructor] [instance] [priority 300]
     (f : a ⟶ b) [H : is_iso f] : split_mono f :=
   split_mono.mk !left_inverse
 
-  definition split_epi_of_is_iso [constructor] [instance] [priority 300] [reducible]
+  definition split_epi_of_is_iso [constructor] [instance] [priority 300]
     (f : a ⟶ b) [H : is_iso f] : split_epi f :=
   split_epi.mk !right_inverse
 
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index 63001121f8..9e0e184f0b 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -152,7 +152,7 @@ namespace category
   attribute Precategory.carrier [coercion]
   attribute Precategory.struct [instance] [priority 10000] [coercion]
   -- definition precategory.carrier [coercion] [reducible] := Precategory.carrier
-  -- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct
+  -- definition precategory.struct [instance] [coercion] := Precategory.struct
   notation g ` ∘[`:60 C:0 `] `:0 f:60 :=
   @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f
   -- TODO: make this left associative
diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean
index 67b8250119..d23c7286ed 100644
--- a/hott/algebra/field.hlean
+++ b/hott/algebra/field.hlean
@@ -23,7 +23,7 @@ section division_ring
 
   protected definition algebra.div (a b : A) : A := a * b⁻¹
 
-  definition division_ring_has_div [reducible] [instance] : has_div A :=
+  definition division_ring_has_div [instance] : has_div A :=
   has_div.mk algebra.div
 
   lemma division.def (a b : A) : a / b = a * b⁻¹ :=
diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index f7c3cd08fc..ffecca5e28 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -462,7 +462,7 @@ section add_group
   -- TODO: derive corresponding facts for div in a field
   protected definition algebra.sub [reducible] (a b : A) : A := a + -b
 
-  definition add_group_has_sub [reducible] [instance] : has_sub A :=
+  definition add_group_has_sub [instance] : has_sub A :=
   has_sub.mk algebra.sub
 
   theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl
diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean
index 3657b2aa52..af18dc0830 100644
--- a/hott/algebra/ring.hlean
+++ b/hott/algebra/ring.hlean
@@ -75,7 +75,7 @@ section comm_semiring
 
   protected definition algebra.dvd (a b : A) : Type := Σc, b = a * c
 
-  definition comm_semiring_has_dvd [reducible] [instance] [priority algebra.prio] : has_dvd A :=
+  definition comm_semiring_has_dvd [instance] [priority algebra.prio] : has_dvd A :=
   has_dvd.mk algebra.dvd
 
   theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b :=
diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean
index 910162dce3..a8ab9bd342 100644
--- a/hott/homotopy/sphere.hlean
+++ b/hott/homotopy/sphere.hlean
@@ -37,10 +37,10 @@ namespace sphere_index
      from 0 and up this comes from a coercion from num to sphere_index (via nat)
   -/
 
-  definition has_zero_sphere_index [instance] [reducible] : has_zero sphere_index :=
+  definition has_zero_sphere_index [instance] : has_zero sphere_index :=
   has_zero.mk (succ minus_one)
 
-  definition has_one_sphere_index [instance] [reducible] : has_one sphere_index :=
+  definition has_one_sphere_index [instance] : has_one sphere_index :=
   has_one.mk (succ (succ minus_one))
 
   postfix `.+1`:(max+1) := sphere_index.succ
@@ -56,7 +56,7 @@ namespace sphere_index
 
   infix `+1+`:65 := sphere_index.add
 
-  definition has_le_sphere_index [instance] [reducible] : has_le sphere_index :=
+  definition has_le_sphere_index [instance] : has_le sphere_index :=
   has_le.mk leq
 
   definition succ_le_succ {n m : sphere_index} (H : n ≤ m) : n.+1 ≤ m.+1 := proof H qed
diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index 2587f6abf3..92bc546322 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -41,13 +41,13 @@ namespace nat
   | nat_refl : le a a    -- use nat_refl to avoid overloading le.refl
   | step : Π {b}, le a b → le a (succ b)
 
-  definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le
+  definition nat_has_le [instance] [priority nat.prio]: has_le nat := has_le.mk nat.le
 
   protected definition le_refl [refl] : Π a : nat, a ≤ a :=
   le.nat_refl
 
   protected definition lt [reducible] (n m : ℕ) := succ n ≤ m
-  definition nat_has_lt [instance] [reducible] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
+  definition nat_has_lt [instance] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
 
   definition pred [unfold 1] (a : nat) : nat :=
   nat.cases_on a zero (λ a₁, a₁)
@@ -60,10 +60,10 @@ namespace nat
   protected definition mul (a b : nat) : nat :=
   nat.rec_on b zero (λ b₁ r, r + a)
 
-  definition nat_has_sub [instance] [reducible] [priority nat.prio] : has_sub nat :=
+  definition nat_has_sub [instance] [priority nat.prio] : has_sub nat :=
   has_sub.mk nat.sub
 
-  definition nat_has_mul [instance] [reducible] [priority nat.prio] : has_mul nat :=
+  definition nat_has_mul [instance] [priority nat.prio] : has_mul nat :=
   has_mul.mk nat.mul
 
   /- properties of ℕ -/
diff --git a/hott/init/num.hlean b/hott/init/num.hlean
index 57c6e74019..255f903d05 100644
--- a/hott/init/num.hlean
+++ b/hott/init/num.hlean
@@ -34,7 +34,7 @@ namespace pos_num
   pos_num.lt a (succ b)
 end pos_num
 
-definition pos_num_has_mul [instance] [reducible] : has_mul pos_num :=
+definition pos_num_has_mul [instance] : has_mul pos_num :=
 has_mul.mk pos_num.mul
 
 namespace num
@@ -50,7 +50,7 @@ namespace num
   num.rec_on a zero (λpa, num.rec_on b zero (λpb, pos (pos_num.mul pa pb)))
 end num
 
-definition num_has_mul [instance] [reducible] : has_mul num :=
+definition num_has_mul [instance] : has_mul num :=
 has_mul.mk num.mul
 
 namespace num
@@ -80,5 +80,5 @@ namespace num
   num.rec_on a zero (λpa, num.rec_on b a (λpb, psub pa pb))
 end num
 
-definition num_has_sub [instance] [reducible] : has_sub num :=
+definition num_has_sub [instance] : has_sub num :=
 has_sub.mk num.sub
diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index ee2cabbef2..14f79ca397 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -41,13 +41,13 @@ definition bit0 [reducible] {A : Type} [s  : has_add A] (a  : A)
 definition bit1 [reducible] {A : Type} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A :=
 add (bit0 a) one
 
-definition num_has_zero [reducible] [instance]  : has_zero num :=
+definition num_has_zero [instance]  : has_zero num :=
 has_zero.mk num.zero
 
-definition num_has_one [reducible] [instance] : has_one num :=
+definition num_has_one [instance] : has_one num :=
 has_one.mk (num.pos pos_num.one)
 
-definition pos_num_has_one [reducible] [instance] : has_one pos_num :=
+definition pos_num_has_one [instance] : has_one pos_num :=
 has_one.mk (pos_num.one)
 
 namespace pos_num
@@ -75,7 +75,7 @@ namespace pos_num
     b
 end pos_num
 
-definition pos_num_has_add [reducible] [instance] : has_add pos_num :=
+definition pos_num_has_add [instance] : has_add pos_num :=
 has_add.mk pos_num.add
 
 namespace num
@@ -85,7 +85,7 @@ namespace num
   num.rec_on a b (λpa, num.rec_on b (pos pa) (λpb, pos (pos_num.add pa pb)))
 end num
 
-definition num_has_add [reducible] [instance] : has_add num :=
+definition num_has_add [instance] : has_add num :=
 has_add.mk num.add
 
 definition std.priority.default : num := 1000
@@ -105,13 +105,13 @@ end nat
 attribute pos_num_has_add pos_num_has_one num_has_zero num_has_one num_has_add
           [instance] [priority nat.prio]
 
-definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat :=
+definition nat_has_zero [instance] [priority nat.prio] : has_zero nat :=
 has_zero.mk nat.zero
 
-definition nat_has_one [reducible] [instance] [priority nat.prio] : has_one nat :=
+definition nat_has_one [instance] [priority nat.prio] : has_one nat :=
 has_one.mk (nat.succ (nat.zero))
 
-definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat :=
+definition nat_has_add [instance] [priority nat.prio] : has_add nat :=
 has_add.mk nat.add
 
 /-
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index e0bf90ad8e..2630de5e1e 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -23,10 +23,10 @@ namespace is_trunc
 
   open trunc_index
 
-  definition has_zero_trunc_index [instance] [priority 2000] [reducible] : has_zero trunc_index :=
+  definition has_zero_trunc_index [instance] [priority 2000] : has_zero trunc_index :=
   has_zero.mk (succ (succ minus_two))
 
-  definition has_one_trunc_index [instance] [priority 2000] [reducible] : has_one trunc_index :=
+  definition has_one_trunc_index [instance] [priority 2000] : has_one trunc_index :=
   has_one.mk (succ (succ (succ minus_two)))
 
   /-
@@ -55,14 +55,14 @@ namespace is_trunc
   definition leq [reducible] (n m : trunc_index) : Type₀ :=
   trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
 
-  definition has_le_trunc_index [instance] [priority 2000] [reducible] : has_le trunc_index :=
+  definition has_le_trunc_index [instance] [priority 2000] : has_le trunc_index :=
   has_le.mk leq
 
   end trunc_index
 
   attribute trunc_index.tr_add [reducible]
   infix `+2+`:65 := trunc_index.add_plus_two
-  definition has_add_trunc_index [instance] [priority 2000] [reducible] : has_add ℕ₋₂ :=
+  definition has_add_trunc_index [instance] [priority 2000] : has_add ℕ₋₂ :=
   has_add.mk trunc_index.tr_add
 
   namespace trunc_index
diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean
index 434b43f9c2..5f387faec4 100644
--- a/hott/types/fin.hlean
+++ b/hott/types/fin.hlean
@@ -113,7 +113,7 @@ end pigeonhole-/
 protected definition zero [constructor] (n : nat) : fin (succ n) :=
 mk 0 !zero_lt_succ
 
-definition fin_has_zero [instance] [reducible] (n : nat) : has_zero (fin (succ n)) :=
+definition fin_has_zero [instance] (n : nat) : has_zero (fin (succ n)) :=
 has_zero.mk (fin.zero n)
 
 definition val_zero (n : nat) : val (0 : fin (succ n)) = 0 := rfl
diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean
index eb07820410..1539554412 100644
--- a/hott/types/int/basic.hlean
+++ b/hott/types/int/basic.hlean
@@ -48,10 +48,10 @@ notation `-[1+ ` n `]` := int.neg_succ_of_nat n    -- for pretty-printing output
 
 protected definition prio : num := num.pred nat.prio
 
-definition int_has_zero [reducible] [instance] [priority int.prio] : has_zero int :=
+definition int_has_zero [instance] [priority int.prio] : has_zero int :=
 has_zero.mk (of_nat 0)
 
-definition int_has_one [reducible] [instance] [priority int.prio] : has_one int :=
+definition int_has_one [instance] [priority int.prio] : has_one int :=
 has_one.mk (of_nat 1)
 
 theorem of_nat_zero : of_nat (0:nat) = (0:int) :=
@@ -89,9 +89,9 @@ protected definition mul : ℤ → ℤ → ℤ
 
 /- notation -/
 
-definition int_has_add [reducible] [instance] [priority int.prio] : has_add int := has_add.mk int.add
-definition int_has_neg [reducible] [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
-definition int_has_mul [reducible] [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
+definition int_has_add [instance] [priority int.prio] : has_add int := has_add.mk int.add
+definition int_has_neg [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
+definition int_has_mul [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
 
 lemma mul_of_nat_of_nat   (m n : nat) : of_nat m * of_nat n = of_nat (m * n) :=
 rfl
@@ -575,10 +575,10 @@ protected definition integral_domain [reducible] [trans_instance] : integral_dom
   eq_zero_sum_eq_zero_of_mul_eq_zero := @int.eq_zero_sum_eq_zero_of_mul_eq_zero,
   is_set_carrier := is_set_of_decidable_eq⦄
 
-definition int_has_sub [reducible] [instance] [priority int.prio] : has_sub int :=
+definition int_has_sub [instance] [priority int.prio] : has_sub int :=
 has_sub.mk has_sub.sub
 
-definition int_has_dvd [reducible] [instance] [priority int.prio] : has_dvd int :=
+definition int_has_dvd [instance] [priority int.prio] : has_dvd int :=
 has_dvd.mk has_dvd.dvd
 
 /- additional properties -/
diff --git a/hott/types/nat/order.hlean b/hott/types/nat/order.hlean
index eec6584196..987b2a2ca3 100644
--- a/hott/types/nat/order.hlean
+++ b/hott/types/nat/order.hlean
@@ -117,7 +117,7 @@ decidable_linear_ordered_semiring nat :=
   mul_lt_mul_of_pos_right    := @nat.mul_lt_mul_of_pos_right,
   decidable_lt               := nat.decidable_lt ⦄
 
-definition nat_has_dvd [reducible] [instance] [priority nat.prio] : has_dvd nat :=
+definition nat_has_dvd [instance] [priority nat.prio] : has_dvd nat :=
 has_dvd.mk has_dvd.dvd
 
 theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b :=
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index 0fd993a688..c44fccb3af 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -51,7 +51,7 @@ namespace category
   definition objects [coercion] [reducible] (C : Category) : Type
   := Category.rec (fun c s, c) C
 
-  definition category_instance [instance] [coercion] [reducible] (C : Category) : category (objects C)
+  definition category_instance [instance] [coercion] (C : Category) : category (objects C)
   := Category.rec (fun c s, s) C
 
 end category
diff --git a/library/algebra/field.lean b/library/algebra/field.lean
index 4005daf5fc..e890353a84 100644
--- a/library/algebra/field.lean
+++ b/library/algebra/field.lean
@@ -22,7 +22,7 @@ section division_ring
 
   protected definition algebra.div (a b : A) : A := a * b⁻¹
 
-  definition division_ring_has_div [reducible] [instance] : has_div A :=
+  definition division_ring_has_div [instance] : has_div A :=
   has_div.mk algebra.div
 
   lemma division.def [simp] (a b : A) : a / b = a * b⁻¹ :=
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 75b2d5b453..c83988ef0f 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -446,7 +446,7 @@ section add_group
   -- TODO: derive corresponding facts for div in a field
   protected definition algebra.sub [reducible] (a b : A) : A := a + -b
 
-  definition add_group_has_sub [reducible] [instance] : has_sub A :=
+  definition add_group_has_sub [instance] : has_sub A :=
   has_sub.mk algebra.sub
 
   theorem sub_eq_add_neg [simp] (a b : A) : a - b = a + -b := rfl
diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean
index 167bdb6099..1667bf7484 100644
--- a/library/algebra/group_power.lean
+++ b/library/algebra/group_power.lean
@@ -40,7 +40,7 @@ definition monoid.pow (a : A) : ℕ → A
 | 0     := 1
 | (n+1) := a * monoid.pow n
 
-definition monoid_has_pow_nat [reducible] [instance] : has_pow_nat A :=
+definition monoid_has_pow_nat [instance] : has_pow_nat A :=
 has_pow_nat.mk monoid.pow
 
 theorem pow_zero (a : A) : a^0 = 1 := rfl
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index 685225875d..ed24a92d5c 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -77,7 +77,7 @@ section comm_semiring
 
   protected definition algebra.dvd (a b : A) : Prop := ∃c, b = a * c
 
-  definition comm_semiring_has_dvd [reducible] [instance] [priority algebra.prio] : has_dvd A :=
+  definition comm_semiring_has_dvd [instance] [priority algebra.prio] : has_dvd A :=
   has_dvd.mk algebra.dvd
 
   theorem dvd.intro {a b c : A} (H : a * c = b) : a ∣ b :=
diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean
index c50d7b895d..43ebf84f89 100644
--- a/library/algebra/ring_power.lean
+++ b/library/algebra/ring_power.lean
@@ -14,7 +14,7 @@ section semiring
 variable [s : semiring A]
 include s
 
-definition semiring_has_pow_nat [reducible] [instance] : has_pow_nat A :=
+definition semiring_has_pow_nat [instance] : has_pow_nat A :=
 monoid_has_pow_nat
 
 theorem zero_pow {m : ℕ} (mpos : m > 0) : 0^m = (0 : A) :=
@@ -33,7 +33,7 @@ section integral_domain
 variable [s : integral_domain A]
 include s
 
-definition integral_domain_has_pow_nat [reducible] [instance] : has_pow_nat A :=
+definition integral_domain_has_pow_nat [instance] : has_pow_nat A :=
 monoid_has_pow_nat
 
 theorem eq_zero_of_pow_eq_zero {a : A} {m : ℕ} (H : a^m = 0) : a = 0 :=
@@ -151,7 +151,7 @@ section decidable_linear_ordered_comm_ring
 variable [s : decidable_linear_ordered_comm_ring A]
 include s
 
-definition decidable_linear_ordered_comm_ring_has_pow_nat [reducible] [instance] : has_pow_nat A :=
+definition decidable_linear_ordered_comm_ring_has_pow_nat [instance] : has_pow_nat A :=
 monoid_has_pow_nat
 
 theorem abs_pow (a : A) (n : ℕ) : abs (a^n) = abs a^n :=
diff --git a/library/data/complex.lean b/library/data/complex.lean
index 8acf0147af..c284d34a42 100644
--- a/library/data/complex.lean
+++ b/library/data/complex.lean
@@ -37,10 +37,10 @@ definition of_num [coercion] [reducible] (n : num) : ℂ := n
 
 protected definition prio : num := num.pred real.prio
 
-definition complex_has_zero [reducible] [instance] [priority complex.prio] : has_zero ℂ :=
+definition complex_has_zero [instance] [priority complex.prio] : has_zero ℂ :=
 has_zero.mk (of_nat 0)
 
-definition complex_has_one [reducible] [instance] [priority complex.prio] : has_one ℂ :=
+definition complex_has_one [instance] [priority complex.prio] : has_one ℂ :=
 has_one.mk (of_nat 1)
 
 theorem re_of_real (x : ℝ) : re (of_real x) = x := rfl
@@ -60,13 +60,13 @@ complex.mk
 
 /- notation -/
 
-definition complex_has_add [reducible] [instance] [priority complex.prio] : has_add complex :=
+definition complex_has_add [instance] [priority complex.prio] : has_add complex :=
 has_add.mk complex.add
 
-definition complex_has_neg [reducible] [instance] [priority complex.prio] : has_neg complex :=
+definition complex_has_neg [instance] [priority complex.prio] : has_neg complex :=
 has_neg.mk complex.neg
 
-definition complex_has_mul [reducible] [instance] [priority complex.prio] : has_mul complex :=
+definition complex_has_mul [instance] [priority complex.prio] : has_mul complex :=
 has_mul.mk complex.mul
 
 protected theorem add_def (z w : ℂ) :
@@ -179,7 +179,7 @@ protected definition comm_ring [reducible] : comm_ring complex :=
 
 local attribute complex.comm_ring [instance]
 
-definition complex_has_sub [reducible] [instance] [priority complex.prio] : has_sub complex :=
+definition complex_has_sub [instance] [priority complex.prio] : has_sub complex :=
 has_sub.mk has_sub.sub
 
 theorem of_real_sub (x y : ℝ) : of_real (x - y) = of_real x - of_real y :=
@@ -234,7 +234,7 @@ end
 
 protected noncomputable definition inv (z : ℂ) : complex := conj z * of_real (cmod z)⁻¹
 
-protected noncomputable definition complex_has_inv [reducible] [instance] [priority complex.prio] :
+protected noncomputable definition complex_has_inv [instance] [priority complex.prio] :
   has_inv complex := has_inv.mk complex.inv
 
 protected theorem inv_def (z : ℂ) : z⁻¹ = conj z * of_real (cmod z)⁻¹ := rfl
@@ -252,7 +252,7 @@ classical.by_cases
 
 noncomputable protected definition div (z w : ℂ) : ℂ := z * w⁻¹
 
-noncomputable definition complex_has_div [instance] [reducible] [priority complex.prio] :
+noncomputable definition complex_has_div [instance] [priority complex.prio] :
     has_div complex :=
   has_div.mk complex.div
 
diff --git a/library/data/fin.lean b/library/data/fin.lean
index 5830042b91..30338ca377 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -88,7 +88,7 @@ end pigeonhole
 protected definition zero (n : nat) : fin (succ n) :=
 mk 0 !zero_lt_succ
 
-definition fin_has_zero [instance] [reducible] (n : nat) : has_zero (fin (succ n)) :=
+definition fin_has_zero [instance] (n : nat) : has_zero (fin (succ n)) :=
 has_zero.mk (fin.zero n)
 
 theorem val_zero (n : nat) : val (0 : fin (succ n)) = 0 := rfl
diff --git a/library/data/hf.lean b/library/data/hf.lean
index d75eb373b3..a75fc78192 100644
--- a/library/data/hf.lean
+++ b/library/data/hf.lean
@@ -23,7 +23,7 @@ protected definition prio : num := num.succ std.priority.default
 protected definition is_inhabited [instance] : inhabited hf :=
 nat.is_inhabited
 
-protected definition has_decidable_eq [reducible] [instance] : decidable_eq hf :=
+protected definition has_decidable_eq [instance] : decidable_eq hf :=
 nat.has_decidable_eq
 
 definition of_finset (s : finset hf) : hf :=
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 57fc5302f6..358752196c 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -48,10 +48,10 @@ notation `-[1+ ` n `]` := int.neg_succ_of_nat n    -- for pretty-printing output
 
 protected definition prio : num := num.pred nat.prio
 
-definition int_has_zero [reducible] [instance] [priority int.prio] : has_zero int :=
+definition int_has_zero [instance] [priority int.prio] : has_zero int :=
 has_zero.mk (of_nat 0)
 
-definition int_has_one [reducible] [instance] [priority int.prio] : has_one int :=
+definition int_has_one [instance] [priority int.prio] : has_one int :=
 has_one.mk (of_nat 1)
 
 theorem of_nat_zero : of_nat (0:nat) = (0:int) :=
@@ -89,9 +89,9 @@ protected definition mul : ℤ → ℤ → ℤ
 
 /- notation -/
 
-definition int_has_add [reducible] [instance] [priority int.prio] : has_add int := has_add.mk int.add
-definition int_has_neg [reducible] [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
-definition int_has_mul [reducible] [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
+definition int_has_add [instance] [priority int.prio] : has_add int := has_add.mk int.add
+definition int_has_neg [instance] [priority int.prio] : has_neg int := has_neg.mk int.neg
+definition int_has_mul [instance] [priority int.prio] : has_mul int := has_mul.mk int.mul
 
 lemma mul_of_nat_of_nat   (m n : nat) : of_nat m * of_nat n = of_nat (m * n) :=
 rfl
@@ -536,10 +536,10 @@ protected definition integral_domain [reducible] [trans_instance] : integral_dom
   zero_ne_one    := int.zero_ne_one,
   eq_zero_or_eq_zero_of_mul_eq_zero := @int.eq_zero_or_eq_zero_of_mul_eq_zero⦄
 
-definition int_has_sub [reducible] [instance] [priority int.prio] : has_sub int :=
+definition int_has_sub [instance] [priority int.prio] : has_sub int :=
 has_sub.mk has_sub.sub
 
-definition int_has_dvd [reducible] [instance] [priority int.prio] : has_dvd int :=
+definition int_has_dvd [instance] [priority int.prio] : has_dvd int :=
 has_dvd.mk has_dvd.dvd
 
 /- additional properties -/
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index 8ea0bef1b0..4b21ddb2f4 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -23,7 +23,7 @@ sign b *
     | -[1+m]   := -[1+ ((m:nat) / (nat_abs b))]
   end)
 
-definition int_has_div [reducible] [instance] [priority int.prio] : has_div int :=
+definition int_has_div [instance] [priority int.prio] : has_div int :=
 has_div.mk int.div
 
 lemma of_nat_div_eq (m : nat) (b : ℤ) : (of_nat m) / b = sign b * of_nat (m / (nat_abs b)) :=
@@ -42,7 +42,7 @@ rfl
 
 protected definition mod (a b : ℤ) : ℤ := a - a / b * b
 
-definition int_has_mod [reducible] [instance] [priority int.prio] : has_mod int :=
+definition int_has_mod [instance] [priority int.prio] : has_mod int :=
 has_mod.mk int.mod
 
 
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index b2b8283141..2d1b8260cc 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -16,12 +16,12 @@ namespace int
 private definition nonneg (a : ℤ) : Prop := int.cases_on a (take n, true) (take n, false)
 protected definition le (a b : ℤ) : Prop := nonneg (b - a)
 
-definition int_has_le [instance] [reducible] [priority int.prio]: has_le int :=
+definition int_has_le [instance] [priority int.prio]: has_le int :=
 has_le.mk int.le
 
 protected definition lt (a b : ℤ) : Prop := (a + 1) ≤ b
 
-definition int_has_lt [instance] [reducible] [priority int.prio]: has_lt int :=
+definition int_has_lt [instance] [priority int.prio]: has_lt int :=
 has_lt.mk int.lt
 
 local attribute nonneg [reducible]
@@ -253,7 +253,7 @@ protected definition linear_ordered_comm_ring [reducible] [trans_instance] :
   zero_lt_one      := int.zero_lt_one,
   add_lt_add_left  := @int.add_lt_add_left⦄
 
-protected definition decidable_linear_ordered_comm_ring [reducible] [instance] :
+protected definition decidable_linear_ordered_comm_ring [instance] :
     decidable_linear_ordered_comm_ring int :=
 ⦃decidable_linear_ordered_comm_ring,
  int.linear_ordered_comm_ring,
diff --git a/library/data/int/power.lean b/library/data/int/power.lean
index abec75efc0..e48782f989 100644
--- a/library/data/int/power.lean
+++ b/library/data/int/power.lean
@@ -9,7 +9,7 @@ import data.int.basic data.int.order data.int.div algebra.group_power data.nat.p
 
 namespace int
 
-definition int_has_pow_nat [reducible] [instance] [priority int.prio] : has_pow_nat int :=
+definition int_has_pow_nat [instance] [priority int.prio] : has_pow_nat int :=
 has_pow_nat.mk has_pow_nat.pow_nat
 
 /-
diff --git a/library/data/matrix.lean b/library/data/matrix.lean
index acb4bfb604..b71de4fc67 100644
--- a/library/data/matrix.lean
+++ b/library/data/matrix.lean
@@ -68,16 +68,16 @@ protected definition mul (M : matrix A m n) (N : matrix A n p) : matrix A m p :=
 definition smul (a : A) (M : matrix A m n) : matrix A m n :=
 λ i j, a * M[i, j]
 
-definition matrix_has_zero [reducible] [instance] (m n : nat) : has_zero (matrix A m n) :=
+definition matrix_has_zero [instance] (m n : nat) : has_zero (matrix A m n) :=
 has_zero.mk (matrix.zero m n)
 
-definition matrix_has_one [reducible] [instance] (n : nat) : has_one (matrix A n n) :=
+definition matrix_has_one [instance] (n : nat) : has_one (matrix A n n) :=
 has_one.mk (identity n)
 
-definition matrix_has_add [reducible] [instance] (m n : nat) : has_add (matrix A m n) :=
+definition matrix_has_add [instance] (m n : nat) : has_add (matrix A m n) :=
 has_add.mk matrix.add
 
-definition matrix_has_mul [reducible] [instance] (n : nat) : has_mul (matrix A n n) :=
+definition matrix_has_mul [instance] (n : nat) : has_mul (matrix A n n) :=
 has_mul.mk matrix.mul
 
 infix ` × ` := mul
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index cdb02734c9..ecf99e4f82 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -21,7 +21,7 @@ if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y + 1 else zero
 
 protected definition div := fix div.F
 
-definition nat_has_divide [reducible] [instance] [priority nat.prio] : has_div nat :=
+definition nat_has_divide [instance] [priority nat.prio] : has_div nat :=
 has_div.mk nat.div
 
 theorem div_def (x y : nat) : div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 :=
@@ -78,7 +78,7 @@ if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
 
 protected definition mod := fix mod.F
 
-definition nat_has_mod [reducible] [instance] [priority nat.prio] : has_mod nat :=
+definition nat_has_mod [instance] [priority nat.prio] : has_mod nat :=
 has_mod.mk nat.mod
 
 notation [priority nat.prio] a ≡ b `[mod `:0 c:0 `]` := a % c = b % c
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 013b979b1b..61a2f976ea 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -117,7 +117,7 @@ decidable_linear_ordered_semiring nat :=
   mul_lt_mul_of_pos_right    := @nat.mul_lt_mul_of_pos_right,
   decidable_lt               := nat.decidable_lt ⦄
 
-definition nat_has_dvd [reducible] [instance] [priority nat.prio] : has_dvd nat :=
+definition nat_has_dvd [instance] [priority nat.prio] : has_dvd nat :=
 has_dvd.mk has_dvd.dvd
 
 theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b :=
diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean
index b97ad5c8f5..1d422bcd00 100644
--- a/library/data/nat/power.lean
+++ b/library/data/nat/power.lean
@@ -9,7 +9,7 @@ import data.nat.basic data.nat.order data.nat.div data.nat.gcd algebra.ring_powe
 
 namespace nat
 
-definition nat_has_pow_nat [instance] [reducible] [priority nat.prio] : has_pow_nat nat :=
+definition nat_has_pow_nat [instance] [priority nat.prio] : has_pow_nat nat :=
 has_pow_nat.mk has_pow_nat.pow_nat
 
 theorem pow_le_pow_of_le {x y : ℕ} (i : ℕ) (H : x ≤ y) : x^i ≤ y^i :=
diff --git a/library/data/pnat.lean b/library/data/pnat.lean
index 8c90792bd4..897d106ff5 100644
--- a/library/data/pnat.lean
+++ b/library/data/pnat.lean
@@ -35,19 +35,19 @@ protected definition le (p q : ℕ+) := p~ ≤ q~
 
 protected definition lt (p q : ℕ+) := p~ < q~
 
-definition pnat_has_add [instance] [reducible] : has_add pnat :=
+definition pnat_has_add [instance] : has_add pnat :=
 has_add.mk pnat.add
 
-definition pnat_has_mul [instance] [reducible] : has_mul pnat :=
+definition pnat_has_mul [instance] : has_mul pnat :=
 has_mul.mk pnat.mul
 
-definition pnat_has_le [instance] [reducible] : has_le pnat :=
+definition pnat_has_le [instance] : has_le pnat :=
 has_le.mk pnat.le
 
-definition pnat_has_lt [instance] [reducible] : has_lt pnat :=
+definition pnat_has_lt [instance] : has_lt pnat :=
 has_lt.mk pnat.lt
 
-definition pnat_has_one [instance] [reducible] : has_one pnat :=
+definition pnat_has_one [instance] : has_one pnat :=
 has_one.mk (pos (1:nat) dec_trivial)
 
 protected lemma mul_def (p q : ℕ+) : p * q = tag (p~ * q~) (mul_pos (pnat_pos p) (pnat_pos q)) :=
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index 4bf4b982eb..3dd17dc7f1 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -358,10 +358,10 @@ definition of_num [coercion] [reducible] (n : num) : ℚ := n
 
 protected definition prio := num.pred int.prio
 
-definition rat_has_zero [reducible] [instance] [priority rat.prio] : has_zero rat :=
+definition rat_has_zero [instance] [priority rat.prio] : has_zero rat :=
 has_zero.mk (of_int 0)
 
-definition rat_has_one [reducible] [instance] [priority rat.prio] : has_one rat :=
+definition rat_has_one [instance] [priority rat.prio] : has_one rat :=
 has_one.mk (of_int 1)
 
 theorem of_int_zero : of_int (0:int) = (0:rat) :=
@@ -401,21 +401,21 @@ definition denom (a : ℚ) : ℤ := prerat.denom (reduce a)
 theorem denom_pos (a : ℚ): denom a > 0 :=
 prerat.denom_pos (reduce a)
 
-definition rat_has_add [reducible] [instance] [priority rat.prio] : has_add rat :=
+definition rat_has_add [instance] [priority rat.prio] : has_add rat :=
 has_add.mk rat.add
 
-definition rat_has_mul [reducible] [instance] [priority rat.prio] : has_mul rat :=
+definition rat_has_mul [instance] [priority rat.prio] : has_mul rat :=
 has_mul.mk rat.mul
 
-definition rat_has_neg [reducible] [instance] [priority rat.prio] : has_neg rat :=
+definition rat_has_neg [instance] [priority rat.prio] : has_neg rat :=
 has_neg.mk rat.neg
 
-definition rat_has_inv [reducible] [instance] [priority rat.prio] : has_inv rat :=
+definition rat_has_inv [instance] [priority rat.prio] : has_inv rat :=
 has_inv.mk rat.inv
 
 protected definition sub [reducible] (a b : ℚ) : rat := a + (-b)
 
-definition rat_has_sub [reducible] [instance] [priority rat.prio] : has_sub rat :=
+definition rat_has_sub [instance] [priority rat.prio] : has_sub rat :=
 has_sub.mk rat.sub
 
 lemma sub.def (a b : ℚ) : a - b = a + (-b) :=
@@ -574,10 +574,10 @@ protected definition discrete_field [reducible] [trans_instance] : discrete_fiel
  inv_zero         := rat.inv_zero,
  has_decidable_eq := has_decidable_eq⦄
 
-definition rat_has_div [instance] [reducible] [priority rat.prio] : has_div rat :=
+definition rat_has_div [instance] [priority rat.prio] : has_div rat :=
 has_div.mk has_div.div
 
-definition rat_has_pow_nat [instance] [reducible] [priority rat.prio] : has_pow_nat rat :=
+definition rat_has_pow_nat [instance] [priority rat.prio] : has_pow_nat rat :=
 has_pow_nat.mk has_pow_nat.pow_nat
 
 theorem eq_num_div_denom (a : ℚ) : a = num a / denom a :=
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index 95c3cf8486..a8b0966cb6 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -142,10 +142,10 @@ quot.rec_on_subsingleton a (take u, int.decidable_lt 0 (prerat.num u))
 protected definition lt (a b : ℚ) : Prop := pos (b - a)
 protected definition le (a b : ℚ) : Prop := nonneg (b - a)
 
-definition rat_has_lt [reducible] [instance] [priority rat.prio] : has_lt rat :=
+definition rat_has_lt [instance] [priority rat.prio] : has_lt rat :=
 has_lt.mk rat.lt
 
-definition rat_has_le [reducible] [instance] [priority rat.prio] : has_le rat :=
+definition rat_has_le [instance] [priority rat.prio] : has_le rat :=
 has_le.mk rat.le
 
 protected lemma lt_def (a b : ℚ) : (a < b) = pos (b - a) :=
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index 9210d1464a..49bff39188 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -1075,18 +1075,18 @@ protected definition neg (x : ℝ) : ℝ :=
                                    quot.sound (rneg_well_defined Hab)))
 --prefix [priority real.prio] `-` := neg
 
-definition real_has_add [reducible] [instance] [priority real.prio] : has_add real :=
+definition real_has_add [instance] [priority real.prio] : has_add real :=
 has_add.mk real.add
 
-definition real_has_mul [reducible] [instance] [priority real.prio] : has_mul real :=
+definition real_has_mul [instance] [priority real.prio] : has_mul real :=
 has_mul.mk real.mul
 
-definition real_has_neg [reducible] [instance] [priority real.prio] : has_neg real :=
+definition real_has_neg [instance] [priority real.prio] : has_neg real :=
 has_neg.mk real.neg
 
 protected definition sub [reducible] (a b : ℝ) : real := a + (-b)
 
-definition real_has_sub [reducible] [instance] [priority real.prio] : has_sub real :=
+definition real_has_sub [instance] [priority real.prio] : has_sub real :=
 has_sub.mk real.sub
 
 open rat -- no coercions before
diff --git a/library/data/real/division.lean b/library/data/real/division.lean
index 1d995d52c9..e6bc53852a 100644
--- a/library/data/real/division.lean
+++ b/library/data/real/division.lean
@@ -587,7 +587,7 @@ noncomputable protected definition inv (x : ℝ) : ℝ :=
   quot.lift_on x (λ a, quot.mk (rat_seq.r_inv a))
            (λ a b H, quot.sound (rat_seq.r_inv_well_defined H))
 
-noncomputable definition real_has_inv [instance] [reducible] [priority real.prio] : has_inv real :=
+noncomputable definition real_has_inv [instance] [priority real.prio] : has_inv real :=
   has_inv.mk real.inv
 
 noncomputable protected definition div (x y : ℝ) : ℝ :=
@@ -596,7 +596,7 @@ noncomputable protected definition div (x y : ℝ) : ℝ :=
 noncomputable definition real_has_div : has_div real :=
   has_div.mk real.div
 
-local attribute real_has_div [instance] [reducible] [priority real.prio]
+local attribute real_has_div [instance] [priority real.prio]
 
 protected theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x :=
   quot.induction_on₂ x y (λ s t, rat_seq.r_le_total s t)
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index 1a8fb6ee23..edeec7082b 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -1026,10 +1026,10 @@ protected definition lt (x y : ℝ) :=
 protected definition le (x y : ℝ) :=
   quot.lift_on₂ x y (λ a b, rat_seq.r_le a b) rat_seq.r_le_well_defined
 
-definition real_has_lt [reducible] [instance] [priority real.prio] : has_lt ℝ :=
+definition real_has_lt [instance] [priority real.prio] : has_lt ℝ :=
 has_lt.mk real.lt
 
-definition real_has_le [reducible] [instance] [priority real.prio] : has_le ℝ :=
+definition real_has_le [instance] [priority real.prio] : has_le ℝ :=
 has_le.mk real.le
 
 definition sep (x y : ℝ) := quot.lift_on₂ x y (λ a b, rat_seq.r_sep a b) rat_seq.r_sep_well_defined
diff --git a/library/init/nat.lean b/library/init/nat.lean
index f111813881..5937bc9934 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -39,13 +39,13 @@ namespace nat
   | nat_refl : le a a    -- use nat_refl to avoid overloading le.refl
   | step : Π {b}, le a b → le a (succ b)
 
-  definition nat_has_le [instance] [reducible] [priority nat.prio]: has_le nat := has_le.mk nat.le
+  definition nat_has_le [instance] [priority nat.prio]: has_le nat := has_le.mk nat.le
 
   protected lemma le_refl [refl] : ∀ a : nat, a ≤ a :=
   le.nat_refl
 
   protected definition lt [reducible] (n m : ℕ) := succ n ≤ m
-  definition nat_has_lt [instance] [reducible] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
+  definition nat_has_lt [instance] [priority nat.prio] : has_lt nat := has_lt.mk nat.lt
 
   definition pred [unfold 1] (a : nat) : nat :=
   nat.cases_on a zero (λ a₁, a₁)
@@ -58,10 +58,10 @@ namespace nat
   protected definition mul (a b : nat) : nat :=
   nat.rec_on b zero (λ b₁ r, r + a)
 
-  definition nat_has_sub [instance] [reducible] [priority nat.prio] : has_sub nat :=
+  definition nat_has_sub [instance] [priority nat.prio] : has_sub nat :=
   has_sub.mk nat.sub
 
-  definition nat_has_mul [instance] [reducible] [priority nat.prio] : has_mul nat :=
+  definition nat_has_mul [instance] [priority nat.prio] : has_mul nat :=
   has_mul.mk nat.mul
 
   /- properties of ℕ -/
diff --git a/library/init/num.lean b/library/init/num.lean
index 84eee17874..4e76abeb32 100644
--- a/library/init/num.lean
+++ b/library/init/num.lean
@@ -34,7 +34,7 @@ namespace pos_num
   pos_num.lt a (succ b)
 end pos_num
 
-definition pos_num_has_mul [instance] [reducible] : has_mul pos_num :=
+definition pos_num_has_mul [instance] : has_mul pos_num :=
 has_mul.mk pos_num.mul
 
 namespace num
@@ -50,7 +50,7 @@ namespace num
   num.rec_on a zero (λpa, num.rec_on b zero (λpb, pos (pos_num.mul pa pb)))
 end num
 
-definition num_has_mul [instance] [reducible] : has_mul num :=
+definition num_has_mul [instance] : has_mul num :=
 has_mul.mk num.mul
 
 namespace num
@@ -80,5 +80,5 @@ namespace num
   num.rec_on a zero (λpa, num.rec_on b a (λpb, psub pa pb))
 end num
 
-definition num_has_sub [instance] [reducible] : has_sub num :=
+definition num_has_sub [instance] : has_sub num :=
 has_sub.mk num.sub
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index a23ca4e2b7..55cad3d402 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -40,13 +40,13 @@ definition gt [reducible] {A : Type} [s : has_lt A] (a b : A) : Prop := lt b a
 definition bit0 {A : Type} [s  : has_add A] (a  : A)                 : A := add a a
 definition bit1 {A : Type} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add (bit0 a) one
 
-definition num_has_zero [reducible] [instance] : has_zero num :=
+definition num_has_zero [instance] : has_zero num :=
 has_zero.mk num.zero
 
-definition num_has_one [reducible] [instance] : has_one num :=
+definition num_has_one [instance] : has_one num :=
 has_one.mk (num.pos pos_num.one)
 
-definition pos_num_has_one [reducible] [instance] : has_one pos_num :=
+definition pos_num_has_one [instance] : has_one pos_num :=
 has_one.mk (pos_num.one)
 
 namespace pos_num
@@ -74,7 +74,7 @@ namespace pos_num
     b
 end pos_num
 
-definition pos_num_has_add [reducible] [instance] : has_add pos_num :=
+definition pos_num_has_add [instance] : has_add pos_num :=
 has_add.mk pos_num.add
 
 namespace num
@@ -84,7 +84,7 @@ namespace num
   num.rec_on a b (λpa, num.rec_on b (pos pa) (λpb, pos (pos_num.add pa pb)))
 end num
 
-definition num_has_add [reducible] [instance] : has_add num :=
+definition num_has_add [instance] : has_add num :=
 has_add.mk num.add
 
 definition std.priority.default : num := 1000
@@ -104,13 +104,13 @@ end nat
 attribute pos_num_has_add pos_num_has_one num_has_zero num_has_one num_has_add
           [instance] [priority nat.prio]
 
-definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat :=
+definition nat_has_zero [instance] [priority nat.prio] : has_zero nat :=
 has_zero.mk nat.zero
 
-definition nat_has_one [reducible] [instance] [priority nat.prio] : has_one nat :=
+definition nat_has_one [instance] [priority nat.prio] : has_one nat :=
 has_one.mk (nat.succ (nat.zero))
 
-definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat :=
+definition nat_has_add [instance] [priority nat.prio] : has_add nat :=
 has_add.mk nat.add
 
 /-
diff --git a/library/theories/measure_theory/extended_real.lean b/library/theories/measure_theory/extended_real.lean
index fd078cebc5..778d2008ca 100644
--- a/library/theories/measure_theory/extended_real.lean
+++ b/library/theories/measure_theory/extended_real.lean
@@ -31,10 +31,10 @@ protected definition prio := num.pred real.prio
 
 /- arithmetic operations on the ereals -/
 
-definition ereal_has_zero [reducible] [instance] [priority ereal.prio] : has_zero ereal :=
+definition ereal_has_zero [instance] [priority ereal.prio] : has_zero ereal :=
 has_zero.mk (of_real 0)
 
-definition ereal_has_one [reducible] [instance] [priority ereal.prio] : has_one ereal :=
+definition ereal_has_one [instance] [priority ereal.prio] : has_one ereal :=
 has_one.mk (of_real 1)
 
 protected definition add : ereal → ereal → ereal
@@ -61,18 +61,18 @@ protected definition mul : ereal → ereal → ereal
 | -∞ a                    := ereal.neg (blow_up a)
 | a -∞                    := ereal.neg (blow_up a)
 
-definition ereal_has_add [reducible] [instance] [priority ereal.prio] : has_add ereal :=
+definition ereal_has_add [instance] [priority ereal.prio] : has_add ereal :=
 has_add.mk ereal.add
 
-definition ereal_has_neg [reducible] [instance] [priority ereal.prio] : has_neg ereal :=
+definition ereal_has_neg [instance] [priority ereal.prio] : has_neg ereal :=
 has_neg.mk ereal.neg
 
 protected definition sub (u v : ereal) : ereal := u + -v
 
-definition ereal_has_sub [reducible] [instance] [priority ereal.prio] : has_sub ereal :=
+definition ereal_has_sub [instance] [priority ereal.prio] : has_sub ereal :=
 has_sub.mk ereal.sub
 
-definition ereal_has_mul [reducible] [instance] [priority ereal.prio] : has_mul ereal :=
+definition ereal_has_mul [instance] [priority ereal.prio] : has_mul ereal :=
 has_mul.mk ereal.mul
 
 protected theorem zero_def : (0 : ereal) = of_real 0 := rfl
@@ -313,7 +313,7 @@ protected definition le : ereal → ereal → Prop
 | ∞ (of_real y)           := false
 | ∞ -∞                    := false
 
-definition ereal_has_le [reducible] [instance] [priority ereal.prio] :
+definition ereal_has_le [instance] [priority ereal.prio] :
   has_le ereal :=
 has_le.mk ereal.le
 
@@ -362,7 +362,7 @@ protected theorem le_antisymm : ∀ u v : ereal, u ≤ v → v ≤ u → u = v
 
 protected definition lt (x y : ereal) : Prop := x ≤ y ∧ x ≠ y
 
-definition ereal_has_lt [reducible] [instance] [priority ereal.prio] :
+definition ereal_has_lt [instance] [priority ereal.prio] :
   has_lt ereal :=
 has_lt.mk ereal.lt
 
diff --git a/library/theories/measure_theory/sigma_algebra.lean b/library/theories/measure_theory/sigma_algebra.lean
index 1c23d8cb84..872c33e45b 100644
--- a/library/theories/measure_theory/sigma_algebra.lean
+++ b/library/theories/measure_theory/sigma_algebra.lean
@@ -112,7 +112,7 @@ theorem measurable_generated_by {G : set (set X)} :
 
 protected definition le (M N : sigma_algebra X) : Prop := @sets _ M ⊆ @sets _ N
 
-definition sigma_algebra_has_le [reducible] [instance] :
+definition sigma_algebra_has_le [instance] :
   has_le (sigma_algebra X) :=
 has_le.mk sigma_algebra.le
 
diff --git a/library/theories/topology/basic.lean b/library/theories/topology/basic.lean
index 989339622a..4561249b0f 100644
--- a/library/theories/topology/basic.lean
+++ b/library/theories/topology/basic.lean
@@ -157,8 +157,8 @@ namespace topology
     (T0_space.T0)
     (assume H, obtain U [OpU xyU], from H,
      suppose x = y,
-     have x ∈ U ↔ y ∈ U, from iff.intro 
-       (assume xU, this ▸ xU) 
+     have x ∈ U ↔ y ∈ U, from iff.intro
+       (assume xU, this ▸ xU)
        (assume yU, this⁻¹ ▸ yU),
      absurd this xyU)
 end topology
@@ -179,16 +179,16 @@ protected definition T0_space.of_T1 [reducible] [trans_instance] {X : Type} [T :
 namespace topology
   variables {X : Type} [T1_space X]
 
-  theorem separation_T1 {x y : X} : x ≠ y ↔ (∃ U, Open U ∧ x ∈ U ∧ y ∉ U) := 
+  theorem separation_T1 {x y : X} : x ≠ y ↔ (∃ U, Open U ∧ x ∈ U ∧ y ∉ U) :=
   iff.intro
     (T1_space.T1)
-    (suppose ∃ U, Open U ∧ x ∈ U ∧ y ∉ U, 
+    (suppose ∃ U, Open U ∧ x ∈ U ∧ y ∉ U,
      obtain U [OpU xU nyU], from this,
-     suppose x = y, 
+     suppose x = y,
      absurd xU (this⁻¹ ▸ nyU))
-     
-  theorem closed_singleton {a : X} : closed '{a} := 
-  let T := ⋃₀ {S| Open S ∧ a ∉ S} in 
+
+  theorem closed_singleton {a : X} : closed '{a} :=
+  let T := ⋃₀ {S| Open S ∧ a ∉ S} in
   have Open T, from Open_sUnion (λS HS, and.elim_left HS),
   have T = -'{a}, from ext(take x, iff.intro
     (assume xT, assume xa,
@@ -197,7 +197,7 @@ namespace topology
        exists.intro S (and.intro OpS (and.intro xS aS)),
      have x ≠ a, from (iff.elim_right separation_T1) this,
      absurd ((iff.elim_left !mem_singleton_iff) xa) this)
-    (assume xa, 
+    (assume xa,
      have x ≠ a, from not.intro(
        assume H, absurd ((iff.elim_right !mem_singleton_iff) H) xa),
      obtain U [OpU xU aU], from (iff.elim_left separation_T1) this,
@@ -223,10 +223,10 @@ protected definition T1_space.of_T2 [reducible] [trans_instance] {X : Type} [T :
 namespace topology
   variables {X : Type} [T2_space X]
 
-  theorem seperation_T2 {x y : X} : x ≠ y ↔ ∃ U V, Open U ∧ Open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = ∅ := 
+  theorem seperation_T2 {x y : X} : x ≠ y ↔ ∃ U V, Open U ∧ Open V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = ∅ :=
   iff.intro
     (T2_space.T2)
-    (assume H, obtain U V [OpU OpV xU yV UV], from H, 
+    (assume H, obtain U V [OpU OpV xU yV UV], from H,
      suppose x = y,
      have ¬(x ∈ U ∩ V), from not.intro(
        assume xUV, absurd (UV ▸ xUV) !not_mem_empty),
@@ -247,7 +247,7 @@ inductive opens_generated_by {X : Type} (B : set (set X)) : set X → Prop :=
                     opens_generated_by B (s ∩ t)
 | sUnion_mem     : ∀ ⦃S : set (set X)⦄, S ⊆ opens_generated_by B → opens_generated_by B (⋃₀ S)
 
-protected definition generated_by [instance] [reducible] {X : Type} (B : set (set X)) : topology X :=
+protected definition generated_by [instance] {X : Type} (B : set (set X)) : topology X :=
 ⦃topology,
   opens            := opens_generated_by B,
   univ_mem_opens   := opens_generated_by.univ_mem B,
diff --git a/library/theories/topology/order_topology.lean b/library/theories/topology/order_topology.lean
index c12b81b2fc..a43a98b5f5 100644
--- a/library/theories/topology/order_topology.lean
+++ b/library/theories/topology/order_topology.lean
@@ -14,7 +14,7 @@ variables {X : Type} [linear_strong_order_pair X]
 
 definition linorder_generators : set (set X) := {y | ∃ a, y = '(a, ∞) } ∪ {y | ∃ a, y = '(-∞, a)}
 
-definition linorder_topology [instance] [reducible] : topology X :=
+definition linorder_topology [instance] : topology X :=
   topology.generated_by linorder_generators
 
 theorem Open_Ioi {a : X} : Open '(a, ∞) :=