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

State before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index ⊕ ys.Index
⊢ (match i with
    | Sum.inl i => Sum.inl i.val
    | Sum.inr j => Sum.inr j.val) =
    (sum i).val
Tactic:
match i with
| .inl i => simp only [sum, val_append, val_map]
| .inr j => simp only [sum, val_append, val_map]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i✝ : xs.Index ⊕ ys.Index
i : xs.Index
⊢ (match Sum.inl i with
    | Sum.inl i => Sum.inl i.val
    | Sum.inr j => Sum.inr j.val) =
    (sum (Sum.inl i)).val
Tactic:
simp only [sum, val_append, val_map]
State after:
no goals

State before:
α : Type u_1
β : Type u_2
xs : List α
ys : List β
i : xs.Index ⊕ ys.Index
j : ys.Index
⊢ (match Sum.inr j with
    | Sum.inl i => Sum.inl i.val
    | Sum.inr j => Sum.inr j.val) =
    (sum (Sum.inr j)).val
Tactic:
simp only [sum, val_append, val_map]
State after:
no goals