-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
refine_1 :
  ∀ (s : Cone F),
    EquivLike.coe (E :=
        (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)) ≃
          Shrink.{u, max u v}
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))
        (equivShrink
          (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                (F ⋙
                      forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier)).obj
                  j) ↦
          x ∈
            (F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections)
          (fun (j : J) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app
                    (Cone.π
                      (Functor.mapCone
                        (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier))
                        s))
                    j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
              1)
          ⋯) =
      1
refine_2 :
  ∀ (s : Cone F) (x y : (↑s.1 : Type u)),
    EquivLike.coe (E :=
        (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)) ≃
          Shrink.{u, max u v}
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))
        (equivShrink
          (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                (F ⋙
                      forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier)).obj
                  j) ↦
          x ∈
            (F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections)
          (fun (j : J) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app
                    (Cone.π
                      (Functor.mapCone
                        (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier))
                        s))
                    j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
              (x * y))
          ⋯) =
      EquivLike.coe (E :=
          (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)) ≃
            Shrink.{u, max u v}
              (↑(F ⋙
                      forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier)).sections :
                Type (max u v)))
          (equivShrink
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))
          (Subtype.mk (p :=
            fun
              (x :
                (j : J) →
                  (F ⋙
                        forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier)).obj
                    j) ↦
            x ∈
              (F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections)
            (fun (j : J) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app
                      (Cone.π
                        (Functor.mapCone
                          (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := carrier))
                          s))
                      j) :
                  (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                    (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
                x)
            ⋯) *
        EquivLike.coe (E :=
          (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)) ≃
            Shrink.{u, max u v}
              (↑(F ⋙
                      forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier)).sections :
                Type (max u v)))
          (equivShrink
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))
          (Subtype.mk (p :=
            fun
              (x :
                (j : J) →
                  (F ⋙
                        forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier)).obj
                    j) ↦
            x ∈
              (F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections)
            (fun (j : J) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app
                      (Cone.π
                        (Functor.mapCone
                          (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := carrier))
                          s))
                      j) :
                  (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                    (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
                y)
            ⋯)
refine_3 :
  ∀ (s : Cone F),
    EquivLike.coe (E :=
        (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)) ≃
          Shrink.{u, max u v}
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))
        (equivShrink
          (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                (F ⋙
                      forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier)).obj
                  j) ↦
          x ∈
            (F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections)
          (fun (j : J) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app
                    (Cone.π
                      (Functor.mapCone
                        (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier))
                        s))
                    j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
              0)
          ⋯) =
      0
⊢ IsLimit (limitCone F)
have refine_4 : ∀ (s : Cone F) (x y : (↑s.1 : Type u)),
  EquivLike.coe (E :=
      (↑(F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections :
          Type (max u v)) ≃
        Shrink.{u, max u v}
          (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)))
      (equivShrink
        (↑(F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections :
          Type (max u v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              (F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).obj
                j) ↦
        x ∈
          (F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cone.π
                    (Functor.mapCone
                      (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier))
                      s))
                  j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
            (x + y))
        sorry) =
    EquivLike.coe (E :=
        (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)) ≃
          Shrink.{u, max u v}
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))
        (equivShrink
          (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                (F ⋙
                      forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier)).obj
                  j) ↦
          x ∈
            (F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections)
          (fun (j : J) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app
                    (Cone.π
                      (Functor.mapCone
                        (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier))
                        s))
                    j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
              x)
          sorry) +
      EquivLike.coe (E :=
        (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)) ≃
          Shrink.{u, max u v}
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))
        (equivShrink
          (↑(F ⋙
                  forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    carrier)).sections :
            Type (max u v)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                (F ⋙
                      forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier)).obj
                  j) ↦
          x ∈
            (F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections)
          (fun (j : J) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app
                    (Cone.π
                      (Functor.mapCone
                        (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier))
                        s))
                    j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget SemiRingCat).mapCone s).pt).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget SemiRingCat).obj j))
              y)
          sorry)
Tactic: refine IsLimit.ofFaithful (forget SemiRingCat.{u}) (Types.Small.limitConeIsLimit.{v, u} _)
    (fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_ })
    (fun s => rfl)