rw [← Multiset.one_le_count_iff_mem] at x_in_X
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : x ∈ X
x_notin_Y : x ∉ Y
⊢ Multiset.count x X ≥ 1
α : Type u_1
inst✝ : DecidableEq α
x : α
X Y : Multiset α
x_in_X : 1 ≤ Multiset.count x X
x_notin_Y : x ∉ Y
⊢ Multiset.count x X ≥ 1