awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have 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
Tactic: subst hm
Cleared hypotheses: m, ham, hm
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have 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
Tactic: subst hm
Cleared hypotheses: m, ham, hm
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
have neg : LE.le (α := ℕ) 0 0
Tactic: rw [if_pos rfl]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (if hd = val then 0 else idxOf val tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have pos : idxOf val tl + 1 ≤ idxOf a tl + 1
Tactic: rw [if_neg, if_neg]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (if hd = val then 0 else idxOf val tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have pos₁ : ¬hd = a
Tactic: rw [if_neg, if_neg]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (if hd = val then 0 else idxOf val tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have pos₂ : ¬hd = val
Tactic: rw [if_neg, if_neg]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (if hd = hd then 0 else idxOf hd tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have neg : 0 ≤ if hd = a then 0 else idxOf a tl + 1
Tactic: rw [if_pos rfl]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ m ∈ argmax f l
have none : ∀ (harg : argmax f l = none), Membership.mem (γ := Option α) none m
Tactic: rcases harg : argmax f l with - | n
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ m ∈ argmax f l
have some : ∀ (n : α) (harg : argmax f l = some n), m ∈ some n
Tactic: rcases harg : argmax f l with - | n
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
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
⊢ m ∈ some n
have this : 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)))
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
this : idxOf m l = idxOf n l
⊢ m ∈ some n
have some : n ∈ some n
Tactic: rw [(idxOf_inj hml).1 this, Option.mem_def]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ m ∈ Option.some n
have some₁ : Option.some n = Option.some n
Tactic: rw [(idxOf_inj hml).1 this, Option.mem_def]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
⊢ ¬l.maximum < (↑a : WithBot α)
have bot : ∀ (h : l.maximum = ⊥), ¬⊥ < (↑a : WithBot α)
Tactic: cases h : l.maximum
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
bot : ∀ (h : l.maximum = ⊥), ¬⊥ < (↑a : WithBot α)
⊢ ¬l.maximum < (↑a : WithBot α)
have coe : ∀ (a_1 : α) (h : l.maximum = (↑a_1 : WithBot α)), ¬(↑a_1 : WithBot α) < (↑a : WithBot α)
Tactic: cases h : l.maximum
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
⊢ ¬(↑a : WithTop α) < l.minimum
have top : ∀ (h : l.minimum = ⊤), ¬(↑a : WithTop α) < ⊤
Tactic: cases h : l.minimum
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableLT α
l : List α
a : α
ha : a ∈ l
top : ∀ (h : l.minimum = ⊤), ¬(↑a : WithTop α) < ⊤
⊢ ¬(↑a : WithTop α) < l.minimum
have coe : ∀ (a_1 : α) (h : l.minimum = (↑a_1 : WithTop α)), ¬(↑a : WithTop α) < (↑a_1 : WithTop α)
Tactic: cases h : l.minimum
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
⊢ (l ++ [a]).maximum = max l.maximum (↑a : WithBot α)
have 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 α)
Tactic: simp only [maximum, argmax_concat, id]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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)
      (argmax id l) =
    max (argmax id l) (↑a : WithBot α)
have none : 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: cases argmax id l
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l : List α
none :
  Option.rec (motive := fun (x : Option α) ↦ Option α) (some a) (fun (val : α) ↦ if val < a then some a else some val)
      Option.none =
    max Option.none (↑a : WithBot α)
