case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
⊢ m ∈ argmax f l
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l) → m ∈ argmax f l
rintro ⟨hml, ham, hma⟩
case intro.intro.none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
harg : argmax f l = none
⊢ m ∈ none

case intro.intro.some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
n : α
harg : argmax f l = some n
⊢ m ∈ some n
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
⊢ m ∈ argmax f l
cases' harg : argmax f l with n
no goals
case intro.intro.none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
harg : argmax f l = none
⊢ m ∈ none
simp_all
case intro.intro.some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
n : α
harg : argmax f l = some n
this : indexOf m l = indexOf n l
⊢ m ∈ some n
case intro.intro.some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
n : α
harg : argmax f l = some n
⊢ m ∈ some n
have :=
  _root_.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg))
    (index_of_argmax harg hml (ham _ (argmax_mem harg)))
no goals
case intro.intro.some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → indexOf m l ≤ indexOf a l
n : α
harg : argmax f l = some n
this : indexOf m l = indexOf n l
⊢ m ∈ some n
rw [(indexOf_inj hml (argmax_mem harg)).1 this, Option.mem_def]