apply bind_congr
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ (match size { data := a :: x.data }, (_ : size { data := a :: x.data } + 0 = size { data := a :: x.data } + 0) with
    | 0, x => pure #[]
    | Nat.succ i, inv => do
      let __do_lift ← f 0 { data := a :: x.data }[0]
      mapIdxM.map { data := a :: x.data } f i (0 + 1) (_ : i + (0 + 1) = size { data := a :: x.data })
          (push #[] __do_lift)) =
    do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
⊢ ∀ (a_1 : β),
    mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
        (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] a_1) =
      do
      let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
      pure (cons a_1 y)