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

Author: hawkrobe

Mathlib/Order/Antisymmetrization.lean

@@ -442,6 +442,51 @@ theorem AntisymmRel.symmGen_congr_right (h : AntisymmRel (· ≤ ·) b c) :
 
 end SymmGen
 
+section Minimal
+
+open Relation
+
+variable {P : α → Prop}
+
+section Preorder
+
+variable [Preorder α]
+
+-- TODO: `to_dual` doesn't work with `AntisymmRel` or `SymmGen`.
+theorem Minimal.antisymmRel_of_ge (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 (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 (ha : Minimal P a) (hb : Minimal P b)
+    (hab : 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 (ha : Maximal P a) (hb : Maximal P b)
+    (hab : SymmGen (· ≤ ·) a b) : AntisymmRel (· ≤ ·) a b :=
+  hab.elim (ha.antisymmRel_of_le hb.prop) (fun h ↦ (hb.antisymmRel_of_le ha.prop h).symm)
+
+end Preorder
+
+section PartialOrder
+
+variable [PartialOrder α]
+
+theorem Minimal.eq_of_symmGen (ha : Minimal P a) (hb : Minimal P b)
+    (hab : SymmGen (· ≤ ·) a b) : a = b :=
+  (ha.antisymmRel_of_symmGen hb hab).eq
+
+theorem Maximal.eq_of_symmGen (ha : Maximal P a) (hb : Maximal P b)
+    (hab : SymmGen (· ≤ ·) a b) : a = b :=
+  (ha.antisymmRel_of_symmGen hb hab).eq
+
+end PartialOrder
+
+end Minimal
+
 section Prod
 
 variable (α β) [Preorder α] [Preorder β]