∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.Functor D ((i : I) → C i)} [inst_4 : F.LaxMonoidal] [inst_5 : G.LaxMonoidal]
  (τ : (i : I) → F.comp (CategoryTheory.Pi.eval C i) ⟶ G.comp (CategoryTheory.Pi.eval C i))
  [∀ (i : I), CategoryTheory.NatTrans.IsMonoidal (τ i)],
  CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.NatTrans.pi' τ)