intros x X Y x_in_X x_notin_Y
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : α) (X Y : Multiset α), x ∈ X → x ∉ Y → x ∈ X - Y
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
⊢ x ∈ X - Y