rw [this]
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ (a0 ::ₘ X).erase a
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a a0 : α
M X : Multiset α
H : M = (a0 ::ₘ X).erase a
hyp : ¬a = a0
this : a0 ∈ (a0 ::ₘ X).erase a ↔ a0 ∈ a0 ::ₘ X
⊢ a0 ∈ a0 ::ₘ X