∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) {N : PresheafOfModules R}
  (hN : CategoryTheory.Presheaf.IsSheaf J N.presheaf) [inst_1 : J.WEqualsLocallyBijective AddCommGrpCat]
  [inst_2 : PresheafOfModules.IsLocallySurjective J f] [inst_3 : PresheafOfModules.IsLocallyInjective J f] (φ : M₂ ⟶ N)
  (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₂.obj X)),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.ObjectProperty.isLocal.homEquiv ⋯ N.presheaf hN).symm
              ((PresheafOfModules.toPresheaf R).map (CategoryTheory.CategoryStruct.comp f φ))).app
          X))
      (r • m) =
    r •
      (CategoryTheory.ConcreteCategory.hom
          (((CategoryTheory.ObjectProperty.isLocal.homEquiv ⋯ N.presheaf hN).symm
                ((PresheafOfModules.toPresheaf R).map (CategoryTheory.CategoryStruct.comp f φ))).app
            X))
        m