∀ {m : Type u → Type v} [inst : Bind m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)],
  (∀ {α β : Type u} {a₁ a₂ : m α} {f : α → m β},
      Lean.Order.PartialOrder.rel a₁ a₂ → Lean.Order.PartialOrder.rel (a₁ >>= f) (a₂ >>= f)) →
    (∀ {α β : Type u} {a : m α} {f₁ f₂ : α → m β},
        (∀ (x : α), Lean.Order.PartialOrder.rel (f₁ x) (f₂ x)) → Lean.Order.PartialOrder.rel (a >>= f₁) (a >>= f₂)) →
      Lean.Order.MonoBind m