feat(Order/WellFoundedSet): minimal element of a nonempty set exists if < is well founded on the set (leanprover-community#39777)

There exists a inimal element in a nonempty set if `<` is well founded on the set.

Author: Hagb

Mathlib/Order/WellFoundedSet.lean

@@ -559,6 +559,12 @@ lemma WellFoundedOn.mapsTo {α β : Type*} {r : α → α → Prop} (f : β →
     t.WellFoundedOn (r on f) := by
   exact InvImage.wf (fun x : t ↦ ⟨f x, h x.prop⟩) hw
 
+@[to_dual]
+theorem WellFoundedOn.exists_minimal {α : Type*} [Preorder α] {s : Set α}
+    (h : s.WellFoundedOn (· < ·)) (nonempty : s.Nonempty) : ∃ a, Minimal (· ∈ s) a :=
+  have ⟨m, hm⟩ := WellFoundedLT.exists_minimal ⟨h⟩ univ <| nonempty.elim (⟨⟨·, ·⟩, trivial⟩)
+  ⟨m, m.property, fun y hy ↦ hm.right (y := ⟨y, hy⟩) trivial⟩
+
 end WellFoundedOn
 
 section LinearOrder