Theorem: List.Index.unbind_bind (Extra/Index/Bind.lean)

State before:
α : Type u_1
β : Type u_2
f : α → List β
xs : List α
i : xs.Index
j : (f i.val).Index
⊢ unbind f (bind f ⟨i, j⟩) = ⟨i, j⟩
Tactic:
induction i with simp only [bind, unbind, unappend_append]
| tail _ ih => rw [ih]
State after:
no goals

State before:
case tail
α : Type u_1
β : Type u_2
f : α → List β
xs xs✝ : List α
x✝ : α
a✝ : xs✝.Index
ih : ∀ (j : (f a✝.val).Index), unbind f (bind f ⟨a✝, j⟩) = ⟨a✝, j⟩
j : (f a✝.tail.val).Index
⊢ ⟨(unbind f (bind f ⟨a✝, j⟩)).fst.tail, (unbind f (bind f ⟨a✝, j⟩)).snd⟩ = ⟨a✝.tail, j⟩
Tactic:
rw [ih]
State after:
no goals