∀ (R : Type u_4) [inst : CommSemiring R] (S : Type u_5) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type u_1}
  [inst_3 : DecidableEq ι₂] (M₁' : Type u_2) (M₂ : ι₂ → Type u_3) [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'] (s : S)
  (t : TensorProduct R M₁' (DirectSum ι₂ fun i => M₂ i)),
  (TensorProduct.directSumRight R M₁' M₂).toAddEquiv.toFun (s • t) =
    (RingHom.id S) s • (TensorProduct.directSumRight R M₁' M₂).toAddEquiv.toFun t