-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
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
⊢ (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
have 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' := sorry, map_smul' := sorry }) :
          (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' := sorry, map_smul' := sorry } ≫
              (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))
Tactic: ext x