rw [Multiset.ext] at h
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
x : α
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q
α : Type u_1
inst✝ : Preorder α
dec : DecidableEq α
M N P Q : Multiset α
h : ∀ (a : α), Multiset.count a (M + N) = Multiset.count a (P + Q)
x : α
⊢ Multiset.count x M + Multiset.count x N = Multiset.count x P + Multiset.count x Q