-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ M₃ M₄ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X Y : Cᵒᵖ
f : X ⟶ Y
m₁ : (↑(M₁.obj X) : Type u)
m₂ m₂' : (↑(M₂.obj X) : Type u)
rw :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (M₁.map f) :
          (a : (↑(M₁.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
        m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
      HAdd.hAdd (α := (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u)) (β :=
        (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂ :
          (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂' :
          (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u)) =
    HAdd.hAdd (α :=
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj
            (tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Y) : Type u)) (M₁.obj Y) (M₂.obj Y))) :
        Type u))
      (β :=
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj
            (tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Y) : Type u)) (M₁.obj Y) (M₂.obj Y))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map f) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂ :
        TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map f) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂' :
        TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u))
rw₁ rw₂ :
  HAdd.hAdd (α := TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u)) (β :=
      TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map f) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂ :
        TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map f) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂' :
        TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u)) =
    HAdd.hAdd (α :=
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj
            (tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Y) : Type u)) (M₁.obj Y) (M₂.obj Y))) :
        Type u))
      (β :=
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj
            (tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Y) : Type u)) (M₁.obj Y) (M₂.obj Y))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map f) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂ :
        TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map f) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂' :
        TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (M₁.map f) :
          (a : (↑(M₁.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
        m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
      (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
            LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (M₂.map f) :
          (a : (↑(M₂.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
        (m₂ + m₂') =
    HAdd.hAdd (α :=
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj
            (tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Y) : Type u)) (M₁.obj Y) (M₂.obj Y))) :
        Type u))
      (β :=
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj
            (tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Y) : Type u)) (M₁.obj Y) (M₂.obj Y))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map f) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂ :
        TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map f) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₁.obj Y)) : Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type u)) ↦
                LinearMap (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₂.map f) :
              (a : (↑(M₂.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj (M₂.obj Y)) : Type u))
            m₂' :
        TensorProduct (↑(R.obj Y) : Type u) (↑(M₁.obj Y) : Type u) (↑(M₂.obj Y) : Type u))

Tactic:
rw [map_add, TensorProduct.tmul_add]

Premises used: map_add, TensorProduct.tmul_add