intros y hy
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ ∀ a' ∈ [], a ≤ a'
case nil.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
y : α
hy : y ∈ []
⊢ a ≤ y