rw [List.Index.map_unmap]
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i✝ : (Fin.iota (n + 1)).Index
i : (List.map succ (Fin.iota n)).Index
⊢ i.val.iotaFind = (List.Index.map succ (List.Index.unmap succ i)).val.iotaFind
no goals