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

State before:
α : Type u_1
x : α
xs : List α
⊢ xs ++ [x] ≠ []
Tactic:
intro h'
State after:
α : Type u_1
x : α
xs : List α
h' : xs ++ [x] = []
⊢ False

State before:
α : Type u_1
x : α
xs : List α
h' : xs ++ [x] = []
⊢ False
Tactic:
cases xs with
| nil =>
  contradiction
| cons head tail =>
  contradiction
State after:
no goals

State before:
case nil
α : Type u_1
x : α
h' : [] ++ [x] = []
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
x head : α
tail : List α
h' : head :: tail ++ [x] = []
⊢ False
Tactic:
contradiction
State after:
no goals