awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
this :
  ∀ (w w_1 : J) (w_2 : w ⟶ w_1) (w_3 : (↑(F.obj w) : Type w))
    (eq :
      a =
        HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
          (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
            ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  carrier) (F.map w_2) :
                (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
              w_3))
          (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)),
    a ∈
      (↑(AddMonoidHom.ker (M := (↑c.pt : Type w))
            (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))) :
        Set (Π₀ (j : J), (↑(F.obj j) : Type w)))
⊢ Membership.mem (γ := Set (Π₀ (j : J), (↑(F.obj j) : Type w)))
      {x : Π₀ (j : J), (↑(F.obj j) : Type w) |
        ∃ (j : J) (j' : J) (u : j ⟶ j') (a : (↑(F.obj j) : Type w)),
          x =
            HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
              (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j'
                ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                      carrier) (F.map u) :
                    (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
                  a))
              (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) j a)}
      a →
    a ∈
      (↑(AddMonoidHom.ker (M := (↑c.pt : Type w))
            (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))) :
        Set (Π₀ (j : J), (↑(F.obj j) : Type w)))

Tactic:
⟨_, _, _, _, eq⟩
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
rw :
  HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3) ∈
    (↑(AddMonoidHom.ker (M := (↑c.pt : Type w))
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))) :
      Set (Π₀ (j : J), (↑(F.obj j) : Type w)))
⊢ a ∈
    (↑(AddMonoidHom.ker (M := (↑c.pt : Type w))
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))) :
      Set (Π₀ (j : J), (↑(F.obj j) : Type w)))

Tactic:
rw [eq]
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
simp :
  HSub.hSub (α := (↑c.pt : Type w)) (β := (↑c.pt : Type w))
      ((Hom.hom (c.ι.app w_1) : (a : (↑(F.obj w_1) : Type w)) → (↑c.pt : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  carrier) (F.map w_2) :
                (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
              w_3 :
            (↑(F.obj w_1) : Type w)) :
        (↑c.pt : Type w))
      ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
    0
⊢ HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3) ∈
    (↑(AddMonoidHom.ker (M := (↑c.pt : Type w))
          (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x))) :
      Set (Π₀ (j : J), (↑(F.obj j) : Type w)))

Tactic:
simp only [SetLike.mem_coe, AddMonoidHom.mem_ker, map_sub, DFinsupp.sumAddHom_single]

Premises used: map_sub, DFinsupp.sumAddHom_single, SetLike.mem_coe, AddMonoidHom.mem_ker
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
change :
  HSub.hSub (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w)) (β :=
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
              (F.map w_2 ≫ c.ι.app w_1) :
            (a : (↑(F.obj w) : Type w)) → (↑(((Functor.const J).obj c.pt).obj w_1) : Type w))
          w_3 :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
    0
⊢ HSub.hSub (α := (↑c.pt : Type w)) (β := (↑c.pt : Type w))
      ((Hom.hom (c.ι.app w_1) : (a : (↑(F.obj w_1) : Type w)) → (↑c.pt : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  carrier) (F.map w_2) :
                (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
              w_3 :
            (↑(F.obj w_1) : Type w)) :
        (↑c.pt : Type w))
      ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
    0

Tactic:
change (F.map _ ≫ c.ι.app _) _ - _ = 0

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
rw :
  HSub.hSub (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w)) (β :=
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
              (c.ι.app w ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const J) c.pt) w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(((Functor.const J).obj c.pt).obj w_1) : Type w))
          w_3 :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
    0
⊢ HSub.hSub (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w)) (β :=
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
              (F.map w_2 ≫ c.ι.app w_1) :
            (a : (↑(F.obj w) : Type w)) → (↑(((Functor.const J).obj c.pt).obj w_1) : Type w))
          w_3 :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
    0

