Theorem: List.Index.unbind_eq_iff_eq_bind (Extra/Index/Bind.lean)

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

case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
⊢ i = bind f j → unbind f i = j

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

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

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

State before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (xs.bind f).Index
j : (i : xs.Index) × (f i.val).Index
h : i = bind f j
⊢ unbind f i = j
Tactic:
rw [h, unbind_bind]
State after:
no goals