awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 hd ≤ f a
neg : 0 ≤ if hd = a then 0 else idxOf a tl + 1
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a 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 hd ≤ f a
⊢ 0 ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- 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 hd ≤ f a
⊢ 0 ≤ if hd = a then 0 else idxOf a tl + 1

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
inst_1 : DecidableEq α
⊢ ∀ {l : List α} {m : α}, m ∈ argmin f l → ∀ {a : α}, a ∈ l → f a ≤ f m → idxOf m l ≤ idxOf a l

Tactic:
@index_of_argmax _ βᵒᵈ _ _ _

Premises used: List.index_of_argmax, List.argmin
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
m : α
inst_1 : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
none : ∀ (harg : argmax f l = Option.none), Membership.mem (γ := Option α) Option.none m
some : ∀ (n : α) (harg : argmax f l = Option.some n), m ∈ Option.some n
⊢ m ∈ argmax f l

Tactic:
rcases harg : argmax f l with - | n

Premises used: List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
m : α
inst_1 : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
harg : argmax f l = none
⊢ Membership.mem (γ := Option α) none m

Tactic:
simp_all
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
m : α
inst_1 : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
⊢ idxOf m l = idxOf n l

Tactic:
have :=
          Nat.le_antisymm (hma n (argmax_mem harg) (le_of_mem_argmax hml harg))
            (index_of_argmax harg hml (ham _ (argmax_mem harg)))
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
m : α
inst_1 : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = Option.some n
this : idxOf m l = idxOf n l
some : n ∈ Option.some n
some₁ some₂ : Option.some n = Option.some n
⊢ m ∈ Option.some n

Tactic:
rw [(idxOf_inj hml).1 this, Option.mem_def]

Premises used: Iff.mp, List.idxOf_inj, Option.mem_def
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
m : α
inst_1 : DecidableEq α
⊢ argmax f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l

Tactic:
mem_argmax_iff

Premises used: List.mem_argmax_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
m : α
inst_1 : DecidableEq α
⊢ m ∈ argmin f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → idxOf m l ≤ idxOf a l

Tactic:
@mem_argmax_iff _ βᵒᵈ _ _ _ _ _

Premises used: List.mem_argmax_iff, List.argmin
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : α → β
l : List α
m : α
inst_1 : DecidableEq α
⊢ argmin f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → idxOf m l ≤ idxOf a l

Tactic:
mem_argmin_iff

Premises used: List.mem_argmin_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
⊢ Eq.{u_1 + 1} (α := WithBot α) (maximum []) ⊥

Tactic:
rfl

Premises used: List.maximum, List.foldl, rfl, List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
⊢ Eq.{u_1 + 1} (α := WithTop α) (minimum []) ⊤

Tactic:
rfl

Premises used: List.minimum, List.foldl, List.argmin, rfl
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a : α
⊢ [a].maximum = (↑a : WithBot α)

Tactic:
rfl

Premises used: List.maximum, WithBot.some, List.argAux, List.foldl, rfl, List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
a : α
⊢ [a].minimum = (↑a : WithTop α)

Tactic:
rfl

Premises used: List.minimum, List.argAux, List.foldl, WithTop.some, List.argmin, rfl
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
m : α
⊢ l.maximum = (↑m : WithBot α) → m ∈ l

Tactic:
argmax_mem

Premises used: List.maximum, WithBot.some, WithBot, List.argmax_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
m : α
⊢ l.minimum = (↑m : WithTop α) → m ∈ l

Tactic:
argmin_mem

Premises used: List.minimum, WithTop.some, List.argmin_mem, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
⊢ l.maximum = ⊥ ↔ l = []

Tactic:
argmax_eq_none

Premises used: List.maximum, WithBot, List.argmax_eq_none
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
⊢ l.minimum = ⊤ ↔ l = []

Tactic:
argmin_eq_none

Premises used: List.minimum, List.argmin_eq_none, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a m : α
⊢ a ∈ l → l.maximum = (↑m : WithBot α) → ¬m < a

Tactic:
not_lt_of_mem_argmax

Premises used: List.maximum, WithBot.some, WithBot, List.not_lt_of_mem_argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a m : α
⊢ a ∈ l → l.minimum = (↑m : WithTop α) → ¬a < m

Tactic:
not_lt_of_mem_argmin

