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

State before:
α✝ : Type u_1
xs ys : List α✝
k : (xs ++ ys).Index
⊢ append k.unappend = k
Tactic:
induction xs generalizing ys with
| nil => rfl
| cons x xs ih =>
  match k with
  | .head => rfl
  | .tail k =>
    simp only [unappend]
    split
    next h => rw [append, ←h, ih]
    next h => rw [append, ←h, ih]
State after:
no goals

State before:
case nil
α✝ : Type u_1
ys : List α✝
k : ([] ++ ys).Index
⊢ append k.unappend = k
Tactic:
rfl
State after:
no goals

State before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k : (x :: xs ++ ys).Index
⊢ append k.unappend = k
Tactic:
match k with
| .head => rfl
| .tail k =>
  simp only [unappend]
  split
  next h => rw [append, ←h, ih]
  next h => rw [append, ←h, ih]
State after:
no goals

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k : (x :: xs ++ ys).Index
⊢ append head.unappend = head
Tactic:
rfl
State after:
no goals

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
⊢ append k.tail.unappend = k.tail
Tactic:
simp only [unappend]
State after:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
⊢ append
      (match k.unappend with
      | Sum.inl i => Sum.inl i.tail
      | Sum.inr i => Sum.inr i) =
    k.tail

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
⊢ append
      (match k.unappend with
      | Sum.inl i => Sum.inl i.tail
      | Sum.inr i => Sum.inr i) =
    k.tail
Tactic:
split
State after:
case h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : xs.Index
heq✝ : k.unappend = Sum.inl i✝
⊢ append (Sum.inl i✝.tail) = k.tail

case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
heq✝ : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail

State before:
case h_1
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : xs.Index
heq✝ : k.unappend = Sum.inl i✝
⊢ append (Sum.inl i✝.tail) = k.tail

case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
heq✝ : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail
Tactic:
next h => rw [append, ←h, ih]
State after:
case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
heq✝ : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail

State before:
case h_2
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
heq✝ : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail
Tactic:
next h => rw [append, ←h, ih]
State after:
no goals

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : xs.Index
h : k.unappend = Sum.inl i✝
⊢ append (Sum.inl i✝.tail) = k.tail
Tactic:
rw [append, ←h, ih]
State after:
no goals

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (k : (xs ++ ys).Index), append k.unappend = k
ys : List α✝
k✝ : (x :: xs ++ ys).Index
k : (xs.append ys).Index
x✝ : xs.Index ⊕ ys.Index
i✝ : ys.Index
h : k.unappend = Sum.inr i✝
⊢ append (Sum.inr i✝) = k.tail
Tactic:
rw [append, ←h, ih]
State after:
no goals