feat(Order/Antisymmetrization): comparable minimal elements are equivalent

Author: hawkrobe

Mathlib/Order/Antisymmetrization.lean

@@ -442,6 +442,31 @@ theorem AntisymmRel.symmGen_congr_right (h : AntisymmRel (· ≤ ·) b c) :
 
 end SymmGen
 
+-- TODO: `to_dual` doesn't work with `AntisymmRel` or `SymmGen`.
+theorem Minimal.antisymmRel_of_ge [Preorder α] {P : α → Prop} (ha : Minimal P a) (hb : P b)
+    (hge : b ≤ a) : AntisymmRel (· ≤ ·) a b :=
+  ⟨ha.le_of_le hb hge, hge⟩
+
+theorem Maximal.antisymmRel_of_le [Preorder α] {P : α → Prop} (ha : Maximal P a) (hb : P b)
+    (hle : a ≤ b) : AntisymmRel (· ≤ ·) a b :=
+  ⟨hle, ha.le_of_ge hb hle⟩
+
+theorem Minimal.antisymmRel_of_symmGen [Preorder α] {P : α → Prop} (ha : Minimal P a)
+    (hb : Minimal P b) (hab : Relation.SymmGen (· ≤ ·) a b) : AntisymmRel (· ≤ ·) a b :=
+  hab.elim (fun h ↦ (hb.antisymmRel_of_ge ha.prop h).symm) (ha.antisymmRel_of_ge hb.prop)
+
+theorem Maximal.antisymmRel_of_symmGen [Preorder α] {P : α → Prop} (ha : Maximal P a)
+    (hb : Maximal P b) (hab : Relation.SymmGen (· ≤ ·) a b) : AntisymmRel (· ≤ ·) a b :=
+  hab.elim (ha.antisymmRel_of_le hb.prop) (fun h ↦ (hb.antisymmRel_of_le ha.prop h).symm)
+
+theorem Minimal.eq_of_symmGen [PartialOrder α] {P : α → Prop} (ha : Minimal P a)
+    (hb : Minimal P b) (hab : Relation.SymmGen (· ≤ ·) a b) : a = b :=
+  (ha.antisymmRel_of_symmGen hb hab).eq
+
+theorem Maximal.eq_of_symmGen [PartialOrder α] {P : α → Prop} (ha : Maximal P a)
+    (hb : Maximal P b) (hab : Relation.SymmGen (· ≤ ·) a b) : a = b :=
+  (ha.antisymmRel_of_symmGen hb hab).eq
+
 section Prod
 
 variable (α β) [Preorder α] [Preorder β]