no goals
α : Type u_1
β : Type ?u.187191
γ : Type ?u.187194
inst✝ : DecidableEq α
s✝ t✝ u✝ : Multiset α
a b : α
s t u : Multiset α
⊢ s + (t ∪ u) = s + t ∪ (s + u)
rw [add_comm, union_add_distrib, add_comm s, add_comm s]