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