{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.val) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.val) →
                      [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          [J.WEqualsLocallyBijective AddCommGrpCat] →
                            {F : SheafOfModules R} →
                              (PresheafOfModules.sheafify α φ ⟶ F) ≃
                                (M₀ ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F))