Premises used: List.not_lt_of_mem_argmin, List.minimum, WithTop.some, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
bot : ∀ (h : l.maximum = ⊥), ¬⊥ < (↑a : WithBot α)
coe : ∀ (a_1 : α) (h : l.maximum = (↑a_1 : WithBot α)), ¬(↑a_1 : WithBot α) < (↑a : WithBot α)
⊢ ¬l.maximum < (↑a : WithBot α)

Tactic:
cases h : l.maximum

Premises used: List.maximum
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
h : l.maximum = ⊥
⊢ ¬⊥ < (↑a : WithBot α)

Tactic:
simp_all [not_maximum_lt_of_mem ha]

Premises used: List.not_maximum_lt_of_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
a_1 : α
h : l.maximum = (↑a_1 : WithBot α)
⊢ ¬(↑a_1 : WithBot α) < (↑a : WithBot α)

Tactic:
simp_all [not_maximum_lt_of_mem ha]

Premises used: List.not_maximum_lt_of_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
top : ∀ (h : l.minimum = ⊤), ¬(↑a : WithTop α) < ⊤
coe : ∀ (a_1 : α) (h : l.minimum = (↑a_1 : WithTop α)), ¬(↑a : WithTop α) < (↑a_1 : WithTop α)
⊢ ¬(↑a : WithTop α) < l.minimum

Tactic:
cases h : l.minimum

Premises used: List.minimum
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
h : l.minimum = ⊤
⊢ ¬(↑a : WithTop α) < ⊤

Tactic:
simp_all [not_lt_minimum_of_mem ha]

Premises used: List.not_lt_minimum_of_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
a_1 : α
h : l.minimum = (↑a_1 : WithTop α)
⊢ ¬(↑a : WithTop α) < (↑a_1 : WithTop α)

Tactic:
simp_all [not_lt_minimum_of_mem ha]

Premises used: List.not_lt_minimum_of_mem
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
simp :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (some a) (fun (val : α) ↦ if val < a then some a else some val)
      (argmax id l) =
    max (argmax id l) (↑a : WithBot α)
⊢ (l ++ [a]).maximum = max l.maximum (↑a : WithBot α)

Tactic:
simp only [maximum, argmax_concat, id]

Premises used: List.maximum, id, List.argmax_concat
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
none :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
      (fun (val : α) ↦ if val < a then Option.some a else Option.some val) Option.none =
    max Option.none (↑a : WithBot α)
some :
  ∀ (val : α),
    Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
        (fun (val : α) ↦ if val < a then Option.some a else Option.some val) (Option.some val) =
      max (Option.some val) (↑a : WithBot α)
⊢ Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
      (fun (val : α) ↦ if val < a then Option.some a else Option.some val) (argmax id l) =
    max (argmax id l) (↑a : WithBot α)

Tactic:
cases argmax id l

Premises used: id, List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
⊢ Option.rec (motive := fun (x : Option α) ↦ Option α) (some a) (fun (val : α) ↦ if val < a then some a else some val)
      none =
    max none (↑a : WithBot α)

Tactic:
(max_eq_right bot_le).symm

Premises used: max_eq_right, Eq.symm, bot_le
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
⊢ Option.rec (motive := fun (x : Option α) ↦ Option α) (some a) (fun (val : α) ↦ if val < a then some a else some val)
      none =
    max none (↑a : WithBot α)

Tactic:
exact (max_eq_right bot_le).symm

Premises used: max_eq_right, Eq.symm, bot_le
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
val : α
⊢ Option.rec (motive := fun (x : Option α) ↦ Option α) (some a) (fun (val : α) ↦ if val < a then some a else some val)
      (some val) =
    max (some val) (↑a : WithBot α)

Tactic:
simp [WithBot.some_eq_coe, max_def_lt, WithBot.coe_lt_coe]

Premises used: max_def_lt, WithBot.coe_lt_coe, WithBot.some_eq_coe
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a m : α
⊢ a ∈ l → l.maximum = (↑m : WithBot α) → a ≤ m

Tactic:
le_of_mem_argmax

Premises used: List.maximum, WithBot.some, WithBot, List.le_of_mem_argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a m : α
⊢ a ∈ l → l.minimum = (↑m : WithTop α) → m ≤ a

Tactic:
le_of_mem_argmin

Premises used: List.minimum, WithTop.some, List.le_of_mem_argmin, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
ha : a ∈ l
⊢ (↑a : WithBot α) ≤ l.maximum

Tactic:
le_of_not_gt <| not_maximum_lt_of_mem' ha