Tactic:
rw [c.ι.naturality]

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
a : Π₀ (j : J), (↑(F.obj j) : Type w)
w w_1 : J
w_2 : w ⟶ w_1
w_3 : (↑(F.obj w) : Type w)
eq :
  a =
    HSub.hSub (α := Π₀ (i : J), (↑(F.obj i) : Type w))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w_1
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(F.obj w_1) : Type w))
          w_3))
      (DFinsupp.single (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) w w_3)
⊢ HSub.hSub (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w)) (β :=
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC := carrier)
              (c.ι.app w ≫ CategoryTheory.Functor.map (Functor.obj (Functor.const J) c.pt) w_2) :
            (a : (↑(F.obj w) : Type w)) → (↑(((Functor.const J).obj c.pt).obj w_1) : Type w))
          w_3 :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) w_1) : Type w))
      ((Hom.hom (c.ι.app w) : (a : (↑(F.obj w) : Type w)) → (↑c.pt : Type w)) w_3 : (↑c.pt : Type w)) =
    0

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id, sub_self]

Premises used: sub_self, CategoryTheory.Category.comp_id, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
j : J
x : (↑(F.obj j) : Type w)
dsimp :
  Eq.{w + 1} (α := (↑c.pt : Type w))
    ((QuotientAddGroup.lift (Relations F)
            (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x)) ⋯ :
          (a : Quot F) → (↑c.pt : Type w))
        ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
            (a : (↑(F.obj j) : Type w)) → Quot F)
          x) :
      (↑c.pt : Type w))
    ((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 :
      (↑c.pt : Type w))
⊢ Eq.{w + 1} (α := (↑c.pt : Type w))
    ((desc F c : (a : Quot F) → (↑c.pt : Type w)) ((ι F j : (a : (↑(F.obj j) : Type w)) → Quot F) x) : (↑c.pt : Type w))
    ((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)) → (↑(((Functor.const J).obj c.pt).obj j) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const J) c.pt) j) : Type w))

Tactic:
dsimp [desc, ι]

Premises used: AddCommGrpCat.Colimits.Quot.ι, AddCommGrpCat.Colimits.Quot.desc
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
j : J
x : (↑(F.obj j) : Type w)
erw :
  Eq.{w + 1} (α := (↑c.pt : Type w))
    ((DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x) :
          (a : Π₀ (j : J), (↑(F.obj j) : Type w)) → (↑c.pt : Type w))
        (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j :
              (↑(F.obj j) : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j) : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          x) :
      (↑c.pt : Type w))
    ((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 :
      (↑c.pt : Type w))
⊢ Eq.{w + 1} (α := (↑c.pt : Type w))
    ((QuotientAddGroup.lift (Relations F)
            (DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x)) ⋯ :
          (a : Quot F) → (↑c.pt : Type w))
        ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
            (a : (↑(F.obj j) : Type w)) → Quot F)
          x) :
      (↑c.pt : Type w))
    ((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 :
      (↑c.pt : Type w))

Tactic:
erw [QuotientAddGroup.lift_mk']

Premises used: QuotientAddGroup.lift_mk'
-- Module: Mathlib.Algebra.Category.Grp.Colimits
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
j : J
x : (↑(F.obj j) : Type w)
⊢ Eq.{w + 1} (α := (↑c.pt : Type w))
    ((DFinsupp.sumAddHom (β := fun (j : J) ↦ (↑(F.obj j) : Type w)) fun (x : J) ↦ Hom.hom (c.ι.app x) :
          (a : Π₀ (j : J), (↑(F.obj j) : Type w)) → (↑c.pt : Type w))
        (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j :
              (↑(F.obj j) : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j) : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          x) :
      (↑c.pt : Type w))
    ((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 :
      (↑c.pt : Type w))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : DecidableEq J
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type w)
⊢ Eq (α := Quot F)
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j') :
          (a : (↑(F.obj j') : Type w)) → Quot F)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
          x) :
      Quot F)
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
          (a : (↑(F.obj j) : Type w)) → Quot F)
        x :
      Quot F)

Tactic:
eq_of_sub_eq_zero ?_

Premises used: eq_of_sub_eq_zero
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : DecidableEq J
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type w)
refine :
  HSub.hSub (α := Quot F) (β := Quot F)
      ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j') :
            (a : (↑(F.obj j') : Type w)) → Quot F)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            x) :
        Quot F)
      ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
            (a : (↑(F.obj j) : Type w)) → Quot F)
          x :
        Quot F) =
    0
