awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
a : α
l : List α
⊢ argmin f (l ++ [a]) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmin f l) (some a) fun (c : α) ↦
      if f a < f c then some a else some c

Tactic:
@argmax_concat _ βᵒᵈ _ _ _ _ _

Premises used: List.argmax_concat, List.argmin
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
m : α
⊢ m ∈ argmax f [] → Membership.mem (γ := List α) [] m

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
hd : α
tl : List α
m : α
⊢ m ∈ argmax f (hd :: tl) → m ∈ hd :: tl

Tactic:
simpa [argmax, argAux] using foldl_argAux_mem _ tl hd m

Premises used: List.argAux, _private.0.List.foldl_argAux_mem, List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
⊢ ∀ {l : List α} {m : α}, m ∈ argmin f l → m ∈ l

Tactic:
@argmax_mem _ βᵒᵈ _ _ _

Premises used: List.argmax_mem, List.argmin
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
l : List α
⊢ argmax f l = none ↔ l = []

Tactic:
simp [argmax]

Premises used: List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
l : List α
⊢ argmin f l = none ↔ l = []

Tactic:
@argmax_eq_none _ βᵒᵈ _ _ _ _

Premises used: List.argmin, List.argmax_eq_none
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
a m : α
⊢ a ∈ l → m ∈ argmax f l → f a ≤ f m

Tactic:
fun ha hm =>
  le_of_not_gt <| not_lt_of_mem_argmax ha hm

Premises used: List.not_lt_of_mem_argmax, le_of_not_gt
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
a m : α
⊢ a ∈ l → m ∈ argmin f l → f m ≤ f a

Tactic:
@le_of_mem_argmax _ βᵒᵈ _ _ _ _ _

Premises used: List.le_of_mem_argmax, List.argmin
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih :
  argmax f (a :: hd) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmax f hd) (some a) fun (c : α) ↦
      if f a < f c then some c else some a
rw :
  Eq.{u_1 + 1} (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (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 α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (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 :
      Option α)
⊢ argmax f (a :: (hd ++ [tl])) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (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]

Premises used: List.argmax_concat, List.cons_append
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih :
  argmax f (a :: hd) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmax f hd) (Option.some a) fun (c : α) ↦
      if f a < f c then Option.some c else Option.some a
none :
  ∀ (h : argmax f hd = Option.none),
    Eq.{u_1 + 1} (α := Option α)
      (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
          (Option.casesOn (motive := fun (x : Option α) ↦ Option α) Option.none (Option.some a) fun (c : α) ↦
            if f a < f c then Option.some c else Option.some a)
          (Option.some tl) fun (c : α) ↦ if f c < f tl then Option.some tl else Option.some c :
        Option α)
      (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
          (Option.casesOn (motive := fun (x : Option α) ↦ Option α) Option.none (Option.some tl) fun (c : α) ↦
            if f c < f tl then Option.some tl else Option.some c)
          (Option.some a) fun (c : α) ↦ if f a < f c then Option.some c else Option.some a :
        Option α)
some :
  ∀ (m : α) (h : argmax f hd = Option.some m),
    Eq.{u_1 + 1} (α := Option α)
      (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
          (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.some m) (Option.some a) fun (c : α) ↦
            if f a < f c then Option.some c else Option.some a)
          (Option.some tl) fun (c : α) ↦ if f c < f tl then Option.some tl else Option.some c :
        Option α)
      (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
          (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.some m) (Option.some tl) fun (c : α) ↦
            if f c < f tl then Option.some tl else Option.some c)
          (Option.some a) fun (c : α) ↦ if f a < f c then Option.some c else Option.some a :
        Option α)
⊢ Eq.{u_1 + 1} (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmax f hd) (Option.some a) fun (c : α) ↦
          if f a < f c then Option.some c else Option.some a)
        (Option.some tl) fun (c : α) ↦ if f c < f tl then Option.some tl else Option.some c :
      Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmax f hd) (Option.some tl) fun (c : α) ↦
          if f c < f tl then Option.some tl else Option.some c)
        (Option.some a) fun (c : α) ↦ if f a < f c then Option.some c else Option.some a :
      Option α)

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

Premises used: List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih :
  argmax f (a :: hd) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmax f hd) (some a) fun (c : α) ↦
      if f a < f c then some c else some a
h : argmax f hd = none
⊢ Eq.{u_1 + 1} (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) 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 α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) 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 :
      Option α)

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih :
  argmax f (a :: hd) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmax f hd) (Option.some a) fun (c : α) ↦
      if f a < f c then Option.some c else Option.some a
