Theorem: List.Index.val_unmap (Extra/Index/Map.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : (List.map f xs).Index
⊢ i.val = f (unmap f i).val
Tactic:
rw [←map_unmap f i, val_map, unmap_map]
State after:
no goals