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

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

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