no goals
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x x_1 => x < x_1
f : α → β
l : List α
o : Option α
a m✝ m : α
⊢ m ∈ argmax f [] → m ∈ []
simp
no goals
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x x_1 => x < x_1
f : α → β
l : List α
o : Option α
a m✝ hd : α
tl : List α
m : α
⊢ m ∈ argmax f (hd :: tl) → m ∈ hd :: tl
simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m