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