have lem : 
  Nat.min head (smallest tail (by simp [c])) = smallest tail (by simp [c]) := by
    apply Nat.min_eq_right
    apply Nat.le_of_not_le 
    assumption
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail
case neg.h
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
c : ¬tail = []
c' : ¬head ≤ smallest tail ⋯
lem : Nat.min head (smallest tail ⋯) = smallest tail ⋯
⊢ Nat.min head (smallest tail ⋯) ∈ tail