@[inline]

def List.minIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] (f : α → β) (xs : List α) (h : xs ≠ []) : Nat

Returns the index of an element of the non-empty list xs that minimizes f. If x, y are such that f x = f y, it returns the index of whichever comes first in the list.

The correctness of this function assumes β to be linearly pre-ordered.

Equations

• List.minIdxOn f (y :: ys) h_2 = List.minIdxOn.go✝ f y 0 1 ys

@[inline]

def List.minIdxOn? {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] (f : α → β) (xs : List α) : Option Nat

Returns the index of an element of xs that minimizes f. If x, y are such that f x = f y, it returns the index of whichever comes first in the list. Returns none if the list is empty.

The correctness of this function assumes β to be linearly pre-ordered.

Equations

• List.minIdxOn? f [] = none
• List.minIdxOn? f (y :: ys) = some (List.minIdxOn f (y :: ys) ⋯)

@[inline]

def List.maxIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] (f : α → β) (xs : List α) (h : xs ≠ []) : Nat

Returns the index of an element of the non-empty list xs that maximizes f. If x, y are such that f x = f y, it returns the index of whichever comes first in the list.

The correctness of this function assumes β to be linearly pre-ordered.

Equations

• List.maxIdxOn f xs h = List.minIdxOn f xs h

@[inline]

def List.maxIdxOn? {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] (f : α → β) (xs : List α) : Option Nat

Returns the index of an element of xs that maximizes f. If x, y are such that f x = f y, it returns the index of whichever comes first in the list. Returns none if the list is empty.

The correctness of this function assumes β to be linearly pre-ordered.

Equations

• List.maxIdxOn? f xs = List.minIdxOn? f xs

theorem List.maxIdxOn_eq_minIdxOn {β : Type u_1} {α : Type u_2} {le : LE β} {x✝ : DecidableLE β} {f : α → β} {xs : List α} {h : xs ≠ []} : maxIdxOn f xs h = minIdxOn f xs h

@[simp]

theorem List.minIdxOn_nil_eq_iff_true {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {x : Nat} (h : [] ≠ []) : minIdxOn f [] h = x ↔ True

theorem List.minIdxOn_nil_eq_iff_false {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {x : Nat} (h : [] ≠ []) : minIdxOn f [] h = x ↔ False

@[simp]

theorem List.minIdxOn_singleton {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {x : α} {f : α → β} : minIdxOn f [x] ⋯ = 0

@[simp]

theorem List.minIdxOn_lt_length {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []) : minIdxOn f xs h < xs.length

theorem List.minIdxOn_le_of_apply_getElem_le_apply_minOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} (h : xs ≠ []) {k : Nat} (hi : k < xs.length) (hle : f xs[k] ≤ f (List.minOn f xs h)) : minIdxOn f xs h ≤ k

theorem List.apply_minOn_lt_apply_getElem_of_lt_minIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {k : Nat} (hk : k < minIdxOn f xs h) : f (List.minOn f xs h) < f xs[k]

@[simp]

theorem List.getElem_minIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} (h : xs ≠ []) : xs[minIdxOn f xs h] = List.minOn f xs h

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

theorem List.minIdxOn_le_of_apply_getElem_le_apply_getElem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : Nat} (hi : i < xs.length) (hi' : ∀ (j : Nat) (x : j < xs.length), f xs[i] ≤ f xs[j]) : minIdxOn f xs h ≤ i

theorem List.minIdxOn_eq_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : Nat} : minIdxOn f xs h = i ↔ ∃ (h : i < xs.length), (∀ (j : Nat) (x : j < xs.length), f xs[i] ≤ f xs[j]) ∧ ∀ (j : Nat) (x : j < i), f xs[i] < f xs[j]

theorem List.minIdxOn_eq_iff_eq_minOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : Nat} : minIdxOn f xs h = i ↔ ∃ (hi : i < xs.length), xs[i] = List.minOn f xs h ∧ ∀ (j : Nat) (hj : j < i), f (List.minOn f xs h) < f xs[j]

theorem List.minIdxOn_cons {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α} {f : α → β} : minIdxOn f (x :: xs) ⋯ = if h : xs = [] then 0 else if f x ≤ f (List.minOn f xs h) then 0 else minIdxOn f xs h + 1

