induction n with
| zero => contradiction
| succ n H =>
  match i with
  | .head => rfl
  | .tail (i : List.Index ((Fin.iota n).map Fin.succ)) =>
    calc
    _ = iotaFind (List.Index.val (.tail i : List.Index (Fin.iota (n+1)))) := rfl
    _ = iotaFind (List.Index.val i) := by rw [List.Index.val_tail]
    _ = iotaFind (List.Index.val (List.Index.map Fin.succ (List.Index.unmap Fin.succ i))) := by rw [List.Index.map_unmap]
    _ = iotaFind (Fin.succ (List.Index.val (List.Index.unmap Fin.succ i))) := by rw [List.Index.val_map]
    _ = .tail (List.Index.map Fin.succ (iotaFind (List.Index.val (List.Index.unmap Fin.succ i)))) := by rw [iotaFind_succ]
    _ = .tail (List.Index.map Fin.succ (List.Index.unmap Fin.succ i)) := by rw [H]
    _ = .tail i := by rw [List.Index.map_unmap]
n✝ n : Nat
i : (Fin.iota n).Index
⊢ i.val.iotaFind = i
no goals