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

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

theorem Finset.exists_minimal_dec {α : Type u_1} [PartialOrder α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 < x2] (T : Finset α) (hne : T.Nonempty) : ∃ x ∈ T, ∀ y ∈ T, ¬y < x

Constructive: every nonempty finite subset of a decidable strict order has a minimal element (no well-foundedness needed).