Theorem: List.Index.unprod_eq_iff_eq_prod (Extra/Index/Prod.lean)

State before:
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i.unprod = j ↔ i = prod j
Tactic:
constructor
State after:
case mp
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i.unprod = j → i = prod j

case mpr
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i = prod j → i.unprod = j

State before:
case mp
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i.unprod = j → i = prod j
Tactic:
intro h
State after:
case mp
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
h : i.unprod = j
⊢ i = prod j

State before:
case mp
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
h : i.unprod = j
⊢ i = prod j
Tactic:
rw [←h, prod_unprod]
State after:
no goals

State before:
case mpr
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
⊢ i = prod j → i.unprod = j
Tactic:
intro h
State after:
case mpr
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
h : i = prod j
⊢ i.unprod = j

State before:
case mpr
α : Type u_2
β : Type u_1
xs : List α
ys : List β
i : (xs.prod ys).Index
j : xs.Index × ys.Index
h : i = prod j
⊢ i.unprod = j
Tactic:
rw [h, unprod_prod]
State after:
no goals