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

State before:
α : Type u_1
xs : List α
⊢ reverse xs = [] → xs = []
Tactic:
cases xs with
| nil => simp only [reverse_nil, forall_true_left]
| cons head tail =>
  intro h
  have h' : (reverse (reverse (head :: tail)) = []) := congrArg reverse h
  simp only [reverse_cons, reverse_append, reverse_nil, nil_append, reverse_reverse, singleton_append] at h'
State after:
no goals

State before:
case nil
α : Type u_1
⊢ reverse [] = [] → [] = []
Tactic:
simp only [reverse_nil, forall_true_left]
State after:
no goals

State before:
case cons
α : Type u_1
head : α
tail : List α
⊢ reverse (head :: tail) = [] → head :: tail = []
Tactic:
intro h
State after:
case cons
α : Type u_1
head : α
tail : List α
h : reverse (head :: tail) = []
⊢ head :: tail = []

State before:
case cons
α : Type u_1
head : α
tail : List α
h : reverse (head :: tail) = []
⊢ head :: tail = []
Tactic:
have h' : (reverse (reverse (head :: tail)) = []) := congrArg reverse h
State after:
case cons
α : Type u_1
head : α
tail : List α
h : reverse (head :: tail) = []
h' : reverse (reverse (head :: tail)) = []
⊢ head :: tail = []

State before:
case cons
α : Type u_1
head : α
tail : List α
h : reverse (head :: tail) = []
h' : reverse (reverse (head :: tail)) = []
⊢ head :: tail = []
Tactic:
simp only [reverse_cons, reverse_append, reverse_nil, nil_append, reverse_reverse, singleton_append] at h'
State after:
no goals