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

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

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

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

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

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

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