no goals
α : Type u_2
β : Type ?u.565928
γ : Type ?u.565931
ι : Type ?u.565934
M : Type ?u.565937
M' : Type ?u.565940
N : Type ?u.565943
P : Type ?u.565946
G : Type u_1
H : Type ?u.565952
R : Type ?u.565955
S : Type ?u.565958
inst✝ : AddGroup G
f : α →₀ G
a : α
b : G
⊢ update f a b = f - single a (↑f a) + single a b
rw [update_eq_erase_add_single, erase_eq_sub_single]