Theorem: List.Index.val_append (Extra/Index/Append.lean)

State before:
α : Type u_1
xs ys : List α
i : xs.Index ⊕ ys.Index
⊢ (append i).val =
    match i with
    | Sum.inl i => i.val
    | Sum.inr j => j.val
Tactic:
match i with
| .inl _ => exact val_append_inl ..
| .inr _ => exact val_append_inr ..
State after:
no goals

State before:
α : Type u_1
xs ys : List α
i : xs.Index ⊕ ys.Index
val✝ : xs.Index
⊢ (append (Sum.inl val✝)).val =
    match Sum.inl val✝ with
    | Sum.inl i => i.val
    | Sum.inr j => j.val
Tactic:
exact val_append_inl ..
State after:
no goals

State before:
α : Type u_1
xs ys : List α
i : xs.Index ⊕ ys.Index
val✝ : ys.Index
⊢ (append (Sum.inr val✝)).val =
    match Sum.inr val✝ with
    | Sum.inl i => i.val
    | Sum.inr j => j.val
Tactic:
exact val_append_inr ..
State after:
no goals