From 10216790bc1a74f4abe44140a4bf6eb8dd0ba362 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 3 Aug 2021 07:45:29 +0000
Subject: [PATCH] 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 | 20 ++++++--
 src/algebra/ordered_group.lean               |  4 +-
 src/algebra/ordered_monoid.lean              | 49 ++++++++++++++++++--
 3 files changed, 63 insertions(+), 10 deletions(-)

diff --git a/src/algebra/covariant_and_contravariant.lean b/src/algebra/covariant_and_contravariant.lean
index 4950767b54fc8..f91a20e872251 100644
--- a/src/algebra/covariant_and_contravariant.lean
+++ b/src/algebra/covariant_and_contravariant.lean
@@ -108,6 +108,18 @@ 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]
 
@@ -115,6 +127,7 @@ 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}
diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean
index 7b9ce868d27e7..128411cff461a 100644
--- a/src/algebra/ordered_group.lean
+++ b/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 α]
diff --git a/src/algebra/ordered_monoid.lean b/src/algebra/ordered_monoid.lean
index 94d1567cd0a1f..979641527210a 100644
--- a/src/algebra/ordered_monoid.lean
+++ b/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 α] :