-- 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
⊢ 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)))
                    ⋯)) :
              (a : (Types.coneOfSection ⋯).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))
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 _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (Cone.π
                (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))
              x) :
          TypeCat.Fun
            (Cone.pt.{w, u, v, u + 1} (J := J) (F :=
              F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
              (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))
            (ToType (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.obj x))) :
        (a : (Types.coneOfSection sorry).pt) → ToType (F.obj x))
      PUnit.unit :
    ToType (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.obj x))
Tactic: simp [← CategoryTheory.comp_apply]