@[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

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_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

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_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