awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h_1 : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
j : J
x : (↑(F.obj j) : Type w)
h :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
        ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
          ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
            AddCircle (𝕜 := ℚ) 1)) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (c'.ι.app j) :
            (a : (↑(F.obj j) : Type w)) → (↑c'.pt : Type w))
          x) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
dsimp [c']
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
c : Cocone F
inst_1 : DecidableEq J
h_1 : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1)),
    ι :=
      {
        app := fun (j : J) ↦
          ofHom
            (AddMonoidHom.comp (AddMonoidHom.comp (AddEquiv.toAddMonoidHom (AddEquiv.symm AddEquiv.ulift)) χ)
              (Quot.ι F j)),
        naturality := ⋯ } }
j : J
x : (↑(F.obj j) : Type w)
h h₁ :
  Eq (α := AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)
⊢ Eq (α := AddCircle (𝕜 := ℚ) 1)
    (((AddEquiv.ulift : ULift.{w, 0} (AddCircle (𝕜 := ℚ) 1) ≃+ AddCircle (𝕜 := ℚ) 1) :
          (a : ULift.{w, 0} (AddCircle 1)) → AddCircle 1)
        ((AddEquiv.symm AddEquiv.ulift : (a : AddCircle 1) → ULift.{w, 0} (AddCircle 1))
          ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
            AddCircle (𝕜 := ℚ) 1)) :
      AddCircle (𝕜 := ℚ) 1)
    ((χ : (a : Colimits.Quot F) → AddCircle 1) ((Quot.ι F j : (a : (↑(F.obj j) : Type w)) → Colimits.Quot F) x) :
      AddCircle (𝕜 := ℚ) 1)

Tactic:
rw [AddEquiv.apply_symm_apply]

Premises used: AddEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Category.Grp.LargeColimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : DecidableEq J
⊢ HasColimit F ↔ Small.{w, max u w} (Colimits.Quot F)

Tactic:
⟨fun _ ↦ Small.mk ⟨_, ⟨(Equiv.ofBijective _ ((isColimit_iff_bijective_desc (colimit.cocone F)).mp
    ⟨colimit.isColimit _⟩))⟩⟩, hasColimit_of_small_quot F⟩

Premises used: AddCommGrpCat.hasColimit_of_small_quot, AddCommGrpCat.isColimit_iff_bijective_desc, CategoryTheory.Limits.colimit.isColimit, Small.mk, Nonempty.intro, AddCommGrpCat.carrier, AddCommGrpCat.Colimits.Quot.desc, Equiv.ofBijective, Iff.intro, Exists.intro, Iff.mp, CategoryTheory.Limits.colimit.cocone, DFunLike.coe, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
⊢ ∀ (X : C ⥤ₗ Type v), PreservesFiniteLimits (Functor.obj inverseAux X)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
rw :
  Eq (α :=
    (𝟙_ (Type v)) (𝒞 := types) ⟶
      CommGrp.X
        (Functor.obj (C := CommGrp.{v, u} C)
          (F ⋙
              forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                carrier)).mapCommGrp
          (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)))
    (η ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
    (CategoryStruct.comp (Y :=
      (F ⋙
            forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              carrier)).obj
        (tensorUnit.{v, u} C (𝒞 := inst)))
      (Functor.LaxMonoidal.ε
        (F ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            carrier)))
      ((F ⋙
            forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              carrier)).map
        η))
⊢ Eq.{v + 1} (α :=
    (𝟙_ (Type v)) (𝒞 := types) ⟶
      CommGrp.X
        (Functor.obj (C := CommGrp.{v, u} C)
          (F ⋙
              forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                carrier)).mapCommGrp
          (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)))
    (η ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd)) η

Tactic:
rw [Functor.obj.η_def X (F := F ⋙ forget AddCommGrpCat)]

Premises used: CategoryTheory.Functor.obj.η_def
-- Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
refine :
  Eq.{v + 1} (α :=
    tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
      CommGrp.X
        (Functor.obj (C := CommGrp.{v, u} C)
          (F ⋙
              forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                carrier)).mapCommGrp
          (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)))
    (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
    ((Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ)
⊢ commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X)) ≅
    Functor.obj (C := CommGrp.{v, u} C)
      (F ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            carrier)).mapCommGrp
      (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)

Tactic:
refine CommGrp.mkIso Multiplicative.toAdd.toIso (by
    rw [Functor.obj.η_def X (F := F ⋙ forget AddCommGrpCat)]
    cat_disch) ?_

