no goals
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a m : α
l : List α
⊢ ∀ (a m : α), m ∈ foldl (argAux r) (some a) [] → m ∈ [a]
simp [eq_comm]
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a m : α
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])
intro tl hd ih a m
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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 (fun a b => Option.rec (some b) (fun val => if r b val then some b else some val) a) (some a) tl) →
    m ∈ a :: (tl ++ [hd])
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
simp only [foldl_append, foldl_cons, foldl_nil, argAux]
case none
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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 (fun a b => Option.rec (some b) (fun val => if r b val then some b else some val) a) (some a) tl) →
    m ∈ a :: (tl ++ [hd])
cases hf : foldl (argAux r) (some a) tl
no goals
case none
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
simp (config := { contextual := true })
case some
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
case some
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
dsimp only
case some.inl
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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 some.inr
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
case some
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
split_ifs
no goals
case some.inl
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
simp (config := { contextual := true })
case some.inr
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
case some.inr
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
simp only [List.mem_cons] at ih
case some.inr.inl
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a m✝ : α
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 some.inr.inr
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
case some.inr
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
rcases ih _ _ hf with rfl | H
no goals
case some.inr.inl
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a m✝ : α
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])
simp (config := { contextual := true }) only [Option.mem_def, Option.some.injEq,
  find?, eq_comm, mem_cons, mem_append, mem_singleton, true_or, implies_true]
no goals
case some.inr.inr
α : Type u_1
β : Type ?u.6653
r : α → α → Prop
inst✝ : DecidableRel r
l✝ : List α
o : Option α
a✝ m✝ : α
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])
simp (config := { contextual := true }) [@eq_comm _ _ m, H]