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

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

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