Theorem: List.Index.val_append_inr (Extra/Index/Append.lean)

State before:
α✝ : Type u_1
ys xs : List α✝
j : ys.Index
⊢ j.append_inr.val = j.val
Tactic:
induction xs with
| nil => rfl
| cons _ _ ih => exact ih
State after:
no goals

State before:
case nil
α✝ : Type u_1
ys : List α✝
j : ys.Index
⊢ j.append_inr.val = j.val
Tactic:
rfl
State after:
no goals

State before:
case cons
α✝ : Type u_1
ys : List α✝
j : ys.Index
head✝ : α✝
tail✝ : List α✝
ih : j.append_inr.val = j.val
⊢ j.append_inr.val = j.val
Tactic:
exact ih
State after:
no goals