⊢ 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 α)
have some : ∀ (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: cases argmax id l
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a : WithBot α) tl.maximum
⊢ (a :: (tl ++ [hd])).maximum = max (↑a : WithBot α) (tl ++ [hd]).maximum
have rw : (a :: tl ++ [hd]).maximum = max (↑a : WithBot α) (tl ++ [hd]).maximum
Tactic: rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (a :: (tl ++ [hd])).maximum = max (↑a : WithBot α) (tl ++ [hd]).maximum
have rw₁ : max (a :: tl).maximum (↑hd : WithBot α) = max (↑a : WithBot α) (tl ++ [hd]).maximum
Tactic: rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (a :: (tl ++ [hd])).maximum = max (↑a : WithBot α) (tl ++ [hd]).maximum
have rw₂ : max (max (↑a : WithBot α) tl.maximum) (↑hd : WithBot α) = max (↑a : WithBot α) (tl ++ [hd]).maximum
Tactic: rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (a :: (tl ++ [hd])).maximum = max (↑a : WithBot α) (tl ++ [hd]).maximum
have rw₃ : max (max (↑a : WithBot α) tl.maximum) (↑hd : WithBot α) = max (↑a : WithBot α) (max tl.maximum (↑hd : WithBot α))
Tactic: rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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 α))
⊢ (a :: (tl ++ [hd])).maximum = max (↑a : WithBot α) (tl ++ [hd]).maximum
have rw₄ : max (↑a : WithBot α) (max tl.maximum (↑hd : WithBot α)) = max (↑a : WithBot α) (max tl.maximum (↑hd : WithBot α))
Tactic: rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l₂ : List α
head : α
tail : List α
ih : (tail ++ l₂).maximum = max tail.maximum l₂.maximum
⊢ (head :: tail ++ l₂).maximum = max (head :: tail).maximum l₂.maximum
have cons : (head :: tail ++ l₂).maximum = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
Tactic: rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (head :: tail ++ l₂).maximum = max (head :: tail).maximum l₂.maximum
have cons₁ : (head :: (tail ++ l₂)).maximum = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
Tactic: rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (head :: tail ++ l₂).maximum = max (head :: tail).maximum l₂.maximum
have cons₂ : max (↑head : WithBot α) (tail ++ l₂).maximum = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
Tactic: rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (head :: tail ++ l₂).maximum = max (head :: tail).maximum l₂.maximum
have cons₃ : max (↑head : WithBot α) (max tail.maximum l₂.maximum) = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
Tactic: rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ (head :: tail ++ l₂).maximum = max (head :: tail).maximum l₂.maximum
have cons₄ : max (max (↑head : WithBot α) tail.maximum) l₂.maximum = max (max (↑head : WithBot α) tail.maximum) l₂.maximum
Tactic: rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum
have nil : ([] ++ l₂).maximum = max (maximum []) l₂.maximum
Tactic: induction l₁ with
  | nil => simp
  | cons _ _ ih => rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l₁ l₂ : List α
nil : ([] ++ l₂).maximum = max (maximum []) l₂.maximum
⊢ (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum
have cons : ∀ (head : α) (tail : List α) (ih : (tail ++ l₂).maximum = max tail.maximum l₂.maximum),
  (head :: tail ++ l₂).maximum = max (head :: tail).maximum l₂.maximum
Tactic: induction l₁ with
  | nil => simp
  | cons _ _ ih => rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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 :: l).maximum ≤ b
