doc-next-gen

Init.Data.List.Count

Module docstring

{"# Lemmas about List.countP and List.count. ","### countP ","### count "}

List.countP_nil theorem
: countP p [] = 0
Full source 
@[simp] theorem countP_nil : countP p [] = 0 := rfl
Count of Satisfying Elements in Empty List is Zero
Informal description
For any predicate $p$, the count of elements satisfying $p$ in the empty list is $0$.
List.countP_go_eq_add theorem
{l} : countP.go p l n = n + countP.go p l 0
Full source 
protected theorem countP_go_eq_add {l} : countP.go p l n = n + countP.go p l 0 := by
  induction l generalizing n with
  | nil => rfl
  | cons hd _ ih =>
    unfold countP.go
    rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
    if h : p hd then simp [h, Nat.add_assoc] else simp [h]
Count of Satisfying Elements in List with Accumulator: $\text{countP.go}\ p\ l\ n = n + \text{countP.go}\ p\ l\ 0$
Informal description
For any predicate $p$, list $l$, and natural number $n$, the count of elements in $l$ satisfying $p$ starting from accumulator $n$ is equal to $n$ plus the count starting from accumulator $0$. That is, $\text{countP.go}\ p\ l\ n = n + \text{countP.go}\ p\ l\ 0$.
List.countP_cons_of_pos theorem
{l} (pa : p a) : countP p (a :: l) = countP p l + 1
Full source 
@[simp] theorem countP_cons_of_pos {l} (pa : p a) : countP p (a :: l) = countP p l + 1 := by
  have : countP.go p (a :: l) 0 = countP.go p l 1 := show cond .. = _ by rw [pa]; rfl
  unfold countP
  rw [this, Nat.add_comm, List.countP_go_eq_add]
Increment of Count in List Cons When Predicate Holds: $\text{countP}_p(a :: l) = \text{countP}_p(l) + 1$ if $p(a)$
Informal description
For any predicate $p$, any element $a$, and any list $l$, if $p(a)$ holds, then the count of elements satisfying $p$ in the list $a :: l$ is equal to the count of elements satisfying $p$ in $l$ plus one, i.e., $\text{countP}_p(a :: l) = \text{countP}_p(l) + 1$.
List.countP_cons_of_neg theorem
{l} (pa : ¬p a) : countP p (a :: l) = countP p l
Full source 
@[simp] theorem countP_cons_of_neg {l} (pa : ¬p a) : countP p (a :: l) = countP p l := by
  simp [countP, countP.go, pa]
Count Preservation in List Cons When Predicate Fails: $\text{countP}_p(a :: l) = \text{countP}_p(l)$ if $\neg p(a)$
Informal description
For any predicate `p`, any element `a`, and any list `l`, if `p a` does not hold (i.e., `¬p a`), then the count of elements satisfying `p` in the list `a :: l` is equal to the count of elements satisfying `p` in the list `l`. In other words, $\text{countP}_p(a :: l) = \text{countP}_p(l)$ when $p(a)$ is false.
List.countP_cons theorem
{a : α} {l : List α} : countP p (a :: l) = countP p l + if p a then 1 else 0
Full source 
theorem countP_cons {a : α} {l : List α} : countP p (a :: l) = countP p l + if p a then 1 else 0 := by
  by_cases h : p a <;> simp [h]
Count of Predicate in Cons List: $\text{countP}_p(a :: l) = \text{countP}_p(l) + \mathbb{1}_{p(a)}$
Informal description
For any predicate $p$, element $a$, and list $l$, the count of elements satisfying $p$ in the list $a :: l$ is equal to the count of elements satisfying $p$ in $l$ plus $1$ if $p(a)$ holds, and $0$ otherwise. That is, \[ \text{countP}_p(a :: l) = \text{countP}_p(l) + \begin{cases} 1 & \text{if } p(a) \\ 0 & \text{otherwise.} \end{cases} \]
List.countP_singleton theorem
{a : α} : countP p [a] = if p a then 1 else 0
Full source 
@[simp] theorem countP_singleton {a : α} : countP p [a] = if p a then 1 else 0 := by
  simp [countP_cons]
Count in Singleton List: $\text{countP}_p([a]) = \mathbb{1}_{p(a)}$
Informal description
For any predicate $p$ and element $a$, the count of elements satisfying $p$ in the singleton list $[a]$ is $1$ if $p(a)$ holds and $0$ otherwise, i.e., \[ \text{countP}_p([a]) = \begin{cases} 1 & \text{if } p(a) \\ 0 & \text{otherwise.} \end{cases} \]
List.length_eq_countP_add_countP theorem
(p : α → Bool) {l : List α} : length l = countP p l + countP (fun a => ¬p a) l
Full source 
theorem length_eq_countP_add_countP (p : α → Bool) {l : List α} : length l = countP p l + countP (fun a => ¬p a) l := by
  induction l with
  | nil => rfl
  | cons hd _ ih =>
    if h : p hd then
      rw [countP_cons_of_pos h, countP_cons_of_neg _, length, ih]
      · rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]
      · simp [h]
    else
      rw [countP_cons_of_pos (p := fun a => ¬p a), countP_cons_of_neg h, length, ih]
      · rfl
      · simp [h]
Length Decomposition via Predicate Counts: $\text{length}(l) = \text{countP}_p(l) + \text{countP}_{\neg p}(l)$
Informal description
For any predicate $p : \alpha \to \mathtt{Bool}$ and any list $l$ of elements of type $\alpha$, the length of $l$ is equal to the sum of the number of elements in $l$ satisfying $p$ and the number of elements in $l$ not satisfying $p$. That is, \[ \text{length}(l) = \text{countP}_p(l) + \text{countP}_{\neg p}(l). \]
List.countP_eq_length_filter theorem
{l : List α} : countP p l = length (filter p l)
Full source 
theorem countP_eq_length_filter {l : List α} : countP p l = length (filter p l) := by
  induction l with
  | nil => rfl
  | cons x l ih =>
    if h : p x
    then rw [countP_cons_of_pos h, ih, filter_cons_of_pos h, length]
    else rw [countP_cons_of_neg h, ih, filter_cons_of_neg h]
Count of Elements Satisfying Predicate Equals Length of Filtered List
Informal description
For any predicate $p$ and list $l$, the count of elements in $l$ satisfying $p$ is equal to the length of the list obtained by filtering $l$ with $p$, i.e., $\text{countP}_p(l) = \text{length}(\text{filter}\ p\ l)$.
List.countP_eq_length_filter' theorem
: countP p = length ∘ filter p
Full source 
theorem countP_eq_length_filter' : countP p = lengthlength ∘ filter p := by
  funext l
  apply countP_eq_length_filter
Count Predicate as Composition of Length and Filter: $\text{countP}_p = \text{length} \circ \text{filter}\ p$
Informal description
For any predicate $p : \alpha \to \mathtt{Bool}$, the count of elements in a list $l$ satisfying $p$ is equal to the length of the list obtained by filtering $l$ with $p$, i.e., \[ \text{countP}_p(l) = \text{length}(\text{filter}\ p\ l). \] Equivalently, the function $\text{countP}_p$ is equal to the composition of the length function with the filter function applied to $p$.
List.countP_le_length theorem
: countP p l ≤ l.length
Full source 
theorem countP_le_length : countP p l ≤ l.length := by
  simp only [countP_eq_length_filter]
  apply length_filter_le
