awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l l_1 : List α
a : α
h : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l_1 → m ∈ a :: l_1
a_1 : α
⊢ ∀ (m : α),
    Membership.mem (γ := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some a)
            (fun (val : α) ↦ if r a val then some a else some val) (foldl (argAux r) (some a_1) l_1) :
          Option α)
        m →
      m ∈ a_1 :: (l_1 ++ [a])
have none : foldl (argAux r) (some a_1) l_1 = none →
  ∀ (m : α),
    Membership.mem (γ := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some a)
            (fun (val : α) ↦ if r a val then some a else some val) none :
          Option α)
        m →
      m ∈ a_1 :: (l_1 ++ [a])
Tactic: cases _ : foldl _ _ _
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l l_1 : List α
a : α
h : ∀ (a m : α), m ∈ foldl (argAux r) (some a) l_1 → m ∈ a :: l_1
a_1 : α
none :
  foldl (argAux r) (some a_1) l_1 = Option.none →
    ∀ (m : α),
      Membership.mem (γ := Option α)
          (Option.rec (motive := fun (x : Option α) ↦ Option α) (some a)
              (fun (val : α) ↦ if r a val then some a else some val) Option.none :
            Option α)
          m →
        m ∈ a_1 :: (l_1 ++ [a])
⊢ ∀ (m : α),
    Membership.mem (γ := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some a)
            (fun (val : α) ↦ if r a val then some a else some val) (foldl (argAux r) (some a_1) l_1) :
          Option α)
        m →
      m ∈ a_1 :: (l_1 ++ [a])
have some : ∀ (val : α),
  foldl (argAux r) (some a_1) l_1 = some val →
    ∀ (m : α),
      Membership.mem (γ := Option α)
          (Option.rec (motive := fun (x : Option α) ↦ Option α) (some a)
              (fun (val : α) ↦ if r a val then some a else some val) (some val) :
            Option α)
          m →
        m ∈ a_1 :: (l_1 ++ [a])
Tactic: cases _ : foldl _ _ _
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m
have append_singleton : ∀ (tl : List α) (a : α) (ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m) {a_1 m : α}
  {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m
Tactic: induction l using List.reverseRecOn with
  | nil => simp
  | append_singleton tl a ih => ?_
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ foldl (argAux r) o (tl ++ [a])
⊢ ¬r b m
have ho₁ : Membership.mem (γ := Option α)
  (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (foldl (argAux r) o tl) (some a) fun (c : α) ↦
      if r a c then some a else some c :
    Option α)
  m
Tactic: rw [foldl_append, foldl_cons, foldl_nil, argAux] at ho
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho :
  Membership.mem (γ := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (foldl (argAux r) o tl) (some a) fun (c : α) ↦
        if r a c then some a else some c :
      Option α)
    m
⊢ ¬r b m
have append_singleton : ∀ (hf : foldl (argAux r) o tl = none), ¬r b m
Tactic: rcases hf : foldl (argAux r) o tl with - | c
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho :
  Membership.mem (γ := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (foldl (argAux r) o tl) (some a) fun (c : α) ↦
        if r a c then some a else some c :
      Option α)
    m
append_singleton : ∀ (hf : foldl (argAux r) o tl = none), ¬r b m
⊢ ¬r b m
have append_singleton₁ : ∀ (c : α) (hf : foldl (argAux r) o tl = some c), ¬r b m
Tactic: rcases hf : foldl (argAux r) o tl with - | c
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho :
  Membership.mem (γ := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (foldl (argAux r) o tl) (some a) fun (c : α) ↦
        if r a c then some a else some c :
      Option α)
    m
hf : foldl (argAux r) o tl = none
⊢ ¬r b m
have ho₁ : Membership.mem (γ := Option α)
  (Option.casesOn (motive := fun (x : Option α) ↦ Option α) none (some a) fun (c : α) ↦
      if r a c then some a else some c :
    Option α)
  m
Tactic: rw [hf] at ho
Cleared hypotheses: ho, hf
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho :
  Membership.mem (γ := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) none (some a) fun (c : α) ↦
        if r a c then some a else some c :
      Option α)
    m
