no goals
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
b : β
l : List β
⊢ eraseP p (map f (b :: l)) = map f (eraseP (p ∘ f) (b :: l))
by_cases h : p (f b) <;> simp [h, eraseP_map f l, eraseP_cons_of_pos]