Minimal elements of well-founded images

Set.IsWF.exists_minimalFor, the well-founded companion of mathlib's Set.IsPWO.exists_minimalFor: if the image of a nonempty set under f is well-founded, some element of the set is minimal for f.

theorem Set.IsWF.exists_minimalFor {ι : Type u_1} {β : Type u_2} [Preorder β] (f : ι → β) (s : Set ι) (h : (f '' s).IsWF) (hs : s.Nonempty) : ∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i