induction x using cons_induction generalizing i with
| empty => cases hi
| cons a x IH =>
  simp only [mapIdx_cons]
  cases i with
  | zero => simp only [getElem_cons_zero]
  | succ i =>
    simp only [getElem_cons_succ]
    have : i < x.size :=
      Nat.lt_of_succ_lt_succ <| trans (s:=Eq) hi (size_mapIdx' ..)
    rw [IH (f ∘ Fin.succ) i ((x.size_mapIdx' (f ∘ Fin.succ)).symm ▸ this)]
    rfl
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x : Array α
f : Fin (size x) → α → β
i : Nat
hi : i < size (mapIdx x f)
⊢ (mapIdx x f)[i] = f { val := i, isLt := (_ : i < size x) } x[i]
no goals