simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M✝ X Y : Multiset α
a : α
M : M✝ = X + Y
nonsense : 0 = X + {a}
a✝ : ∀ y ∈ Y, y < a
⊢ a ∈ X + {a}
no goals