Upper Bound on Count of Elements Satisfying Predicate in a List: $\text{countP}_p(l) \leq |l|$
Informal description
For any predicate $p$ and list $l$, the count of elements in $l$ satisfying $p$ is less than or equal to the length of $l$, i.e., $\text{countP}_p(l) \leq \text{length}(l)$.
List.countP_append theorem
{l₁ l₂ : List α} : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂
Full source 
@[simp] theorem countP_append {l₁ l₂ : List α} : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂ := by
  simp only [countP_eq_length_filter, filter_append, length_append]
Additivity of List Count Under Concatenation: $\text{countP}_p(l_1 ++ l_2) = \text{countP}_p(l_1) + \text{countP}_p(l_2)$
Informal description
For any predicate $p$ and any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the count of elements satisfying $p$ in the concatenated list $l_1 ++ l_2$ is equal to the sum of the counts of elements satisfying $p$ in $l_1$ and $l_2$ separately. In symbols: \[ \text{countP}_p(l_1 ++ l_2) = \text{countP}_p(l_1) + \text{countP}_p(l_2) \]
List.countP_pos_iff theorem
{p} : 0 < countP p l ↔ ∃ a ∈ l, p a
Full source 
@[simp] theorem countP_pos_iff {p} : 0 < countP p l ↔ ∃ a ∈ l, p a := by
  simp only [countP_eq_length_filter, length_pos_iff_exists_mem, mem_filter, exists_prop]
Positive Count of Satisfying Elements in List if and only if Exists Satisfying Element
Informal description
For any predicate $p$ and list $l$, the count of elements in $l$ satisfying $p$ is positive if and only if there exists an element $a$ in $l$ such that $p(a)$ holds. In other words, $0 < \text{countP}_p(l) \leftrightarrow \exists a \in l, p(a)$.
List.countP_pos abbrev
Full source 
@[deprecated countP_pos_iff (since := "2024-09-09")] abbrev countP_pos := @countP_pos_iff
Positive Count of Satisfying Elements in List if and only if Exists Satisfying Element
Informal description
For any predicate $p$ and list $l$, the count of elements in $l$ satisfying $p$ is positive if and only if there exists an element $a$ in $l$ such that $p(a)$ holds. In other words, $\text{countP}_p(l) > 0 \leftrightarrow \exists a \in l, p(a)$.
List.one_le_countP_iff theorem
{p} : 1 ≤ countP p l ↔ ∃ a ∈ l, p a
Full source 
@[simp] theorem one_le_countP_iff {p} : 1 ≤ countP p l ↔ ∃ a ∈ l, p a :=
  countP_pos_iff
