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

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

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

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

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

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

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