-- Module: Mathlib.Algebra.Category.MonCat.Limits
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
h :
  ∀
    (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
⊢ Eq (α :=
    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 ⟶
      (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).obj x)
    (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 } }))
      x)
    (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)

Tactic:
ext