∀ {J : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} J] (F : CategoryTheory.Functor J CommRingCat)
  [inst_1 : Small.{u_3, max u_3 u_2} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections]
  (this :
    Small.{u_3, max u_3 u_2}
      ↑((F.comp ((CategoryTheory.forget₂ CommRingCat RingCat).comp (CategoryTheory.forget₂ RingCat SemiRingCat))).comp
            (CategoryTheory.forget SemiRingCat)).sections)
  (x x_1 : J) (f : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const J).obj
            { carrier := (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommRingCat))).pt,
              commRing := CommRingCat.limitCommRing F }).map
        f)
      (CommRingCat.ofHom
        (SemiRingCat.limitπRingHom
          (F.comp ((CategoryTheory.forget₂ CommRingCat RingCat).comp (CategoryTheory.forget₂ RingCat SemiRingCat)))
          x_1)) =
    CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom
        (SemiRingCat.limitπRingHom
          (F.comp ((CategoryTheory.forget₂ CommRingCat RingCat).comp (CategoryTheory.forget₂ RingCat SemiRingCat))) x))
      (F.map f)