[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
j : J
⊢ Semiring ((F ⋙ forget SemiRingCat).obj j)
[PROOFSTEP]
change Semiring (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
j : J
⊢ Semiring ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
⊢ IsLimit (limitCone F)
[PROOFSTEP]
refine
  IsLimit.ofFaithful (forget SemiRingCatMax.{v, u}) (Types.limitConeIsLimit.{v, u} _)
    (fun s : Cone F =>
      ofHom
        ⟨⟨⟨_, Subtype.ext <| funext fun j => by exact (s.π.app j).map_one⟩, fun x y =>
            Subtype.ext <| funext fun j => by exact (s.π.app j).map_mul x y⟩,
          Subtype.ext <| funext fun j => by exact (s.π.app j).map_zero, fun x y =>
          Subtype.ext <| funext fun j => by exact (s.π.app j).map_add x y⟩)
    fun s => rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
s : Cone F
j : J
⊢ ↑{ val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
          property :=
            (_ :
              ∀ {j j' : J} (f : j ⟶ j'),
                (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f) 1 =
                  NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) }
      j =
    ↑1 j
[PROOFSTEP]
exact (s.π.app j).map_one
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
s : Cone F
x y : ↑s.1
j : J
⊢ ↑(OneHom.toFun
          {
            toFun := fun v =>
              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                property :=
                  (_ :
                    ∀ {j j' : J} (f : j ⟶ j'),
                      (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f) v =
                        NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
            map_one' :=
              (_ :
                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                    property :=
                      (_ :
                        ∀ {j j' : J} (f : j ⟶ j'),
                          (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f) 1 =
                            NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                  1) }
          (x * y))
      j =
    ↑(OneHom.toFun
            {
              toFun := fun v =>
                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                  property :=
                    (_ :
                      ∀ {j j' : J} (f : j ⟶ j'),
                        (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f) v =
                          NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
              map_one' :=
                (_ :
                  { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                      property :=
                        (_ :
                          ∀ {j j' : J} (f : j ⟶ j'),
                            (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f)
                                1 =
                              NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                    1) }
            x *
          OneHom.toFun
            {
              toFun := fun v =>
                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                  property :=
                    (_ :
                      ∀ {j j' : J} (f : j ⟶ j'),
                        (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f) v =
                          NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
              map_one' :=
                (_ :
                  { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                      property :=
                        (_ :
                          ∀ {j j' : J} (f : j ⟶ j'),
                            (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f)
                                1 =
                              NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                    1) }
            y)
      j
[PROOFSTEP]
exact (s.π.app j).map_mul x y
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
s : Cone F
j : J
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun v =>
                    { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                      property :=
                        (_ :
                          ∀ {j j' : J} (f : j ⟶ j'),
                            (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f)
                                v =
                              NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                  map_one' :=
                    (_ :
                      { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                      (F ⋙ forget SemiRingCatMax).map f)
                                    1 =
                                  NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑s.1),
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                          (F ⋙ forget SemiRingCatMax).map f)
                                        v =
                                      NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                          map_one' :=
                            (_ :
                              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                              (F ⋙ forget SemiRingCatMax).map f)
                                            1 =
                                          NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                            (F ⋙ forget SemiRingCatMax).map f)
                                          v =
                                        NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                            map_one' :=
                              (_ :
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                (F ⋙ forget SemiRingCatMax).map f)
                                              1 =
                                            NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                            (F ⋙ forget SemiRingCatMax).map f)
                                          v =
                                        NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                            map_one' :=
                              (_ :
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                (F ⋙ forget SemiRingCatMax).map f)
                                              1 =
                                            NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                  1) }
                          y) })
          0)
      j =
    ↑0 j
[PROOFSTEP]
exact (s.π.app j).map_zero
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
s : Cone F
x y : ↑s.1
j : J
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun v =>
                    { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                      property :=
                        (_ :
                          ∀ {j j' : J} (f : j ⟶ j'),
                            (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f)
                                v =
                              NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                  map_one' :=
                    (_ :
                      { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                      (F ⋙ forget SemiRingCatMax).map f)
                                    1 =
                                  NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑s.1),
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                          (F ⋙ forget SemiRingCatMax).map f)
                                        v =
                                      NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                          map_one' :=
                            (_ :
                              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                              (F ⋙ forget SemiRingCatMax).map f)
                                            1 =
                                          NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                            (F ⋙ forget SemiRingCatMax).map f)
                                          v =
                                        NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                            map_one' :=
                              (_ :
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                (F ⋙ forget SemiRingCatMax).map f)
                                              1 =
                                            NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                            (F ⋙ forget SemiRingCatMax).map f)
                                          v =
                                        NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                            map_one' :=
                              (_ :
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                (F ⋙ forget SemiRingCatMax).map f)
                                              1 =
                                            NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                  1) }
                          y) })
          (x + y))
      j =
    ↑(OneHom.toFun
            (↑{
                toOneHom :=
                  {
                    toFun := fun v =>
                      { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'),
                              (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f)
                                  v =
                                NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                    map_one' :=
                      (_ :
                        { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                        (F ⋙ forget SemiRingCatMax).map f)
                                      1 =
                                    NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : ↑s.1),
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                            (F ⋙ forget SemiRingCatMax).map f)
                                          v =
                                        NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                            map_one' :=
                              (_ :
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                (F ⋙ forget SemiRingCatMax).map f)
                                              1 =
                                            NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                  1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                              (F ⋙ forget SemiRingCatMax).map f)
                                            v =
                                          NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                              map_one' :=
                                (_ :
                                  { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                  (F ⋙ forget SemiRingCatMax).map f)
                                                1 =
                                              NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                    1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                              (F ⋙ forget SemiRingCatMax).map f)
                                            v =
                                          NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                              map_one' :=
                                (_ :
                                  { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                  (F ⋙ forget SemiRingCatMax).map f)
                                                1 =
                                              NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                    1) }
                            y) })
            x +
          OneHom.toFun
            (↑{
                toOneHom :=
                  {
                    toFun := fun v =>
                      { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'),
                              (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫ (F ⋙ forget SemiRingCatMax).map f)
                                  v =
                                NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                    map_one' :=
                      (_ :
                        { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                        (F ⋙ forget SemiRingCatMax).map f)
                                      1 =
                                    NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : ↑s.1),
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                            (F ⋙ forget SemiRingCatMax).map f)
                                          v =
                                        NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                            map_one' :=
                              (_ :
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                (F ⋙ forget SemiRingCatMax).map f)
                                              1 =
                                            NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                  1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                              (F ⋙ forget SemiRingCatMax).map f)
                                            v =
                                          NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                              map_one' :=
                                (_ :
                                  { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                  (F ⋙ forget SemiRingCatMax).map f)
                                                1 =
                                              NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                    1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun v =>
                                { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                              (F ⋙ forget SemiRingCatMax).map f)
                                            v =
                                          NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' v) },
                              map_one' :=
                                (_ :
                                  { val := fun j => NatTrans.app ((forget SemiRingCatMax).mapCone s).π j 1,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            (NatTrans.app ((forget SemiRingCatMax).mapCone s).π j ≫
                                                  (F ⋙ forget SemiRingCatMax).map f)
                                                1 =
                                              NatTrans.app ((forget SemiRingCatMax).mapCone s).π j' 1) } =
                                    1) }
                            y) })
            y)
      j
