∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (xs : Array α) (f : γ → α → m β),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Array.mapM (f x) xs