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