diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index a63a29071..1ed9d5928 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -611,7 +611,7 @@ or_of_or_of_imp_of_imp H3
 section
   open [classes] algebra
 
-  protected definition integral_domain [instance] : algebra.integral_domain int :=
+  protected definition integral_domain [instance] [reducible] : algebra.integral_domain int :=
   algebra.integral_domain.mk add add.assoc zero zero_add add_zero neg add.left_inv
   add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
   zero_ne_one mul.comm @eq_zero_or_eq_zero_of_mul_eq_zero
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index abe08e05f..99a7657c9 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -214,14 +214,15 @@ lt.intro
 section
   open [classes] algebra
 
-  protected definition linear_ordered_comm_ring [instance] : algebra.linear_ordered_comm_ring int :=
+  protected definition linear_ordered_comm_ring [instance] [reducible] :
+    algebra.linear_ordered_comm_ring int :=
   algebra.linear_ordered_comm_ring.mk add add.assoc zero zero_add add_zero neg add.left_inv
     add.comm mul mul.assoc (of_num 1) one_mul mul_one mul.left_distrib mul.right_distrib
     zero_ne_one le le.refl @le.trans @le.antisymm lt lt_iff_le_and_ne @add_le_add_left
     @mul_nonneg @mul_pos le_iff_lt_or_eq le.total mul.comm
 
 
-  protected definition decidable_linear_ordered_comm_ring [instance] :
+  protected definition decidable_linear_ordered_comm_ring [instance] [reducible] :
     algebra.decidable_linear_ordered_comm_ring int :=
   ⦃algebra.decidable_linear_ordered_comm_ring,
     int.linear_ordered_comm_ring,
diff --git a/library/data/nat/comm_semiring.lean b/library/data/nat/comm_semiring.lean
index 5474db55a..2d144166a 100644
--- a/library/data/nat/comm_semiring.lean
+++ b/library/data/nat/comm_semiring.lean
@@ -14,7 +14,7 @@ namespace nat
 section
   open [classes] algebra
 
-  protected definition comm_semiring [instance] : algebra.comm_semiring nat :=
+  protected definition comm_semiring [instance] [reducible] : algebra.comm_semiring nat :=
   algebra.comm_semiring.mk add add.assoc zero zero_add add_zero add.comm
     mul mul.assoc (succ zero) one_mul mul_one mul.left_distrib mul.right_distrib
     zero_mul mul_zero (ne.symm (succ_ne_zero zero)) mul.comm
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index c5f4ff17a..2bd00f6c9 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -150,7 +150,8 @@ le.intro !zero_add
 section
   open [classes] algebra
 
-  protected definition linear_ordered_semiring [instance] : algebra.linear_ordered_semiring nat :=
+  protected definition linear_ordered_semiring [instance] [reducible] :
+    algebra.linear_ordered_semiring nat :=
   ⦃ algebra.linear_ordered_semiring, nat.comm_semiring,
     add_left_cancel            := @add.cancel_left,
     add_right_cancel           := @add.cancel_right,