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

State before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
⊢ (map f i).val = f i.val
Tactic:
induction i with
| head => rfl
| tail _ ih => exact ih
State after:
no goals

State before:
case head
α : Type u_1
β : Type u_2
f : α → β
xs : List α
x✝ : α
xs✝ : List α
⊢ (map f head).val = f head.val
Tactic:
rfl
State after:
no goals

State before:
case tail
α : Type u_1
β : Type u_2
f : α → β
xs xs✝ : List α
x✝ : α
a✝ : xs✝.Index
ih : (map f a✝).val = f a✝.val
⊢ (map f a✝.tail).val = f a✝.tail.val
Tactic:
exact ih
State after:
no goals