{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F₁ F₂ : CategoryTheory.Functor C D} →
              {τ : F₁ ⟶ F₂} →
                [inst_4 : F₁.LaxMonoidal] →
                  [inst_5 : F₂.LaxMonoidal] →
                    {motive : CategoryTheory.NatTrans.IsMonoidal τ → Sort u} →
                      ((unit :
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F₁)
                                (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
                              CategoryTheory.Functor.LaxMonoidal.ε F₂) →
                          (tensor :
                              ∀ (X Y : C),
                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F₁ X Y)
                                    (τ.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) =
                                  CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.tensorHom (τ.app X) (τ.app Y))
                                    (CategoryTheory.Functor.LaxMonoidal.μ F₂ X Y)) →
                            motive ⋯) →
                        (t : CategoryTheory.NatTrans.IsMonoidal τ) → motive t