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

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

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

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

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

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

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