awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
⊢ PreservesFiniteLimits.{u, u, u + 1, u + 1} (C := J ⥤ AddCommGrpCat) colim

Tactic:
apply Functor.preservesFiniteLimits_of_preservesHomology

Premises used: CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
⊢ AB4 AddCommGrpCat

Tactic:
AB4.of_AB5 _

Premises used: CategoryTheory.AB4.of_AB5
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst_1 : SmallCategory J
inst_2 : IsFiltered J
inst : Functor.PreservesEpimorphisms.{u, u, u + 1, u + 1} (C := Discrete J ⥤ AddCommGrpCat) lim
⊢ HasExactLimitsOfShape (Discrete J) AddCommGrpCat

Tactic:
apply +allowSynthFailures hasExactLimitsOfShape_of_preservesEpi

Premises used: CategoryTheory.hasExactLimitsOfShape_of_preservesEpi
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j }) (Iso.symm (Pi.isoLimit X))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ X.obj { as := j })))
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ Y.obj { as := j })))
⊢ Eq (α := ((i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
          (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)) :
      (a : (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u)) →
        (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))

Tactic:
have : Pi.map (fun i ↦ f.app ⟨i⟩) = iX.inv ≫ lim.map f ≫ iY.hom := by
        simp only [Discrete.functor_obj_eq_as, Discrete.mk_as, Pi.isoLimit,
          IsLimit.conePointUniqueUpToIso, limit.cone, AddCommGrpCat.HasLimit.productLimitCone,
          Iso.trans_inv, Functor.mapIso_inv, IsLimit.uniqueUpToIso_inv, Cone.forget_map,
          IsLimit.liftConeMorphism_hom, limit.isLimit_lift, Iso.symm_inv, Functor.mapIso_hom,
          IsLimit.uniqueUpToIso_hom, lim_obj, lim_map, Iso.trans_hom, Iso.symm_hom,
          AddCommGrpCat.HasLimit.lift, Functor.const_obj_obj, Category.assoc, limit.lift_map_assoc,
          Pi.cone_pt, iX, iY]
        ext g j
        change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _
        simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π, Fan.mk_pt,
          Fan.mk_π_app, Pi.map_apply]
        change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _
        simp
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j }) (Iso.symm (Pi.isoLimit X))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ X.obj { as := j })))
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ Y.obj { as := j })))
this_1 :
  Eq (α := ((i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
          (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)) :
      (a : (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u)) →
        (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))
this : Epi (iX.hom ≫ (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom) ≫ iY.inv)
⊢ Epi (X := Functor.obj lim X) (CategoryTheory.Functor.map lim f)

Tactic:
simpa using this
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j }) (Iso.symm (Pi.isoLimit X))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ X.obj { as := j })))
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ Y.obj { as := j })))
this :
  Eq (α := ((i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
          (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)) :
      (a : (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u)) →
        (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))
suffices : Epi (iX.hom ≫ (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom) ≫ iY.inv)
⊢ Epi (X := Functor.obj lim X) (CategoryTheory.Functor.map lim f)

Tactic:
suffices Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv) by simpa using this
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j }) (Iso.symm (Pi.isoLimit X))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ X.obj { as := j })))
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ Y.obj { as := j })))
this :
  Eq (α := ((i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
          (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)) :
      (a : (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u)) →
        (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))
suffices :
  Epi (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
    (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)
⊢ Epi (iX.hom ≫ (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom) ≫ iY.inv)

Tactic:
suffices Epi (iX.inv ≫ lim.map f ≫ iY.hom) from inferInstance
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j }) (Iso.symm (Pi.isoLimit X))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ X.obj { as := j })))
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ Y.obj { as := j })))
this :
  Eq (α := ((i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
          (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)) :
      (a : (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u)) →
        (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))
rw :
  Function.Surjective.{u + 1, u + 1} (α := (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u))
    (β := (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
⊢ Epi (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
    (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)

Tactic:
rw [AddCommGrpCat.epi_iff_surjective, ← this]

Premises used: AddCommGrpCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j }) (Iso.symm (Pi.isoLimit X))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ X.obj { as := j })))
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ Y.obj { as := j })))
this :
  Eq (α := ((i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
          (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)) :
      (a : (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u)) →
        (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))
⊢ ∀ (k : Discrete J),
    Function.Surjective (α := (↑(X.obj k) : Type u)) (β := (↑(Y.obj k) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (f.app k)) :
        (a : (↑(X.obj k) : Type u)) → (↑(Y.obj k) : Type u))

Tactic:
simp_rw [CategoryTheory.NatTrans.epi_iff_epi_app, AddCommGrpCat.epi_iff_surjective] at hf

Premises used: CategoryTheory.NatTrans.epi_iff_epi_app, AddCommGrpCat.epi_iff_surjective
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
iX : limit X ≅ AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ X.obj { as := j }) (Iso.symm (Pi.isoLimit X))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ X.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ X.obj { as := j })))
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)) :=
  Iso.trans (Y := ∏ᶜ fun (j : J) ↦ Y.obj { as := j }) (Iso.symm (Pi.isoLimit Y))
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Discrete.functor fun (j : J) ↦ Y.obj { as := j }))
      (LimitCone.isLimit (AddCommGrpCat.HasLimit.productLimitCone fun (j : J) ↦ Y.obj { as := j })))
