Theorem: List.Index.arr_eq_iff_eq_unarr (Extra/Index/Arr.lean)

State before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ arr h = k ↔ h = k.unarr
Tactic:
constructor
State after:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ arr h = k → h = k.unarr

case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ h = k.unarr → arr h = k

State before:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ arr h = k → h = k.unarr
Tactic:
intro h
State after:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h✝ : xs.Index → ys.Index
k : (xs.arr ys).Index
h : arr h✝ = k
⊢ h✝ = k.unarr

State before:
case mp
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h✝ : xs.Index → ys.Index
k : (xs.arr ys).Index
h : arr h✝ = k
⊢ h✝ = k.unarr
Tactic:
rw [←h, unarr_arr]
State after:
no goals

State before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h : xs.Index → ys.Index
k : (xs.arr ys).Index
⊢ h = k.unarr → arr h = k
Tactic:
intro h
State after:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h✝ : xs.Index → ys.Index
k : (xs.arr ys).Index
h : h✝ = k.unarr
⊢ arr h✝ = k

State before:
case mpr
α : Type u_1
β : Type u_2
xs : List α
ys : List β
h✝ : xs.Index → ys.Index
k : (xs.arr ys).Index
h : h✝ = k.unarr
⊢ arr h✝ = k
Tactic:
rw [h, arr_unarr]
State after:
no goals