-- 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 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R (↑Y : Type (max u₂ u_1)) := Module.compHom (↑Y : Type (max u₂ u_1)) f
s : S
x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))
ih1 :
  (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (s • x) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          x :
        (↑Y : Type (max u₂ u_1)))
ih2 :
  (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (s • y) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          y :
        (↑Y : Type (max u₂ u_1)))
refine_3 :
  (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (s • x + s • y) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          (x + y) :
        (↑Y : Type (max u₂ u_1)))
refine_3₁ :
  HAdd.hAdd (α := (↑Y : Type (max u₂ u_1))) (β := (↑Y : Type (max u₂ u_1)))
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          (s • x) :
        (↑Y : Type (max u₂ u_1)))
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          (s • y) :
        (↑Y : Type (max u₂ u_1))) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          (x + y) :
        (↑Y : Type (max u₂ u_1)))
refine_3₂ :
  HAdd.hAdd (β := (↑Y : Type (max u₂ u_1)))
      (HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            x :
          (↑Y : Type (max u₂ u_1))))
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          (s • y) :
        (↑Y : Type (max u₂ u_1))) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          (x + y) :
        (↑Y : Type (max u₂ u_1)))
refine_3₃ :
  HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            x :
          (↑Y : Type (max u₂ u_1))) +
      HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            y :
          (↑Y : Type (max u₂ u_1))) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          (x + y) :
        (↑Y : Type (max u₂ u_1)))
refine_3₄ :
  HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            x :
          (↑Y : Type (max u₂ u_1))) +
      HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            y :
          (↑Y : Type (max u₂ u_1))) =
    s •
      HAdd.hAdd (α := (↑Y : Type (max u₂ u_1))) (β := (↑Y : Type (max u₂ u_1)))
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            x :
          (↑Y : Type (max u₂ u_1)))
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            y :
          (↑Y : Type (max u₂ u_1)))
refine_3₅ refine_3₆ :
  HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            x :
          (↑Y : Type (max u₂ u_1))) +
      HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            y :
          (↑Y : Type (max u₂ u_1))) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            x :
          (↑Y : Type (max u₂ u_1))) +
      HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
        ((lift
                { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                  map_smul' := ⋯ :
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
                (↑Y : Type (max u₂ u_1)))
            y :
          (↑Y : Type (max u₂ u_1)))
⊢ (lift
          { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
            map_smul' := ⋯ } :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) → (↑Y : Type (max u₂ u_1)))
      (s • (x + y)) =
    HSMul.hSMul (β := (↑Y : Type (max u₂ u_1))) s
      ((lift
              { toFun := fun (s : (↑((restrictScalars f).obj (of S S)) : Type u₂)) ↦ evalAt f s g, map_add' := ⋯,
                map_smul' := ⋯ :
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑X : Type (max u_1 u₂)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max u_1 u₂))) →
              (↑Y : Type (max u₂ u_1)))
          (x + y) :
        (↑Y : Type (max u₂ u_1)))

Tactic:
rw [smul_add, map_add, ih1, ih2, map_add, smul_add]

Premises used: map_add, smul_add