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

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

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

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

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

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

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