no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
d : Nodup l
⊢ a ∈ List.erase l b ↔ a ≠ b ∧ a ∈ l
rw [d.erase_eq_filter, mem_filter, and_comm, decide_eq_true_iff]