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

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

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

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