m : α
h : argmax f hd = Option.some m
some :
  Eq (α := Option α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some tl)
        (fun (val : α) ↦ if f val < f tl then Option.some tl else Option.some val)
        (if f a < f m then Option.some m else Option.some a) :
      Option α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
        (fun (val : α) ↦ if f a < f val then Option.some val else Option.some a)
        (if f m < f tl then Option.some tl else Option.some m) :
      Option α)
⊢ Eq.{u_1 + 1} (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.some m) (Option.some a) fun (c : α) ↦
          if f a < f c then Option.some c else Option.some a)
        (Option.some tl) fun (c : α) ↦ if f c < f tl then Option.some tl else Option.some c :
      Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (Option.some m) (Option.some tl) fun (c : α) ↦
          if f c < f tl then Option.some tl else Option.some c)
        (Option.some a) fun (c : α) ↦ if f a < f c then Option.some c else Option.some a :
      Option α)

Tactic:
dsimp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih :
  argmax f (a :: hd) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmax f hd) (Option.some a) fun (c : α) ↦
      if f a < f c then Option.some c else Option.some a
m : α
h : argmax f hd = Option.some m
some :
  Eq (α := Option α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some tl)
        (fun (val : α) ↦ if f val < f tl then Option.some tl else Option.some val)
        (Option.some (if f a < f m then m else a)) :
      Option α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
        (fun (val : α) ↦ if f a < f val then Option.some val else Option.some a)
        (Option.some (if f m < f tl then tl else m)) :
      Option α)
⊢ Eq (α := Option α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some tl)
        (fun (val : α) ↦ if f val < f tl then Option.some tl else Option.some val)
        (if f a < f m then Option.some m else Option.some a) :
      Option α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
        (fun (val : α) ↦ if f a < f val then Option.some val else Option.some a)
        (if f m < f tl then Option.some tl else Option.some m) :
      Option α)

Tactic:
rw [← apply_ite, ← apply_ite]

Premises used: apply_ite
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih :
  argmax f (a :: hd) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (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
⊢ Eq (α := Option α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (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 α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (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)) :
      Option α)

Tactic:
grind
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
a : α
l : List α
⊢ argmin f (a :: l) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmin f l) (some a) fun (c : α) ↦
      if f c < f a then some c else some a

Tactic:
@argmax_cons α βᵒᵈ _ _ _ _

Premises used: List.argmax_cons, List.argmin
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
m : α
h : m ∈ argmax f []
x : α
h_1 : Membership.mem (γ := List α) [] x
h_2 : f m ≤ f x
⊢ idxOf m [] ≤ idxOf x []

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m : α
hm : m ∈ argmax f (hd :: tl)
a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
simp :
  ∀
    (hm :
      Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
          (fun (val : α) ↦ if f hd < f val then some val else some hd) (argmax f tl) =
        some m),
    (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
⊢ idxOf m (hd :: tl) ≤ idxOf a (hd :: tl)

Tactic:
simp only [idxOf_cons, argmax_cons, Option.mem_def] at hm ⊢

Premises used: List.idxOf_cons, List.argmax_cons, Option.mem_def
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some hd)
      (fun (val : α) ↦ if f hd < f val then Option.some val else Option.some hd) (argmax f tl) =
    Option.some m
