-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
t : IsLimit c
this :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
x : J
x_1 :
  Functor.obj.{w, u, v, u + 1}
    (Functor.obj (Functor.const J)
      (Cone.pt (F :=
        F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
        (Functor.mapCone
          (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
          {
            pt :=
              of
                (Types.Small.limitCone
                    (F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier))).pt,
            π :=
              { app := fun (j : J) ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ :
                NatTrans
                  (Functor.obj (Functor.const J)
                    (of
                      (Types.Small.limitCone
                          (F ⋙
                            forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                              carrier))).pt))
                  F } :
            Cone F })))
    x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Cone.π
            (Functor.mapCone
              (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
              {
                pt :=
                  of
                    (Types.Small.limitCone
                        (F ⋙
                          forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                            carrier))).pt,
                π :=
                  { app := fun (j : J) ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ :
                    NatTrans
                      (Functor.obj (Functor.const J)
                        (of
                          (Types.Small.limitCone
                              (F ⋙
                                forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                                  carrier))).pt))
                      F } :
                Cone F }))
          x))
      x_1 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            (Equiv.toIso
              (Equiv.symm
                ((Types.isLimitEquivSections t).trans
                  (equivShrink
                    (↑(F ⋙
                            forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                              carrier)).sections :
                      Type (max u v)))))) ≫
          c.π.app x))
      x_1
have h : Eq (α := ToType (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.obj x))
  ((limitπMonoidHom F x :
        (a : Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v))) → (↑(F.obj x) : Type u))
      x_1 :
    (↑(F.obj x) : Type u))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app x) : (a : c.pt) → ToType (F.obj x))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (t.lift
                (Types.coneOfSection (s :=
                  (↑((Equiv.symm
                            (equivShrink
                              (↑(F ⋙
                                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                                        (CC := carrier)).sections :
                                Type (max u v))) :
                          (a : ToType (of (Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v))))) →
                            (↑(F ⋙ forget MonCat).sections : Type (max u v)))
                        x_1) :
                    (j : J) → ToType (F.obj j)))
                  sorry)) :
            (a : (Types.coneOfSection sorry).pt) → c.pt)
          PUnit.unit :
        c.pt) :
    ToType (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.obj x))
Tactic: simp [Types.isLimitEquivSections]