Premises used: le_of_not_gt, List.not_maximum_lt_of_mem'
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
ha : a ∈ l
⊢ l.minimum ≤ (↑a : WithTop α)

Tactic:
le_of_not_gt <| not_lt_minimum_of_mem' ha

Premises used: le_of_not_gt, List.not_lt_minimum_of_mem'
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
⊢ (l ++ [a]).minimum = min l.minimum (↑a : WithTop α)

Tactic:
@maximum_concat αᵒᵈ _ _ _

Premises used: List.minimum, WithTop.some, List.argmin, OrderDual, List.maximum_concat, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
⊢ [a].maximum = max (↑a : WithBot α) (maximum [])

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a : WithBot α) tl.maximum
rw : (a :: tl ++ [hd]).maximum = max (↑a : WithBot α) (tl ++ [hd]).maximum
rw₁ : max (a :: tl).maximum (↑hd : WithBot α) = max (↑a : WithBot α) (tl ++ [hd]).maximum
rw₂ : max (max (↑a : WithBot α) tl.maximum) (↑hd : WithBot α) = max (↑a : WithBot α) (tl ++ [hd]).maximum
rw₃ : max (max (↑a : WithBot α) tl.maximum) (↑hd : WithBot α) = max (↑a : WithBot α) (max tl.maximum (↑hd : WithBot α))
rw₄ rw₅ :
  max (↑a : WithBot α) (max tl.maximum (↑hd : WithBot α)) = max (↑a : WithBot α) (max tl.maximum (↑hd : WithBot α))
⊢ (a :: (tl ++ [hd])).maximum = max (↑a : WithBot α) (tl ++ [hd]).maximum

Tactic:
rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]

Premises used: max_assoc, List.cons_append, List.maximum_concat
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
⊢ (a :: l).minimum = min (↑a : WithTop α) l.minimum

Tactic:
@maximum_cons αᵒᵈ _ _ _

Premises used: List.maximum_cons, List.minimum, WithTop.some, List.argmin, OrderDual, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l₂ : List α
⊢ ([] ++ l₂).maximum = max (maximum []) l₂.maximum

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l₂ : List α
head : α
tail : List α
ih : (tail ++ l₂).maximum = max tail.maximum l₂.maximum
cons : (head :: tail ++ l₂).maximum = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
cons₁ : (head :: (tail ++ l₂)).maximum = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
cons₂ : max (↑head : WithBot α) (tail ++ l₂).maximum = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
cons₃ : max (↑head : WithBot α) (max tail.maximum l₂.maximum) = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
cons₄ cons₅ :
  max (max (↑head : WithBot α) tail.maximum) l₂.maximum = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
⊢ (head :: tail ++ l₂).maximum = max (head :: tail).maximum l₂.maximum

Tactic:
rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]

Premises used: List.maximum_cons, max_assoc, List.cons_append
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l₁ l₂ : List α
nil : ([] ++ l₂).maximum = max (maximum []) l₂.maximum
cons :
  ∀ (head : α) (tail : List α) (ih : (tail ++ l₂).maximum = max tail.maximum l₂.maximum),
    (head :: tail ++ l₂).maximum = max (head :: tail).maximum l₂.maximum
⊢ (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum

Tactic:
induction l₁ with
  | nil => simp
  | cons _ _ ih => rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]

Premises used: List.maximum_cons, List.cons, max_assoc, List.cons_append, List.nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).minimum = min l₁.minimum l₂.minimum

Tactic:
@maximum_append αᵒᵈ _ _ _

Premises used: List.minimum, WithTop.some, List.argmin, OrderDual, List.maximum_append, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), Membership.mem (γ := List α) [] a → (↑a : WithBot α) ≤ b
⊢ maximum [] ≤ b

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l_1 : List α
b : WithBot α
a : α
l : List α
ih : ∀ (h : ∀ (a : α), a ∈ l → (↑a : WithBot α) ≤ b), l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → (↑a_1 : WithBot α) ≤ b
cons : (↑a : WithBot α) ≤ b ∧ l.maximum ≤ b
⊢ (a :: l).maximum ≤ b

Tactic:
simp only [maximum_cons, max_le_iff]

