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]
case succ
n✝ n : Nat
H : ∀ (i : (Fin.iota n).Index), i.val.iotaFind = i
i : (Fin.iota (n + 1)).Index
⊢ i.val.iotaFind = i
no goals