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
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.tail.val.iotaFind = i.tail
no goals