Premises used: List.maximum_cons, max_le_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l_1 : List α
b : WithBot α
a : α
l : List α
ih : ∀ (h : ∀ (a : α), a ∈ l → (↑a : WithBot α) ≤ b), l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → (↑a_1 : WithBot α) ≤ b
⊢ a ∈ a :: l

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l_1 : List α
b : WithBot α
a : α
l : List α
ih : ∀ (h : ∀ (a : α), a ∈ l → (↑a : WithBot α) ≤ b), l.maximum ≤ b
h : ∀ (a_1 : α), a_1 ∈ a :: l → (↑a_1 : WithBot α) ≤ b
⊢ (↑a : WithBot α) ≤ b ∧ l.maximum ≤ b

Tactic:
exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ l → (↑a : WithBot α) ≤ b
nil : ∀ (h : ∀ (a : α), Membership.mem (γ := List α) [] a → (↑a : WithBot α) ≤ b), maximum [] ≤ b
cons :
  ∀ (a : α) (l : List α) (ih : ∀ (h : ∀ (a : α), a ∈ l → (↑a : WithBot α) ≤ b), l.maximum ≤ b)
    (h : ∀ (a_1 : α), a_1 ∈ a :: l → (↑a_1 : WithBot α) ≤ b), (a :: l).maximum ≤ b
⊢ l.maximum ≤ b

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    simp only [maximum_cons, max_le_iff]
    exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

Premises used: List.maximum_cons, max_le_iff, List.cons, List.nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
b : WithTop α
h : ∀ (a : α), Membership.mem (γ := List α) [] a → b ≤ (↑a : WithTop α)
⊢ b ≤ minimum []

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l_1 : List α
b : WithTop α
a : α
l : List α
ih : ∀ (h : ∀ (a : α), a ∈ l → b ≤ (↑a : WithTop α)), b ≤ l.minimum
h : ∀ (a_1 : α), a_1 ∈ a :: l → b ≤ (↑a_1 : WithTop α)
cons : b ≤ (↑a : WithTop α) ∧ b ≤ l.minimum
⊢ b ≤ (a :: l).minimum

Tactic:
simp only [minimum_cons, le_min_iff]

Premises used: List.minimum_cons, le_min_iff
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l_1 : List α
b : WithTop α
a : α
l : List α
ih : ∀ (h : ∀ (a : α), a ∈ l → b ≤ (↑a : WithTop α)), b ≤ l.minimum
h : ∀ (a_1 : α), a_1 ∈ a :: l → b ≤ (↑a_1 : WithTop α)
⊢ a ∈ a :: l

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l_1 : List α
b : WithTop α
a : α
l : List α
ih : ∀ (h : ∀ (a : α), a ∈ l → b ≤ (↑a : WithTop α)), b ≤ l.minimum
h : ∀ (a_1 : α), a_1 ∈ a :: l → b ≤ (↑a_1 : WithTop α)
⊢ b ≤ (↑a : WithTop α) ∧ b ≤ l.minimum

Tactic:
exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
b : WithTop α
h : ∀ (a : α), a ∈ l → b ≤ (↑a : WithTop α)
nil : ∀ (h : ∀ (a : α), Membership.mem (γ := List α) [] a → b ≤ (↑a : WithTop α)), b ≤ minimum []
cons :
  ∀ (a : α) (l : List α) (ih : ∀ (h : ∀ (a : α), a ∈ l → b ≤ (↑a : WithTop α)), b ≤ l.minimum)
    (h : ∀ (a_1 : α), a_1 ∈ a :: l → b ≤ (↑a_1 : WithTop α)), b ≤ (a :: l).minimum
⊢ b ≤ l.minimum

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    simp only [minimum_cons, le_min_iff]
    exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

Premises used: List.minimum_cons, List.cons, le_min_iff, List.nil
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l₁ l₂ : List α
h : l₁ ⊆ l₂
⊢ l₁.maximum ≤ l₂.maximum

Tactic:
maximum_le_of_forall_le fun _ ↦ (le_maximum_of_mem' <| h ·)

Premises used: List.maximum_le_of_forall_le, List.le_maximum_of_mem'
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l₁ l₂ : List α
h : l₁ ⊆ l₂
⊢ l₂.minimum ≤ l₁.minimum

Tactic:
@maximum_mono αᵒᵈ _ _ _ h

Premises used: List.minimum, List.maximum_mono, List.argmin, OrderDual
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
m : α
rw :
  (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → idxOf m l ≤ idxOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
⊢ l.maximum = (↑m : WithBot α) ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Tactic:
rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]

Premises used: List.maximum, List.argmax_eq_some_iff, WithBot.some_eq_coe
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
m : α
simp : m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → idxOf m l ≤ idxOf a l
⊢ (m ∈ l ∧ (∀ (a : α), a ∈ l → id a ≤ id m) ∧ ∀ (a : α), a ∈ l → id m ≤ id a → idxOf m l ≤ idxOf a l) ↔
    m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m

Tactic:
simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]

