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

State before:
α : Type u_1
xs ys : List α
x y : α
⊢ xs = ys ∧ x = y → xs ++ [x] = ys ++ [y]
Tactic:
intro H
State after:
α : Type u_1
xs ys : List α
x y : α
H : xs = ys ∧ x = y
⊢ xs ++ [x] = ys ++ [y]

State before:
α : Type u_1
xs ys : List α
x y : α
H : xs = ys ∧ x = y
⊢ xs ++ [x] = ys ++ [y]
Tactic:
cases H with
| intro H1 H2 =>
  rw [H1, H2]
State after:
no goals

State before:
case intro
α : Type u_1
xs ys : List α
x y : α
H1 : xs = ys
H2 : x = y
⊢ xs ++ [x] = ys ++ [y]
Tactic:
rw [H1, H2]
State after:
no goals