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