-- 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.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 : (if r a c then some a else some c) = some m
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

Tactic:
split_ifs at ho with hac <;> rcases mem_append.1 hb with h | h <;>
  injection ho with ho <;> subst ho

Result:
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

case pos.inr
α : 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 ∈ [a]
⊢ ¬r b a

case neg.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 c

case neg.inr
α : 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 ∈ [a]
⊢ ¬r b c

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 : tl = [] ∧ o = none
⊢ ¬r b m

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

Result:
no goals

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
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
⊢ ¬r b m

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

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 (foldl (argAux r) o tl) (some a) fun c => if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m

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

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
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ foldl (argAux r) o (tl ++ [a])
⊢ ¬r b m

Tactic:
rw [foldl_append, foldl_cons, foldl_nil, argAux] at 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 ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c => if r a c then some a else some c
⊢ ¬r b m

Proof state:
case pos.inr
α : 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 ∈ [a]
⊢ ¬r b a

Tactic:
simp_all [hr₀ _]

Result:
no goals

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]
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

Tactic:
dsimp only 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 : (if r a c then some a else some c) = some m
hf : foldl (argAux r) o tl = some c
⊢ ¬r b m

Proof state:
case neg.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 c

Tactic:
exact ih h hf

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 (foldl (argAux r) o tl) (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 [hf] at ho

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 : foldl (argAux r) o tl = none
⊢ ¬r b m

Proof state:
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

Tactic:
simp

Result:
no goals

Proof state:
case neg.inr
α : 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 ∈ [a]
⊢ ¬r b c

Tactic:
simp_all

Result:
no goals