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

State before:
α✝ : Type u_1
xs ys : List α✝
i : xs.Index ⊕ ys.Index
⊢ (append i).unappend = i
Tactic:
induction xs generalizing ys with
| nil =>
  match i with
  | .inl i => contradiction
  | .inr j => rfl
| cons x xs ih =>
  match i with
  | .inl .head => rfl
  | .inl (.tail i) => simp only [append, unappend, ih]
  | .inr j => simp only [append, unappend, ih]
State after:
no goals

State before:
case nil
α✝ : Type u_1
ys : List α✝
i : [].Index ⊕ ys.Index
⊢ (append i).unappend = i
Tactic:
match i with
| .inl i => contradiction
| .inr j => rfl
State after:
no goals

State before:
α✝ : Type u_1
ys : List α✝
i✝ : [].Index ⊕ ys.Index
i : [].Index
⊢ (append (Sum.inl i)).unappend = Sum.inl i
Tactic:
contradiction
State after:
no goals

State before:
α✝ : Type u_1
ys : List α✝
i : [].Index ⊕ ys.Index
j : ys.Index
⊢ (append (Sum.inr j)).unappend = Sum.inr j
Tactic:
rfl
State after:
no goals

State before:
case cons
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (i : xs.Index ⊕ ys.Index), (append i).unappend = i
ys : List α✝
i : (x :: xs).Index ⊕ ys.Index
⊢ (append i).unappend = i
Tactic:
match i with
| .inl .head => rfl
| .inl (.tail i) => simp only [append, unappend, ih]
| .inr j => simp only [append, unappend, ih]
State after:
no goals

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

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

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
ih : ∀ {ys : List α✝} (i : xs.Index ⊕ ys.Index), (append i).unappend = i
ys : List α✝
i : (x :: xs).Index ⊕ ys.Index
j : ys.Index
⊢ (append (Sum.inr j)).unappend = Sum.inr j
Tactic:
simp only [append, unappend, ih]
State after:
no goals