Theorem: List.Index.val_iota (Extra/Index/Iota.lean)

State before:
α✝ : Type u_1
xs : List α✝
i : xs.Index
⊢ i.iota.val = i
Tactic:
induction i with
| head => rfl
| tail i ih => rw [iota, val_tail, val_map, ih]
State after:
no goals

State before:
case head
α✝ : Type u_1
xs : List α✝
x✝ : α✝
xs✝ : List α✝
⊢ head.iota.val = head
Tactic:
rfl
State after:
no goals

State before:
case tail
α✝ : Type u_1
xs xs✝ : List α✝
x✝ : α✝
i : xs✝.Index
ih : i.iota.val = i
⊢ i.tail.iota.val = i.tail
Tactic:
rw [iota, val_tail, val_map, ih]
State after:
no goals