-- 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 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
φ : M₁.presheaf ⟶ M₂.presheaf
hφ :
  ∀ (X : Cᵒᵖ) (r : (↑(R.obj X) : Type u)) (m : (↑(M₁.obj X) : Type v)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier) (φ.app X) :
          (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
        (r • m) =
      HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                AddCommGrpCat.carrier) (φ.app X) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
            m :
          (↑(M₂.presheaf.obj X) : Type v))
X Y : Cᵒᵖ
f : X ⟶ Y
hf :
  ∀ (x : (↑(M₁.obj X) : Type v)),
    Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
      ((ModuleCat.Hom.hom
              (M₁.map f ≫
                (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                  (ModuleCat.ofHom
                    {
                      toFun :=
                        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦
                              (↑x1 : Type v) →+ (↑x2 : Type v)) (CC := AddCommGrpCat.carrier) (φ.app Y)) :
                          (a : (↑(M₁.presheaf.obj Y) : Type v)) → (↑(M₂.presheaf.obj Y) : Type v)),
                      map_add' := ⋯, map_smul' := ⋯ })) :
            (a : (↑(M₁.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
      ((ModuleCat.Hom.hom
              (ModuleCat.ofHom
                  {
                    toFun :=
                      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v))
                            (CC := AddCommGrpCat.carrier) (φ.app X)) :
                        (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v)),
                    map_add' := ⋯, map_smul' := ⋯ } ≫
                M₂.map f) :
            (a : (↑(M₁.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type v))
⊢ M₁.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
        (ModuleCat.ofHom
          {
            toFun :=
              (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                    AddCommGrpCat.carrier) (φ.app Y)) :
                (a : (↑(M₁.presheaf.obj Y) : Type v)) → (↑(M₂.presheaf.obj Y) : Type v)),
            map_add' := ⋯, map_smul' := ⋯ }) =
    ModuleCat.ofHom
        {
          toFun :=
            (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                  AddCommGrpCat.carrier) (φ.app X)) :
              (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v)),
          map_add' := ⋯, map_smul' := ⋯ :
          LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑(M₁.1 X) : Type v)
            (↑(M₂.1 X) : Type v) } ≫
      M₂.map f

Tactic:
ext x