∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [CategoryTheory.Presheaf.IsLocallyInjective J α] {M₀ : PresheafOfModules R₀}
  {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj) [CategoryTheory.Presheaf.IsLocallyInjective J φ]
  {X : Cᵒᵖ} (r : ↑(R.obj.obj X)) (m : ↑(A.obj.obj X)),
  ∀ S ∈ J (Opposite.unop X),
    ∀ (r₀ : CategoryTheory.Presieve.FamilyOfElements (R₀.comp (CategoryTheory.forget RingCat)) S.arrows)
      (m₀ : CategoryTheory.Presieve.FamilyOfElements (M₀.presheaf.comp (CategoryTheory.forget Ab)) S.arrows),
      (r₀.map (CategoryTheory.Functor.whiskerRight α (CategoryTheory.forget RingCat))).IsAmalgamation r →
        (m₀.map (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget Ab))).IsAmalgamation m →
          ∀ (a : ↑(A.obj.obj X)),
            ((r₀.smul m₀).map (CategoryTheory.Functor.whiskerRight φ (CategoryTheory.forget Ab))).IsAmalgamation a →
              ∀ (Y : Cᵒᵖ) (f : X ⟶ Y) (a₀ : ↑(R₀.obj Y)),
                (CategoryTheory.ConcreteCategory.hom (α.app Y)) a₀ =
                    (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
                  ∀ (b₀ : ↑(M₀.obj Y)),
                    (CategoryTheory.ConcreteCategory.hom (φ.app Y)) b₀ =
                        (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
                      (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) a =
                        (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (a₀ • b₀)