Theorem: List.Index.val_unsum (Extra/Index/Sum.lean)

State before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
k : (xs.sum ys).Index
⊢ k.val =
    match k.unsum with
    | Sum.inl i => Sum.inl i.val
    | Sum.inr j => Sum.inr j.val
Tactic:
rw [←sum_unsum k, val_sum, unsum_sum]
State after:
no goals