split_ifs
case mpr.cons
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
⊢ x ∈ if a ≤ y then a :: y :: ys else y :: insert' a ys
case pos
α : Type
hp : LE α
inst✝ : DecidableRel LE.le
x a y : α
ys : List α
ih : x = a ∨ x ∈ ys → x ∈ insert' a ys
hor : x = a ∨ x ∈ y :: ys
h✝ : a ≤ y
⊢ x ∈ a :: y :: ys

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