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

State before:
α : Type u_1
n : ℕ
xs ys : List α
⊢ reverse xs = reverse ys → xs = ys
Tactic:
intro h
State after:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
⊢ xs = ys

State before:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
⊢ xs = ys
Tactic:
have h' : reverse (reverse xs) = reverse (reverse ys) :=
  congrArg reverse h
State after:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
h' : reverse (reverse xs) = reverse (reverse ys)
⊢ xs = ys

State before:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
h' : reverse (reverse xs) = reverse (reverse ys)
⊢ xs = ys
Tactic:
simp only [reverse_reverse] at h'
State after:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
h' : xs = ys
⊢ xs = ys

State before:
α : Type u_1
n : ℕ
xs ys : List α
h : reverse xs = reverse ys
h' : xs = ys
⊢ xs = ys
Tactic:
assumption
State after:
no goals