diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean
index e454a686884a8d..62b5383d8a0248 100644
--- a/Mathlib/Order/WellFoundedSet.lean
+++ b/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