this :
  Eq (α := ((i : J) → (↑(X.obj { as := i }) : Type u)) → (i : J) → (↑(Y.obj { as := i }) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u)))
          (iX.inv ≫ CategoryTheory.Functor.map lim f ≫ iY.hom)) :
      (a : (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u)) →
        (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))
hf :
  ∀ (k : Discrete J),
    Function.Surjective (α := (↑(X.obj k) : Type u)) (β := (↑(Y.obj k) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (f.app k)) :
        (a : (↑(X.obj k) : Type u)) → (↑(Y.obj k) : Type u))
⊢ Function.Surjective.{u + 1, u + 1} (α := (↑(AddCommGrpCat.of ((i : J) → (↑(X.obj { as := i }) : Type u))) : Type u))
    (β := (↑(AddCommGrpCat.of ((i : J) → (↑(Y.obj { as := i }) : Type u))) : Type u))
    (Pi.map (α := fun (i : J) ↦ (↑(X.obj { as := i }) : Type u)) (β := fun (i : J) ↦ (↑(Y.obj { as := i }) : Type u))
      fun (i : J) ↦
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (X := X.obj { as := i }) (f.app { as := i })) :
        (a : (↑(X.obj { as := i }) : Type u)) → (↑(Y.obj { as := i }) : Type u)))

Tactic:
fun b ↦ ⟨fun i ↦ (hf ⟨i⟩ (b i)).choose, ?_⟩

Premises used: CategoryTheory.Discrete.mk, Exists.intro, Exists.choose, Function.Surjective
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
⊢ Functor.PreservesEpimorphisms.{u, u, u + 1, u + 1} (C := Discrete J ⥤ AddCommGrpCat) lim

Tactic:
exact {
    preserves {X Y} f hf := by
      let iX : limit X ≅ AddCommGrpCat.of ((i : J) → X.obj ⟨i⟩) := (Pi.isoLimit X).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
      let iY : limit Y ≅ AddCommGrpCat.of ((i : J) → Y.obj ⟨i⟩) := (Pi.isoLimit Y).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
      have : Pi.map (fun i ↦ f.app ⟨i⟩) = iX.inv ≫ lim.map f ≫ iY.hom := by
        simp only [Discrete.functor_obj_eq_as, Discrete.mk_as, Pi.isoLimit,
          IsLimit.conePointUniqueUpToIso, limit.cone, AddCommGrpCat.HasLimit.productLimitCone,
          Iso.trans_inv, Functor.mapIso_inv, IsLimit.uniqueUpToIso_inv, Cone.forget_map,
          IsLimit.liftConeMorphism_hom, limit.isLimit_lift, Iso.symm_inv, Functor.mapIso_hom,
          IsLimit.uniqueUpToIso_hom, lim_obj, lim_map, Iso.trans_hom, Iso.symm_hom,
          AddCommGrpCat.HasLimit.lift, Functor.const_obj_obj, Category.assoc, limit.lift_map_assoc,
          Pi.cone_pt, iX, iY]
        ext g j
        change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _
        simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π, Fan.mk_pt,
          Fan.mk_π_app, Pi.map_apply]
        change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _
        simp
      suffices Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv) by simpa using this
      suffices Epi (iX.inv ≫ lim.map f ≫ iY.hom) from inferInstance
      rw [AddCommGrpCat.epi_iff_surjective, ← this]
      simp_rw [CategoryTheory.NatTrans.epi_iff_epi_app, AddCommGrpCat.epi_iff_surjective] at hf
      refine fun b ↦ ⟨fun i ↦ (hf ⟨i⟩ (b i)).choose, ?_⟩
      funext i
      exact (hf ⟨i⟩ (b i)).choose_spec }
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
h : IsSeparator (AddCommGrpCat.of (ULift.{u, 0} ℤ))
⊢ ∃ (G : AddCommGrpCat.{u}), IsSeparator G

