Theorem: List.Index.unsigma_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).unsigma = i
Tactic:
induction xs with
| nil => cases i; contradiction
| cons x xs ih =>
  match i with
  | ⟨head, j⟩ => simp only [sigma, unsigma, unappend_append, unmap_map]
  | ⟨tail i, j⟩ => simp only [sigma, unsigma, unappend_append]; rw [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).unsigma = i
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✝⟩).unsigma = ⟨fst✝, snd✝⟩

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✝⟩).unsigma = ⟨fst✝, snd✝⟩
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).unsigma = i
i : (i : (x :: xs).Index) × (f i.val).Index
⊢ (sigma i).unsigma = i
Tactic:
match i with
| ⟨head, j⟩ => simp only [sigma, unsigma, unappend_append, unmap_map]
| ⟨tail i, j⟩ => simp only [sigma, unsigma, unappend_append]; rw [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).unsigma = i
i : (i : (x :: xs).Index) × (f i.val).Index
j : (f head.val).Index
⊢ (sigma ⟨head, j⟩).unsigma = ⟨head, j⟩
Tactic:
simp only [sigma, unsigma, unappend_append, unmap_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).unsigma = i
i✝ : (i : (x :: xs).Index) × (f i.val).Index
i : xs.Index
j : (f i.tail.val).Index
⊢ (sigma ⟨i.tail, j⟩).unsigma = ⟨i.tail, j⟩
Tactic:
simp only [sigma, unsigma, unappend_append]
State after:
α : Type u_1
β : α → Type u_2
f : (x : α) → List (β x)
x : α
xs : List α
ih : ∀ (i : (i : xs.Index) × (f i.val).Index), (sigma i).unsigma = i
i✝ : (i : (x :: xs).Index) × (f i.val).Index
i : xs.Index
j : (f i.tail.val).Index
⊢ ⟨(sigma ⟨i, j⟩).unsigma.fst.tail, (sigma ⟨i, j⟩).unsigma.snd⟩ = ⟨i.tail, j⟩

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).unsigma = i
i✝ : (i : (x :: xs).Index) × (f i.val).Index
i : xs.Index
j : (f i.tail.val).Index
⊢ ⟨(sigma ⟨i, j⟩).unsigma.fst.tail, (sigma ⟨i, j⟩).unsigma.snd⟩ = ⟨i.tail, j⟩
Tactic:
rw [ih]
State after:
no goals