-- 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))
h :
  (s : Cone F) →
    s.pt ⟶
      (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
h₁ :
  ∀ (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))
⊢ IsLimit
    (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 })

Tactic:
refine IsLimit.ofFaithful (forget MonCat.{u}) (Types.Small.limitConeIsLimit.{v, u} _) ?_ ?_