-- 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))
f : M₁ ⟶ M₂
g : M₃ ⟶ M₄
X Y : Cᵒᵖ
φ : X ⟶ Y
m₁ : (↑(M₁.obj X) : Type u)
m₃ : (↑(M₃.obj X) : Type u)
⊢ Eq (α :=
    (↑(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))
                φ)))
          ((tensorObj M₂ M₄).obj Y)) :
      Type u))
    ((ModuleCat.Hom.hom
            ((tensorObj M₁ M₃).map φ ≫
              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.app Y ⊗ₘ g.app Y)) :
          (a : (↑(M₁.obj X ⊗ M₃.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).obj
                  ((tensorObj M₂ M₄).obj Y)) :
              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
              (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))
                  φ)))
            ((tensorObj M₂ M₄).obj Y)) :
        Type u))
    ((ModuleCat.Hom.hom ((f.app X ⊗ₘ g.app X) ≫ (tensorObj M₂ M₄).map φ) :
          (a : (↑(M₁.obj X ⊗ M₃.obj X) : Type u)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map φ))).obj
                  ((tensorObj M₂ M₄).obj Y)) :
              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
              (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))
                  φ)))
            ((tensorObj M₂ M₄).obj Y)) :
        Type u))
have dsimp : 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))
      ((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))
        (m₁ ⊗ₜ[(↑(R.obj X) : 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: dsimp