rw [insert', List.mem_singleton] at hel
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x ∈ insert' a []
⊢ x = a ∨ x ∈ []
case mp.nil
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a : α
hel : x = a
⊢ x = a ∨ x ∈ []