∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {P₁ P₂ Q : CategoryTheory.ObjectProperty C} [self : P₁.TensorLE P₂ Q] (X₁ X₂ : C),
  P₁ X₁ → P₂ X₂ → Q (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)