rw [insert_mem] at hy
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y ∈ insert' a xs
⊢ x ≤ y
case neg.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : (∀ a' ∈ xs, x ≤ a') ∧ List.Pairwise LE.le xs
h : ¬a ≤ x
y : α
hy : y = a ∨ y ∈ xs
⊢ x ≤ y