-- 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
x y : (↑X : Type u_1)
rw :
  s •
      HAdd.hAdd (α := (↑((restrictScalars f).obj Y) : Type u_1)) (β := (↑((restrictScalars f).obj Y) : Type u_1))
        ((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))
        ((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))
            y :
          (↑((restrictScalars f).obj Y) : 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)) +
      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))
            y :
          (↑((restrictScalars f).obj Y) : 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 + y) :
        (↑((restrictScalars f).obj Y) : 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)) +
      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))
            y :
          (↑((restrictScalars f).obj Y) : Type u_1))
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))
          x :
        (↑((restrictScalars f).obj Y) : 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))
          y :
        (↑((restrictScalars f).obj Y) : 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)) +
    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))
          y :
        (↑((restrictScalars f).obj Y) : Type u_1))
Tactic: rw [map_add, smul_add]