-- Mathlib/Algebra/Category/Grp/Colimits.lean
@[simp]
lemma Quot.map_ι [DecidableEq J] {j j' : J} {f : j ⟶ j'} (x : F.obj j) :
    Quot.ι F j' (F.map f x) = Quot.ι F j x

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j'))
      ((ConcreteCategory.hom (F.map f)) x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x

Tactic:
refine eq_of_sub_eq_zero ?_

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j'))
        ((ConcreteCategory.hom (F.map f)) x) -
      ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x =
    0

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j'))
        ((ConcreteCategory.hom (F.map f)) x) -
      ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x =
    0

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

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j) x ∈
    (QuotientAddGroup.mk' (Relations F)).ker

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ DFinsupp.single j' ((ConcreteCategory.hom (F.map f)) x) - DFinsupp.single j x ∈ Relations F

Tactic:
exact AddSubgroup.subset_closure ⟨j, j', f, x, rfl⟩

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j) x ∈
    (QuotientAddGroup.mk' (Relations F)).ker

Tactic:
rw [QuotientAddGroup.ker_mk']

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j) x ∈
    Relations F

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j') ((ConcreteCategory.hom (F.map f)) x) -
      (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j) x ∈
    Relations F

Tactic:
simp only [DFinsupp.singleAddHom_apply]

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ DFinsupp.single j' ((ConcreteCategory.hom (F.map f)) x) - DFinsupp.single j x ∈ Relations F

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ι F j') ((ConcreteCategory.hom (F.map f)) x) = (ι F j) x

Tactic:
dsimp [ι]

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j'))
      ((ConcreteCategory.hom (F.map f)) x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x