cases i with
| zero => simp
| succ i =>
  simp
  rw [length_cons, succ_lt_succ_iff] at hi
  rw [ih hi, Nat.sub_add_cancel (zero_lt_of_lt hi)]
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i < (t :: l).length
⊢ ((t :: l).eraseIdx i).length = (t :: l).length - 1
no goals