English
For natural numbers a,b, count p (a+b) equals count p a plus count (p ∘ (a+·)) b.
Русский
Для натуральных a,b: count p (a+b) = count p a + count (обозначение p( a+· )) b.
LaTeX
$$$$\operatorname{count}(p, a+b) = \operatorname{count}(p, a) + \operatorname{count}(\lambda k. p(a+k), b).$$$$
Lean4
theorem count_add (a b : ℕ) : count p (a + b) = count p a + count (fun k ↦ p (a + k)) b :=
by
have : Disjoint ({x ∈ range a | p x}) ({x ∈ (range b).map <| addLeftEmbedding a | p x}) := by
grind [Finset.disjoint_left]
simp_rw [count_eq_card_filter_range, range_add, filter_union, card_union_of_disjoint this, filter_map,
addLeftEmbedding, card_map, Function.Embedding.coeFn_mk, Function.comp_def]
