have : Multiset.count x Y = 0 := by apply Multiset.count_eq_zero_of_not_mem; exact x_notin_Y
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this : Multiset.count x X ≥ 1
⊢ x ∈ X - Y
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
this✝ : Multiset.count x X ≥ 1
this : Multiset.count x Y = 0
⊢ x ∈ X - Y