-- Mathlib/Algebra/Category/Grp/Colimits.lean
lemma quotToQuotUlift_ι [DecidableEq J] (j : J) (x : F.obj j) :
    quotToQuotUlift F (Quot.ι F j x) = Quot.ι _ j (ULift.up x)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (QuotientAddGroup.lift (Relations F)
        (DFinsupp.sumAddHom fun j =>
          ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
                (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j)).comp
            ↑AddEquiv.ulift.symm)
        ⋯)
      (((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x) =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j))
      { down := x }

Tactic:
conv_lhs => erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations F))
  (DFinsupp.singleAddHom _ j), QuotientAddGroup.lift_mk']

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun j =>
        ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
              (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j)).comp
          ↑AddEquiv.ulift.symm)
      ((DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j) x) =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j))
      { down := x }

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j))
      (AddEquiv.ulift.symm x) =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j))
      { down := x }

Tactic:
rfl

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun j =>
        ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
              (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j)).comp
          ↑AddEquiv.ulift.symm)
      ((DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j) x) =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j))
      { down := x }

Tactic:
simp only [DFinsupp.singleAddHom_apply, DFinsupp.sumAddHom_single, AddMonoidHom.coe_comp,
  AddMonoidHom.coe_coe, Function.comp_apply]

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j))
      (AddEquiv.ulift.symm x) =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j))
      { down := x }

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (quotToQuotUlift F) ((Quot.ι F j) x) = (Quot.ι (F ⋙ uliftFunctor) j) { down := x }

Tactic:
dsimp [quotToQuotUlift, Quot.ι]

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (QuotientAddGroup.lift (Relations F)
        (DFinsupp.sumAddHom fun j =>
          ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
                (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j)).comp
            ↑AddEquiv.ulift.symm)
        ⋯)
      (((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x) =
    ((QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor))).comp
        (DFinsupp.singleAddHom (fun j => ULift.{u_1, w} ↑(F.obj j)) j))
      { down := x }