∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ X')
  (q : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Y')
  (wf :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) q =
      CategoryTheory.CategoryStruct.comp p f')
  (wg :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) q =
      CategoryTheory.CategoryStruct.comp p g')
  (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π f g) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimMap
            (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) f' g' p q wf wg))
          (CategoryTheory.Limits.coequalizer.desc h wh))) =
    CategoryTheory.CategoryStruct.comp q h