∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ M₂ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) {X Y : Cᵒᵖ} (f : X ⟶ Y)
  (m₁ m₂ : ↑(M₁.obj X)) (n : ↑(M₂.obj X)),
  (fun m₁ m₂ =>
        (CategoryTheory.ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)]
          (CategoryTheory.ConcreteCategory.hom (M₂.map f)) m₂)
      (m₁ + m₂) n =
    (fun m₁ m₂ =>
          (CategoryTheory.ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)]
            (CategoryTheory.ConcreteCategory.hom (M₂.map f)) m₂)
        m₁ n +
      (fun m₁ m₂ =>
          (CategoryTheory.ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)]
            (CategoryTheory.ConcreteCategory.hom (M₂.map f)) m₂)
        m₂ n