-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommGrpCat
c :
  Cone
    (F ⋙
      forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
        (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
hc : IsLimit c
this_1 :
  HasLimit
    (F ⋙
      forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
        (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier))
this_2 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
this_3 :
  Small.{u, max u v}
    (↑((F ⋙
              forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                  GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier) ⋙
                forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                  GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                  MonCat.carrier)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              MonCat.carrier)).sections :
      Type (max u v))
this :
  Small.{u, max u v}
    (↑((F ⋙
              forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier)) ⋙
            forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              GrpCat.carrier)).sections :
      Type (max u v))
⊢ IsLimit.{w, u, v, u + 1} (J := J) (F :=
    F ⋙
      forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
          (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier) ⋙
        forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := GrpCat.carrier) MonCat
          (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
    (Functor.mapCone
      (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) GrpCat
          (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := GrpCat.carrier) ⋙
        forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := GrpCat.carrier) MonCat
          (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
      {
        pt :=
          of
            (Types.Small.limitCone
                (F ⋙
                  forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier))).pt,
        π :=
          {
            app := fun (j : J) ↦
              ofHom
                (MonCat.limitπMonoidHom
                  (F ⋙
                    forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                        GrpCat.carrier) ⋙
                      forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := MonCat.carrier))
                  j),
            naturality := ⋯ } })

Tactic:
apply MonCat.HasLimits.limitConeIsLimit _

Premises used: MonCat.HasLimits.limitConeIsLimit