have lem :
  min head (smallest tail h) = smallest tail h :=   by
    apply min_eq_right
    apply le_of_not_ge
    exact h'
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
⊢ min head (smallest tail h) ∈ tail
case neg
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
h : ¬tail = []
h' : ¬head ≤ smallest tail h
lem : min head (smallest tail h) = smallest tail h
⊢ min head (smallest tail h) ∈ tail