rw [Multiset.eq_union_left]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ M = M ∪ N
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
h : N ≤ M
⊢ N ≤ M