rw [Finsupp.update_eq_erase_add_single]
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₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) =
    (f.update i (f i)).sum g + g i a
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₂
⊢ (((Finsupp.erase i f).sum fun i => g i) + (Finsupp.single i a).sum fun i => g i) + g i (f i) =
    (Finsupp.erase i f + Finsupp.single i (f i)).sum g + g i a