-- 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))
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : (↑(M₁.obj X) : Type u)
m₃ : (↑(M₃.obj X) : Type u)
erw :
  Eq (α :=
    (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map φ))).obj
          (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))
                    Y) :
                Type u))
            (M₂.obj Y) (M₄.obj Y))) :
      Type u))
    ((ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  ModuleCat
                    (↑(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))
                          Y) :
                      Type u)) ↦
              LinearMap (R :=
                (↑(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))
                      Y) :
                  Type u))
                (RingHom.id
                  (↑(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))
                        Y) :
                    Type u))
                (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (f.app Y) :
            (a : (↑(M₁.obj Y) : Type u)) → (↑(M₂.obj Y) : Type u))
          ((ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      ModuleCat
                        (↑(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)) ↦
                  LinearMap (R :=
                    (↑(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))
                    (RingHom.id
                      (↑(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))
                    (↑x1 : Type u) (↑x2 : Type u))
                  (CC := ModuleCat.carrier) (M₁.map φ) :
                (a : (↑(M₁.obj X) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).obj
                        (M₁.obj Y)) :
                    Type u))
              m₁ :
            (↑(Functor.obj
                  (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))
                        φ)))
                  (M₁.obj Y)) :
              Type
                u)) ⊗ₜ[(↑(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))
              Y) :
          Type u)]
        (ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  ModuleCat
                    (↑(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))
                          Y) :
                      Type u)) ↦
              LinearMap (R :=
                (↑(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))
                      Y) :
                  Type u))
                (RingHom.id
                  (↑(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))
                        Y) :
                    Type u))
                (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (g.app Y) :
            (a : (↑(M₃.obj Y) : Type u)) → (↑(M₄.obj Y) : Type u))
          ((ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      ModuleCat
                        (↑(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)) ↦
                  LinearMap (R :=
                    (↑(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))
                    (RingHom.id
                      (↑(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))
                    (↑x1 : Type u) (↑x2 : Type u))
                  (CC := ModuleCat.carrier) (M₃.map φ) :
                (a : (↑(M₃.obj X) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).obj
                        (M₃.obj Y)) :
                    Type u))
              m₃ :
            (↑(Functor.obj
                  (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))
                        φ)))
                  (M₃.obj Y)) :
              Type u)) :
      TensorProduct
        (↑(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))
              Y) :
          Type u)
        (↑(M₂.obj Y) : Type u) (↑(M₄.obj Y) : Type u))
    ((ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  ModuleCat
                    (↑(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)) ↦
              LinearMap (R :=
                (↑(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))
                (RingHom.id
                  (↑(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))
                (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (M₂.map φ) :
            (a : (↑(M₂.obj X) : Type u)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).obj
                    (M₂.obj Y)) :
                Type u))
          ((ModuleCat.Hom.hom (f.app X) : (a : (↑(M₁.obj X) : Type u)) → (↑(M₂.obj X) : Type u)) (m₁, m₃).1 :
            (↑(M₂.obj X) : Type u)) ⊗ₜ[(↑(R.obj Y) : Type u)]
        (ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  ModuleCat
                    (↑(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)) ↦
              LinearMap (R :=
                (↑(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))
                (RingHom.id
                  (↑(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))
                (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (M₄.map φ) :
            (a : (↑(M₄.obj X) : Type u)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).obj
                    (M₄.obj Y)) :
                Type u))
          ((ModuleCat.Hom.hom (g.app X) : (a : (↑(M₃.obj X) : Type u)) → (↑(M₄.obj X) : Type u)) (m₁, m₃).2 :
            (↑(M₄.obj X) : Type u)) :
      TensorProduct (↑(R.obj Y) : Type u)
        (↑(Functor.obj
              (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))
                    φ)))
              (M₂.obj Y)) :
          Type u)
        (↑(Functor.obj
              (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))
                    φ)))
              (M₄.obj Y)) :
          Type u))
⊢ Eq (α :=
    (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map φ))).obj
          (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))
                    Y) :
                Type u))
            (M₂.obj Y) (M₄.obj Y))) :
      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) (X :=
            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))
                      Y) :
                  Type u))
              (M₁.obj Y) (M₃.obj Y))
            (f.app Y ⊗ₘ g.app Y) :
          (a : (↑(M₁.obj Y ⊗ M₃.obj Y) : Type u)) → (↑(M₂.obj Y ⊗ M₄.obj Y) : Type u))
        ((ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    ModuleCat
                      (↑(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)) ↦
                LinearMap (R :=
                  (↑(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))
                  (RingHom.id
                    (↑(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))
                  (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₁.map φ) :
              (a : (↑(M₁.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).obj
                      (M₁.obj Y)) :
                  Type u))
            m₁ ⊗ₜ[(↑(R.obj Y) : Type u)]
          (ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    ModuleCat
                      (↑(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)) ↦
                LinearMap (R :=
                  (↑(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))
                  (RingHom.id
                    (↑(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))
                  (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M₃.map φ) :
              (a : (↑(M₃.obj X) : Type u)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).obj
                      (M₃.obj Y)) :
                  Type u))
            m₃) :
      (↑(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))
                    Y) :
                Type u))
            (M₂.obj Y) (M₄.obj Y)) :
        Type u))
    ((ModuleCat.Hom.hom ((tensorObj M₂ M₄).map φ) :
          (a : (↑(M₂.obj X ⊗ M₄.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map φ))).obj (M₂.obj Y ⊗ M₄.obj Y)) : Type u))
        ((ModuleCat.Hom.hom (f.app X ⊗ₘ g.app X) :
            (a : (↑(M₁.obj X ⊗ M₃.obj X) : Type u)) → (↑(M₂.obj X ⊗ M₄.obj X) : Type u))
          (m₁ ⊗ₜ[(↑(R.obj X) : Type u)] m₃)) :
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map φ))).obj
            (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))
                      Y) :
                  Type u))
              (M₂.obj Y) (M₄.obj Y))) :
        Type u))

Tactic:
erw [ModuleCat.MonoidalCategory.tensorHom_tmul, tensorObj_map_tmul]

Premises used: ModuleCat.MonoidalCategory.tensorHom_tmul, PresheafOfModules.Monoidal.tensorObj_map_tmul