Theorem: List.head?_isSome (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
l : List α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).head?.isSome = true ↔ head✝ :: tail✝ ≠ []
Tactic:
simp
State after:
no goals