[PROOFSTEP]
exact (s.π.app j).map_add x y
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
⊢ IsLimit ((forget₂ SemiRingCat AddCommMonCat).mapCone (limitCone F))
[PROOFSTEP]
apply AddCommMonCat.limitConeIsLimit.{v, u}
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
⊢ IsLimit ((forget₂ SemiRingCat MonCat).mapCone (limitCone F))
[PROOFSTEP]
apply MonCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ SemiRingCat MonCat.{max v u})
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommSemiRingCatMax
j : J
⊢ CommSemiring ((F ⋙ forget CommSemiRingCat).obj j)
[PROOFSTEP]
change CommSemiring (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommSemiRingCatMax
j : J
⊢ CommSemiring ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommSemiRingCatMax
this✝ : ReflectsIsomorphisms (forget CommSemiRingCatMax) := forgetReflectIsos
this : ReflectsIsomorphisms (forget₂ CommSemiRingCatMax SemiRingCatMax) :=
  reflectsIsomorphisms_forget₂ CommSemiRingCatMax SemiRingCatMax
c : Cone F :=
  { pt := of (Types.limitCone (F ⋙ forget CommSemiRingCatMax)).pt,
    π := NatTrans.mk fun j => ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) j) }
c' : Cone (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax)
t : IsLimit c'
⊢ IsLimit
    { liftedCone := c,
        validLift :=
          IsLimit.uniqueUpToIso (SemiRingCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax))
            t }.liftedCone
