feat(order/basic): Checking associativity in partial order (#17942)

Simpler conditions to check commutativity/associativity of a function valued in a partial order.

src/order/basic.lean

@@ -378,6 +378,23 @@ lemma le_implies_le_of_le_of_le {a b c d : α} [preorder α] (hca : c ≤ a) (hb
   a ≤ b → c ≤ d :=
 λ hab, (hca.trans hab).trans hbd
 
+section partial_order
+variables [partial_order α]
+
+/-- To prove commutativity of a binary operation `○`, we only to check `a ○ b ≤ b ○ a` for all `a`,
+`b`. -/
+lemma commutative_of_le {f : β → β → α} (comm : ∀ a b, f a b ≤ f b a) : ∀ a b, f a b = f b a :=
+λ a b, (comm _ _).antisymm $ comm _ _
+
+/-- To prove associativity of a commutative binary operation `○`, we only to check
+`(a ○ b) ○ c ≤ a ○ (b ○ c)` for all `a`, `b`, `c`. -/
+lemma associative_of_commutative_of_le {f : α → α → α} (comm : commutative f)
+  (assoc : ∀ a b c, f (f a b) c ≤ f a (f b c)) :
+  associative f :=
+λ a b c, le_antisymm (assoc _ _ _) $ by { rw [comm, comm b, comm _ c, comm a], exact assoc _ _ _ }
+
+end partial_order
+
 @[ext]
 lemma preorder.to_has_le_injective {α : Type*} :
   function.injective (@preorder.to_has_le α) :=