English
If two maps g1,g2 : σ → S1 agree on all indices that actually appear in p (i.e., for every i and every c with i ∈ supp(c) and coeff c p ≠ 0, g1 i = g2 i), then eval₂ f g1 p = eval₂ f g2 p.
Русский
Если две функции g1,g2 : σ → S1 совпадают на всех индексах, которые действительно встречаются в p, то eval₂ f g1 p = eval₂ f g2 p.
LaTeX
$$$\\Big( \\forall i,c,\, i \\in \\operatorname{supp}(c) \\Rightarrow \\coeff c p \\neq 0 \\Rightarrow g_1 i = g_2 i \\Big) \\Rightarrow \\mathrm{eval}_2 f g_1 p = \\mathrm{eval}_2 f g_2 p$$$
Lean4
theorem eval₂_congr (g₁ g₂ : σ → S₁) (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i) :
p.eval₂ f g₁ = p.eval₂ f g₂ := by
apply Finset.sum_congr rfl
intro C hc; dsimp; congr 1
apply Finset.prod_congr rfl
intro i hi; dsimp; congr 1
apply h hi
rwa [Finsupp.mem_support_iff] at hc
