no goals
α : Type u_1
β : Type ?u.305712
γ : Type ?u.305715
ι : Type ?u.305718
M : Type u_2
M' : Type ?u.305724
N : Type ?u.305727
P : Type ?u.305730
G : Type ?u.305733
H : Type ?u.305736
R : Type ?u.305739
S : Type ?u.305742
inst✝ : AddZeroClass M
a : α
f : α →₀ M
⊢ single a (↑f a) + erase a f = f
rw [← update_eq_single_add_erase, update_self]