-- 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
h :
  ∀ (x y : (↑s.1 : Type u)),
    (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)
        (x * y) =
      HMul.hMul (α :=
        (Types.Small.limitCone
            (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
        (β :=
        (Types.Small.limitCone
            (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
        ((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)
            x :
          (fun (X : Type u) ↦ X)
            (Types.Small.limitCone
                (F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier))).pt)
        ((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)
            y :
          (fun (X : Type u) ↦ X)
            (Types.Small.limitCone
                (F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier))).pt)
⊢ 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

Tactic:
refine ofHom
      { toFun := (Types.Small.limitConeIsLimit.{v, u} _).lift ((forget MonCat).mapCone _),
        map_one' := by simp; rfl, map_mul' := ?_ }