α : Type u_1
β : Type ?u.92933
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (argmax (fun a => a) l) =
    max (argmax (fun a => a) l) ↑a
α : Type u_1
β : Type ?u.92933
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
⊢ maximum (l ++ [a]) = max (maximum l) ↑a
simp only [maximum, argmax_concat, id]
case none
α : Type u_1
β : Type ?u.92933
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
h : argmax id l = none
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) none = max none ↑a

case some
α : Type u_1
β : Type ?u.92933
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
val✝ : α
h : argmax id l = some val✝
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (some val✝) = max (some val✝) ↑a
α : Type u_1
β : Type ?u.92933
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (argmax (fun a => a) l) =
    max (argmax (fun a => a) l) ↑a
cases h : argmax id l
no goals
case none
α : Type u_1
β : Type ?u.92933
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
h : argmax id l = none
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) none = max none ↑a
exact (max_eq_right bot_le).symm
no goals
case some
α : Type u_1
β : Type ?u.92933
inst✝ : LinearOrder α
l✝ : List α
a✝ m a : α
l : List α
val✝ : α
h : argmax id l = some val✝
⊢ Option.rec (some a) (fun val => if val < a then some a else some val) (some val✝) = max (some val✝) ↑a
simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]