theorem Finset.exists_minimal_of_nonempty {α : Type u_1} [PartialOrder α] [WellFoundedLT α] (T : Finset α) (hne : T.Nonempty) : ∃ x ∈ T, ∀ y ∈ T, y < x → False

A non-empty finite subset of a well-founded partial order has a minimal element.