∀ {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 : (i : I) → CategoryTheory.Functor D (C i)) [inst_4 : (i : I) → (F i).Monoidal] (i : I),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Functor.pi' F) i = CategoryTheory.Functor.LaxMonoidal.ε (F i)