Counting in lists

This file proves basic properties of List.countP and List.count, which count the number of elements of a list satisfying a predicate and equal to a given element respectively.

theorem List.countP_erase {α : Type u_1} [DecidableEq α] (p : α → Bool) (l : List α) (a : α) : List.countP p (l.erase a) = List.countP p l - if a ∈ l ∧ p a = true then 1 else 0

theorem List.count_diff {α : Type u_1} [DecidableEq α] (a : α) (l₁ l₂ : List α) : List.count a (l₁.diff l₂) = List.count a l₁ - List.count a l₂

theorem List.countP_diff {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} (hl : l₂.Subperm l₁) (p : α → Bool) : List.countP p (l₁.diff l₂) = List.countP p l₁ - List.countP p l₂

@[simp]

theorem List.count_map_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (l : List α) (f : α → β) (hf : Function.Injective f) (x : α) : List.count (f x) (List.map f l) = List.count x l