-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal (goal)
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 : Cᵒᵖ
m₁ : (↑(M₁.obj X) : Type u)
m₂ : (↑(M₂.obj X) : Type u)
⊢ Eq (α :=
    (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj X) : Type u)) (M₁.obj X)
            (M₂.obj X))) :
      Type u))
    ((ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (𝟙 X)) :
          (a : (↑(M₁.obj X ⊗ M₂.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj (M₁.obj X ⊗ M₂.obj X)) : 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₂) :
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj X) : Type u)) (M₁.obj X)
              (M₂.obj X))) :
        Type u))
    ((ModuleCat.Hom.hom
            (NatTrans.app
              (Iso.inv
                (ModuleCat.restrictScalarsId'
                  (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))
                      (𝟙 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))
                        X) :
                    Type u))
                (M₁.obj X) (M₂.obj X))) :
          (a : (↑(M₁.obj X ⊗ M₂.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj (M₁.obj X ⊗ M₂.obj X)) : 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₂) :
      (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj
            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj X) : Type u)) (M₁.obj X)
              (M₂.obj X))) :
        Type u))
have dsimp : Eq (α :=
  (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory (↑(R.obj X) : Type u)) (M₁.obj X)
          (M₂.obj X))) :
    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 :=
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj (M₁.obj X)) (M₁.map (𝟙 X)) :
          (a : (↑(M₁.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj (M₁.obj X)) : Type u))
        m₁ ⊗ₜ[(↑(R.obj X) : 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 :=
            (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj (M₂.obj X)) (M₂.map (𝟙 X)) :
          (a : (↑(M₂.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map (𝟙 X)))).obj (M₂.obj X)) : Type u))
        m₂ :
    TensorProduct (↑(R.obj X) : Type u) (↑(M₁.obj X) : Type u) (↑(M₂.obj X) : Type u))
  (m₁ ⊗ₜ[(↑(R.obj X) : Type u)] m₂ : TensorProduct (↑(R.obj X) : Type u) (↑(M₁.obj X) : Type u) (↑(M₂.obj X) : Type u))
Tactic: dsimp [tensorObjMap]