simp only [List.mem_cons]
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x ∈ y :: ys
case neg
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x ∈ insert' a ys → x = a ∨ x ∈ ys
h✝ : ¬a ≤ y
hel : x = y ∨ x ∈ insert' a ys
⊢ x = a ∨ x = y ∨ x ∈ ys