@[inline]

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

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

The correctness of this function assumes β to be linearly pre-ordered. The property that List.minOn is the first minimizer in the list is guaranteed by the lemma List.getElem_minIdxOn.

Equations

• List.minOn f (x :: xs) h_2 = List.foldl (minOn f) x xs

@[inline]

def List.maxOn {β : Type u_1} {α : Type u_2} [i : LE β] [DecidableLE β] (f : α → β) (l : List α) (h : l ≠ []) : α

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

The correctness of this function assumes β to be linearly pre-ordered. The property that List.maxOn is the first maximizer in the list is guaranteed by the lemma List.getElem_maxIdxOn.

Equations

• List.maxOn f l h = List.minOn f l h

@[inline]

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

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

The correctness of this function assumes β to be linearly pre-ordered. The property that List.minOn? is the first minimizer in the list is guaranteed by the lemma List.getElem_get_minIdxOn?

Equations

• List.minOn? f [] = none
• List.minOn? f (x :: xs) = some (List.foldl (minOn f) x xs)

@[inline]

def List.maxOn? {β : Type u_1} {α : Type u_2} [i : LE β] [DecidableLE β] (f : α → β) (l : List α) : Option α

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

The correctness of this function assumes β to be linearly pre-ordered. The property that List.maxOn? is the first minimizer in the list is guaranteed by the lemma List.getElem_get_maxIdxOn?.

Equations

• List.maxOn? f l = List.minOn? f l

@[simp]

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

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

theorem List.minOn_cons_cons {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {a b : α} {l : List α} {f : α → β} : List.minOn f (a :: b :: l) ⋯ = List.minOn f (minOn f a b :: l) ⋯

@[simp]

theorem List.minOn_cons_cons_nil {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {a b : α} {f : α → β} : List.minOn f [a, b] ⋯ = minOn f a b

@[simp]

theorem List.minOn_id {α : Type u_1} [Min α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α] {xs : List α} (h : xs ≠ []) : List.minOn id xs h = xs.min h

@[simp]

theorem List.minOn_mem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {xs : List α} {f : α → β} {h : xs ≠ []} : List.minOn f xs h ∈ xs

theorem List.apply_minOn_le_of_mem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) : f (List.minOn f xs ⋯) ≤ f y

theorem List.le_apply_minOn_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} : b ≤ f (List.minOn f xs h) ↔ ∀ (x : α), x ∈ xs → b ≤ f x

theorem List.apply_minOn_le_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} : f (List.minOn f xs h) ≤ b ↔ ∃ (x : α), x ∈ xs ∧ f x ≤ b

theorem List.lt_apply_minOn_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} : b < f (List.minOn f xs h) ↔ ∀ (x : α), x ∈ xs → b < f x

theorem List.apply_minOn_lt_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} : f (List.minOn f xs h) < b ↔ ∃ (x : α), x ∈ xs ∧ f x < b

theorem List.apply_minOn_le_apply_minOn_of_subset {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α} {f : α → β} (hxs : ys ⊆ xs) (hys : ys ≠ []) : f (List.minOn f xs ⋯) ≤ f (List.minOn f ys hys)

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

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

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

@[simp]

theorem List.minOn_append {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α} {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) : List.minOn f (xs ++ ys) ⋯ = minOn f (List.minOn f xs hxs) (List.minOn f ys hys)

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

theorem List.min_map {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Min β] [Std.IsLinearPreorder β] [Std.LawfulOrderLeftLeaningMin β] {xs : List α} {f : α → β} (h : xs ≠ []) : (map f xs).min ⋯ = f (List.minOn f xs h)

theorem List.minOn_eq_min {α : Type u_1} {β : Type u_2} [Min α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α] [LE β] [DecidableLE β] {f : α → β} {l : List α} {h : l ≠ []} (hf : ∀ (a b : α), f a ≤ f b ↔ a ≤ b) : List.minOn f l h = l.min h

theorem List.min_map_eq_min {α : Type u_1} {β : Type u_2} [Min α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α] [Min β] [LE β] [DecidableLE β] [Std.IsLinearPreorder β] [Std.LawfulOrderLeftLeaningMin β] {f : α → β} (hf : ∀ (a b : α), f a ≤ f b ↔ a ≤ b) {l : List α} {h : l ≠ []} : (map f l).min ⋯ = f (l.min h)

@[simp]

theorem List.minOn_replicate {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) : List.minOn f (replicate n a) h = a

theorem List.maxOn_eq_minOn {β : Type u_1} {α : Type u_2} {le : LE β} {dle : DecidableLE β} {xs : List α} {f : α → β} {h : xs ≠ []} : List.maxOn f xs h = List.minOn f xs h

@[simp]

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

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

theorem List.maxOn_cons_cons {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {a b : α} {l : List α} {f : α → β} : List.maxOn f (a :: b :: l) ⋯ = List.maxOn f (maxOn f a b :: l) ⋯

@[simp]

theorem List.maxOn_cons_cons_nil {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {a b : α} {f : α → β} : List.maxOn f [a, b] ⋯ = maxOn f a b

theorem List.min_eq_max {α : Type u_1} {min : Min α} {xs : List α} {h : xs ≠ []} : xs.min h = xs.max h

theorem List.max_eq_min {α : Type u_1} {max : Max α} {xs : List α} {h : xs ≠ []} : xs.max h = xs.min h

theorem List.max?_eq_min? {α : Type u_1} {max : Max α} {xs : List α} : xs.max? = xs.min?

@[simp]

theorem List.maxOn_id {α : Type u_1} [Max α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α] {xs : List α} (h : xs ≠ []) : List.maxOn id xs h = xs.max h

@[simp]

theorem List.maxOn_mem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] {xs : List α} {f : α → β} {h : xs ≠ []} : List.maxOn f xs h ∈ xs

theorem List.le_apply_maxOn_of_mem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} {y : α} (hx : y ∈ xs) : f y ≤ f (List.maxOn f xs ⋯)

