induction i generalizing j y with
| zero => dsimp [mapIdxM.map]; rw [pure_bind]
| succ i IH =>
  dsimp [mapIdxM.map]; simp only [bind_assoc]
  apply bind_congr; intro b'
  dsimp [push, cons, List.concat]
  exact IH ..
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
b : β
f' : Fin (size x) → α → m β
i j : Nat
h : i + j = size x
y : Array β
⊢ mapIdxM.map x f' i j h (cons b y) = do
    let y ← mapIdxM.map x f' i j h y
    pure (cons b y)
no goals