feat(algebra/ordered_monoid): a few more order_dual instances (#8519)

* add `covariant.flip` and `contravariant.flip`;
* add `[to_additive]` to `group.covariant_iff_contravariant` and
  `covconv` (renamed to `group.covconv`);
* use `group.covconv` in
  `group.covariant_class_le.to_contravariant_class_le`;
* add some `order_dual` instances for `covariant_class` and
  `contravariant_class`;
* golf `order_dual.ordered_comm_monoid`.

src/algebra/covariant_and_contravariant.lean

@@ -108,13 +108,26 @@ lemma rel_iff_cov [covariant_class M N μ r] [contravariant_class M N μ r] (m :
   r (μ m a) (μ m b) ↔ r a b :=
 ⟨contravariant_class.elim _, covariant_class.elim _⟩
 
+section flip
+
+variables {M N μ r}
+
+lemma covariant.flip (h : covariant M N μ r) : covariant M N μ (flip r) :=
+λ a b c hbc, h a hbc
+
+lemma contravariant.flip (h : contravariant M N μ r) : contravariant M N μ (flip r) :=
+λ a b c hbc, h a hbc
+
+end flip
+
 section covariant
 variables {M N μ r} [covariant_class M N μ r]
 
 lemma act_rel_act_of_rel (m : M) {a b : N} (ab : r a b) :
   r (μ m a) (μ m b) :=
 covariant_class.elim _ ab
 
+@[to_additive]
 lemma group.covariant_iff_contravariant [group N] :
   covariant N N (*) r ↔ contravariant N N (*) r :=
 begin
@@ -125,9 +138,10 @@ begin
     exact h a⁻¹ bc }
 end
 
-lemma covconv [group N] [cov : covariant_class N N (*) r] : contravariant_class N N (*) r :=
-{ elim := λ a b c bc, group.covariant_iff_contravariant.mp cov.elim _ bc }
-
+@[to_additive]
+lemma group.covconv [group N] [covariant_class N N (*) r] :
+  contravariant_class N N (*) r :=
+⟨group.covariant_iff_contravariant.mp covariant_class.elim⟩
 
 section is_trans
 variables [is_trans N r] (m n : M) {a b c d : N}

src/algebra/ordered_group.lean

@@ -27,9 +27,7 @@ variable {α : Type u}
 @[to_additive]
 instance group.covariant_class_le.to_contravariant_class_le
   [group α] [has_le α] [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_le_mul_left' bc a⁻¹
-                          ... = c             : inv_mul_cancel_left a c }
+group.covconv
 
 @[to_additive]
 instance group.swap.covariant_class_le.to_contravariant_class_le [group α] [has_le α]

src/algebra/ordered_monoid.lean

@@ -838,13 +838,54 @@ namespace order_dual
 @[to_additive]
 instance [h : has_mul α] : has_mul (order_dual α) := h
 
+@[to_additive]
+instance contravariant_class_mul_le [has_le α] [has_mul α] [c : contravariant_class α α (*) (≤)] :
+  contravariant_class (order_dual α) (order_dual α) (*) (≤) :=
+⟨c.1.flip⟩
+
+@[to_additive]
+instance covariant_class_mul_le [has_le α] [has_mul α] [c : covariant_class α α (*) (≤)] :
+  covariant_class (order_dual α) (order_dual α) (*) (≤) :=
+⟨c.1.flip⟩
+
+@[to_additive] instance contravariant_class_swap_mul_le [has_le α] [has_mul α]
+  [c : contravariant_class α α (function.swap (*)) (≤)] :
+  contravariant_class (order_dual α) (order_dual α) (function.swap (*)) (≤) :=
+⟨c.1.flip⟩
+
+@[to_additive]
+instance covariant_class_swap_mul_le [has_le α] [has_mul α]
+  [c : covariant_class α α (function.swap (*)) (≤)] :
+  covariant_class (order_dual α) (order_dual α) (function.swap (*)) (≤) :=
+⟨c.1.flip⟩
+
+@[to_additive]
+instance contravariant_class_mul_lt [has_lt α] [has_mul α] [c : contravariant_class α α (*) (<)] :
+  contravariant_class (order_dual α) (order_dual α) (*) (<) :=
+⟨c.1.flip⟩
+
+@[to_additive]
+instance covariant_class_mul_lt [has_lt α] [has_mul α] [c : covariant_class α α (*) (<)] :
+  covariant_class (order_dual α) (order_dual α) (*) (<) :=
+⟨c.1.flip⟩
+
+@[to_additive] instance contravariant_class_swap_mul_lt [has_lt α] [has_mul α]
+  [c : contravariant_class α α (function.swap (*)) (<)] :
+  contravariant_class (order_dual α) (order_dual α) (function.swap (*)) (<) :=
+⟨c.1.flip⟩
+
+@[to_additive]
+instance covariant_class_swap_mul_lt [has_lt α] [has_mul α]
+  [c : covariant_class α α (function.swap (*)) (<)] :
+  covariant_class (order_dual α) (order_dual α) (function.swap (*)) (<) :=
+⟨c.1.flip⟩
+
 @[to_additive]
 instance [ordered_comm_monoid α] : ordered_comm_monoid (order_dual α) :=
-{ mul_le_mul_left := λ a b h c, show (id c : α) * b ≤ c * a, from mul_le_mul_left' h _,
-  lt_of_mul_lt_mul_left := λ a b c h, by
-    apply lt_of_mul_lt_mul_left' (by convert h : (id a : α) * c < a * b),
+{ mul_le_mul_left := λ a b h c, mul_le_mul_left' h c,
+  lt_of_mul_lt_mul_left := λ a b c, lt_of_mul_lt_mul_left',
   ..order_dual.partial_order α,
-  ..show comm_monoid α, by apply_instance }
+  ..(infer_instance : comm_monoid α) }
 
 @[to_additive ordered_cancel_add_comm_monoid.to_contravariant_class]
 instance ordered_cancel_comm_monoid.to_contravariant_class [ordered_cancel_comm_monoid α] :