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

State before:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ map f i = j ↔ i = unmap f j
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ map f i = j → i = unmap f j

case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ i = unmap f j → map f i = j

State before:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ map f i = j → i = unmap f j
Tactic:
intro h
State after:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
h : map f i = j
⊢ i = unmap f j

State before:
case mp
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
h : map f i = j
⊢ i = unmap f j
Tactic:
rw [←h, unmap_map]
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
⊢ i = unmap f j → map f i = j
Tactic:
intro h
State after:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
h : i = unmap f j
⊢ map f i = j

State before:
case mpr
α : Type u_1
β : Type u_2
f : α → β
xs : List α
i : xs.Index
j : (List.map f xs).Index
h : i = unmap f j
⊢ map f i = j
Tactic:
rw [h, map_unmap]
State after:
no goals