Theorem: List.Index.val_join (Extra/Index/Join.lean)

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

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

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

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

State before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).val = i.snd.val
i : (i : (xs :: xss).Index) × i.val.Index
j : head.val.Index
⊢ (join ⟨head, j⟩).val = ⟨head, j⟩.snd.val
Tactic:
rw [join, val_append_inl]
State after:
no goals

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