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