no goals
α : Type u_1
β : Type ?u.187851
γ : Type ?u.187854
inst✝ : DecidableEq α
s✝ t✝ u : Multiset α
a✝ b a : α
s t : Multiset α
⊢ a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t
simpa using add_union_distrib (a ::ₘ 0) s t