no goals
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m✝ : α
inst✝ : DecidableEq α
m : α
x✝³ : m ∈ argmax f []
x✝² : α
x✝¹ : x✝² ∈ []
x✝ : f m ≤ f x✝²
⊢ indexOf m [] ≤ indexOf x✝² []
simp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m : α
hm : m ∈ argmax f (hd :: tl)
a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
⊢ indexOf m (hd :: tl) ≤ indexOf a (hd :: tl)
simp only [indexOf_cons, argmax_cons, Option.mem_def] at hm⊢
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
h : argmax f tl = none
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)

case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
val✝ : α
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
cases h : argmax f tl
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (some val✝) = some m
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
val✝ : α
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
rw [h] at hm
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (some val✝) = some m
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
dsimp only at hm
case some.head.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : f hd < f val✝
ham : f val✝ ≤ f hd
⊢ (if val✝ = hd then 0 else Nat.succ (indexOf val✝ tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)

case some.head.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : ¬f hd < f val✝
ham : f hd ≤ f hd
⊢ (if hd = hd then 0 else Nat.succ (indexOf hd tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)

case some.tail.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if val✝ = hd then 0 else Nat.succ (indexOf val✝ tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)

case some.tail.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else Nat.succ (indexOf hd tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val✝ : α
hm : (if f hd < f val✝ then some val✝ else some hd) = some m
h : argmax f tl = some val✝
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
obtain ha | ha := ha <;> split_ifs at hm <;> injection hm with hm <;> subst hm
no goals
case some.tail.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else Nat.succ (indexOf hd tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
. rw [if_pos rfl]
  exact Nat.zero_le _
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) none = some m
h : argmax f tl = none
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) (argmax f tl) = some m
h : argmax f tl = none
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
rw [h] at hm
no goals
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝ m✝ : α
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val => if f hd < f val then some val else some hd) none = some m
h : argmax f tl = none
⊢ (if m = hd then 0 else Nat.succ (indexOf m tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
simp_all
no goals
case some.head.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : f hd < f val✝
ham : f val✝ ≤ f hd
⊢ (if val✝ = hd then 0 else Nat.succ (indexOf val✝ tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
cases not_le_of_lt ‹_› ‹_›
no goals
case some.head.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a m : α
inst✝ : DecidableEq α
hd : α
tl : List α
val✝ : α
h : argmax f tl = some val✝
h✝ : ¬f hd < f val✝
ham : f hd ≤ f hd
⊢ (if hd = hd then 0 else Nat.succ (indexOf hd tl)) ≤ if hd = hd then 0 else Nat.succ (indexOf hd tl)
rw [if_pos rfl]
case some.tail.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ Nat.succ (indexOf val✝ tl) ≤ Nat.succ (indexOf a tl)

case some.tail.inl.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬a = hd

case some.tail.inl.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬val✝ = hd
case some.tail.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ (if val✝ = hd then 0 else Nat.succ (indexOf val✝ tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
rw [if_neg, if_neg]
case some.tail.inl.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬a = hd

case some.tail.inl.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬val✝ = hd
case some.tail.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ Nat.succ (indexOf val✝ tl) ≤ Nat.succ (indexOf a tl)

case some.tail.inl.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬a = hd

case some.tail.inl.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬val✝ = hd
exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)
no goals
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ a ∈ tl
assumption
no goals
case some.tail.inl.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬a = hd
exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne'
no goals
case some.tail.inl.hnc
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : f hd < f val✝
ham : f val✝ ≤ f a
⊢ ¬val✝ = hd
exact ne_of_apply_ne _ ‹f hd < f _›.ne'
case some.tail.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ 0 ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
case some.tail.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ (if hd = hd then 0 else Nat.succ (indexOf hd tl)) ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
rw [if_pos rfl]
no goals
case some.tail.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
o : Option α
a✝¹ m : α
inst✝ : DecidableEq α
hd : α
tl : List α
a val✝ : α
h : argmax f tl = some val✝
a✝ : Mem a tl
h✝ : ¬f hd < f val✝
ham : f hd ≤ f a
⊢ 0 ≤ if a = hd then 0 else Nat.succ (indexOf a tl)
exact Nat.zero_le _