theorem List.apply_maxOn_le_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} : f (List.maxOn f xs h) ≤ b ↔ ∀ (x : α), x ∈ xs → f x ≤ b

theorem List.le_apply_maxOn_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} : b ≤ f (List.maxOn f xs h) ↔ ∃ (x : α), x ∈ xs ∧ b ≤ f x

theorem List.apply_maxOn_lt_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} : f (List.maxOn f xs h) < b ↔ ∀ (x : α), x ∈ xs → f x < b

theorem List.lt_apply_maxOn_iff {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [LT β] [Std.IsLinearPreorder β] [Std.LawfulOrderLT β] {xs : List α} {f : α → β} (h : xs ≠ []) {b : β} : b < f (List.maxOn f xs h) ↔ ∃ (x : α), x ∈ xs ∧ b < f x

theorem List.apply_maxOn_le_apply_maxOn_of_subset {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α} {f : α → β} (hxs : ys ⊆ xs) (hys : ys ≠ []) : f (List.maxOn f ys hys) ≤ f (List.maxOn f xs ⋯)

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

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

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

@[simp]

theorem List.maxOn_append {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α} {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []) : List.maxOn f (xs ++ ys) ⋯ = maxOn f (List.maxOn f xs hxs) (List.maxOn f ys hys)

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

theorem List.max_map {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Max β] [Std.IsLinearPreorder β] [Std.LawfulOrderLeftLeaningMax β] {xs : List α} {f : α → β} (h : xs ≠ []) : (map f xs).max ⋯ = f (List.maxOn f xs h)

theorem List.maxOn_eq_max {α : Type u_1} {β : Type u_2} [Max α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α] [LE β] [DecidableLE β] {f : α → β} {l : List α} {h : l ≠ []} (hf : ∀ (a b : α), f a ≤ f b ↔ a ≤ b) : List.maxOn f l h = l.max h

theorem List.max_map_eq_max {α : Type u_1} {β : Type u_2} [Max α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α] [Max β] [LE β] [DecidableLE β] [Std.IsLinearPreorder β] [Std.LawfulOrderLeftLeaningMax β] {f : α → β} (hf : ∀ (a b : α), f a ≤ f b ↔ a ≤ b) {l : List α} {h : l ≠ []} : (map f l).max ⋯ = f (l.max h)

@[simp]

theorem List.maxOn_replicate {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {n : Nat} {a : α} {f : α → β} (h : replicate n a ≠ []) : List.maxOn f (replicate n a) h = a

@[simp]

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

List.minOn? returns none when applied to an empty list.

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

theorem List.minOn?_cons {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} : List.minOn? f (x :: xs) = some ((List.minOn? f xs).elim x (minOn f x))

@[simp]

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

@[simp]

theorem List.minOn?_id {α : Type u_1} [Min α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α] {xs : List α} : List.minOn? id xs = xs.min?

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

@[simp]

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

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

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

@[simp]

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

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

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

theorem List.apply_get_minOn?_le_of_mem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) : f ((List.minOn? f xs).get ⋯) ≤ f x

theorem List.minOn?_mem {β : Type u_1} {α : Type u_2} {a : α} [LE β] [DecidableLE β] {xs : List α} {f : α → β} (h : List.minOn? f xs = some a) : a ∈ xs

theorem List.minOn?_replicate {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {n : Nat} {a : α} {f : α → β} : List.minOn? f (replicate n a) = if n = 0 then none else some a

@[simp]

theorem List.minOn?_replicate_of_pos {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {n : Nat} {a : α} {f : α → β} (h : 0 < n) : List.minOn? f (replicate n a) = some a

@[simp]

theorem List.minOn?_append {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs ys : List α) (f : α → β) : List.minOn? f (xs ++ ys) = Option.merge (minOn f) (List.minOn? f xs) (List.minOn? f ys)

theorem List.maxOn?_eq_minOn? {β : Type u_1} {α : Type u_2} {le : LE β} {dle : DecidableLE β} {xs : List α} {f : α → β} : List.maxOn? f xs = List.minOn? f xs

@[simp]

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

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

theorem List.maxOn?_cons {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x : α} {xs : List α} : List.maxOn? f (x :: xs) = some ((List.maxOn? f xs).elim x (maxOn f x))

@[simp]

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

@[simp]

theorem List.maxOn?_id {α : Type u_1} [Max α] [LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α] {xs : List α} : List.maxOn? id xs = xs.max?

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

@[simp]

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

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

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

@[simp]

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

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

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

theorem List.le_apply_get_maxOn?_of_mem {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {xs : List α} {x : α} (h : x ∈ xs) : f x ≤ f ((List.maxOn? f xs).get ⋯)

theorem List.maxOn?_mem {β : Type u_1} {α : Type u_2} {a : α} [LE β] [DecidableLE β] {xs : List α} {f : α → β} (h : List.maxOn? f xs = some a) : a ∈ xs

theorem List.maxOn?_replicate {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {n : Nat} {a : α} {f : α → β} : List.maxOn? f (replicate n a) = if n = 0 then none else some a

@[simp]

theorem List.maxOn?_replicate_of_pos {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] {n : Nat} {a : α} {f : α → β} (h : 0 < n) : List.maxOn? f (replicate n a) = some a

@[simp]

theorem List.maxOn?_append {β : Type u_1} {α : Type u_2} [LE β] [DecidableLE β] [Std.IsLinearPreorder β] (xs ys : List α) (f : α → β) : List.maxOn? f (xs ++ ys) = Option.merge (maxOn f) (List.maxOn? f xs) (List.maxOn? f ys)