have cons : (↑a : WithBot α) ≤ b ∧ l.maximum ≤ b
Tactic: simp only [maximum_cons, max_le_iff]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ l → (↑a : WithBot α) ≤ b
⊢ l.maximum ≤ b
have nil : ∀ (h : ∀ (a : α), Membership.mem (γ := List α) [] a → (↑a : WithBot α) ≤ b), 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))⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ l.maximum ≤ b
have 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
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))⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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 :: l).minimum
have cons : b ≤ (↑a : WithTop α) ∧ b ≤ l.minimum
Tactic: simp only [minimum_cons, le_min_iff]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
b : WithTop α
h : ∀ (a : α), a ∈ l → b ≤ (↑a : WithTop α)
⊢ b ≤ l.minimum
have nil : ∀ (h : ∀ (a : α), Membership.mem (γ := List α) [] a → b ≤ (↑a : WithTop α)), b ≤ 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))⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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 []
⊢ b ≤ l.minimum
have 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
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))⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
m : α
⊢ l.maximum = (↑m : WithBot α) ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
have 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
Tactic: rw [maximum, ← WithBot.some_eq_coe, argmax_eq_some_iff]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
m : α
⊢ (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
have simp : m ∈ l → (∀ (a : α), a ∈ l → a ≤ m) → ∀ (a : α), a ∈ l → m ≤ a → idxOf m l ≤ idxOf a l
Tactic: simp only [id_eq, and_congr_right_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ idxOf m l ≤ idxOf a l
have rw : idxOf a l ≤ idxOf a l
Tactic: rw [_root_.le_antisymm hma (h a hal)]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
⊢ (↑a : WithBot α) ≤ l.maximum ↔ ∃ (b : α), b ∈ l ∧ a ≤ b
have nil : (↑a : WithBot α) ≤ maximum [] ↔ ∃ (b : α), Membership.mem (γ := List α) [] b ∧ a ≤ b
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
nil : (↑a : WithBot α) ≤ maximum [] ↔ ∃ (b : α), Membership.mem (γ := List α) [] b ∧ a ≤ b
⊢ (↑a : WithBot α) ≤ l.maximum ↔ ∃ (b : α), b ∈ l ∧ a ≤ b
have cons : ∀ (head : α) (tail : List α),
  ((↑a : WithBot α) ≤ tail.maximum ↔ ∃ (b : α), b ∈ tail ∧ a ≤ b) →
    ((↑a : WithBot α) ≤ (head :: tail).maximum ↔ ∃ (b : α), b ∈ head :: tail ∧ a ≤ b)
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
⊢ l.minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ l ∧ b ≤ a
have nil : minimum [] ≤ (↑a : WithTop α) ↔ ∃ (b : α), Membership.mem (γ := List α) [] b ∧ b ≤ a
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
nil : minimum [] ≤ (↑a : WithTop α) ↔ ∃ (b : α), Membership.mem (γ := List α) [] b ∧ b ≤ a
⊢ l.minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ l ∧ b ≤ a
have cons : ∀ (head : α) (tail : List α),
  (tail.minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ tail ∧ b ≤ a) →
    ((head :: tail).minimum ≤ (↑a : WithTop α) ↔ ∃ (b : α), b ∈ head :: tail ∧ b ≤ a)
Tactic: induction l
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
h : 0 < l.length
⊢ maximum_of_length_pos h ∈ l
have a : l.maximum = (↑(maximum_of_length_pos h) : WithBot α)
Tactic: apply maximum_mem
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
a : α
h : a ∈ l
w : 0 < l.length
⊢ a ≤ maximum_of_length_pos w
have simp : (↑a : WithBot α) ≤ l.maximum
Tactic: simp only [le_maximum_of_length_pos_iff]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l : List α
i : ℕ
w : i < l.length
h : 0 < l.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i w ≤ maximum_of_length_pos h
have h₁ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i w ∈ l
Tactic: apply le_maximum_of_length_pos_of_mem
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
⊢ l.maximum = l'.maximum
have nil : Eq.{u_1 + 1} (α := WithBot α) (maximum []) (maximum [])
Tactic: induction h with grind [maximum_cons]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
nil : Eq.{u_1 + 1} (α := WithBot α) (maximum []) (maximum [])
⊢ l.maximum = l'.maximum
have cons : ∀ (x : α) {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.maximum = l₂.maximum → (x :: l₁).maximum = (x :: l₂).maximum
Tactic: induction h with grind [maximum_cons]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
nil : Eq.{u_1 + 1} (α := WithBot α) (maximum []) (maximum [])
cons : ∀ (x : α) {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.maximum = l₂.maximum → (x :: l₁).maximum = (x :: l₂).maximum
⊢ l.maximum = l'.maximum
have swap : ∀ (x y : α) (l : List α), (y :: x :: l).maximum = (x :: y :: l).maximum
Tactic: induction h with grind [maximum_cons]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
nil : Eq.{u_1 + 1} (α := WithBot α) (maximum []) (maximum [])
cons : ∀ (x : α) {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.maximum = l₂.maximum → (x :: l₁).maximum = (x :: l₂).maximum
swap : ∀ (x y : α) (l : List α), (y :: x :: l).maximum = (x :: y :: l).maximum
⊢ l.maximum = l'.maximum
have trans : ∀ {l₁ l₂ l₃ : List α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁.maximum = l₂.maximum → l₂.maximum = l₃.maximum → l₁.maximum = l₃.maximum
Tactic: induction h with grind [maximum_cons]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
⊢ l.minimum = l'.minimum
have nil : Eq.{u_1 + 1} (α := WithTop α) (minimum []) (minimum [])
Tactic: induction h with grind [minimum_cons]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
inst : LinearOrder α
l l' : List α
h : l ~ l'
nil : Eq.{u_1 + 1} (α := WithTop α) (minimum []) (minimum [])
⊢ l.minimum = l'.minimum
have cons : ∀ (x : α) {l₁ l₂ : List α}, l₁ ~ l₂ → l₁.minimum = l₂.minimum → (x :: l₁).minimum = (x :: l₂).minimum
Tactic: induction h with grind [minimum_cons]
Cleared hypotheses: h