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

case right
α : Type
inst✝ : LinearOrder α
l : List α
head : α
tail : List α
hyp : head :: tail ≠ []
⊢ ∀ a ∈ tail, (if c : tail = [] then head else min head (smallest tail c)) ≤ a