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

State before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
xs : List α
k : (xs.sigma f).Index
⊢ sigma k.unsigma = k
Tactic:
induction xs with
| nil => contradiction
| cons x xs ih =>
  match h : unappend k with
  | .inl j => rw [unappend_eq_iff_eq_append] at h; cases h; rw [unsigma, unappend_append, sigma, map_unmap]
  | .inr k => rw [unappend_eq_iff_eq_append] at h; cases h; rw [unsigma, unappend_append, sigma, ih]
State after:
no goals

State before:
case nil
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
k : ([].sigma f).Index
⊢ sigma k.unsigma = k
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : ((x :: xs).sigma f).Index
⊢ sigma k.unsigma = k
Tactic:
match h : unappend k with
| .inl j => rw [unappend_eq_iff_eq_append] at h; cases h; rw [unsigma, unappend_append, sigma, map_unmap]
| .inr k => rw [unappend_eq_iff_eq_append] at h; cases h; rw [unsigma, unappend_append, sigma, ih]
State after:
no goals

State before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : ((x :: xs).sigma f).Index
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
h : k.unappend = Sum.inl j
⊢ sigma k.unsigma = k
Tactic:
rw [unappend_eq_iff_eq_append] at h
State after:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : ((x :: xs).sigma f).Index
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
h : k = append (Sum.inl j)
⊢ sigma k.unsigma = k

State before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : ((x :: xs).sigma f).Index
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
h : k = append (Sum.inl j)
⊢ sigma k.unsigma = k
Tactic:
cases h
State after:
case refl
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
⊢ sigma (append (Sum.inl j)).unsigma = append (Sum.inl j)

State before:
case refl
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
j : ((fun a => List.map (Sigma.mk a) (f a)) x).Index
⊢ sigma (append (Sum.inl j)).unsigma = append (Sum.inl j)
Tactic:
rw [unsigma, unappend_append, sigma, map_unmap]
State after:
no goals

State before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k✝ : ((x :: xs).sigma f).Index
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
h : k✝.unappend = Sum.inr k
⊢ sigma k✝.unsigma = k✝
Tactic:
rw [unappend_eq_iff_eq_append] at h
State after:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k✝ : ((x :: xs).sigma f).Index
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
h : k✝ = append (Sum.inr k)
⊢ sigma k✝.unsigma = k✝

State before:
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k✝ : ((x :: xs).sigma f).Index
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
h : k✝ = append (Sum.inr k)
⊢ sigma k✝.unsigma = k✝
Tactic:
cases h
State after:
case refl
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
⊢ sigma (append (Sum.inr k)).unsigma = append (Sum.inr k)

State before:
case refl
α : Type u_1
σ✝ : α → Type u_2
f : (a : α) → List (σ✝ a)
x : α
xs : List α
ih : ∀ (k : (xs.sigma f).Index), sigma k.unsigma = k
k : (List.map (fun a => List.map (Sigma.mk a) (f a)) xs).join.Index
⊢ sigma (append (Sum.inr k)).unsigma = append (Sum.inr k)
Tactic:
rw [unsigma, unappend_append, sigma, ih]
State after:
no goals