feat(Order/WellFoundedSet): sufficient conditions for unique minima of well-founded sets (#18977)

This PR adds two results about minima in well-founded sets.  For preorders, if an element is strictly smaller than all others, then it is equal to the minimum.  For partial orders, if an element is less than or equal to all elements, then it is equal to the minimum.  We add an application to the support of Hahn series.

Author: ScottCarnahan

Mathlib/Order/WellFoundedSet.lean

@@ -594,8 +594,25 @@ theorem isWF_min_singleton (a) {hs : IsWF ({a} : Set α)} {hn : ({a} : Set α).N
     hs.min hn = a :=
   eq_of_mem_singleton (IsWF.min_mem hs hn)
 
+theorem IsWF.min_eq_of_lt (hs : s.IsWF) (ha : a ∈ s) (hlt : ∀ b ∈ s, b ≠ a → a < b) :
+    hs.min (nonempty_of_mem ha) = a := by
+  by_contra h
+  exact (hs.not_lt_min (nonempty_of_mem ha) ha) (hlt (hs.min (nonempty_of_mem ha))
+    (hs.min_mem (nonempty_of_mem ha)) h)
+
 end Preorder
 
+section PartialOrder
+
+variable [PartialOrder α] {s : Set α} {a : α}
+
+theorem IsWF.min_eq_of_le (hs : s.IsWF) (ha : a ∈ s) (hle : ∀ b ∈ s, a ≤ b) :
+    hs.min (nonempty_of_mem ha) = a :=
+  (eq_of_le_of_not_lt (hle (hs.min (nonempty_of_mem ha))
+    (hs.min_mem (nonempty_of_mem ha))) (hs.not_lt_min (nonempty_of_mem ha) ha)).symm
+
+end PartialOrder
+
 section LinearOrder
 
 variable [LinearOrder α] {s t : Set α} {a : α}

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -248,6 +248,11 @@ theorem orderTop_eq_top_iff {x : HahnSeries Γ R} : orderTop x = ⊤ ↔ x = 0 :
     exact ne_zero_iff_orderTop.mp
   · simp_all only [orderTop_zero, implies_true]
 
+theorem orderTop_eq_of_le {x : HahnSeries Γ R} {g : Γ} (hg : g ∈ x.support)
+    (hx : ∀ g' ∈ x.support, g ≤ g') : orderTop x = g := by
+  rw [orderTop_of_ne <| support_nonempty_iff.mp <| Set.nonempty_of_mem hg,
+    x.isWF_support.min_eq_of_le hg hx]
+
 theorem untop_orderTop_of_ne_zero {x : HahnSeries Γ R} (hx : x ≠ 0) :
     WithTop.untop x.orderTop (ne_zero_iff_orderTop.mp hx) =
       x.isWF_support.min (support_nonempty_iff.2 hx) :=