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

State before:
α : Type u_1
xs : List α
⊢ length xs = 0 → xs = []
Tactic:
cases xs
State after:
case nil
α : Type u_1
⊢ length [] = 0 → [] = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
⊢ length (head✝ :: tail✝) = 0 → head✝ :: tail✝ = []

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 h'
State after:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h' : length (head✝ :: tail✝) = 0
⊢ head✝ :: tail✝ = []

State before:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h' : length (head✝ :: tail✝) = 0
⊢ head✝ :: tail✝ = []
Tactic:
simp only [length, add_eq_zero_iff, and_false] at h'
State after:
no goals