have : M + P - N + N = (M + P) ∪ N := by apply Eq.refl
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this : M - N + P + N = M - N + N + P
⊢ M + P - N + N = M + P
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
h : N ≤ M
this✝ : M - N + P + N = M - N + N + P
this : M + P - N + N = M + P ∪ N
⊢ M + P - N + N = M + P