theorem List.minIdxOn_eq_zero_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} (h : xs ≠ []) : minIdxOn f xs h = 0 ↔ ∀ (x : α), x ∈ xs → f (xs.head h) ≤ f x

The proof of List.minOn_append uses associativity of minOn and applies foldl_assoc. The proof of minIdxOn_append is analogous, but the aggregation operation, combineMinIdxOn, depends on the length of the lists to combine. After proving associativity of the aggregation operation, the proof closely follows the proof of foldl_assoc.

theorem List.minIdxOn_append {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α} {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) : minIdxOn f (xs ++ ys) ⋯ = if f (List.minOn f xs hxs) ≤ f (List.minOn f ys hys) then minIdxOn f xs hxs else xs.length + minIdxOn f ys hys

theorem List.left_le_minIdxOn_append {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α} {f : α → β} (h : xs ≠ []) : minIdxOn f xs h ≤ minIdxOn f (xs ++ ys) ⋯

theorem List.minIdxOn_take_le {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {i : Nat} (h : take i xs ≠ []) : minIdxOn f (take i xs) h ≤ minIdxOn f xs ⋯

@[simp]

theorem List.minIdxOn_replicate {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.Refl fun (x1 x2 : β) => x1 ≤ x2] {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) : minIdxOn f (replicate n a) h = 0

@[simp]

theorem List.maxIdxOn_nil_eq_iff_true {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {x : Nat} (h : [] ≠ []) : maxIdxOn f [] h = x ↔ True

theorem List.maxIdxOn_nil_eq_iff_false {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {x : Nat} (h : [] ≠ []) : maxIdxOn f [] h = x ↔ False

@[simp]

theorem List.maxIdxOn_singleton {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {x : α} {f : α → β} : maxIdxOn f [x] ⋯ = 0

@[simp]

theorem List.maxIdxOn_lt_length {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []) : maxIdxOn f xs h < xs.length

theorem List.maxIdxOn_le_of_apply_getElem_le_apply_maxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} (h : xs ≠ []) {k : Nat} (hi : k < xs.length) (hle : f (List.maxOn f xs h) ≤ f xs[k]) : maxIdxOn f xs h ≤ k

theorem List.apply_maxOn_lt_apply_getElem_of_lt_maxIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {k : Nat} (hk : k < maxIdxOn f xs h) : f xs[k] < f (List.maxOn f xs h)

@[simp]

theorem List.getElem_maxIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} (h : xs ≠ []) : xs[maxIdxOn f xs h] = List.maxOn f xs h

theorem List.le_maxIdxOn_of_apply_getElem_lt_apply_getElem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : Nat} (hi : i < xs.length) (hi' : ∀ (j : Nat) (x : j < i), f xs[j] < f xs[i]) : i ≤ maxIdxOn f xs h

theorem List.maxIdxOn_le_of_apply_getElem_le_apply_getElem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : Nat} (hi : i < xs.length) (hi' : ∀ (j : Nat) (x : j < xs.length), f xs[j] ≤ f xs[i]) : maxIdxOn f xs h ≤ i

theorem List.maxIdxOn_eq_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : Nat} : maxIdxOn f xs h = i ↔ ∃ (h : i < xs.length), (∀ (j : Nat) (x : j < xs.length), f xs[j] ≤ f xs[i]) ∧ ∀ (j : Nat) (x : j < i), f xs[j] < f xs[i]

theorem List.maxIdxOn_eq_iff_eq_maxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {f : α → β} {xs : List α} (h : xs ≠ []) {i : Nat} : maxIdxOn f xs h = i ↔ ∃ (hi : i < xs.length), xs[i] = List.maxOn f xs h ∧ ∀ (j : Nat) (hj : j < i), f xs[j] < f (List.maxOn f xs h)

theorem List.maxIdxOn_cons {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {x : α} {xs : List α} {f : α → β} : maxIdxOn f (x :: xs) ⋯ = if h : xs = [] then 0 else if f (List.maxOn f xs h) ≤ f x then 0 else maxIdxOn f xs h + 1

theorem List.maxIdxOn_eq_zero_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} (h : xs ≠ []) : maxIdxOn f xs h = 0 ↔ ∀ (x : α), x ∈ xs → f x ≤ f (xs.head h)

theorem List.maxIdxOn_append {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α} {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) : maxIdxOn f (xs ++ ys) ⋯ = if f (List.maxOn f ys hys) ≤ f (List.maxOn f xs hxs) then maxIdxOn f xs hxs else xs.length + maxIdxOn f ys hys

theorem List.left_le_maxIdxOn_append {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α} {f : α → β} (h : xs ≠ []) : maxIdxOn f xs h ≤ maxIdxOn f (xs ++ ys) ⋯

theorem List.maxIdxOn_take_le {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {i : Nat} (h : take i xs ≠ []) : maxIdxOn f (take i xs) h ≤ maxIdxOn f xs ⋯

@[simp]

theorem List.maxIdxOn_replicate {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.Refl fun (x1 x2 : β) => x1 ≤ x2] {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) : maxIdxOn f (replicate n a) h = 0

@[simp]

theorem List.minIdxOn?_nil {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} : minIdxOn? f [] = none

@[simp]

theorem List.minIdxOn?_singleton {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {x : α} {f : α → β} : minIdxOn? f [x] = some 0

@[simp]

theorem List.isSome_minIdxOn?_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : (minIdxOn? f xs).isSome = true ↔ xs ≠ []

theorem List.minIdxOn_eq_get_minIdxOn? {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []) : minIdxOn f xs h = (minIdxOn? f xs).get ⋯

@[simp]

theorem List.get_minIdxOn?_eq_minIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : (minIdxOn? f xs).isSome = true) : (minIdxOn? f xs).get h = minIdxOn f xs ⋯

theorem List.minIdxOn?_eq_some_minIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []) : minIdxOn? f xs = some (minIdxOn f xs h)

theorem List.minIdxOn_eq_of_minIdxOn?_eq_some {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} {i : Nat} (h : minIdxOn? f xs = some i) : minIdxOn f xs ⋯ = i

theorem List.isSome_minIdxOn?_of_mem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) : (minIdxOn? f xs).isSome = true

