no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
hl₁ : Nodup l₁
⊢ a ∈ List.diff l₁ l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂
rw [hl₁.diff_eq_filter, mem_filter, decide_eq_true_iff]