-- Mathlib/Algebra/Category/Grp/Colimits.lean
lemma quotUliftToQuot_ι [DecidableEq J] (j : J) (x : (F ⋙ uliftFunctor.{u'}).obj j) :
    quotUliftToQuot F (Quot.ι _ j x) = Quot.ι F j x.down

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

Tactic:
dsimp [quotUliftToQuot, Quot.ι]

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

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

Tactic:
conv_lhs => erw [AddMonoidHom.comp_apply (QuotientAddGroup.mk' (Relations (F ⋙ uliftFunctor)))
  (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 ⋙ uliftFunctor).obj j)
⊢ (DFinsupp.sumAddHom fun j =>
        ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)).comp
          ↑AddEquiv.ulift)
      ((DFinsupp.singleAddHom (fun j => ↑((F ⋙ uliftFunctor).obj j)) j) x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x.down

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

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 ⋙ uliftFunctor).obj j)
⊢ (DFinsupp.sumAddHom fun j =>
        ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)).comp
          ↑AddEquiv.ulift)
      ((DFinsupp.singleAddHom (fun j => ↑((F ⋙ uliftFunctor).obj j)) j) x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x.down

Tactic:
simp only [Functor.comp_obj, uliftFunctor_obj, 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 ⋙ uliftFunctor).obj j)
⊢ ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) (AddEquiv.ulift x) =
    ((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x.down