-- 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 R
Y : ModuleCat S
g : (extendScalars f).obj X ⟶ Y
x x_1 : (↑X : Type (max u₂ u_1))
rw :
  (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
          (CC := carrier) g :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (HAdd.hAdd (α := (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) (1 ⊗ₜ[R] x)
        (1 ⊗ₜ[R] x_1)) =
    HAdd.hAdd (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) (β :=
      (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] x) :
        (↑Y : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] x_1) :
        (↑Y : Type (max u₂ u_1)))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
          (CC := carrier) g :
        (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (1 ⊗ₜ[R] (x + x_1)) =
    HAdd.hAdd (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) (β :=
      (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] x) :
        (↑Y : Type (max u₂ u_1)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦
              (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
            (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (1 ⊗ₜ[R] x_1) :
        (↑Y : Type (max u₂ u_1)))
have rw₁ : HAdd.hAdd (α := (↑Y : Type (max u₂ u_1))) (β := (↑Y : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (1 ⊗ₜ[R] x) :
      (↑Y : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (1 ⊗ₜ[R] x_1) :
      (↑Y : Type (max u₂ u_1))) =
  HAdd.hAdd (α := (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) (β :=
    (↑((restrictScalars f).obj Y) : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (1 ⊗ₜ[R] x) :
      (↑Y : Type (max u₂ u_1)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat S) ↦ (↑x1 : Type (max u₂ u_1)) →ₗ[S] (↑x2 : Type (max u₂ u_1)))
            (CC := carrier) g :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (1 ⊗ₜ[R] x_1) :
      (↑Y : Type (max u₂ u_1)))
Tactic: rw [tmul_add, map_add]