∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) {M N : PresheafOfModules R} (α : M ⟶ N) (X : Cᵒᵖ)
  (m : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))),
  (ModuleCat.Hom.hom (((PresheafOfModules.pushforward φ).map α).app X)) m =
    (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op (F.obj (Opposite.unop X))))) m