rw [IH (f ∘ Fin.succ) i ((x.size_mapIdx' (f ∘ Fin.succ)).symm ▸ this)]
case cons.succ
α : 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 : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (mapIdx x (f ∘ Fin.succ))[i] = f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]
case cons.succ
α : 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 : Nat.succ i < size (mapIdx (cons a x) f)
this : i < size x
⊢ (f ∘ Fin.succ) { val := i, isLt := (_ : i < size x) } x[i] =
    f { val := Nat.succ i, isLt := (_ : Nat.succ i < size (cons a x)) } x[i]