-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X_1 : Cᵒᵖ
hX_1 : Limits.IsInitial.{v₁, u₁} X_1
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M N : PresheafOfModules.{v, v₁, u₁, u} R
f : M ⟶ N
Y Z : Cᵒᵖ
g : Y ⟶ Z
hf :
  ∀ (x : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)),
    Eq (α := (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
      ((ModuleCat.Hom.hom
              ((forgetToPresheafModuleCatObj X hX M).map g ≫
                ModuleCat.ofHom
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
                            LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u))
                              (↑x1 : Type v) (↑x2 : Type v))
                            (CC := ModuleCat.carrier) (f.app Z)) :
                        (a : (↑(M.obj Z) : Type v)) → (↑(N.obj Z) : Type v)),
                    map_add' := ⋯, map_smul' := ⋯ }) :
            (a : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)) →
              (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
          x :
        (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                            LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u))
                              (↑x1 : Type v) (↑x2 : Type v))
                            (CC := ModuleCat.carrier) (f.app Y)) :
                        (a : (↑(M.obj Y) : Type v)) → (↑(N.obj Y) : Type v)),
                    map_add' := ⋯, map_smul' := ⋯ } ≫
                (forgetToPresheafModuleCatObj X hX N).map g) :
            (a : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)) →
              (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
          x :
        (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
⊢ (forgetToPresheafModuleCatObj X hX M).map g ≫
      ModuleCat.ofHom
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u)) (↑x1 : Type v)
                    (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (f.app Z)) :
              (a : (↑(M.obj Z) : Type v)) → (↑(N.obj Z) : Type v)),
          map_add' := ⋯, map_smul' := ⋯ } =
    ModuleCat.ofHom
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                  LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                    (↑x2 : Type v))
                  (CC := ModuleCat.carrier) (f.app Y)) :
              (a : (↑(M.obj Y) : Type v)) → (↑(N.obj Y) : Type v)),
          map_add' := ⋯, map_smul' := ⋯ :
          LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u))
            (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)
            (↑((forgetToPresheafModuleCatObj X hX N).obj Y) : Type v) } ≫
      (forgetToPresheafModuleCatObj X hX N).map g

Tactic:
ext x