-- Mathlib/Data/List/MinMax.lean
theorem foldl_argAux_mem (l) : ∀ a m : α, m ∈ foldl (argAux r) (some a) l → m ∈ a :: l :=
  List.reverseRecOn l (by simp [eq_comm])
    (by
      intro tl hd ih a m
      simp only [foldl_append, foldl_cons, foldl_nil, argAux]
      cases hf : foldl (argAux r) (some a) tl
      · simp +contextual
      · dsimp only
        split_ifs
        · simp +contextual
        · -- `finish [ih _ _ hf]` closes this goal
          simp only [List.mem_cons] at ih
          rcases ih _ _ hf with rfl | H
          · simp +contextual only [Option.mem_def, Option.some.injEq,
              find?, eq_comm, mem_cons, mem_append, mem_singleton, true_or, implies_true]
          · simp +contextual [@eq_comm _ _ m, H])

Proof state:
case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
hf : foldl (argAux r) (some a) tl = none
⊢ m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) none → m ∈ a :: (tl ++ [hd])

Tactic:
simp +contextual

Result:
no goals

Proof state:
case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
⊢ m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) (some val✝) → m ∈ a :: (tl ++ [hd])

Tactic:
dsimp only

Result:
case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
⊢ (m ∈ if r hd val✝ then some hd else some val✝) → m ∈ a :: (tl ++ [hd])

Proof state:
case neg.inl
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd m val✝ : α
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
hf : foldl (argAux r) (some val✝) tl = some val✝
⊢ m ∈ some val✝ → m ∈ val✝ :: (tl ++ [hd])

Tactic:
simp +contextual only [Option.mem_def, Option.some.injEq,
  find?, eq_comm, mem_cons, mem_append, mem_singleton, true_or, implies_true]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) [] → m ∈ [a]

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
⊢ m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) (foldl (argAux r) (some a) tl) →
    m ∈ a :: (tl ++ [hd])

Tactic:
cases hf : foldl (argAux r) (some a) tl

Result:
case none
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
hf : foldl (argAux r) (some a) tl = none
⊢ m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) none → m ∈ a :: (tl ++ [hd])

case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
⊢ m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) (some val✝) → m ∈ a :: (tl ++ [hd])

Proof state:
case some
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
⊢ (m ∈ if r hd val✝ then some hd else some val✝) → m ∈ a :: (tl ++ [hd])

Tactic:
split_ifs

Result:
case pos
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : r hd val✝
⊢ m ∈ some hd → m ∈ a :: (tl ++ [hd])

case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])

Proof state:
case neg.inr
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
H : val✝ ∈ tl
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])

Tactic:
simp +contextual [@eq_comm _ _ m, H]

Result:
no goals

Proof state:
case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])

Tactic:
simp only [List.mem_cons] at ih

Result:
case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])

Proof state:
case pos
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : r hd val✝
⊢ m ∈ some hd → m ∈ a :: (tl ++ [hd])

Tactic:
simp +contextual

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (a m : α), m ∈ foldl (argAux r) (some a) l → m ∈ a :: l) →
      ∀ (a_2 m : α), m ∈ foldl (argAux r) (some a_2) (l ++ [a]) → m ∈ a_2 :: (l ++ [a])

Tactic:
intro tl hd ih a m

Result:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
⊢ m ∈ foldl (argAux r) (some a) (tl ++ [hd]) → m ∈ a :: (tl ++ [hd])

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
⊢ m ∈ foldl (argAux r) (some a) (tl ++ [hd]) → m ∈ a :: (tl ++ [hd])

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

Result:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd : α
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m ∈ a :: tl
a m : α
⊢ m ∈ Option.rec (some hd) (fun val => if r hd val then some hd else some val) (foldl (argAux r) (some a) tl) →
    m ∈ a :: (tl ++ [hd])

Proof state:
case neg
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])

Tactic:
rcases ih _ _ hf with rfl | H

Result:
case neg.inl
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd m val✝ : α
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
hf : foldl (argAux r) (some val✝) tl = some val✝
⊢ m ∈ some val✝ → m ∈ val✝ :: (tl ++ [hd])

case neg.inr
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l tl : List α
hd a m val✝ : α
hf : foldl (argAux r) (some a) tl = some val✝
h✝ : ¬r hd val✝
ih : ∀ (a m : α), m ∈ foldl (argAux r) (some a) tl → m = a ∨ m ∈ tl
H : val✝ ∈ tl
⊢ m ∈ some val✝ → m ∈ a :: (tl ++ [hd])