Theorem: list_app_inv_head (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_left_eq] at H
State after:
α : Type u_1
xs ys zs : List α
H : ys = zs
⊢ ys = zs

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