classical
simp_rw [Finsupp.update_eq_erase_add_single]
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
conv_rhs => rw [← Finsupp.update_self f i]
rw [Finsupp.update_eq_erase_add_single]
rw [Finsupp.sum_add_index (fun i _ => hg i) fun i _ => hgg i]
rw [add_assoc]
rw [add_assoc]
congr 1
rw [add_comm]
rw [Finsupp.sum_single_index (hg _)]
rw [Finsupp.sum_single_index (hg _)]
R : Type ?u.11
ι : Type u_3
inst✝² : CommSemiring R
α : Type u_1
β : Type u_2
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f : ι →₀ α
i : ι
a : α
g : ι → α → β
hg : ∀ (i : ι), g i 0 = 0
hgg : ∀ (a : ι) (b₁ b₂ : α), g a (b₁ + b₂) = g a b₁ + g a b₂
⊢ (f.update i a).sum g + g i (f i) = f.sum g + g i a
no goals