Premises used: and_congr_right_iff, and_iff_left_iff_imp, id_eq
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
m : α
h_1 : m ∈ l
h : ∀ (a : α), a ∈ l → a ≤ m
a : α
hal : a ∈ l
hma : m ≤ a
rw rw₁ : idxOf a l ≤ idxOf a l
⊢ idxOf m l ≤ idxOf a l

Tactic:
rw [_root_.le_antisymm hma (h a hal)]

Premises used: le_antisymm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
m : α
⊢ l.minimum = (↑m : WithTop α) ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → m ≤ a

Tactic:
@maximum_eq_coe_iff αᵒᵈ _ _ _

Premises used: List.minimum, WithTop.some, List.argmin, OrderDual, List.maximum_eq_coe_iff, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
nil : (↑a : WithBot α) ≤ maximum [] ↔ ∃ (b : α), Membership.mem (γ := List α) [] b ∧ a ≤ b
cons :
  ∀ (head : α) (tail : List α),
    ((↑a : WithBot α) ≤ tail.maximum ↔ ∃ (b : α), b ∈ tail ∧ a ≤ b) →
      ((↑a : WithBot α) ≤ (head :: tail).maximum ↔ ∃ (b : α), b ∈ head :: tail ∧ a ≤ b)
⊢ (↑a : WithBot α) ≤ l.maximum ↔ ∃ (b : α), b ∈ l ∧ a ≤ b

Tactic:
induction l
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
⊢ (↑a : WithBot α) ≤ maximum [] ↔ ∃ (b : α), Membership.mem (γ := List α) [] b ∧ a ≤ b

Tactic:
simp [maximum_cons, *]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a head : α
tail : List α
tail_ih : (↑a : WithBot α) ≤ tail.maximum ↔ ∃ (b : α), b ∈ tail ∧ a ≤ b
⊢ (↑a : WithBot α) ≤ (head :: tail).maximum ↔ ∃ (b : α), b ∈ head :: tail ∧ a ≤ b

Tactic:
simp [maximum_cons, *]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
nil : minimum [] ≤ (↑a : WithTop α) ↔ ∃ (b : α), Membership.mem (γ := List α) [] b ∧ b ≤ a
cons :
  ∀ (head : α) (tail : List α),
    (tail.minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ tail ∧ b ≤ a) →
      ((head :: tail).minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ head :: tail ∧ b ≤ a)
⊢ l.minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ l ∧ b ≤ a

Tactic:
induction l
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
⊢ minimum [] ≤ (↑a : WithTop α) ↔ ∃ (b : α), Membership.mem (γ := List α) [] b ∧ b ≤ a

Tactic:
simp [minimum_cons, *]

Premises used: List.minimum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a head : α
tail : List α
tail_ih : tail.minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ tail ∧ b ≤ a
⊢ (head :: tail).minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ head :: tail ∧ b ≤ a

Tactic:
simp [minimum_cons, *]

Premises used: List.minimum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : l ≠ []
head : α
tail : List α
h_1 : head :: tail ≠ []
⊢ (head :: tail).maximum ≠ ⊥

Tactic:
simp [maximum_cons]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : l ≠ []
⊢ l.minimum ≠ ⊤

Tactic:
@maximum_ne_bot_of_ne_nil αᵒᵈ _ _ h

Premises used: List.maximum_ne_bot_of_ne_nil, List.minimum, List.argmin, OrderDual, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : 0 < l.length
head : α
tail : List α
h_1 : 0 < (head :: tail).length
⊢ (head :: tail).maximum ≠ ⊥

Tactic:
simp [maximum_cons]

Premises used: List.maximum_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : 0 < l.length
⊢ l.minimum ≠ ⊤

Tactic:
maximum_ne_bot_of_length_pos (α := αᵒᵈ) h

Premises used: List.minimum, List.maximum_ne_bot_of_length_pos, List.argmin, OrderDual, WithTop
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : 0 < l.length
⊢ (↑(maximum_of_length_pos h) : WithBot α) = l.maximum

Tactic:
WithBot.coe_unbot _ _

Premises used: WithBot.coe_unbot, List.maximum_of_length_pos