Theorem: Misc.List.Nodup.mem_erase_iff (LeanSAT/Util/Misc.lean)

State before:
α : Type u_1
l : List α
b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
d : l.Nodup
⊢ a ∈ l.erase b ↔ (a != b) = true ∧ a ∈ l
Tactic:
rw [List.Nodup.erase_eq_filter d, mem_filter, and_comm]
State after:
no goals