⊢ Eq (α := Quot F)
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j') :
          (a : (↑(F.obj j') : Type w)) → Quot F)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
          x) :
      Quot F)
    ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
            (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
          (a : (↑(F.obj j) : Type w)) → Quot F)
        x :
      Quot F)

Tactic:
refine eq_of_sub_eq_zero ?_

Premises used: eq_of_sub_eq_zero
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : DecidableEq J
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type w)
erw :
  HSub.hSub (α := Π₀ (j : J), (↑(F.obj j) : Type w)) (β := Π₀ (j : J), (↑(F.obj j) : Type w))
      (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j' :
              (↑(F.obj j') : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j') : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            x) :
        Π₀ (j : J), (↑(F.obj j) : Type w))
      (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j :
              (↑(F.obj j) : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j) : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          x :
        Π₀ (j : J), (↑(F.obj j) : Type w)) ∈
    AddMonoidHom.ker (QuotientAddGroup.mk' (Relations F))
⊢ HSub.hSub (α := Quot F) (β := Quot F)
      ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j') :
            (a : (↑(F.obj j') : Type w)) → Quot F)
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            x) :
        Quot F)
      ((AddMonoidHom.comp (QuotientAddGroup.mk' (Relations F))
              (DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j) :
            (a : (↑(F.obj j) : Type w)) → Quot F)
          x :
        Quot F) =
    0

Tactic:
erw [← (QuotientAddGroup.mk' (Relations F)).map_sub, ← AddMonoidHom.mem_ker]

Premises used: QuotientAddGroup.mk', AddMonoidHom.map_sub, AddCommGrpCat.Colimits.Relations, AddMonoidHom.mem_ker
-- Module: Mathlib.Algebra.Category.Grp.Colimits
Goal:
J : Type u
inst : Category.{v, u} J
F : CategoryTheory.Functor.{v, w, u, w + 1} J AddCommGrpCat
inst_1 : DecidableEq J
j j' : J
f : j ⟶ j'
x : (↑(F.obj j) : Type w)
rw :
  HSub.hSub (α := Π₀ (j : J), (↑(F.obj j) : Type w)) (β := Π₀ (j : J), (↑(F.obj j) : Type w))
      (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j' :
              (↑(F.obj j') : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j') : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            x) :
        Π₀ (j : J), (↑(F.obj j) : Type w))
      (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j :
              (↑(F.obj j) : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j) : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          x :
        Π₀ (j : J), (↑(F.obj j) : Type w)) ∈
    Relations F
⊢ HSub.hSub (α := Π₀ (j : J), (↑(F.obj j) : Type w)) (β := Π₀ (j : J), (↑(F.obj j) : Type w))
      (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j' :
              (↑(F.obj j') : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j') : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                carrier) (F.map f) :
              (a : (↑(F.obj j) : Type w)) → (↑(F.obj j') : Type w))
            x) :
        Π₀ (j : J), (↑(F.obj j) : Type w))
      (((DFinsupp.singleAddHom.{u, w} (fun (j : J) ↦ (↑(F.obj j) : Type w)) j :
              (↑(F.obj j) : Type w) →+ Π₀ (i : J), (↑(F.obj i) : Type w)) :
            (a : (↑(F.obj j) : Type w)) → Π₀ (j : J), (↑(F.obj j) : Type w))
          x :
        Π₀ (j : J), (↑(F.obj j) : Type w)) ∈
    AddMonoidHom.ker (QuotientAddGroup.mk' (Relations F))

Tactic:
rw [QuotientAddGroup.ker_mk']

Premises used: QuotientAddGroup.ker_mk'