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

State before:
α : Type u_1
⊢ ∀ {xs ys zs : List α}, xs = ys → xs ++ zs = ys ++ zs
Tactic:
intro xs ys zs H
State after:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs ++ zs = ys ++ zs

State before:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs ++ zs = ys ++ zs
Tactic:
simp only [append_cancel_right_eq]
State after:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs = ys

State before:
α : Type u_1
xs ys zs : List α
H : xs = ys
⊢ xs = ys
Tactic:
assumption
State after:
no goals