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

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

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

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

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

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

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