Theorem: List.Index.append_eq_iff_eq_unappend (Extra/Index/Append.lean)

State before:
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ append i = j ↔ i = j.unappend
Tactic:
constructor
State after:
case mp
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ append i = j → i = j.unappend

case mpr
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ i = j.unappend → append i = j

State before:
case mp
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ append i = j → i = j.unappend
Tactic:
intro h
State after:
case mp
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
h : append i = j
⊢ i = j.unappend

State before:
case mp
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
h : append i = j
⊢ i = j.unappend
Tactic:
rw [←h, unappend_append]
State after:
no goals

State before:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
⊢ i = j.unappend → append i = j
Tactic:
intro h
State after:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
h : i = j.unappend
⊢ append i = j

State before:
case mpr
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
j : (xs ++ ys).Index
h : i = j.unappend
⊢ append i = j
Tactic:
rw [h, append_unappend]
State after:
no goals