-- 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 Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
m₁ : (↑(M₁.obj X) : Type u)
m₂ : (↑(M₂.obj X) : Type u)
dsimp :
  Eq (α :=
    (↑(Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g))))
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Z) : Type u)) (M₁.obj Z)
            (M₂.obj Z))) :
      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) (Y :=
              Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g)))) (M₁.obj Z))
              (M₁.map (f ≫ g)) :
            (a : (↑(M₁.obj X) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g)))).obj (M₁.obj Z)) : Type u))
          m₁ ⊗ₜ[(↑(R.obj Z) : 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) (Y :=
              Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g)))) (M₂.obj Z))
              (M₂.map (f ≫ g)) :
            (a : (↑(M₂.obj X) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g)))).obj (M₂.obj Z)) : Type u))
          m₂ :
      TensorProduct (↑(R.obj Z) : Type u) (↑(M₁.obj Z) : Type u) (↑(M₂.obj Z) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj Y) : Type u)) ↦
              LinearMap (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (M₁.map g) :
            (a : (↑(M₁.obj Y) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map g))).obj (M₁.obj Z)) : 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)) ⊗ₜ[(↑(R.obj Z) : Type u)]
        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj Y) : Type u)) ↦
              LinearMap (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (M₂.map g) :
            (a : (↑(M₂.obj Y) : Type u)) →
              (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map g))).obj (M₂.obj Z)) : 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)) :
      TensorProduct (↑(R.obj Z) : Type u) (↑(M₁.obj Z) : Type u) (↑(M₂.obj Z) : Type u))
⊢ Eq (α :=
    (↑(Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g))))
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Z) : Type u)) (M₁.obj Z)
            (M₂.obj Z))) :
      Type u))
    ((ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (f ≫ g)) :
          (a : (↑(M₁.obj X ⊗ M₂.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g)))).obj (M₁.obj Z ⊗ M₂.obj Z)) : Type u))
        (m₁ ⊗ₜ[(↑(Functor.obj
                (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) :
            Type u)]
          m₂) :
      (↑(Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g))))
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Z) : Type u)) (M₁.obj Z)
              (M₂.obj Z))) :
        Type u))
    ((ModuleCat.Hom.hom
            (tensorObjMap M₁ M₂ f ≫
              CategoryTheory.Functor.map
                  (ModuleCat.restrictScalars
                    (RingCat.Hom.hom
                      (CategoryTheory.Functor.map
                        (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))
                        f)))
                  (tensorObjMap M₁ M₂ g) ≫
                NatTrans.app
                  (Iso.inv
                    (ModuleCat.restrictScalarsComp'
                      (RingCat.Hom.hom
                        (CategoryTheory.Functor.map
                          (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))
                          f))
                      (RingCat.Hom.hom
                        (CategoryTheory.Functor.map
                          (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))
                          g))
                      (RingCat.Hom.hom
                        (CategoryTheory.Functor.map
                          (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))
                          (f ≫ g)))
                      ⋯))
                  (MonoidalCategoryStruct.tensorObj (𝒞 :=
                    ModuleCat.moduleCategory
                      (↑(Functor.obj
                            (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))
                            Z) :
                        Type u))
                    (M₁.obj Z) (M₂.obj Z))) :
          (a : (↑(M₁.obj X ⊗ M₂.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g)))).obj (M₁.obj Z ⊗ M₂.obj Z)) : Type u))
        (m₁ ⊗ₜ[(↑(Functor.obj
                (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) :
            Type u)]
          m₂) :
      (↑(Functor.obj (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (f ≫ g))))
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj Z) : Type u)) (M₁.obj Z)
              (M₂.obj Z))) :
        Type u))

Tactic:
dsimp [tensorObjMap]

Premises used: PresheafOfModules.Monoidal.tensorObjMap