-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M : PresheafOfModules.{v, v₁, u₁, u} R
Y Z : Cᵒᵖ
f : Y ⟶ Z
r : (↑(R.obj X) : Type u)
x : (↑(forgetToPresheafModuleCatObjObj X hX M Y) : Type v)
⊢ HSMul.hSMul (α := (↑(R.obj Z) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              (R.map f) :
            (a : (↑(R.obj Y) : Type u)) → (↑(R.obj Z) : Type u))
          ((RingCat.Hom.hom (R.map (hX.to Y)) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u)) r :
            (↑(R.obj Y) : Type u)) :
        (↑(R.obj Z) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M.map f) :
            (a : (↑(M.obj Y) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v)) =
    HSMul.hSMul (α := (↑(R.obj Z) : Type u)) (β := (↑(M.obj Z) : Type v))
      ((RingCat.Hom.hom (R.map (hX.to Z)) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Z) : Type u)) r :
        (↑(R.obj Z) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M.map f) :
            (a : (↑(M.obj Y) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
have rw : HSMul.hSMul (α := (↑(R.obj Z) : Type u)) (β :=
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
            (R.map (hX.to Y ≫ f)) :
          (a : (↑(R.obj X) : Type u)) → (↑(R.obj Z) : Type u))
        r :
      (↑(R.obj Z) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map f) :
          (a : (↑(M.obj Y) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v)) =
  HSMul.hSMul (α := (↑(R.obj Z) : Type u)) (β := (↑(M.obj Z) : Type v))
    ((RingCat.Hom.hom (R.map (hX.to Z)) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Z) : Type u)) r :
      (↑(R.obj Z) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map f) :
          (a : (↑(M.obj Y) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (M.obj Z)) : Type v))
Tactic: rw [← RingCat.comp_apply, ← R.map_comp]