-- Mathlib/Data/List/MinMax.lean
theorem foldl_argAux_eq_none : l.foldl (argAux r) o = none ↔ l = [] ∧ o = none :=
  List.reverseRecOn l (by simp) fun tl hd => by
    simp only [foldl_append, foldl_cons, argAux, foldl_nil, append_eq_nil_iff, and_false, false_and,
      iff_false]
    cases foldl (argAux r) o tl
    · simp
    · simp only [false_iff, not_and]
      split_ifs <;> simp

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (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, and_false, false_and,
  iff_false]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val => if r hd val then some hd else some val) (foldl (argAux r) o tl) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Proof state:
case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (none = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val => if r hd val then some hd else some val) none = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val => if r hd val then some hd else some val) (foldl (argAux r) o tl) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
cases foldl (argAux r) o tl

Result:
case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd : α
⊢ (none = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val => if r hd val then some hd else some val) none = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val => if r hd val then some hd else some val) (some val✝) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Proof state:
case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    ((if r hd val✝ then some hd else some val✝) = none ↔ (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    (Option.rec (some hd) (fun val => if r hd val then some hd else some val) (some val✝) = none ↔
      (tl = [] ∧ [hd] = []) ∧ o = none)

Tactic:
simp only [false_iff, not_and]

Result:
case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
tl : List α
hd val✝ : α
⊢ (some val✝ = none ↔ tl = [] ∧ o = none) →
    ((if r hd val✝ then some hd else some val✝) = none ↔ (tl = [] ∧ [hd] = []) ∧ o = none)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
⊢ foldl (argAux r) o [] = none ↔ [] = [] ∧ o = none

Tactic:
simp

Result:
no goals