∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J RingCat)
  [inst_1 : Small.{u_1, max u_1 u_3} ↑(F.comp (CategoryTheory.forget RingCat)).sections]
  (x : CategoryTheory.Limits.Cone F) (x_1 y : ↑((CategoryTheory.forget₂ RingCat SemiRingCat).mapCone x).1),
  EquivLike.coe
      (equivShrink
        ↑((F.comp (CategoryTheory.forget₂ RingCat SemiRingCat)).comp (CategoryTheory.forget SemiRingCat)).sections)
      ⟨fun j =>
        ((CategoryTheory.forget SemiRingCat).mapCone ((CategoryTheory.forget₂ RingCat SemiRingCat).mapCone x)).π.app j
          (x_1 + y),
        ⋯⟩ =
    EquivLike.coe
        (equivShrink
          ↑((F.comp (CategoryTheory.forget₂ RingCat SemiRingCat)).comp (CategoryTheory.forget SemiRingCat)).sections)
        ⟨fun j =>
          ((CategoryTheory.forget SemiRingCat).mapCone ((CategoryTheory.forget₂ RingCat SemiRingCat).mapCone x)).π.app j
            x_1,
          ⋯⟩ +
      EquivLike.coe
        (equivShrink
          ↑((F.comp (CategoryTheory.forget₂ RingCat SemiRingCat)).comp (CategoryTheory.forget SemiRingCat)).sections)
        ⟨fun j =>
          ((CategoryTheory.forget SemiRingCat).mapCone ((CategoryTheory.forget₂ RingCat SemiRingCat).mapCone x)).π.app j
            y,
          ⋯⟩