conv => lhs; rw [fins_succ]
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
⊢ get? (fins (Nat.succ n')) j = some { val := j, isLt := ⋯ }
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }