induction n with
| zero => cases i; contradiction
| succ n H =>
  match i with
  | ⟨0,_⟩ => rfl
  | ⟨i+1,hi⟩ =>
    apply Fin.eq
    open List.Index in rw [iotaFind, val_tail, val_map, H, Fin.succ]
n✝ n : Nat
i : Fin n
⊢ i.iotaFind.val = i
no goals