From a14d76ebae3e2fe037adf512a7133fa4b5b6c160 Mon Sep 17 00:00:00 2001
From: FR-vdash-bot <zhao.yu-yang@foxmail.com>
Date: Fri, 3 Jan 2025 14:34:08 +0800
Subject: [PATCH] feat: mixin ordered algebraic typeclasses

---
 Mathlib/Algebra/Order/Monoid/Defs.lean | 92 ++++++++++++++++++++------
 Mathlib/Algebra/Order/Ring/Defs.lean   | 75 ++++++++++++++++-----
 2 files changed, 131 insertions(+), 36 deletions(-)

diff --git a/Mathlib/Algebra/Order/Monoid/Defs.lean b/Mathlib/Algebra/Order/Monoid/Defs.lean
index f5e69a42848e2..f43739eac5dda 100644
--- a/Mathlib/Algebra/Order/Monoid/Defs.lean
+++ b/Mathlib/Algebra/Order/Monoid/Defs.lean
@@ -17,6 +17,72 @@ open Function
 
 variable {α : Type*}
 
+-- TODO: use weaker typeclasses
+
+/-- An ordered (additive) monoid is a monoid with a order such that addition is monotone. -/
+class IsOrderedAddMonoid (α : Type*) [AddCommMonoid α] [PartialOrder α] where
+  protected add_le_add_left : ∀ a b : α, a ≤ b → ∀ c, c + a ≤ c + b
+  protected add_le_add_right : ∀ a b : α, a ≤ b → ∀ c, a + c ≤ b + c := fun a b h c ↦ by
+    rw [add_comm _ c, add_comm _ c]; exact add_le_add_left a b h c
+
+/-- An ordered monoid is a monoid with a order such that multiplication is monotone. -/
+@[to_additive]
+class IsOrderedMonoid (α : Type*) [CommMonoid α] [PartialOrder α] where
+  protected mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c, c * a ≤ c * b
+  protected mul_le_mul_right : ∀ a b : α, a ≤ b → ∀ c, a * c ≤ b * c := fun a b h c ↦ by
+    rw [mul_comm _ c, mul_comm _ c]; exact mul_le_mul_left a b h c
+
+section IsOrderedMonoid
+variable [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α]
+
+@[to_additive]
+instance IsOrderedMonoid.toMulLeftMono : MulLeftMono α where
+  elim := fun a _ _ bc ↦ IsOrderedMonoid.mul_le_mul_left _ _ bc a
+
+@[to_additive]
+instance IsOrderedMonoid.toMulRightMono : MulRightMono α where
+  elim := fun a _ _ bc ↦ IsOrderedMonoid.mul_le_mul_right _ _ bc a
+
+end IsOrderedMonoid
+
+/-- An ordered cancellative additive monoid is a ordered additive
+monoid in which addition is cancellative and monotone. -/
+class IsOrderedCancelAddMonoid (α : Type*) [AddCommMonoid α] [PartialOrder α] extends
+    IsOrderedAddMonoid α where
+  protected le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c
+  protected le_of_add_le_add_right : ∀ a b c : α, b + a ≤ c + a → b ≤ c := fun a b c h ↦ by
+    rw [add_comm _ a, add_comm _ a] at h; exact le_of_add_le_add_left a b c h
+
+/-- An ordered cancellative monoid is a ordered monoid in which
+multiplication is cancellative and monotone. -/
+@[to_additive IsOrderedCancelAddMonoid]
+class IsOrderedCancelMonoid (α : Type*) [CommMonoid α] [PartialOrder α] extends
+    IsOrderedMonoid α where
+  protected le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c
+  protected le_of_mul_le_mul_right : ∀ a b c : α, b * a ≤ c * a → b ≤ c := fun a b c h ↦ by
+    rw [mul_comm _ a, mul_comm _ a] at h; exact le_of_mul_le_mul_left a b c h
+
+section IsOrderedCancelMonoid
+variable [CommMonoid α] [PartialOrder α] [IsOrderedCancelMonoid α]
+
+-- See note [lower instance priority]
+@[to_additive]
+instance (priority := 200) IsOrderedCancelMonoid.toMulLeftReflectLE :
+    MulLeftReflectLE α :=
+  ⟨IsOrderedCancelMonoid.le_of_mul_le_mul_left⟩
+
+@[to_additive]
+instance IsOrderedCancelMonoid.toMulLeftReflectLT :
+    MulLeftReflectLT α where
+  elim := contravariant_lt_of_contravariant_le α α _ ContravariantClass.elim
+
+@[to_additive]
+theorem IsOrderedCancelMonoid.toMulRightReflectLT :
+    MulRightReflectLT α :=
+  inferInstance
+
+end IsOrderedCancelMonoid
+
 /-- An ordered (additive) commutative monoid is a commutative monoid with a partial order such that
 addition is monotone. -/
 class OrderedAddCommMonoid (α : Type*) extends AddCommMonoid α, PartialOrder α where
