-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem extractP_eq_find?_eraseP
    (l : List α) : extractP p l = (find? p l, eraseP p l)

Proof state:
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs → extractP.go p l (x :: xs) acc = (find? p (x :: xs), acc.toList ++ eraseP p (x :: xs))

Tactic:
simp [extractP.go, find?, eraseP]

Result:
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs →
    (bif p x then (some x, acc.toList ++ xs) else extractP.go p l xs (acc.push x)) =
      (match p x with
        | true => some x
        | false => find? p xs,
        acc.toList ++ bif p x then xs else x :: eraseP p xs)

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.toList ++ x :: xs
⊢ (find? p xs, (acc.push x).toList ++ eraseP p xs) = (find? p xs, acc.toList ++ x :: eraseP p xs)

Tactic:
simp

Result:
no goals

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.toList ++ x :: xs
⊢ (find? p xs, (acc.push x).toList ++ eraseP p xs) = (find? p xs, acc.toList ++ x :: eraseP p xs)

case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.toList ++ x :: xs
⊢ l = (acc.push x).toList ++ xs

Tactic:
{simp}

Result:
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.toList ++ x :: xs
⊢ l = (acc.push x).toList ++ xs

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ extractP p l = (find? p l, eraseP p l)

Tactic:
exact go #[] _ rfl

Result:
no goals

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.toList ++ x :: xs
⊢ extractP.go p l xs (acc.push x) = (find? p xs, acc.toList ++ x :: eraseP p xs)

Tactic:
rw [go _ xs]

Result:
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.toList ++ x :: xs
⊢ (find? p xs, (acc.push x).toList ++ eraseP p xs) = (find? p xs, acc.toList ++ x :: eraseP p xs)

case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.toList ++ x :: xs
⊢ l = (acc.push x).toList ++ xs

Proof state:
α : Type u_1
p : α → Bool
l : List α
acc : Array α
h : l = acc.toList ++ []
⊢ extractP.go p l [] acc = (find? p [], acc.toList ++ eraseP p [])

Tactic:
simp [extractP.go, find?, eraseP, h]

Result:
no goals

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
h : l = acc.toList ++ x :: xs
⊢ l = (acc.push x).toList ++ xs

Tactic:
simp [h]

Result:
no goals

Proof state:
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs → extractP.go p l xs (acc.push x) = (find? p xs, acc.toList ++ x :: eraseP p xs)

Tactic:
intro h

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

Proof state:
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs →
    (bif p x then (some x, acc.toList ++ xs) else extractP.go p l xs (acc.push x)) =
      (match p x with
        | true => some x
        | false => find? p xs,
        acc.toList ++ bif p x then xs else x :: eraseP p xs)

Tactic:
cases p x <;> simp

Result:
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs → extractP.go p l xs (acc.push x) = (find? p xs, acc.toList ++ x :: eraseP p xs)