-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Images (goal)
Goal:
R : Type u
inst : Ring R
G H : ModuleCat.{v, u} R
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
⊢ Eq (α := (↑H : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) F'.m :
          (a : (↑F'.I : Type v)) → (↑H : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) F'.e :
              (a : (↑G : Type v)) → (↑F'.I : Type v))
            (↑(Classical.indefiniteDescription
                  (fun (x_1 : (↑G : Type v)) ↦
                    (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑(x + y) : (↑H : Type v)))
                  ⋯) :
              (↑G : Type v)) :
          (↑F'.I : Type v)) :
      (↑H : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) F'.m :
          (a : (↑F'.I : Type v)) → (↑H : Type v))
        (HAdd.hAdd (α := (↑F'.1 : Type v)) (β := (↑F'.1 : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  carrier) F'.e :
                (a : (↑G : Type v)) → (↑F'.I : Type v))
              (↑(Classical.indefiniteDescription
                    (fun (x_1 : (↑G : Type v)) ↦
                      (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
                    ⋯) :
                (↑G : Type v)) :
            (↑F'.I : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                  carrier) F'.e :
                (a : (↑G : Type v)) → (↑F'.I : Type v))
              (↑(Classical.indefiniteDescription
                    (fun (x : (↑G : Type v)) ↦
                      (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x = (↑y : (↑H : Type v)))
                    ⋯) :
                (↑G : Type v)) :
            (↑F'.I : Type v))) :
      (↑H : Type v))
have a : (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
        F'.m :
      (a : (↑F'.I : Type v)) → (↑H : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) F'.e :
          (a : (↑G : Type v)) → (↑F'.I : Type v))
        (↑(Classical.indefiniteDescription
              (fun (x_1 : (↑G : Type v)) ↦
                (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑(x + y) : (↑H : Type v)))
              sorry) :
          (↑G : Type v)) :
      (↑F'.I : Type v)) =
  HAdd.hAdd (α := (↑H : Type v)) (β := (↑H : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) F'.m :
          (a : (↑F'.I : Type v)) → (↑H : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) F'.e :
              (a : (↑G : Type v)) → (↑F'.I : Type v))
            (↑(Classical.indefiniteDescription
                  (fun (x_1 : (↑G : Type v)) ↦
                    (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x_1 = (↑x : (↑H : Type v)))
                  sorry) :
              (↑G : Type v)) :
          (↑F'.I : Type v)) :
      (↑H : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
            carrier) F'.m :
          (a : (↑F'.I : Type v)) → (↑H : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
                carrier) F'.e :
              (a : (↑G : Type v)) → (↑F'.I : Type v))
            (↑(Classical.indefiniteDescription
                  (fun (x : (↑G : Type v)) ↦ (Hom.hom f : (a : (↑G : Type v)) → (↑H : Type v)) x = (↑y : (↑H : Type v)))
                  sorry) :
              (↑G : Type v)) :
          (↑F'.I : Type v)) :
      (↑H : Type v))
Tactic: rw [map_add]