no goals
α : Type u_1
β : Type ?u.179823
γ : Type ?u.179826
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
⊢ s + u - (t + u) = s - t
rw [add_comm t, tsub_add_eq_tsub_tsub, add_tsub_cancel_right]