[PROOFSTEP]
refine
  IsLimit.ofFaithful (forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u})
    (SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _)
    (fun s : Cone F =>
      CommSemiRingCat.ofHom
        ⟨⟨⟨_, Subtype.ext <| funext fun j => by exact (s.π.app j).map_one⟩, fun x y =>
            Subtype.ext <| funext fun j => by exact (s.π.app j).map_mul x y⟩,
          Subtype.ext <| funext fun j => by exact (s.π.app j).map_zero, fun x y =>
          Subtype.ext <| funext fun j => by exact (s.π.app j).map_add x y⟩)
    fun s => rfl
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommSemiRingCatMax
this✝ : ReflectsIsomorphisms (forget CommSemiRingCatMax) := forgetReflectIsos
this : ReflectsIsomorphisms (forget₂ CommSemiRingCatMax SemiRingCatMax) :=
  reflectsIsomorphisms_forget₂ CommSemiRingCatMax SemiRingCatMax
c : Cone F :=
  { pt := of (Types.limitCone (F ⋙ forget CommSemiRingCatMax)).pt,
    π := NatTrans.mk fun j => ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) j) }
c' : Cone (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax)
t : IsLimit c'
s : Cone F
j : J
⊢ ↑{
          val := fun j =>
            NatTrans.app ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j
              1,
          property :=
            (_ :
              ∀ {j j' : J} (f : j ⟶ j'),
                (NatTrans.app
                        ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j ≫
                      ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                    1 =
                  NatTrans.app
                    ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j' 1) }
      j =
    ↑1 j
[PROOFSTEP]
exact (s.π.app j).map_one
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommSemiRingCatMax
this✝ : ReflectsIsomorphisms (forget CommSemiRingCatMax) := forgetReflectIsos
this : ReflectsIsomorphisms (forget₂ CommSemiRingCatMax SemiRingCatMax) :=
  reflectsIsomorphisms_forget₂ CommSemiRingCatMax SemiRingCatMax
c : Cone F :=
  { pt := of (Types.limitCone (F ⋙ forget CommSemiRingCatMax)).pt,
    π := NatTrans.mk fun j => ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) j) }
c' : Cone (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax)
t : IsLimit c'
s : Cone F
x y : ↑s.1
j : J
⊢ ↑(OneHom.toFun
          {
            toFun := fun v =>
              {
                val := fun j =>
                  NatTrans.app
                    ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j v,
                property :=
                  (_ :
                    ∀ {j j' : J} (f : j ⟶ j'),
                      (NatTrans.app
                              ((forget SemiRingCatMax).mapCone
                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                              j ≫
                            ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                          v =
                        NatTrans.app
                          ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j'
                          v) },
            map_one' :=
              (_ :
                {
                    val := fun j =>
                      NatTrans.app
                        ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j 1,
                    property :=
                      (_ :
                        ∀ {j j' : J} (f : j ⟶ j'),
                          (NatTrans.app
                                  ((forget SemiRingCatMax).mapCone
                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                  j ≫
                                ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                              1 =
                            NatTrans.app
                              ((forget SemiRingCatMax).mapCone
                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                              j' 1) } =
                  1) }
          (x * y))
      j =
    ↑(OneHom.toFun
            {
              toFun := fun v =>
                {
                  val := fun j =>
                    NatTrans.app
                      ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j v,
                  property :=
                    (_ :
                      ∀ {j j' : J} (f : j ⟶ j'),
                        (NatTrans.app
                                ((forget SemiRingCatMax).mapCone
                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                j ≫
                              ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                            v =
                          NatTrans.app
                            ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                            j' v) },
              map_one' :=
                (_ :
                  {
                      val := fun j =>
                        NatTrans.app
                          ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j
                          1,
                      property :=
                        (_ :
                          ∀ {j j' : J} (f : j ⟶ j'),
                            (NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j ≫
                                  ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                1 =
                              NatTrans.app
                                ((forget SemiRingCatMax).mapCone
                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                j' 1) } =
                    1) }
            x *
          OneHom.toFun
            {
              toFun := fun v =>
                {
                  val := fun j =>
                    NatTrans.app
                      ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j v,
                  property :=
                    (_ :
                      ∀ {j j' : J} (f : j ⟶ j'),
                        (NatTrans.app
                                ((forget SemiRingCatMax).mapCone
                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                j ≫
                              ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                            v =
                          NatTrans.app
                            ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                            j' v) },
              map_one' :=
                (_ :
                  {
                      val := fun j =>
                        NatTrans.app
                          ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j
                          1,
                      property :=
                        (_ :
                          ∀ {j j' : J} (f : j ⟶ j'),
                            (NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j ≫
                                  ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                1 =
                              NatTrans.app
                                ((forget SemiRingCatMax).mapCone
                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                j' 1) } =
                    1) }
            y)
      j
[PROOFSTEP]
exact (s.π.app j).map_mul x y
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommSemiRingCatMax
this✝ : ReflectsIsomorphisms (forget CommSemiRingCatMax) := forgetReflectIsos
this : ReflectsIsomorphisms (forget₂ CommSemiRingCatMax SemiRingCatMax) :=
  reflectsIsomorphisms_forget₂ CommSemiRingCatMax SemiRingCatMax
c : Cone F :=
  { pt := of (Types.limitCone (F ⋙ forget CommSemiRingCatMax)).pt,
    π := NatTrans.mk fun j => ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) j) }
c' : Cone (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax)
t : IsLimit c'
s : Cone F
j : J
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun v =>
                    {
                      val := fun j =>
                        NatTrans.app
                          ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j
                          v,
                      property :=
                        (_ :
                          ∀ {j j' : J} (f : j ⟶ j'),
                            (NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j ≫
                                  ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                v =
                              NatTrans.app
                                ((forget SemiRingCatMax).mapCone
                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                j' v) },
                  map_one' :=
                    (_ :
                      {
                          val := fun j =>
                            NatTrans.app
                              ((forget SemiRingCatMax).mapCone
                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                              j 1,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                (NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j ≫
                                      ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                    1 =
                                  NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j' 1) } =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑s.1),
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            {
                              val := fun j =>
                                NatTrans.app
                                  ((forget SemiRingCatMax).mapCone
                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                  j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    (NatTrans.app
                                            ((forget SemiRingCatMax).mapCone
                                                ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                            j ≫
                                          ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map
                                            f)
                                        v =
                                      NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j' v) },
                          map_one' :=
                            (_ :
                              {
                                  val := fun j =>
                                    NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j 1,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j ≫
                                              ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                    forget SemiRingCatMax).map
                                                f)
                                            1 =
                                          NatTrans.app
                                            ((forget SemiRingCatMax).mapCone
                                                ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                            j' 1) } =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              {
                                val := fun j =>
                                  NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j ≫
                                            ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                  forget SemiRingCatMax).map
                                              f)
                                          v =
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j' v) },
                            map_one' :=
                              (_ :
                                {
                                    val := fun j =>
                                      NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app
                                                  ((forget SemiRingCatMax).mapCone
                                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                  j ≫
                                                ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                      forget SemiRingCatMax).map
                                                  f)
                                              1 =
                                            NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j' 1) } =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun v =>
                              {
                                val := fun j =>
                                  NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j ≫
                                            ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                  forget SemiRingCatMax).map
                                              f)
                                          v =
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j' v) },
                            map_one' :=
                              (_ :
                                {
                                    val := fun j =>
                                      NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app
                                                  ((forget SemiRingCatMax).mapCone
                                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                  j ≫
                                                ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                      forget SemiRingCatMax).map
                                                  f)
                                              1 =
                                            NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j' 1) } =
                                  1) }
                          y) })
          0)
      j =
    ↑0 j
[PROOFSTEP]
exact (s.π.app j).map_zero
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommSemiRingCatMax
this✝ : ReflectsIsomorphisms (forget CommSemiRingCatMax) := forgetReflectIsos
this : ReflectsIsomorphisms (forget₂ CommSemiRingCatMax SemiRingCatMax) :=
  reflectsIsomorphisms_forget₂ CommSemiRingCatMax SemiRingCatMax
c : Cone F :=
  { pt := of (Types.limitCone (F ⋙ forget CommSemiRingCatMax)).pt,
    π := NatTrans.mk fun j => ofHom (SemiRingCat.limitπRingHom (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) j) }
c' : Cone (F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax)
t : IsLimit c'
s : Cone F
x y : ↑s.1
j : J
⊢ ↑(OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun v =>
                    {
                      val := fun j =>
                        NatTrans.app
                          ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π j
                          v,
                      property :=
                        (_ :
                          ∀ {j j' : J} (f : j ⟶ j'),
                            (NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j ≫
                                  ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                v =
                              NatTrans.app
                                ((forget SemiRingCatMax).mapCone
                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                j' v) },
                  map_one' :=
                    (_ :
                      {
                          val := fun j =>
                            NatTrans.app
                              ((forget SemiRingCatMax).mapCone
                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                              j 1,
                          property :=
                            (_ :
                              ∀ {j j' : J} (f : j ⟶ j'),
                                (NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j ≫
                                      ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                    1 =
                                  NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j' 1) } =
                        1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ↑s.1),
                    OneHom.toFun
                        {
                          toFun := fun v =>
                            {
                              val := fun j =>
                                NatTrans.app
                                  ((forget SemiRingCatMax).mapCone
                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                  j v,
                              property :=
                                (_ :
                                  ∀ {j j' : J} (f : j ⟶ j'),
                                    (NatTrans.app
                                            ((forget SemiRingCatMax).mapCone
                                                ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                            j ≫
                                          ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map
                                            f)
                                        v =
                                      NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j' v) },
                          map_one' :=
                            (_ :
                              {
                                  val := fun j =>
                                    NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j 1,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j ≫
                                              ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                    forget SemiRingCatMax).map
                                                f)
                                            1 =
                                          NatTrans.app
                                            ((forget SemiRingCatMax).mapCone
                                                ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                            j' 1) } =
                                1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              {
                                val := fun j =>
                                  NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j ≫
                                            ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                  forget SemiRingCatMax).map
                                              f)
                                          v =
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j' v) },
                            map_one' :=
                              (_ :
                                {
                                    val := fun j =>
                                      NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app
                                                  ((forget SemiRingCatMax).mapCone
                                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                  j ≫
                                                ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                      forget SemiRingCatMax).map
                                                  f)
                                              1 =
                                            NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j' 1) } =
                                  1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun v =>
                              {
                                val := fun j =>
                                  NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j ≫
                                            ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                  forget SemiRingCatMax).map
                                              f)
                                          v =
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j' v) },
                            map_one' :=
                              (_ :
                                {
                                    val := fun j =>
                                      NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app
                                                  ((forget SemiRingCatMax).mapCone
                                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                  j ≫
                                                ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                      forget SemiRingCatMax).map
                                                  f)
                                              1 =
                                            NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j' 1) } =
                                  1) }
                          y) })
          (x + y))
      j =
    ↑(OneHom.toFun
            (↑{
                toOneHom :=
                  {
                    toFun := fun v =>
                      {
                        val := fun j =>
                          NatTrans.app
                            ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                            j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'),
                              (NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j ≫
                                    ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                  v =
                                NatTrans.app
                                  ((forget SemiRingCatMax).mapCone
                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                  j' v) },
                    map_one' :=
                      (_ :
                        {
                            val := fun j =>
                              NatTrans.app
                                ((forget SemiRingCatMax).mapCone
                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                j 1,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  (NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j ≫
                                        ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                      1 =
                                    NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j' 1) } =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : ↑s.1),
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              {
                                val := fun j =>
                                  NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j ≫
                                            ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                  forget SemiRingCatMax).map
                                              f)
                                          v =
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j' v) },
                            map_one' :=
                              (_ :
                                {
                                    val := fun j =>
                                      NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app
                                                  ((forget SemiRingCatMax).mapCone
                                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                  j ≫
                                                ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                      forget SemiRingCatMax).map
                                                  f)
                                              1 =
                                            NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j' 1) } =
                                  1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun v =>
                                {
                                  val := fun j =>
                                    NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j ≫
                                              ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                    forget SemiRingCatMax).map
                                                f)
                                            v =
                                          NatTrans.app
                                            ((forget SemiRingCatMax).mapCone
                                                ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                            j' v) },
                              map_one' :=
                                (_ :
                                  {
                                      val := fun j =>
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j 1,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            (NatTrans.app
                                                    ((forget SemiRingCatMax).mapCone
                                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                    j ≫
                                                  ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                        forget SemiRingCatMax).map
                                                    f)
                                                1 =
                                              NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j' 1) } =
                                    1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun v =>
                                {
                                  val := fun j =>
                                    NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j ≫
                                              ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                    forget SemiRingCatMax).map
                                                f)
                                            v =
                                          NatTrans.app
                                            ((forget SemiRingCatMax).mapCone
                                                ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                            j' v) },
                              map_one' :=
                                (_ :
                                  {
                                      val := fun j =>
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j 1,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            (NatTrans.app
                                                    ((forget SemiRingCatMax).mapCone
                                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                    j ≫
                                                  ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                        forget SemiRingCatMax).map
                                                    f)
                                                1 =
                                              NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j' 1) } =
                                    1) }
                            y) })
            x +
          OneHom.toFun
            (↑{
                toOneHom :=
                  {
                    toFun := fun v =>
                      {
                        val := fun j =>
                          NatTrans.app
                            ((forget SemiRingCatMax).mapCone ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                            j v,
                        property :=
                          (_ :
                            ∀ {j j' : J} (f : j ⟶ j'),
                              (NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j ≫
                                    ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                  v =
                                NatTrans.app
                                  ((forget SemiRingCatMax).mapCone
                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                  j' v) },
                    map_one' :=
                      (_ :
                        {
                            val := fun j =>
                              NatTrans.app
                                ((forget SemiRingCatMax).mapCone
                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                j 1,
                            property :=
                              (_ :
                                ∀ {j j' : J} (f : j ⟶ j'),
                                  (NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j ≫
                                        ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙ forget SemiRingCatMax).map f)
                                      1 =
                                    NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j' 1) } =
                          1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : ↑s.1),
                      OneHom.toFun
                          {
                            toFun := fun v =>
                              {
                                val := fun j =>
                                  NatTrans.app
                                    ((forget SemiRingCatMax).mapCone
                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                    j v,
                                property :=
                                  (_ :
                                    ∀ {j j' : J} (f : j ⟶ j'),
                                      (NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j ≫
                                            ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                  forget SemiRingCatMax).map
                                              f)
                                          v =
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j' v) },
                            map_one' :=
                              (_ :
                                {
                                    val := fun j =>
                                      NatTrans.app
                                        ((forget SemiRingCatMax).mapCone
                                            ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                        j 1,
                                    property :=
                                      (_ :
                                        ∀ {j j' : J} (f : j ⟶ j'),
                                          (NatTrans.app
                                                  ((forget SemiRingCatMax).mapCone
                                                      ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                  j ≫
                                                ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                      forget SemiRingCatMax).map
                                                  f)
                                              1 =
                                            NatTrans.app
                                              ((forget SemiRingCatMax).mapCone
                                                  ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                              j' 1) } =
                                  1) }
                          (x * y) =
                        OneHom.toFun
                            {
                              toFun := fun v =>
                                {
                                  val := fun j =>
                                    NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j ≫
                                              ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                    forget SemiRingCatMax).map
                                                f)
                                            v =
                                          NatTrans.app
                                            ((forget SemiRingCatMax).mapCone
                                                ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                            j' v) },
                              map_one' :=
                                (_ :
                                  {
                                      val := fun j =>
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j 1,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            (NatTrans.app
                                                    ((forget SemiRingCatMax).mapCone
                                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                    j ≫
                                                  ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                        forget SemiRingCatMax).map
                                                    f)
                                                1 =
                                              NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j' 1) } =
                                    1) }
                            x *
                          OneHom.toFun
                            {
                              toFun := fun v =>
                                {
                                  val := fun j =>
                                    NatTrans.app
                                      ((forget SemiRingCatMax).mapCone
                                          ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                      j v,
                                  property :=
                                    (_ :
                                      ∀ {j j' : J} (f : j ⟶ j'),
                                        (NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j ≫
                                              ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                    forget SemiRingCatMax).map
                                                f)
                                            v =
                                          NatTrans.app
                                            ((forget SemiRingCatMax).mapCone
                                                ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                            j' v) },
                              map_one' :=
                                (_ :
                                  {
                                      val := fun j =>
                                        NatTrans.app
                                          ((forget SemiRingCatMax).mapCone
                                              ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                          j 1,
                                      property :=
                                        (_ :
                                          ∀ {j j' : J} (f : j ⟶ j'),
                                            (NatTrans.app
                                                    ((forget SemiRingCatMax).mapCone
                                                        ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                    j ≫
                                                  ((F ⋙ forget₂ CommSemiRingCatMax SemiRingCatMax) ⋙
                                                        forget SemiRingCatMax).map
                                                    f)
                                                1 =
                                              NatTrans.app
                                                ((forget SemiRingCatMax).mapCone
                                                    ((forget₂ CommSemiRingCatMax SemiRingCatMax).mapCone s)).π
                                                j' 1) } =
                                    1) }
                            y) })
            y)
      j
[PROOFSTEP]
exact (s.π.app j).map_add x y
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCatMax
j : J
⊢ Ring ((F ⋙ forget RingCat).obj j)
[PROOFSTEP]
change Ring (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCatMax
j : J
⊢ Ring ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCatMax
this : ReflectsIsomorphisms (forget₂ RingCatMax SemiRingCatMax) :=
  reflectsIsomorphisms_forget₂ RingCatMax SemiRingCatMax
c : Cone F :=
  { pt := of (Types.limitCone (F ⋙ forget RingCatMax)).pt,
    π :=
      NatTrans.mk fun x =>
        SemiRingCat.ofHom (NatTrans.app (SemiRingCat.HasLimits.limitCone (F ⋙ forget₂ RingCat SemiRingCat)).π x) }
c' : Cone (F ⋙ forget₂ RingCatMax SemiRingCatMax)
t : IsLimit c'
⊢ (forget₂ RingCatMax SemiRingCatMax).mapCone c ≅ c'
[PROOFSTEP]
apply IsLimit.uniqueUpToIso (SemiRingCat.HasLimits.limitConeIsLimit _) t
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCatMax
this : ReflectsIsomorphisms (forget₂ RingCatMax SemiRingCatMax) :=
  reflectsIsomorphisms_forget₂ RingCatMax SemiRingCatMax
c : Cone F :=
  { pt := of (Types.limitCone (F ⋙ forget RingCatMax)).pt,
    π :=
      NatTrans.mk fun x =>
        SemiRingCat.ofHom (NatTrans.app (SemiRingCat.HasLimits.limitCone (F ⋙ forget₂ RingCat SemiRingCat)).π x) }
c' : Cone (F ⋙ forget₂ RingCatMax SemiRingCatMax)
t : IsLimit c'
⊢ IsLimit
    ((forget₂ RingCat SemiRingCat).mapCone
      { liftedCone := c,
          validLift :=
            IsLimit.uniqueUpToIso (SemiRingCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ RingCatMax SemiRingCatMax))
              t }.liftedCone)
[PROOFSTEP]
apply SemiRingCat.HasLimits.limitConeIsLimit _
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCatMax
⊢ IsLimit ((forget₂ RingCatMax AddCommGroupCat).mapCone (limitCone F))
[PROOFSTEP]
letI f := (F ⋙ forget₂ RingCatMax.{v, u} AddCommGroupCat.{max v u})
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCatMax
f : J ⥤ AddCommGroupCat := F ⋙ forget₂ RingCatMax AddCommGroupCat
⊢ IsLimit ((forget₂ RingCatMax AddCommGroupCat).mapCone (limitCone F))
[PROOFSTEP]
apply AddCommGroupCat.limitConeIsLimit.{v, u} f
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCatMax
j : J
⊢ CommRing ((F ⋙ forget CommRingCat).obj j)
[PROOFSTEP]
change CommRing (F.obj j)
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCatMax
j : J
⊢ CommRing ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCatMax
⊢ IsLimit ((forget₂ CommRingCat CommSemiRingCat).mapCone (limitCone F))
[PROOFSTEP]
apply CommSemiRingCat.limitConeIsLimit (F ⋙ forget₂ CommRingCat CommSemiRingCat.{max v u})