fix(library/algebra): add missing [reducible]

It addresses issues raised at #403

library/algebra/group.lean

@@ -261,11 +261,11 @@ section group
      ... = (c * b) * b⁻¹ : H
      ... = c : mul_inv_cancel_right
 
-  definition group.to_left_cancel_semigroup [instance] [coercion] : left_cancel_semigroup A :=
+  definition group.to_left_cancel_semigroup [instance] [coercion] [reducible] : left_cancel_semigroup A :=
   ⦃ left_cancel_semigroup, s,
     mul_left_cancel := @mul_left_cancel A s ⦄
 
-  definition group.to_right_cancel_semigroup [instance] [coercion] : right_cancel_semigroup A :=
+  definition group.to_right_cancel_semigroup [instance] [coercion] [reducible] : right_cancel_semigroup A :=
   ⦃ right_cancel_semigroup, s,
     mul_right_cancel := @mul_right_cancel A s ⦄
 
@@ -388,12 +388,12 @@ section add_group
      ... = (c + b) + -b : H
      ... = c : add_neg_cancel_right
 
-  definition add_group.to_left_cancel_semigroup [instance] [coercion] :
+  definition add_group.to_left_cancel_semigroup [instance] [coercion] [reducible] :
     add_left_cancel_semigroup A :=
   ⦃ add_left_cancel_semigroup, s,
     add_left_cancel := @add_left_cancel A s ⦄
 
-  definition add_group.to_add_right_cancel_semigroup [instance] [coercion] :
+  definition add_group.to_add_right_cancel_semigroup [instance] [coercion] [reducible] :
     add_right_cancel_semigroup A :=
   ⦃ add_right_cancel_semigroup, s,
     add_right_cancel := @add_right_cancel A s ⦄

library/algebra/order.lean

@@ -157,7 +157,7 @@ section
       ne_ab eq_ab,
   show a < c, from lt_of_le_of_ne le_ac ne_ac
 
-  definition order_pair.to_strict_order [instance] [coercion] [s : order_pair A] : strict_order A :=
+  definition order_pair.to_strict_order [instance] [coercion] [reducible] [s : order_pair A] : strict_order A :=
   ⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
 
   theorem lt_of_lt_of_le : a < b → b ≤ c → a < c :=
@@ -242,7 +242,7 @@ iff.intro
       iff.mp !strict_order_with_le.le_iff_lt_or_eq (and.elim_left H),
     show a < b, from or_resolve_left H1 (and.elim_right H))
 
-definition strict_order_with_le.to_order_pair [instance] [coercion] [s : strict_order_with_le A] :
+definition strict_order_with_le.to_order_pair [instance] [coercion] [reducible] [s : strict_order_with_le A] :
   strong_order_pair A :=
 ⦃ strong_order_pair, s,
   le_refl      := le_refl s,
@@ -277,7 +277,7 @@ section
     (assume H, H1 H)
     (assume H, or.elim H (assume H', H2 H') (assume H', H3 H'))
 
-  definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion]
+  definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] [reducible]
      [s : linear_strong_order_pair A] : linear_order_pair A :=
   ⦃ linear_order_pair, s ⦄
 

library/algebra/ordered_group.lean

@@ -203,7 +203,7 @@ theorem ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b
 have H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
 !neg_add_cancel_left ▸ !neg_add_cancel_left ▸ H'
 
-definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion]
+definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible]
     [s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
 ⦃ ordered_cancel_comm_monoid, s,
   add_left_cancel       := @add.left_cancel A s,

library/algebra/ordered_ring.lean

@@ -154,7 +154,7 @@ have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
 have H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc,
 iff.mp !sub_pos_iff_lt (!mul_sub_right_distrib ▸ H2)
 
-definition ordered_ring.to_ordered_semiring [instance] [coercion] [s : ordered_ring A] :
+definition ordered_ring.to_ordered_semiring [instance] [coercion] [reducible] [s : ordered_ring A] :
   ordered_semiring A :=
 ⦃ ordered_semiring, s,
   mul_zero                   := mul_zero,
@@ -209,7 +209,7 @@ structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_
 
 -- print fields linear_ordered_semiring
 
-definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion]
+definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] [reducible]
     [s : linear_ordered_ring A] :
   linear_ordered_semiring A :=
 ⦃ linear_ordered_semiring, s,
@@ -245,7 +245,7 @@ lt.by_cases
         absurd (H ▸ show 0 < a * b, from mul_pos_of_neg_of_neg Ha Hb) (lt.irrefl 0)))
 
 -- Linearity implies no zero divisors. Doesn't need commutativity.
-definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion]
+definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion] [reducible]
     [s: linear_ordered_comm_ring A] : integral_domain A :=
 ⦃ integral_domain, s,
   eq_zero_or_eq_zero_of_mul_eq_zero :=
@@ -359,11 +359,11 @@ section
     (assume H1 : 0 < a,
       calc
         sign (-a) = -1        : sign_of_neg (neg_neg_of_pos H1)
-              ... = -(sign a) : {(sign_of_pos H1)⁻¹})
+              ... = -(sign a) : sign_of_pos H1)
     (assume H1 : 0 = a,
       calc
         sign (-a) = sign (-0) : H1
-              ... = sign 0    : {neg_zero} -- TODO: why do we need {}?
+              ... = sign 0    : neg_zero
               ... = 0         : sign_zero
               ... = -0        : neg_zero
               ... = -(sign 0) : sign_zero
@@ -372,7 +372,7 @@ section
       calc
         sign (-a) = 1         : sign_of_pos (neg_pos_of_neg H1)
               ... = -(-1)     : neg_neg
-              ... = -(sign a) : {(sign_of_neg H1)⁻¹})
+              ... = -(sign a) : sign_of_neg H1)
 
   -- hopefully, will be quick with the simplifier
   theorem sign_mul (a b : A) : sign (a * b) = sign a * sign b := sorry

library/algebra/ring.lean

@@ -166,7 +166,7 @@ have H : 0 * a + 0 = 0 * a + 0 * a, from calc
         ... = 0 * a + 0 * a : ring.right_distrib,
 show 0 * a = 0, from  (add.left_cancel H)⁻¹
 
-definition ring.to_semiring [instance] [coercion] [s : ring A] : semiring A :=
+definition ring.to_semiring [instance] [coercion] [reducible] [s : ring A] : semiring A :=
 ⦃ semiring, s,
   mul_zero := ring.mul_zero,
   zero_mul := ring.zero_mul ⦄
@@ -199,7 +199,7 @@ section
 
   theorem neg_eq_neg_one_mul : -a = -1 * a :=
   calc
-    -a = -(1 * a)  : one_mul a ▸ rfl
+    -a = -(1 * a)  : one_mul
       ... = -1 * a : neg_mul_eq_neg_mul
 
   theorem mul_sub_left_distrib : a * (b - c) = a * b - a * c :=
@@ -228,7 +228,7 @@ end
 
 structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
 
-definition comm_ring.to_comm_semiring [instance] [coercion] [s : comm_ring A] : comm_semiring A :=
+definition comm_ring.to_comm_semiring [instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A :=
 ⦃ comm_semiring, s,
   mul_zero := mul_zero,
   zero_mul := zero_mul ⦄