case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = erasePTR p l
⊢ @eraseP = @erasePTR
funext α p l
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = erasePTR.go p l l #[]
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = erasePTR p l
simp [erasePTR]
no goals
case h.h.h
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l = erasePTR.go p l l #[]
exact (go #[] _ rfl).symm
no goals
α : Type u_1
p : α → Bool
l : List α
acc : Array α
h : l = acc.data ++ []
⊢ erasePTR.go p l [] acc = acc.data ++ eraseP p []
simp [erasePTR.go, eraseP, h]
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.data ++ x :: xs →
    (bif p x then acc.data ++ xs else erasePTR.go p l xs (Array.push acc x)) =
      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 → erasePTR.go p l (x :: xs) acc = acc.data ++ eraseP p (x :: xs)
simp [erasePTR.go, eraseP]
case false
α : Type u_1
p : α → Bool
l : List α
acc : Array α
x : α
xs : List α
⊢ l = acc.data ++ x :: xs → erasePTR.go p l xs (Array.push acc x) = 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 acc.data ++ xs else erasePTR.go p l xs (Array.push acc x)) =
      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
⊢ erasePTR.go p l xs (Array.push acc x) = 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 → erasePTR.go p l xs (Array.push acc x) = 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
⊢ (Array.push acc x).data ++ eraseP 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
⊢ erasePTR.go p l xs (Array.push acc x) = 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
⊢ (Array.push acc x).data ++ eraseP 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]