awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
atl : List α
head_1 : β
btl : List β
⊢ zipWithLeft Prod.mk atl btl = (zipWithLeft' Prod.mk atl btl).fst

Tactic:
exact zipLeft_eq_zipLeft' atl btl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
bs : List β
head : α
atl : List α
cons :
  Eq (α := List (Prod.{u, v} α (Option β))) (zipWithLeft Prod.mk (head :: atl) [])
    (Prod.fst (zipWithLeft' Prod.mk (head :: atl) []))
cons₁ :
  ∀ (head_1 : β) (btl : List β),
    zipWithLeft Prod.mk (head :: atl) (head_1 :: btl) = (zipWithLeft' Prod.mk (head :: atl) (head_1 :: btl)).fst
⊢ zipWithLeft Prod.mk (head :: atl) bs = (zipWithLeft' Prod.mk (head :: atl) bs).fst

Tactic:
cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl

Premises used: List.zipWithLeft, List.cons_inj_right, List.cons, List.zipWithLeft', List.nil
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
as : List α
bs : List β
nil : Eq (α := List (Prod.{u, v} α (Option β))) (zipWithLeft Prod.mk [] bs) (Prod.fst (zipWithLeft' Prod.mk [] bs))
cons : ∀ (head : α) (atl : List α), zipWithLeft Prod.mk (head :: atl) bs = (zipWithLeft' Prod.mk (head :: atl) bs).fst
⊢ zipWithLeft Prod.mk as bs = (zipWithLeft' Prod.mk as bs).fst

Tactic:
cases as with
  | nil => rfl
  | cons _ atl =>
    cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl

Premises used: List.zipWithLeft, List.cons_inj_right, List.cons, List.zipWithLeft', List.nil
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
bs : List β
nil : Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] []) (map (fun (b : β) ↦ (none, b)) [])
cons :
  ∀ (head : β) (tail : List β),
    Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] (head :: tail))
      (map (fun (b : β) ↦ (none, b)) (head :: tail))
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (map (fun (b : β) ↦ (none, b)) bs)

Tactic:
cases bs
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] []) (map (fun (b : β) ↦ (none, b)) [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : β
tail : List β
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] (head :: tail)) (map (fun (b : β) ↦ (none, b)) (head :: tail))

Tactic:
rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
as : List α
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (as.zipRight []) []

Tactic:
rfl

Premises used: List.zipWithLeft, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
b : β
bs : List β
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] (b :: bs)) ((none, b) :: map (fun (b : β) ↦ (none, b)) bs)

Tactic:
rfl

Premises used: List.zipWithLeft, List.map, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
a : α
as : List α
b : β
bs : List β
⊢ (a :: as).zipRight (b :: bs) = (some a, b) :: as.zipRight bs

Tactic:
rfl

Premises used: List.zipWithLeft, rfl
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
as : List α
bs : List β
nil : ∀ (bs : List β), Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (Prod.fst (zipRight' [] bs))
cons :
  ∀ (head : α) (tail : List α),
    (∀ (bs : List β), tail.zipRight bs = (tail.zipRight' bs).fst) →
      ∀ (bs : List β), (head :: tail).zipRight bs = ((head :: tail).zipRight' bs).fst
⊢ as.zipRight bs = (as.zipRight' bs).fst

Tactic:
induction as generalizing bs
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
bs : List β
nil : Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] []) (Prod.fst (zipRight' [] []))
nil₁ :
  ∀ (head : β) (tail : List β),
    Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] (head :: tail)) (Prod.fst (zipRight' [] (head :: tail)))
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] bs) (Prod.fst (zipRight' [] bs))

Tactic:
cases bs
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
tail : List α
tail_ih : ∀ (bs : List β), tail.zipRight bs = (tail.zipRight' bs).fst
bs : List β
cons : Eq (α := List (Prod.{u, v} (Option α) β)) ((head :: tail).zipRight []) (Prod.fst ((head :: tail).zipRight' []))
cons₁ :
  ∀ (head_1 : β) (tail_1 : List β),
    (head :: tail).zipRight (head_1 :: tail_1) = ((head :: tail).zipRight' (head_1 :: tail_1)).fst
⊢ (head :: tail).zipRight bs = ((head :: tail).zipRight' bs).fst

Tactic:
cases bs
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] []) (Prod.fst (zipRight' [] []))

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : β
tail : List β
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) (zipRight [] (head :: tail)) (Prod.fst (zipRight' [] (head :: tail)))

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
tail : List α
tail_ih : ∀ (bs : List β), tail.zipRight bs = (tail.zipRight' bs).fst
⊢ Eq (α := List (Prod.{u, v} (Option α) β)) ((head :: tail).zipRight []) (Prod.fst ((head :: tail).zipRight' []))

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Map2
Goal:
α : Type u
β : Type v
head : α
tail : List α
tail_ih : ∀ (bs : List β), tail.zipRight bs = (tail.zipRight' bs).fst
head_1 : β
tail_1 : List β
⊢ (head :: tail).zipRight (head_1 :: tail_1) = ((head :: tail).zipRight' (head_1 :: tail_1)).fst

Tactic:
simp [*]
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
⊢ foldl (argAux r) o [] = none ↔ Eq.{u_1 + 1} (α := List α) [] [] ∧ o = none

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
simp :
  (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (Eq (α := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
            (fun (val : α) ↦ if r hd val then some hd else some val) (foldl (argAux r) o tl) :
          Option α)
        (none : Option α) ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)

Tactic:
simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil_iff]

Premises used: List.argAux, List.append_eq_nil_iff, List.foldl_nil, List.foldl_append, List.foldl_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
none :
  (Eq.{u_1 + 1} (α := Option α) Option.none Option.none ↔ tl = [] ∧ o = Option.none) →
    (Eq.{u_1 + 1} (α := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some hd)
            (fun (val : α) ↦ if r hd val then Option.some hd else Option.some val) Option.none :
          Option α)
        (Option.none : Option α) ↔
      (tl = [] ∧ [hd] = []) ∧ o = Option.none)
some :
  ∀ (val : α),
    (Option.some val = Option.none ↔ tl = [] ∧ o = Option.none) →
      (Eq (α := Option α)
          (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some hd)
              (fun (val : α) ↦ if r hd val then Option.some hd else Option.some val) (Option.some val) :
            Option α)
          (Option.none : Option α) ↔
        (tl = [] ∧ [hd] = []) ∧ o = Option.none)
⊢ (foldl (argAux r) o tl = Option.none ↔ tl = [] ∧ o = Option.none) →
    (Eq (α := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some hd)
            (fun (val : α) ↦ if r hd val then Option.some hd else Option.some val) (foldl (argAux r) o tl) :
          Option α)
        (Option.none : Option α) ↔
      (tl = [] ∧ [hd] = []) ∧ o = Option.none)

Tactic:
cases foldl (argAux r) o tl

Premises used: List.argAux, List.foldl
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (Eq.{u_1 + 1} (α := Option α) none none ↔ tl = [] ∧ o = none) →
    (Eq.{u_1 + 1} (α := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (some hd)
            (fun (val : α) ↦ if r hd val then some hd else some val) none :
          Option α)
        (none : Option α) ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd val : α
pos : r hd val → (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)
neg : ¬r hd val → (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)
⊢ (some val = none ↔ tl = [] ∧ o = none) →
    ((if r hd val then some hd else some val) = none ↔ (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
split_ifs
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd val : α
h : r hd val
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
o : Option α
tl : List α
hd val : α
h : ¬r hd val
⊢ (False ↔ tl = [] ∧ o = none) → (False ↔ (tl = [] ∧ False) ∧ o = none)

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) [] → m ∈ [a]

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l l_1 : List α
_ :
  ∀ (a : α),
    (∀ (a m : α), m ∈ foldl (argAux r) (some a) l_1 → m ∈ a :: l_1) →
      ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l_1 ++ [a]) → m ∈ a_2 :: (l_1 ++ [a])
⊢ ∀ (a : α),
    (∀ (a m : α), m ∈ foldl (argAux r) (some a) l_1 → m ∈ a :: l_1) →
      ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l_1 ++ [a]) → m ∈ a_2 :: (l_1 ++ [a])

Tactic:
_
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l l_1 : List α
a : α
_ :
  (∀ (a m : α), m ∈ foldl (argAux r) (some a) l_1 → m ∈ a :: l_1) →
    ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l_1 ++ [a]) → m ∈ a_2 :: (l_1 ++ [a])
⊢ (∀ (a m : α), m ∈ foldl (argAux r) (some a) l_1 → m ∈ a :: l_1) →
    ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l_1 ++ [a]) → m ∈ a_2 :: (l_1 ++ [a])

Tactic:
_
-- Module: Mathlib.Data.List.MinMax
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 : α), m ∈ foldl (argAux r) (some a_1) (l_1 ++ [a]) → m ∈ a_1 :: (l_1 ++ [a])
⊢ ∀ (a_1 m : α), m ∈ foldl (argAux r) (some a_1) (l_1 ++ [a]) → m ∈ a_1 :: (l_1 ++ [a])

Tactic:
_
-- Module: Mathlib.Data.List.MinMax
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 : α
simp :
  ∀ (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])
⊢ ∀ (m : α), m ∈ foldl (argAux r) (some a_1) (l_1 ++ [a]) → m ∈ a_1 :: (l_1 ++ [a])

Tactic:
simp only [foldl_append, foldl_cons, foldl_nil, argAux]

Premises used: List.argAux, List.foldl_nil, List.foldl_append, List.foldl_cons
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l l_1 : List α
a : α
h : ∀ (a m : α), m ∈ foldl (argAux r) (Option.some a) l_1 → m ∈ a :: l_1
a_1 : α
none :
  foldl (argAux r) (Option.some a_1) l_1 = Option.none →
    ∀ (m : α),
      Membership.mem (γ := Option α)
          (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
              (fun (val : α) ↦ if r a val then Option.some a else Option.some val) Option.none :
            Option α)
          m →
        m ∈ a_1 :: (l_1 ++ [a])
some :
  ∀ (val : α),
    foldl (argAux r) (Option.some a_1) l_1 = Option.some val →
      ∀ (m : α),
        Membership.mem (γ := Option α)
            (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
                (fun (val : α) ↦ if r a val then Option.some a else Option.some val) (Option.some val) :
              Option α)
            m →
          m ∈ a_1 :: (l_1 ++ [a])
⊢ ∀ (m : α),
    Membership.mem (γ := Option α)
        (Option.rec (motive := fun (x : Option α) ↦ Option α) (Option.some a)
            (fun (val : α) ↦ if r a val then Option.some a else Option.some val)
            (foldl (argAux r) (Option.some a_1) l_1) :
          Option α)
        m →
      m ∈ a_1 :: (l_1 ++ [a])

Tactic:
cases _ : foldl _ _ _

Premises used: List.foldl
-- Module: Mathlib.Data.List.MinMax
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 : α
h_1 : 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:
grind
-- Module: Mathlib.Data.List.MinMax
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 val : α
h_1 : 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:
grind
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
hr₀ : Std.Irrefl r
a : α
⊢ argAux r (some a) a = some a

Tactic:
if_neg <| hr₀.irrefl _

Premises used: Std.Irrefl.irrefl, List.argAux, if_neg
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, Membership.mem (γ := List α) [] a → m ∈ foldl (argAux r) o [] → ¬r a m

Tactic:
simp
-- Module: Mathlib.Data.List.MinMax
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
⊢ ∀ {a_1 m : α} {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m

Tactic:
?_
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
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
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

Tactic:
induction l using List.reverseRecOn with
  | nil => simp
  | append_singleton tl a ih => ?_

Premises used: List.nil
-- Module: Mathlib.Data.List.MinMax
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])
⊢ 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

Premises used: List.argAux, List.foldl_nil, List.foldl_append, List.foldl_cons
-- Module: Mathlib.Data.List.MinMax
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
append_singleton₁ : ∀ (c : α) (hf : foldl (argAux r) o tl = some c), ¬r b m
⊢ ¬r b m

Tactic:
rcases hf : foldl (argAux r) o tl with - | c

Premises used: List.argAux, List.foldl
-- Module: Mathlib.Data.List.MinMax
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
⊢ 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
-- Module: Mathlib.Data.List.MinMax
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
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
⊢ foldl (argAux r) o tl = none

Tactic:
rw [hf] at ho
-- Module: Mathlib.Data.List.MinMax
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
⊢ tl = [] ∧ o = none

Tactic:
rw [foldl_argAux_eq_none] at hf

Premises used: List.foldl_argAux_eq_none
-- Module: Mathlib.Data.List.MinMax
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 : tl = [] ∧ o = none
⊢ ¬r b m

Tactic:
simp_all [hf.1, hf.2, hr₀.irrefl _]

Premises used: Std.Irrefl.irrefl, And.right, And.left
-- Module: Mathlib.Data.List.MinMax
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
⊢ (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

Premises used: Option.mem_def
-- Module: Mathlib.Data.List.MinMax
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
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
⊢ foldl (argAux r) o tl = some c

Tactic:
rw [hf, Option.mem_def] at ho

Premises used: Option.mem_def
-- Module: Mathlib.Data.List.MinMax
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]
c : α
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
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

Tactic:
grind +splitIndPred
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
⊢ argmax f [] = none

Tactic:
rfl

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

Tactic:
rfl

Premises used: List.foldl, List.argmin, rfl
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
a : α
⊢ argmax f [a] = some a

Tactic:
rfl

Premises used: List.argAux, List.foldl, rfl, List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
a : α
⊢ argmin f [a] = some a

Tactic:
rfl

Premises used: List.argAux, List.foldl, List.argmin, rfl
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
l : List α
a m : α
⊢ a ∈ l → m ∈ argmax f l → ¬f m < f a

Tactic:
not_of_mem_foldl_argAux _ ⟨fun x h => lt_irrefl (f x) h⟩
    ⟨fun _ _ z hxy hyz => lt_trans (a := f z) hyz hxy⟩

Premises used: List.not_of_mem_foldl_argAux, lt_irrefl, IsTrans.mk, lt_trans, Std.Irrefl.mk, List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
l : List α
a m : α
⊢ a ∈ l → m ∈ argmin f l → ¬f a < f m

Tactic:
not_of_mem_foldl_argAux _ ⟨fun x h => lt_irrefl (f x) h⟩
    ⟨fun x _ _ hxy hyz => lt_trans (a := f x) hxy hyz⟩

Premises used: List.not_of_mem_foldl_argAux, lt_irrefl, IsTrans.mk, lt_trans, Std.Irrefl.mk, List.argmin
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
a : α
l : List α
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
⊢ 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

Tactic:
rw [argmax, argmax]

Premises used: List.argmax
-- Module: Mathlib.Data.List.MinMax
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : DecidableLT β
f : α → β
a : α
l : List α
⊢ 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:
simp [argAux]

Premises used: List.argAux