no goals
α : Type u_1
p : α → Bool
l : List α
⊢ extractP p l = (find? p l, eraseP p l)
exact go #[] _ rfl
no goals
α : Type u_1
p : α → Bool
l : List α
acc : Array α
h : l = acc.data ++ []
⊢ extractP.go p l [] acc = (find? p [], acc.data ++ eraseP p [])
simp [extractP.go, find?, eraseP, h]
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.data ++ x :: xs →
    (bif p x then (some x, acc.data ++ xs) else extractP.go p l xs (Array.push acc x)) =
      (match p x with
        | true => some x
        | false => find? p xs,
        acc.data ++ bif p x then xs else x :: eraseP p xs)
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.data ++ x :: xs → extractP.go p l (x :: xs) acc = (find? p (x :: xs), acc.data ++ eraseP p (x :: xs))
simp [extractP.go, find?, eraseP]
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.data ++ x :: xs → extractP.go p l xs (Array.push acc x) = (find? p xs, acc.data ++ x :: eraseP p xs)
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.data ++ x :: xs →
    (bif p x then (some x, acc.data ++ xs) else extractP.go p l xs (Array.push acc x)) =
      (match p x with
        | true => some x
        | false => find? p xs,
        acc.data ++ bif p x then xs else x :: eraseP p xs)
cases p x <;> simp
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.data ++ x :: xs
⊢ extractP.go p l xs (Array.push acc x) = (find? p xs, acc.data ++ x :: eraseP p xs)
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.data ++ x :: xs → extractP.go p l xs (Array.push acc x) = (find? p xs, acc.data ++ x :: eraseP p xs)
intro h
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.data ++ x :: xs
⊢ (find? p xs, (Array.push acc x).data ++ eraseP p xs) = (find? p xs, acc.data ++ x :: eraseP p xs)

case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.data ++ x :: xs
⊢ extractP.go p l xs (Array.push acc x) = (find? p xs, acc.data ++ x :: eraseP p xs)
rw [go _ xs]
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.data ++ x :: xs
⊢ (find? p xs, (Array.push acc x).data ++ eraseP p xs) = (find? p xs, acc.data ++ x :: eraseP p xs)

case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
{simp}
no goals
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp [h]