∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : LT β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : ℕ} (hi : i < xs.length),
  (∀ (j : ℕ) (x : j < i), f xs[i] < f xs[j]) → i ≤ List.minIdxOn f xs h