English
If for a fixed element a, membership in s and the equality of f(a) with b are given and a is in s, then the product over s with f replaced still equals the same value after adjusting by b.
Русский
Если существует элемент a в s и f(a) соответствует некоторому b, тогда изменение в одной позиции не изменит произведение.
LaTeX
$$$a \\in s \\rightarrow (a ∈ s) \\rightarrow b_1 = b_2 \\Rightarrow (\\prod_{a∈s} f(a)) b_1 = (\\prod_{a∈s} f(a)) b_2$$$
Lean4
@[to_additive]
theorem prod_mul_eq_prod_mul_of_exists {s : Finset ι} {f : ι → M} {b₁ b₂ : M} (a : ι) (ha : a ∈ s)
(h : f a * b₁ = f a * b₂) : (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂ := by
classical
rw [← insert_erase ha]
simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]
