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

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

State before:
case nil
α : Type u_1
β : Type u_2
f : α → β
i : (List.map f []).Index
⊢ map f (unmap f i) = i
Tactic:
contradiction
State after:
no goals

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

State before:
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : ∀ (i : (List.map f xs).Index), map f (unmap f i) = i
i : (List.map f (x :: xs)).Index
⊢ map f (unmap f head) = head
Tactic:
rfl
State after:
no goals

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