theorem List.minIdxOn?_cons_eq_some_minIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {x : α} {xs : List α} : minIdxOn? f (x :: xs) = some (minIdxOn f (x :: xs) ⋯)

theorem List.minIdxOn?_eq_ite {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : minIdxOn? f xs = if h : xs ≠ [] then some (minIdxOn f xs h) else none

@[deprecated List.minIdxOn?_eq_ite (since := "2026-07-21")]

theorem List.minIdxOn?_eq_if {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : minIdxOn? f xs = if h : xs ≠ [] then some (minIdxOn f xs h) else none

theorem List.minIdxOn?_cons {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} : minIdxOn? f (x :: xs) = some (if h : xs = [] then 0 else if f x ≤ f (List.minOn f xs h) then 0 else minIdxOn f xs h + 1)

theorem List.ne_nil_of_minIdxOn?_eq_some {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {k : Nat} {xs : List α} (h : minIdxOn? f xs = some k) : xs ≠ []

theorem List.lt_length_of_minIdxOn?_eq_some {β : Type u_1} {α : Type u_2} {i : Nat} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : minIdxOn? f xs = some i) : i < xs.length

@[simp]

theorem List.get_minIdxOn?_lt_length {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : (minIdxOn? f xs).isSome = true) : (minIdxOn? f xs).get h < xs.length

@[simp]

theorem List.getElem_get_minIdxOn? {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} (h : (minIdxOn? f xs).isSome = true) : xs[(minIdxOn? f xs).get h] = List.minOn f xs ⋯

theorem List.minIdxOn?_eq_some_zero_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} : minIdxOn? f xs = some 0 ↔ ∃ (h : xs ≠ []), ∀ (x : α), x ∈ xs → f (xs.head h) ≤ f x

theorem List.minIdxOn?_replicate {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.Refl fun (x1 x2 : β) => x1 ≤ x2] {n : Nat} {a : α} {f : α → β} : minIdxOn? f (replicate n a) = if n = 0 then none else some 0

@[simp]

theorem List.minIdxOn?_replicate_of_pos {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.Refl fun (x1 x2 : β) => x1 ≤ x2] {n : Nat} {a : α} {f : α → β} (h : 0 < n) : minIdxOn? f (replicate n a) = some 0

maxIdxOn?

theorem List.maxIdxOn?_eq_minIdxOn? {β : Type u_1} {α : Type u_2} {le : LE β} {x✝ : DecidableLE β} {f : α → β} {xs : List α} : maxIdxOn? f xs = minIdxOn? f xs

@[simp]

theorem List.maxIdxOn?_nil {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} : maxIdxOn? f [] = none

@[simp]

theorem List.maxIdxOn?_singleton {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {x : α} {f : α → β} : maxIdxOn? f [x] = some 0

@[simp]

theorem List.isSome_maxIdxOn?_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : (maxIdxOn? f xs).isSome = true ↔ xs ≠ []

theorem List.maxIdxOn_eq_get_maxIdxOn? {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []) : maxIdxOn f xs h = (maxIdxOn? f xs).get ⋯

@[simp]

theorem List.get_maxIdxOn?_eq_maxIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : (maxIdxOn? f xs).isSome = true) : (maxIdxOn? f xs).get h = maxIdxOn f xs ⋯

theorem List.maxIdxOn?_eq_some_maxIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []) : maxIdxOn? f xs = some (maxIdxOn f xs h)

