induction l generalizing l' with
| nil => exact Nat.zero_le _
| cons a l IH =>
  let .cons nodup_head (nodup_tail : l.Nodup) := nodup
  simp only [countP_cons]
  cases hpa : p a <;> simp only [if_pos, if_neg, Nat.add_zero]
  . refine IH (subset_of_cons_subset hsub) nodup_tail
  let l'' := l'.erase a
  have : l ⊆ l'' := fun b h => by
    simp only [List.mem_erase_of_ne (nodup_head b h).symm]
    specialize @hsub b
    simp only [List.mem_cons] at hsub
    exact hsub <| Or.inr h
  specialize IH this nodup_tail
  refine trans (s:=Eq) (Nat.succ_le_succ IH) ?_
  refine Eq.symm <| countP_erase_true ?_ hpa
  exact (cons_subset.mp hsub).1
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
l l' : List α
hsub : l ⊆ l'
nodup : Nodup l
⊢ countP p l ≤ countP p l'
no goals