-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Limits (goal)
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 :
  ∀ (x : J),
    Eq (α :=
      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 ⟶
        (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).obj x)
      (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 } }))
        x)
      (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)
⊢ LiftsToLimit F (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) c t
have h₁ : 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 := sorry :
              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))))))
          sorry :
      LiftableCone F (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
        c })
Tactic: refine LiftsToLimit.mk (LiftableCone.mk
    { pt := MonCat.of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
      π := NatTrans.mk
        (fun j => ofHom (limitπMonoidHom F j))
        (MonCat.HasLimits.limitCone F).π.naturality }
    (Cone.ext
      ((Types.isLimitEquivSections t).trans (equivShrink _)).symm.toIso
      (fun _ ↦ ?_))) ?_