no goals
α : Type u_1
β : Type ?u.97707
γ : Type ?u.97710
inst✝ : DecidableEq α
s✝ t✝ : Multiset α
a✝ b a : α
s t : Multiset α
h : a ∈ t
⊢ erase (s + t) a = s + erase t a
rw [add_comm, erase_add_left_pos s h, add_comm]