none :
  ∀ (h : argmax f tl = Option.none), (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
some :
  ∀ (val : α) (h : argmax f tl = Option.some val),
    (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
cases h : argmax f tl

Premises used: List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (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
⊢ Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
      (fun (val : α) ↦ if f hd < f val then some val else some hd) none =
    some m

Tactic:
rw [h] at hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (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
hm₁ :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
      (fun (val : α) ↦ if f hd < f val then some val else some hd) none =
    some m
⊢ argmax f tl = none

Tactic:
rw [h] at hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
      (fun (val : α) ↦ if f hd < f val then some val else some hd) none =
    some m
h : argmax f tl = none
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
simp_all
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (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
⊢ Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
      (fun (val : α) ↦ if f hd < f val then some val else some hd) (some val) =
    some m

Tactic:
rw [h] at hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (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
hm₁ :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
      (fun (val : α) ↦ if f hd < f val then some val else some hd) (some val) =
    some m
⊢ argmax f tl = some val

Tactic:
rw [h] at hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val : α
hm : (if f hd < f val then Option.some val else Option.some hd) = Option.some m
h : argmax f tl = Option.some val
some : (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1

Tactic:
simp only [cond_eq_ite, beq_iff_eq]

Premises used: beq_iff_eq, Bool.cond_eq_ite
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
val : α
hm : (if f hd < f val then Option.some val else Option.some hd) = Option.some m
h : argmax f tl = Option.some val
some : ∀ (ham : f m ≤ f hd), (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
some₁ : Mem a tl → (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
obtain ha | ha := ha
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m val : α
hm : (if f hd < f val then some val else some hd) = some m
h : argmax f tl = some val
ham : f m ≤ f hd
pos :
  f hd < f val →
    ∀ (hm : some val = some m), (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
neg :
  ¬f hd < f val →
    ∀ (hm : some hd = some m), (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

Tactic:
split_ifs at hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
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
h_1 : Mem a tl
pos :
  f hd < f val →
    ∀ (hm : some val = some m), (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
neg :
  ¬f hd < f val →
    ∀ (hm : some hd = some m), (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
split_ifs at hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m val : α
h : argmax f tl = some val
ham : f m ≤ f hd
h_1 : f hd < f val
hm : some val = some m
⊢ val = m

Tactic:
injection hm with hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m val : α
h : argmax f tl = some val
ham : f m ≤ f hd
h_1 : ¬f hd < f val
hm : some hd = some m
⊢ hd = m

Tactic:
injection hm with hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
hm : some val = some m
⊢ val = m

Tactic:
injection hm with hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : ¬f hd < f val
hm : some hd = some m
⊢ hd = m

Tactic:
injection hm with hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m val : α
h : argmax f tl = some val
ham : f m ≤ f hd
h_1 : f hd < f val
hm : val = m
pos : ∀ (ham : f val ≤ f hd), (if hd = val then 0 else idxOf val tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

Tactic:
subst hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m val : α
h : argmax f tl = some val
ham : f m ≤ f hd
h_1 : ¬f hd < f val
hm : hd = m
neg : ∀ (ham : f hd ≤ f hd), (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

Tactic:
subst hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
hm : val = m
pos : ∀ (ham : f val ≤ f a), (if hd = val then 0 else idxOf val tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
subst hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
m a : α
ham : f m ≤ f a
val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : ¬f hd < f val
hm : hd = m
neg : ∀ (ham : f hd ≤ f a), (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
subst hm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
val : α
h : argmax f tl = some val
h_1 : f hd < f val
ham : f val ≤ f hd
⊢ (if hd = val then 0 else idxOf val tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

Tactic:
cases not_le_of_gt ‹_› ‹_›

Premises used: not_le_of_gt
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
val : α
h : argmax f tl = some val
h_1 : ¬f hd < f val
ham : f hd ≤ f hd
neg neg₁ : LE.le (α := ℕ) 0 0
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1

Tactic:
rw [if_pos rfl]

Premises used: if_pos, rfl
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
a val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
ham : f val ≤ f a
pos : idxOf val tl + 1 ≤ idxOf a tl + 1
pos₁ : ¬hd = a
pos₂ : ¬hd = val
⊢ (if hd = val then 0 else idxOf val tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
rw [if_neg, if_neg]

Premises used: if_neg
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
a val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
ham : f val ≤ f a
⊢ a ∈ tl

Tactic:
assumption
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
a val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
ham : f val ≤ f a
⊢ idxOf val tl + 1 ≤ idxOf a tl + 1

Tactic:
exact Nat.succ_le_succ (index_of_argmax h (by assumption) ham)

Premises used: Nat.succ_le_succ
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
a val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
ham : f val ≤ f a
⊢ ¬hd = a

Tactic:
ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne

Premises used: ne_of_apply_ne, lt_of_lt_of_le, LT.lt.ne
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
a val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
ham : f val ≤ f a
⊢ ¬hd = a

Tactic:
exact ne_of_apply_ne f (lt_of_lt_of_le ‹_› ‹_›).ne

Premises used: ne_of_apply_ne, lt_of_lt_of_le, LT.lt.ne
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
a val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
ham : f val ≤ f a
⊢ ¬hd = val

Tactic:
ne_of_apply_ne _ ‹f hd < f _›.ne

Premises used: ne_of_apply_ne, LT.lt.ne
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
hd : α
tl : List α
a val : α
h : argmax f tl = some val
h_1 : Mem a tl
h_2 : f hd < f val
ham : f val ≤ f a
⊢ ¬hd = val

Tactic:
exact ne_of_apply_ne _ ‹f hd < f _›.ne

Premises used: ne_of_apply_ne, LT.lt.ne