Theorem: List.Index.val_option (Extra/Index/Option.lean)

State before:
α : Type u_1
xs : List α
i : Option xs.Index
⊢ (match i with
    | none => none
    | some i => some i.val) =
    (option i).val
Tactic:
match i with
| none => rfl
| some i => rw [option, val_map]
State after:
no goals

State before:
α : Type u_1
xs : List α
i : Option xs.Index
⊢ (match none with
    | none => none
    | some i => some i.val) =
    (option none).val
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
xs : List α
i✝ : Option xs.Index
i : xs.Index
⊢ (match some i with
    | none => none
    | some i => some i.val) =
    (option (some i)).val
Tactic:
rw [option, val_map]
State after:
no goals