-- 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))
j : J
x x_1 :
  (Types.Small.limitCone
      (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt
⊢ (↑(HMul.hMul (α :=
            (↑(F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      carrier)).sections :
              Type (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)))
            ((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 : Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v))) →
                    (↑(F ⋙ forget MonCat).sections : Type (max u v)))
                x :
              (↑(F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier)).sections :
                Type (max u v)))
            ((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 : Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v))) →
                    (↑(F ⋙ forget MonCat).sections : Type (max u v)))
                x_1 :
              (↑(F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier)).sections :
                Type (max u v)))) :
        (j : J) → ToType (F.obj j))
      j =
    HMul.hMul (α := (↑(F.obj j) : Type u))
      ((↑((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 : Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v))) →
                  (↑(F ⋙ forget MonCat).sections : Type (max u v)))
              x) :
          (j : J) → ToType (F.obj j))
        j)
      ((↑((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 : 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))
        j)

Tactic:
rfl