English
If f,g,h: ι → R satisfy f = g = h outside a distinguished i where f(i) = g(i) + h(i), then the product over s of f equals the sum of the products over t⊆s of (∏ f on t) (∏ g on s\\t).
Русский
Пусть f,g,h: ι → R совпадают вне индекса i, и в i выполняется f(i) = g(i) + h(i). Тогда произведение по i∈s f(i) равно сумме по подмножествам t⊆s произведений по t от f и по s\\t от g.
LaTeX
$$$\\prod_{i\\in s} f(i) = \\sum_{t\\subseteq s} \\left( \\prod_{i\\in t} f(i) \\right) \\left( \\prod_{i\\in s\\setminus t} g(i) \\right)$$$
Lean4
/-- If `f = g = h` everywhere but at `i`, where `f i = g i + h i`, then the product of `f` over `s`
is the sum of the products of `g` and `h`. -/
theorem prod_add_prod_eq {s : Finset ι} {i : ι} {f g h : ι → R} (hi : i ∈ s) (h1 : g i + h i = f i)
(h2 : ∀ j ∈ s, j ≠ i → g j = f j) (h3 : ∀ j ∈ s, j ≠ i → h j = f j) :
(∏ i ∈ s, g i) + ∏ i ∈ s, h i = ∏ i ∈ s, f i := by
classical
simp_rw [prod_eq_mul_prod_diff_singleton hi, ← h1, right_distrib]
congr 2 <;> apply prod_congr rfl <;> simpa
