-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings (goal)
Goal:
C : Type u'
inst : Category.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
M' : PresheafOfModules.{v, v', u', u} R'
α : R ⟶ R'
X Y : Cᵒᵖ
f : X ⟶ Y
r : (↑(R.obj X) : Type u)
x : (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).obj (M'.obj X)) : Type v)
eq :
  Eq (α := (↑(R'.obj Y) : Type u))
    ((RingCat.Hom.hom (α.app Y) : (a : (↑(R.obj Y) : Type u)) → (↑(R'.obj Y) : Type u))
        ((RingCat.Hom.hom (R.map f) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u)) r : (↑(R.obj Y) : Type u)) :
      (↑(R'.obj Y) : Type u))
    ((RingCat.Hom.hom (R'.map f) : (a : (↑(R'.obj X) : Type u)) → (↑(R'.obj Y) : Type u))
        ((RingCat.Hom.hom (α.app X) : (a : (↑(R.obj X) : Type u)) → (↑(R'.obj X) : Type u)) r :
          (↑(R'.obj X) : Type u)) :
      (↑(R'.obj Y) : Type u))
⊢ HSMul.hSMul (α := (↑(R'.obj Y) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : 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 X) : Type u)) → (↑(R'.obj Y) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  RingCat.carrier) (α.app X) :
                (a : (↑(R.obj X) : Type u)) → (↑(R'.obj X) : Type u))
              r :
            (↑(R'.obj X) : Type u)) :
        (↑(R'.obj Y) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M'.map f) :
            (a : (↑(M'.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v)) =
    HSMul.hSMul (α := (↑(R.obj X) : Type u)) (β :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app Y))).obj (M'.obj Y))) :
        Type v))
      ((RingHom.id (↑(R.obj X) : Type u) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj X) : Type u)) r :
        (↑(R.obj X) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
              LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
                (↑x2 : Type v))
              (CC := ModuleCat.carrier) (M'.map f) :
            (a : (↑(M'.obj X) : Type v)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
have rw : HSMul.hSMul (α := (↑(R'.obj Y) : Type u)) (β :=
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
    ((RingCat.Hom.hom (α.app Y) : (a : (↑(R.obj Y) : Type u)) → (↑(R'.obj Y) : Type u))
        ((RingCat.Hom.hom (R.map f) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj Y) : Type u)) r : (↑(R.obj Y) : Type u)) :
      (↑(R'.obj Y) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M'.map f) :
          (a : (↑(M'.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v)) =
  HSMul.hSMul (α := (↑(R.obj X) : Type u)) (β :=
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
          ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app Y))).obj (M'.obj Y))) :
      Type v))
    ((RingHom.id (↑(R.obj X) : Type u) : (a : (↑(R.obj X) : Type u)) → (↑(R.obj X) : Type u)) r : (↑(R.obj X) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R'.obj X) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R'.obj X) : Type u)) (RingHom.id (↑(R'.obj X) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M'.map f) :
          (a : (↑(M'.obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R'.map f))).obj (M'.obj Y)) : Type v))
Tactic: rw [← eq]