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.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