hf : foldl (argAux r) o tl = none
⊢ ¬r b m
have hf₁ : tl = [] ∧ o = none
Tactic: rw [foldl_argAux_eq_none] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho :
  Membership.mem (γ := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (foldl (argAux r) o tl) (some a) fun (c : α) ↦
        if r a c then some a else some c :
      Option α)
    m
c : α
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m
have ho₁ : (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (some c) (some a) fun (c : α) ↦
    if r a c then some a else some c) =
  some m
Tactic: rw [hf, Option.mem_def] at ho
Cleared hypotheses: ho, hf
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
a : α
l : List α
⊢ argmax f (l ++ [a]) =
    Option.casesOn (motive := fun (x : Option α) ↦ Option α) (argmax f l) (some a) fun (c : α) ↦
      if f c < f a then some a else some c
have rw : foldl (argAux fun (b c : α) ↦ f c < f b) none (l ++ [a]) =
  Option.casesOn (motive := fun (x : Option α) ↦ Option α) (foldl (argAux fun (b c : α) ↦ f c < f b) none l) (some a)
    fun (c : α) ↦ if f c < f a then some a else some c
Tactic: rw [argmax, argmax]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ 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
have 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 α)
Tactic: rw [← cons_append, argmax_concat, ih, argmax_concat]
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
⊢ 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 α)
have none : ∀ (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: rcases h : argmax f hd with - | m
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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
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 (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 α) 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 α)
⊢ 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 α)
have some : ∀ (m : α) (h : argmax f hd = some m),
  Eq.{u_1 + 1} (α := Option α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (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 α)
    (Option.casesOn (motive := fun (x : Option α) ↦ Option α)
        (Option.casesOn (motive := fun (x : Option α) ↦ Option α) (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 :
      Option α)
Tactic: rcases h : argmax f hd with - | m
-- Lean 4 proof step from Mathlib.Data.List.MinMax (goal)
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) (if f a < f m then some m else some a) :
      Option α)
    (Option.rec (motive := fun (x : Option α) ↦ Option α) (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) :
      Option α)
have some : 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: rw [← apply_ite, ← apply_ite]
-- 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 : α
hm : m ∈ argmax f (hd :: tl)
a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
⊢ idxOf m (hd :: tl) ≤ idxOf a (hd :: tl)
have 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
Tactic: simp only [idxOf_cons, argmax_cons, Option.mem_def] at hm ⊢
Cleared hypotheses: 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 : α
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
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
have none : ∀ (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: cases h : argmax f tl
-- 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 : α
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
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
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
have some : ∀ (val : α) (h : argmax f tl = some val),
  (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
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
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
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
have 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
Tactic: rw [h] at hm
Cleared hypotheses: hm, h
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
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
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
have 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
Tactic: rw [h] at hm
Cleared hypotheses: hm, h
-- 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 : α
ha : a ∈ hd :: tl
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
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
have some : (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
Tactic: simp only [cond_eq_ite, beq_iff_eq]
-- 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 : α
ha : a ∈ hd :: tl
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have 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
Tactic: obtain ha | ha := ha
Cleared hypotheses: a, ha, ham
-- 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 : α
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have some₁ : Mem a tl → (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
Cleared hypotheses: ha
-- 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 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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
have 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
Tactic: split_ifs at hm
Cleared hypotheses: 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 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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
have 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
Tactic: split_ifs at hm
Cleared hypotheses: 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 : α
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have 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
Tactic: split_ifs at hm
Cleared hypotheses: 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 : α
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have 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
Tactic: split_ifs at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
have hm₁ : val = m
Tactic: injection hm with hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
have hm₁ : hd = m
Tactic: injection hm with hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have hm₁ : val = m
Tactic: injection hm with hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.List.MinMax (hypothesis)
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
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = a then 0 else idxOf a tl + 1
have hm₁ : hd = m
Tactic: injection hm with hm
Cleared hypotheses: 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 val : α
h : argmax f tl = some val
ham : f m ≤ f hd
h_1 : f hd < f val
hm : val = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
have 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
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 val : α
h : argmax f tl = some val
ham : f m ≤ f hd
h_1 : ¬f hd < f val
hm : hd = m
⊢ (if hd = m then 0 else idxOf m tl + 1) ≤ if hd = hd then 0 else idxOf hd tl + 1
have 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
Tactic: subst hm
Cleared hypotheses: m, ham, hm