awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
this_1 : Functor.ReflectsIsomorphisms
  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
    fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier)) :=
  ⋯
c' :
  Cone
    (F ⋙
      forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
        fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
t : IsLimit c'
this_2 :
  Small.{u, max u v}
    (↑((F ⋙
              forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := 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 GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ Functor.mapCone
      (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
        fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
      {
        pt :=
          of
            (Types.Small.limitCone
                (F ⋙
                  forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier))).pt,
        π :=
          {
            app := fun (j : J) ↦
              ofHom
                (MonCat.limitπMonoidHom
                  (F ⋙
                    forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                      MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
                  j),
            naturality := ⋯ } } ≅
    c'

Tactic:
apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit.{v, u} _) t
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ HasLimit F

Tactic:
HasLimit.mk {
    cone := limitCone F
    isLimit := limitConeIsLimit F
  }

Premises used: GrpCat.limitConeIsLimit, GrpCat.limitCone, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
mp :
  HasLimit F →
    Small.{u, max u v}
      (↑(F ⋙
              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v))
mpr :
  Small.{u, max u v}
      (↑(F ⋙
              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v)) →
    HasLimit F
⊢ HasLimit F ↔
    Small.{u, max u v}
      (↑(F ⋙
              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v))

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
⊢ HasLimit F →
    Small.{u, max u v}
      (↑(F ⋙
              forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v))

Tactic:
apply Concrete.small_sections_of_hasLimit

Premises used: CategoryTheory.Limits.Concrete.small_sections_of_hasLimit
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
h :
  Small.{u, max u v}
    (↑(F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ HasLimit F

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
⊢ HasLimits GrpCat

Tactic:
GrpCat.hasLimitsOfSize.{u, u}

Premises used: GrpCat.hasLimitsOfSize
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
⊢ PreservesLimits
    (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat (FD :=
      fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))

Tactic:
GrpCat.forget₂Mon_preservesLimitsOfSize.{u, u}

Premises used: GrpCat.forget₂Mon_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
⊢ PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
⊢ PreservesLimits (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
GrpCat.forget_preservesLimitsOfSize.{u, u}

Premises used: GrpCat.forget_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Grp.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J GrpCat
e : Iso (C := GrpCat ⥤ Type u)
  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := 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))
  (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) :=
  Iso.refl
    (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := 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))
⊢ CreatesLimit F (forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
exact createsLimitOfNatIso e

Premises used: CategoryTheory.createsLimitOfNatIso
-- 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
⊢ Functor.ReflectsIsomorphisms
    (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))

Tactic:
reflectsIsomorphisms_forget₂ _ _

Premises used: CategoryTheory.reflectsIsomorphisms_forget₂
-- 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
⊢ 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))

Tactic:
have : HasLimit _ := ⟨_, hc⟩
-- 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 :
  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))
⊢ 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))

Tactic:
have : Small.{u} (F ⋙ forget CommGrpCat).sections :=
      Concrete.small_sections_of_hasLimit (F ⋙ forget₂ CommGrpCat GrpCat)
-- 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 :
  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))
⊢ 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))

Tactic:
have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat ⋙ forget₂ GrpCat MonCat) ⋙
      forget MonCat).sections := this
-- 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 :
  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))
⊢ 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))

Tactic:
have : Small.{u} ((F ⋙ forget₂ CommGrpCat GrpCat) ⋙ forget GrpCat).sections := this
-- 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))
⊢ LiftsToLimit 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))
    c hc

Tactic:
exact
      { liftedCone :=
          { pt := CommGrpCat.of (Types.Small.limitCone.{v, u} (F ⋙ forget CommGrpCat)).pt
            π :=
              { app j := ofHom <| MonCat.limitπMonoidHom
                  (F ⋙ forget₂ CommGrpCat GrpCat.{u} ⋙ forget₂ GrpCat MonCat.{u}) j
                naturality i j h := hom_ext <| congr_arg MonCat.Hom.hom <|
                  (MonCat.HasLimits.limitCone _).π.naturality h } }
        validLift := by apply IsLimit.uniqueUpToIso (GrpCat.limitConeIsLimit _) hc
        makesLimit :=
          IsLimit.ofFaithful (forget₂ _ GrpCat.{u} ⋙ forget₂ _ MonCat.{u})
            (by apply MonCat.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl }
-- 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
inst_1 :
  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))
⊢ HasLimit F

Tactic:
HasLimit.mk {
    cone := limitCone F
    isLimit := limitConeIsLimit F
  }

Premises used: CategoryTheory.Limits.HasLimit.mk, CommGrpCat.limitCone, CategoryTheory.Limits.LimitCone.mk, CommGrpCat.limitConeIsLimit
-- 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
mp :
  HasLimit F →
    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))
mpr :
  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)) →
    HasLimit F
⊢ HasLimit F ↔
    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))

Tactic:
constructor
-- 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
⊢ HasLimit F →
    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))

Tactic:
apply Concrete.small_sections_of_hasLimit

Premises used: CategoryTheory.Limits.Concrete.small_sections_of_hasLimit
-- 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
h :
  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))
⊢ HasLimit F

Tactic:
infer_instance
-- 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
⊢ HasLimits CommGrpCat

Tactic:
CommGrpCat.hasLimitsOfSize.{u, u}

Premises used: CommGrpCat.hasLimitsOfSize
-- 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
hc : IsLimit c
rw :
  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))
⊢ 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))

Tactic:
rw [GrpCat.hasLimit_iff_small_sections]

Premises used: GrpCat.hasLimit_iff_small_sections
-- 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
hc : IsLimit c
change :
  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))
⊢ 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))

Tactic:
change Small.{u} (F ⋙ forget CommGrpCat).sections
-- 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
hc : IsLimit c
rw : HasLimit F
⊢ 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))

Tactic:
rw [← CommGrpCat.hasLimit_iff_small_sections]

Premises used: CommGrpCat.hasLimit_iff_small_sections
-- 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
hc : IsLimit c
⊢ HasLimit F

Tactic:
⟨_, hc⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- 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
hc : IsLimit c
⊢ HasLimit F

Tactic:
exact ⟨_, hc⟩
-- 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
hc : IsLimit c
⊢ 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))

Tactic:
have : HasLimit (F ⋙ forget₂ CommGrpCat GrpCat) := by
      rw [GrpCat.hasLimit_iff_small_sections]
      change Small.{u} (F ⋙ forget CommGrpCat).sections
      rw [← CommGrpCat.hasLimit_iff_small_sections]
      exact ⟨_, hc⟩
-- 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
hc : IsLimit c
this :
  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))
⊢ IsLimit (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))
    (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))
      c)

Tactic:
exact isLimitOfPreserves _ hc

Premises used: CategoryTheory.Limits.isLimitOfPreserves
-- 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
⊢ PreservesLimits
    (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))

Tactic:
CommGrpCat.forget₂Group_preservesLimitsOfSize.{u, u}

Premises used: CommGrpCat.forget₂Group_preservesLimitsOfSize
-- 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
⊢ PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (forget CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
inferInstance

Premises used: inferInstance
-- 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
⊢ PreservesLimits
    (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
      AddCommGrpCat.carrier))

Tactic:
AddCommGrpCat.forget_preservesLimitsOfSize.{u, u}

Premises used: AddCommGrpCat.forget_preservesLimitsOfSize