@@ -32,13 +98,8 @@ section OrderedCommMonoid
 variable [OrderedCommMonoid α]
 
 @[to_additive]
-instance OrderedCommMonoid.toMulLeftMono : MulLeftMono α where
-  elim := fun a _ _ bc ↦ OrderedCommMonoid.mul_le_mul_left _ _ bc a
-
-@[to_additive]
-theorem OrderedCommMonoid.toMulRightMono (M : Type*) [OrderedCommMonoid M] :
-    MulRightMono M :=
-  inferInstance
+instance OrderedCommMonoid.toIsOrderedMonoid : IsOrderedMonoid α where
+  mul_le_mul_left := OrderedCommMonoid.mul_le_mul_left
 
 end OrderedCommMonoid
 
@@ -56,21 +117,10 @@ class OrderedCancelCommMonoid (α : Type*) extends OrderedCommMonoid α where
 section OrderedCancelCommMonoid
 variable [OrderedCancelCommMonoid α]
 
--- See note [lower instance priority]
-@[to_additive]
-instance (priority := 200) OrderedCancelCommMonoid.toMulLeftReflectLE :
-    MulLeftReflectLE α :=
-  ⟨OrderedCancelCommMonoid.le_of_mul_le_mul_left⟩
-
 @[to_additive]
-instance OrderedCancelCommMonoid.toMulLeftReflectLT :
-    MulLeftReflectLT α where
-  elim := contravariant_lt_of_contravariant_le α α _ ContravariantClass.elim
-
-@[to_additive]
-theorem OrderedCancelCommMonoid.toMulRightReflectLT :
-    MulRightReflectLT α :=
-  inferInstance
+instance OrderedCancelCommMonoid.toIsOrderedCancelMonoid :
+    IsOrderedCancelMonoid α where
+  le_of_mul_le_mul_left := OrderedCancelCommMonoid.le_of_mul_le_mul_left
 
 -- See note [lower instance priority]
 @[to_additive OrderedCancelAddCommMonoid.toCancelAddCommMonoid]
diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean
index 6b1c7f820095d..637b87b45b4f8 100644
--- a/Mathlib/Algebra/Order/Ring/Defs.lean
+++ b/Mathlib/Algebra/Order/Ring/Defs.lean
@@ -109,6 +109,62 @@ universe u
 
 variable {α : Type u}
 
