-- 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
Y : ModuleCat S
s : S
z : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))
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
zero :
  (lift
          {
            toFun := fun (s : S) ↦
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } :
        (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (HSMul.hSMul (β :=
        (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))) s 0) =
    HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
      ((lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ :
                  (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
              map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        0)
tmul :
  ∀ (s' : (↑((restrictScalars f).obj (of S S)) : Type u₂)) (y : (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))),
    (lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (HSMul.hSMul (β :=
          (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))) s
          (s' ⊗ₜ[R] y)) =
      HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
        ((lift
                {
                  toFun := fun (s : S) ↦
                    { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ :
                      (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
                  map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
            (s' ⊗ₜ[R] y) :
          (↑Y : Type (max u₂ u_1)))
add :
  ∀ (x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u_1 u₂)))
    (ih1 :
      (lift
              {
                toFun := fun (s : S) ↦
                  { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ } :
            (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (s • x) =
        HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
          ((lift
                  {
                    toFun := fun (s : S) ↦
                      { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ :
                        (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
                    map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
                (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
              x :
            (↑Y : Type (max u₂ u_1))))
    (ih2 :
      (lift
              {
                toFun := fun (s : S) ↦
                  { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ } :
            (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          (s • y) =
        HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
          ((lift
                  {
                    toFun := fun (s : S) ↦
                      { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ :
                        (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
                    map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
                (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
              y :
            (↑Y : Type (max u₂ u_1)))),
    (lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
              map_add' := ⋯, map_smul' := ⋯ } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        (s • (x + y)) =
      HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
        ((lift
                {
                  toFun := fun (s : S) ↦
                    { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ :
                      (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
                  map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
              (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
            (x + y) :
          (↑Y : Type (max u₂ u_1)))
⊢ (lift
          {
            toFun := fun (s : S) ↦
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } :
        (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (s • z) =
    HSMul.hSMul (α := S) (β := (↑Y : Type (max u₂ u_1))) ((RingHom.id S : (a : S) → S) s : S)
      ((lift
              {
                toFun := fun (s : S) ↦
                  { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ :
                    (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
                map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          z :
        (↑Y : Type (max u₂ u_1)))

Tactic:
induction z using TensorProduct.induction_on with
      | zero => rw [smul_zero, map_zero, smul_zero]
      | tmul s' y => simp [mul_smul]
      | add _ _ ih1 ih2 => rw [smul_add, map_add, map_add, ih1, ih2, smul_add]

Premises used: smul_zero, map_zero, map_add, TensorProduct.tmul, SemigroupAction.mul_smul, smul_add