Theorem: List.Index.toFin_ofFin (Extra/Index/Basic.lean)

State before:
α : Type u_1
xs : List α
i : Fin xs.length
⊢ (Index.ofFin i).toFin = i
Tactic:
apply Fin.eq_of_val_eq
State after:
case a
α : Type u_1
xs : List α
i : Fin xs.length
⊢ ↑(Index.ofFin i).toFin = ↑i

State before:
case a
α : Type u_1
xs : List α
i : Fin xs.length
⊢ ↑(Index.ofFin i).toFin = ↑i
Tactic:
apply toNat_ofFin
State after:
no goals