rw [Multiset.count_add]
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q + (P - M))
case a
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x N = Multiset.count x (N ∩ Q) + Multiset.count x (P - M)