no goals
α : Type u_1
β : Type ?u.246
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
⊢ foldl (argAux r) o [] = none ↔ [] = [] ∧ o = none
simp
α : Type u_1
β : Type ?u.246
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd : α
⊢ (foldl (fun a b => Option.rec (some b) (fun val => if r b val then some b else some val) a) o tl = none ↔
      tl = [] ∧ o = none) →
    ¬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) o tl) =
        none
α : Type u_1
β : Type ?u.246
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd : α
⊢ (foldl (argAux r) o tl = none ↔ tl = [] ∧ o = none) →
    (foldl (argAux r) o (tl ++ [hd]) = none ↔ tl ++ [hd] = [] ∧ o = none)
simp [argAux]
case some
α : Type u_1
β : Type ?u.246
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd val✝ : α
⊢ (tl = [] → ¬o = none) → ¬(if r hd val✝ then some hd else some val✝) = none
α : Type u_1
β : Type ?u.246
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd : α
⊢ (foldl (fun a b => Option.rec (some b) (fun val => if r b val then some b else some val) a) o tl = none ↔
      tl = [] ∧ o = none) →
    ¬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) o tl) =
        none
cases foldl (argAux r) o tl <;> simp
no goals
case some
α : Type u_1
β : Type ?u.246
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd val✝ : α
⊢ (tl = [] → ¬o = none) → ¬(if r hd val✝ then some hd else some val✝) = none
try split_ifs <;> simp
no goals
case some
α : Type u_1
β : Type ?u.246
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
o : Option α
a m : α
tl : List α
hd val✝ : α
⊢ (tl = [] → ¬o = none) → ¬(if r hd val✝ then some hd else some val✝) = none
split_ifs <;> simp