-- Module: Mathlib.Algebra.Category.Grp.Images
Goal:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
a :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
          (F'.e ≫ F'.m) :
        (a : (↑G : Type)) → (↑H : Type))
      (↑(Classical.indefiniteDescription
            (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
            ⋯) :
        (↑G : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              (F'.e ≫ F'.m) :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              (F'.e ≫ F'.m) :
            (a : (↑G : Type)) → (↑H : Type))
          (↑(Classical.indefiniteDescription
                (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
            (↑G : Type)) :
        (↑H : Type))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier) F'.m :
        (a : (↑F'.I : Type)) → (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.e :
            (a : (↑G : Type)) → (↑F'.I : Type))
          (↑(Classical.indefiniteDescription
                (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑(x + y) : (↑H : Type)))
                ⋯) :
            (↑G : Type)) :
        (↑F'.I : Type)) =
    HAdd.hAdd (α := (↑H : Type)) (β := (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.m :
            (a : (↑F'.I : Type)) → (↑H : Type))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
                  F'.e :
                (a : (↑G : Type)) → (↑F'.I : Type))
              (↑(Classical.indefiniteDescription
                    (fun (x_1 : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x_1 = (↑x : (↑H : Type)))
                    ⋯) :
                (↑G : Type)) :
            (↑F'.I : Type)) :
        (↑H : Type))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
              F'.m :
            (a : (↑F'.I : Type)) → (↑H : Type))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{0}) ↦ (↑x1 : Type) →+ (↑x2 : Type)) (CC := carrier)
                  F'.e :
                (a : (↑G : Type)) → (↑F'.I : Type))
              (↑(Classical.indefiniteDescription
                    (fun (x : (↑G : Type)) ↦ (Hom.hom f : (a : (↑G : Type)) → (↑H : Type)) x = (↑y : (↑H : Type))) ⋯) :
                (↑G : Type)) :
            (↑F'.I : Type)) :
        (↑H : Type))

Tactic:
change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.MonoFactorisation.e, CategoryTheory.Limits.MonoFactorisation.m, DFunLike.coe