refactor(algebra/order/group): unify instances (#14705)

Drop `group.covariant_class_le.to_contravariant_class_le` etc in favor
of `group.covconv` (now an instance) and a new similar instance
`group.covconv_swap`.

Author: urkud

src/algebra/covariant_and_contravariant.lean

@@ -142,11 +142,27 @@ begin
     exact h a⁻¹ bc }
 end
 
-@[to_additive]
-lemma group.covconv [group N] [covariant_class N N (*) r] :
+@[priority 100, to_additive]
+instance group.covconv [group N] [covariant_class N N (*) r] :
   contravariant_class N N (*) r :=
 ⟨group.covariant_iff_contravariant.mp covariant_class.elim⟩
 
+@[to_additive]
+lemma group.covariant_swap_iff_contravariant_swap [group N] :
+  covariant N N (swap (*)) r ↔ contravariant N N (swap (*)) r :=
+begin
+  refine ⟨λ h a b c bc, _, λ h a b c bc, _⟩,
+  { rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a],
+    exact h a⁻¹ bc },
+  { rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc,
+    exact h a⁻¹ bc }
+end
+
+@[priority 100, to_additive]
+instance group.covconv_swap [group N] [covariant_class N N (swap (*)) r] :
+  contravariant_class N N (swap (*)) r :=
+⟨group.covariant_swap_iff_contravariant_swap.mp covariant_class.elim⟩
+
 section is_trans
 variables [is_trans N r] (m n : M) {a b c d : N}
 

src/algebra/order/group.lean

@@ -24,32 +24,6 @@ open function
 universe u
 variable {α : Type u}
 
-@[to_additive]
-instance group.covariant_class_le.to_contravariant_class_le
-  [group α] [has_le α] [covariant_class α α (*) (≤)] : contravariant_class α α (*) (≤) :=
-group.covconv
-
-@[to_additive]
-instance group.swap.covariant_class_le.to_contravariant_class_le [group α] [has_le α]
-  [covariant_class α α (swap (*)) (≤)] : contravariant_class α α (swap (*)) (≤) :=
-{ elim := λ a b c bc, calc  b = b * a * a⁻¹ : eq_mul_inv_of_mul_eq rfl
-                          ... ≤ c * a * a⁻¹ : mul_le_mul_right' bc a⁻¹
-                          ... = c           : mul_inv_eq_of_eq_mul rfl }
-
-@[to_additive]
-instance group.covariant_class_lt.to_contravariant_class_lt
-  [group α] [has_lt α] [covariant_class α α (*) (<)] : contravariant_class α α (*) (<) :=
-{ elim := λ a b c bc, calc  b = a⁻¹ * (a * b) : eq_inv_mul_of_mul_eq rfl
-                          ... < a⁻¹ * (a * c) : mul_lt_mul_left' bc a⁻¹
-                          ... = c             : inv_mul_cancel_left a c }
-
-@[to_additive]
-instance group.swap.covariant_class_lt.to_contravariant_class_lt [group α] [has_lt α]
-  [covariant_class α α (swap (*)) (<)] : contravariant_class α α (swap (*)) (<) :=
-{ elim := λ a b c bc, calc  b = b * a * a⁻¹ : eq_mul_inv_of_mul_eq rfl
-                          ... < c * a * a⁻¹ : mul_lt_mul_right' bc a⁻¹
-                          ... = c           : mul_inv_eq_of_eq_mul rfl }
-
 /-- An ordered additive commutative group is an additive commutative group
 with a partial order in which addition is strictly monotone. -/
 @[protect_proj, ancestor add_comm_group partial_order]