-- Mathlib/Data/List/MinMax.lean
theorem argmax_cons (f : α → β) (a : α) (l : List α) :
    argmax f (a :: l) =
      Option.casesOn (argmax f l) (some a) fun c => if f a < f c then some c else some a :=
  List.reverseRecOn l rfl fun hd tl ih => by
    rw [← cons_append, argmax_concat, ih, argmax_concat]
    rcases h : argmax f hd with - | m
    · simp [h]
    dsimp
    rw [← apply_ite, ← apply_ite]
    dsimp
    split_ifs <;> try rfl
    · exact absurd (lt_trans ‹f a < f m› ‹_›) ‹_›
    · cases (‹f a < f tl›.lt_or_lt _).elim ‹_› ‹_›

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Tactic:
rw [← cons_append, argmax_concat, ih, argmax_concat]

Result:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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))

Tactic:
dsimp

Result:
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Tactic:
cases (‹f a < f tl›.lt_or_lt _).elim ‹_› ‹_›

Result:
no goals

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Tactic:
split_ifs <;> try rfl

Result:
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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 neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Proof state:
case none
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Tactic:
rcases h : argmax f hd with - | m

Result:
case none
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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 : α → β
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

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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

Tactic:
dsimp

Result:
case some
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
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)