no goals
α : Type u_1
β : Type ?u.308019
γ : Type ?u.308022
ι : Type ?u.308025
M : Type u_2
M' : Type ?u.308031
N : Type ?u.308034
P : Type ?u.308037
G : Type ?u.308040
H : Type ?u.308043
R : Type ?u.308046
S : Type ?u.308049
inst✝ : AddZeroClass M
a : α
f : α →₀ M
⊢ erase a f + single a (↑f a) = f
rw [← update_eq_erase_add_single, update_self]