Theorem: List.Index.val_sigma (Extra/Index/Sigma.lean)

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

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

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

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

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

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