-- 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
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
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)))
                    ⋯)) :
              (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))
⊢ 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

Tactic:
simp [Types.isLimitEquivSections]

Premises used: CategoryTheory.Limits.Types.isLimitEquivSections