-- 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))
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
have refine_1 : Eq.{u + 1} (α :=
  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)) :
        (a : (↑(F ⋙ forget SemiRingCat).sections : Type (max u v))) →
          Shrink.{u, max u v} (↑(F ⋙ forget SemiRingCat).sections : Type (max u v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (F.obj j)) ↦
        x ∈
          (F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦ 1) sorry) :
    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)))
  (1 :
    (Types.Small.limitCone
        (F ⋙
          forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))).pt)
Tactic: simp