Theorem: List.Index.sum_unsum (Extra/Index/Sum.lean)

State before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
⊢ sum k.unsum = k
Tactic:
match h : unappend k with
| .inl i => rw [unappend_eq_iff_eq_append] at h; simp only [h, unsum, unappend_append, sum, map_unmap]
| .inr j => rw [unappend_eq_iff_eq_append] at h; simp only [h, unsum, unappend_append, sum, map_unmap]
State after:
no goals

State before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : (List.map Sum.inl xs).Index
h : k.unappend = Sum.inl i
⊢ sum k.unsum = k
Tactic:
rw [unappend_eq_iff_eq_append] at h
State after:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : (List.map Sum.inl xs).Index
h : k = append (Sum.inl i)
⊢ sum k.unsum = k

State before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : (List.map Sum.inl xs).Index
h : k = append (Sum.inl i)
⊢ sum k.unsum = k
Tactic:
simp only [h, unsum, unappend_append, sum, map_unmap]
State after:
no goals

State before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
j : (List.map Sum.inr ys).Index
h : k.unappend = Sum.inr j
⊢ sum k.unsum = k
Tactic:
rw [unappend_eq_iff_eq_append] at h
State after:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
j : (List.map Sum.inr ys).Index
h : k = append (Sum.inr j)
⊢ sum k.unsum = k

State before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
j : (List.map Sum.inr ys).Index
h : k = append (Sum.inr j)
⊢ sum k.unsum = k
Tactic:
simp only [h, unsum, unappend_append, sum, map_unmap]
State after:
no goals