∀ {C : Type u_4} {D : Type u_2} [inst : CategoryTheory.Groupoid C] [inst_1 : CategoryTheory.Category.{u_1, u_2} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.LeftRigidCategory D]
  (F : CategoryTheory.Functor C D) (X Y : C) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C D)).map f)
      (η_
        ({ obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (CategoryTheory.inv f), map_id := ⋯,
              map_comp := ⋯ }.obj
          Y)
        (F.obj Y)) =
    CategoryTheory.CategoryStruct.comp
      (η_
        ({ obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (CategoryTheory.inv f), map_id := ⋯,
              map_comp := ⋯ }.obj
          X)
        (F.obj X))
      ((CategoryTheory.MonoidalCategoryStruct.tensorObj
            { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (CategoryTheory.inv f), map_id := ⋯,
              map_comp := ⋯ }
            F).map
        f)