rcases i with ⟨j,hj⟩
n : Nat
i : Fin (length (fins n))
⊢ get (fins n) i = { val := ↑i, isLt := ⋯ }
case mk
n j : Nat
hj : j < length (fins n)
⊢ get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }