-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem eraseP_eq_erasePTR : @eraseP = @erasePTR

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 h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = erasePTR p l

Tactic:
simp [erasePTR]

Result:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = erasePTR.go p l l #[]

Proof state:
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs →
    (bif p x then acc.toList ++ xs else erasePTR.go p l xs (acc.push x)) =
      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 → erasePTR.go p l xs (acc.push x) = acc.toList ++ x :: eraseP p xs

Proof state:
α : Type u_1
p : α → Bool
l : List α
acc : Array α
h : l = acc.toList ++ []
⊢ erasePTR.go p l [] acc = acc.toList ++ eraseP p []

Tactic:
simp [erasePTR.go, eraseP, 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 → erasePTR.go p l xs (acc.push x) = 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
⊢ erasePTR.go p l xs (acc.push x) = acc.toList ++ x :: eraseP p xs

Proof state:
⊢ @eraseP = @erasePTR

Tactic:
funext α p l

Result:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = erasePTR p l

Proof state:
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = erasePTR.go p l l #[]

Tactic:
exact (go #[] _ rfl).symm

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
⊢ (acc.push x).toList ++ eraseP 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
⊢ erasePTR.go p l xs (acc.push x) = 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
⊢ (acc.push x).toList ++ eraseP 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 α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs → erasePTR.go p l (x :: xs) acc = acc.toList ++ eraseP p (x :: xs)

Tactic:
simp [erasePTR.go, eraseP]

Result:
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.toList ++ x :: xs →
    (bif p x then acc.toList ++ xs else erasePTR.go p l xs (acc.push x)) =
      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
⊢ (acc.push x).toList ++ eraseP 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