+-- TODO: use weaker typeclasses
+
+/-- An ordered semiring is a semiring with a order such that addition is monotone and
+multiplication by a nonnegative number is monotone. -/
+class IsOrderedRing (α : Type*) [Semiring α] [PartialOrder α] extends
+    IsOrderedAddMonoid α where
+  /-- `0 ≤ 1` in any ordered semiring. -/
+  protected zero_le_one : (0 : α) ≤ 1
+  /-- In an ordered semiring, we can multiply an inequality `a ≤ b` on the left
+  by a non-negative element `0 ≤ c` to obtain `c * a ≤ c * b`. -/
+  protected mul_le_mul_of_nonneg_left : ∀ a b c : α, a ≤ b → 0 ≤ c → c * a ≤ c * b
+  /-- In an ordered semiring, we can multiply an inequality `a ≤ b` on the right
+  by a non-negative element `0 ≤ c` to obtain `a * c ≤ b * c`. -/
+  protected mul_le_mul_of_nonneg_right : ∀ a b c : α, a ≤ b → 0 ≤ c → a * c ≤ b * c
+
+/-- A strict ordered semiring is a nontrivial semiring with a order such that addition is
+strictly monotone and multiplication by a positive number is strictly monotone. -/
+class IsStrictOrderedRing (α : Type*) [Semiring α] [PartialOrder α] extends
+    IsOrderedCancelAddMonoid α, Nontrivial α where
+  /-- In a strict ordered semiring, `0 ≤ 1`. -/
+  protected zero_le_one : (0 : α) ≤ 1
+  /-- Left multiplication by a positive element is strictly monotone. -/
+  protected mul_lt_mul_of_pos_left : ∀ a b c : α, a < b → 0 < c → c * a < c * b
+  /-- Right multiplication by a positive element is strictly monotone. -/
+  protected mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c
+
+section IsOrderedRing
+variable [Semiring α] [PartialOrder α] [IsOrderedRing α]
+
+-- see Note [lower instance priority]
+instance (priority := 100) IsOrderedRing.zeroLEOneClass : ZeroLEOneClass α :=
+  { ‹IsOrderedRing α› with }
+
+-- see Note [lower instance priority]
+instance (priority := 200) IsOrderedRing.toPosMulMono : PosMulMono α :=
+  ⟨fun x _ _ h => IsOrderedRing.mul_le_mul_of_nonneg_left _ _ _ h x.2⟩
+
+-- see Note [lower instance priority]
+instance (priority := 200) IsOrderedRing.toMulPosMono : MulPosMono α :=
+  ⟨fun x _ _ h => IsOrderedRing.mul_le_mul_of_nonneg_right _ _ _ h x.2⟩
+
+end IsOrderedRing
+
+section IsStrictOrderedRing
+variable [Semiring α] [PartialOrder α] [IsStrictOrderedRing α]
+
+-- see Note [lower instance priority]
+instance (priority := 200) IsStrictOrderedRing.toPosMulStrictMono : PosMulStrictMono α :=
+  ⟨fun x _ _ h => IsStrictOrderedRing.mul_lt_mul_of_pos_left _ _ _ h x.prop⟩
+
+-- see Note [lower instance priority]
+instance (priority := 200) IsStrictOrderedRing.toMulPosStrictMono : MulPosStrictMono α :=
+  ⟨fun x _ _ h => IsStrictOrderedRing.mul_lt_mul_of_pos_right _ _ _ h x.prop⟩
+
+end IsStrictOrderedRing
+
 /-! Note that `OrderDual` does not satisfy any of the ordered ring typeclasses due to the
 `zero_le_one` field. -/
 
@@ -194,17 +250,10 @@ class LinearOrderedCommRing (α : Type u) extends LinearOrderedRing α, CommMono
 section OrderedSemiring
 
 variable [OrderedSemiring α]
--- see Note [lower instance priority]
-instance (priority := 100) OrderedSemiring.zeroLEOneClass : ZeroLEOneClass α :=
-  { ‹OrderedSemiring α› with }
 
 -- see Note [lower instance priority]
-instance (priority := 200) OrderedSemiring.toPosMulMono : PosMulMono α :=
-  ⟨fun x _ _ h => OrderedSemiring.mul_le_mul_of_nonneg_left _ _ _ h x.2⟩
-
--- see Note [lower instance priority]
-instance (priority := 200) OrderedSemiring.toMulPosMono : MulPosMono α :=
-  ⟨fun x _ _ h => OrderedSemiring.mul_le_mul_of_nonneg_right _ _ _ h x.2⟩
+instance OrderedSemiring.toIsOrderedRing : IsOrderedRing α :=
+  { ‹OrderedSemiring α› with }
 
 end OrderedSemiring
 
@@ -253,12 +302,8 @@ section StrictOrderedSemiring
 variable [StrictOrderedSemiring α]
 
 -- see Note [lower instance priority]
-instance (priority := 200) StrictOrderedSemiring.toPosMulStrictMono : PosMulStrictMono α :=
-  ⟨fun x _ _ h => StrictOrderedSemiring.mul_lt_mul_of_pos_left _ _ _ h x.prop⟩
-
--- see Note [lower instance priority]
-instance (priority := 200) StrictOrderedSemiring.toMulPosStrictMono : MulPosStrictMono α :=
-  ⟨fun x _ _ h => StrictOrderedSemiring.mul_lt_mul_of_pos_right _ _ _ h x.prop⟩
+instance StrictOrderedSemiring.toIsStrictOrderedRing : IsStrictOrderedRing α :=
+  { ‹StrictOrderedSemiring α› with }
 
 -- See note [reducible non-instances]
 /-- A choice-free version of `StrictOrderedSemiring.toOrderedSemiring` to avoid using choice in