-- Mathlib/Data/List/MinMax.lean
theorem not_of_mem_foldl_argAux (hr₀ : Irreflexive r) (hr₁ : Transitive r) :
    ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

Proof state:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive 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:
intro b m o hb ho

Result:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive 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

Proof state:
case pos.inl
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b : α
o : Option α
hb : b ∈ tl ++ [a]
c : α
hf : foldl (argAux r) o tl = some c
hac : r a c
h : b ∈ tl
⊢ ¬r b a

Tactic:
exact fun hba => ih h hf (hr₁ hba hac)

Result:
no goals

Proof state:
case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive 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 ∈ Option.casesOn none (some a) fun c => if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m

Tactic:
rw [foldl_argAux_eq_none] at hf

Result:
case append_singleton.none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive 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 ∈ Option.casesOn none (some a) fun c => if r a c then some a else some c
hf : tl = [] ∧ o = none
⊢ ¬r b m

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive r
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

Tactic:
induction' l using List.reverseRecOn with tl a ih

Result:
case nil
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive r
⊢ ∀ {a m : α} {o : Option α}, a ∈ [] → m ∈ foldl (argAux r) o [] → ¬r a m

case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive 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

Proof state:
case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive 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 ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c => if r a c then some a else some c
c : α
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

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

Result:
case append_singleton.some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Irreflexive r
hr₁ : Transitive 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 (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