Premises used: Equiv.toIso, Multiplicative.toAdd, CategoryTheory.CommGrp.mkIso
-- Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
dsimp :
  (𝟙
          (tensorObj (𝒞 := types)
            (MonTypeEquivalenceMon.inverse.obj
                (Functor.obj
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                      (CD := GrpCat.carrier))
                    (toCommGrp.obj (F.obj X))))).X
            (MonTypeEquivalenceMon.inverse.obj
                (Functor.obj
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                      (CD := GrpCat.carrier))
                    (toCommGrp.obj (F.obj X))))).X) ≫
        μ) ≫
      Iso.hom (Equiv.toIso Multiplicative.toAdd) =
    (Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ
⊢ Eq.{v + 1} (α :=
    tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
      CommGrp.X
        (Functor.obj (C := CommGrp.{v, u} C)
          (F ⋙
              forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                carrier)).mapCommGrp
          (Functor.obj (Equivalence.functor Preadditive.commGrpEquivalence) X)))
    (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
    ((Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ)

Tactic:
dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_ofHom]

Premises used: CategoryTheory.ConcreteCategory.forget_map_eq_ofHom, CategoryTheory.Functor.comp_map
-- Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ F.Additive

Tactic:
have : F.Additive := Functor.additive_of_preserves_binary_products _
-- Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this_2 : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
simp :
  Eq.{v + 1} (α :=
    tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⟶
      ToType (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier) (F.obj X))
    (μ ≫ Iso.hom (Equiv.toIso Multiplicative.toAdd))
    ((Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ)
⊢ (𝟙
          (tensorObj (𝒞 := types)
            (MonTypeEquivalenceMon.inverse.obj
                (Functor.obj
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                      (CD := GrpCat.carrier))
                    (toCommGrp.obj (F.obj X))))).X
            (MonTypeEquivalenceMon.inverse.obj
                (Functor.obj
                  (forget₂ GrpCat (FC := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                    GrpCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CD :=
                    MonCat.carrier))
                  (Functor.obj
                    (forget₂ CommGrpCat (FC := fun (x1 x2 : CommGrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                      CommGrpCat.carrier) GrpCat (FD := fun (x1 x2 : GrpCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v))
                      (CD := GrpCat.carrier))
                    (toCommGrp.obj (F.obj X))))).X) ≫
        μ) ≫
      Iso.hom (Equiv.toIso Multiplicative.toAdd) =
    (Iso.hom (Equiv.toIso Multiplicative.toAdd) ⊗ₘ Iso.hom (Equiv.toIso Multiplicative.toAdd)) ≫ μ

Tactic:
simp only [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
F : C ⥤ AddCommGrpCat
inst_3 : PreservesFiniteLimits F
X : C
this_1 : (F ⋙
    forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      carrier)).Braided :=
  Functor.Braided.ofChosenFiniteProducts
    (F ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := carrier))
this_2 : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
x :
  tensorObj (𝒞 := types) (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
    (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
⊢ (Multiplicative.toAdd :
        (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) μ :
            (a :
                (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ×
                  (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) →
              (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X)
          x :
        (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) =
    HAdd.hAdd (α := (↑(F.obj X) : Type v)) (β := (↑(F.obj X) : Type v))
      ((Hom.hom (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X)) :
            (a : (↑(F.obj X ⊗ F.obj X) : Type v)) → (↑(F.obj X) : Type v))
          (((Multiplicative.toAdd :
                  (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
                x.1,
              (Multiplicative.toAdd :
                  (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
                x.2) :
            (↑(F.obj X) : Type v) × (↑(F.obj X) : Type v)) :
        (↑(F.obj X) : Type v))
      ((Hom.hom (SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X)) :
            (a : (↑(F.obj X ⊗ F.obj X) : Type v)) → (↑(F.obj X) : Type v))
          (((Multiplicative.toAdd :
                  (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
                x.1,
              (Multiplicative.toAdd :
                  (a : (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X) → ToType (F.obj X))
                x.2) :
            (↑(F.obj X) : Type v) × (↑(F.obj X) : Type v)) :
        (↑(F.obj X) : Type v))

Tactic:
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 GrpCat
a : (j : J) → (↑(F.obj j) : Type u)
ah :
  a ∈ (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections
j j' : J
f : j ⟶ j'
simp :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                  (F.map f)) :
              (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))) :
        (a : (F ⋙ forget GrpCat).obj j) → (F ⋙ forget GrpCat).obj j')
      (a j)⁻¹ =
    (a j')⁻¹
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).map
            f) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget GrpCat).obj j)) → (fun (X : Type u) ↦ X) ((F ⋙ forget GrpCat).obj j'))
      (a⁻¹ j) =
    a⁻¹ j'

Tactic:
simp only [Functor.comp_map, Pi.inv_apply]

Premises used: CategoryTheory.Functor.comp_map, Pi.inv_apply
-- 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
a : (j : J) → (↑(F.obj j) : Type u)
ah :
  a ∈ (F ⋙ forget GrpCat (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections
j j' : J
f : j ⟶ j'
dsimp :
  (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.map f) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))
      (a j)⁻¹ =
    (a j')⁻¹
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                  (F.map f)) :
              (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))) :
        (a : (F ⋙ forget GrpCat).obj j) → (F ⋙ forget GrpCat).obj j')
      (a j)⁻¹ =
    (a j')⁻¹

Tactic:
dsimp [Functor.sections] at ah ⊢

Premises used: CategoryTheory.Functor.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 GrpCat
a : (j : J) → (↑(F.obj j) : Type u)
ah :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))
        (a j) =
      a j'
j j' : J
f : j ⟶ j'
rw : ((Hom.hom (F.map f) : (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u)) (a j))⁻¹ = (a j')⁻¹
rw₁ rw₂ : (a j')⁻¹ = (a j')⁻¹
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.map f) :
        (a : (↑(F.obj j) : Type u)) → (↑(F.obj j') : Type u))
      (a j)⁻¹ =
    (a j')⁻¹

Tactic:
rw [(F.map f).hom.map_inv (a j), ah f]

Premises used: GrpCat.Hom.hom, CategoryTheory.Functor.map, MonoidHom.map_inv
-- 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))
⊢ 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))

Tactic:
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget GrpCat))

Premises used: _private.0.GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections._proof_1
-- 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 : 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'
⊢ HasLimit
    (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))

Tactic:
have : HasLimit (F ⋙ forget₂ GrpCat MonCat) := ⟨_, 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))
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 :
  HasLimit
    (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))
⊢ 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))

Tactic:
apply Concrete.small_sections_of_hasLimit (F ⋙ forget₂ GrpCat MonCat)

Premises used: GrpCat, CategoryTheory.Functor.comp, MonCat, CategoryTheory.forget₂, CategoryTheory.Limits.Concrete.small_sections_of_hasLimit