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

State before:
α : Type u_1
xs : List α
i : xs.indexIota.Index
⊢ i.val.iota = i
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  match i with
  | head => rfl
  | tail i => rw [←map_unmap Index.tail i, val_tail, val_unmap Index.tail, iota, ih, map_unmap]
State after:
no goals

State before:
case nil
α : Type u_1
i : [].indexIota.Index
⊢ i.val.iota = i
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : ∀ (i : xs.indexIota.Index), i.val.iota = i
i : (x :: xs).indexIota.Index
⊢ i.val.iota = i
Tactic:
match i with
| head => rfl
| tail i => rw [←map_unmap Index.tail i, val_tail, val_unmap Index.tail, iota, ih, map_unmap]
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : xs.indexIota.Index), i.val.iota = i
i : (x :: xs).indexIota.Index
⊢ head.val.iota = head
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
ih : ∀ (i : xs.indexIota.Index), i.val.iota = i
i✝ : (x :: xs).indexIota.Index
i : (List.map tail xs.indexIota).Index
⊢ i.tail.val.iota = i.tail
Tactic:
rw [←map_unmap Index.tail i, val_tail, val_unmap Index.tail, iota, ih, map_unmap]
State after:
no goals