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

State before:
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
i : (i : xs.Index) × (f i.val).Index
⊢ (bind f i).val = i.snd.val
Tactic:
induction xs with
| nil => cases i; contradiction
| cons x xs ih =>
  match i with
  | ⟨head, j⟩ => rw [bind, val_append_inl]
  | ⟨tail i, j⟩ => rw [bind, val_append_inr, ih]
State after:
no goals

State before:
case nil
α : Type u_1
β : Type u_2
f : α → List β
i : (i : [].Index) × (f i.val).Index
⊢ (bind f i).val = i.snd.val
Tactic:
cases i
State after:
case nil.mk
α : Type u_1
β : Type u_2
f : α → List β
fst✝ : [].Index
snd✝ : (f fst✝.val).Index
⊢ (bind f ⟨fst✝, snd✝⟩).val = ⟨fst✝, snd✝⟩.snd.val

State before:
case nil.mk
α : Type u_1
β : Type u_2
f : α → List β
fst✝ : [].Index
snd✝ : (f fst✝.val).Index
⊢ (bind f ⟨fst✝, snd✝⟩).val = ⟨fst✝, snd✝⟩.snd.val
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (bind f i).val = i.snd.val
i : (i : (x :: xs).Index) × (f i.val).Index
⊢ (bind f i).val = i.snd.val
Tactic:
match i with
| ⟨head, j⟩ => rw [bind, val_append_inl]
| ⟨tail i, j⟩ => rw [bind, val_append_inr, ih]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
f : α → List β
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (bind f i).val = i.snd.val
i : (i : (x :: xs).Index) × (f i.val).Index
j : (f head.val).Index
⊢ (bind f ⟨head, j⟩).val = ⟨head, j⟩.snd.val
Tactic:
rw [bind, val_append_inl]
State after:
no goals

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