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
case cons
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
a : α
x : Array α
IH :
  ∀ (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]
f : Fin (size (cons a x)) → α → β
i : Nat
hi : i < size (mapIdx (cons a x) f)
⊢ (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ)))[i] =
    f { val := i, isLt := (_ : i < size (cons a x)) } (cons a x)[i]
no goals