feat: Checking associativity in partial order (#1030)

Match leanprover-community/mathlib3#17942

Author: YaelDillies

Mathlib/Order/Basic.lean

@@ -428,6 +428,23 @@ theorem le_implies_le_of_le_of_le {a b c d : α} [Preorder α] (hca : c ≤ a) (
     a ≤ b → c ≤ d :=
   fun hab ↦ (hca.trans hab).trans hbd
 
+section PartialOrder
+variable [PartialOrder α]
+
+/-- 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 :=
+fun _ _ ↦ (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 :=
+fun a b c ↦ le_antisymm (assoc _ _ _) $ by rw [comm, comm b, comm _ c, comm a]; exact assoc _ _ _
+
+end PartialOrder
+
 @[ext]
 theorem Preorder.toLE_injective {α : Type _} : Function.Injective (@Preorder.toLE α) :=
   fun A B h ↦ match A, B with