theorem List.countP_set {α : Type u_1} {p : α → Bool} {l : List α} {i : Nat} {a : α} (h : i < l.length) : countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

theorem List.count_set {α : Type u_1} [BEq α] {a b : α} {l : List α} {i : Nat} (h : i < l.length) : count b (l.set i a) = (count b l - if (l[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0

theorem List.countP_replace {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {l : List α} {p : α → Bool} : countP p (l.replace a b) = if l.contains a = true then (countP p l + if p b = true then 1 else 0) - if p a = true then 1 else 0 else countP p l

theorem List.count_replace {α : Type u_1} [BEq α] [LawfulBEq α] {a b c : α} {l : List α} : count c (l.replace a b) = if l.contains a = true then (count c l + if (b == c) = true then 1 else 0) - if (a == c) = true then 1 else 0 else count c l

theorem List.count_insert {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {l : List α} : count a (List.insert b l) = max (count a l) (if (b == a) = true then 1 else 0)

theorem List.Sublist.le_countP {α✝ : Type u_1} {l₁ l₂ : List α✝} (s : l₁.Sublist l₂) (p : α✝ → Bool) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁

The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list, minus the difference in the lengths.

theorem List.IsPrefix.le_countP {α✝ : Type u_1} {l₁ l₂ : List α✝} {p : α✝ → Bool} (s : l₁ <+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁

theorem List.IsSuffix.le_countP {α✝ : Type u_1} {l₁ l₂ : List α✝} {p : α✝ → Bool} (s : l₁ <:+ l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁

theorem List.IsInfix.le_countP {α✝ : Type u_1} {l₁ l₂ : List α✝} {p : α✝ → Bool} (s : l₁ <:+: l₂) : countP p l₂ - (l₂.length - l₁.length) ≤ countP p l₁

theorem List.le_countP_tail {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} : countP p l - 1 ≤ countP p l.tail

The number of elements satisfying a predicate in the tail of a list is at least one less than the number of elements satisfying the predicate in the list.

theorem List.Sublist.le_count {α : Type u_1} [BEq α] {l₁ l₂ : List α} (s : l₁.Sublist l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁

theorem List.IsPrefix.le_count {α : Type u_1} [BEq α] {l₁ l₂ : List α} (s : l₁ <+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁

theorem List.IsSuffix.le_count {α : Type u_1} [BEq α] {l₁ l₂ : List α} (s : l₁ <:+ l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁

theorem List.IsInfix.le_count {α : Type u_1} [BEq α] {l₁ l₂ : List α} (s : l₁ <:+: l₂) (a : α) : count a l₂ - (l₂.length - l₁.length) ≤ count a l₁

theorem List.le_count_tail {α : Type u_1} [BEq α] {a : α} {l : List α} : count a l - 1 ≤ count a l.tail