-- 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))
⊢ ∀ (s : Cone F),
    Eq (α :=
      Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
          s.pt ⟶
        Functor.obj (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
          (LiftableCone.liftedCone (D := Type u) (F :=
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) (c :=
              c)
              {
                liftedCone :=
                  {
                    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 },
                validLift :=
                  Cone.ext
                    (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))))))
                    ⋯ :
                LiftableCone F
                  (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
                  c }).pt)
      (CategoryTheory.Functor.map
        (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
        (ofHom
          {
            toFun :=
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                    (IsLimit.lift
                      (Types.Small.limitConeIsLimit
                        (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))
                        s))) :
                (a : (fun (X : Type u) ↦ X) ((forget MonCat).mapCone s).pt) →
                  (fun (X : Type u) ↦ X) (Types.Small.limitCone (F ⋙ forget MonCat)).pt),
            map_one' := ⋯, map_mul' := ⋯ }))
      (IsLimit.lift
        (Types.Small.limitConeIsLimit
          (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)) s))

Tactic:
exact fun _ ↦ rfl

Premises used: rfl