simp [h, Fin.last]
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? [Fin.last n'] (j - length (map Fin.castSucc (fins n'))) = some { val := j, isLt := ⋯ }
no goals