-- 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 Y : Cᵒᵖ
f : X ⟶ Y
a :
  (↑(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₁ : (↑(M₁.obj X) : Type u)
m₂ : (↑(M₂.obj X) : Type u)
⊢ (fun (m₁ : (↑(M₁.obj X) : Type u)) (m₂ : (↑(M₂.obj X) : 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 f) :
                (a : (↑(M₁.obj X) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).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 f) :
                (a : (↑(M₂.obj X) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).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)))
      (a • m₁) m₂ =
    HSMul.hSMul (β :=
      (↑((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))
      a
      ((fun (m₁ : (↑(M₁.obj X) : Type u)) (m₂ : (↑(M₂.obj X) : 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 f) :
                  (a : (↑(M₁.obj X) : Type u)) →
                    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).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 f) :
                  (a : (↑(M₂.obj X) : Type u)) →
                    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).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)))
        m₁ m₂)
have dsimp : (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))
      (a • 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₂ =
  HSMul.hSMul (β :=
    (↑((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))
    a
    ((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: dsimp