Theorem: List.length_nonempty (LeanColls/Data/List.lean)

State before:
α : Type u_1
lst : Nonempty α
⊢ lst.toList.length > 0
Tactic:
have := lst.property
State after:
α : Type u_1
lst : Nonempty α
this : ↑lst ≠ []
⊢ lst.toList.length > 0

State before:
α : Type u_1
lst : Nonempty α
this : ↑lst ≠ []
⊢ lst.toList.length > 0
Tactic:
cases h : lst.val with
| nil        => contradiction
| cons hd tl => simp [Nonempty.toList, h]
State after:
no goals

State before:
case nil
α : Type u_1
lst : Nonempty α
this : ↑lst ≠ []
h : ↑lst = []
⊢ lst.toList.length > 0
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
lst : Nonempty α
this : ↑lst ≠ []
hd : α
tl : List α
h : ↑lst = hd :: tl
⊢ lst.toList.length > 0
Tactic:
simp [Nonempty.toList, h]
State after:
no goals