theorem List.maxIdxOn_eq_of_maxIdxOn?_eq_some {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} {i : Nat} (h : maxIdxOn? f xs = some i) : maxIdxOn f xs ⋯ = i

theorem List.isSome_maxIdxOn?_of_mem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) : (maxIdxOn? f xs).isSome = true

theorem List.maxIdxOn?_cons_eq_some_maxIdxOn {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {x : α} {xs : List α} : maxIdxOn? f (x :: xs) = some (maxIdxOn f (x :: xs) ⋯)

theorem List.maxIdxOn?_eq_ite {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : maxIdxOn? f xs = if h : xs ≠ [] then some (maxIdxOn f xs h) else none

@[deprecated List.maxIdxOn?_eq_ite (since := "2026-07-21")]

theorem List.maxIdxOn?_eq_if {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} : maxIdxOn? f xs = if h : xs ≠ [] then some (maxIdxOn f xs h) else none

theorem List.maxIdxOn?_cons {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} : maxIdxOn? f (x :: xs) = some (if h : xs = [] then 0 else if f (List.maxOn f xs h) ≤ f x then 0 else maxIdxOn f xs h + 1)

theorem List.ne_nil_of_maxIdxOn?_eq_some {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {k : Nat} {xs : List α} (h : maxIdxOn? f xs = some k) : xs ≠ []

theorem List.lt_length_of_maxIdxOn?_eq_some {β : Type u_1} {α : Type u_2} {i : Nat} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : maxIdxOn? f xs = some i) : i < xs.length

@[simp]

theorem List.get_maxIdxOn?_lt_length {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {f : α → β} {xs : List α} (h : (maxIdxOn? f xs).isSome = true) : (maxIdxOn? f xs).get h < xs.length

@[simp]

theorem List.getElem_get_maxIdxOn? {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} (h : (maxIdxOn? f xs).isSome = true) : xs[(maxIdxOn? f xs).get h] = List.maxOn f xs ⋯

theorem List.maxIdxOn?_eq_some_zero_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} : maxIdxOn? f xs = some 0 ↔ ∃ (h : xs ≠ []), ∀ (x : α), x ∈ xs → f x ≤ f (xs.head h)

theorem List.maxIdxOn?_replicate {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.Refl fun (x1 x2 : β) => x1 ≤ x2] {n : Nat} {a : α} {f : α → β} : maxIdxOn? f (replicate n a) = if n = 0 then none else some 0

@[simp]

theorem List.maxIdxOn?_replicate_of_pos {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.Refl fun (x1 x2 : β) => x1 ≤ x2] {n : Nat} {a : α} {f : α → β} (h : 0 < n) : maxIdxOn? f (replicate n a) = some 0