∀ {J : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J CommSemiRingCat)
  (s : CategoryTheory.Limits.Cone F) (x y : ↑((CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).mapCone s).1)
  {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.forget SemiRingCat).mapCone
              ((CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).mapCone s)).π.app
        j)
      (((F.comp (CategoryTheory.forget₂ CommSemiRingCat SemiRingCat)).comp (CategoryTheory.forget SemiRingCat)).map f)
      (x * y) =
    ((CategoryTheory.forget SemiRingCat).mapCone ((CategoryTheory.forget₂ CommSemiRingCat SemiRingCat).mapCone s)).π.app
      j' (x * y)