-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
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 : Ring R
inst_3 : Ring S
f : R →+* S
Y : ModuleCat.{u_1, u₂} S
y1 y2 : (↑Y : Type u_1)
s : S
⊢ Eq.{u_1 + 1} (α := (↑((restrictScalars f).obj Y) : Type u_1))
    ((((CoextendScalars.equiv f ((restrictScalars f).obj Y) :
                (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y) : Type u_1))
              ((LinearEquiv.symm (CoextendScalars.equiv f ((restrictScalars f).obj Y)) :
                  (a :
                      (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y) : Type u_1)) →
                    (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1)))
                { toFun := fun (s : S) ↦ s • (y1 + y2), map_add' := ⋯, map_smul' := ⋯ }) :
            LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂)
              (↑((restrictScalars f).obj Y) : Type u_1)) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y) : Type u_1))
        s :
      (↑((restrictScalars f).obj Y) : Type u_1))
    ((((CoextendScalars.equiv f ((restrictScalars f).obj Y) :
                (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y) : Type u_1))
              (HAdd.hAdd (α := (↑((restrictScalars f ⋙ coextendScalars f).obj Y) : Type (max u₂ u_1))) (β :=
                (↑((restrictScalars f ⋙ coextendScalars f).obj Y) : Type (max u₂ u_1)))
                ((LinearEquiv.symm (CoextendScalars.equiv f ((restrictScalars f).obj Y)) :
                      (a :
                          (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                            (↑((restrictScalars f).obj Y) : Type u_1)) →
                        (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1)))
                    { toFun := fun (s : S) ↦ s • y1, map_add' := ⋯, map_smul' := ⋯ } :
                  (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1)))
                ((LinearEquiv.symm (CoextendScalars.equiv f ((restrictScalars f).obj Y)) :
                      (a :
                          (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                            (↑((restrictScalars f).obj Y) : Type u_1)) →
                        (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1)))
                    { toFun := fun (s : S) ↦ s • y2, map_add' := ⋯, map_smul' := ⋯ } :
                  (↑((coextendScalars f).obj ((restrictScalars f).obj Y)) : Type (max u₂ u_1)))) :
            LinearMap.{u₁, u₁, u₂, u_1} (RingHom.id R) (↑((restrictScalars f).obj (of S S)) : Type u₂)
              (↑((restrictScalars f).obj Y) : Type u_1)) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y) : Type u_1))
        s :
      (↑((restrictScalars f).obj Y) : Type u_1))

Tactic:
simp [smul_add]

Premises used: smul_add