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

State before:
α✝ : Type u_1
xs ys : List α✝
i : xs.Index
⊢ i.append_inl.val = i.val
Tactic:
induction i with
| head => rfl
| tail _ ih => exact ih
State after:
no goals

State before:
case head
α✝ : Type u_1
xs ys : List α✝
x✝ : α✝
xs✝ : List α✝
⊢ head.append_inl.val = head.val
Tactic:
rfl
State after:
no goals

State before:
case tail
α✝ : Type u_1
xs ys xs✝ : List α✝
x✝ : α✝
a✝ : xs✝.Index
ih : a✝.append_inl.val = a✝.val
⊢ a✝.tail.append_inl.val = a✝.tail.val
Tactic:
exact ih
State after:
no goals