α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
⊢ (Option.casesOn (Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a) (some tl)
      fun c => if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (argmax f hd) (some tl) fun c => if f c < f tl then some tl else some c) (some a)
      fun c => if f a < f c then some c else some a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
⊢ argmax f (a :: (hd ++ [tl])) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c => if f a < f c then some c else some a
rw [← cons_append, argmax_concat, ih, argmax_concat]
case none
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
h : argmax f hd = none
⊢ (Option.casesOn (Option.casesOn none (some a) fun c => if f a < f c then some c else some a) (some tl) fun c =>
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn none (some tl) fun c => if f c < f tl then some tl else some c) (some a) fun c =>
      if f a < f c then some c else some a

case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ (Option.casesOn (Option.casesOn (some m) (some a) fun c => if f a < f c then some c else some a) (some tl) fun c =>
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (some m) (some tl) fun c => if f c < f tl then some tl else some c) (some a) fun c =>
      if f a < f c then some c else some a
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
⊢ (Option.casesOn (Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a) (some tl)
      fun c => if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (argmax f hd) (some tl) fun c => if f c < f tl then some tl else some c) (some a)
      fun c => if f a < f c then some c else some a
cases' h : argmax f hd with m
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (if f a < f m then some m else some a) =
    Option.rec (some a) (fun val => if f a < f val then some val else some a) (if f m < f tl then some tl else some m)
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ (Option.casesOn (Option.casesOn (some m) (some a) fun c => if f a < f c then some c else some a) (some tl) fun c =>
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn (some m) (some tl) fun c => if f c < f tl then some tl else some c) (some a) fun c =>
      if f a < f c then some c else some a
dsimp
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (some (if f a < f m then m else a)) =
    Option.rec (some a) (fun val => if f a < f val then some val else some a) (some (if f m < f tl then tl else m))
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (if f a < f m then some m else some a) =
    Option.rec (some a) (fun val => if f a < f val then some val else some a) (if f m < f tl then some tl else some m)
rw [← apply_ite, ← apply_ite]
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ (if f (if f a < f m then m else a) < f tl then some tl else some (if f a < f m then m else a)) =
    if f a < f (if f m < f tl then tl else m) then some (if f m < f tl then tl else m) else some a
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ Option.rec (some tl) (fun val => if f val < f tl then some tl else some val) (some (if f a < f m then m else a)) =
    Option.rec (some a) (fun val => if f a < f val then some val else some a) (some (if f m < f tl then tl else m))
dsimp
case some.inl.inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : f a < f m
h✝¹ : f m < f tl
h✝ : ¬f a < f tl
⊢ some tl = some a

case some.inr.inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : f a < f tl
h✝ : ¬f m < f tl
⊢ some tl = some a
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
⊢ (if f (if f a < f m then m else a) < f tl then some tl else some (if f a < f m then m else a)) =
    if f a < f (if f m < f tl then tl else m) then some (if f m < f tl then tl else m) else some a
split_ifs <;> try rfl
no goals
case none
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
h : argmax f hd = none
⊢ (Option.casesOn (Option.casesOn none (some a) fun c => if f a < f c then some c else some a) (some tl) fun c =>
      if f c < f tl then some tl else some c) =
    Option.casesOn (Option.casesOn none (some tl) fun c => if f c < f tl then some tl else some c) (some a) fun c =>
      if f a < f c then some c else some a
simp [h]
no goals
case some.inr.inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : ¬f a < f tl
h✝ : ¬f m < f tl
⊢ some a = some a
rfl
no goals
case some.inl.inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : f a < f m
h✝¹ : f m < f tl
h✝ : ¬f a < f tl
⊢ some tl = some a
exact absurd (lt_trans ‹f a < f m› ‹_›) ‹_›
no goals
case some.inr.inl.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f✝ : α → β
l✝ : List α
o : Option α
a✝ m✝ : α
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c => if f a < f c then some c else some a
m : α
h : argmax f hd = some m
h✝² : ¬f a < f m
h✝¹ : f a < f tl
h✝ : ¬f m < f tl
⊢ some tl = some a
cases (‹f a < f tl›.lt_or_lt _).elim ‹_› ‹_›