∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_6, u_2} C] (V : Type u_5)
  [inst_1 : CategoryTheory.Category.{u_3, u_5} V] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory V] (D : Type u_4) [inst_4 : CategoryTheory.Category.{u_1, u_4} D]
  [inst_5 : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D],
  (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).Faithful