∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs : List α}
  {f : α → β} (h : xs ≠ []), (∀ x ∈ xs, f (xs.head h) ≤ f x) → List.minOn f xs h = xs.head h