apply And.intro
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ head ∧
    ∀ a ∈ tail, (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a
case left
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ head

case right
l : List ℕ
head : ℕ
tail : List ℕ
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else Nat.min head (smallest tail c)) ≤ a