intros M N P Q h
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
⊢ ∀ (M N P Q : Multiset α), M + N = P + Q → N = N ∩ Q + (P - M)
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N = N ∩ Q + (P - M)