∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F X : CategoryTheory.Functor C V)
  (a :
    (CategoryTheory.coyoneda.obj
          (Opposite.op
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V), F).2)).obj
      X)
  (X_1 : CategoryTheory.Discrete PUnit.{1} × C),
  ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso F).inv.app X a).app X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X_1.2)).hom
      (CategoryTheory.CategoryStruct.comp (a.app X_1.2)
        (CategoryTheory.CategoryStruct.comp (X.map ((CategoryTheory.prod.leftUnitorEquivalence C).unit.app X_1).2)
          (CategoryTheory.CategoryStruct.comp (X.map ((CategoryTheory.prod.leftUnitorEquivalence C).unitInv.app X_1).2)
            (X.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X_1.2).inv))))