no goals
α : Type u_1
β : Type ?u.8207
γ : Type ?u.8210
r : α → α → Prop
s t : Multiset α
a✝ : α
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : Nodup l
⊢ a ∈ Multiset.erase l b ↔ a ≠ b ∧ a ∈ l
rw [d.erase_eq_filter b, mem_filter, and_comm]