Count of Satisfying Elements is at Least One if and Only if Exists Satisfying Element
Informal description
For any predicate $p$ and list $l$, the count of elements in $l$ satisfying $p$ is at least one if and only if there exists an element $a$ in $l$ such that $p(a)$ holds. In other words, $1 \leq \text{countP}_p(l) \leftrightarrow \exists a \in l, p(a)$.
List.countP_eq_zero theorem
{p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a
Full source 
@[simp] theorem countP_eq_zero {p} : countPcountP p l = 0 ↔ ∀ a ∈ l, ¬p a := by
  simp only [countP_eq_length_filter, length_eq_zero_iff, filter_eq_nil_iff]
$\text{countP}_p(l) = 0 \leftrightarrow \forall a \in l, \neg p(a)$
Informal description
For any predicate $p$ and list $l$, the count of elements in $l$ satisfying $p$ is zero if and only if no element in $l$ satisfies $p$, i.e., $\text{countP}_p(l) = 0 \leftrightarrow \forall a \in l, \neg p(a)$.
List.countP_eq_length theorem
{p} : countP p l = l.length ↔ ∀ a ∈ l, p a
Full source 
@[simp] theorem countP_eq_length {p} : countPcountP p l = l.length ↔ ∀ a ∈ l, p a := by
  rw [countP_eq_length_filter, length_filter_eq_length_iff]
Count Equals Length if and only if All Elements Satisfy Predicate
Informal description
For any predicate $p$ and list $l$, the count of elements in $l$ satisfying $p$ equals the length of $l$ if and only if every element $a$ in $l$ satisfies $p(a)$. That is: $$\text{countP}_p(l) = |l| \leftrightarrow \forall a \in l, p(a)$$
List.countP_replicate theorem
{p : α → Bool} {a : α} {n : Nat} : countP p (replicate n a) = if p a then n else 0
Full source 
theorem countP_replicate {p : α → Bool} {a : α} {n : Nat} :
    countP p (replicate n a) = if p a then n else 0 := by
  simp only [countP_eq_length_filter, filter_replicate]
  split <;> simp
Count of Predicate-Satisfying Elements in Replicated List: $\text{countP}_p(\text{replicate}(n, a)) = \text{if } p(a) \text{ then } n \text{ else } 0$
Informal description
For any predicate $p : \alpha \to \text{Bool}$, element $a \in \alpha$, and natural number $n$, the count of elements in the list $\text{replicate}(n, a)$ (which contains $n$ copies of $a$) that satisfy $p$ is equal to $n$ if $p(a)$ holds, and $0$ otherwise. In other words, $\text{countP}_p(\text{replicate}(n, a)) = \begin{cases} n & \text{if } p(a) \\ 0 & \text{otherwise} \end{cases}$
List.boole_getElem_le_countP theorem
{p : α → Bool} {l : List α} {i : Nat} (h : i < l.length) : (if p l[i] then 1 else 0) ≤ l.countP p
Full source 
theorem boole_getElem_le_countP {p : α → Bool} {l : List α} {i : Nat} (h : i < l.length) :
    (if p l[i] then 1 else 0) ≤ l.countP p := by
  induction l generalizing i with
  | nil => simp at h
  | cons x l ih =>
    cases i with
    | zero => simp [countP_cons]
    | succ i =>
      simp only [length_cons, add_one_lt_add_one_iff] at h
      simp only [getElem_cons_succ, countP_cons]
      specialize ih h
      exact le_add_right_of_le ih
Indicator Bound for List Predicate Count: $\mathbb{1}_{p(l[i])} \leq \mathtt{countP}\ p\ l$
Informal description
For any predicate $p : \alpha \to \mathtt{Bool}$, list $l : \mathtt{List}\ \alpha$, and natural number index $i$ such that $i < \mathtt{length}\ l$, the indicator function $\mathbb{1}_{p(l[i])}$ is less than or equal to the count of elements in $l$ satisfying $p$. That is, \[ \begin{cases} 1 & \text{if } p(l[i]) \\ 0 & \text{otherwise} \end{cases} \leq \mathtt{countP}\ p\ l. \]
List.Sublist.countP_le theorem
(s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂
Full source 
theorem Sublist.countP_le (s : l₁ <+ l₂) : countP p l₁ ≤ countP p l₂ := by
  simp only [countP_eq_length_filter]
  apply s.filter _ |>.length_le
Sublist Preserves Count of Elements Satisfying Predicate: $\text{countP}_p(l_1) \leq \text{countP}_p(l_2)$ when $l_1 <+ l_2$
Informal description
For any predicate $p$ and lists $l_1, l_2$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then the count of elements in $l_1$ satisfying $p$ is less than or equal to the count of elements in $l_2$ satisfying $p$, i.e., $\text{countP}_p(l_1) \leq \text{countP}_p(l_2)$.
List.IsPrefix.countP_le theorem
(s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂
Full source 
theorem IsPrefix.countP_le (s : l₁ <+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
Prefix Preserves Count of Elements Satisfying Predicate: $\text{countP}_p(l_1) \leq \text{countP}_p(l_2)$ when $l_1$ is a prefix of $l_2$
Informal description
For any predicate $p$ and lists $l_1, l_2$, if $l_1$ is a prefix of $l_2$ (denoted $l_1 <+: l_2$), then the count of elements in $l_1$ satisfying $p$ is less than or equal to the count of elements in $l_2$ satisfying $p$, i.e., $\text{countP}_p(l_1) \leq \text{countP}_p(l_2)$.
List.IsSuffix.countP_le theorem
(s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂
Full source 
theorem IsSuffix.countP_le (s : l₁ <:+ l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
Suffix Preserves Count of Elements Satisfying Predicate
Informal description
For any predicate $p$ and lists $l_1, l_2$, if $l_1$ is a suffix of $l_2$ (denoted $l_1 <:+ l_2$), then the count of elements in $l_1$ satisfying $p$ is less than or equal to the count of elements in $l_2$ satisfying $p$, i.e., $\text{countP}_p(l_1) \leq \text{countP}_p(l_2)$.
List.IsInfix.countP_le theorem
(s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂
Full source 
theorem IsInfix.countP_le (s : l₁ <:+: l₂) : countP p l₁ ≤ countP p l₂ := s.sublist.countP_le
Infix Sublist Preserves Predicate Count: $\text{countP}_p(l₁) \leq \text{countP}_p(l₂)$ when $l₁$ is an infix of $l₂$
Informal description
For any predicate $p$ and lists $l₁, l₂$, if $l₁$ is an infix of $l₂$ (denoted $l₁ <:+: l₂$), then the number of elements in $l₁$ satisfying $p$ is less than or equal to the number of elements in $l₂$ satisfying $p$, i.e., $\text{countP}_p(l₁) \leq \text{countP}_p(l₂)$.
List.countP_tail_le theorem
(l) : countP p l.tail ≤ countP p l
Full source 
theorem countP_tail_le (l) : countP p l.tail ≤ countP p l :=
  (tail_sublist l).countP_le
Tail Count Inequality: $\text{countP}_p(\text{tail}(l)) \leq \text{countP}_p(l)$
Informal description
For any list $l$ and predicate $p$, the count of elements in the tail of $l$ satisfying $p$ is less than or equal to the count of elements in $l$ satisfying $p$, i.e., $\text{countP}_p(\text{tail}(l)) \leq \text{countP}_p(l)$.
List.countP_filter theorem
{l : List α} : countP p (filter q l) = countP (fun a => p a && q a) l
Full source 
theorem countP_filter {l : List α} :
    countP p (filter q l) = countP (fun a => p a && q a) l := by
  simp only [countP_eq_length_filter, filter_filter]
Count of Predicate on Filtered List Equals Count of Conjunction Predicate on Original List
Informal description
For any list $l$ of elements of type $\alpha$ and predicates $p, q : \alpha \to \text{Bool}$, the count of elements in the filtered list $\text{filter}\ q\ l$ that satisfy $p$ is equal to the count of elements in $l$ that satisfy both $p$ and $q$, i.e., $$\text{countP}_p(\text{filter}\ q\ l) = \text{countP}_{p \land q}(l).$$
List.countP_true theorem
: (countP fun (_ : α) => true) = length
Full source 
@[simp] theorem countP_true : (countP fun (_ : α) => true) = length := by
  funext l
  simp
Count of True Predicate Equals List Length
Informal description
For any list `l` of elements of type `α`, the count of elements satisfying the always-true predicate is equal to the length of the list, i.e., $\text{countP}(\lambda \_\colon \alpha, \text{true}) = \text{length}(l)$.
List.countP_false theorem
: (countP fun (_ : α) => false) = Function.const _ 0
Full source 
@[simp] theorem countP_false : (countP fun (_ : α) => false) = Function.const _ 0 := by
  funext l
  simp
Count of False Predicate is Zero Function
Informal description
For any list `l` of elements of type `α`, the count of elements satisfying the always-false predicate is equal to the constant zero function, i.e., $\text{countP}(\lambda \_\colon \alpha, \text{false}) = \text{const}_\alpha(0)$.
List.countP_map theorem
{p : β → Bool} {f : α → β} : ∀ {l}, countP p (map f l) = countP (p ∘ f) l
Full source 
@[simp] theorem countP_map {p : β → Bool} {f : α → β} :
    ∀ {l}, countP p (map f l) = countP (p ∘ f) l
  | [] => rfl
  | a :: l => by rw [map_cons, countP_cons, countP_cons, countP_map]; rfl
Count Preservation Under List Mapping: $\mathtt{countP}_p(\mathtt{map}\ f\ l) = \mathtt{countP}_{p \circ f}(l)$
Informal description
For any predicate $p : \beta \to \mathtt{Bool}$, function $f : \alpha \to \beta$, and list $l$ of elements of type $\alpha$, the count of elements in the mapped list $\mathtt{map}\ f\ l$ that satisfy $p$ is equal to the count of elements in $l$ that satisfy the composed predicate $p \circ f$. That is, \[ \mathtt{countP}\ p\ (\mathtt{map}\ f\ l) = \mathtt{countP}\ (p \circ f)\ l. \]
List.length_filterMap_eq_countP theorem
{f : α → Option β} {l : List α} : (filterMap f l).length = countP (fun a => (f a).isSome) l
Full source 
theorem length_filterMap_eq_countP {f : α → Option β} {l : List α} :
    (filterMap f l).length = countP (fun a => (f a).isSome) l := by
  induction l with
  | nil => rfl
  | cons x l ih =>
    simp only [filterMap_cons, countP_cons]
    split <;> simp [ih, *]
Length of `filterMap` Equals Count of Defined Values: $\text{length}(\text{filterMap}\ f\ l) = \text{countP}\ (\lambda a, \text{isSome}(f\ a))\ l$
Informal description
For any function $f : \alpha \to \text{Option}\ \beta$ and list $l$ of elements of type $\alpha$, the length of the list obtained by applying `filterMap` $f$ to $l$ is equal to the count of elements $a$ in $l$ for which $f(a)$ is `some` value (i.e., $\text{isSome}(f(a))$ holds).
List.countP_filterMap theorem
{p : β → Bool} {f : α → Option β} {l : List α} : countP p (filterMap f l) = countP (fun a => ((f a).map p).getD false) l
Full source 
theorem countP_filterMap {p : β → Bool} {f : α → Option β} {l : List α} :
    countP p (filterMap f l) = countP (fun a => ((f a).map p).getD false) l := by
  simp only [countP_eq_length_filter, filter_filterMap, ← filterMap_eq_filter]
  simp only [length_filterMap_eq_countP]
  congr
  ext a
  simp +contextual [Option.getD_eq_iff, Option.isSome_eq_isSome]
Count of Predicate-Satisfying Elements in Filter-Mapped List Equals Count of Mapped Predicate Evaluations
Informal description
For any predicate $p : \beta \to \text{Bool}$, function $f : \alpha \to \text{Option } \beta$, and list $l$ of elements of type $\alpha$, the count of elements in the filtered-mapped list $\text{filterMap } f\ l$ that satisfy $p$ is equal to the count of elements $a$ in $l$ for which $f(a)$ is mapped through $p$ (with a default value of $\text{false}$ when $f(a)$ is $\text{none}$). That is, \[ \text{countP } p\ (\text{filterMap } f\ l) = \text{countP } (\lambda a, \text{Option.map } p\ (f\ a).\text{getD } \text{false})\ l. \]
List.countP_flatten theorem
{l : List (List α)} : countP p l.flatten = (l.map (countP p)).sum
Full source 
@[simp] theorem countP_flatten {l : List (List α)} :
    countP p l.flatten = (l.map (countP p)).sum := by
  simp only [countP_eq_length_filter, filter_flatten]
  simp [countP_eq_length_filter']
Count of Predicate-Satisfying Elements in Flattened List Equals Sum of Sublist Counts
Informal description
For any predicate $p$ and list of lists $l$, the count of elements in the flattened list $\text{flatten}(l)$ that satisfy $p$ is equal to the sum of counts of elements satisfying $p$ in each sublist of $l$. That is, \[ \text{countP}_p(\text{flatten}(l)) = \sum_{s \in l} \text{countP}_p(s). \]
List.countP_join abbrev
Full source 
@[deprecated countP_flatten (since := "2024-10-14")] abbrev countP_join := @countP_flatten
Count Preservation under List Join: $\text{countP}_p(\text{join}(l)) = \sum_{s \in l} \text{countP}_p(s)$
Informal description
For any predicate $p$ and list of lists $l$, the count of elements in the joined list $\text{join}(l)$ that satisfy $p$ is equal to the sum of counts of elements satisfying $p$ in each sublist of $l$. That is, \[ \text{countP}_p(\text{join}(l)) = \sum_{s \in l} \text{countP}_p(s). \]
List.countP_flatMap theorem
{p : β → Bool} {l : List α} {f : α → List β} : countP p (l.flatMap f) = sum (map (countP p ∘ f) l)
Full source 
theorem countP_flatMap {p : β → Bool} {l : List α} {f : α → List β} :
    countP p (l.flatMap f) = sum (map (countPcountP p ∘ f) l) := by
  rw [List.flatMap, countP_flatten, map_map]
Count Preservation under FlatMap: $\text{countP}_p(\text{flatMap}\ f\ l) = \sum_{x \in l} \text{countP}_p(f\ x)$
Informal description
For any predicate $p : \beta \to \text{Bool}$, list $l : \text{List}\ \alpha$, and function $f : \alpha \to \text{List}\ \beta$, the count of elements satisfying $p$ in the flat-mapped list $\text{flatMap}\ f\ l$ is equal to the sum of counts of elements satisfying $p$ in each sublist obtained by applying $f$ to elements of $l$. That is, \[ \text{countP}_p(\text{flatMap}\ f\ l) = \sum_{x \in l} \text{countP}_p(f\ x). \]
List.countP_reverse theorem
{l : List α} : countP p l.reverse = countP p l
Full source 
@[simp] theorem countP_reverse {l : List α} : countP p l.reverse = countP p l := by
  simp [countP_eq_length_filter, filter_reverse]
Count Preservation under List Reversal: $\text{countP}_p(l^{\text{rev}}) = \text{countP}_p(l)$
Informal description
For any predicate $p$ and list $l$, the count of elements in the reversed list $l^{\text{rev}}$ satisfying $p$ is equal to the count of elements in $l$ satisfying $p$, i.e., $\text{countP}_p(l^{\text{rev}}) = \text{countP}_p(l)$.
List.countP_mono_left theorem
(h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l
Full source 
theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l := by
  induction l with
  | nil => apply Nat.le_refl
  | cons a l ihl =>
    rw [forall_mem_cons] at h
    have ⟨ha, hl⟩ := h
    simp [countP_cons]
    cases h : p a
    · simp only [Bool.false_eq_true, ↓reduceIte, Nat.add_zero]
      apply Nat.le_trans ?_ (Nat.le_add_right _ _)
      apply ihl hl
    · simp only [↓reduceIte, ha h, succ_le_succ_iff]
      apply ihl hl
Monotonicity of Count with Respect to Predicate Implication: $(\forall x \in l, p(x) \to q(x)) \implies \text{countP}_p(l) \leq \text{countP}_q(l)$
Informal description
For any list $l$ and predicates $p, q$, if for every element $x \in l$ we have $p(x) \to q(x)$, then the count of elements in $l$ satisfying $p$ is less than or equal to the count of elements satisfying $q$.
List.countP_congr theorem
(h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l
Full source 
theorem countP_congr (h : ∀ x ∈ l, p x ↔ q x) : countP p l = countP q l :=
  Nat.le_antisymm
    (countP_mono_left fun x hx => (h x hx).1)
    (countP_mono_left fun x hx => (h x hx).2)
Count Preservation under Predicate Equivalence: $(\forall x \in l, p(x) \leftrightarrow q(x)) \implies \text{countP}_p(l) = \text{countP}_q(l)$
Informal description
For any list $l$ and predicates $p, q$, if for every element $x \in l$ we have $p(x) \leftrightarrow q(x)$, then the count of elements in $l$ satisfying $p$ is equal to the count of elements satisfying $q$.
List.count_nil theorem
{a : α} : count a [] = 0
Full source 
@[simp] theorem count_nil {a : α} : count a [] = 0 := rfl
Count of Any Element in Empty List is Zero
Informal description
For any element $a$ of type $\alpha$, the count of occurrences of $a$ in the empty list is $0$.
List.count_cons theorem
{a b : α} {l : List α} : count a (b :: l) = count a l + if b == a then 1 else 0
Full source 
theorem count_cons {a b : α} {l : List α} :
    count a (b :: l) = count a l + if b == a then 1 else 0 := by
  simp [count, countP_cons]
Count in Cons List: $\text{count}(a, b :: l) = \text{count}(a, l) + \mathbb{1}_{b = a}$
Informal description
For any elements $a, b$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the list $b :: l$ is equal to the count of $a$ in $l$ plus $1$ if $b = a$, and $0$ otherwise. That is, \[ \text{count}(a, b :: l) = \text{count}(a, l) + \begin{cases} 1 & \text{if } b = a \\ 0 & \text{otherwise.} \end{cases} \]
List.count_eq_countP theorem
{a : α} {l : List α} : count a l = countP (· == a) l
Full source 
theorem count_eq_countP {a : α} {l : List α} : count a l = countP (· == a) l := rfl
Count Equals Count Predicate for List Membership
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in $l$ is equal to the count of elements in $l$ that satisfy the predicate $\lambda x, x == a$. In other words, $\text{count}(a, l) = \text{countP}(\lambda x, x == a, l)$.
List.count_eq_countP' theorem
{a : α} : count a = countP (· == a)
Full source 
theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
  funext l
  apply count_eq_countP
Count Function Equals Predicate Count for List Membership
Informal description
For any element $a$ of type $\alpha$, the function $\text{count}(a, \cdot)$ that counts occurrences of $a$ in a list is equal to the function $\text{countP}(\lambda x, x == a, \cdot)$ that counts elements satisfying the predicate $\lambda x, x == a$ in a list.
List.count_tail theorem
: ∀ {l : List α} (h : l ≠ []) (a : α), l.tail.count a = l.count a - if l.head h == a then 1 else 0
Full source 
theorem count_tail : ∀ {l : List α} (h : l ≠ []) (a : α),
      l.tail.count a = l.count a - if l.head h == a then 1 else 0
  | _ :: _, a, _ => by simp [count_cons]
Tail Count Formula: $\text{count}(a, \text{tail}(l)) = \text{count}(a, l) - \mathbb{1}_{\text{head}(l) = a}$
Informal description
For any non-empty list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the count of $a$ in the tail of $l$ is equal to the count of $a$ in $l$ minus $1$ if the head of $l$ equals $a$, and $0$ otherwise. That is, \[ \text{count}(a, \text{tail}(l)) = \text{count}(a, l) - \begin{cases} 1 & \text{if } \text{head}(l) = a \\ 0 & \text{otherwise.} \end{cases} \]
List.count_le_length theorem
{a : α} {l : List α} : count a l ≤ l.length
Full source 
theorem count_le_length {a : α} {l : List α} : count a l ≤ l.length := countP_le_length
Upper Bound on Element Count in List: $\text{count}(a, l) \leq |l|$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the number of occurrences of $a$ in $l$ is less than or equal to the length of $l$, i.e., $\text{count}(a, l) \leq \text{length}(l)$.
List.Sublist.count_le theorem
(a : α) (h : l₁ <+ l₂) : count a l₁ ≤ count a l₂
Full source 
theorem Sublist.count_le (a : α) (h : l₁ <+ l₂) : count a l₁ ≤ count a l₂ := h.countP_le
Sublist Preserves Element Count: $\text{count}(a, l_1) \leq \text{count}(a, l_2)$ when $l_1 <+ l_2$
Informal description
For any element $a$ of type $\alpha$ and lists $l_1, l_2$ of type $\alpha$, if $l_1$ is a sublist of $l_2$ (denoted $l_1 <+ l_2$), then the count of $a$ in $l_1$ is less than or equal to the count of $a$ in $l_2$, i.e., $\text{count}(a, l_1) \leq \text{count}(a, l_2)$.
List.IsPrefix.count_le theorem
(a : α) (h : l₁ <+: l₂) : count a l₁ ≤ count a l₂
Full source 
theorem IsPrefix.count_le (a : α) (h : l₁ <+: l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
Prefix Preserves Element Count: $\text{count}(a, l_1) \leq \text{count}(a, l_2)$ when $l_1$ is a prefix of $l_2$
Informal description
For any element $a$ of type $\alpha$ and lists $l_1, l_2$ of type $\alpha$, if $l_1$ is a prefix of $l_2$ (denoted $l_1 <+: l_2$), then the count of $a$ in $l_1$ is less than or equal to the count of $a$ in $l_2$, i.e., $\text{count}(a, l_1) \leq \text{count}(a, l_2)$.
List.IsSuffix.count_le theorem
(a : α) (h : l₁ <:+ l₂) : count a l₁ ≤ count a l₂
Full source 
theorem IsSuffix.count_le (a : α) (h : l₁ <:+ l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
Suffix Preserves Element Count: $\text{count}(a, l_1) \leq \text{count}(a, l_2)$ when $l_1$ is a suffix of $l_2$
Informal description
For any element $a$ of type $\alpha$ and lists $l_1, l_2$ of type $\alpha$, if $l_1$ is a suffix of $l_2$ (denoted $l_1 <:+ l_2$), then the count of $a$ in $l_1$ is less than or equal to the count of $a$ in $l_2$, i.e., $\text{count}(a, l_1) \leq \text{count}(a, l_2)$.
List.IsInfix.count_le theorem
(a : α) (h : l₁ <:+: l₂) : count a l₁ ≤ count a l₂
Full source 
theorem IsInfix.count_le (a : α) (h : l₁ <:+: l₂) : count a l₁ ≤ count a l₂ := h.sublist.count_le a
Infix Sublist Preserves Element Count: $\text{count}(a, l_1) \leq \text{count}(a, l_2)$ when $l_1$ is an infix of $l_2$
Informal description
For any element $a$ of type $\alpha$ and lists $l_1, l_2$ of type $\alpha$, if $l_1$ is an infix of $l_2$ (denoted $l_1 <:+: l_2$), then the count of $a$ in $l_1$ is less than or equal to the count of $a$ in $l_2$, i.e., $\text{count}(a, l_1) \leq \text{count}(a, l_2)$.
List.count_tail_le theorem
{a : α} {l : List α} : count a l.tail ≤ count a l
Full source 
theorem count_tail_le {a : α} {l : List α} : count a l.tail ≤ count a l :=
  (tail_sublist l).count_le a
Tail Count Inequality: $\text{count}(a, \text{tail}(l)) \leq \text{count}(a, l)$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of type $\alpha$, the count of $a$ in the tail of $l$ is less than or equal to the count of $a$ in $l$ itself, i.e., $\text{count}(a, \text{tail}(l)) \leq \text{count}(a, l)$.
List.count_le_count_cons theorem
{a b : α} {l : List α} : count a l ≤ count a (b :: l)
Full source 
theorem count_le_count_cons {a b : α} {l : List α} : count a l ≤ count a (b :: l) :=
  (sublist_cons_self _ _).count_le a
Monotonicity of List Count Under Cons: $\text{count}(a, l) \leq \text{count}(a, b :: l)$
Informal description
For any elements $a$ and $b$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of $a$ in $l$ is less than or equal to the count of $a$ in the list obtained by prepending $b$ to $l$, i.e., $\text{count}(a, l) \leq \text{count}(a, b :: l)$.
List.count_singleton theorem
{a b : α} : count a [b] = if b == a then 1 else 0
Full source 
theorem count_singleton {a b : α} : count a [b] = if b == a then 1 else 0 := by
  simp [count_cons]
Count in Singleton List: $\text{count}(a, [b]) = \mathbb{1}_{b = a}$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the count of occurrences of $a$ in the singleton list $[b]$ is equal to $1$ if $b = a$, and $0$ otherwise. That is, \[ \text{count}(a, [b]) = \begin{cases} 1 & \text{if } b = a \\ 0 & \text{otherwise.} \end{cases} \]
List.count_append theorem
{a : α} {l₁ l₂ : List α} : count a (l₁ ++ l₂) = count a l₁ + count a l₂
Full source 
@[simp] theorem count_append {a : α} {l₁ l₂ : List α} : count a (l₁ ++ l₂) = count a l₁ + count a l₂ :=
  countP_append
Additivity of List Count Under Concatenation: $\text{count}(a, l_1 ++ l_2) = \text{count}(a, l_1) + \text{count}(a, l_2)$
Informal description
For any element $a$ of type $\alpha$ and any two lists $l_1$ and $l_2$ of elements of type $\alpha$, the count of occurrences of $a$ in the concatenated list $l_1 ++ l_2$ is equal to the sum of the counts of $a$ in $l_1$ and $l_2$ separately. In symbols: \[ \text{count}(a, l_1 ++ l_2) = \text{count}(a, l_1) + \text{count}(a, l_2) \]
List.count_flatten theorem
{a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum
Full source 
theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
  simp only [count_eq_countP, countP_flatten, count_eq_countP']
Count Additivity in Flattened Lists: $\text{count}(a, \text{flatten}(l)) = \sum_{s \in l} \text{count}(a, s)$
Informal description
For any element $a$ of type $\alpha$ and any list of lists $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the flattened list $\text{flatten}(l)$ is equal to the sum of the counts of $a$ in each sublist of $l$. That is, \[ \text{count}(a, \text{flatten}(l)) = \sum_{s \in l} \text{count}(a, s). \]
List.count_join abbrev
Full source 
@[deprecated count_flatten (since := "2024-10-14")] abbrev count_join := @count_flatten
Count Additivity in Joined Lists: $\text{count}(a, \text{join}(l)) = \sum_{s \in l} \text{count}(a, s)$
Informal description
For any element $a$ of type $\alpha$ and any list of lists $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the joined list $\text{join}(l)$ is equal to the sum of the counts of $a$ in each sublist of $l$. That is, \[ \text{count}(a, \text{join}(l)) = \sum_{s \in l} \text{count}(a, s). \]
List.count_reverse theorem
{a : α} {l : List α} : count a l.reverse = count a l
Full source 
@[simp] theorem count_reverse {a : α} {l : List α} : count a l.reverse = count a l := by
  simp only [count_eq_countP, countP_eq_length_filter, filter_reverse, length_reverse]
Count Preservation under List Reversal: $\text{count}_a(l^{\text{rev}}) = \text{count}_a(l)$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the reversed list $l^{\text{rev}}$ is equal to the count of occurrences of $a$ in the original list $l$, i.e., \[ \text{count}_a(l^{\text{rev}}) = \text{count}_a(l). \]
List.boole_getElem_le_count theorem
{a : α} {l : List α} {i : Nat} (h : i < l.length) : (if l[i] == a then 1 else 0) ≤ l.count a
Full source 
theorem boole_getElem_le_count {a : α} {l : List α} {i : Nat} (h : i < l.length) :
    (if l[i] == a then 1 else 0) ≤ l.count a := by
  rw [count_eq_countP]
  apply boole_getElem_le_countP (p := (· == a))
Indicator Bound for List Element Count: $\mathbb{1}_{l[i] = a} \leq \text{count}(a, l)$
Informal description
For any element $a$ of type $\alpha$, any list $l$ of elements of type $\alpha$, and any natural number index $i$ such that $i < \text{length}(l)$, the indicator function $\mathbb{1}_{l[i] = a}$ is less than or equal to the count of occurrences of $a$ in $l$. That is, \[ \begin{cases} 1 & \text{if } l[i] = a \\ 0 & \text{otherwise} \end{cases} \leq \text{count}(a, l). \]
List.count_cons_self theorem
{a : α} {l : List α} : count a (a :: l) = count a l + 1
Full source 
@[simp] theorem count_cons_self {a : α} {l : List α} : count a (a :: l) = count a l + 1 := by
  simp [count_cons]
Count of Element in Cons List: $\text{count}(a, a :: l) = \text{count}(a, l) + 1$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the list $a :: l$ is equal to the count of $a$ in $l$ plus one, i.e., \[ \text{count}(a, a :: l) = \text{count}(a, l) + 1. \]
List.count_cons_of_ne theorem
(h : b ≠ a) {l : List α} : count a (b :: l) = count a l
Full source 
@[simp] theorem count_cons_of_ne (h : b ≠ a) {l : List α} : count a (b :: l) = count a l := by
  simp [count_cons, h]
Count Preservation in Cons List for Distinct Elements: $\text{count}(a, b :: l) = \text{count}(a, l)$ when $b \neq a$
Informal description
For any elements $a$ and $b$ of a type $\alpha$ with $b \neq a$, and for any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the list $b :: l$ is equal to the count of $a$ in $l$.
List.count_singleton_self theorem
{a : α} : count a [a] = 1
Full source 
theorem count_singleton_self {a : α} : count a [a] = 1 := by simp
Count in Singleton List: $\text{count}(a, [a]) = 1$
Informal description
For any element $a$ of type $\alpha$, the count of occurrences of $a$ in the singleton list $[a]$ is equal to $1$, i.e., \[ \text{count}(a, [a]) = 1. \]
List.count_concat_self theorem
{a : α} {l : List α} : count a (concat l a) = count a l + 1
Full source 
theorem count_concat_self {a : α} {l : List α} : count a (concat l a) = count a l + 1 := by simp
Count Increment When Appending Element to List: $\text{count}(a, \text{concat}(l, a)) = \text{count}(a, l) + 1$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the list obtained by appending $a$ to the end of $l$ is equal to the count of $a$ in $l$ plus one, i.e., \[ \text{count}(a, \text{concat}(l, a)) = \text{count}(a, l) + 1. \]
List.count_pos_iff theorem
{a : α} {l : List α} : 0 < count a l ↔ a ∈ l
Full source 
@[simp]
theorem count_pos_iff {a : α} {l : List α} : 0 < count a l ↔ a ∈ l := by
  simp only [count, countP_pos_iff, beq_iff_eq, exists_eq_right]
Positive Count Implies Membership in List
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of $a$ in $l$ is positive (i.e., $0 < \text{count}(a, l)$) if and only if $a$ is a member of $l$ (i.e., $a \in l$).
List.count_pos_iff_mem abbrev
Full source 
@[deprecated count_pos_iff (since := "2024-09-09")] abbrev count_pos_iff_mem := @count_pos_iff
Positive Count Implies Membership in List
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of $a$ in $l$ is positive (i.e., $0 < \text{count}(a, l)$) if and only if $a$ is a member of $l$ (i.e., $a \in l$).
List.one_le_count_iff theorem
{a : α} {l : List α} : 1 ≤ count a l ↔ a ∈ l
Full source 
@[simp] theorem one_le_count_iff {a : α} {l : List α} : 1 ≤ count a l ↔ a ∈ l :=
  count_pos_iff
Count At Least One Implies Membership in List
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of $a$ in $l$ is at least one (i.e., $1 \leq \text{count}(a, l)$) if and only if $a$ is a member of $l$ (i.e., $a \in l$).
List.count_eq_zero_of_not_mem theorem
{a : α} {l : List α} (h : a ∉ l) : count a l = 0
Full source 
theorem count_eq_zero_of_not_mem {a : α} {l : List α} (h : a ∉ l) : count a l = 0 :=
  Decidable.byContradiction fun h' => h <| count_pos_iff.1 (Nat.pos_of_ne_zero h')
Count Zero for Non-Member Elements in List
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, if $a$ is not a member of $l$ (i.e., $a \notin l$), then the count of $a$ in $l$ is zero (i.e., $\text{count}(a, l) = 0$).
List.not_mem_of_count_eq_zero theorem
{a : α} {l : List α} (h : count a l = 0) : a ∉ l
Full source 
theorem not_mem_of_count_eq_zero {a : α} {l : List α} (h : count a l = 0) : a ∉ l :=
  fun h' => Nat.ne_of_lt (count_pos_iff.2 h') h.symm
Non-Membership from Zero Count in List
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, if the count of $a$ in $l$ is zero (i.e., $\text{count}(a, l) = 0$), then $a$ is not a member of $l$ (i.e., $a \notin l$).
List.count_eq_zero theorem
{l : List α} : count a l = 0 ↔ a ∉ l
Full source 
theorem count_eq_zero {l : List α} : countcount a l = 0 ↔ a ∉ l :=
  ⟨not_mem_of_count_eq_zero, count_eq_zero_of_not_mem⟩
Zero Count Equivalence to Non-Membership in List
Informal description
For any list $l$ of elements of type $\alpha$ and any element $a$ of type $\alpha$, the count of $a$ in $l$ is zero if and only if $a$ is not a member of $l$. In other words, $\text{count}(a, l) = 0 \leftrightarrow a \notin l$.
List.count_eq_length theorem
{l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b
Full source 
theorem count_eq_length {l : List α} : countcount a l = l.length ↔ ∀ b ∈ l, a = b := by
  rw [count, countP_eq_length]
  refine ⟨fun h b hb => Eq.symm ?_, fun h b hb => ?_⟩
  · simpa using h b hb
  · rw [h b hb, beq_self_eq_true]
Count Equals Length if and only if All Elements Equal $a$
Informal description
For any list $l$ of elements of type $\alpha$ and any element $a$ of type $\alpha$, the count of occurrences of $a$ in $l$ equals the length of $l$ if and only if every element $b$ in $l$ is equal to $a$. That is: $$\text{count}(a, l) = |l| \leftrightarrow \forall b \in l, b = a$$
List.count_replicate_self theorem
{a : α} {n : Nat} : count a (replicate n a) = n
Full source 
@[simp] theorem count_replicate_self {a : α} {n : Nat} : count a (replicate n a) = n :=
  (count_eq_length.2 <| fun _ h => (eq_of_mem_replicate h).symm).trans (length_replicate ..)
Count of Element in Replicated List Equals Replication Count
Informal description
For any element $a$ of type $\alpha$ and any natural number $n$, the count of $a$ in the list consisting of $n$ copies of $a$ is equal to $n$. That is, $\text{count}(a, \text{replicate}(n, a)) = n$.
List.count_replicate theorem
{a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0
Full source 
theorem count_replicate {a b : α} {n : Nat} : count a (replicate n b) = if b == a then n else 0 := by
  split <;> (rename_i h; simp only [beq_iff_eq] at h)
  · exact ‹b = a› ▸ count_replicate_self ..
  · exact count_eq_zero.2 <| mt eq_of_mem_replicate (Ne.symm h)
Count in Replicated List: $\text{count}(a, \text{replicate}(n, b)) = n \text{ if } b == a \text{ else } 0$
Informal description
For any elements $a$ and $b$ of type $\alpha$ and any natural number $n$, the count of $a$ in the list consisting of $n$ copies of $b$ equals $n$ if $b$ is boolean-equal to $a$, and $0$ otherwise. That is: $$\text{count}(a, \text{replicate}(n, b)) = \begin{cases} n & \text{if } b == a \\ 0 & \text{otherwise} \end{cases}$$
List.filter_beq theorem
{l : List α} (a : α) : l.filter (· == a) = replicate (count a l) a
Full source 
theorem filter_beq {l : List α} (a : α) : l.filter (· == a) = replicate (count a l) a := by
  simp only [count, countP_eq_length_filter, eq_replicate_iff, mem_filter, beq_iff_eq]
  exact ⟨trivial, fun _ h => h.2⟩
Filtering by Boolean Equality Yields Replicated Count
Informal description
For any list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the sublist obtained by filtering $l$ to retain only elements that are boolean-equal to $a$ is equal to the list consisting of $n$ copies of $a$, where $n$ is the count of occurrences of $a$ in $l$. In other words, $\text{filter}\ (\cdot == a)\ l = \text{replicate}\ (\text{count}\ a\ l)\ a$.
List.filter_eq theorem
{α} [DecidableEq α] {l : List α} (a : α) : l.filter (· = a) = replicate (count a l) a
Full source 
theorem filter_eq {α} [DecidableEq α] {l : List α} (a : α) : l.filter (· = a) = replicate (count a l) a :=
  filter_beq a
Filtering by Equality Yields Replicated Count
Informal description
For any list $l$ of elements of type $\alpha$ with decidable equality and any element $a \in \alpha$, the sublist obtained by filtering $l$ to retain only elements equal to $a$ is equal to the list consisting of $n$ copies of $a$, where $n$ is the count of occurrences of $a$ in $l$. In other words, $\text{filter}\ (\cdot = a)\ l = \text{replicate}\ (\text{count}\ a\ l)\ a$.
List.le_count_iff_replicate_sublist theorem
{l : List α} : n ≤ count a l ↔ replicate n a <+ l
Full source 
theorem le_count_iff_replicate_sublist {l : List α} : n ≤ count a l ↔ replicate n a <+ l := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · exact ((replicate_sublist_replicate a).2 h).trans <| filter_beq a ▸ filter_sublist
  · simpa only [count_replicate_self] using h.count_le a
Sublist Characterization of Element Count: $n \leq \text{count}(a, l) \leftrightarrow \text{replicate}(n, a) <+ l$
Informal description
For any list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the inequality $n \leq \text{count}(a, l)$ holds if and only if the list consisting of $n$ copies of $a$ is a sublist of $l$.
List.replicate_count_eq_of_count_eq_length theorem
{l : List α} (h : count a l = length l) : replicate (count a l) a = l
Full source 
theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = length l) :
    replicate (count a l) a = l :=
  (le_count_iff_replicate_sublist.mp (Nat.le_refl _)).eq_of_length <| length_replicate.trans h
Replicate Equals List When Count Equals Length
Informal description
For any list $l$ of elements of type $\alpha$, if the count of an element $a$ in $l$ equals the length of $l$, then the list consisting of $\text{count}(a, l)$ copies of $a$ is equal to $l$ itself, i.e., $\text{replicate}(\text{count}(a, l), a) = l$.
List.count_filter theorem
{l : List α} (h : p a) : count a (filter p l) = count a l
Full source 
@[simp] theorem count_filter {l : List α} (h : p a) : count a (filter p l) = count a l := by
  rw [count, countP_filter]; congr; funext b
  simp; rintro rfl; exact h
Count Preservation Under Filtering for Satisfying Elements
Informal description
For any list $l$ of elements of type $\alpha$ and a predicate $p : \alpha \to \text{Bool}$, if $p(a)$ holds for an element $a \in \alpha$, then the count of $a$ in the filtered list $\text{filter}\ p\ l$ is equal to the count of $a$ in the original list $l$, i.e., $$\text{count}_a(\text{filter}\ p\ l) = \text{count}_a(l).$$
List.count_le_count_map theorem
[DecidableEq β] {l : List α} {f : α → β} {x : α} : count x l ≤ count (f x) (map f l)
Full source 
theorem count_le_count_map [DecidableEq β] {l : List α} {f : α → β} {x : α} :
    count x l ≤ count (f x) (map f l) := by
  rw [count, count, countP_map]
  apply countP_mono_left; simp +contextual
Count Inequality Under List Mapping: $\mathtt{count}_x(l) \leq \mathtt{count}_{f(x)}(\mathtt{map}\ f\ l)$
Informal description
For any list $l$ of elements of type $\alpha$, any function $f : \alpha \to \beta$ (where $\beta$ has decidable equality), and any element $x \in \alpha$, the count of $x$ in $l$ is less than or equal to the count of $f(x)$ in the mapped list $\mathtt{map}\ f\ l$. That is, \[ \mathtt{count}\ x\ l \leq \mathtt{count}\ (f\ x)\ (\mathtt{map}\ f\ l). \]
List.count_filterMap theorem
{α} [BEq β] {b : β} {f : α → Option β} {l : List α} : count b (filterMap f l) = countP (fun a => f a == some b) l
Full source 
theorem count_filterMap {α} [BEq β] {b : β} {f : α → Option β} {l : List α} :
    count b (filterMap f l) = countP (fun a => f a == some b) l := by
  rw [count_eq_countP, countP_filterMap]
  congr
  ext a
  obtain _ | b := f a
  · simp
  · simp
Count of Elements in Filter-Mapped List Equals Count of Preimages Under Option Mapping
Informal description
For any type $\beta$ with a boolean equality relation, any element $b \in \beta$, any function $f : \alpha \to \text{Option } \beta$, and any list $l$ of elements of type $\alpha$, the count of occurrences of $b$ in the filtered-mapped list $\text{filterMap } f\ l$ is equal to the count of elements $a$ in $l$ for which $f(a) = \text{some } b$. That is, \[ \text{count}(b, \text{filterMap } f\ l) = \text{countP } (\lambda a, f(a) = \text{some } b)\ l. \]
List.count_flatMap theorem
{α} [BEq β] {l : List α} {f : α → List β} {x : β} : count x (l.flatMap f) = sum (map (count x ∘ f) l)
Full source 
theorem count_flatMap {α} [BEq β] {l : List α} {f : α → List β} {x : β} :
    count x (l.flatMap f) = sum (map (countcount x ∘ f) l) := countP_flatMap
Count Preservation under FlatMap: $\text{count}(x, \text{flatMap}\ f\ l) = \sum_{a \in l} \text{count}(x, f\ a)$
Informal description
For any list $l$ of elements of type $\alpha$, any function $f : \alpha \to \text{List}\ \beta$ (where $\beta$ has a boolean equality relation), and any element $x \in \beta$, the count of $x$ in the flat-mapped list $\text{flatMap}\ f\ l$ is equal to the sum of counts of $x$ in each sublist obtained by applying $f$ to elements of $l$. That is, \[ \text{count}(x, \text{flatMap}\ f\ l) = \sum_{a \in l} \text{count}(x, f\ a). \]
List.count_erase theorem
{a b : α} : ∀ {l : List α}, count a (l.erase b) = count a l - if b == a then 1 else 0
Full source 
theorem count_erase {a b : α} :
    ∀ {l : List α}, count a (l.erase b) = count a l - if b == a then 1 else 0
  | [] => by simp
  | c :: l => by
    rw [erase_cons]
    if hc : c = b then
      have hc_beq := beq_iff_eq.mpr hc
      rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
    else
      have hc_beq := beq_false_of_ne hc
      simp only [hc_beq, if_false, count_cons, count_cons, count_erase, reduceCtorEq]
      if ha : b = a then
        rw [ha, eq_comm] at hc
        rw [if_pos (beq_iff_eq.2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]
      else
        rw [if_neg (by simpa using ha), Nat.sub_zero, Nat.sub_zero]
Count After Erasure: $\text{count}(a, \text{erase}(l, b)) = \text{count}(a, l) - \mathbb{1}_{b = a}$
Informal description
For any elements $a$ and $b$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the list obtained by removing the first occurrence of $b$ from $l$ is equal to the count of $a$ in $l$ minus $1$ if $b = a$, and $0$ otherwise. That is, \[ \text{count}(a, \text{erase}(l, b)) = \text{count}(a, l) - \begin{cases} 1 & \text{if } b = a \\ 0 & \text{otherwise.} \end{cases} \]
List.count_erase_self theorem
{a : α} {l : List α} : count a (List.erase l a) = count a l - 1
Full source 
@[simp] theorem count_erase_self {a : α} {l : List α} :
    count a (List.erase l a) = count a l - 1 := by rw [count_erase, if_pos (by simp)]
Count Decreases by One After Self-Erasure: $\text{count}(a, \text{erase}(l, a)) = \text{count}(a, l) - 1$
Informal description
For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the list obtained by removing the first occurrence of $a$ from $l$ is equal to the count of $a$ in $l$ minus 1, i.e., \[ \text{count}(a, \text{erase}(l, a)) = \text{count}(a, l) - 1. \]
List.count_erase_of_ne theorem
(ab : a ≠ b) {l : List α} : count a (l.erase b) = count a l
Full source 
@[simp] theorem count_erase_of_ne (ab : a ≠ b) {l : List α} : count a (l.erase b) = count a l := by
  rw [count_erase, if_neg (by simpa using ab.symm), Nat.sub_zero]
Count Preservation Under Erasure of Distinct Element: $\text{count}(a, \text{erase}(l, b)) = \text{count}(a, l)$ for $a \neq b$
Informal description
For any elements $a$ and $b$ of type $\alpha$ such that $a \neq b$, and for any list $l$ of elements of type $\alpha$, the count of occurrences of $a$ in the list obtained by removing the first occurrence of $b$ from $l$ is equal to the count of $a$ in $l$. That is, \[ \text{count}(a, \text{erase}(l, b)) = \text{count}(a, l). \]