Tactic:
use AddCommGrpCat.of (ULift ℤ)

Premises used: ULift, Int, AddCommGrpCat.of
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h :
  ∀ (G : AddCommGrpCat.{u}),
    ObjectProperty.singleton (AddCommGrpCat.of (ULift.{u, 0} ℤ)) G → ∀ (h : G ⟶ A), h ≫ f = h ≫ g
h₁ :
  ∀
    (h :
      ∀ (h : AddCommGrpCat.of (ULift.{u, 0} ℤ) ⟶ A) (x : ℤ),
        Eq (α := (↑B : Type u))
          ((AddCommGrpCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u))
              ((AddCommGrpCat.Hom.hom h : (a : ULift.{u, 0} ℤ) → (↑A : Type u)) { down := x : ULift.{u, 0} ℤ } :
                (↑A : Type u)) :
            (↑B : Type u))
          ((AddCommGrpCat.Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u))
              ((AddCommGrpCat.Hom.hom h : (a : ULift.{u, 0} ℤ) → (↑A : Type u)) { down := x : ULift.{u, 0} ℤ } :
                (↑A : Type u)) :
            (↑B : Type u)))
    (x : (↑A : Type u)),
    Eq (α := (↑B : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) f :
            (a : (↑A : Type u)) → (↑B : Type u))
          x :
        (↑B : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) g :
            (a : (↑A : Type u)) → (↑B : Type u))
          x :
        (↑B : Type u))
⊢ f = g

Tactic:
simp_all only [ObjectProperty.singleton_iff, AddCommGrpCat.ext_iff,
      AddCommGrpCat.hom_comp, AddMonoidHom.coe_comp, Function.comp_apply, forall_eq', ULift.forall]

Premises used: ULift.forall, AddCommGrpCat.ext_iff, forall_eq', CategoryTheory.ObjectProperty.singleton_iff, AddCommGrpCat.hom_comp, AddMonoidHom.coe_comp, Function.comp_apply
-- Module: Mathlib.Algebra.Category.Grp.AB
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h :
  ∀ (h : AddCommGrpCat.of (ULift.{u, 0} ℤ) ⟶ A) (x : ℤ),
    Eq (α := (↑B : Type u))
      ((AddCommGrpCat.Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u))
          ((AddCommGrpCat.Hom.hom h : (a : ULift.{u, 0} ℤ) → (↑A : Type u)) { down := x : ULift.{u, 0} ℤ } :
            (↑A : Type u)) :
        (↑B : Type u))
      ((AddCommGrpCat.Hom.hom g : (a : (↑A : Type u)) → (↑B : Type u))
          ((AddCommGrpCat.Hom.hom h : (a : ULift.{u, 0} ℤ) → (↑A : Type u)) { down := x : ULift.{u, 0} ℤ } :
            (↑A : Type u)) :
        (↑B : Type u))
x : (↑A : Type u)
y z : ULift.{u, 0} ℤ
⊢ (fun (y : ULift.{u, 0} ℤ) ↦ y • x) (y + z) =
    HAdd.hAdd (α := (↑A : Type u)) ((fun (y : ULift.{u, 0} ℤ) ↦ y • x) y) ((fun (y : ULift.{u, 0} ℤ) ↦ y • x) z)

Tactic:
simp only [add_smul]

Premises used: add_smul