From ebc18780283e15a95d1f9affba4021ae71b4d2d7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Jan 2015 17:23:41 -0800
Subject: [PATCH] refactor(library/algebra/group): using new structure instance
 syntax sugar to define instances

---
 library/algebra/group.lean | 28 ++++++++++++++++------------
 1 file changed, 16 insertions(+), 12 deletions(-)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index bf1e19637..3426a3f08 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -252,22 +252,24 @@ section group
   iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv
 
   definition group.to_left_cancel_semigroup [instance] [coercion] : left_cancel_semigroup A :=
-  left_cancel_semigroup.mk (@group.mul A s) (@group.mul_assoc A s)
-    (take a b c,
+  ⦃ left_cancel_semigroup,
+    mul_left_cancel := take a b c,
       assume H : a * b = a * c,
       calc
         b = a⁻¹ * (a * b) : inv_mul_cancel_left
           ... = a⁻¹ * (a * c) : H
-          ... = c : inv_mul_cancel_left)
+          ... = c : inv_mul_cancel_left,
+    using s ⦄
 
   definition group.to_right_cancel_semigroup [instance] [coercion] : right_cancel_semigroup A :=
-  right_cancel_semigroup.mk (@group.mul A s) (@group.mul_assoc A s)
-    (take a b c,
+  ⦃ right_cancel_semigroup,
+    mul_right_cancel := take a b c,
       assume H : a * b = c * b,
       calc
         a = (a * b) * b⁻¹ : mul_inv_cancel_right
           ... = (c * b) * b⁻¹ : H
-          ... = c : mul_inv_cancel_right)
+          ... = c : mul_inv_cancel_right,
+    using s ⦄
 
 end group
 
@@ -380,23 +382,25 @@ section add_group
 
   definition add_group.to_left_cancel_semigroup [instance] [coercion] :
     add_left_cancel_semigroup A :=
-  add_left_cancel_semigroup.mk add_group.add add_group.add_assoc
-    (take a b c,
+  ⦃ add_left_cancel_semigroup,
+    add_left_cancel := take a b c,
       assume H : a + b = a + c,
       calc
         b = -a + (a + b) : !neg_add_cancel_left⁻¹
           ... = -a + (a + c) : H
-          ... = c : neg_add_cancel_left)
+          ... = c : neg_add_cancel_left,
+    using s ⦄
 
   definition add_group.to_add_right_cancel_semigroup [instance] [coercion] :
     add_right_cancel_semigroup A :=
-  add_right_cancel_semigroup.mk add_group.add add_group.add_assoc
-    (take a b c,
+  ⦃ add_right_cancel_semigroup,
+    add_right_cancel := take a b c,
       assume H : a + b = c + b,
       calc
         a = (a + b) + -b : !add_neg_cancel_right⁻¹
           ... = (c + b) + -b : H
-          ... = c : add_neg_cancel_right)
+          ... = c : add_neg_cancel_right,
+    using s ⦄
 
   /- sub -/