-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat.{u_1, u₁} R
Y : ModuleCat.{u_1, u₂} S
s : S
g : X ⟶ (restrictScalars f).obj Y
r : R
x : (↑X : Type u_1)
rw :
  ({
          toFun := fun (x : (↑X : Type u_1)) ↦
            HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦
                      (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) g :
                    (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
                  x :
                (↑((restrictScalars f).obj Y) : Type u_1)),
          map_add' := ⋯ } :
        (a : (↑X : Type u_1)) → (↑Y : Type u_1))
      (r • x) =
    HSMul.hSMul (α := R) (β := (↑Y : Type u_1)) ((RingHom.id R : (a : R) → R) r : R)
      (({
              toFun := fun (x : (↑X : Type u_1)) ↦
                HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
                  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦
                          (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) g :
                        (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
                      x :
                    (↑((restrictScalars f).obj Y) : Type u_1)),
              map_add' := ⋯ : (↑X : Type u_1) →ₙ+ (↑Y : Type u_1) } :
            (a : (↑X : Type u_1)) → (↑Y : Type u_1))
          x :
        (↑Y : Type u_1))
rw₁ :
  HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
              (CC := carrier) g :
            (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
          (r • x) :
        (↑((restrictScalars f).obj Y) : Type u_1)) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
                (CC := carrier) g :
              (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
            x :
          (↑((restrictScalars f).obj Y) : Type u_1)))
⊢ AddHom.toFun
      {
        toFun := fun (x : (↑X : Type u_1)) ↦
          HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
            ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
                    (CC := carrier) g :
                  (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
                x :
              (↑((restrictScalars f).obj Y) : Type u_1)),
        map_add' := ⋯ }
      (r • x) =
    HSMul.hSMul (α := R) (β := (↑Y : Type u_1)) ((RingHom.id R : (a : R) → R) r : R)
      (AddHom.toFun
        {
          toFun := fun (x : (↑X : Type u_1)) ↦
            HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
              ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦
                      (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC := carrier) g :
                    (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
                  x :
                (↑((restrictScalars f).obj Y) : Type u_1)),
          map_add' := ⋯ : (↑X : Type u_1) →ₙ+ (↑Y : Type u_1) }
        x)
have rw₂ : HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1)) (CC :=
            carrier) g :
          (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
        (r • x) :
      (↑((restrictScalars f).obj Y) : Type u_1)) =
  r •
    HSMul.hSMul (β := (↑((restrictScalars f).obj Y) : Type u_1)) s
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u₁} R) ↦ (↑x1 : Type u_1) →ₗ[R] (↑x2 : Type u_1))
              (CC := carrier) g :
            (a : (↑X : Type u_1)) → (↑((restrictScalars f).obj Y) : Type u_1))
          x :
        (↑((restrictScalars f).obj Y) : Type u_1))
Tactic: rw [AddHom.toFun_eq_coe, AddHom.coe_mk, RingHom.id_apply, map_smul, smul_comm r s (g x : Y)]