Theorem: list_length_zero_or_smaller_is_empty (Katydid/Std/Lists.lean)

State before:
α : Type u_1
xs : List α
⊢ length xs ≤ 0 → xs = []
Tactic:
cases xs with
| nil => intro; rfl
| cons head tail => intro; contradiction
State after:
no goals

State before:
case nil
α : Type u_1
⊢ length [] ≤ 0 → [] = []
Tactic:
intro
State after:
case nil
α : Type u_1
a✝ : length [] ≤ 0
⊢ [] = []

State before:
case nil
α : Type u_1
a✝ : length [] ≤ 0
⊢ [] = []
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
head : α
tail : List α
⊢ length (head :: tail) ≤ 0 → head :: tail = []
Tactic:
intro
State after:
case cons
α : Type u_1
head : α
tail : List α
a✝ : length (head :: tail) ≤ 0
⊢ head :: tail = []

State before:
case cons
α : Type u_1
head : α
tail : List α
a✝ : length (head :: tail) ≤ 0
⊢ head :: tail = []
Tactic:
contradiction
State after:
no goals