∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] (X : C × CategoryTheory.Discrete PUnit.{u_2 + 1}),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.prod.rightUnitor C).map
        ((CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × CategoryTheory.Discrete PUnit.{u_2 + 1}))).hom.app X))
      ((CategoryTheory.Iso.refl
              ((CategoryTheory.prod.rightInverseUnitor C).comp (CategoryTheory.prod.rightUnitor C))).hom.app
        ((CategoryTheory.prod.rightUnitor C).obj X)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.prod.rightUnitor C).obj X)