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

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

State before:
α : Type u_1
xs ys zs : List α
H : xs ++ zs = ys ++ zs
⊢ xs = ys
Tactic:
simp only [append_cancel_right_eq] at H
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