simp only [← List.diff_erase]
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.erase x).diff l2).length < (l1.diff l2).length
α : Type
inst✝ : DecidableEq α
l1 l2 : List α
x : α
h1 : x ∈ l1
h2 : x ∉ l2
⊢ ((l1.diff l2).erase x).length < (l1.diff l2).length